From c125fdafa6a6d5bda29cb678117c6d52db7e2230 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 22 Jun 2018 21:01:22 -0500 Subject: [PATCH] fix(sat): use `Conflict` exn to signal conflict on `add_clause` --- src/sat/Internal.ml | 79 ++++++++++++++++++--------------------------- 1 file changed, 32 insertions(+), 47 deletions(-) diff --git a/src/sat/Internal.ml b/src/sat/Internal.ml index 0db0df99..ba6a56ff 100644 --- a/src/sat/Internal.ml +++ b/src/sat/Internal.ml @@ -963,6 +963,7 @@ module Make (Th : Theory_intf.S) = struct backtrack_down_to st b_lvl; ); assert (Vec.size st.elt_levels = Vec.size st.backtrack_levels); + Log.debugf 15 (fun k->k "(@[sat.trail@ %a@])" (Vec.print Atom.debug) st.trail); () (* Unsatisfiability is signaled through an exception, since it can happen @@ -1075,7 +1076,7 @@ module Make (Th : Theory_intf.S) = struct Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms in Log.debugf 5 - (fun k -> k "(@[sat.analyzing-conflict (%d)@ %a@])" conflict_level Clause.debug c_clause); + (fun k -> k "(@[sat.analyzing-conflict :lvl %d@ :clause %a@])" conflict_level Clause.debug c_clause); while !cond do let clause = !c in Log.debugf 5 (fun k->k"(@[sat.resolving-clause@ %a@])" Clause.debug clause); @@ -1149,28 +1150,29 @@ module Make (Th : Theory_intf.S) = struct - if clause is already true, probably just do nothing - if clause is unit, propagate lit immediately (with clause as justification) but do not add clause + - if clause is false, raise Conflict - permanent stuff: just re-add it on backtrack *) - let rec add_clause_ st (c:clause) : unit = + let add_clause_ st (c0:clause) : unit = Log.debugf 5 - (fun k -> k "(@[@{sat.add_clause@}@ %a@])" Clause.debug c); - assert (not @@ Clause.dead c); - match eliminate_duplicates c with + (fun k -> k "(@[@{sat.add_clause@}@ %a@])" Clause.debug c0); + assert (not @@ Clause.dead c0); + match eliminate_duplicates c0 with | exception Trivial -> - Log.debugf 3 (fun k->k "(@[sat.add_clause.ignore-trivial@ %a@])" Clause.debug c) + Log.debugf 3 (fun k->k "(@[sat.add_clause.ignore-trivial@ %a@])" Clause.debug c0) | c -> - Log.debugf 5 (fun k -> k "(@[sat.add_clause.after_eliminate_dups@ %a@])" Clause.debug c); - (* sort atoms by decreasing level of decision (undecided first) *) - let atoms = sort_lits_by_level c.atoms in - (* update order of atoms *) - assert (List.length atoms = Array.length c.atoms); - List.iteri (fun i a -> c.atoms.(i) <- a) atoms; + if c != c0 then ( + Log.debugf 5 (fun k -> k "(@[sat.add_clause.after-eliminate-dups@ %a@])" Clause.debug c); + ); + (* update order of atoms to put the two highest-level/unassigned ones first, + so that watch literals are correct *) + put_high_level_atoms_first c.atoms; Log.debugf 3 (fun k->k "(@[sat.add_clause.new_clause@ %a@])" Clause.debug c); - match atoms with - | [] -> + match c.atoms with + | [||] -> (* report Unsat immediately *) report_unsat st c - | [a] -> + | [|a|] -> if a.neg.is_true then ( Log.debug 5 "(sat.add_clause: false unit clause, report unsat)"; report_unsat st c @@ -1183,26 +1185,21 @@ module Make (Th : Theory_intf.S) = struct (fun k->k "(@[sat.add_clause.unit_clause@ :propagating %a@])" Atom.debug a); enqueue_bool st a (Bcp c) ) - | _::_::_ -> + | _ -> Vec.push st.clauses c; - (* Atoms need to be sorted in decreasing order of decision level, - or we might watch the wrong literals. *) - put_high_level_atoms_first c.atoms; attach_clause st c; let a = c.atoms.(0) in let b = c.atoms.(1) in if a.neg.is_true then ( (* conflict, even the last literal is false *) - add_boolean_conflict st c + raise (Conflict c) ) else if b.neg.is_true && not a.is_true && not a.neg.is_true then ( - let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in - cancel_until st (max lvl (base_level st)); enqueue_bool st a (Bcp c) ) (* Add a new clause, simplifying, propagating, and backtracking if the clause is false in the current trail *) - and add_clause ~permanent st (c:clause) : unit = + let add_clause ~permanent st (c:clause) : unit = add_clause_ st c; if permanent then ( (* need to re-internalize *) @@ -1217,7 +1214,7 @@ module Make (Th : Theory_intf.S) = struct - backtrack - report unsat if conflict at level 0 *) - and add_boolean_conflict st (confl:clause): unit = + let add_boolean_conflict st (confl:clause): unit = Log.debugf 3 (fun k -> k "(@[@{sat.boolean-conflict@}@ %a@ :decision-lvl %d@])" Clause.debug confl (decision_level st)); @@ -1325,7 +1322,8 @@ module Make (Th : Theory_intf.S) = struct Log.debugf 3 (fun k->k "(@[sat.push_clause_from_theory@ :permanent %B@ %a@])" permanent Clause.debug c); - add_clause ~permanent st c + add_clause ~permanent st c; + () let act_push_local = act_push_ ~permanent:false let act_push_persistent = act_push_ ~permanent:true @@ -1338,10 +1336,10 @@ module Make (Th : Theory_intf.S) = struct if p.is_true then ( ) else if p.neg.is_true then ( (* propagate other lits in the clause *) - add_clause ~permanent:false st c + add_clause ~permanent:false st c; ) else ( insert_var_order st p.var; - enqueue_bool st p (Bcp c) + enqueue_bool st p (Bcp c); ) ) else ( Error.errorf "(@[sat.act_propagate.invalid_guard@ :guard %a@ \ @@ -1364,8 +1362,6 @@ module Make (Th : Theory_intf.S) = struct end in (module A) - let act_at_level_0 st () = at_level_0 st - let actions st: (formula,lemma) Theory_intf.actions = let module A = struct type nonrec formula = formula @@ -1411,8 +1407,6 @@ module Make (Th : Theory_intf.S) = struct | Theory_intf.Unsat (l, p) -> (* conflict *) let l = List.rev_map (Atom.make st) l in - (* TODO: do that when the conflict clause is added *) - List.iter (fun a -> insert_var_order st a.var) l; let c = Clause.make_l l (Lemma p) in Some c ) @@ -1422,22 +1416,13 @@ module Make (Th : Theory_intf.S) = struct and propagate (st:t) : clause option = (* Now, check that the situation is sane *) assert (st.elt_head <= Vec.size st.trail); - if st.elt_head = Vec.size st.trail then ( - theory_propagate st - ) else ( - let num_props = ref 0 in - let res = ref None in - 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.bcp.propagate_atom_on_trail@ %a@])" Atom.pp a); - propagate_atom st a; - st.elt_head <- st.elt_head + 1; - done; - match !res with - | None -> theory_propagate st - | _ -> !res - ) + while st.elt_head < Vec.size st.trail do + let a = Vec.get st.trail st.elt_head in + Log.debugf 5 (fun k->k "(@[sat.bcp.propagate_atom_on_trail@ %a@])" Atom.pp a); + propagate_atom st a; + st.elt_head <- st.elt_head + 1; + done; + theory_propagate st (* remove some learnt clauses NOTE: so far we do not forget learnt clauses. We could, as long as