From 2caf53c24f82e6e0bdef8a1c499d60c8ba1bfcd4 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 29 Dec 2017 21:29:43 +0100
Subject: [PATCH] expose `{push,pop}` in main solver

---
 src/core/Internal.ml    |  5 +++++
 src/core/Solver.ml      | 37 +++++++++++++++++++++++++++++++------
 src/core/Solver_intf.ml |  8 ++++++++
 3 files changed, 44 insertions(+), 6 deletions(-)

diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index b22c1d92..59d41972 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -115,6 +115,10 @@ module Make
     mutable learntsize_factor : float;
     (* initial limit for the number of learnt clauses, 1/3 of initial
         number of clauses by default *)
+
+    mutable dirty: bool;
+    (* is there a [pop()] on top of the stack for examining
+       current model/proof? *)
   }
 
   (* Starting environment. *)
@@ -146,6 +150,7 @@ module Make
     restart_first = 100;
 
     learntsize_factor = 1. /. 3. ;
+    dirty=false;
   }
 
   let create ?(size=`Big) ?st () : t =
diff --git a/src/core/Solver.ml b/src/core/Solver.ml
index cc64cfaf..a8099c38 100644
--- a/src/core/Solver.ml
+++ b/src/core/Solver.ml
@@ -79,21 +79,41 @@ module Make
     in
     { unsat_conflict; get_proof; }
 
-  (* Wrappers around internal functions*)
-  let assume = S.assume
+  (* clean local state *)
+  let[@inline] cleanup_ (st:t) : unit =
+    if st.S.dirty then (
+      S.pop st; (* reset *)
+      st.S.dirty <- false;
+    )
 
-  let add_clause = S.add_clause
+  (* Wrappers around internal functions*)
+  let[@inline] assume st ?tag cls : unit =
+    cleanup_ st;
+    S.assume st ?tag cls
+
+  let[@inline] add_clause st c : unit =
+    cleanup_ st;
+    S.add_clause st c
 
   let solve (st:t) ?(assumptions=[]) () =
+    cleanup_ st;
     try
-      S.pop st; (* FIXME: what?! *)
       S.push st;
+      st.S.dirty <- true; (* to call [pop] before any other action *)
       S.local st assumptions;
       S.solve st;
       Sat (mk_sat st)
     with S.Unsat ->
       Unsat (mk_unsat st)
 
+  let[@inline] push st =
+    cleanup_ st;
+    S.push st
+
+  let[@inline] pop st =
+    cleanup_ st;
+    S.pop st
+
   let unsat_core = S.Proof.unsat_core
 
   let true_at_level0 st a =
@@ -104,8 +124,13 @@ module Make
 
   let get_tag cl = St.(cl.tag)
 
-  let new_lit = S.new_lit
-  let new_atom = S.new_atom
+  let[@inline] new_lit st t =
+    cleanup_ st;
+    S.new_lit st t
+
+  let[@inline] new_atom st a =
+    cleanup_ st;
+    S.new_atom st a
 
   let export (st:t) : St.clause export =
     let hyps = S.hyps st in
diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml
index ae98b8d0..7bb371ff 100644
--- a/src/core/Solver_intf.ml
+++ b/src/core/Solver_intf.ml
@@ -115,6 +115,14 @@ module type S = sig
   val get_tag : clause -> int option
   (** Recover tag from a clause, if any *)
 
+  val push : t -> unit
+  (** Push a new save point *)
+
+  val pop : t -> unit
+  (** Return to last save point *)
+
+  val pop : t -> unit
+
   val export : t -> clause export
 
   (** {2 Re-export some functions} *)