some more sat stuff for tim: assertions now go to theory_uf

1 files changed, 112 insertions, 60 deletions

diff --git a/src/prop/sat.h b/src/prop/sat.h
index 2468990f2..fb8930910 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -13,13 +13,11 @@
  ** SAT Solver.
  **/
 
-#include "cvc4_private.h"
-#include "context/context.h"
-#include "theory/theory_engine.h"
-
 #ifndef __CVC4__PROP__SAT_H
 #define __CVC4__PROP__SAT_H
 
+#include "cvc4_private.h"
+
 #define __CVC4_USE_MINISAT
 
 #ifdef __CVC4_USE_MINISAT
@@ -36,6 +34,7 @@ class TheoryEngine;
 namespace prop {
 
 class PropEngine;
+class CnfStream;
 
 /** Type of the SAT variables */
 typedef minisat::Var SatVariable;
@@ -47,6 +46,67 @@ typedef minisat::Lit SatLiteral;
 typedef minisat::vec<SatLiteral> SatClause;
 
 /**
+ * The proxy class that allows us to modify the internals of the SAT solver.
+ * It's only accessible from the PropEngine, and should be treated with major
+ * care.
+ */
+class SatSolver {
+
+  /** The prop engine we are using */
+  PropEngine* d_propEngine;
+
+  /** The CNF engine we are using */
+  CnfStream* d_cnfStream;
+
+  /** The theory engine we are using */
+  TheoryEngine* d_theoryEngine;
+
+  /** Context we will be using to synchronzie the sat solver */
+  context::Context* d_context;
+
+  /** Minisat solver */
+  minisat::SimpSolver* d_minisat;
+
+  /** Remember the options */
+  Options* d_options;
+
+public:
+
+  /** Hash function for literals */
+  struct SatLiteralHashFcn {
+    inline size_t operator()(const SatLiteral& literal) const;
+  };
+
+  inline SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, context::Context* context,
+            const Options* options);
+
+  inline ~SatSolver();
+
+  inline bool solve();
+
+  inline void addClause(SatClause& clause);
+
+  inline SatVariable newVar(bool theoryAtom = false);
+
+  inline void theoryCheck(SatClause& conflict);
+
+  inline void enqueueTheoryLiteral(const SatLiteral& l);
+
+  inline void setCnfStream(CnfStream* cnfStream);
+};
+
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#include "context/context.h"
+#include "theory/theory_engine.h"
+#include "prop/prop_engine.h"
+#include "prop/cnf_stream.h"
+
+namespace CVC4 {
+namespace prop {
+
+/**
  * Returns the variable of the literal.
  * @param lit the literal
  */
@@ -58,13 +118,13 @@ inline bool literalSign(SatLiteral lit) {
   return minisat::sign(lit);
 }
 
-inline std::ostream& operator << (std::ostream& out, SatLiteral lit) {
+inline std::ostream& operator <<(std::ostream& out, SatLiteral lit) {
   const char * s = (literalSign(lit)) ? "~" : " ";
   out << s << literalToVariable(lit);
   return out;
 }
 
-inline std::ostream& operator << (std::ostream& out, const SatClause& clause) {
+inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) {
   out << "clause:";
   for(int i = 0; i < clause.size(); ++i) {
     out << " " << clause[i];
@@ -73,66 +133,59 @@ inline std::ostream& operator << (std::ostream& out, const SatClause& clause) {
   return out;
 }
 
-/**
- * The proxy class that allows us to modify the internals of the SAT solver.
- * It's only accessible from the PropEngine, and should be treated with major
- * care.
- */
-class SatSolver {
+size_t SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const {
+  return (size_t) minisat::toInt(literal);
+}
 
-  /** The prop engine we are using */
-  PropEngine* d_propEngine;
+SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
+                     context::Context* context, const Options* options) :
+  d_propEngine(propEngine),
+  d_cnfStream(NULL),
+  d_theoryEngine(theoryEngine),
+  d_context(context)
+{
+  // Create the solver
+  d_minisat = new minisat::SimpSolver(this, d_context);
+  // Setup the verbosity
+  d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
+  // Do not delete the satisfied clauses, just the learnt ones
+  d_minisat->remove_satisfied = false;
+  // Make minisat reuse the literal values
+  d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
+}
 
-  /** The theory engine we are using */
-  TheoryEngine* d_theoryEngine;
+SatSolver::~SatSolver() {
+  delete d_minisat;
+}
 
-  /** Context we will be using to synchronzie the sat solver */
-  context::Context* d_context;
+bool SatSolver::solve() {
+  return d_minisat->solve();
+}
 
-  /** Minisat solver */
-  minisat::SimpSolver* d_minisat;
+void SatSolver::addClause(SatClause& clause) {
+  d_minisat->addClause(clause);
+}
 
-  /** Remember the options */
-  Options* d_options;
+SatVariable SatSolver::newVar(bool theoryAtom) {
+  return d_minisat->newVar(true, true, theoryAtom);
+}
 
-  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
-      d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
-      // Do not delete the satisfied clauses, just the learnt ones
-      d_minisat->remove_satisfied = false;
-      // Make minisat reuse the literal values
-      d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
-    }
-
-    ~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) {
-    }
-};
+void SatSolver::theoryCheck(SatClause& conflict) {
+  d_theoryEngine->check(theory::Theory::STANDARD);
+}
 
+void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
+  Node literalNode = d_cnfStream->getNode(l);
+  // We can get null from the prop engine if the literal is useless (i.e.)
+  // the expression is not in context anyomore
+  if(!literalNode.isNull()) {
+    d_theoryEngine->assertFact(literalNode);
+  }
+}
+
+void SatSolver::setCnfStream(CnfStream* cnfStream) {
+  d_cnfStream = cnfStream;
+}
 
 
 }/* CVC4::prop namespace */
@@ -140,5 +193,4 @@ class SatSolver {
 
 #endif
 
-
 #endif /* __CVC4__PROP__SAT_H */