From d3702d1e1f76cdc4a664926093ac2150940f9f7b Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 1 Mar 2019 19:13:24 -0600
Subject: [PATCH] refactor: fix issues found by @gbury

---
 src/core/Internal.ml    | 19 ++++++++++++++++---
 src/core/Solver_intf.ml | 13 +++++++++----
 2 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index b6da8fce..fad444d3 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -1691,6 +1691,14 @@ module Make(Plugin : PLUGIN)
     Log.debugf 5 (fun k->k "(@[@{<yellow>sat.th.raise-conflict@}@ %a@])" Clause.debug c);
     raise_notrace (Th_conflict c)
 
+  let check_consequence_lits_false_ l : unit =
+    match List.find Atom.is_true l with
+    | a ->
+      invalid_argf
+        "slice.acts_propagate:@ Consequence should contain only true literals, but %a isn't"
+        Atom.debug (Atom.neg a)
+    | exception Not_found -> ()
+
   let acts_propagate (st:t) f = function
     | Solver_intf.Eval l ->
       let a = mk_atom st f in
@@ -1701,9 +1709,7 @@ module Make(Plugin : PLUGIN)
       else if Atom.is_false p then (
         let lits, proof = mk_expl() in
         let l = List.rev_map (fun f -> Atom.neg @@ mk_atom st f) lits in
-        if List.exists Atom.is_true l then (
-          invalid_argf "slice.acts_propagate: Consequence should contain only true literals"
-        );
+        check_consequence_lits_false_ l;
         let c = Clause.make_removable (p :: l) (Lemma proof) in
         raise_notrace (Th_conflict c)
       ) else (
@@ -1711,6 +1717,13 @@ module Make(Plugin : PLUGIN)
         let c = lazy (
           let lits, proof = mk_expl () in
           let l = List.rev_map (fun f -> Atom.neg @@ mk_atom st f) lits in
+          (* note: we can check that invariant here in the [lazy] block,
+             as conflict analysis will run in an environment where
+             the literals should be true anyway, since it's an extension of the
+             current trail
+             (otherwise the propagated lit would have been backtracked and
+             discarded already.) *)
+          check_consequence_lits_false_ l;
           Clause.make_removable (p :: l) (Lemma proof)
         ) in
         let level = decision_level st in
diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml
index e6ffffb1..5815e659 100644
--- a/src/core/Solver_intf.ml
+++ b/src/core/Solver_intf.ml
@@ -80,15 +80,20 @@ type ('term, 'formula, 'proof) reason =
   (** [Consequence (l, p)] means that the formulas in [l] imply the propagated
       formula [f]. The proof should be a proof of the clause "[l] implies [f]".
 
-      invariant: in [Consequence (l,p)], all elements of [l] must be true in
+      invariant: in [Consequence (fun () -> l,p)], all elements of [l] must be true in
       the current trail.
 
-      note on lazyiness: the justification is suspended (using [unit -> …])
+      {b note} on lazyiness: the justification is suspended (using [unit -> …])
       to avoid potentially costly computations that might never be used
       if this literal is backtracked without participating in a conflict.
-      However, if the theory isn't robust wrt backtracking an subsequent changes,
+      Therefore the function that produces [(l,p)] needs only be safe in
+      trails (partial models) that are conservative extensions of the current
+      trail.
+      If the theory isn't robust w.r.t. extensions of the trail (e.g. if
+      its internal state undergoes significant changes),
       it can be easier to produce the explanation eagerly when
-      propagating, and then use [Consequence (fun () -> expl, proof)].
+      propagating, and then use [Consequence (fun () -> expl, proof)] with
+      the already produced [(expl,proof)] tuple.
   *)
 (** The type of reasons for propagations of a formula [f]. *)