adding simple-uf to the regressions, and the code that apparently solves it

4 files changed, 53 insertions, 10 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 2efad3cb2..51992a31c 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -87,6 +87,25 @@ SatLiteral CnfStream::newLiteral(const TNode& node, bool theoryLiteral) {
   return lit;
 }
 
+Node CnfStream::getNode(const SatLiteral& literal) {
+  Node node;
+  NodeCache::iterator find = d_nodeCache.find(literal);
+  if(find != d_nodeCache.end()) {
+    node = find->second;
+  }
+  return node;
+}
+
+SatLiteral CnfStream::getLiteral(const TNode& node) {
+  TranslationCache::iterator find = d_translationCache.find(node);
+  SatLiteral literal;
+  if(find != d_translationCache.end()) {
+    literal = find->second;
+  }
+  Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
+  return literal;
+}
+
 SatLiteral TseitinCnfStream::handleAtom(const TNode& node) {
   Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom");
   Assert(!isCached(node), "atom already mapped!");
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 93c1f529a..2581046c1 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -143,14 +143,13 @@ public:
    * @param literal the literal from the sat solver
    * @return the actual node
    */
-  Node getNode(const SatLiteral& literal) {
-    Node node;
-    NodeCache::iterator find = d_nodeCache.find(literal);
-    if (find != d_nodeCache.end()) {
-      node = find->second;
-    }
-    return node;
-  }
+  Node getNode(const SatLiteral& literal);
+
+  /**
+   * Returns the literal the represents the given node in the SAT CNF
+   * representation.
+   */
+  SatLiteral getLiteral(const TNode& node);
 
 }; /* class CnfStream */
 
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index e3ce088b1..5ad647baa 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -436,9 +436,15 @@ Clause* Solver::propagate()
 |________________________________________________________________________________________________@*/
 Clause* Solver::propagateTheory()
 {
+  Clause* c = NULL;
   SatClause clause;
   proxy->theoryCheck(clause);
-  return NULL;
+  if (clause.size() > 0) {
+    Clause* c = Clause_new(clause, false);
+    clauses.push(c);
+    attachClause(*c);
+  }
+  return c;
 }
 
 /*_________________________________________________________________________________________________
diff --git a/src/prop/sat.h b/src/prop/sat.h
index fb8930910..922d596be 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -171,7 +171,26 @@ SatVariable SatSolver::newVar(bool theoryAtom) {
 }
 
 void SatSolver::theoryCheck(SatClause& conflict) {
-  d_theoryEngine->check(theory::Theory::STANDARD);
+  // Run the thoery checks
+  d_theoryEngine->check(theory::Theory::FULL_EFFORT);
+  // Try to get the conflict
+  Node conflictNode = d_theoryEngine->getConflict();
+  // If the conflict is there, construct the conflict clause
+  if (!conflictNode.isNull()) {
+    Debug("prop") << "SatSolver::theoryCheck() => conflict" << std::endl;
+    Node::const_iterator literal_it = conflictNode.begin();
+    Node::const_iterator literal_end = conflictNode.end();
+    while (literal_it != literal_end) {
+      // Get the node and construct it's negation
+      Node literalNode = (*literal_it);
+      Node negated = literalNode.getKind() == kind::NOT ? literalNode[0] : literalNode.notNode();
+      // Get the literal corresponding to the node
+      SatLiteral l = d_cnfStream->getLiteral(negated);
+      // Add to the conflict clause and continue
+      conflict.push(l);
+      literal_it ++;
+    }
+  }
 }
 
 void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {