From 035002fd95a968de321bdb1758c0d564d36238ab Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 4 Aug 2016 22:18:39 +0200
Subject: [PATCH] Add forgetful propagation

This may be not really needed if late propagations can be done, as the
current code could allow. To think about...
---
 src/core/internal.ml    | 18 ++++++++++++++----
 src/core/plugin_intf.ml | 10 +++++++++-
 src/core/theory_intf.ml |  7 ++++++-
 src/solver/solver.ml    | 12 +++++++++---
 4 files changed, 38 insertions(+), 9 deletions(-)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index db29c488..3630f336 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -905,10 +905,20 @@ module Make
        be done *)
     Stack.push c env.clauses_to_add
 
-  let slice_propagate f lvl =
-    let a = atom f in
-    Iheap.grow_to_by_double env.order (St.nb_elt ());
-    enqueue_bool a lvl (Semantic lvl)
+  let slice_propagate f = function
+    | Plugin_intf.Eval lvl ->
+      let a = atom f in
+      Iheap.grow_to_by_double env.order (St.nb_elt ());
+      enqueue_bool a lvl (Semantic lvl)
+    | 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;
diff --git a/src/core/plugin_intf.ml b/src/core/plugin_intf.ml
index afe5c526..40d2fba1 100644
--- a/src/core/plugin_intf.ml
+++ b/src/core/plugin_intf.ml
@@ -34,12 +34,20 @@ type ('term, 'formula) assumption =
 (** Asusmptions made by the core SAT solver. Can be either a formula, or an assignment.
     Assignemnt are given a level. *)
 
+type ('formula, 'proof) reason =
+  | Eval of int
+  | 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;
   length : int;
   get : int -> ('term, 'formula) assumption;
   push : 'formula list -> 'proof -> unit;
-  propagate : 'formula -> int -> unit;
+  propagate : 'formula -> ('formula, 'proof) reason -> unit;
 }
 (** The type for a slice of litterals to assume/propagate in the theory.
     [get] operations should only be used for integers [ start <= i < start + length].
diff --git a/src/core/theory_intf.ml b/src/core/theory_intf.ml
index 2cdd121f..170b042a 100644
--- a/src/core/theory_intf.ml
+++ b/src/core/theory_intf.ml
@@ -25,10 +25,15 @@ type ('form, 'proof) slice = {
   length : int;
   get : int -> 'form;
   push : 'form list -> 'proof -> unit;
+  propagate : 'form -> 'form list -> 'proof -> unit;
 }
 (** The type for a slice of literals to assume/propagate in the theory.
     [get] operations should only be used for integers [ start <= i < start + length].
-    [push clause proof] allows to add a tautological clause to the sat solver. *)
+    [push clause proof] allows to add a tautological clause to the sat solver.
+    [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. *)
 
 module type S = sig
   (** Signature for theories to be given to the Solver. *)
diff --git a/src/solver/solver.ml b/src/solver/solver.ml
index 274d3962..b9965980 100644
--- a/src/solver/solver.ml
+++ b/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 =
-    match s.Plugin_intf.get i with
+  let assume_get get =
+    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)