diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 23:03:48 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 23:03:48 +0000 |
commit | de0160112edbed8ce9b62bf87172ae2f0e99a013 (patch) | |
tree | c9fc1e4b7f365dbd34a79b8360f3ac8a006aad68 /src/prop | |
parent | fc810750142ee15917c6d77d21d987c369ce774b (diff) |
adding simple-uf to the regressions, and the code that apparently solves it
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 19 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 15 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.C | 8 | ||||
-rw-r--r-- | src/prop/sat.h | 21 |
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) { |