diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-11-26 17:40:31 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-11-26 17:40:31 +0000 |
commit | 78f459b303ed292a297a36cd0c435fdd025b0865 (patch) | |
tree | 80be491bc4525d70d599fbd72869dd592f70d56a /src/prop/cnf_stream.h | |
parent | c3ca3d8c58cc9954f8ad190e1e2dedbcbb5372f0 (diff) |
fixup for incremental solving
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 61 |
1 files changed, 14 insertions, 47 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index c085fd384..6ab639712 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -47,19 +47,10 @@ class CnfStream { public: /** Cache of what nodes have been registered to a literal. */ - typedef __gnu_cxx::hash_map<SatLiteral, TNode, SatLiteralHashFunction> NodeCache; - - /** Per node translation information */ - struct TranslationInfo { - bool recorded; - /** The level at which this node was translated (negative if not translated) */ - int level; - /** The literal of this node */ - SatLiteral literal; - }; + typedef context::CDHashMap<SatLiteral, TNode, SatLiteralHashFunction> LiteralToNodeMap; /** Cache of what literals have been registered to a node. */ - typedef __gnu_cxx::hash_map<Node, TranslationInfo, NodeHashFunction> TranslationCache; + typedef context::CDHashMap<Node, SatLiteral, NodeHashFunction> NodeToLiteralMap; protected: @@ -69,8 +60,11 @@ protected: /** Boolean variables that we translated */ context::CDList<TNode> d_booleanVariables; - TranslationCache d_translationCache; - NodeCache d_nodeCache; + /** Map from nodes to literals */ + NodeToLiteralMap d_nodeToLiteralMap; + + /** Map from literals to nodes */ + LiteralToNodeMap d_literalToNodeMap; /** * True if the lit-to-Node map should be kept for all lits, not just @@ -82,9 +76,6 @@ protected: /** The "registrar" for pre-registration of terms */ Registrar* d_registrar; - /** Top level nodes that we translated */ - std::vector<TNode> d_translationTrail; - /** * How many literals were already mapped at the top-level when we * tried to convertAndAssert() something. This @@ -111,23 +102,11 @@ protected: return node; } - /** Record this translation */ - void recordTranslation(TNode node, bool alwaysRecord = false); - - /** - * Moves the node and all of it's parents to level 0. - */ - void moveToBaseLevel(TNode node); - - /** - * Mark the node, and all parent at levels above level as untranslated. - */ - void undoTranslate(TNode node, int level); - /** * Are we asserting a removable clause (true) or a permanent clause (false). - * This is set at the begining of convertAndAssert so that it doesn't - * need to be passed on over the stack. + * This is set at the beginning of convertAndAssert so that it doesn't + * need to be passed on over the stack. Only pure clauses can be asserted as + * removable. */ bool d_removable; @@ -219,13 +198,6 @@ public: TNode getNode(const SatLiteral& literal); /** - * 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; - - /** * Returns true iff the node has an assigned literal (it might not be translated). * @param node the node */ @@ -253,19 +225,14 @@ public: */ void getBooleanVariables(std::vector<TNode>& outputVariables) const; - const TranslationCache& getTranslationCache() const { - return d_translationCache; + const NodeToLiteralMap& getTranslationCache() const { + return d_nodeToLiteralMap; } - const NodeCache& getNodeCache() const { - return d_nodeCache; + const LiteralToNodeMap& getNodeCache() const { + return d_literalToNodeMap; } - /** - * Removes all the translation information of clauses that have the given associated assert level. - */ - void removeClausesAboveLevel(int level); - };/* class CnfStream */ |