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

[bugfix] uip clause detection was wrong

Browse source
This commit is contained in:
Guillaume Bury 2015-02-06 17:05:37 +01:00
parent 3203dadb8d
commit 7a5e8e082d
1 changed files with 12 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
solver/mcsolver.ml
View file

@ -338,15 +338,23 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
let history = ref [c_clause] in let history = ref [c_clause] in
clause_bump_activity c_clause; clause_bump_activity c_clause;
let is_semantic a = match a.var.tag.reason with let is_semantic a = match a.var.tag.reason with
| Semantic _ -> true | Semantic _ -> true
| _ -> false | _ -> false
in
let is_decision a = match a.var.tag.reason with
| Bcp None -> true
| _ -> false
in in
try while true do try while true do
let _, atoms = max_lvl_atoms !c in let _, atoms = max_lvl_atoms !c in
L.debug 15 "Current conflict clause :"; L.debug 15 "Current conflict clause :";
List.iter (fun a -> L.debug 15 " |- %a" St.pp_atom a) !c; List.iter (fun a -> L.debug 15 " |- %a" St.pp_atom a) !c;
match atoms with match atoms with
| [] | _ :: [] -> | [] ->
L.debug 15 "Found Empty clause";
is_uip := true;
raise Exit
| [a] when is_decision a ->
L.debug 15 "Found UIP clause"; L.debug 15 "Found UIP clause";
is_uip := true; is_uip := true;
raise Exit raise Exit
@ -356,6 +364,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
| _ -> | _ ->
decr tr_ind; decr tr_ind;
L.debug 20 "Looking at trail element %d" !tr_ind; L.debug 20 "Looking at trail element %d" !tr_ind;
assert (!tr_ind >= 0);
Either.destruct (Vec.get env.trail !tr_ind) Either.destruct (Vec.get env.trail !tr_ind)
(fun v -> L.debug 15 "%a" St.pp_semantic_var v) (fun v -> L.debug 15 "%a" St.pp_semantic_var v)
(fun a -> match a.var.tag.reason with (fun a -> match a.var.tag.reason with