From cddf914ce63a747211c2a8c444eb6f3d0d490dec Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 13 Mar 2015 14:23:40 +0100 Subject: [PATCH] Better proving of hypothesis --- solver/mcsolver.ml | 2 +- solver/res_intf.ml | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 2316543d..da3f94f6 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -501,7 +501,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) L.debug 10 "Adding clause : %a" St.pp_clause init0; try if Proof.has_been_proved init0 then raise Trivial; - assert (Proof.is_proven init0); let atoms, init = partition atoms init0 in let size = List.length atoms in match atoms with @@ -514,6 +513,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) else make_clause name atoms size true (History [init0]) in L.debug 1 "New clause : %a" St.pp_clause init0; + Proof.prove clause; attach_clause clause; Vec.push env.clauses clause; if a.neg.is_true then begin diff --git a/solver/res_intf.ml b/solver/res_intf.ml index 24072b36..78344400 100644 --- a/solver/res_intf.ml +++ b/solver/res_intf.ml @@ -52,6 +52,9 @@ module type S = sig hyptohesis and theory lemmas always have trivial derivations, and as such [is_proven c] (where [c] is a hypothesis or lemma) will always return [true] and add it to the proof graph. *) + val prove : clause -> unit + (** Same as 'learn', but works on single clauses instead of vectors. *) + val learn : clause Vec.t -> unit (** Learn and build proofs for the clause in the vector. Clauses in the vector should be in the order they were learned. *)