diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 21:08:40 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 21:08:40 +0000 |
commit | b1d9707979074abb8fed7ad4e8a2b15648c69324 (patch) | |
tree | 236c83135c62a7499d1039fff94037950e05061e /src/prop/cnf_stream.h | |
parent | 7b19de6b01d9a896560c39c9ef4a3731cf29b19d (diff) |
some more sat stuff for tim: assertions now go to theory_uf
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 9af15ba31..93c1f529a 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -46,7 +46,12 @@ private: SatSolver *d_satSolver; /** Cache of what literal have been registered to a node. */ - __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFcn> d_translationCache; + typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFcn> TranslationCache; + TranslationCache d_translationCache; + + /** Cache of what nodes have been registered to a literal. */ + typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFcn> NodeCache; + NodeCache d_nodeCache; protected: @@ -103,9 +108,11 @@ protected: * 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 + * @param theoryLiteral is this literal a theory literal (i.e. theory to be + * informed when set to true/false * @return the literal corresponding to the formula */ - SatLiteral newLiteral(const TNode& node); + SatLiteral newLiteral(const TNode& node, bool theoryLiteral = false); public: @@ -131,6 +138,20 @@ public: */ virtual void convertAndAssert(const TNode& node) = 0; + /** + * Returns a node the is represented by a give SatLiteral literal. + * @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; + } + }; /* class CnfStream */ /** |