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

allow propagation of lits under base_level

Browse source
This commit is contained in:
Simon Cruanes 2016-07-27 18:16:26 +02:00
parent 3e9c0d3a1e
commit 73c2500b05
1 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/core/internal.ml
View file

@ -414,11 +414,17 @@ module Make
for c = env.elt_head to Vec.size env.elt_queue - 1 do for c = env.elt_head to Vec.size env.elt_queue - 1 do
match (Vec.get env.elt_queue c) with match (Vec.get env.elt_queue c) with
(* A literal is unassigned, we nedd to add it back to (* A literal is unassigned, we nedd to add it back to
the heap of potentially assignable literals. *) the heap of potentially assignable literals, unless it has
a level lower than [lvl], in which case we just move it back. *)
| Lit l -> | Lit l ->
l.assigned <- None; if l.l_level <= lvl then begin
l.l_level <- -1; Vec.set env.elt_queue env.elt_head (of_lit l);
insert_var_order (elt_of_lit l) env.elt_head <- env.elt_head + 1
end else begin
l.assigned <- None;
l.l_level <- -1;
insert_var_order (elt_of_lit l)
end
(* A variable is not true/false anymore, one of two things can happen: *) (* A variable is not true/false anymore, one of two things can happen: *)
| Atom a -> | Atom a ->
if a.var.v_level <= lvl then begin if a.var.v_level <= lvl then begin
@ -543,8 +549,9 @@ module Make
| [] -> env.base_level | [] -> env.base_level
| [a] -> | [a] ->
assert is_uip; assert is_uip;
env.base_level 0
| a :: b :: r -> | a :: b :: r ->
assert(a.var.v_level > env.base_level);
if is_uip then ( if is_uip then (
(* backtrack below [a], so we can propagate [not a] *) (* backtrack below [a], so we can propagate [not a] *)
assert(a.var.v_level > b.var.v_level); assert(a.var.v_level > b.var.v_level);