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

Only pure hypothesis are instantly learned

Browse source
This commit is contained in:
Guillaume Bury 2015-03-13 14:39:48 +01:00
parent 5786e26705
commit 6005652f3f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
solver/mcsolver.ml
View file

@ -501,6 +501,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
L.debug 10 "Adding clause : %a" St.pp_clause init0; L.debug 10 "Adding clause : %a" St.pp_clause init0;
try try
if Proof.has_been_proved init0 then raise Trivial; if Proof.has_been_proved init0 then raise Trivial;
assert (Proof.is_proven init0); (* Important side-effect, DO NOT REMOVE *)
let atoms, init = partition atoms init0 in let atoms, init = partition atoms init0 in
let size = List.length atoms in let size = List.length atoms in
match atoms with match atoms with
@ -513,7 +514,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
else make_clause name atoms size true (History [init0]) else make_clause name atoms size true (History [init0])
in in
L.debug 1 "New clause : %a" St.pp_clause clause; L.debug 1 "New clause : %a" St.pp_clause clause;
Proof.prove clause;
attach_clause clause; attach_clause clause;
Vec.push env.clauses clause; Vec.push env.clauses clause;
if a.neg.is_true then begin if a.neg.is_true then begin