From 3af700bbd0a3aad1a2cb815fc453194db9dd2cde Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 9 Nov 2016 14:27:50 +0100 Subject: [PATCH] [bugfix] Better fix for propagation at level 0 Previously a fix was introduced to mitigate the fact that some atoms couldn't be propagated at level 0 because of local assumptions. However that fix didn't take into account propagation that implicated the already propagated atom: for instance consider an atom [a] propagted at level 1 because of some local hyp, and then atoms [b] propagated at level 1 because [a] is true in a clause [C = not a \/ b]. If we propagte 0 and modify its level in-place as done in the previous fix, then we should also propagate [b] at level 0, which is hard. Instead of modifying levels in place, we simply store unit clauses at level 0 in a stack, which we transfer to the clauses to add when we pop local hyps. --- src/core/internal.ml | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index 8fea0435..bee00c77 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -30,13 +30,15 @@ module Make clause. *) clauses_hyps : clause Vec.t; - (* clauses assumed (subject to user levels) *) + (* clauses added by the user *) clauses_learnt : clause Vec.t; (* learnt clauses (tautologies true at any time, whatever the user level) *) clauses_temp : clause Vec.t; (* Temp clauses, corresponding to the local assumptions. This vec is used only to have an efficient way to access the list of local assumptions. *) + clauses_root : clause Stack.t; + (* Clauses that should propagate at level 0, but couldn't *) clauses_to_add : clause Stack.t; (* Clauses either assumed or pushed by the theory, waiting to be added. *) @@ -128,6 +130,7 @@ module Make clauses_learnt = Vec.make 0 dummy_clause; clauses_temp = Vec.make 0 dummy_clause; + clauses_root = Stack.create (); clauses_to_add = Stack.create (); th_head = 0; @@ -486,18 +489,6 @@ module Make Log.debugf 20 "Enqueue (%d): %a" (fun k->k (Vec.size env.elt_queue) pp_atom a) - (* Special case for atoms enqueued at level 0 - Indeed atoms true at level 0 are supposed to never disappear, because - we cannot watch a clause with only one atom. This causes a problem when - the atom [a] is already propagated at a level 0 < l <= base_level - In that case, we simply change the level and reason of the propagation. *) - let enqueue_root a clause : unit = - if a.is_true then begin - a.var.v_level <- 0; - a.var.reason <- Some (Bcp clause) - end else - enqueue_bool a ~level:0 (Bcp clause) - (* MCsat semantic assignment *) let enqueue_assign l value lvl = match l.assigned with @@ -797,8 +788,17 @@ module Make Stack.push clause env.clauses_to_add; Vec.pop vec; report_unsat clause + end else if a.is_true then begin + (* If the atom is already true, then it should be because of a local hyp. + However it means we can't propagate it at level 0. In order to not lose + that information, we store the clause in a stack of clauses that we will + add to the solver at the next pop. *) + assert (0 < a.var.v_level && a.var.v_level <= base_level ()); + Stack.push clause env.clauses_root; + Vec.pop vec; + () end else - enqueue_root a clause + enqueue_bool a ~level:0 (Bcp clause) | a::b::_ -> if a.neg.is_true then begin (* Atoms need to be sorted in decreasing order of decision level, @@ -1166,10 +1166,10 @@ module Make env.unsat_conflict <- None; let n = Vec.last env.user_levels in Vec.pop env.user_levels; (* before the [cancel_until]! *) + (* Add the root clauses to the clauses to add *) + Stack.iter (fun c -> Stack.push c env.clauses_to_add) env.clauses_root; + Stack.clear env.clauses_root; (* remove from env.clauses_temp the now invalid caluses. *) - Log.debugf 5 "Popping; temp clauses:" (fun k -> k); - Vec.iter (fun c -> - Log.debugf 5 " %a" (fun k -> k St.pp_clause c)) env.clauses_temp; Vec.shrink env.clauses_temp (Vec.size env.clauses_temp - n); assert (Vec.for_all (fun c -> Array.length c.atoms = 1) env.clauses_temp); assert (Vec.for_all (fun c -> c.atoms.(0).var.v_level <= base_level ()) env.clauses_temp);