From de0160112edbed8ce9b62bf87172ae2f0e99a013 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Mon, 8 Mar 2010 23:03:48 +0000 Subject: [PATCH] adding simple-uf to the regressions, and the code that apparently solves it --- .../org.eclipse.ltk.core.refactoring.prefs | 3 ++ src/prop/cnf_stream.cpp | 19 +++++++++ src/prop/cnf_stream.h | 15 ++++--- src/prop/minisat/core/Solver.C | 8 +++- src/prop/sat.h | 21 +++++++++- src/theory/theory.h | 5 +++ src/theory/theory_engine.h | 42 +++++++++++++++---- src/theory/uf/theory_uf.cpp | 5 ++- test/regress/regress0/Makefile.am | 1 + 9 files changed, 99 insertions(+), 20 deletions(-) create mode 100644 .settings/org.eclipse.ltk.core.refactoring.prefs 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::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 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 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 \ -- 2.30.2