simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

remove Either

Browse source
This commit is contained in:
Simon Cruanes 2016-07-22 13:19:16 +02:00
parent 51f10d7ad5
commit 8b1d657695
5 changed files with 44 additions and 68 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/core/internal.ml
View file

@ -255,8 +255,8 @@ module Make
its subterms. its subterms.
*) *)
let insert_var_order = function let insert_var_order = function
| Either.Left l -> Iheap.insert f_weight env.order l.lid | E_lit l -> Iheap.insert f_weight env.order l.lid
| Either.Right v -> | E_var v ->
Iheap.insert f_weight env.order v.vid; Iheap.insert f_weight env.order v.vid;
iter_sub (fun t -> Iheap.insert f_weight env.order t.lid) v iter_sub (fun t -> Iheap.insert f_weight env.order t.lid) v
@ -456,12 +456,12 @@ module Make
match (Vec.get env.elt_queue c) with match (Vec.get env.elt_queue c) with
(* A literal is unassigned, we nedd to add it back to (* A literal is unassigned, we nedd to add it back to
the heap of potentially assignable literals. *) the heap of potentially assignable literals. *)
| Either.Left l -> | Lit l ->
l.assigned <- None; l.assigned <- None;
l.l_level <- -1; l.l_level <- -1;
insert_var_order (elt_of_lit l) insert_var_order (elt_of_lit l)
(* A variable is not true/false anymore, one of two things can happen: *) (* A variable is not true/false anymore, one of two things can happen: *)
| Either.Right a -> | Atom a ->
if a.var.v_level <= lvl then begin if a.var.v_level <= lvl then begin
(* It is a semantic propagation, which can be late, and has a level (* It is a semantic propagation, which can be late, and has a level
lower than where we backtrack, so we just move it to the head lower than where we backtrack, so we just move it to the head
@ -594,8 +594,8 @@ module Make
decr tr_ind; decr tr_ind;
Log.debugf 20 "Looking at trail element %d" (fun k->k !tr_ind); Log.debugf 20 "Looking at trail element %d" (fun k->k !tr_ind);
match Vec.get env.elt_queue !tr_ind with match Vec.get env.elt_queue !tr_ind with
| Either.Left _ -> () | Lit _ -> ()
| Either.Right a -> | Atom a ->
begin match a.var.reason with begin match a.var.reason with
| Some (Bcp d) -> | Some (Bcp d) ->
let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in
@ -619,7 +619,7 @@ module Make
let get_atom i = let get_atom i =
match Vec.get env.elt_queue i with match Vec.get env.elt_queue i with
| Either.Left _ -> assert false | Either.Right x -> x | Lit _ -> assert false | Atom x -> x
let analyze_sat c_clause = let analyze_sat c_clause =
let pathC = ref 0 in let pathC = ref 0 in
@ -829,11 +829,11 @@ module Make
let slice_get i = let slice_get i =
match Vec.get env.elt_queue i with match Vec.get env.elt_queue i with
| Either.Right a -> | Atom a ->
Plugin_intf.Lit a.lit Plugin_intf.Lit a.lit
| Either.Left {l_level; term; assigned = Some v} -> | Lit {l_level; term; assigned = Some v} ->
Plugin_intf.Assign (term, v, l_level) Plugin_intf.Assign (term, v, l_level)
| Either.Left _ -> assert false | Lit _ -> assert false
let slice_push l lemma = let slice_push l lemma =
let atoms = List.rev_map (fun x -> new_atom x) l in let atoms = List.rev_map (fun x -> new_atom x) l in
@ -900,8 +900,8 @@ module Make
let res = ref None in let res = ref None in
while env.elt_head < Vec.size env.elt_queue do while env.elt_head < Vec.size env.elt_queue do
begin match Vec.get env.elt_queue env.elt_head with begin match Vec.get env.elt_queue env.elt_head with
| Either.Left _ -> () | Lit _ -> ()
| Either.Right a -> | Atom a ->
incr num_props; incr num_props;
propagate_atom a res propagate_atom a res
end; end;
@ -1011,7 +1011,7 @@ module Make
| None -> | None ->
begin try begin try
begin match St.get_elt (Iheap.remove_min f_weight env.order) with begin match St.get_elt (Iheap.remove_min f_weight env.order) with
| Either.Left l -> | E_lit l ->
if l.l_level >= 0 then if l.l_level >= 0 then
pick_branch_lit () pick_branch_lit ()
else begin else begin
@ -1021,7 +1021,7 @@ module Make
let current_level = decision_level () in let current_level = decision_level () in
enqueue_assign l value current_level enqueue_assign l value current_level
end end
| Either.Right v -> | E_var v ->
pick_branch_aux v.pa pick_branch_aux v.pa
end end
with Not_found -> raise Sat with Not_found -> raise Sat
@ -1142,8 +1142,8 @@ module Make
let model () = let model () =
let opt = function Some a -> a | None -> assert false in let opt = function Some a -> a | None -> assert false in
Vec.fold (fun acc e -> match e with Vec.fold (fun acc e -> match e with
| Either.Left v -> (v.term, opt v.assigned) :: acc | Lit v -> (v.term, opt v.assigned) :: acc
| Either.Right _ -> acc | Atom _ -> acc
) [] env.elt_queue ) [] env.elt_queue
(* Backtrack to decision_level 0, with trail_lim && theory env specified *) (* Backtrack to decision_level 0, with trail_lim && theory env specified *)
@ -1153,11 +1153,11 @@ module Make
env.elt_head <- elt_lvl; env.elt_head <- elt_lvl;
for c = env.elt_head to Vec.size env.elt_queue - 1 do for c = env.elt_head to Vec.size env.elt_queue - 1 do
match Vec.get env.elt_queue c with match Vec.get env.elt_queue c with
| Either.Left l -> | Lit l ->
l.assigned <- None; l.assigned <- None;
l.l_level <- -1; l.l_level <- -1;
insert_var_order (elt_of_lit l) insert_var_order (elt_of_lit l)
| Either.Right a -> | Atom a ->
begin match a.var.reason with begin match a.var.reason with
| Some Bcp { c_level } when c_level > push_lvl -> | Some Bcp { c_level } when c_level > push_lvl ->
a.is_true <- false; a.is_true <- false;
@ -1210,8 +1210,8 @@ module Make
(if i = ul.ul_th_lvl then "*" else " ") (if i = ul.ul_th_lvl then "*" else " ")
i (fun fmt e -> i (fun fmt e ->
match e with match e with
| Either.Left l -> St.pp_lit fmt l | Lit l -> St.pp_lit fmt l
| Either.Right a -> St.pp_atom fmt a) | Atom a -> St.pp_atom fmt a)
(Vec.get env.elt_queue i) (Vec.get env.elt_queue i)
done done
in in

33
src/core/solver_types.ml
View file

@ -75,7 +75,9 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
| Lemma of proof | Lemma of proof
| History of clause list | History of clause list
type elt = (lit, var) Either.t type elt =
| E_lit of lit
| E_var of var
(* Dummy values *) (* Dummy values *)
let dummy_lit = E.dummy let dummy_lit = E.dummy
@ -118,7 +120,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
let f_map = MF.create 4096 let f_map = MF.create 4096
let t_map = MT.create 4096 let t_map = MT.create 4096
let vars = Vec.make 107 (Either.mk_right dummy_var) let vars = Vec.make 107 (E_var dummy_var)
let nb_elt () = Vec.size vars let nb_elt () = Vec.size vars
let get_elt i = Vec.get vars i let get_elt i = Vec.get vars i
let iter_elt f = Vec.iter f vars let iter_elt f = Vec.iter f vars
@ -137,7 +139,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
} in } in
incr cpt_mk_var; incr cpt_mk_var;
MT.add t_map t res; MT.add t_map t res;
Vec.push vars (Either.mk_left res); Vec.push vars (E_lit res);
res res
let make_boolean_var : formula -> var * Expr_intf.negated = let make_boolean_var : formula -> var * Expr_intf.negated =
@ -172,7 +174,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
MF.add f_map lit var; MF.add f_map lit var;
incr cpt_mk_var; incr cpt_mk_var;
Vec.push vars (Either.mk_right var); Vec.push vars (E_var var);
var, negated var, negated
let add_term t = make_semantic_var t let add_term t = make_semantic_var t
@ -203,27 +205,28 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
let empty_clause = make_clause "Empty" [] (History []) let empty_clause = make_clause "Empty" [] (History [])
(* Decisions & propagations *) (* Decisions & propagations *)
type t = (lit, atom) Either.t type t =
| Lit of lit
| Atom of atom
let of_lit = Either.mk_left let of_lit l = Lit l
let of_atom = Either.mk_right let of_atom a = Atom a
let destruct = Either.destruct
(* Elements *) (* Elements *)
let elt_of_lit = Either.mk_left let elt_of_lit l = E_lit l
let elt_of_var = Either.mk_right let elt_of_var v = E_var v
let get_elt_id = function let get_elt_id = function
| Either.Left l -> l.lid | Either.Right v -> v.vid | E_lit l -> l.lid | E_var v -> v.vid
let get_elt_level = function let get_elt_level = function
| Either.Left l -> l.l_level | Either.Right v -> v.v_level | E_lit l -> l.l_level | E_var v -> v.v_level
let get_elt_weight = function let get_elt_weight = function
| Either.Left l -> l.l_weight | Either.Right v -> v.v_weight | E_lit l -> l.l_weight | E_var v -> v.v_weight
let set_elt_level e lvl = match e with let set_elt_level e lvl = match e with
| Either.Left l -> l.l_level <- lvl | Either.Right v -> v.v_level <- lvl | E_lit l -> l.l_level <- lvl | E_var v -> v.v_level <- lvl
let set_elt_weight e w = match e with let set_elt_weight e w = match e with
| Either.Left l -> l.l_weight <- w | Either.Right v -> v.v_weight <- w | E_lit l -> l.l_weight <- w | E_var v -> v.v_weight <- w
(* Name generation *) (* Name generation *)
let fresh_lname = let fresh_lname =

8
src/core/solver_types_intf.ml
View file

@ -71,7 +71,9 @@ module type S = sig
| History of clause list | History of clause list
(** {2 Decisions and propagations} *) (** {2 Decisions and propagations} *)
type t = (lit, atom) Either.t type t =
| Lit of lit
| Atom of atom
(** Either a lit of an atom *) (** Either a lit of an atom *)
val of_lit : lit -> t val of_lit : lit -> t
@ -80,7 +82,9 @@ module type S = sig
(** {2 Elements} *) (** {2 Elements} *)
type elt = (lit, var) Either.t type elt =
| E_lit of lit
| E_var of var
(** Either a lit of a var *) (** Either a lit of a var *)
val nb_elt : unit -> int val nb_elt : unit -> int

16
src/util/either.ml
View file

@ -1,16 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
type ('a, 'b) t =
| Left of 'a
| Right of 'b
let mk_left a = Left a
let mk_right b = Right b
let destruct e f_left f_right = match e with
| Left a -> f_left a
| Right b -> f_right b

15
src/util/either.mli
View file

@ -1,15 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
type ('a, 'b) t =
| Left of 'a
| Right of 'b
val mk_left : 'a -> ('a, 'b) t
val mk_right : 'b -> ('a, 'b) t
val destruct : ('a, 'b) t ->
('a -> 'c) -> ('b -> 'c) -> 'c