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

9 files changed, 99 insertions, 20 deletions

diff --git a/.settings/org.eclipse.ltk.core.refactoring.prefs b/.settings/org.eclipse.ltk.core.refactoring.prefs
new file mode 100644
index 000000000..fdaecac4f
--- /dev/null
+++ b/.settings/org.eclipse.ltk.core.refactoring.prefs
@@ -0,0 +1,3 @@
+#Mon Mar 08 12:18:42 EST 2010
+eclipse.preferences.version=1
+org.eclipse.ltk.core.refactoring.enable.project.refactoring.history=false
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) {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 86badb9bd..83082ff5d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -169,6 +169,7 @@ public:
    * Assert a fact in the current context.
    */
   void assertFact(TNode n) {
+    Debug("theory") << "Theory::assertFact(" << n << ")" << std::endl;
     d_facts.push(n);
   }
 
@@ -293,10 +294,14 @@ Node TheoryImpl<T>::get() {
   Node fact = d_facts.front();
   d_facts.pop();
 
+  Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl;
+
   if(! fact.getAttribute(RegisteredAttr())) {
     std::list<TNode> toReg;
     toReg.push_back(fact);
 
+    Debug("theory") << "Theory::get(): registering new atom" << std::endl;
+
     /* Essentially this is doing a breadth-first numbering of
      * non-registered subterms with children.  Any non-registered
      * leaves are immediately registered. */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5453aab93..87a78d920 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -54,14 +54,26 @@ class TheoryEngine {
    * back to a TheoryEngine.
    */
   class EngineOutputChannel : public theory::OutputChannel {
+
+    friend class TheoryEngine;
+
     TheoryEngine* d_engine;
+    context::Context* d_context;
+    context::CDO<Node> d_conflictNode;
+
   public:
-    void setEngine(TheoryEngine& engine) throw() {
-      d_engine = &engine;
+
+    EngineOutputChannel(TheoryEngine* engine, context::Context* context)
+    : d_engine(engine),
+      d_context(context),
+      d_conflictNode(context)
+    {
     }
 
     void conflict(TNode conflictNode, bool) throw(theory::Interrupted) {
-      Debug("theory") << "conflict(" << conflictNode << ")" << std::endl;
+      Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl;
+      d_conflictNode = conflictNode;
+      throw theory::Interrupted();
     }
 
     void propagate(TNode, bool) throw(theory::Interrupted) {
@@ -88,13 +100,13 @@ public:
    */
   TheoryEngine(SmtEngine* smt, context::Context* ctxt) :
     d_smt(smt),
-    d_theoryOut(),
+    d_theoryOut(this, ctxt),
     d_bool(ctxt, d_theoryOut),
     d_uf(ctxt, d_theoryOut),
     d_arith(ctxt, d_theoryOut),
     d_arrays(ctxt, d_theoryOut),
-    d_bv(ctxt, d_theoryOut) {
-    d_theoryOut.setEngine(*this);
+    d_bv(ctxt, d_theoryOut)
+  {
     theoryOfTable.registerTheory(&d_bool);
     theoryOfTable.registerTheory(&d_uf);
     theoryOfTable.registerTheory(&d_arith);
@@ -109,7 +121,8 @@ public:
    * of built-in type.
    */
   theory::Theory* theoryOf(const TNode& node) {
-    return theoryOfTable[node];
+    if (node.getKind() == kind::EQUAL) return &d_uf;
+    else return NULL;
   }
 
   /**
@@ -118,12 +131,23 @@ public:
    */
   inline void assertFact(const TNode& node) {
     Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
-    theory::Theory* theory = theoryOf(node);
+    theory::Theory* theory = node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node);
     if (theory != NULL) theory->assertFact(node);
   }
 
   inline void check(theory::Theory::Effort effort) {
-    d_uf.check(effort);
+    try {
+      d_uf.check(effort);
+    } catch (const theory::Interrupted&) {
+      Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
+    }
+  }
+
+  /**
+   * Returns the last conflict (if any).
+   */
+  inline Node getConflict() {
+    return d_theoryOut.d_conflictNode;
   }
 
 };/* class TheoryEngine */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 111f06fe9..ef0142352 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -250,7 +250,7 @@ void TheoryUF::merge(){
     (ecX->getRep()).printAst(Debug("uf"));
     Debug("uf") << "right equivalence class :";
     (ecY->getRep()).printAst(Debug("uf"));
-
+    Debug("uf") << std::endl;
 
     ccUnion(ecX, ecY);
   }
@@ -282,6 +282,7 @@ void TheoryUF::check(Effort level){
 
   while(!done()){
     Node assertion = get();
+    Debug("uf") << "TheoryUF::check(): " << assertion << std::endl;
 
     switch(assertion.getKind()){
     case EQUAL:
@@ -295,6 +296,8 @@ void TheoryUF::check(Effort level){
     default:
       Unreachable();
     }
+
+    Debug("uf") << "TheoryUF::check(): done = " << (done() ? "true" : "false") << std::endl;
   }
 
   //Make sure all outstanding merges are completed.
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 421f94418..987a2dfe2 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -11,6 +11,7 @@ TESTS =	bug32.cvc \
 	simple2.smt \
 	simple.cvc \
 	simple.smt \
+  simple-uf.smt \
 	smallcnf.cvc \
 	test11.cvc \
 	test9.cvc \