Some SAT stuff, not doing anything special yet, just to keep it in sync.

9 files changed, 136 insertions, 43 deletions

diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index 9cde8ae2d..366cc34c8 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
+	-I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@srcdir@/../../include
 AM_CXXFLAGS = -Wall -fvisibility=hidden -DNDEBUG
 
 noinst_LTLIBRARIES = libminisat.la
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index e99870654..771d79f62 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -19,6 +19,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "Solver.h"
 #include "Sort.h"
+#include "prop/sat.h"
 #include <cmath>
 
 //=================================================================================================
@@ -28,10 +29,14 @@ namespace CVC4 {
 namespace prop {
 namespace minisat {
 
-Solver::Solver() :
+Solver::Solver(SatSolver* proxy, context::Context* context) :
+
+    // SMT stuff
+    proxy(proxy)
+  , context(context)
 
     // Parameters: (formerly in 'SearchParams')
-    var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02)
+  , var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02)
   , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
 
     // More parameters:
@@ -159,14 +164,20 @@ bool Solver::satisfied(const Clause& c) const {
 //
 void Solver::cancelUntil(int level) {
     if (decisionLevel() > level){
-        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+        // Pop the SMT context
+        for (int l = trail_lim.size() - level; l > 0; --l)
+          context->pop();
+        // Now the minisat stuff
+        for (int c = trail.size()-1; c >= trail_lim[level]; c--) {
             Var     x  = var(trail[c]);
             assigns[x] = toInt(l_Undef);
-            insertVarOrder(x); }
+            insertVarOrder(x);
+        }
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
-    } }
+    }
+}
 
 
 //=================================================================================================
@@ -390,9 +401,40 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from)
 }
 
 
+Clause* Solver::propagate()
+{
+    Clause* confl = NULL;
+
+    while(qhead < trail.size()) {
+      confl = propagateBool();
+      if (confl != NULL) break;
+      confl = propagateTheory();
+      if (confl != NULL) break;
+    }
+
+    return confl;
+}
+
 /*_________________________________________________________________________________________________
 |
-|  propagate : [void]  ->  [Clause*]
+|  propagateTheory : [void]  ->  [Clause*]
+|
+|  Description:
+|    Propagates all enqueued theory facts. If a conflict arises, the conflicting clause is returned,
+|    otherwise NULL.
+|
+|    Note: the propagation queue might be NOT empty
+|________________________________________________________________________________________________@*/
+Clause* Solver::propagateTheory()
+{
+  SatClause clause;
+  proxy->theoryCheck(clause);
+  return NULL;
+}
+
+/*_________________________________________________________________________________________________
+|
+|  propagateBool : [void]  ->  [Clause*]
 |  
 |  Description:
 |    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
@@ -401,7 +443,7 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from)
 |    Post-conditions:
 |      * the propagation queue is empty, even if there was a conflict.
 |________________________________________________________________________________________________@*/
-Clause* Solver::propagate()
+Clause* Solver::propagateBool()
 {
     Clause* confl     = NULL;
     int     num_props = 0;
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 44499246e..c593d8b2c 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -17,11 +17,12 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "cvc4_private.h"
-
 #ifndef __CVC4__PROP__MINISAT__SOLVER_H
 #define __CVC4__PROP__MINISAT__SOLVER_H
 
+#include "cvc4_private.h"
+#include "context/context.h"
+
 #include <cstdio>
 #include <cassert>
 
@@ -32,27 +33,34 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "SolverTypes.h"
 
-
 //=================================================================================================
 // Solver -- the main class:
 
 namespace CVC4 {
 namespace prop {
 
-class SatSolverProxy;
+class SatSolver;
 
 namespace minisat {
 
 class Solver {
 
   /** The only CVC4 entry point to the private solver data */
-  friend class CVC4::prop::SatSolverProxy;
+  friend class CVC4::prop::SatSolver;
+
+protected:
+
+  /** The pointer to the proxy that provides interfaces to the SMT engine */
+  SatSolver* proxy;
+
+  /** The context from the SMT solver */
+  context::Context* context;
 
 public:
 
     // Constructor/Destructor:
     //
-    Solver();
+    Solver(SatSolver* proxy, context::Context* context);
     CVC4_PUBLIC ~Solver();
 
     // Problem specification:
@@ -165,7 +173,9 @@ protected:
     void     newDecisionLevel ();                                                      // Begins a new decision level.
     void     uncheckedEnqueue (Lit p, Clause* from = NULL);                            // Enqueue a literal. Assumes value of literal is undefined.
     bool     enqueue          (Lit p, Clause* from = NULL);                            // Test if fact 'p' contradicts current state, enqueue otherwise.
-    Clause*  propagate        ();                                                      // Perform unit propagation. Returns possibly conflicting clause.
+    Clause*  propagate        ();                                                      // Perform Boolean and Theory. Returns possibly conflicting clause.
+    Clause*  propagateBool    ();                                                      // Perform Boolean propagation. Returns possibly conflicting clause.
+    Clause*  propagateTheory  ();                                                      // Perform Theory propagation. Returns possibly conflicting clause.
     void     cancelUntil      (int level);                                             // Backtrack until a certain level.
     void     analyze          (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
     void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
@@ -217,11 +227,9 @@ protected:
         return (int)(drand(seed) * size); }
 };
 
-
 //=================================================================================================
 // Implementation of inline methods:
 
-
 inline void Solver::insertVarOrder(Var x) {
     if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); }
 
@@ -247,7 +255,7 @@ inline void Solver::claBumpActivity (Clause& c) {
 
 inline bool     Solver::enqueue         (Lit p, Clause* from)   { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
 inline bool     Solver::locked          (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); context->push(); }
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level[x] & 31); }
diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C
index 063332e74..124849155 100644
--- a/src/prop/minisat/simp/SimpSolver.C
+++ b/src/prop/minisat/simp/SimpSolver.C
@@ -28,8 +28,9 @@ namespace CVC4 {
 namespace prop {
 namespace minisat {
 
-SimpSolver::SimpSolver() :
-    grow               (0)
+SimpSolver::SimpSolver(SatSolver* proxy, context::Context* context) :
+    Solver(proxy, context)
+  , grow               (0)
   , asymm_mode         (false)
   , redundancy_check   (false)
   , merges             (0)
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 223b21998..67d0d2b95 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -30,13 +30,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 namespace CVC4 {
 namespace prop {
+
+class SatSolver;
+
 namespace minisat {
 
 class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-    SimpSolver();
+    SimpSolver(SatSolver* proxy, context::Context* context);
     CVC4_PUBLIC ~SimpSolver();
 
     // Problem specification:
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 76be5d6d8..32be206b0 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -26,20 +26,21 @@
 #include <map>
 
 using namespace std;
+using namespace CVC4::context;
 
 namespace CVC4 {
 namespace prop {
 
 PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
-                       TheoryEngine* te)
+                       TheoryEngine* te, Context* context)
 : d_inCheckSat(false),
   d_options(opts),
   d_decisionEngine(de),
-  d_theoryEngine(te) 
+  d_theoryEngine(te),
+  d_context(context)
 {
   Debug("prop") << "Constructing the PropEngine" << endl;
-  d_satSolver = new SatSolver();
-  SatSolverProxy::initSatSolver(d_satSolver, d_options);
+  d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options);
   d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
 }
 
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index f57161fde..0c3916162 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -53,7 +53,9 @@ class PropEngine {
   /** The theory engine we will be using */
   TheoryEngine *d_theoryEngine;
 
-  /** The SAT solver*/
+  context::Context* d_context;
+
+  /** The SAT solver proxy */
   SatSolver* d_satSolver;
 
   /** List of all of the assertions that need to be made */
@@ -67,7 +69,7 @@ public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(const Options*, DecisionEngine*, TheoryEngine*);
+  PropEngine(const Options*, DecisionEngine*, TheoryEngine*, context::Context*);
 
   /**
    * Destructor.
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 65752f20b..1cd5d0bfe 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -14,6 +14,8 @@
  **/
 
 #include "cvc4_private.h"
+#include "context/context.h"
+#include "theory/theory_engine.h"
 
 #ifndef __CVC4__PROP__SAT_H
 #define __CVC4__PROP__SAT_H
@@ -28,10 +30,12 @@
 #include "prop/minisat/simp/SimpSolver.h"
 
 namespace CVC4 {
+
+class TheoryEngine;
+
 namespace prop {
 
-/** The solver we are using */
-typedef minisat::SimpSolver SatSolver;
+class PropEngine;
 
 /** Type of the SAT variables */
 typedef minisat::Var SatVariable;
@@ -74,24 +78,56 @@ inline std::ostream& operator << (std::ostream& out, const SatClause& clause) {
  * It's only accessible from the PropEngine, and should be treated with major
  * care.
  */
-class SatSolverProxy {
+class SatSolver {
+
+  /** The prop engine we are using */
+  PropEngine* d_propEngine;
+
+  /** The theory engine we are using */
+  TheoryEngine* d_theoryEngine;
 
-  /** Only the prop engine can modify the internals of the SAT solver */
-  friend class PropEngine;
+  /** Context we will be using to synchronzie the sat solver */
+  context::Context* d_context;
 
-  private:
+  /** Minisat solver */
+  minisat::SimpSolver* d_minisat;
 
-    /**
-     * Initializes the given sat solver with the given options.
-     * @param satSolver the SAT solver
-     * @param options the options
-     */
-    inline static void initSatSolver(SatSolver* satSolver,
-                                     const Options* options) {
+  /** Remember the options */
+  Options* d_options;
+
+  public:
+
+    SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
+                   context::Context* context, const Options* options)
+      : d_propEngine(propEngine),
+        d_theoryEngine(theoryEngine),
+        d_context(context)
+    {
+      // Create the solver
+      d_minisat = new minisat::SimpSolver(this, d_context);
       // Setup the verbosity
-      satSolver->verbosity = (options->verbosity > 0) ? 1 : -1;
+      d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
       // Do not delete the satisfied clauses, just the learnt ones
-      satSolver->remove_satisfied = false;
+      d_minisat->remove_satisfied = false;
+    }
+
+    ~SatSolver() {
+      delete d_minisat;
+    }
+
+    inline bool solve() {
+      return d_minisat->solve();
+    }
+
+    inline void addClause(SatClause& clause) {
+      d_minisat->addClause(clause);
+    }
+
+    inline SatVariable newVar() {
+      return d_minisat->newVar();
+    }
+
+    inline void theoryCheck(SatClause& conflict) {
     }
 };
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ae676e48d..c45314a55 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -33,7 +33,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
   NodeManagerScope nms(d_nodeManager);
   d_decisionEngine = new DecisionEngine;
   d_theoryEngine = new TheoryEngine(this, d_ctxt);
-  d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine);
+  d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt);
 }
 
 SmtEngine::~SmtEngine() {