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/theory/ite_simplifier.cpp | |
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/theory/ite_simplifier.cpp')
-rw-r--r-- | src/theory/ite_simplifier.cpp | 501 |
1 files changed, 0 insertions, 501 deletions
diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp deleted file mode 100644 index 463a9c41a..000000000 --- a/src/theory/ite_simplifier.cpp +++ /dev/null @@ -1,501 +0,0 @@ -/********************* */ -/*! \file ite_simplifier.cpp - ** \verbatim - ** Original author: Clark Barrett - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Simplifications for ITE expressions - ** - ** This module implements preprocessing phases designed to simplify ITE - ** expressions. Based on: - ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009. - ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC '96 - **/ - - -#include "theory/ite_simplifier.h" - - -using namespace std; -using namespace CVC4; -using namespace theory; - - -bool ITESimplifier::containsTermITE(TNode e) -{ - if (e.getKind() == kind::ITE && !e.getType().isBoolean()) { - return true; - } - - hash_map<Node, bool, NodeHashFunction>::iterator it; - it = d_containsTermITECache.find(e); - if (it != d_containsTermITECache.end()) { - return (*it).second; - } - - size_t k = 0, sz = e.getNumChildren(); - for (; k < sz; ++k) { - if (containsTermITE(e[k])) { - d_containsTermITECache[e] = true; - return true; - } - } - - d_containsTermITECache[e] = false; - return false; -} - - -bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid) -{ - Assert((e.getKind() == kind::ITE && !e.getType().isBoolean()) || - Theory::theoryOf(e) != THEORY_BOOL); - if (e.isConst()) { - return true; - } - - hash_map<Node, bool, NodeHashFunction>::iterator it; - it = d_leavesConstCache.find(e); - if (it != d_leavesConstCache.end()) { - return (*it).second; - } - - if (!containsTermITE(e) && Theory::isLeafOf(e, tid)) { - d_leavesConstCache[e] = false; - return false; - } - - Assert(e.getNumChildren() > 0); - size_t k = 0, sz = e.getNumChildren(); - - if (e.getKind() == kind::ITE) { - k = 1; - } - - for (; k < sz; ++k) { - if (!leavesAreConst(e[k], tid)) { - d_leavesConstCache[e] = false; - return false; - } - } - d_leavesConstCache[e] = true; - return true; -} - - -Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVar) -{ - NodePairMap::iterator it; - it = d_simpConstCache.find(pair<Node, Node>(simpContext,iteNode)); - if (it != d_simpConstCache.end()) { - return (*it).second; - } - - if (iteNode.getKind() == kind::ITE) { - NodeBuilder<> builder(kind::ITE); - builder << iteNode[0]; - unsigned i = 1; - for (; i < iteNode.getNumChildren(); ++ i) { - Node n = simpConstants(simpContext, iteNode[i], simpVar); - if (n.isNull()) { - return n; - } - builder << n; - } - // Mark the substitution and continue - Node result = builder; - result = Rewriter::rewrite(result); - d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result; - return result; - } - - if (!containsTermITE(iteNode)) { - Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode)); - d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n; - return n; - } - - Node iteNode2; - Node simpVar2; - d_simpContextCache.clear(); - Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2); - if (!simpContext2.isNull()) { - Assert(!iteNode2.isNull()); - simpContext2 = simpContext.substitute(simpVar, simpContext2); - Node n = simpConstants(simpContext2, iteNode2, simpVar2); - if (n.isNull()) { - return n; - } - d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n; - return n; - } - return Node(); -} - - -Node ITESimplifier::getSimpVar(TypeNode t) -{ - std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it; - it = d_simpVars.find(t); - if (it != d_simpVars.end()) { - return (*it).second; - } - else { - Node var = NodeManager::currentNM()->mkSkolem("iteSimp_$$", t, "is a variable resulting from ITE simplification"); - d_simpVars[t] = var; - return var; - } -} - - -Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) -{ - NodeMap::iterator it; - it = d_simpContextCache.find(c); - if (it != d_simpContextCache.end()) { - return (*it).second; - } - - if (!containsTermITE(c)) { - d_simpContextCache[c] = c; - return c; - } - - if (c.getKind() == kind::ITE && !c.getType().isBoolean()) { - // Currently only support one ite node in a simp context - // Return Null if more than one is found - if (!iteNode.isNull()) { - return Node(); - } - simpVar = getSimpVar(c.getType()); - if (simpVar.isNull()) { - return Node(); - } - d_simpContextCache[c] = simpVar; - iteNode = c; - return simpVar; - } - - NodeBuilder<> builder(c.getKind()); - if (c.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << c.getOperator(); - } - unsigned i = 0; - for (; i < c.getNumChildren(); ++ i) { - Node newChild = createSimpContext(c[i], iteNode, simpVar); - if (newChild.isNull()) { - return newChild; - } - builder << newChild; - } - // Mark the substitution and continue - Node result = builder; - d_simpContextCache[c] = result; - return result; -} - - -Node ITESimplifier::simpITEAtom(TNode atom) -{ - if (leavesAreConst(atom)) { - Node iteNode; - Node simpVar; - d_simpContextCache.clear(); - Node simpContext = createSimpContext(atom, iteNode, simpVar); - if (!simpContext.isNull()) { - if (iteNode.isNull()) { - Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext)); - return Rewriter::rewrite(simpContext); - } - Node n = simpConstants(simpContext, iteNode, simpVar); - if (!n.isNull()) { - return n; - } - } - } - return atom; -} - - -struct preprocess_stack_element { - TNode node; - bool children_added; - preprocess_stack_element(TNode node) - : node(node), children_added(false) {} -};/* struct preprocess_stack_element */ - - -Node ITESimplifier::simpITE(TNode assertion) -{ - // Do a topological sort of the subexpressions and substitute them - vector<preprocess_stack_element> toVisit; - toVisit.push_back(assertion); - - while (!toVisit.empty()) - { - // The current node we are processing - preprocess_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.node; - - // If node has no ITE's or already in the cache we're done, pop from the stack - if (current.getNumChildren() == 0 || - (Theory::theoryOf(current) != THEORY_BOOL && !containsTermITE(current))) { - d_simpITECache[current] = current; - toVisit.pop_back(); - continue; - } - - NodeMap::iterator find = d_simpITECache.find(current); - if (find != d_simpITECache.end()) { - toVisit.pop_back(); - continue; - } - - // Not yet substituted, so process - if (stackHead.children_added) { - // Children have been processed, so substitute - NodeBuilder<> builder(current.getKind()); - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << current.getOperator(); - } - for (unsigned i = 0; i < current.getNumChildren(); ++ i) { - Assert(d_simpITECache.find(current[i]) != d_simpITECache.end()); - builder << d_simpITECache[current[i]]; - } - // Mark the substitution and continue - Node result = builder; - - // If this is an atom, we process it - if (Theory::theoryOf(result) != THEORY_BOOL && - result.getType().isBoolean()) { - result = simpITEAtom(result); - } - - result = Rewriter::rewrite(result); - d_simpITECache[current] = result; - toVisit.pop_back(); - } else { - // Mark that we have added the children if any - if (current.getNumChildren() > 0) { - stackHead.children_added = true; - // We need to add the children - for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { - TNode childNode = *child_it; - NodeMap::iterator childFind = d_simpITECache.find(childNode); - if (childFind == d_simpITECache.end()) { - toVisit.push_back(childNode); - } - } - } else { - // No children, so we're done - d_simpITECache[current] = current; - toVisit.pop_back(); - } - } - } - return d_simpITECache[assertion]; -} - - -ITESimplifier::CareSetPtr ITESimplifier::getNewSet() -{ - if (d_usedSets.empty()) { - return ITESimplifier::CareSetPtr::mkNew(*this); - } - else { - ITESimplifier::CareSetPtr cs = ITESimplifier::CareSetPtr::recycle(d_usedSets.back()); - cs.getCareSet().clear(); - d_usedSets.pop_back(); - return cs; - } -} - - -void ITESimplifier::updateQueue(CareMap& queue, - TNode e, - ITESimplifier::CareSetPtr& careSet) -{ - CareMap::iterator it = queue.find(e), iend = queue.end(); - if (it != iend) { - set<Node>& cs2 = (*it).second.getCareSet(); - ITESimplifier::CareSetPtr csNew = getNewSet(); - set_intersection(careSet.getCareSet().begin(), - careSet.getCareSet().end(), - cs2.begin(), cs2.end(), - inserter(csNew.getCareSet(), csNew.getCareSet().begin())); - (*it).second = csNew; - } - else { - queue[e] = careSet; - } -} - - -Node ITESimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cache) -{ - TNodeMap::iterator it = cache.find(e), iend = cache.end(); - if (it != iend) { - return it->second; - } - - // do substitution? - it = substTable.find(e); - iend = substTable.end(); - if (it != iend) { - Node result = substitute(it->second, substTable, cache); - cache[e] = result; - return result; - } - - size_t sz = e.getNumChildren(); - if (sz == 0) { - cache[e] = e; - return e; - } - - NodeBuilder<> builder(e.getKind()); - if (e.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << e.getOperator(); - } - for (unsigned i = 0; i < e.getNumChildren(); ++ i) { - builder << substitute(e[i], substTable, cache); - } - - Node result = builder; - // it = substTable.find(result); - // if (it != iend) { - // result = substitute(it->second, substTable, cache); - // } - cache[e] = result; - return result; -} - - -Node ITESimplifier::simplifyWithCare(TNode e) -{ - TNodeMap substTable; - CareMap queue; - CareMap::iterator it; - ITESimplifier::CareSetPtr cs = getNewSet(); - ITESimplifier::CareSetPtr cs2; - queue[e] = cs; - - TNode v; - bool done; - unsigned i; - - while (!queue.empty()) { - it = queue.end(); - --it; - v = it->first; - cs = it->second; - set<Node>& css = cs.getCareSet(); - queue.erase(v); - - done = false; - set<Node>::iterator iCare, iCareEnd = css.end(); - - switch (v.getKind()) { - case kind::ITE: { - iCare = css.find(v[0]); - if (iCare != iCareEnd) { - Assert(substTable.find(v) == substTable.end()); - substTable[v] = v[1]; - updateQueue(queue, v[1], cs); - done = true; - break; - } - else { - iCare = css.find(v[0].negate()); - if (iCare != iCareEnd) { - Assert(substTable.find(v) == substTable.end()); - substTable[v] = v[2]; - updateQueue(queue, v[2], cs); - done = true; - break; - } - } - updateQueue(queue, v[0], cs); - cs2 = getNewSet(); - cs2.getCareSet() = css; - cs2.getCareSet().insert(v[0]); - updateQueue(queue, v[1], cs2); - cs2 = getNewSet(); - cs2.getCareSet() = css; - cs2.getCareSet().insert(v[0].negate()); - updateQueue(queue, v[2], cs2); - done = true; - break; - } - case kind::AND: { - for (i = 0; i < v.getNumChildren(); ++i) { - iCare = css.find(v[i].negate()); - if (iCare != iCareEnd) { - Assert(substTable.find(v) == substTable.end()); - substTable[v] = d_false; - done = true; - break; - } - } - if (done) break; - - Assert(v.getNumChildren() > 1); - updateQueue(queue, v[0], cs); - cs2 = getNewSet(); - cs2.getCareSet() = css; - cs2.getCareSet().insert(v[0]); - for (i = 1; i < v.getNumChildren(); ++i) { - updateQueue(queue, v[i], cs2); - } - done = true; - break; - } - case kind::OR: { - for (i = 0; i < v.getNumChildren(); ++i) { - iCare = css.find(v[i]); - if (iCare != iCareEnd) { - Assert(substTable.find(v) == substTable.end()); - substTable[v] = d_true; - done = true; - break; - } - } - if (done) break; - - Assert(v.getNumChildren() > 1); - updateQueue(queue, v[0], cs); - cs2 = getNewSet(); - cs2.getCareSet() = css; - cs2.getCareSet().insert(v[0].negate()); - for (i = 1; i < v.getNumChildren(); ++i) { - updateQueue(queue, v[i], cs2); - } - done = true; - break; - } - default: - break; - } - - if (done) { - continue; - } - - for (unsigned i = 0; i < v.getNumChildren(); ++i) { - updateQueue(queue, v[i], cs); - } - } - while (!d_usedSets.empty()) { - delete d_usedSets.back(); - d_usedSets.pop_back(); - } - - TNodeMap cache; - return substitute(e, substTable, cache); -} - |