New clauses are memorized, and redundant ones eliminated.

solver/mcproof.ml

@@ -83,6 +83,8 @@ module Make(St : Mcsolver_types.S) = struct
     res
 
   (* Adding hyptoheses *)
+  let has_been_proved c = H.mem proof (to_list c)
+
   let is_proved (c, cl) =
     if H.mem proof cl then
       true

solver/mcsolver.ml

@@ -495,11 +495,13 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
         partition_aux [] [] [] true atoms
 
   let add_clause name atoms history =
-    if env.is_unsat then raise Unsat;
+    if env.is_unsat then raise Unsat; (* is it necessary ? *)
     let init_name = name in
     let init0 = make_clause init_name atoms (List.length atoms) (history <> History []) history in
-    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);
+      L.debug 10 "Adding clause : %a" St.pp_clause init0;
       let atoms, init = partition atoms init0 in
       let size = List.length atoms in
       match atoms with
@@ -528,7 +530,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
         enqueue_bool a 0 (Bcp (Some init0))
     with Trivial -> ()
 
-
   let progress_estimate () =
     let prg = ref 0. in
     let nbv = to_float (nb_vars()) in

solver/res.ml

@@ -83,6 +83,8 @@ module Make(St : Solver_types.S) = struct
     res
 
   (* Adding hyptoheses *)
+  let has_been_proved c = H.mem proof (to_list c)
+
   let is_proved (c, cl) =
     if H.mem proof cl then
       true

solver/res_intf.ml

@@ -42,8 +42,15 @@ module type S = sig
 
   (** {3 Proof building functions} *)
 
+  val has_been_proved : clause -> bool
+  (** Returns [true] if the clause is part of the current proof graph. This function does not alter
+      the proof graph (contrary to [is_proven]). *)
+
   val is_proven : clause -> bool
-  (** Returns [true] if the clause has a derivation in the current proof graph, and [false] otherwise. *)
+  (** Checks if the given clause has a derivation in the current state. Whatever the result,
+      new proven clauses (including the given clause) may be added to the proof graph. In particular,
+      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 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. *)

solver/solver.ml

@@ -400,6 +400,8 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
     let init0 = make_clause ?tag init_name atoms (List.length atoms) (history <> History []) history in
     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