Add forgetful propagation

src/core/internal.ml

@@ -907,9 +907,19 @@ module Make
        be done *)
     Stack.push c env.clauses_to_add
 
-  let slice_propagate f l =
+  let slice_propagate f = function
-    let a = atom f in
+    | Plugin_intf.Eval l ->
-    enqueue_semantic a l
+      let a = atom f in
+      enqueue_semantic a l
+    | Plugin_intf.Consequence (causes, proof) ->
+      let l = List.rev_map atom causes in
+      if List.for_all (fun a -> a.is_true) l then
+        let p = atom f in
+        let c = make_clause (fresh_tname ())
+            (p :: List.map (fun a -> a.neg) l) (Lemma proof) in
+        enqueue_bool p (decision_level ()) (Bcp c)
+      else
+        raise (Invalid_argument "Msat.Internal.slice_propagate")
 
   let current_slice (): (_,_,_) Plugin_intf.slice = {
     Plugin_intf.start = env.th_head;

src/core/plugin_intf.ml

@@ -53,6 +53,14 @@ type ('term, 'formula) assumption =
   | Assign of 'term * 'term (** The first term is assigned to the second *)
 (** Asusmptions made by the core SAT solver. *)
 
+type ('term, 'formula, 'proof) reason =
+  | Eval of 'term list
+  | Consequence of 'formula list * 'proof
+(** The type of reasons for propagations of a formula [f].
+    [Semantic lvl] means that [f] is true because of the assignments whose level is [<= lvl].
+    [Consequence (l, p)] means that the formulas in [l] imply [f]. The proof should be a proof
+    of the clause "[l] implies [f]". *)
+
 type ('term, 'formula, 'proof) slice = {
   start : int;                                (** Start of the slice *)
   length : int;                               (** Length of the slice *)
@@ -60,7 +68,8 @@ type ('term, 'formula, 'proof) slice = {
                                                   Should only be called on integers [i] s.t.
                                                   [start <= i < start + length] *)
   push : 'formula list -> 'proof -> unit;     (** Add a clause to the solver. *)
-  propagate : 'formula -> 'term list -> unit; (** Propagate a formula, i.e. the theory can
+  propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit;
+                                              (** Propagate a formula, i.e. the theory can
                                                   evaluate the formula to be true (see the
                                                   definition of {!type:eval_res} *)
 }

src/core/theory_intf.ml

@@ -34,12 +34,17 @@ type ('formula, 'proof) res = ('formula, 'proof) Plugin_intf.res =
     current set of assumptions, i.e must have been encountered in a slice. *)
 
 type ('form, 'proof) slice = {
-  start : int;                        (** Start of the slice *)
+  start : int;                          (** Start of the slice *)
-  length : int;                       (** Length of the slice *)
+  length : int;                         (** Length of the slice *)
-  get : int -> 'form;                 (** Accesor for the formuals in the slice.
+  get : int -> 'form;                   (** Accesor for the formuals in the slice.
-                                          Should only be called on integers [i] s.t.
+                                            Should only be called on integers [i] s.t.
-                                          [start <= i < start + length] *)
+                                            [start <= i < start + length] *)
-  push : 'form list -> 'proof -> unit; (** Allows to add to the solver a clause. *)
+  push : 'form list -> 'proof -> unit;  (** Allows to add to the solver a clause. *)
+  propagate : 'form -> 'form list -> 'proof -> unit;
+  (** [propagate lit causes proof] informs the solver to propagate [lit], with the reason
+    that the clause [causes => lit] is a theory tautology. It is faster than pushing
+    the associated clause but the clause will not be remembered by the sat solver,
+    i.e it will not be used by the solver to do boolean propagation. *)
 }
 (** The type for a slice. Slices are some kind of view of the current
     propagation queue. They allow to look at the propagated literals,

src/solver/solver.ml

@@ -39,16 +39,22 @@ module Plugin(E : Formula_intf.S)
 
   let current_level = Th.current_level
 
-  let assume_get s i =
+  let assume_get get =
-    match s.Plugin_intf.get i with
+    function i ->
+    match get i with
     | Plugin_intf.Lit f -> f
     | _ -> assert false
 
+  let assume_propagate propagate =
+    fun f l proof ->
+      propagate f (Plugin_intf.Consequence (l, proof))
+
   let mk_slice s = {
       Theory_intf.start = s.Plugin_intf.start;
       length = s.Plugin_intf.length;
-      get = assume_get s;
+      get = assume_get s.Plugin_intf.get;
       push = s.Plugin_intf.push;
+      propagate = assume_propagate s.Plugin_intf.propagate;
     }
 
   let assume s = Th.assume (mk_slice s)