diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-05 23:51:57 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-05 23:51:57 +0000 |
commit | a8d7333d8fb03c95ef3d1d7d9501076b97add756 (patch) | |
tree | 9f217a8cdb8905dea26529684584b401c4a47323 /src/prop | |
parent | 9bdf1355af20c4dd2b97ea9bc5f34cc20fbdde0f (diff) |
ensureLiteral() in CNF stream to support Andy's quantifiers work; an update to model gen on booleans; and a little cleanup
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 58 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 33 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 5 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 7 |
4 files changed, 79 insertions, 24 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index c211a9c71..6810d3a94 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -22,6 +22,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "theory/theory_engine.h" +#include "theory/theory.h" #include "expr/node.h" #include "util/Assert.h" #include "util/output.h" @@ -100,17 +101,59 @@ void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral bool CnfStream::isTranslated(TNode n) const { TranslationCache::const_iterator find = d_translationCache.find(n); - return find != d_translationCache.end() && find->second.level >= 0; + return find != d_translationCache.end() && (*find).second.level >= 0; } -bool CnfStream::hasEverHadLiteral(TNode n) const { +bool CnfStream::hasLiteral(TNode n) const { TranslationCache::const_iterator find = d_translationCache.find(n); return find != d_translationCache.end(); } -bool CnfStream::currentlyHasLiteral(TNode n) const { - TranslationCache::const_iterator find = d_translationCache.find(n); - return find != d_translationCache.end() && (*find).second.level != -1; +void TseitinCnfStream::ensureLiteral(TNode n) { + if(hasLiteral(n)) { + // Already a literal! + SatLiteral lit = getLiteral(n); + NodeCache::iterator i = d_nodeCache.find(lit); + if(i == d_nodeCache.end()) { + // Store backward-mappings + d_nodeCache[lit] = n; + d_nodeCache[~lit] = n.notNode(); + } + return; + } + + CheckArgument(n.getType().isBoolean(), n, + "CnfStream::ensureLiteral() requires a node of Boolean type.\n" + "got node: %s\n" + "its type: %s\n", + n.toString().c_str(), + n.getType().toString().c_str()); + + bool negated = false; + SatLiteral lit; + + if(n.getKind() == kind::NOT) { + negated = true; + n = n[0]; + } + + if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL && + n.getMetaKind() != kind::metakind::VARIABLE ) { + // If we were called with something other than a theory atom (or + // Boolean variable), we get a SatLiteral that is definitionally + // equal to it. + lit = toCNF(n, false); + + // Store backward-mappings + d_nodeCache[lit] = n; + d_nodeCache[~lit] = n.notNode(); + } else { + // We have a theory atom or variable. + lit = convertAtom(n); + } + + Assert(hasLiteral(n) && getNode(lit) == n); + Debug("ensureLiteral") << "CnfStream::ensureLiteral(): out lit is " << lit << std::endl; } SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { @@ -118,7 +161,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { // Get the literal for this node SatLiteral lit; - if (!hasEverHadLiteral(node)) { + if (!hasLiteral(node)) { // If no literal, well make one lit = variableToLiteral(d_satSolver->newVar(theoryLiteral)); d_translationCache[node].literal = lit; @@ -605,7 +648,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; /* - if(currentlyHasLiteral(node)) { + if(isTranslated(node)) { Debug("cnf") << "==> fortunate literal detected!" << endl; ++d_fortunateLiterals; SatLiteral lit = getLiteral(node); @@ -739,7 +782,6 @@ void CnfStream::moveToBaseLevel(TNode node) { moveToBaseLevel(*child); ++ child; } - } }/* CVC4::prop namespace */ diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 3ef636811..5eaeeef94 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -61,7 +61,7 @@ public: /** Cache of what literals have been registered to a node. */ typedef __gnu_cxx::hash_map<Node, TranslationInfo, NodeHashFunction> TranslationCache; -private: +protected: /** The SAT solver we will be using */ SatInputInterface *d_satSolver; @@ -69,8 +69,6 @@ private: TranslationCache d_translationCache; NodeCache d_nodeCache; -protected: - /** The "registrar" for pre-registration of terms */ theory::Registrar d_registrar; @@ -155,13 +153,6 @@ protected: void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); /** - * Returns true if the node has been cached in the translation cache. - * @param node the node - * @return true if the node has been cached - */ - bool isTranslated(TNode node) const; - - /** * Acquires a new variable from the SAT solver to represent the node * and inserts the necessary data it into the mapping tables. * @param node a formula @@ -203,7 +194,7 @@ public: * Converts and asserts a formula. * @param node node to convert and assert * @param removable whether the sat solver can choose to remove the clauses - * @param negated wheather we are asserting the node negated + * @param negated whether we are asserting the node negated */ virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0; @@ -215,16 +206,26 @@ public: TNode getNode(const SatLiteral& literal); /** - * Returns true iff the node has an assigned literal (it might not be translated). + * Returns true if the node has been cached in the translation cache. * @param node the node + * @return true if the node has been cached */ - bool hasEverHadLiteral(TNode node) const; + bool isTranslated(TNode node) const; /** - * Returns true iff the node has an assigned literal and it's translated. + * Returns true iff the node has an assigned literal (it might not be translated). * @param node the node */ - bool currentlyHasLiteral(TNode node) const; + bool hasLiteral(TNode node) const; + + /** + * Ensure that the given node will have a designated SAT literal + * that is definitionally equal to it. The result of this function + * is that the Node can be queried via getSatValue(). Essentially, + * this is like a "convert-but-don't-assert" version of + * convertAndAssert(). + */ + virtual void ensureLiteral(TNode n) = 0; /** * Returns the literal that represents the given node in the SAT CNF @@ -319,6 +320,8 @@ private: */ SatLiteral toCNF(TNode node, bool negated = false); + void ensureLiteral(TNode n); + };/* class TseitinCnfStream */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 7b4155bde..e123db0ed 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -167,7 +167,7 @@ Node PropEngine::getValue(TNode node) { } bool PropEngine::isSatLiteral(TNode node) { - return d_cnfStream->hasEverHadLiteral(node); + return d_cnfStream->hasLiteral(node); } bool PropEngine::hasValue(TNode node, bool& value) { @@ -187,6 +187,9 @@ bool PropEngine::hasValue(TNode node, bool& value) { } } +void PropEngine::ensureLiteral(TNode n) { + d_cnfStream->ensureLiteral(n); +} void PropEngine::push() { Assert(!d_inCheckSat, "Sat solver in solve()!"); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index bb8ed86e1..16cb34e04 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -127,6 +127,13 @@ public: bool hasValue(TNode node, bool& value); /** + * Ensure that the given node will have a designated SAT literal + * that is definitionally equal to it. The result of this function + * is that the Node can be queried via getSatValue(). + */ + void ensureLiteral(TNode n); + + /** * Push the context level. */ void push(); |