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 | |
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')
28 files changed, 2697 insertions, 744 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 1858d4d32..d6a0ffe0a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -142,8 +142,8 @@ libcvc4_la_SOURCES = \ theory/shared_terms_database.cpp \ theory/term_registration_visitor.h \ theory/term_registration_visitor.cpp \ - theory/ite_simplifier.h \ - theory/ite_simplifier.cpp \ + theory/ite_utilities.h \ + theory/ite_utilities.cpp \ theory/unconstrained_simplifier.h \ theory/unconstrained_simplifier.cpp \ theory/quantifiers_engine.h \ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 92a21546c..056e68c69 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -26,6 +26,19 @@ namespace CVC4 { namespace expr { namespace attr { +AttributeManager::AttributeManager(context::Context* ctxt) : + d_cdbools(ctxt), + d_cdints(ctxt), + d_cdtnodes(ctxt), + d_cdnodes(ctxt), + d_cdstrings(ctxt), + d_cdptrs(ctxt), + d_inGarbageCollection(false) +{} + +bool AttributeManager::inGarbageCollection() const { + return d_inGarbageCollection; +} void AttributeManager::debugHook(int debugFlag) { /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS! @@ -36,6 +49,7 @@ void AttributeManager::debugHook(int debugFlag) { } void AttributeManager::deleteAllAttributes(NodeValue* nv) { + Assert(!inGarbageCollection()); d_bools.erase(nv); deleteFromTable(d_ints, nv); deleteFromTable(d_tnodes, nv); diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 605427190..1e3f25461 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -101,17 +101,14 @@ class AttributeManager { template <class T, bool context_dep> friend struct getTable; + bool d_inGarbageCollection; + + void clearDeleteAllAttributesBuffer(); + public: /** Construct an attribute manager. */ - AttributeManager(context::Context* ctxt) : - d_cdbools(ctxt), - d_cdints(ctxt), - d_cdtnodes(ctxt), - d_cdnodes(ctxt), - d_cdstrings(ctxt), - d_cdptrs(ctxt) { - } + AttributeManager(context::Context* ctxt); /** * Get a particular attribute on a particular node. @@ -177,6 +174,10 @@ public: */ void deleteAllAttributes(); + /** + * Returns true if a table is currently being deleted. + */ + bool inGarbageCollection() const ; /** * Determines the AttrTableId of an attribute. @@ -563,6 +564,8 @@ AttributeManager::setAttribute(NodeValue* nv, /** * Search for the NodeValue in all attribute tables and remove it, * calling the cleanup function if one is defined. + * + * This cannot use nv as anything other than a pointer! */ template <class T> inline void AttributeManager::deleteFromTable(AttrHash<T>& table, @@ -600,6 +603,9 @@ inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table, */ template <class T> inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) { + Assert(!d_inGarbageCollection); + d_inGarbageCollection = true; + bool anyRequireClearing = false; typedef AttributeTraits<T, false> traits_t; typedef AttrHash<T> hash_t; @@ -627,6 +633,8 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) { } } table.clear(); + d_inGarbageCollection = false; + Assert(!d_inGarbageCollection); } template <class AttrKind> @@ -639,6 +647,7 @@ AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){ template <class T> void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){ + d_inGarbageCollection = true; typedef AttributeTraits<T, false> traits_t; typedef AttrHash<T> hash_t; @@ -664,6 +673,7 @@ void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std:: ++it; } } + d_inGarbageCollection = false; static const size_t ReconstructShrinkRatio = 8; if(initialSize/ReconstructShrinkRatio > table.size()){ reconstructTable(table); @@ -672,10 +682,12 @@ void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std:: template <class T> void AttributeManager::reconstructTable(AttrHash<T>& table){ + d_inGarbageCollection = true; typedef AttrHash<T> hash_t; hash_t cpy; cpy.insert(table.begin(), table.end()); cpy.swap(table); + d_inGarbageCollection = false; } diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 8c94db3cc..9e7a2596f 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -65,6 +65,7 @@ exportConstant_cases= typerules= construles= +neverconstrules= seen_theory=false seen_theory_builtin=false @@ -168,6 +169,12 @@ function construle { #line $lineno \"$kf\" return $2::computeIsConst(nodeManager, n); " + neverconstrules="${neverconstrules} +#line $lineno \"$kf\" + case kind::$1: +#line $lineno \"$kf\" + return false; +" } function sort { @@ -294,6 +301,7 @@ for var in \ typechecker_includes \ typerules \ construles \ + neverconstrules \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done diff --git a/src/expr/node.cpp b/src/expr/node.cpp index b1614f31b..39bbfbc2e 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -73,6 +73,10 @@ bool NodeTemplate<ref_count>::isConst() const { Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl; return false; default: + if(expr::TypeChecker::neverIsConst(NodeManager::currentNM(), *this)){ + Debug("isConst") << "Node::isConst() returning false, the kind is never const" << std::endl; + return false; + } if(getAttribute(IsConstComputedAttr())) { bool bval = getAttribute(IsConstAttr()); Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index cede6ff1f..9c76a41f3 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -134,6 +134,7 @@ NodeManager::~NodeManager() { d_operators[i] = Node::null(); } + Assert(!d_attrManager->inGarbageCollection() ); while(!d_zombies.empty()) { reclaimZombies(); } @@ -161,6 +162,7 @@ NodeManager::~NodeManager() { void NodeManager::reclaimZombies() { // FIXME multithreading + Assert(!d_attrManager->inGarbageCollection()); Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n"; @@ -435,6 +437,23 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { return dtt; } +void NodeManager::reclaimAllZombies(){ + reclaimZombiesUntil(0u); +} + +/** Reclaim zombies while there are more than k nodes in the pool (if possible).*/ +void NodeManager::reclaimZombiesUntil(uint32_t k){ + if(safeToReclaimZombies()){ + while(poolSize() >= k && !d_zombies.empty()){ + reclaimZombies(); + } + } +} + +size_t NodeManager::poolSize() const{ + return d_nodeValuePool.size(); +} + TypeNode NodeManager::mkSort(uint32_t flags) { NodeBuilder<1> nb(this, kind::SORT_TYPE); Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); @@ -586,6 +605,11 @@ Node NodeManager::mkAbstractValue(const TypeNode& type) { return n; } +bool NodeManager::safeToReclaimZombies() const{ + // FIXME multithreading + return !d_inReclaimZombies && !d_attrManager->inGarbageCollection(); +} + void NodeManager::deleteAttributes(const std::vector<const expr::attr::AttributeUniqueId*>& ids){ d_attrManager->deleteAttributes(ids); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 32c492003..af771bd89 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -229,8 +229,7 @@ class NodeManager { } d_zombies.insert(nv);// FIXME multithreading - if(!d_inReclaimZombies) {// FIXME multithreading - // for now, collect eagerly. can add heuristic here later.. + if(safeToReclaimZombies()) { if(d_zombies.size() > 5000) { reclaimZombies(); } @@ -243,6 +242,11 @@ class NodeManager { void reclaimZombies(); /** + * It is safe to collect zombies. + */ + bool safeToReclaimZombies() const; + + /** * This template gives a mechanism to stack-allocate a NodeValue * with enough space for N children (where N is a compile-time * constant). You use it like this: @@ -860,6 +864,15 @@ public: */ static inline TypeNode fromType(Type t); + /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/ + void reclaimZombiesUntil(uint32_t k); + + /** Reclaims all zombies (if possible).*/ + void reclaimAllZombies(); + + /** Size of the node pool. */ + size_t poolSize() const; + /** Deletes a list of attributes from the NM's AttributeManager.*/ void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids); @@ -871,7 +884,6 @@ public: * any published code! */ void debugHook(int debugFlag); - };/* class NodeManager */ /** diff --git a/src/expr/options b/src/expr/options index 223189d1b..cf893a7a5 100644 --- a/src/expr/options +++ b/src/expr/options @@ -21,5 +21,8 @@ option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :defaul option typeChecking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking never type check expressions +option biasedITERemoval --biased-ites bool :default false + try the new remove ite pass that is biased against term ites appearing + endmodule diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h index ac461bb7b..d34a7c7d6 100644 --- a/src/expr/type_checker.h +++ b/src/expr/type_checker.h @@ -34,6 +34,9 @@ public: static bool computeIsConst(NodeManager* nodeManager, TNode n) throw (AssertionException); + static bool neverIsConst(NodeManager* nodeManager, TNode n) + throw (AssertionException); + };/* class TypeChecker */ }/* CVC4::expr namespace */ diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index b2138c9a1..4e476f4d9 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -78,5 +78,22 @@ ${construles} }/* TypeChecker::computeIsConst */ +bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n) + throw (AssertionException) { + + Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED); + + switch(n.getKind()) { +${neverconstrules} + +#line 90 "${template}" + + default:; + } + + return true; + +}/* TypeChecker::neverIsConst */ + }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/smt/options b/src/smt/options index d2455b520..6b9944cdd 100644 --- a/src/smt/options +++ b/src/smt/options @@ -42,18 +42,31 @@ common-option interactive interactive-mode --interactive bool :read-write option doITESimp --ite-simp bool :read-write turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) +option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false + do the ite simplification pass again if repeating simplification + +option simplifyWithCareEnabled --simp-with-care bool :default false :read-write + enables simplifyWithCare in ite simplificiation + +option compressItes --simp-ite-compress bool :default false :read-write + enables compressing ites after ite simplification + option unconstrainedSimp --unconstrained-simp bool :default false :read-write turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis) option repeatSimp --repeat-simp bool :read-write make multiple passes with nonclausal simplifier +option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288 + post ite compression enables zombie removal while the number of nodes is above this threshold + option sortInference --sort-inference bool :read-write :default false calculate sort inference of input problem, convert the input based on monotonic sorts common-option incrementalSolving incremental -i --incremental bool enable incremental solving + option abstractValues abstract-values --abstract-values bool :default false in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard option modelUninterpDtEnum --model-u-dt-enum bool :default false diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 21f2d9209..2cc606fa9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -52,6 +52,7 @@ #include "util/node_visitor.h" #include "util/configuration.h" #include "util/exception.h" +#include "util/nary_builder.h" #include "smt/command_list.h" #include "smt/boolean_terms.h" #include "smt/options.h" @@ -90,6 +91,19 @@ namespace CVC4 { namespace smt { +/** Useful for counting the number of recursive calls. */ +class ScopeCounter { +private: + unsigned& d_depth; +public: + ScopeCounter(unsigned& d) : d_depth(d) { + ++d_depth; + } + ~ScopeCounter(){ + --d_depth; + } +}; + /** * Representation of a defined function. We keep these around in * SmtEngine to permit expanding definitions late (and lazily), to @@ -150,6 +164,9 @@ struct SmtEngineStatistics { /** time spent in processAssertions() */ TimerStat d_processAssertionsTime; + /** Has something simplified to false? */ + IntStat d_simplifiedToFalse; + SmtEngineStatistics() : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"), @@ -168,7 +185,10 @@ struct SmtEngineStatistics { d_checkModelTime("smt::SmtEngine::checkModelTime"), d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), - d_processAssertionsTime("smt::SmtEngine::processAssertionsTime") { + d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), + d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) + + { StatisticsRegistry::registerStat(&d_definitionExpansionTime); StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime); @@ -188,6 +208,7 @@ struct SmtEngineStatistics { StatisticsRegistry::registerStat(&d_solveTime); StatisticsRegistry::registerStat(&d_pushPopTime); StatisticsRegistry::registerStat(&d_processAssertionsTime); + StatisticsRegistry::registerStat(&d_simplifiedToFalse); } ~SmtEngineStatistics() { @@ -209,6 +230,7 @@ struct SmtEngineStatistics { StatisticsRegistry::unregisterStat(&d_solveTime); StatisticsRegistry::unregisterStat(&d_pushPopTime); StatisticsRegistry::unregisterStat(&d_processAssertionsTime); + StatisticsRegistry::unregisterStat(&d_simplifiedToFalse); } };/* struct SmtEngineStatistics */ @@ -305,6 +327,10 @@ class SmtEnginePrivate : public NodeManagerListener { */ Node d_modZero; + /** Number of calls of simplify assertions active. + */ + unsigned d_simplifyAssertionsDepth; + public: /** * Map from skolem variables to index in d_assertionsToCheck containing @@ -353,11 +379,15 @@ private: void bvToBool(); // Simplify ITE structure - void simpITE(); + bool simpITE(); // Simplify based on unconstrained values void unconstrainedSimp(); + // Ensures the assertions asserted after before now + // effectively come before d_realAssertionsEnd + void compressBeforeRealAssertions(size_t before); + /** * Any variable in an assertion that is declared as a subtype type * (predicate subtype or integer subrange type) must be constrained @@ -402,6 +432,7 @@ public: d_divByZero(), d_intDivByZero(), d_modZero(), + d_simplifyAssertionsDepth(0), d_iteSkolemMap(), d_iteRemover(smt.d_userContext), d_topLevelSubstitutions(smt.d_userContext) @@ -869,12 +900,41 @@ void SmtEngine::setLogicInternal() throw() { } // Turn on ite simplification for QF_LIA and QF_AUFBV if(! options::doITESimp.wasSetByUser()) { - bool iteSimp = !d_logic.isQuantified() && - ((d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areRealsUsed()) || - (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV))); + bool qf_aufbv = !d_logic.isQuantified() && + d_logic.isTheoryEnabled(THEORY_ARRAY) && + d_logic.isTheoryEnabled(THEORY_UF) && + d_logic.isTheoryEnabled(THEORY_BV); + bool qf_lia = !d_logic.isQuantified() && + d_logic.isPure(THEORY_ARITH) && + d_logic.isLinear() && + !d_logic.isDifferenceLogic() && + !d_logic.areRealsUsed(); + + bool iteSimp = (qf_aufbv || qf_lia); Trace("smt") << "setting ite simplification to " << iteSimp << endl; options::doITESimp.set(iteSimp); } + if(! options::compressItes.wasSetByUser() ){ + bool qf_lia = !d_logic.isQuantified() && + d_logic.isPure(THEORY_ARITH) && + d_logic.isLinear() && + !d_logic.isDifferenceLogic() && + !d_logic.areRealsUsed(); + + bool compressIte = qf_lia; + Trace("smt") << "setting ite compression to " << compressIte << endl; + options::compressItes.set(compressIte); + } + if(! options::simplifyWithCareEnabled.wasSetByUser() ){ + bool qf_aufbv = !d_logic.isQuantified() && + d_logic.isTheoryEnabled(THEORY_ARRAY) && + d_logic.isTheoryEnabled(THEORY_UF) && + d_logic.isTheoryEnabled(THEORY_BV); + + bool withCare = qf_aufbv; + Trace("smt") << "setting ite simplify with care to " << withCare << endl; + options::simplifyWithCareEnabled.set(withCare); + } // Turn off array eager index splitting for QF_AUFLIA if(! options::arraysEagerIndexSplitting.wasSetByUser()) { if (not d_logic.isQuantified() && @@ -2031,16 +2091,56 @@ void SmtEnginePrivate::bvToBool() { } } -void SmtEnginePrivate::simpITE() { +bool SmtEnginePrivate::simpITE() { TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl; + unsigned numAssertionOnEntry = d_assertionsToCheck.size(); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) { - d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]); + Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]); + d_assertionsToCheck[i] = result; + if(result.isConst() && !result.getConst<bool>()){ + return false; + } } + bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertionsToCheck); + if(numAssertionOnEntry < d_assertionsToCheck.size()){ + compressBeforeRealAssertions(numAssertionOnEntry); + } + return result; } +void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ + size_t curr = d_assertionsToCheck.size(); + if(before >= curr || + d_realAssertionsEnd <= 0 || + d_realAssertionsEnd >= curr){ + return; + } + + // assertions + // original: [0 ... d_realAssertionsEnd) + // can be modified + // ites skolems [d_realAssertionsEnd, before) + // cannot be moved + // added [before, curr) + // can be modified + Assert(0 < d_realAssertionsEnd); + Assert(d_realAssertionsEnd <= before); + Assert(before < curr); + + std::vector<Node> intoConjunction; + for(size_t i = before; i<curr; ++i){ + intoConjunction.push_back(d_assertionsToCheck[i]); + } + d_assertionsToCheck.resize(before); + size_t lastBeforeItes = d_realAssertionsEnd - 1; + intoConjunction.push_back(d_assertionsToCheck[lastBeforeItes]); + Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); + d_assertionsToCheck[lastBeforeItes] = newLast; + Assert(d_assertionsToCheck.size() == before); +} void SmtEnginePrivate::unconstrainedSimp() { TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime); @@ -2490,11 +2590,13 @@ void SmtEnginePrivate::doMiplibTrick() { d_realAssertionsEnd = d_assertionsToCheck.size(); } + // returns false if simplification led to "false" bool SmtEnginePrivate::simplifyAssertions() throw(TypeCheckingException, LogicException) { Assert(d_smt.d_pendingPops == 0); try { + ScopeCounter depth(d_simplifyAssertionsDepth); Trace("simplify") << "SmtEnginePrivate::simplify()" << endl; @@ -2560,9 +2662,14 @@ bool SmtEnginePrivate::simplifyAssertions() Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; // ITE simplification - if(options::doITESimp()) { + if(options::doITESimp() && + (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) { Chat() << "...doing ITE simplification..." << endl; - simpITE(); + bool noConflict = simpITE(); + if(!noConflict){ + Chat() << "...ITE simplification found unsat..." << endl; + return false; + } } dumpAssertions("post-itesimp", d_assertionsToCheck); @@ -2916,6 +3023,9 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("pre-simplify", d_assertionsToPreprocess); Chat() << "simplifying assertions..." << endl; bool noConflict = simplifyAssertions(); + if(!noConflict){ + ++(d_smt.d_stats->d_simplifiedToFalse); + } dumpAssertions("post-simplify", d_assertionsToCheck); dumpAssertions("pre-static-learning", d_assertionsToCheck); @@ -2954,6 +3064,7 @@ void SmtEnginePrivate::processAssertions() { if(options::repeatSimp()) { d_assertionsToCheck.swap(d_assertionsToPreprocess); Chat() << "re-simplifying assertions..." << endl; + ScopeCounter depth(d_simplifyAssertionsDepth); noConflict &= simplifyAssertions(); if (noConflict) { // Need to fix up assertion list to maintain invariants: diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 9867ccd4e..1caa4b429 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -22,6 +22,10 @@ namespace CVC4 { namespace theory { namespace booleans { +RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) { + return preRewrite(node); +} + /** * flattenNode looks for children of same kind, and if found merges * them into the parent. @@ -88,6 +92,40 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) } } +// Equality parity returns +// * 0 if no relation between a and b is found +// * 1 if a == b +// * 2 if a == not(b) +// * 3 or b == not(a) +inline int equalityParity(TNode a, TNode b){ + if(a == b){ + return 1; + }else if(a.getKind() == kind::NOT && a[0] == b){ + return 2; + }else if(b.getKind() == kind::NOT && b[0] == a){ + return 3; + }else{ + return 0; + } +} + +inline Node makeNegation(TNode n){ + bool even = false; + while(n.getKind() == kind::NOT){ + n = n[0]; + even = !even; + } + if(even){ + return n; + } else { + if(n.isConst()){ + return NodeManager::currentNM()->mkConst(!n.getConst<bool>()); + }else{ + return n.notNode(); + } + } +} + RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); Node tt = nodeManager->mkConst(true); @@ -132,7 +170,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff); if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); - if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); break; } case kind::IFF: @@ -146,10 +184,10 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { return RewriteResponse(REWRITE_AGAIN, n[0]); } else if(n[0] == ff) { // IFF false x - return RewriteResponse(REWRITE_AGAIN, n[1].notNode()); + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1])); } else if(n[1] == ff) { // IFF x false - return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } else if(n[0] == n[1]) { // IFF x x return RewriteResponse(REWRITE_DONE, tt); @@ -207,7 +245,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if(kappa.knownLessThanOrEqual(two)){ return RewriteResponse(REWRITE_DONE, ff); }else{ - Node neitherEquality = (n[0].notNode()).andNode(n[1].notNode()); + Node neitherEquality = (makeNegation(n[0])).andNode(makeNegation(n[1])); return RewriteResponse(REWRITE_AGAIN, neitherEquality); } } @@ -219,10 +257,10 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { // rewrite simple cases of XOR if(n[0] == tt) { // XOR true x - return RewriteResponse(REWRITE_AGAIN, n[1].notNode()); + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1])); } else if(n[1] == tt) { // XCR x true - return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } else if(n[0] == ff) { // XOR false x return RewriteResponse(REWRITE_AGAIN, n[1]); @@ -248,33 +286,79 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if (n[0].isConst()) { if (n[0] == tt) { // ITE true x y + + Debug("bool-ite") << "n[0] ==tt " << n << ": " << n[1] << std::endl; return RewriteResponse(REWRITE_AGAIN, n[1]); } else { Assert(n[0] == ff); // ITE false x y + Debug("bool-ite") << "n[0] ==ff " << n << ": " << n[1] << std::endl; return RewriteResponse(REWRITE_AGAIN, n[2]); } } else if (n[1].isConst()) { if (n[1] == tt && n[2] == ff) { + Debug("bool-ite") << "n[1] ==tt && n[2] == ff " << n << ": " << n[0] << std::endl; return RewriteResponse(REWRITE_AGAIN, n[0]); } else if (n[1] == ff && n[2] == tt) { - return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + Debug("bool-ite") << "n[1] ==ff && n[2] == tt " << n << ": " << n[0].notNode() << std::endl; + return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } + // else if(n[1] == ff){ + // Node resp = (n[0].notNode()).andNode(n[2]); + // return RewriteResponse(REWRITE_AGAIN, resp); + // } } - if (n[1] == n[2]) { - return RewriteResponse(REWRITE_AGAIN, n[1]); + // else if (n[2].isConst()) { + // if(n[2] == ff){ + // Node resp = (n[0]).andNode(n[1]); + // return RewriteResponse(REWRITE_AGAIN, resp); + // } + // } + + int parityTmp; + if ((parityTmp = equalityParity(n[1], n[2])) != 0) { + Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].iffNode(n[1]); + Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp + << " " << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); // Curiously, this rewrite affects several benchmarks dramatically, including copy_array and some simple_startup - disable for now // } else if (n[0].getKind() == kind::NOT) { // return RewriteResponse(REWRITE_AGAIN, n[0][0].iteNode(n[2], n[1])); - } else if (n[0] == n[1]) { - return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(tt, n[2])); - } else if (n[0] == n[2]) { - return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], ff)); - } else if (n[1].getKind() == kind::NOT && n[1][0] == n[0]) { - return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(ff, n[2])); - } else if (n[2].getKind() == kind::NOT && n[2][0] == n[0]) { - return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], tt)); + } else if(!n[1].isConst() && (parityTmp = equalityParity(n[0], n[1])) != 0){ + // (parityTmp == 1) if n[0] == n[1] + // otherwise, n[0] == not(n[1]) or not(n[0]) == n[1] + + // if n[1] is constant this can loop, this is possible in prewrite + Node resp = n[0].iteNode( (parityTmp == 1) ? tt : ff, n[2]); + Debug("bool-ite") << "equalityParity n[0], n[1] " << parityTmp + << " " << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } else if(!n[2].isConst() && (parityTmp = equalityParity(n[0], n[2])) != 0){ + // (parityTmp == 1) if n[0] == n[2] + // otherwise, n[0] == not(n[2]) or not(n[0]) == n[2] + Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? ff : tt); + Debug("bool-ite") << "equalityParity n[0], n[2] " << parityTmp + << " " << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } else if(n[1].getKind() == kind::ITE && + (parityTmp = equalityParity(n[0], n[1][0])) != 0){ + // (parityTmp == 1) then n : (ite c (ite c x y) z) + // (parityTmp > 1) then n : (ite c (ite (not c) x y) z) or + // n: (ite (not c) (ite c x y) z) + Node resp = n[0].iteNode((parityTmp == 1) ? n[1][1] : n[1][2], n[2]); + Debug("bool-ite") << "equalityParity n[0], n[1][0] " << parityTmp + << " " << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } else if(n[2].getKind() == kind::ITE && + (parityTmp = equalityParity(n[0], n[2][0])) != 0){ + // (parityTmp == 1) then n : (ite c x (ite c y z)) + // (parityTmp > 1) then n : (ite c x (ite (not c) y z)) or + // n: (ite (not c) x (ite c y z)) + Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? n[2][2] : n[2][1]); + Debug("bool-ite") << "equalityParity n[0], n[2][0] " << parityTmp + << " " << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); } break; } diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index 96bd2ae29..ac9469980 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -31,9 +31,7 @@ class TheoryBoolRewriter { public: static RewriteResponse preRewrite(TNode node); - static RewriteResponse postRewrite(TNode node) { - return preRewrite(node); - } + static RewriteResponse postRewrite(TNode node); static void init() {} static void shutdown() {} 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); -} - diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h deleted file mode 100644 index 07fa0dedb..000000000 --- a/src/theory/ite_simplifier.h +++ /dev/null @@ -1,165 +0,0 @@ -/********************* */ -/*! \file ite_simplifier.h - ** \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 "cvc4_private.h" - -#ifndef __CVC4__ITE_SIMPLIFIER_H -#define __CVC4__ITE_SIMPLIFIER_H - -#include <deque> -#include <vector> -#include <utility> - -#include "expr/node.h" -#include "expr/command.h" -#include "prop/prop_engine.h" -#include "context/cdhashset.h" -#include "theory/theory.h" -#include "theory/rewriter.h" -#include "theory/shared_terms_database.h" -#include "theory/term_registration_visitor.h" -#include "theory/valuation.h" -#include "util/statistics_registry.h" -#include "util/hash.h" -#include "util/cache.h" -#include "util/ite_removal.h" - -namespace CVC4 { -namespace theory { - -class ITESimplifier { - Node d_true; - Node d_false; - - std::hash_map<Node, bool, NodeHashFunction> d_containsTermITECache; - bool containsTermITE(TNode e); - - std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache; - bool leavesAreConst(TNode e, theory::TheoryId tid); - bool leavesAreConst(TNode e) - { return leavesAreConst(e, theory::Theory::theoryOf(e)); } - - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; - typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; - - typedef std::pair<Node, Node> NodePair; - struct NodePairHashFunction { - size_t operator () (const NodePair& pair) const { - size_t hash = 0; - hash = 0x9e3779b9 + NodeHashFunction().operator()(pair.first); - hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2); - return hash; - } - };/* struct ITESimplifier::NodePairHashFunction */ - - typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap; - - - NodePairMap d_simpConstCache; - Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar); - std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; - Node getSimpVar(TypeNode t); - - NodeMap d_simpContextCache; - Node createSimpContext(TNode c, Node& iteNode, Node& simpVar); - - Node simpITEAtom(TNode atom); - - NodeMap d_simpITECache; - -public: - Node simpITE(TNode assertion); - -private: - - class CareSetPtr; - class CareSetPtrVal { - friend class ITESimplifier::CareSetPtr; - ITESimplifier& d_iteSimplifier; - unsigned d_refCount; - std::set<Node> d_careSet; - CareSetPtrVal(ITESimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {} - }; - - std::vector<CareSetPtrVal*> d_usedSets; - void careSetPtrGC(CareSetPtrVal* val) { - d_usedSets.push_back(val); - } - - class CareSetPtr { - CareSetPtrVal* d_val; - CareSetPtr(CareSetPtrVal* val) : d_val(val) {} - public: - CareSetPtr() : d_val(NULL) {} - CareSetPtr(const CareSetPtr& cs) { - d_val = cs.d_val; - if (d_val != NULL) { - ++(d_val->d_refCount); - } - } - ~CareSetPtr() { - if (d_val != NULL && (--(d_val->d_refCount) == 0)) { - d_val->d_iteSimplifier.careSetPtrGC(d_val); - } - } - CareSetPtr& operator=(const CareSetPtr& cs) { - if (d_val != cs.d_val) { - if (d_val != NULL && (--(d_val->d_refCount) == 0)) { - d_val->d_iteSimplifier.careSetPtrGC(d_val); - } - d_val = cs.d_val; - if (d_val != NULL) { - ++(d_val->d_refCount); - } - } - return *this; - } - std::set<Node>& getCareSet() { return d_val->d_careSet; } - static CareSetPtr mkNew(ITESimplifier& simp) { - CareSetPtrVal* val = new CareSetPtrVal(simp); - return CareSetPtr(val); - } - static CareSetPtr recycle(CareSetPtrVal* val) { - Assert(val != NULL && val->d_refCount == 0); - val->d_refCount = 1; - return CareSetPtr(val); - } - }; - - CareSetPtr getNewSet(); - - typedef std::map<TNode, CareSetPtr> CareMap; - void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet); - Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache); - -public: - Node simplifyWithCare(TNode e); - - ITESimplifier() { - d_true = NodeManager::currentNM()->mkConst<bool>(true); - d_false = NodeManager::currentNM()->mkConst<bool>(false); - } - ~ITESimplifier() {} - -}; - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp new file mode 100644 index 000000000..facd5f4f0 --- /dev/null +++ b/src/theory/ite_utilities.cpp @@ -0,0 +1,1613 @@ +/********************* */ +/*! \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_utilities.h" +#include <utility> +#include "theory/rewriter.h" +#include "theory/theory.h" + +using namespace std; +namespace CVC4 { +namespace theory { + +namespace ite { +inline static bool isTermITE(TNode e) { + return (e.getKind() == kind::ITE && !e.getType().isBoolean()); +} + +inline static bool triviallyContainsNoTermITEs(TNode e) { + return e.isConst() || e.isVar(); +} + +static bool isTheoryAtom(TNode a){ + using namespace kind; + switch(a.getKind()){ + case EQUAL: + case DISTINCT: + return !(a[0].getType().isBoolean()); + + /* from uf */ + case APPLY_UF: + return a.getType().isBoolean(); + case CARDINALITY_CONSTRAINT: + case DIVISIBLE: + case LT: + case LEQ: + case GT: + case GEQ: + case IS_INTEGER: + case BITVECTOR_COMP: + case BITVECTOR_ULT: + case BITVECTOR_ULE: + case BITVECTOR_UGT: + case BITVECTOR_UGE: + case BITVECTOR_SLT: + case BITVECTOR_SLE: + case BITVECTOR_SGT: + case BITVECTOR_SGE: + return true; + default: + return false; + } +} + +struct CTIVStackElement { + TNode curr; + unsigned pos; + CTIVStackElement(){} + CTIVStackElement(TNode c) : curr(c), pos(0){ } +};/* CTIVStackElement */ + +} /* CVC4::theory::ite */ + + + +ITEUtilities::ITEUtilities(ContainsTermITEVistor* containsVisitor) + : d_containsVisitor(containsVisitor) + , d_compressor(NULL) + , d_simplifier(NULL) + , d_careSimp(NULL) +{ + Assert(d_containsVisitor != NULL); +} + +ITEUtilities::~ITEUtilities(){ + + if(d_simplifier != NULL){ + delete d_simplifier; + } + if(d_compressor != NULL){ + delete d_compressor; + } + if(d_careSimp != NULL){ + delete d_careSimp; + } +} + +Node ITEUtilities::simpITE(TNode assertion){ + if(d_simplifier == NULL){ + d_simplifier = new ITESimplifier(d_containsVisitor); + } + return d_simplifier->simpITE(assertion); +} + +bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const{ + if(d_simplifier == NULL){ + return false; + }else{ + return d_simplifier->doneALotOfWorkHeuristic(); + } +} + +/* returns false if an assertion is discovered to be equal to false. */ +bool ITEUtilities::compress(std::vector<Node>& assertions){ + if(d_compressor == NULL){ + d_compressor = new ITECompressor(d_containsVisitor); + } + return d_compressor->compress(assertions); +} + +Node ITEUtilities::simplifyWithCare(TNode e){ + if(d_careSimp == NULL){ + d_careSimp = new ITECareSimplifier(); + } + return d_careSimp->simplifyWithCare(e); +} + +void ITEUtilities::clear(){ + if(d_simplifier != NULL){ + d_simplifier->clearSimpITECaches(); + } + if(d_compressor != NULL){ + d_compressor->garbageCollect(); + } + if(d_careSimp != NULL){ + d_careSimp->clear(); + } +} + +/********************* */ +/* ContainsTermITEVistor + */ +ContainsTermITEVistor::ContainsTermITEVistor(): d_cache() {} +ContainsTermITEVistor::~ContainsTermITEVistor(){} +bool ContainsTermITEVistor::containsTermITE(TNode e){ + /* throughout execution skip through NOT nodes. */ + e = (e.getKind() == kind::NOT) ? e[0] : e; + if(ite::triviallyContainsNoTermITEs(e)){ return false; } + + NodeBoolMap::const_iterator end = d_cache.end(); + NodeBoolMap::const_iterator tmp_it = d_cache.find(e); + if(tmp_it != end){ + return (*tmp_it).second; + } + + bool foundTermIte = false; + std::vector<ite::CTIVStackElement> stack; + stack.push_back(ite::CTIVStackElement(e)); + while(!foundTermIte && !stack.empty()){ + ite::CTIVStackElement& top = stack.back(); + TNode curr = top.curr; + if(top.pos >= curr.getNumChildren()){ + // all of the children have been visited + // no term ites were found + d_cache[curr] = false; + stack.pop_back(); + }else{ + // this is someone's child + TNode child = curr[top.pos]; + child = (child.getKind() == kind::NOT) ? child[0] : child; + ++top.pos; + if(ite::triviallyContainsNoTermITEs(child)){ + // skip + }else{ + tmp_it = d_cache.find(child); + if(tmp_it != end){ + foundTermIte = (*tmp_it).second; + }else{ + stack.push_back(ite::CTIVStackElement(child)); + foundTermIte = ite::isTermITE(child); + } + } + } + } + if(foundTermIte){ + while(!stack.empty()){ + TNode curr = stack.back().curr; + stack.pop_back(); + d_cache[curr] = true; + } + } + return foundTermIte; +} +void ContainsTermITEVistor::garbageCollect() { + d_cache.clear(); +} + +/********************* */ +/* IncomingArcCounter + */ +IncomingArcCounter::IncomingArcCounter(bool skipVars, bool skipConstants) + : d_reachCount() + , d_skipVariables(skipVars) + , d_skipConstants(skipConstants) +{} +IncomingArcCounter::~IncomingArcCounter(){} + +void IncomingArcCounter::computeReachability(const std::vector<Node>& assertions){ + std::vector<TNode> tovisit(assertions.begin(), assertions.end()); + + while(!tovisit.empty()){ + TNode back = tovisit.back(); + tovisit.pop_back(); + + bool skip = false; + switch(back.getMetaKind()){ + case kind::metakind::CONSTANT: + skip = d_skipConstants; + break; + case kind::metakind::VARIABLE: + skip = d_skipVariables; + break; + default: + break; + } + + if(skip) { continue; } + if(d_reachCount.find(back) != d_reachCount.end()){ + d_reachCount[back] = 1 + d_reachCount[back]; + }else{ + d_reachCount[back] = 1; + for(TNode::iterator cit=back.begin(), end = back.end(); cit != end; ++cit){ + tovisit.push_back(*cit); + } + } + } +} + +void IncomingArcCounter::clear() { + d_reachCount.clear(); +} + +/********************* */ +/* ITECompressor + */ +ITECompressor::ITECompressor(ContainsTermITEVistor* contains) + : d_contains(contains) + , d_assertions(NULL) + , d_incoming(true, true) +{ + Assert(d_contains != NULL); + + d_true = NodeManager::currentNM()->mkConst<bool>(true); + d_false = NodeManager::currentNM()->mkConst<bool>(false); +} + +ITECompressor::~ITECompressor() { + reset(); +} + +void ITECompressor::reset(){ + d_incoming.clear(); + d_compressed.clear(); +} + +void ITECompressor::garbageCollect(){ + reset(); +} + +ITECompressor::Statistics::Statistics(): + d_compressCalls("ite-simp::compressCalls", 0), + d_skolemsAdded("ite-simp::skolems", 0) +{ + StatisticsRegistry::registerStat(&d_compressCalls); + StatisticsRegistry::registerStat(&d_skolemsAdded); + +} +ITECompressor::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_compressCalls); + StatisticsRegistry::unregisterStat(&d_skolemsAdded); +} + +Node ITECompressor::push_back_boolean(Node original, Node compressed){ + Node rewritten = Rewriter::rewrite(compressed); + // There is a bug if the rewritter takes a pure boolean expression + // and changes its theory + if(rewritten.isConst()){ + d_compressed[compressed] = rewritten; + d_compressed[original] = rewritten; + d_compressed[rewritten] = rewritten; + return rewritten; + }else if(d_compressed.find(rewritten) != d_compressed.end()){ + Node res = d_compressed[rewritten]; + d_compressed[original] = res; + d_compressed[compressed] = res; + return res; + }else if(rewritten.isVar() || + (rewritten.getKind() == kind::NOT && rewritten[0].isVar())){ + d_compressed[original] = rewritten; + d_compressed[compressed] = rewritten; + d_compressed[rewritten] = rewritten; + return rewritten; + }else{ + NodeManager* nm = NodeManager::currentNM(); + Node skolem = nm->mkSkolem("compress_$$", nm->booleanType()); + d_compressed[rewritten] = skolem; + d_compressed[original] = skolem; + d_compressed[compressed] = skolem; + + Node iff = skolem.iffNode(rewritten); + d_assertions->push_back(iff); + ++(d_statistics.d_skolemsAdded); + return skolem; + } +} + +bool ITECompressor::multipleParents(TNode c){ + return d_incoming.lookupIncoming(c) >= 2; +} + +Node ITECompressor::compressBooleanITEs(Node toCompress){ + Assert(toCompress.getKind() == kind::ITE); + Assert(toCompress.getType().isBoolean()); + + if(!(toCompress[1] == d_false || toCompress[2] == d_false)){ + Node cmpCnd = compressBoolean(toCompress[0]); + if(cmpCnd.isConst()){ + Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2]; + Node res = compressBoolean(branch); + d_compressed[toCompress] = res; + return res; + }else{ + Node cmpThen = compressBoolean(toCompress[1]); + Node cmpElse = compressBoolean(toCompress[2]); + Node newIte = cmpCnd.iteNode(cmpThen, cmpElse); + if(multipleParents(toCompress)){ + return push_back_boolean(toCompress, newIte); + }else{ + return newIte; + } + } + } + + NodeBuilder<> nb(kind::AND); + Node curr = toCompress; + while(curr.getKind() == kind::ITE && + (curr[1] == d_false || curr[2] == d_false) && + (!multipleParents(curr) || curr == toCompress)){ + + bool negateCnd = (curr[1] == d_false); + Node compressCnd = compressBoolean(curr[0]); + if(compressCnd.isConst()){ + if(compressCnd.getConst<bool>() == negateCnd){ + return push_back_boolean(toCompress, d_false); + }else{ + // equivalent to true don't push back + } + }else{ + Node pb = negateCnd ? compressCnd.notNode() : compressCnd; + nb << pb; + } + curr = negateCnd ? curr[2] : curr[1]; + } + Assert(toCompress != curr); + + nb << compressBoolean(curr); + Node res = nb.getNumChildren() == 1 ? nb[0] : (Node)nb; + return push_back_boolean(toCompress, res); +} + +Node ITECompressor::compressTerm(Node toCompress){ + if(toCompress.isConst() || toCompress.isVar()){ + return toCompress; + } + + if(d_compressed.find(toCompress) != d_compressed.end()){ + return d_compressed[toCompress]; + } + if(toCompress.getKind() == kind::ITE){ + Node cmpCnd = compressBoolean(toCompress[0]); + if(cmpCnd.isConst()){ + Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2]; + Node res = compressTerm(toCompress); + d_compressed[toCompress] = res; + return res; + }else{ + Node cmpThen = compressTerm(toCompress[1]); + Node cmpElse = compressTerm(toCompress[2]); + Node newIte = cmpCnd.iteNode(cmpThen, cmpElse); + d_compressed[toCompress] = newIte; + return newIte; + } + } + + NodeBuilder<> nb(toCompress.getKind()); + + if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) { + nb << (toCompress.getOperator()); + } + for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){ + nb << compressTerm(*it); + } + Node compressed = (Node)nb; + if(multipleParents(toCompress)){ + d_compressed[toCompress] = compressed; + } + return compressed; +} + +Node ITECompressor::compressBoolean(Node toCompress){ + static int instance = 0; + ++instance; + if(toCompress.isConst() || toCompress.isVar()){ + return toCompress; + } + if(d_compressed.find(toCompress) != d_compressed.end()){ + return d_compressed[toCompress]; + }else if(toCompress.getKind() == kind::ITE){ + return compressBooleanITEs(toCompress); + }else{ + bool ta = ite::isTheoryAtom(toCompress); + NodeBuilder<> nb(toCompress.getKind()); + if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) { + nb << (toCompress.getOperator()); + } + for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){ + Node pb = (ta) ? compressTerm(*it) : compressBoolean(*it); + nb << pb; + } + Node compressed = nb; + if(ta || multipleParents(toCompress)){ + return push_back_boolean(toCompress, compressed); + }else{ + return compressed; + } + } +} + + + +bool ITECompressor::compress(std::vector<Node>& assertions){ + reset(); + + d_assertions = &assertions; + d_incoming.computeReachability(assertions); + + ++(d_statistics.d_compressCalls); + Chat() << "Computed reachability" << endl; + + bool nofalses = true; + size_t original_size = assertions.size(); + Chat () << "compressing " << original_size << endl; + for(size_t i = 0; i < original_size && nofalses; ++i){ + Node assertion = assertions[i]; + Node compressed = compressBoolean(assertion); + Node rewritten = Rewriter::rewrite(compressed); + assertions[i] = rewritten; + Assert(!d_contains->containsTermITE(rewritten)); + + nofalses = (rewritten != d_false); + } + + d_assertions = NULL; + + return nofalses; +} + +TermITEHeightCounter::TermITEHeightCounter() + :d_termITEHeight() +{} + +TermITEHeightCounter::~TermITEHeightCounter(){} + +void TermITEHeightCounter::clear(){ + d_termITEHeight.clear(); +} + +size_t TermITEHeightCounter::cache_size() const{ + return d_termITEHeight.size(); +} + +namespace ite { +struct TITEHStackElement { + TNode curr; + unsigned pos; + uint32_t maxChildHeight; + TITEHStackElement(){} + TITEHStackElement(TNode c) : curr(c), pos(0), maxChildHeight(0){ } +}; +} /* namespace ite */ + +uint32_t TermITEHeightCounter::termITEHeight(TNode e){ + + if(ite::triviallyContainsNoTermITEs(e)){ return 0; } + + NodeCountMap::const_iterator end = d_termITEHeight.end(); + NodeCountMap::const_iterator tmp_it = d_termITEHeight.find(e); + if(tmp_it != end){ + return (*tmp_it).second; + } + + + uint32_t returnValue = 0; + // This is initially 0 as the very first call this is included in the max, + // but this has no effect. + std::vector<ite::TITEHStackElement> stack; + stack.push_back(ite::TITEHStackElement(e)); + while(!stack.empty()){ + ite::TITEHStackElement& top = stack.back(); + top.maxChildHeight = std::max(top.maxChildHeight, returnValue); + TNode curr = top.curr; + if(top.pos >= curr.getNumChildren()){ + // done with the current node + returnValue = top.maxChildHeight + (ite::isTermITE(curr) ? 1 : 0); + d_termITEHeight[curr] = returnValue; + stack.pop_back(); + continue; + }else{ + if(top.pos == 0 && curr.getKind() == kind::ITE){ + ++top.pos; + returnValue = 0; + continue; + } + // this is someone's child + TNode child = curr[top.pos]; + ++top.pos; + if(ite::triviallyContainsNoTermITEs(child)){ + returnValue = 0; + }else{ + tmp_it = d_termITEHeight.find(child); + if(tmp_it != end){ + returnValue = (*tmp_it).second; + }else{ + stack.push_back(ite::TITEHStackElement(child)); + } + } + } + } + return returnValue; +} + + + +ITESimplifier::ITESimplifier(ContainsTermITEVistor* contains) + : d_containsVisitor(contains) + , d_termITEHeight() + , d_constantLeaves() + , d_allocatedConstantLeaves() + , d_citeEqConstApplications(0) + , d_constantIteEqualsConstantCache() + , d_replaceOverCache() + , d_replaceOverTermIteCache() + , d_leavesConstCache() + , d_simpConstCache() + , d_simpContextCache() + , d_simpITECache() +{ + Assert(d_containsVisitor != NULL); + d_true = NodeManager::currentNM()->mkConst<bool>(true); + d_false = NodeManager::currentNM()->mkConst<bool>(false); +} + +ITESimplifier::~ITESimplifier() { + clearSimpITECaches(); + Assert(d_constantLeaves.empty()); + Assert(d_allocatedConstantLeaves.empty()); +} + +bool ITESimplifier::leavesAreConst(TNode e){ + return leavesAreConst(e, theory::Theory::theoryOf(e)); +} + +void ITESimplifier::clearSimpITECaches(){ + Chat() << "clear ite caches " << endl; + for(size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i){ + NodeVec* curr = d_allocatedConstantLeaves[i]; + delete curr; + } + d_citeEqConstApplications = 0; + d_constantLeaves.clear(); + d_allocatedConstantLeaves.clear(); + d_termITEHeight.clear(); + d_constantIteEqualsConstantCache.clear(); + d_replaceOverCache.clear(); + d_replaceOverTermIteCache.clear(); + d_simpITECache.clear(); + d_simpVars.clear(); + d_simpConstCache.clear(); + d_leavesConstCache.clear(); + d_simpContextCache.clear(); +} + +bool ITESimplifier::doneALotOfWorkHeuristic() const { + static const size_t SIZE_BOUND = 1000; + Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications << endl; + return (d_citeEqConstApplications > SIZE_BOUND); +} + +ITESimplifier::Statistics::Statistics(): + d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0), + d_unexpected("ite-simp::unexpected", 0), + d_unsimplified("ite-simp::unsimplified", 0), + d_exactMatchFold("ite-simp::exactMatchFold", 0), + d_binaryPredFold("ite-simp::binaryPredFold", 0), + d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0), + d_simpITEVisits("ite-simp::simpITE.visits", 0), + d_inSmaller("ite-simp::inSmaller") +{ + StatisticsRegistry::registerStat(&d_maxNonConstantsFolded); + StatisticsRegistry::registerStat(&d_unexpected); + StatisticsRegistry::registerStat(&d_unsimplified); + StatisticsRegistry::registerStat(&d_exactMatchFold); + StatisticsRegistry::registerStat(&d_binaryPredFold); + StatisticsRegistry::registerStat(&d_specialEqualityFolds); + StatisticsRegistry::registerStat(&d_simpITEVisits); + StatisticsRegistry::registerStat(&d_inSmaller); +} + +ITESimplifier::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_maxNonConstantsFolded); + StatisticsRegistry::unregisterStat(&d_unexpected); + StatisticsRegistry::unregisterStat(&d_unsimplified); + StatisticsRegistry::unregisterStat(&d_exactMatchFold); + StatisticsRegistry::unregisterStat(&d_binaryPredFold); + StatisticsRegistry::unregisterStat(&d_specialEqualityFolds); + StatisticsRegistry::unregisterStat(&d_simpITEVisits); + StatisticsRegistry::unregisterStat(&d_inSmaller); +} + +bool ITESimplifier::isConstantIte(TNode e){ + if(e.isConst()){ + return true; + }else if(ite::isTermITE(e)){ + NodeVec* constants = computeConstantLeaves(e); + return constants != NULL; + }else{ + return false; + } +} + +ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){ + Assert(ite::isTermITE(ite)); + ConstantLeavesMap::const_iterator it = d_constantLeaves.find(ite); + ConstantLeavesMap::const_iterator end = d_constantLeaves.end(); + if(it != end){ + return (*it).second; + } + TNode thenB = ite[1]; + TNode elseB = ite[2]; + + // special case 2 constant children + if(thenB.isConst() && elseB.isConst()){ + NodeVec* pair = new NodeVec(2); + (*pair)[0] = std::min(thenB, elseB); + (*pair)[1] = std::max(thenB, elseB); + d_constantLeaves[ite] = pair; + return pair; + } + // At least 1 is an ITE + if(!(thenB.isConst() || thenB.getKind() == kind::ITE) || + !(elseB.isConst() || elseB.getKind() == kind::ITE)){ + // Cannot be a termITE tree + d_constantLeaves[ite] = NULL; + return NULL; + } + + // At least 1 is not a constant + TNode definitelyITE = thenB.isConst() ? elseB : thenB; + TNode maybeITE = thenB.isConst() ? thenB : elseB; + + NodeVec* defChildren = computeConstantLeaves(definitelyITE); + if(defChildren == NULL){ + d_constantLeaves[ite] = NULL; + return NULL; + } + + NodeVec scratch; + NodeVec* maybeChildren = NULL; + if(maybeITE.getKind() == kind::ITE){ + maybeChildren = computeConstantLeaves(maybeITE); + }else{ + scratch.push_back(maybeITE); + maybeChildren = &scratch; + } + if(maybeChildren == NULL){ + d_constantLeaves[ite] = NULL; + return NULL; + } + + NodeVec* both = new NodeVec(defChildren->size()+maybeChildren->size()); + NodeVec::iterator newEnd; + newEnd = std::set_union(defChildren->begin(), defChildren->end(), + maybeChildren->begin(), maybeChildren->end(), + both->begin()); + both->resize(newEnd - both->begin()); + d_constantLeaves[ite] = both; + return both; +} + +// This is uncached! Better for protoyping or getting limited size examples +struct IteTreeSearchData{ + set<Node> visited; + set<Node> constants; + set<Node> nonConstants; + int maxConstants; + int maxNonconstants; + int maxDepth; + bool failure; + IteTreeSearchData() + : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false) + {} +}; +void iteTreeSearch(Node e, int depth, IteTreeSearchData& search){ + if(search.maxDepth >= 0 && depth > search.maxDepth){ + search.failure = true; + } + if(search.failure){ + return; + } + if(search.visited.find(e) != search.visited.end()){ + return; + }else{ + search.visited.insert(e); + } + + if(e.isConst()){ + search.constants.insert(e); + if(search.maxConstants >= 0 && + search.constants.size() > (unsigned)search.maxConstants){ + search.failure = true; + } + }else if(e.getKind() == kind::ITE){ + iteTreeSearch(e[1], depth+1, search); + iteTreeSearch(e[2], depth+1, search); + }else{ + search.nonConstants.insert(e); + if(search.maxNonconstants >= 0 && + search.nonConstants.size() > (unsigned)search.maxNonconstants){ + search.failure = true; + } + } +} + +Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar){ + if(n == simpVar){ + return replaceWith; + }else if(n.getNumChildren() == 0){ + return n; + } + Assert(n.getNumChildren() > 0); + Assert(!n.isVar()); + + pair<Node, Node> p = make_pair(n, replaceWith); + if(d_replaceOverCache.find(p) != d_replaceOverCache.end()){ + return d_replaceOverCache[p]; + } + + NodeBuilder<> builder(n.getKind()); + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << n.getOperator(); + } + unsigned i = 0; + for (; i < n.getNumChildren(); ++ i) { + Node newChild = replaceOver(n[i], replaceWith, simpVar); + builder << newChild; + } + // Mark the substitution and continue + Node result = builder; + d_replaceOverCache[p] = result; + return result; +} + +Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar){ + if(e.getKind() == kind::ITE){ + pair<Node, Node> p = make_pair(e, simpAtom); + if(d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end()){ + return d_replaceOverTermIteCache[p]; + } + Assert(!e.getType().isBoolean()); + Node cnd = e[0]; + Node newThen = replaceOverTermIte(e[1], simpAtom, simpVar); + Node newElse = replaceOverTermIte(e[2], simpAtom, simpVar); + Node newIte = cnd.iteNode(newThen, newElse); + d_replaceOverTermIteCache[p] = newIte; + return newIte; + }else{ + return replaceOver(simpAtom, e, simpVar); + } +} + +Node ITESimplifier::attemptLiftEquality(TNode atom){ + if(atom.getKind() == kind::EQUAL){ + TNode left = atom[0]; + TNode right = atom[1]; + if((left.getKind() == kind::ITE || right.getKind() == kind::ITE)&& + !(left.getKind() == kind::ITE && right.getKind() == kind::ITE)){ + + // exactly 1 is an ite + TNode ite = left.getKind() == kind::ITE ? left :right; + TNode notIte = left.getKind() == kind::ITE ? right : left; + + if(notIte == ite[1]){ + ++(d_statistics.d_exactMatchFold); + return ite[0].iteNode(d_true, notIte.eqNode(ite[2])); + }else if(notIte == ite[2]){ + ++(d_statistics.d_exactMatchFold); + return ite[0].iteNode(notIte.eqNode(ite[1]), d_true); + } + if(notIte.isConst() && + (ite[1].isConst() || ite[2].isConst())){ + ++(d_statistics.d_exactMatchFold); + return ite[0].iteNode(notIte.eqNode(ite[1]), notIte.eqNode(ite[2])); + } + } + } + + // try a similar more relaxed version for non-equality operators + if(atom.getMetaKind() == kind::metakind::OPERATOR && + atom.getNumChildren() == 2 && + !atom[1].getType().isBoolean()){ + + TNode left = atom[0]; + TNode right = atom[1]; + if( (left.getKind() == kind::ITE || right.getKind() == kind::ITE)&& + !(left.getKind() == kind::ITE && right.getKind() == kind::ITE)){ + // exactly 1 is an ite + bool leftIsIte = left.getKind() == kind::ITE; + Node ite = leftIsIte ? left :right; + Node notIte = leftIsIte ? right : left; + + if(notIte.isConst()){ + IteTreeSearchData search; + search.maxNonconstants = 2; + iteTreeSearch(ite, 0, search); + if(!search.failure){ + d_statistics.d_maxNonConstantsFolded.maxAssign(search.nonConstants.size()); + Debug("ite::simpite") << "used " << search.nonConstants.size() << " nonconstants" << endl; + NodeManager* nm = NodeManager::currentNM(); + Node simpVar = getSimpVar(notIte.getType()); + TNode newLeft = leftIsIte ? simpVar : notIte; + TNode newRight = leftIsIte ? notIte : simpVar; + Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight); + + ++(d_statistics.d_binaryPredFold); + return replaceOverTermIte(ite, newAtom, simpVar); + } + } + } + } + + // TODO "This is way too tailored. Must generalize!" + if(atom.getKind() == kind::EQUAL && + atom.getNumChildren() == 2 && + ite::isTermITE(atom[0]) && + atom[1].getKind() == kind::MULT && + atom[1].getNumChildren() == 2 && + atom[1][0].isConst() && + atom[1][0].getConst<Rational>().isNegativeOne() && + ite::isTermITE(atom[1][1]) && + d_termITEHeight.termITEHeight(atom[0]) == 1 && + d_termITEHeight.termITEHeight(atom[1][1]) == 1 && + (atom[0][1].isConst() || atom[0][2].isConst()) && + (atom[1][1][1].isConst() || atom[1][1][2].isConst()) ){ + // expand all 4 cases + + Node negOne = atom[1][0]; + + Node lite = atom[0]; + Node lC = lite[0]; + Node lT = lite[1]; + Node lE = lite[2]; + + NodeManager* nm = NodeManager::currentNM(); + Node negRite = atom[1][1]; + Node rC = negRite[0]; + Node rT = nm->mkNode(kind::MULT, negOne, negRite[1]); + Node rE = nm->mkNode(kind::MULT, negOne, negRite[2]); + + // (ite lC lT lE) = (ite rC rT rE) + // (ite lc (= lT (ite rC rT rE) (= lE (ite rC rT rE)))) + // (ite lc (ite rC (= lT rT) (= lT rE)) + // (ite rC (= lE rT) (= lE rE))) + + Node eqTT = lT.eqNode(rT); + Node eqTE = lT.eqNode(rE); + Node eqET = lE.eqNode(rT); + Node eqEE = lE.eqNode(rE); + Node thenLC = rC.iteNode(eqTT, eqTE); + Node elseLC = rC.iteNode(eqET, eqEE); + Node newIte = lC.iteNode(thenLC, elseLC); + + ++(d_statistics.d_specialEqualityFolds); + return newIte; + } + return Node::null(); +} + +// Interesting classes of atoms: +// 2. Contains constants and 1 constant term ite +// 3. Contains 2 constant term ites +Node ITESimplifier::transformAtom(TNode atom){ + if(! d_containsVisitor->containsTermITE(atom)){ + if(atom.getKind() == kind::EQUAL && + atom[0].isConst() && atom[1].isConst()){ + // constant equality + return NodeManager::currentNM()->mkConst<bool>(atom[0] == atom[1]); + } + return Node::null(); + }else{ + Node acr = attemptConstantRemoval(atom); + if(!acr.isNull()){ + return acr; + } + // Node ale = attemptLiftEquality(atom); + // if(!ale.isNull()){ + // //return ale; + // } + return Node::null(); + } +} + +static unsigned numBranches = 0; +static unsigned numFalseBranches = 0; +static unsigned itesMade = 0; + +Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){ + static int instance = 0; + ++instance; + Debug("ite::constantIteEqualsConstant") << instance << "constantIteEqualsConstant("<<cite << ", " << constant<<")"<< endl; + if(cite.isConst()){ + Node res = (cite == constant) ? d_true : d_false; + Debug("ite::constantIteEqualsConstant") << instance << "->" << res << endl; + return res; + } + std::pair<Node,Node> pair = make_pair(cite, constant); + + NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair); + if(eq_pos != d_constantIteEqualsConstantCache.end()){ + Debug("ite::constantIteEqualsConstant") << instance << "->" << (*eq_pos).second << endl; + return (*eq_pos).second; + } + + ++d_citeEqConstApplications; + + NodeVec* leaves = computeConstantLeaves(cite); + Assert(leaves != NULL); + if(std::binary_search(leaves->begin(), leaves->end(), constant)){ + if(leaves->size() == 1){ + // probably unreachable + d_constantIteEqualsConstantCache[pair] = d_true; + Debug("ite::constantIteEqualsConstant") << instance << "->" << d_true << endl; + return d_true; + }else{ + Assert(cite.getKind() == kind::ITE); + TNode cnd = cite[0]; + TNode tB = cite[1]; + TNode fB = cite[2]; + Node tEqs = constantIteEqualsConstant(tB, constant); + Node fEqs = constantIteEqualsConstant(fB, constant); + Node boolIte = cnd.iteNode(tEqs, fEqs); + if(!(tEqs.isConst() || fEqs.isConst())){ + ++numBranches; + } + if(!(tEqs == d_false || fEqs == d_false)){ + ++numFalseBranches; + } + ++itesMade; + d_constantIteEqualsConstantCache[pair] = boolIte; + //Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte << endl; + return boolIte; + } + }else{ + d_constantIteEqualsConstantCache[pair] = d_false; + Debug("ite::constantIteEqualsConstant") << instance << "->" << d_false << endl; + return d_false; + } +} + + +Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){ + // intersect the constant ite trees lcite and rcite + + if(lcite.isConst() || rcite.isConst()){ + bool lIsConst = lcite.isConst(); + TNode constant = lIsConst ? lcite : rcite; + TNode cite = lIsConst ? rcite : lcite; + + (d_statistics.d_inSmaller)<< 1; + unsigned preItesMade = itesMade; + unsigned preNumBranches = numBranches; + unsigned preNumFalseBranches = numFalseBranches; + Node bterm = constantIteEqualsConstant(cite, constant); + Debug("intersectConstantIte") + << (numBranches - preNumBranches) + << " " << (numFalseBranches - preNumFalseBranches) + << " " << (itesMade - preItesMade) << endl; + return bterm; + } + Assert(lcite.getKind() == kind::ITE); + Assert(rcite.getKind() == kind::ITE); + + NodeVec* leftValues = computeConstantLeaves(lcite); + NodeVec* rightValues = computeConstantLeaves(rcite); + + uint32_t smaller = std::min(leftValues->size(), rightValues->size()); + + (d_statistics.d_inSmaller)<< smaller; + NodeVec intersection(smaller, Node::null()); + NodeVec::iterator newEnd; + newEnd = std::set_intersection(leftValues->begin(), leftValues->end(), + rightValues->begin(), rightValues->end(), + intersection.begin()); + intersection.resize(newEnd - intersection.begin()); + if(intersection.empty()){ + return d_false; + }else{ + NodeBuilder<> nb(kind::OR); + NodeVec::const_iterator it = intersection.begin(), end=intersection.end(); + for(; it != end; ++it){ + Node inBoth = *it; + Node lefteq = constantIteEqualsConstant(lcite, inBoth); + Node righteq = constantIteEqualsConstant(rcite, inBoth); + Node bothHold = lefteq.andNode(righteq); + nb << bothHold; + } + Node result = (nb.getNumChildren() >= 1) ? (Node)nb : nb[0]; + return result; + } +} + + +Node ITESimplifier::attemptEagerRemoval(TNode atom){ + if(atom.getKind() == kind::EQUAL){ + TNode left = atom[0]; + TNode right = atom[1]; + if((left.isConst() && + right.getKind() == kind::ITE && isConstantIte(right)) || + (right.isConst() && + left.getKind() == kind::ITE && isConstantIte(left))){ + TNode constant = left.isConst() ? left : right; + TNode cite = left.isConst() ? right : left; + + std::pair<Node,Node> pair = make_pair(cite, constant); + NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair); + if(eq_pos != d_constantIteEqualsConstantCache.end()){ + Node ret = (*eq_pos).second; + if(ret.isConst()){ + return ret; + }else{ + return Node::null(); + } + } + + NodeVec* leaves = computeConstantLeaves(cite); + Assert(leaves != NULL); + if(!std::binary_search(leaves->begin(), leaves->end(), constant)){ + std::pair<Node,Node> pair = make_pair(cite, constant); + d_constantIteEqualsConstantCache[pair] = d_false; + return d_false; + } + } + } + return Node::null(); +} + +Node ITESimplifier::attemptConstantRemoval(TNode atom){ + if(atom.getKind() == kind::EQUAL){ + TNode left = atom[0]; + TNode right = atom[1]; + if(isConstantIte(left) && isConstantIte(right)){ + return intersectConstantIte(left, right); + } + } + return Node::null(); +} + + +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; +} +typedef std::hash_set<Node, NodeHashFunction> NodeSet; +void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){ + if(visited.find(x) != visited.end()){ + return; + } + visited.insert(x); + if(x.getKind() == k){ + ++reached; + } + for(unsigned i =0, N=x.getNumChildren(); i < N; ++i){ + countReachable_(x[i], k, visited, reached); + } +} + +uint32_t countReachable(TNode x, Kind k){ + NodeSet visited; + uint32_t reached = 0; + countReachable_(x, k, visited, reached); + return reached; +} + +Node ITESimplifier::simpITEAtom(TNode atom) +{ + static int CVC4_UNUSED instance = 0; + Debug("ite::atom") << "still simplifying " << (++instance) << endl; + Node attempt = transformAtom(atom); + Debug("ite::atom") << " finished " << instance << endl; + if(!attempt.isNull()){ + Node rewritten = Rewriter::rewrite(attempt); + Debug("ite::print-success") + << instance << " " + << "rewriting " << countReachable(rewritten, kind::ITE) + << " from " << countReachable(atom, kind::ITE) << endl + << "\t rewritten " << rewritten << endl + << "\t input " << atom << endl; + return rewritten; + } + + 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)); + ++(d_statistics.d_unexpected); + Debug("ite::simpite") << instance << " " + << "how about?" << atom << endl; + Debug("ite::simpite") << instance << " " + << "\t" << simpContext << endl; + return Rewriter::rewrite(simpContext); + } + Node n = simpConstants(simpContext, iteNode, simpVar); + if (!n.isNull()) { + ++(d_statistics.d_unexpected); + Debug("ite::simpite") << instance << " " + << "here?" << atom << endl; + Debug("ite::simpite") << instance << " " + << "\t" << n << endl; + return n; + } + } + } + if(Debug.isOn("ite::simpite")){ + if(countReachable(atom, kind::ITE) > 0){ + Debug("ite::simpite") << instance << " " + << "remaining " << atom << endl; + } + } + ++(d_statistics.d_unsimplified); + 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); + + static int call = 0; + ++call; + int iteration = 0; + + while (!toVisit.empty()) + { + iteration ++; + //cout << "call " << call << " : " << iteration << endl; + // 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; + ++(d_statistics.d_simpITEVisits); + 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()); + Node child = current[i]; + Node childRes = d_simpITECache[current[i]]; + builder << childRes; + } + // 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); + } + + // if(current != result && result.isConst()){ + // static int instance = 0; + // //cout << instance << " " << result << current << endl; + // } + + result = Rewriter::rewrite(result); + d_simpITECache[current] = result; + ++(d_statistics.d_simpITEVisits); + 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; + ++(d_statistics.d_simpITEVisits); + toVisit.pop_back(); + } + } + } + return d_simpITECache[assertion]; +} + +ITECareSimplifier::ITECareSimplifier() + : d_usedSets() +{ + d_true = NodeManager::currentNM()->mkConst<bool>(true); + d_false = NodeManager::currentNM()->mkConst<bool>(false); +} + +ITECareSimplifier::~ITECareSimplifier(){} + +void ITECareSimplifier::clear(){ + d_usedSets.clear(); +} + +ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet() +{ + if (d_usedSets.empty()) { + return ITECareSimplifier::CareSetPtr::mkNew(*this); + } + else { + ITECareSimplifier::CareSetPtr cs = ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back()); + cs.getCareSet().clear(); + d_usedSets.pop_back(); + return cs; + } +} + + +void ITECareSimplifier::updateQueue(CareMap& queue, + TNode e, + ITECareSimplifier::CareSetPtr& careSet) +{ + CareMap::iterator it = queue.find(e), iend = queue.end(); + if (it != iend) { + set<Node>& cs2 = (*it).second.getCareSet(); + ITECareSimplifier::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 ITECareSimplifier::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 ITECareSimplifier::simplifyWithCare(TNode e) +{ + TNodeMap substTable; + CareMap queue; + CareMap::iterator it; + ITECareSimplifier::CareSetPtr cs = getNewSet(); + ITECareSimplifier::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); +} + + +} /* namespace theory */ +} /* namespace CVC4 */ diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h new file mode 100644 index 000000000..73f0386d2 --- /dev/null +++ b/src/theory/ite_utilities.h @@ -0,0 +1,373 @@ +/********************* */ +/*! \file ite_simplifier.h + ** \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 "cvc4_private.h" + +#ifndef __CVC4__ITE_UTILITIES_H +#define __CVC4__ITE_UTILITIES_H + +#include <vector> +#include <ext/hash_map> +#include <ext/hash_set> +#include "expr/node.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { + +class ContainsTermITEVistor; +class IncomingArcCounter; +class TermITEHeightCounter; +class ITECompressor; +class ITESimplifier; +class ITECareSimplifier; + +class ITEUtilities { +public: + ITEUtilities(ContainsTermITEVistor* containsVisitor); + ~ITEUtilities(); + + Node simpITE(TNode assertion); + + bool simpIteDidALotOfWorkHeuristic() const; + + /* returns false if an assertion is discovered to be equal to false. */ + bool compress(std::vector<Node>& assertions); + + Node simplifyWithCare(TNode e); + + void clear(); + +private: + ContainsTermITEVistor* d_containsVisitor; + ITECompressor* d_compressor; + ITESimplifier* d_simplifier; + ITECareSimplifier* d_careSimp; +}; + +/** + * A caching visitor that computes whether a node contains a term ite. + */ +class ContainsTermITEVistor { +public: + ContainsTermITEVistor(); + ~ContainsTermITEVistor(); + + /** returns true if a node contains a term ite. */ + bool containsTermITE(TNode n); + + /** Garbage collects the cache. */ + void garbageCollect(); + + /** returns the size of the cache. */ + size_t cache_size() const { return d_cache.size(); } + +private: + typedef std::hash_map<Node, bool, NodeHashFunction> NodeBoolMap; + NodeBoolMap d_cache; +}; + +class IncomingArcCounter { +public: + IncomingArcCounter(bool skipVars = false, bool skipConstants = false); + ~IncomingArcCounter(); + void computeReachability(const std::vector<Node>& assertions); + + inline uint32_t lookupIncoming(Node n) const { + NodeCountMap::const_iterator it = d_reachCount.find(n); + if(it == d_reachCount.end()){ + return 0; + }else{ + return (*it).second; + } + } + void clear(); +private: + typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + NodeCountMap d_reachCount; + + bool d_skipVariables; + bool d_skipConstants; +}; + +class TermITEHeightCounter { +public: + TermITEHeightCounter(); + ~TermITEHeightCounter(); + + /** + * Compute and [potentially] cache the termITEHeight() of e. + * The term ite height equals the maximum number of term ites + * encountered on any path from e to a leaf. + * Inductively: + * - termITEHeight(leaves) = 0 + * - termITEHeight(e: term-ite(c, t, e) ) = + * 1 + max(termITEHeight(t), termITEHeight(e)) ; Don't include c + * - termITEHeight(e not term ite) = max_{c in children(e)) (termITEHeight(c)) + */ + uint32_t termITEHeight(TNode e); + + /** Clear the cache. */ + void clear(); + + /** Size of the cache. */ + size_t cache_size() const; + +private: + typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + NodeCountMap d_termITEHeight; +}; + +/** + * A routine designed to undo the potentially large blow up + * due to expansion caused by the ite simplifier. + */ +class ITECompressor { +public: + ITECompressor(ContainsTermITEVistor* contains); + ~ITECompressor(); + + /* returns false if an assertion is discovered to be equal to false. */ + bool compress(std::vector<Node>& assertions); + + /* garbage Collects the compressor. */ + void garbageCollect(); + +private: + + Node d_true; /* Copy of true. */ + Node d_false; /* Copy of false. */ + ContainsTermITEVistor* d_contains; + std::vector<Node>* d_assertions; + IncomingArcCounter d_incoming; + + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_compressed; + + void reset(); + + Node push_back_boolean(Node original, Node compressed); + bool multipleParents(TNode c); + Node compressBooleanITEs(Node toCompress); + Node compressTerm(Node toCompress); + Node compressBoolean(Node toCompress); + + class Statistics { + public: + IntStat d_compressCalls; + IntStat d_skolemsAdded; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; +}; + +class ITESimplifier { +public: + ITESimplifier(ContainsTermITEVistor* d_containsVisitor); + ~ITESimplifier(); + + Node simpITE(TNode assertion); + + bool doneALotOfWorkHeuristic() const; + void clearSimpITECaches(); + +private: + Node d_true; + Node d_false; + + ContainsTermITEVistor* d_containsVisitor; + inline bool containsTermITE(TNode n) { + return d_containsVisitor->containsTermITE(n); + } + TermITEHeightCounter d_termITEHeight; + inline uint32_t termITEHeight(TNode e) { + return d_termITEHeight.termITEHeight(e); + } + + // ConstantIte is a small inductive sublanguage: + // constant + // or termITE(cnd, ConstantIte, ConstantIte) + typedef std::vector<Node> NodeVec; + typedef std::hash_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap; + ConstantLeavesMap d_constantLeaves; + + // d_constantLeaves satisfies the following invariants: + // not containsTermITE(x) then !isKey(x) + // containsTermITE(x): + // - not isKey(x) then this value is uncomputed + // - d_constantLeaves[x] == NULL, then this contains a non-constant leaf + // - d_constantLeaves[x] != NULL, then this contains a sorted list of constant leaf + bool isConstantIte(TNode e); + + /** If its not a constant and containsTermITE(ite), + * returns a sorted NodeVec of the leaves. */ + NodeVec* computeConstantLeaves(TNode ite); + + // Lists all of the vectors in d_constantLeaves for fast deletion. + std::vector<NodeVec*> d_allocatedConstantLeaves; + + + /* transforms */ + Node transformAtom(TNode atom); + Node attemptConstantRemoval(TNode atom); + Node attemptLiftEquality(TNode atom); + Node attemptEagerRemoval(TNode atom); + + // Given ConstantIte trees lcite and rcite, + // return a boolean expression equivalent to (= lcite rcite) + Node intersectConstantIte(TNode lcite, TNode rcite); + + // Given ConstantIte tree cite and a constant c, + // return a boolean expression equivalent to (= lcite c) + Node constantIteEqualsConstant(TNode cite, TNode c); + uint32_t d_citeEqConstApplications; + + typedef std::pair<Node, Node> NodePair; + struct NodePairHashFunction { + size_t operator () (const NodePair& pair) const { + size_t hash = 0; + hash = 0x9e3779b9 + NodeHashFunction().operator()(pair.first); + hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2); + return hash; + } + };/* struct ITESimplifier::NodePairHashFunction */ + typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap; + NodePairMap d_constantIteEqualsConstantCache; + NodePairMap d_replaceOverCache; + NodePairMap d_replaceOverTermIteCache; + Node replaceOver(Node n, Node replaceWith, Node simpVar); + Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar); + + std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache; + bool leavesAreConst(TNode e, theory::TheoryId tid); + bool leavesAreConst(TNode e); + + NodePairMap d_simpConstCache; + Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar); + std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; + Node getSimpVar(TypeNode t); + + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_simpContextCache; + Node createSimpContext(TNode c, Node& iteNode, Node& simpVar); + + NodeMap d_simpITECache; + Node simpITEAtom(TNode atom); + + +private: + class Statistics { + public: + IntStat d_maxNonConstantsFolded; + IntStat d_unexpected; + IntStat d_unsimplified; + IntStat d_exactMatchFold; + IntStat d_binaryPredFold; + IntStat d_specialEqualityFolds; + IntStat d_simpITEVisits; + + HistogramStat<uint32_t> d_inSmaller; + + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; +}; + +class ITECareSimplifier { +public: + ITECareSimplifier(); + ~ITECareSimplifier(); + + Node simplifyWithCare(TNode e); + + void clear(); +private: + Node d_true; + Node d_false; + + typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; + + class CareSetPtr; + class CareSetPtrVal { + friend class ITECareSimplifier::CareSetPtr; + ITECareSimplifier& d_iteSimplifier; + unsigned d_refCount; + std::set<Node> d_careSet; + CareSetPtrVal(ITECareSimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {} + }; + + std::vector<CareSetPtrVal*> d_usedSets; + void careSetPtrGC(CareSetPtrVal* val) { + d_usedSets.push_back(val); + } + + class CareSetPtr { + CareSetPtrVal* d_val; + CareSetPtr(CareSetPtrVal* val) : d_val(val) {} + public: + CareSetPtr() : d_val(NULL) {} + CareSetPtr(const CareSetPtr& cs) { + d_val = cs.d_val; + if (d_val != NULL) { + ++(d_val->d_refCount); + } + } + ~CareSetPtr() { + if (d_val != NULL && (--(d_val->d_refCount) == 0)) { + d_val->d_iteSimplifier.careSetPtrGC(d_val); + } + } + CareSetPtr& operator=(const CareSetPtr& cs) { + if (d_val != cs.d_val) { + if (d_val != NULL && (--(d_val->d_refCount) == 0)) { + d_val->d_iteSimplifier.careSetPtrGC(d_val); + } + d_val = cs.d_val; + if (d_val != NULL) { + ++(d_val->d_refCount); + } + } + return *this; + } + std::set<Node>& getCareSet() { return d_val->d_careSet; } + static CareSetPtr mkNew(ITECareSimplifier& simp) { + CareSetPtrVal* val = new CareSetPtrVal(simp); + return CareSetPtr(val); + } + static CareSetPtr recycle(CareSetPtrVal* val) { + Assert(val != NULL && val->d_refCount == 0); + val->d_refCount = 1; + return CareSetPtr(val); + } + }; + + CareSetPtr getNewSet(); + + typedef std::map<TNode, CareSetPtr> CareMap; + void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet); + Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache); +}; + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif diff --git a/src/theory/model.h b/src/theory/model.h index a18d66ab0..8192274b5 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -22,7 +22,6 @@ #include "theory/rep_set.h" #include "theory/substitutions.h" #include "theory/type_enumerator.h" -#include "theory/ite_simplifier.h" namespace CVC4 { @@ -38,7 +37,6 @@ class TheoryModel : public Model protected: /** substitution map for this model */ SubstitutionMap d_substitutions; - ITESimplifier d_iteSimp; public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel(){} diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 84bbbc179..93b3f0d7e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -35,6 +35,11 @@ #include "util/node_visitor.h" #include "util/ite_removal.h" +//#include "theory/ite_simplifier.h" +//#include "theory/ite_compressor.h" +#include "theory/ite_utilities.h" +#include "theory/unconstrained_simplifier.h" + #include "theory/model.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/theory_quantifiers.h" @@ -122,7 +127,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), - d_unconstrainedSimp(context, logicInfo), + d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)), d_bvToBoolPreprocessor() { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { @@ -140,7 +145,9 @@ TheoryEngine::TheoryEngine(context::Context* context, StatisticsRegistry::registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); - PROOF (ProofManager::currentPM()->initTheoryProof(); ); + PROOF (ProofManager::currentPM()->initTheoryProof(); ); + + d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); } TheoryEngine::~TheoryEngine() { @@ -161,6 +168,10 @@ TheoryEngine::~TheoryEngine() { delete d_masterEqualityEngine; StatisticsRegistry::unregisterStat(&d_combineTheoriesTime); + + delete d_unconstrainedSimp; + + delete d_iteUtilities; } void TheoryEngine::interrupt() throw(ModalException) { @@ -1401,9 +1412,48 @@ void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<N Node TheoryEngine::ppSimpITE(TNode assertion) { - Node result = d_iteSimplifier.simpITE(assertion); - result = d_iteSimplifier.simplifyWithCare(Rewriter::rewrite(result)); - result = Rewriter::rewrite(result); + if(!d_iteRemover.containsTermITE(assertion)){ + return assertion; + }else{ + + Node result = d_iteUtilities->simpITE(assertion); + Node res_rewritten = Rewriter::rewrite(result); + + if(options::simplifyWithCareEnabled()){ + Chat() << "starting simplifyWithCare()" << endl; + Node postSimpWithCare = d_iteUtilities->simplifyWithCare(res_rewritten); + Chat() << "ending simplifyWithCare()" + << " post simplifyWithCare()" << postSimpWithCare.getId() << endl; + result = Rewriter::rewrite(postSimpWithCare); + }else{ + result = res_rewritten; + } + + return result; + } +} + +bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){ + bool result = true; + if(d_iteUtilities->simpIteDidALotOfWorkHeuristic()){ + if(options::compressItes()){ + result = d_iteUtilities->compress(assertions); + } + + if(result){ + // if false, don't bother to reclaim memory here. + NodeManager* nm = NodeManager::currentNM(); + if(nm->poolSize() >= options::zombieHuntThreshold()){ + Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl; + Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl; + d_iteUtilities->clear(); + Rewriter::garbageCollect(); + d_iteRemover.garbageCollect(); + nm->reclaimZombiesUntil(options::zombieHuntThreshold()); + Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl; + } + } + } return result; } @@ -1481,7 +1531,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) { - d_unconstrainedSimp.processAssertions(assertions); + d_unconstrainedSimp->processAssertions(assertions); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 53ff4d167..e5b2ad8d2 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -37,12 +37,8 @@ #include "options/options.h" #include "smt/options.h" #include "util/statistics_registry.h" -#include "util/hash.h" -#include "util/cache.h" #include "util/cvc4_assert.h" #include "util/sort_inference.h" -#include "theory/ite_simplifier.h" -#include "theory/unconstrained_simplifier.h" #include "theory/uf/equality_engine.h" #include "theory/bv/bv_to_bool.h" #include "theory/atom_requests.h" @@ -77,18 +73,19 @@ struct NodeTheoryPairHashFunction { - +/* Forward Declarations Block */ namespace theory { class TheoryModel; class TheoryEngineModelBuilder; + class ITEUtilities; namespace eq { class EqualityEngine; } }/* CVC4::theory namespace */ - - class DecisionEngine; +class RemoveITE; +class UnconstrainedSimplifier; /** * This is essentially an abstraction for a collection of theories. A @@ -771,11 +768,14 @@ private: /** Dump the assertions to the dump */ void dumpAssertions(const char* tag); - /** For preprocessing pass simplifying ITEs */ - theory::ITESimplifier d_iteSimplifier; + /** + * A collection of ite preprocessing passes. + */ + theory::ITEUtilities* d_iteUtilities; + /** For preprocessing pass simplifying unconstrained expressions */ - UnconstrainedSimplifier d_unconstrainedSimp; + UnconstrainedSimplifier* d_unconstrainedSimp; /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; @@ -783,6 +783,9 @@ public: void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); Node ppSimpITE(TNode assertion); + /** Returns false if an assertion simplified to false. */ + bool donePPSimpITE(std::vector<Node>& assertions); + void ppUnconstrainedSimp(std::vector<Node>& assertions); SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 9b172a561..8bbdded3e 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -18,6 +18,7 @@ #include "theory/unconstrained_simplifier.h" #include "theory/rewriter.h" +#include "theory/logic_info.h" using namespace std; using namespace CVC4; diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h index 7d8e85036..0ee754256 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/theory/unconstrained_simplifier.h @@ -24,11 +24,14 @@ #include <utility> #include "expr/node.h" -#include "theory/theory.h" #include "theory/substitutions.h" +#include "util/statistics_registry.h" namespace CVC4 { +/* Forward Declarations */ +class LogicInfo; + class UnconstrainedSimplifier { /** number of expressions eliminated due to unconstrained simplification */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 156288600..5647a2057 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -76,6 +76,8 @@ libutil_la_SOURCES = \ boolean_simplification.cpp \ ite_removal.h \ ite_removal.cpp \ + nary_builder.h \ + nary_builder.cpp \ node_visitor.h \ chain.h \ index.h \ diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index 7d4948251..5231e05c2 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -17,15 +17,37 @@ #include <vector> #include "util/ite_removal.h" -#include "theory/rewriter.h" #include "expr/command.h" #include "theory/quantifiers/options.h" +#include "theory/ite_utilities.h" using namespace CVC4; using namespace std; namespace CVC4 { +RemoveITE::RemoveITE(context::UserContext* u) + : d_iteCache(u) +{ + d_containsVisitor = new theory::ContainsTermITEVistor(); +} + +RemoveITE::~RemoveITE(){ + delete d_containsVisitor; +} + +void RemoveITE::garbageCollect(){ + d_containsVisitor->garbageCollect(); +} + +theory::ContainsTermITEVistor* RemoveITE::getContainsVisitor(){ + return d_containsVisitor; +} + +size_t RemoveITE::collectedCacheSizes() const{ + return d_containsVisitor->cache_size() + d_iteCache.size(); +} + void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap) { for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { @@ -38,18 +60,28 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap) } } +bool RemoveITE::containsTermITE(TNode e){ + return d_containsVisitor->containsTermITE(e); +} + Node RemoveITE::run(TNode node, std::vector<Node>& output, - IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) { + IteSkolemMap& iteSkolemMap, + std::vector<Node>& quantVar) { // Current node Debug("ite") << "removeITEs(" << node << ")" << endl; + if(node.isVar() || node.isConst() || + (options::biasedITERemoval() && !containsTermITE(node))){ + return Node(node); + } + // The result may be cached already NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::iterator i = d_iteCache.find(node); + ITECache::const_iterator i = d_iteCache.find(node); if(i != d_iteCache.end()) { - Node cachedRewrite = (*i).second; - Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl; - return cachedRewrite.isNull() ? Node(node) : cachedRewrite; + Node cached = (*i).second; + Debug("ite") << "removeITEs: in-cache: " << cached << endl; + return cached.isNull() ? Node(node) : cached; } // If an ITE replace it @@ -81,7 +113,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; // Attach the skolem - d_iteCache[node] = skolem; + d_iteCache.insert(node, skolem); // Remove ITEs from the new assertion, rewrite it and push it to the output newAssertion = run(newAssertion, output, iteSkolemMap, quantVar); @@ -127,17 +159,18 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, // If changes, we rewrite if(somethingChanged) { - Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); - d_iteCache[node] = cachedRewrite; - return cachedRewrite; + Node cached = nodeManager->mkNode(node.getKind(), newChildren); + d_iteCache.insert(node, cached); + return cached; } else { - d_iteCache[node] = Node::null(); + d_iteCache.insert(node, Node::null()); return node; } } else { - d_iteCache[node] = Node::null(); + d_iteCache.insert(node, Node::null()); return node; } } + }/* CVC4 namespace */ 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 */ diff --git a/src/util/nary_builder.cpp b/src/util/nary_builder.cpp new file mode 100644 index 000000000..004dd3382 --- /dev/null +++ b/src/util/nary_builder.cpp @@ -0,0 +1,183 @@ + +#include "util/nary_builder.h" +#include "expr/metakind.h" +using namespace std; + +namespace CVC4 { +namespace util { + +Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children){ + if(children.size() == 0){ + return zeroArity(kind); + }else if(children.size() == 1){ + return children[0]; + }else{ + const unsigned int max = kind::metakind::getUpperBoundForKind(kind); + const unsigned int min = kind::metakind::getLowerBoundForKind(kind); + + Assert(min <= children.size()); + + unsigned int numChildren = children.size(); + NodeManager* nm = NodeManager::currentNM(); + if( numChildren <= max ) { + return nm->mkNode(kind,children); + } + + typedef std::vector<Node>::const_iterator const_iterator; + const_iterator it = children.begin() ; + const_iterator end = children.end() ; + + /* The new top-level children and the children of each sub node */ + std::vector<Node> newChildren; + std::vector<Node> subChildren; + + while( it != end && numChildren > max ) { + /* Grab the next max children and make a node for them. */ + for(const_iterator next = it + max; it != next; ++it, --numChildren ) { + subChildren.push_back(*it); + } + Node subNode = nm->mkNode(kind,subChildren); + newChildren.push_back(subNode); + subChildren.clear(); + } + + /* If there's children left, "top off" the Expr. */ + if(numChildren > 0) { + /* If the leftovers are too few, just copy them into newChildren; + * otherwise make a new sub-node */ + if(numChildren < min) { + for(; it != end; ++it) { + newChildren.push_back(*it); + } + } else { + for(; it != end; ++it) { + subChildren.push_back(*it); + } + Node subNode = nm->mkNode(kind, subChildren); + newChildren.push_back(subNode); + } + } + + /* It's inconceivable we could have enough children for this to fail + * (more than 2^32, in most cases?). */ + AlwaysAssert( newChildren.size() <= max, + "Too many new children in mkAssociative" ); + + /* It would be really weird if this happened (it would require + * min > 2, for one thing), but let's make sure. */ + AlwaysAssert( newChildren.size() >= min, + "Too few new children in mkAssociative" ); + + return nm->mkNode(kind,newChildren); + } +} + +Node NaryBuilder::zeroArity(Kind k){ + using namespace kind; + NodeManager* nm = NodeManager::currentNM(); + switch(k){ + case AND: + return nm->mkConst(true); + case OR: + return nm->mkConst(false); + case PLUS: + return nm->mkConst(Rational(0)); + case MULT: + return nm->mkConst(Rational(1)); + default: + return Node::null(); + } +} + + +RePairAssocCommutativeOperators::RePairAssocCommutativeOperators() + : d_cache() +{} +RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){} +size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); } +void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); } + +bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){ + using namespace kind; + switch(k){ + case BITVECTOR_CONCAT: + case BITVECTOR_AND: + case BITVECTOR_OR: + case BITVECTOR_XOR: + case BITVECTOR_MULT: + case BITVECTOR_PLUS: + case DISTINCT: + case PLUS: + case MULT: + case AND: + case OR: + return true; + default: + return false; + } +} + +Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){ + if(d_cache.find(n) != d_cache.end()){ + return d_cache[n]; + } + Node result = + isAssociateCommutative(n.getKind()) ? + case_assoccomm(n) : case_other(n); + + d_cache[n] = result; + return result; +} + +Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){ + Kind k = n.getKind(); + Assert(isAssociateCommutative(k)); + Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED); + unsigned N = n.getNumChildren(); + Assert(N >= 2); + + + Node last = rePairAssocCommutativeOperators( n[N-1]); + Node nextToLast = rePairAssocCommutativeOperators(n[N-2]); + + NodeManager* nm = NodeManager::currentNM(); + Node last2 = nm->mkNode(k, nextToLast, last); + + if(N <= 2){ + return last2; + } else{ + Assert(N > 2); + Node prevRound = last2; + for(unsigned prevPos = N-2; prevPos > 0; --prevPos){ + unsigned currPos = prevPos-1; + Node curr = rePairAssocCommutativeOperators(n[currPos]); + Node round = nm->mkNode(k, curr, prevRound); + prevRound = round; + } + return prevRound; + } +} + +Node RePairAssocCommutativeOperators::case_other(TNode n){ + if(n.isConst() || n.isVar()){ + return n; + } + + NodeBuilder<> nb(n.getKind()); + + if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { + nb << n.getOperator(); + } + + // Remove the ITEs from the children + for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) { + Node newChild = rePairAssocCommutativeOperators(*i); + nb << newChild; + } + + Node result = (Node)nb; + return result; +} + +}/* util namespace */ +}/* CVC4 namespace */ diff --git a/src/util/nary_builder.h b/src/util/nary_builder.h new file mode 100644 index 000000000..ceaa44e77 --- /dev/null +++ b/src/util/nary_builder.h @@ -0,0 +1,38 @@ + +#include "cvc4_private.h" + +#pragma once + +#include <vector> +#include "expr/node.h" + +namespace CVC4{ +namespace util { + +class NaryBuilder { +public: + static Node mkAssoc(Kind k, const std::vector<Node>& children); + static Node zeroArity(Kind k); +};/* class NaryBuilder */ + +class RePairAssocCommutativeOperators { +public: + RePairAssocCommutativeOperators(); + ~RePairAssocCommutativeOperators(); + + Node rePairAssocCommutativeOperators(TNode n); + + static bool isAssociateCommutative(Kind k); + + size_t size() const; + void clear(); +private: + Node case_assoccomm(TNode n); + Node case_other(TNode n); + + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_cache; +};/* class RePairAssocCommutativeOperators */ + +}/* util namespace */ +}/* CVC4 namespace */ |