From d5d7234afcf007ef49327dd1b9a68dbef3afafd9 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 3 Nov 2016 16:04:51 +0100 Subject: [PATCH] [bugfix] Avoid forgetting 1 atom clauses When a new clause with only 1 atom is added with (usually from simplifying a theory lemma), the usual strategy is to backtrack to the base level, then propagate the atom. However, when the atom is already false at base level, Unsat is raised, in which case the information that the atom must be true is lost. To avoid that, the single atom clause is simply pushed back in the stack of clauses to add, so that it will be re-examined later. --- src/core/internal.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index 50896a26..ab14a589 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -753,8 +753,8 @@ module Make Log.debugf 90 "Adding clause:@[%a@]" (fun k -> k St.pp_clause init); let vec = match init.cpremise with | Hyp -> env.clauses_hyps - | Lemma _ -> env.clauses_learnt - | Local | History _ -> assert false + | Local -> env.clauses_temp + | History _ | Lemma _ -> env.clauses_learnt in try let atoms, history = partition init.atoms in @@ -776,6 +776,13 @@ module Make Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a); cancel_until (base_level ()); if a.neg.is_true then begin + (* Since we cannot propagate the atom [a], in order to not lose + the information that [a] must be true, we add clause to the list + of clauses to add, so that it will be e-examined later. + Also, in order to avoid it being twice in a clause vector, we pop + the vector where it was added. *) + Stack.push clause env.clauses_to_add; + Vec.pop vec; report_unsat clause end else enqueue_bool a 0 (Bcp clause)