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

[bugfix] Attempt at fixing enqueue bug

Browse source 
When we enqueue an atom at level 0, we expect it to stay unconditionally
true whatever happens. However, if it happens that the atom is alrady
true at a level strictly greater than 0 (but lower than base_level),
then enqueue_bool would simply do nothing. To fix this, there is a new
function enqueue_root which modifies in place the level and reason of
the propagated atom if it is already true.
Additionally, enqueue_bool now requires that the atom be undecided,
since if it not (i.e if it is propagated while already decided) it is
most likely a bug.
This commit is contained in:
Guillaume Bury 2016-11-09 00:24:41 +01:00
parent d681e247ed
commit 443a3b0731
1 changed files with 25 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/core/internal.ml
View file

@ -473,19 +473,30 @@ module Make
Log.debugf 0 "Trying to enqueue a false literal: %a" (fun k->k St.pp_atom a); Log.debugf 0 "Trying to enqueue a false literal: %a" (fun k->k St.pp_atom a);
assert false assert false
end; end;
if not a.is_true then begin assert (not a.is_true && a.var.v_level < 0 &&
assert (a.var.v_level < 0 && a.var.reason = None && lvl >= 0); a.var.reason = None && lvl >= 0);
let reason = let reason =
if lvl > 0 then reason if lvl > 0 then reason
else simpl_reason reason else simpl_reason reason
in in
a.is_true <- true; a.is_true <- true;
a.var.v_level <- lvl; a.var.v_level <- lvl;
a.var.reason <- Some reason; a.var.reason <- Some reason;
Vec.push env.elt_queue (of_atom a); Vec.push env.elt_queue (of_atom a);
Log.debugf 20 "Enqueue (%d): %a" Log.debugf 20 "Enqueue (%d): %a"
(fun k->k (Vec.size env.elt_queue) pp_atom a) (fun k->k (Vec.size env.elt_queue) pp_atom a)
end
(* 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 *) (* MCsat semantic assignment *)
let enqueue_assign l value lvl = let enqueue_assign l value lvl =
@ -787,7 +798,7 @@ module Make
Vec.pop vec; Vec.pop vec;
report_unsat clause report_unsat clause
end else end else
enqueue_bool a 0 (Bcp clause) enqueue_root a 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,