diff options
Diffstat (limited to 'src/util/ite_removal.h')
-rw-r--r-- | src/util/ite_removal.h | 29 |
1 files changed, 24 insertions, 5 deletions
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index 03197be89..9d79687f4 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -22,21 +22,25 @@ #include "expr/node.h" #include "util/dump.h" #include "context/context.h" -#include "context/cdhashmap.h" +#include "context/cdinsert_hashmap.h" namespace CVC4 { +namespace theory { +class ContainsTermITEVistor; +} + typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; class RemoveITE { - typedef context::CDHashMap<Node, Node, NodeHashFunction> ITECache; + typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> ITECache; ITECache d_iteCache; + public: - RemoveITE(context::UserContext* u) : - d_iteCache(u) { - } + RemoveITE(context::UserContext* u); + ~RemoveITE(); /** * Removes the ITE nodes by introducing skolem variables. All @@ -57,6 +61,21 @@ public: Node run(TNode node, std::vector<Node>& additionalAssertions, IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar); + /** Returns true if e contains a term ite.*/ + bool containsTermITE(TNode e); + + /** Returns the collected size of the caches.*/ + size_t collectedCacheSizes() const; + + /** Garbage collects non-context dependent data-structures.*/ + void garbageCollect(); + + /** Return the RemoveITE's containsVisitor.*/ + theory::ContainsTermITEVistor* getContainsVisitor(); + +private: + theory::ContainsTermITEVistor* d_containsVisitor; + };/* class RemoveTTE */ }/* CVC4 namespace */ |