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/cnf_stream.h | |
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/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 33 |
1 files changed, 18 insertions, 15 deletions
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 */ |