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

fix(cc): public add function must also saturate CC

Browse source
This commit is contained in:
Simon Cruanes 2018-05-28 01:22:58 -05:00
parent 1d99547856
commit 10d394a9c3
2 changed files with 14 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/sat/Internal.ml
View file

@ -979,7 +979,8 @@ module Make (Th : Theory_intf.S) = struct
); );
let level = decision_level st in let level = decision_level st in
Log.debugf 5 Log.debugf 5
(fun k->k "(@[sat.enqueue_bool@ :lvl %d@ %a@])" level Atom.debug a); (fun k->k "(@[sat.enqueue_bool@ :lvl %d@ %a@ :reason %a@])"
level Atom.debug a Atom.debug_reason (level,Some reason));
(* backtrack assignment if needed. Trail is backtracked automatically. *) (* backtrack assignment if needed. Trail is backtracked automatically. *)
assert (not a.is_true && a.var.v_level < 0 && a.var.reason = None); assert (not a.is_true && a.var.v_level < 0 && a.var.reason = None);
a.is_true <- true; a.is_true <- true;
@ -1428,7 +1429,7 @@ module Make (Th : Theory_intf.S) = struct
while st.elt_head < Vec.size st.trail do while st.elt_head < Vec.size st.trail do
let a = Vec.get st.trail st.elt_head in let a = Vec.get st.trail st.elt_head in
incr num_props; incr num_props;
Log.debugf 5 (fun k->k "(@[sat.bcp.propagate_atom@ %a@])" Atom.pp a); Log.debugf 5 (fun k->k "(@[sat.bcp.propagate_atom_on_trail@ %a@])" Atom.pp a);
propagate_atom st a; propagate_atom st a;
st.elt_head <- st.elt_head + 1; st.elt_head <- st.elt_head + 1;
done; done;

15
src/smt/Congruence_closure.ml
View file

@ -338,7 +338,7 @@ let rec update_pending (cc:t): unit =
assert (Cst.equal f1 f2); assert (Cst.equal f1 f2);
assert (IArray.length a1 = IArray.length a2); assert (IArray.length a1 = IArray.length a2);
Explanation.mk_merges @@ Explanation.mk_merges @@
IArray.map2 (fun u1 u2 -> add cc u1, add cc u2) a1 a2 IArray.map2 (fun u1 u2 -> add_ cc u1, add_ cc u2) a1 a2
| If _, _ | App_cst _, _ | Bool _, _ | If _, _ | App_cst _, _ | Bool _, _
-> assert false -> assert false
in in
@ -445,7 +445,7 @@ and add_new_term cc (t:term) : node =
in in
(* add sub-term to [cc], and register [n] to its parents *) (* add sub-term to [cc], and register [n] to its parents *)
let add_sub_t (u:term) : unit = let add_sub_t (u:term) : unit =
let n_u = add cc u in let n_u = add_ cc u in
add_to_parents_of_sub_node n_u add_to_parents_of_sub_node n_u
in in
(* register sub-terms, add [t] to their parent list *) (* register sub-terms, add [t] to their parent list *)
@ -470,11 +470,18 @@ and add_new_term cc (t:term) : node =
n n
(* add a term *) (* add a term *)
and[@inline] add cc t : node = and[@inline] add_ cc t : node =
try Term.Tbl.find cc.tbl t try Term.Tbl.find cc.tbl t
with Not_found -> add_new_term cc t with Not_found -> add_new_term cc t
let[@inline] add_seq cc seq = seq (fun t -> ignore @@ add cc t) let add cc t : node =
let n = add_ cc t in
update_pending cc;
n
let add_seq cc seq =
seq (fun t -> ignore @@ add_ cc t);
update_pending cc
(* before we push tasks into [pending], ensure they are removed when we backtrack *) (* before we push tasks into [pending], ensure they are removed when we backtrack *)
let reset_on_backtrack cc : unit = let reset_on_backtrack cc : unit =