From 77af72e7394e18e8ad108b3fb5449e36102d86c7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 19 Feb 2018 21:27:26 -0600 Subject: [PATCH] fix bugs in SAT solver - new atoms must always be added to heap if not present - fix slices dimensions at creation, do not depend on mutable indices --- src/sat/Internal.ml | 71 +++++++++++++++++++---------------- src/sat/Solver.ml | 6 +-- src/sat/Solver_types.ml | 7 ++-- src/smt/Congruence_closure.ml | 14 +++---- src/smt/Solver_types.ml | 2 +- src/smt/Term.ml | 3 +- src/smt/Term.mli | 2 +- src/smt/Term_cell.ml | 2 +- src/smt/Term_cell.mli | 2 +- 9 files changed, 55 insertions(+), 54 deletions(-) diff --git a/src/sat/Internal.ml b/src/sat/Internal.ml index fd5f5cbe..eef0398a 100644 --- a/src/sat/Internal.ml +++ b/src/sat/Internal.ml @@ -160,7 +160,6 @@ module Make let[@inline] nb_clauses st = Vec.size st.clauses_hyps let[@inline] decision_level st = Vec.size st.elt_levels let[@inline] base_level st = Vec.size st.user_levels - let[@inline] mk_atom st (f:St.formula) : atom = Atom.make st.st f (* [redo_down_to_level_0 f ~undo] performs [f] now. Upon backtracking before current level, some undo actions scheduled by [f] @@ -194,21 +193,22 @@ module Make is done. Uses a heap (implemented in {!Heap}), to keep track of variable activity. *) let insert_var_order st (v:var) : unit = - if not (Var.in_heap v) then ( - (* remove variable when we backtrack *) + if not (Var.in_heap v) && Var.level v < 0 then ( + (* new variable that is not assigned, add to heap. + remember to remove variable when we backtrack *) on_backtrack_if_not_at_0 st (fun () -> H.remove st.order v); H.insert st.order v; ) - let new_atom ~permanent st (p:formula) : unit = - let a = mk_atom st p in + let new_atom ~permanent st (p:formula) : St.atom = + let a = Atom.make st.st p in if permanent then ( - (* TODO: also internalize term… *) redo_down_to_level_0 st (fun () -> insert_var_order st a.var) ) else ( insert_var_order st a.var - ) + ); + a (* Rather than iterate over all the heap when we want to decrease all the variables/literals activity, we instead increase the value by which @@ -458,7 +458,8 @@ module Make rebuild the whole resolution tree when we want to prove [a]. *) let c' = Clause.make_l l (History (cl :: history)) in Log.debugf 5 - (fun k -> k "Simplified reason: @[%a@,%a@]" Clause.debug cl Clause.debug c'); + (fun k -> k "(@[sat.simplified-reason@ :old %a@ :new %a@])" + Clause.debug cl Clause.debug c'); Bcp c' ) | _ -> @@ -768,6 +769,9 @@ module Make permanent Clause.debug init); let vec_for_clause = clause_vector st init in match eliminate_duplicates init with + | exception Trivial -> + Vec.push vec_for_clause init; + Log.debugf 3 (fun k->k "(@[sat.add_clause.ignore-trivial@ %a@])" Clause.debug init) | c -> Log.debugf 5 (fun k -> k "(@[sat.add_clause.after_eliminate_dups@ %a@])" Clause.debug c); let atoms, history = partition c.atoms in @@ -806,7 +810,7 @@ module Make assert (0 < a.var.v_level && a.var.v_level <= base_level st); ) else ( Log.debugf 5 - (fun k->k "(@[sat.add_clause.unit-clause@ :propagating %a@])" Atom.debug a); + (fun k->k "(@[sat.add_clause.unit_clause@ :propagating %a@])" Atom.debug a); (* propagate but without adding the clause. May need to re-propagate after backtracking *) redo_down_to_level_0 st @@ -815,10 +819,11 @@ module Make | a::b::_ -> on_backtrack_if_not_at_0 st (fun () -> Vec.pop vec_for_clause); Vec.push vec_for_clause clause; + (* Atoms need to be sorted in decreasing order of decision level, + or we might watch the wrong literals. *) + put_high_level_atoms_first clause.atoms; if a.neg.is_true then ( - (* Atoms need to be sorted in decreasing order of decision level, - or we might watch the wrong literals. *) - put_high_level_atoms_first clause.atoms; + (* conflict, even the last literal is false *) attach_clause st clause; add_boolean_conflict st clause ) else ( @@ -829,9 +834,6 @@ module Make enqueue_bool st a (Bcp clause) ) ) - | exception Trivial -> - Vec.push vec_for_clause init; - Log.debugf 3 (fun k->k "(@[sat.add_clause.ignore-trivial@ %a@])" Clause.debug init) type watch_res = | Watch_kept @@ -905,15 +907,14 @@ module Make ) done - let slice_iter st (hd:int) (f:_ -> unit) : unit = - let n = Vec.size st.trail in - for i = hd to n-1 do + let slice_iter st (hd:int) (last:int) (f:_ -> unit) : unit = + for i = hd to last-1 do let a = Vec.get st.trail i in f a.lit done let act_push_ ~permanent st (l:formula IArray.t) (lemma:proof): unit = - let atoms = IArray.to_array_map (mk_atom st) l in + let atoms = IArray.to_array_map (new_atom ~permanent st) l in let c = Clause.make atoms (Lemma lemma) in Log.debugf 3 (fun k->k "(@[sat.push_clause@ %a@])" Clause.debug c); add_clause ~permanent st c @@ -924,9 +925,9 @@ module Make (* TODO: ensure that the clause is removed upon backtracking *) let act_propagate (st:t) f causes proof : unit = - let l = List.rev_map (mk_atom st) causes in + let l = List.rev_map (new_atom ~permanent:false st) causes in if List.for_all (fun a -> a.is_true) l then ( - let p = mk_atom st f in + let p = new_atom ~permanent:false st f in let c = Clause.make_l (p :: List.map Atom.neg l) (Lemma proof) in if p.is_true then ( ) else if p.neg.is_true then ( @@ -942,12 +943,12 @@ module Make ) let current_slice st head = Theory_intf.Slice_acts { - slice_iter = slice_iter st head; + slice_iter = slice_iter st head (Vec.size st.trail); } (* full slice, for [if_sat] final check *) let full_slice st = Theory_intf.Slice_acts { - slice_iter = slice_iter st 0; + slice_iter = slice_iter st 0 (Vec.size st.trail); } let act_at_level_0 st () = at_level_0 st @@ -994,7 +995,7 @@ module Make propagate st | Theory_intf.Unsat (l, p) -> (* conflict *) - let l = List.rev_map (mk_atom st) l in + let l = List.rev_map (new_atom ~permanent:false st) l in List.iter (fun a -> insert_var_order st a.var) l; let c = St.Clause.make_l l (Lemma p) in Some c @@ -1013,6 +1014,7 @@ module Make while st.elt_head < Vec.size st.trail do let a = Vec.get st.trail st.elt_head in incr num_props; + Log.debugf 5 (fun k->k "(@sat.propagate_atom@ %a@])" Atom.pp a); propagate_atom st a; st.elt_head <- st.elt_head + 1; done; @@ -1089,10 +1091,14 @@ module Make in value, var.v_level - let eval st lit = fst (eval_level st lit) - + let[@inline] eval st lit = fst (eval_level st lit) let[@inline] unsat_conflict st = st.unsat_conflict + let pp_trail st = + Log.debugf 5 + (fun k -> k "(@[sat.current_trail:@ %a@])" + (Vec.print ~sep:"" Atom.debug) st.trail) + (* fixpoint of propagation and decisions until a model is found, or a conflict is reached *) let solve (st:t) : unit = @@ -1111,6 +1117,7 @@ module Make n_of_learnts := !n_of_learnts *. learntsize_inc | Sat -> assert (st.elt_head = Vec.size st.trail); + pp_trail st; begin match Th.if_sat (theory st) (full_slice st) with | Theory_intf.Sat -> (* if no propagation is to be done, exit; @@ -1119,7 +1126,7 @@ module Make raise Sat ) | Theory_intf.Unsat (l, p) -> - let atoms = List.rev_map (mk_atom st) l in + let atoms = List.rev_map (new_atom ~permanent:false st) l in let c = Clause.make_l atoms (Lemma p) in Log.debugf 3 (fun k -> k "(@[@{sat.theory_conflict_clause@}@ %a@])" Clause.debug c); @@ -1135,7 +1142,7 @@ module Make let assume ~permanent st ?tag cnf = let cs = List.rev_map (fun atoms -> - let atoms = List.rev_map (mk_atom st) atoms in + let atoms = List.rev_map (new_atom ~permanent st) atoms in Clause.make_l ?tag atoms Hyp) cnf in @@ -1146,7 +1153,7 @@ module Make add_clause ~permanent:false st c) cs in - if permanent + if permanent then redo_down_to_level_0 st add_clauses else add_clauses() @@ -1161,9 +1168,7 @@ module Make | Some confl -> report_unsat st confl | None -> - Log.debugf 5 - (fun k -> k "@[Current trail:@,@[%a@]@]" - (Vec.print ~sep:"" Atom.debug) st.trail); + pp_trail st; Log.debug 3 "Creating new user level"; new_decision_level st; Vec.push st.user_levels (Vec.size st.clauses_temp); @@ -1190,7 +1195,7 @@ module Make (* Add local hyps to the current decision level *) let local (st:t) (assumptions:formula list) : unit = let add_lit lit : unit = - let a = mk_atom st lit in + let a = new_atom ~permanent:false st lit in Log.debugf 3 (fun k-> k "(@[sat.local_assumption@ %a@])" Atom.debug a); assert (decision_level st = base_level st); if not a.is_true then ( diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 96c4ee8b..8521302c 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -121,7 +121,7 @@ module Make let[@inline] new_atom ~permanent st a = cleanup_ st; - S.new_atom ~permanent st a + ignore (S.new_atom ~permanent st a) let actions = S.actions @@ -135,7 +135,7 @@ module Make type t = lit let pp = St.Atom.pp - let make = S.mk_atom + let make = S.new_atom ~permanent:false end module Clause = struct @@ -148,7 +148,7 @@ module Make let[@inline] make_l ?tag l : t = St.Clause.make_l ?tag l St.Hyp let of_atoms st ?tag l = - let l = List.map (S.mk_atom st) l in + let l = List.map (S.new_atom ~permanent:false st) l in make_l ?tag l end diff --git a/src/sat/Solver_types.ml b/src/sat/Solver_types.ml index 6446aa2a..1f258ff8 100644 --- a/src/sat/Solver_types.ml +++ b/src/sat/Solver_types.ml @@ -136,8 +136,8 @@ module Make (E : Theory_intf.S) = struct let[@inline] reason v = v.reason let[@inline] weight v = v.v_weight - let[@inline] id v =v.vid - let[@inline] level v =v.v_level + let[@inline] id v = v.vid + let[@inline] level v = v.v_level let[@inline] idx v = v.v_idx let[@inline] set_level v lvl = v.v_level <- lvl @@ -324,8 +324,7 @@ module Make (E : Theory_intf.S) = struct | Hyp -> Format.fprintf out "hyp" | Local -> Format.fprintf out "local" | Lemma _ -> Format.fprintf out "th_lemma" - | History v -> - List.iter (fun c -> Format.fprintf out "%s,@ " (name_of_clause c)) v + | History v -> Util.pp_list (CCFormat.of_to_string name_of_clause) out v let debug out ({atoms=arr; cpremise=cp;_}as c) = Format.fprintf out "%s@[{@[%a@]}@ cpremise={@[%a@]}@]" diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index 3519bcc7..72c45ded 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -123,7 +123,10 @@ let signature cc (t:term): node term_cell option = | App_cst (_, a) when IArray.is_empty a -> None | App_cst (f, a) -> App_cst (f, IArray.map find a) |> CCOpt.return | Custom {view;tc} -> - Custom {tc; view=tc.tc_t_subst find view} |> CCOpt.return + begin match tc.tc_t_subst find view with + | None -> None + | Some u' -> Some (Custom{tc; view=u'}) + end | Bool _ | If _ | Case _ @@ -322,8 +325,7 @@ and update_combine cc = be merged w.r.t. the theories. Side effect: also pushes sub-tasks *) and notify_merge cc (ra:repr) ~into:(rb:repr) (e:explanation): unit = - assert (is_root_ (ra:>node)); - assert (is_root_ (rb:>node)); + assert (is_root_ rb); cc.acts.on_merge ra rb e @@ -546,17 +548,11 @@ let explain_loop (cc : t) : Lit.Set.t = cc.ps_lits let explain_unfold_seq cc (seq:explanation Sequence.t): Lit.Set.t = - Log.debugf 5 - (fun k->k "(@[explain_confict@ (@[%a@])@])" - (Util.pp_seq Explanation.pp) seq); ps_clear cc; Sequence.iter (decompose_explain cc) seq; explain_loop cc let explain_unfold_bag cc (b:explanation Bag.t) : Lit.Set.t = - Log.debugf 5 - (fun k->k "(@[explain_confict@ (@[%a@])@])" - (Util.pp_seq Explanation.pp) (Bag.to_seq b)); match b with | Bag.E -> Lit.Set.empty | Bag.L (E_lit lit) -> Lit.Set.singleton lit diff --git a/src/smt/Solver_types.ml b/src/smt/Solver_types.ml index 2ab553c6..679262b8 100644 --- a/src/smt/Solver_types.ml +++ b/src/smt/Solver_types.ml @@ -56,7 +56,7 @@ and term_view_tc = { tc_t_sub : 'a. 'a term_view_custom -> 'a Sequence.t; (* iter on immediate subterms *) tc_t_abs : 'a. self:'a -> 'a term_view_custom -> 'a * bool; (* remove the sign? *) tc_t_relevant : 'a. 'a term_view_custom -> 'a Sequence.t; (* iter on relevant immediate subterms *) - tc_t_subst : 'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom; (* substitute immediate subterms and canonize *) + tc_t_subst : 'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom option; (* substitute immediate subterms and canonize *) tc_t_explain : 'a. 'a CCEqual.t -> 'a term_view_custom -> 'a term_view_custom -> ('a * 'a) list; (* explain why the two views are equal *) } diff --git a/src/smt/Term.ml b/src/smt/Term.ml index ce7ab70b..02e623cc 100644 --- a/src/smt/Term.ml +++ b/src/smt/Term.ml @@ -26,7 +26,7 @@ type tc = Solver_types.term_view_tc = { tc_t_sub : 'a. 'a custom -> 'a Sequence.t; tc_t_abs : 'a. self:'a -> 'a custom -> 'a * bool; tc_t_relevant : 'a. 'a custom -> 'a Sequence.t; - tc_t_subst : 'a 'b. ('a -> 'b) -> 'a custom -> 'b custom; + tc_t_subst : 'a 'b. ('a -> 'b) -> 'a custom -> 'b custom option; tc_t_explain : 'a. 'a CCEqual.t -> 'a custom -> 'a custom -> ('a * 'a) list; } @@ -112,6 +112,7 @@ let[@inline] is_custom t = match t.term_cell with | _ -> false let[@inline] is_semantic t = match t.term_cell with + | Bool _ -> true | Custom {view;tc} -> tc.tc_t_is_semantic view | _ -> false diff --git a/src/smt/Term.mli b/src/smt/Term.mli index b409591d..904372e2 100644 --- a/src/smt/Term.mli +++ b/src/smt/Term.mli @@ -26,7 +26,7 @@ type tc = Solver_types.term_view_tc = { tc_t_sub : 'a. 'a custom -> 'a Sequence.t; tc_t_abs : 'a. self:'a -> 'a custom -> 'a * bool; tc_t_relevant : 'a. 'a custom -> 'a Sequence.t; - tc_t_subst : 'a 'b. ('a -> 'b) -> 'a custom -> 'b custom; + tc_t_subst : 'a 'b. ('a -> 'b) -> 'a custom -> 'b custom option; tc_t_explain : 'a. 'a CCEqual.t -> 'a custom -> 'a custom -> ('a * 'a) list; } diff --git a/src/smt/Term_cell.ml b/src/smt/Term_cell.ml index 94a2eb71..6a312761 100644 --- a/src/smt/Term_cell.ml +++ b/src/smt/Term_cell.ml @@ -26,7 +26,7 @@ type tc = Solver_types.term_view_tc = { tc_t_abs : 'a. self:'a -> 'a custom -> 'a * bool; tc_t_relevant : 'a. 'a term_view_custom -> 'a Sequence.t; tc_t_subst : - 'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom; + 'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom option; tc_t_explain : 'a. 'a CCEqual.t -> 'a term_view_custom -> 'a term_view_custom -> ('a * 'a) list; } diff --git a/src/smt/Term_cell.mli b/src/smt/Term_cell.mli index e1afa933..99fdfe90 100644 --- a/src/smt/Term_cell.mli +++ b/src/smt/Term_cell.mli @@ -24,7 +24,7 @@ type tc = Solver_types.term_view_tc = { tc_t_abs : 'a. self:'a -> 'a custom -> 'a * bool; tc_t_relevant : 'a. 'a term_view_custom -> 'a Sequence.t; tc_t_subst : - 'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom; + 'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom option; tc_t_explain : 'a. 'a CCEqual.t -> 'a term_view_custom -> 'a term_view_custom -> ('a * 'a) list; }