diff options
author | Tim King <taking@cs.nyu.edu> | 2013-11-25 18:36:06 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-11-25 18:36:06 -0500 |
commit | 22df6e9e8618614e8c33700c55705266912500ae (patch) | |
tree | 20d78676c1e819517f371e8bc5e6363008fc9154 /src/util/ite_removal.h | |
parent | 91424455840a7365a328cbcc3d02ec453fe9d0ea (diff) |
Substantial Changes:
-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.
- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.
- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.
Minor Changes:
- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.
- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
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 */ |