From 5fdffe1f855637e0c3381d03c5165af742cd03cb Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 29 Jul 2016 21:00:24 +0200 Subject: [PATCH] Handle new clauses unsat at level >0 && <=base_lvl --- src/core/internal.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index 4e77b073..75d0ef3f 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -749,6 +749,13 @@ module Make match atoms with | [] -> report_unsat clause + | [a] -> + Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a); + cancel_until env.base_level; + if a.neg.is_true then begin + report_unsat clause + end else + enqueue_bool a 0 (Bcp clause) | a::b::_ -> if a.neg.is_true then begin (* Atoms need to be sorted in decreasing order of decision level, @@ -766,10 +773,6 @@ module Make enqueue_bool a lvl (Bcp clause) end end - | [a] -> - Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a); - cancel_until env.base_level; - enqueue_bool a 0 (Bcp clause) with Trivial -> Vec.push vec init; Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init)