simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-29 04:44:52 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revert "Removed an error that was raised for tautological conflict clauses"

Browse source 
This reverts commit 803b61c7dc.
This commit is contained in:
Guillaume Bury 2015-01-29 15:49:01 +01:00
parent 436dc49111
commit 0e84c5bfb3
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
solver/mcproof.ml
View file

@ -78,7 +78,10 @@ module Make(St : Mcsolver_types.S) = struct
for i = 0 to Vec.size v - 1 do for i = 0 to Vec.size v - 1 do
l := (Vec.get v i) :: !l l := (Vec.get v i) :: !l
done; done;
List.sort_uniq compare_atoms !l let l, res = resolve (List.sort_uniq compare_atoms !l) in
if l <> [] then
raise (Resolution_error "Input cause is a tautology");
res
(* Adding hyptoheses *) (* Adding hyptoheses *)
let is_unit_hyp = function let is_unit_hyp = function

5
solver/mcsolver.ml
View file

@ -370,10 +370,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
var_bump_activity a.var; var_bump_activity a.var;
history := d :: !history; history := d :: !history;
c := res c := res
| _ -> | _ -> assert false
L.debug 0 "Found %d resolution lits" (List.length tmp);
List.iter (fun c -> L.debug 0 " |- %a" St.pp_atom c) tmp;
assert false
end end
| Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a | Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a
| Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a) | Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a)