Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.

7 files changed, 214 insertions, 62 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 45f7ab398..9136a73c3 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -102,26 +102,10 @@ Node CnfStream::getNode(const SatLiteral& literal) {
   return node;
 }
 
-SatLiteral CnfStream::getLiteral(TNode node) {
-  TranslationCache::iterator find = d_translationCache.find(node);
-  Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
-  SatLiteral literal = find->second;
-  Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
-  return literal;
-}
-
-const CnfStream::NodeCache& CnfStream::getNodeCache() const {
-  return d_nodeCache;
-}
-
-const CnfStream::TranslationCache& CnfStream::getTranslationCache() const {
-  return d_translationCache;
-}
-
-SatLiteral TseitinCnfStream::handleAtom(TNode node) {
+SatLiteral CnfStream::convertAtom(TNode node) {
   Assert(!isCached(node), "atom already mapped!");
 
-  Debug("cnf") << "handleAtom(" << node << ")" << endl;
+  Debug("cnf") << "convertAtom(" << node << ")" << endl;
 
   bool theoryLiteral = node.getKind() != kind::VARIABLE;
   SatLiteral lit = newLiteral(node, theoryLiteral);
@@ -137,6 +121,23 @@ SatLiteral TseitinCnfStream::handleAtom(TNode node) {
   return lit;
 }
 
+SatLiteral CnfStream::getLiteral(TNode node, bool create /* = false */) {
+  TranslationCache::iterator find = d_translationCache.find(node);
+  SatLiteral literal;
+  if(create) {
+    if(find == d_translationCache.end()) {
+      literal = convertAtom(node);
+    } else {
+      literal = find->second;
+    }
+  } else {
+    Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
+    literal = find->second;
+  }
+  Debug("cnf") << "CnfStream::getLiteral(" << node << ", create = " << create << ") => " << literal << std::endl;
+  return literal;
+}
+
 SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
   Assert(!isCached(xorNode), "Atom already mapped!");
   Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
@@ -366,10 +367,10 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
     default:
       {
         //TODO make sure this does not contain any boolean substructure
-        nodeLit = handleAtom(node);
+        nodeLit = convertAtom(node);
         //Unreachable();
         //Node atomic = handleNonAtomicNode(node);
-        //return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
+        //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic);
       }
     }
   }
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index abb69f590..ba87cf269 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -127,6 +127,16 @@ protected:
    */
   SatLiteral newLiteral(TNode node, bool theoryLiteral = false);
 
+  /**
+   * Constructs a new literal for an atom and returns it.  Calls
+   * newLiteral().
+   *
+   * @param node the node to convert; there should be no boolean
+   * structure in this expression.  Assumed to not be in the
+   * translation cache.
+   */
+  SatLiteral convertAtom(TNode node);
+
 public:
 
   /**
@@ -161,14 +171,25 @@ public:
 
   /**
    * Returns the literal that represents the given node in the SAT CNF
-   * representation. [Presumably there are some constraints on the kind
-   * of node? E.g., it needs to be a boolean? -Chris]
-   *
+   * representation.
+   * @param node [Presumably there are some constraints on the kind of
+   * node? E.g., it needs to be a boolean? -Chris]
+   * @param create Controls whether or not to create a new SAT literal
+   * mapping for Node if it does not exist.  This exists to break
+   * circular dependencies, where an atom is converted and asserted to
+   * the SAT solver, which propagates it immediately since it's a
+   * unit, which can theory-propagate additional literals that don't
+   * yet have a SAT literal mapping.
    */
-  SatLiteral getLiteral(TNode node);
+  SatLiteral getLiteral(TNode node, bool create = false);
+
+  const TranslationCache& getTranslationCache() const {
+    return d_translationCache;
+  }
 
-  const TranslationCache& getTranslationCache() const;
-  const NodeCache& getNodeCache() const;
+  const NodeCache& getNodeCache() const {
+    return d_nodeCache;
+  }
 }; /* class CnfStream */
 
 /**
@@ -178,7 +199,7 @@ public:
  * will be equivalent to each subexpression in the constructed equi-satisfiable
  * formula, then substitute the new literal for the formula, and so on,
  * recursively.
- * 
+ *
  * This implementation does this in a single recursive pass. [??? -Chris]
  */
 class TseitinCnfStream : public CnfStream {
@@ -211,7 +232,6 @@ private:
   //   - returning l
   //
   // handleX( n ) can assume that n is not in d_translationCache
-  SatLiteral handleAtom(TNode node);
   SatLiteral handleNot(TNode node);
   SatLiteral handleXor(TNode node);
   SatLiteral handleImplies(TNode node);
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index 8533e191b..1667af20d 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -29,6 +29,28 @@ namespace CVC4 {
 namespace prop {
 namespace minisat {
 
+Clause* Solver::lazy_reason = reinterpret_cast<Clause*>(1);
+
+Clause* Solver::getReason(Lit l)
+{
+    if (reason[var(l)] != lazy_reason) return reason[var(l)];
+    // Get the explanation from the theory
+    SatClause explanation;
+    if (value(l) == l_True) {
+      proxy->explainPropagation(l, explanation);
+      assert(explanation[0] == l);
+    } else {
+      proxy->explainPropagation(~l, explanation);
+      assert(explanation[0] == ~l);
+    }
+    Clause* real_reason = Clause_new(explanation, true);
+    reason[var(l)] = real_reason;
+    // Add it to the database
+    learnts.push(real_reason);
+    attachClause(*real_reason);
+    return real_reason;
+}
+
 Solver::Solver(SatSolver* proxy, context::Context* context) :
 
     // SMT stuff
@@ -122,7 +144,7 @@ bool Solver::addClause(vec<Lit>& ps, ClauseType type)
         assert(type != CLAUSE_LEMMA);
         assert(value(ps[0]) == l_Undef);
         uncheckedEnqueue(ps[0]);
-        return ok = (propagate() == NULL);
+        return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL);
     }else{
         Clause* c = Clause_new(ps, false);
         clauses.push(c);
@@ -282,7 +304,7 @@ void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
         // Select next clause to look at:
         while (!seen[var(trail[index--])]);
         p     = trail[index+1];
-        confl = reason[var(p)];
+        confl = getReason(p);
         seen[var(p)] = 0;
         pathC--;
 
@@ -299,12 +321,12 @@ void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
 
         out_learnt.copyTo(analyze_toclear);
         for (i = j = 1; i < out_learnt.size(); i++)
-            if (reason[var(out_learnt[i])] == NULL || !litRedundant(out_learnt[i], abstract_level))
+            if (getReason(out_learnt[i]) == NULL || !litRedundant(out_learnt[i], abstract_level))
                 out_learnt[j++] = out_learnt[i];
     }else{
         out_learnt.copyTo(analyze_toclear);
         for (i = j = 1; i < out_learnt.size(); i++){
-            Clause& c = *reason[var(out_learnt[i])];
+            Clause& c = *getReason(out_learnt[i]);
             for (int k = 1; k < c.size(); k++)
                 if (!seen[var(c[k])] && level[var(c[k])] > 0){
                     out_learnt[j++] = out_learnt[i];
@@ -342,13 +364,13 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
     analyze_stack.clear(); analyze_stack.push(p);
     int top = analyze_toclear.size();
     while (analyze_stack.size() > 0){
-        assert(reason[var(analyze_stack.last())] != NULL);
+        assert(getReason(analyze_stack.last()) != NULL);
         Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop();
 
         for (int i = 1; i < c.size(); i++){
             Lit p  = c[i];
             if (!seen[var(p)] && level[var(p)] > 0){
-                if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){
+                if (getReason(p) != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){
                     seen[var(p)] = 1;
                     analyze_stack.push(p);
                     analyze_toclear.push(p);
@@ -415,42 +437,74 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from)
     polarity [var(p)] = sign(p);
     trail.push(p);
 
-    if (theory[var(p)]) {
+    if (theory[var(p)] && from != lazy_reason) {
       // Enqueue to the theory
       proxy->enqueueTheoryLiteral(p);
     }
 }
 
 
-Clause* Solver::propagate()
+Clause* Solver::propagate(TheoryCheckType type)
 {
     Clause* confl = NULL;
 
-    while(qhead < trail.size()) {
-      confl = propagateBool();
-      if (confl != NULL) break;
-      confl = propagateTheory();
-      if (confl != NULL) break;
+    // If this is the final check, no need for Boolean propagation and
+    // theory propagation
+    if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
+      return theoryCheck(theory::Theory::FULL_EFFORT);
     }
 
+    // The effort we will be using to theory check
+    theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ?
+        theory::Theory::QUICK_CHECK : theory::Theory::STANDARD;
+
+    // Keep running until we have checked everything, we
+    // have no conflict and no new literals have been asserted
+    bool new_assertions;
+    do {
+        new_assertions = false;
+        while(qhead < trail.size()) {
+            confl = propagateBool();
+            if (confl != NULL) break;
+            confl = theoryCheck(effort);
+            if (confl != NULL) break;
+        }
+
+        if (confl == NULL && type == CHECK_WITH_PROPAGATION_STANDARD) {
+          new_assertions = propagateTheory();
+          if (!new_assertions) break;
+        }
+    } while (new_assertions);
+
     return confl;
 }
 
+bool Solver::propagateTheory() {
+  std::vector<Lit> propagatedLiterals;
+  proxy->theoryPropagate(propagatedLiterals);
+  const unsigned i_end = propagatedLiterals.size();
+  for (unsigned i = 0; i < i_end; ++ i) {
+    uncheckedEnqueue(propagatedLiterals[i], lazy_reason);
+  }
+  proxy->clearPropagatedLiterals();
+  return propagatedLiterals.size() > 0;
+}
+
 /*_________________________________________________________________________________________________
 |
-|  propagateTheory : [void]  ->  [Clause*]
+|  theoryCheck: [void]  ->  [Clause*]
 |
 |  Description:
-|    Propagates all enqueued theory facts. If a conflict arises, the conflicting clause is returned,
-|    otherwise NULL.
+|    Checks all enqueued theory facts for satisfiability. If a conflict arises, the conflicting
+|    clause is returned, otherwise NULL.
 |
 |    Note: the propagation queue might be NOT empty
 |________________________________________________________________________________________________@*/
-Clause* Solver::propagateTheory()
+Clause* Solver::theoryCheck(theory::Theory::Effort effort)
 {
   Clause* c = NULL;
   SatClause clause;
-  proxy->theoryCheck(clause);
+  proxy->theoryCheck(effort, clause);
   int clause_size = clause.size();
   Assert(clause_size != 1, "Can't handle unit clause explanations");
   if(clause_size > 0) {
@@ -598,7 +652,7 @@ bool Solver::simplify()
 {
     assert(decisionLevel() == 0);
 
-    if (!ok || propagate() != NULL)
+    if (!ok || propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL)
         return ok = false;
 
     if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
@@ -643,9 +697,9 @@ lbool Solver::search(int nof_conflicts, int nof_learnts)
     starts++;
 
     bool first = true;
-
+    TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD;
     for (;;){
-        Clause* confl = propagate();
+        Clause* confl = propagate(check_type);
         if (confl != NULL){
             // CONFLICT
             conflicts++; conflictC++;
@@ -671,9 +725,16 @@ lbool Solver::search(int nof_conflicts, int nof_learnts)
             varDecayActivity();
             claDecayActivity();
 
+            // We have a conflict so, we are going back to standard checks
+            check_type = CHECK_WITH_PROPAGATION_STANDARD;
+
         }else{
             // NO CONFLICT
 
+            // If this was a final check, we are satisfiable
+            if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL)
+              return l_True;
+
             if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
                 // Reached bound on number of conflicts:
                 progress_estimate = progressEstimate();
@@ -709,9 +770,11 @@ lbool Solver::search(int nof_conflicts, int nof_learnts)
                 decisions++;
                 next = pickBranchLit(polarity_mode, random_var_freq);
 
-                if (next == lit_Undef)
-                    // Model found:
-                    return l_True;
+                if (next == lit_Undef) {
+                    // We need to do a full theory check to confirm
+                    check_type = CHECK_WITHOUTH_PROPAGATION_FINAL;
+                    continue;
+                }
             }
 
             // Increase decision level and enqueue 'next'
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 312fe44d5..2e44803e9 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define __CVC4__PROP__MINISAT__SOLVER_H
 
 #include "context/context.h"
+#include "theory/theory.h"
 
 #include <cstdio>
 #include <cassert>
@@ -161,7 +162,11 @@ protected:
     vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
     vec<Clause*>        lemmas;           // List of lemmas we added (context dependent)
     vec<int>            lemmas_lim;       // Separator indices for different decision levels in 'lemmas'.
-    vec<Clause*>        reason;           // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
+    static Clause*      lazy_reason;      // The mark when we need to ask the theory engine for a reason
+    vec<Clause*>        reason;           // 'reason[var]' is the clause that implied the variables current value, lazy_reason if theory propagated, or 'NULL' if none.
+
+    Clause* getReason(Lit l);             // Returns the reason, or asks the theory for an explanation
+
     vec<int>            level;            // 'level[var]' contains the level at which the assignment was made.
     int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
     int                 lhead;            // Head of the lemma stack (for backtracking)
@@ -181,6 +186,15 @@ protected:
     vec<Lit>            analyze_toclear;
     vec<Lit>            add_tmp;
 
+    enum TheoryCheckType {
+      // Quick check, but don't perform theory propagation
+      CHECK_WITHOUTH_PROPAGATION_QUICK,
+      // Check and perform theory propagation
+      CHECK_WITH_PROPAGATION_STANDARD,
+      // The SAT problem is satisfiable, perform a full theory check
+      CHECK_WITHOUTH_PROPAGATION_FINAL
+    };
+
     // Main internal methods:
     //
     void     insertVarOrder   (Var x);                                                 // Insert a variable in the decision order priority queue.
@@ -188,9 +202,10 @@ 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 Boolean and Theory. Returns possibly conflicting clause.
+    Clause*  propagate        (TheoryCheckType type);                                  // 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.
+    bool     propagateTheory  ();                                                      // Perform Theory propagation. Return true if any literals were asserted.
+    Clause*  theoryCheck      (theory::Theory::Effort effort);                         // Perform a theory satisfiability check. 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?
@@ -216,7 +231,7 @@ protected:
 
     // Misc:
     //
-    int      decisionLevel    ()      const; // Gives the current decisionlevel.
+    int      decisionLevel    ()      const; // Gives the current decision level.
     uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
 
diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C
index 9aad6aea7..00f93402f 100644
--- a/src/prop/minisat/simp/SimpSolver.C
+++ b/src/prop/minisat/simp/SimpSolver.C
@@ -212,7 +212,7 @@ bool SimpSolver::strengthenClause(Clause& c, Lit l)
         updateElimHeap(var(l));
     }
 
-    return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : true;
+    return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL : true;
 }
 
 
@@ -312,7 +312,7 @@ bool SimpSolver::implied(const vec<Lit>& c)
             uncheckedEnqueue(~c[i]);
         }
 
-    bool result = propagate() != NULL;
+    bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL;
     cancelUntil(0);
     return result;
 }
@@ -394,7 +394,7 @@ bool SimpSolver::asymm(Var v, Clause& c)
         else
             l = c[i];
 
-    if (propagate() != NULL){
+    if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL){
         cancelUntil(0);
         asymm_lits++;
         if (!strengthenClause(c, l))
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 207bda4db..a7b536a57 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -26,9 +26,9 @@
 namespace CVC4 {
 namespace prop {
 
-void SatSolver::theoryCheck(SatClause& conflict) {
+void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) {
   // Try theory propagation
-  bool ok = d_theoryEngine->check(theory::Theory::FULL_EFFORT);
+  bool ok = d_theoryEngine->check(effort);
   // If in conflict construct the conflict clause
   if (!ok) {
     // We have a conflict, get it
@@ -47,6 +47,47 @@ void SatSolver::theoryCheck(SatClause& conflict) {
   }
 }
 
+void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) {
+  // Propagate
+  d_theoryEngine->propagate();
+  // Get the propagated literals
+  const std::vector<TNode>& outputNodes = d_theoryEngine->getPropagatedLiterals();
+  // If any literals, make a clause
+  const unsigned i_end = outputNodes.size();
+  for (unsigned i = 0; i < i_end; ++ i) {
+    Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << endl;
+    // The second argument ("true") instructs the CNF stream to create
+    // a new literal mapping if it doesn't exist.  This can happen due
+    // to a circular dependence, if a SAT literal "a" is asserted as a
+    // unit to the SAT solver, a round of theory propagation can occur
+    // before all Nodes have SAT variable mappings.
+    SatLiteral l = d_cnfStream->getLiteral(outputNodes[i], true);
+    output.push_back(l);
+  }
+}
+
+void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) {
+  TNode lNode = d_cnfStream->getNode(l);
+  Debug("prop-explain") << "explainPropagation(" << lNode.toString() << ")" << endl;
+  Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
+  Debug("prop-explain") << "explainPropagation() => " <<  theoryExplanation.toString() << endl;
+  if (lNode.getKind() == kind::AND) {
+    Node::const_iterator it = theoryExplanation.begin();
+    Node::const_iterator it_end = theoryExplanation.end();
+    explanation.push(l);
+    for (; it != it_end; ++ it) {
+      explanation.push(~d_cnfStream->getLiteral(*it));
+    }
+  } else {
+    explanation.push(l);
+    explanation.push(~d_cnfStream->getLiteral(theoryExplanation));
+  }
+}
+
+void SatSolver::clearPropagatedLiterals() {
+  d_theoryEngine->clearPropagatedLiterals();
+}
+
 void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
   Node literalNode = d_cnfStream->getNode(l);
   Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
diff --git a/src/prop/sat.h b/src/prop/sat.h
index f64697d7b..992d8ecd2 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -27,6 +27,7 @@
 
 #include "util/options.h"
 #include "util/stats.h"
+#include "theory/theory.h"
 
 #ifdef __CVC4_USE_MINISAT
 
@@ -199,7 +200,13 @@ public:
 
   SatVariable newVar(bool theoryAtom = false);
 
-  void theoryCheck(SatClause& conflict);
+  void theoryCheck(theory::Theory::Effort effort, SatClause& conflict);
+
+  void explainPropagation(SatLiteral l, SatClause& explanation);
+
+  void theoryPropagate(std::vector<SatLiteral>& output);
+
+  void clearPropagatedLiterals();
 
   void enqueueTheoryLiteral(const SatLiteral& l);
 
@@ -229,6 +236,11 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   // Make minisat reuse the literal values
   d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
 
+  // No random choices
+  if(debugTagIsOn("no_rnd_decisions")){
+    d_minisat->random_var_freq = 0;
+  }
+
   d_statistics.init(d_minisat);
 }