simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 04:35:35 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Handle new clauses unsat at level >0 && <=base_lvl

Browse source
This commit is contained in:
Guillaume Bury 2016-07-29 21:00:24 +02:00
parent 6eeaa8513c
commit 5fdffe1f85
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/core/internal.ml
View file

@ -749,6 +749,13 @@ module Make
match atoms with match atoms with
| [] -> | [] ->
report_unsat clause 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::_ -> | a::b::_ ->
if a.neg.is_true then begin if a.neg.is_true then begin
(* Atoms need to be sorted in decreasing order of decision level, (* Atoms need to be sorted in decreasing order of decision level,
@ -766,10 +773,6 @@ module Make
enqueue_bool a lvl (Bcp clause) enqueue_bool a lvl (Bcp clause)
end end
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 -> with Trivial ->
Vec.push vec init; Vec.push vec init;
Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init) Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init)