From: Clark Barrett Date: Fri, 11 May 2012 14:00:27 +0000 (+0000) Subject: Added some ITE rewrites, X-Git-Tag: cvc5-1.0.0~8189 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=57790a14676596e8c6ed42ff7ecd8038ddbaf09b;p=cvc5.git Added some ITE rewrites, Added ITE simplifier - on by default only for QF_LIA benchmarks Fixed one bug in arrays Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode() --- diff --git a/src/expr/node.h b/src/expr/node.h index 37499c3bf..4d39ec60f 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -848,6 +848,7 @@ public: NodeTemplate eqNode(const NodeTemplate& right) const; NodeTemplate notNode() const; + NodeTemplate negate() const; template NodeTemplate andNode(const NodeTemplate& right) const; template @@ -1117,6 +1118,12 @@ NodeTemplate NodeTemplate::notNode() const { return NodeManager::currentNM()->mkNode(kind::NOT, *this); } +template +NodeTemplate NodeTemplate::negate() const { + assertTNodeNotExpired(); + return (getKind() == kind::NOT) ? NodeTemplate(d_nv->getChild(0)) : NodeManager::currentNM()->mkNode(kind::NOT, *this); +} + template template NodeTemplate @@ -1235,6 +1242,9 @@ TypeNode NodeTemplate::getType(bool check) const template inline Node NodeTemplate::substitute(TNode node, TNode replacement) const { + if (node == *this) { + return replacement; + } std::hash_map cache; return substitute(node, replacement, cache); } @@ -1243,6 +1253,12 @@ template Node NodeTemplate::substitute(TNode node, TNode replacement, std::hash_map& cache) const { + Assert(node != *this); + + if (getNumChildren() == 0) { + return *this; + } + // in cache? typename std::hash_map::const_iterator i = cache.find(*this); if(i != cache.end()) { @@ -1268,6 +1284,7 @@ NodeTemplate::substitute(TNode node, TNode replacement, // put in cache Node n = nb; + Assert(node != n); cache[*this] = n; return n; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2759f5717..75b332314 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -156,6 +156,9 @@ class SmtEnginePrivate { */ void removeITEs(); + // Simplify ITE structure + void simpITE(); + /** * Any variable in a assertion that is declared as a subtype type * (predicate subtype or integer subrange type) must be constrained @@ -251,6 +254,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), d_staticLearningTime("smt::SmtEngine::staticLearningTime"), + d_simpITETime("smt::SmtEngine::simpITETime"), + d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"), + d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), + d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), + d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), + d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), d_statResultSource("smt::resultSource", "unknown") { NodeManagerScope nms(d_nodeManager); @@ -258,6 +267,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : StatisticsRegistry::registerStat(&d_definitionExpansionTime); StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime); StatisticsRegistry::registerStat(&d_staticLearningTime); + StatisticsRegistry::registerStat(&d_simpITETime); + StatisticsRegistry::registerStat(&d_iteRemovalTime); + StatisticsRegistry::registerStat(&d_theoryPreprocessTime); + StatisticsRegistry::registerStat(&d_cnfConversionTime); + StatisticsRegistry::registerStat(&d_numAssertionsPre); + StatisticsRegistry::registerStat(&d_numAssertionsPost); StatisticsRegistry::registerStat(&d_statResultSource); // We have mutual dependency here, so we add the prop engine to the theory @@ -347,9 +362,14 @@ SmtEngine::~SmtEngine() throw() { StatisticsRegistry::unregisterStat(&d_definitionExpansionTime); StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime); StatisticsRegistry::unregisterStat(&d_staticLearningTime); + StatisticsRegistry::unregisterStat(&d_simpITETime); + StatisticsRegistry::unregisterStat(&d_iteRemovalTime); + StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime); + StatisticsRegistry::unregisterStat(&d_cnfConversionTime); + StatisticsRegistry::unregisterStat(&d_numAssertionsPre); + StatisticsRegistry::unregisterStat(&d_numAssertionsPost); StatisticsRegistry::unregisterStat(&d_statResultSource); - delete d_private; delete d_userContext; @@ -404,6 +424,13 @@ void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() { } else { theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF); } + // Turn on ite simplification only for QF_LIA + if(! Options::current()->doITESimpSetByUser) { + bool iteSimp = logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() && !logic.isQuantified() && !logic.areRealsUsed(); + Trace("smt") << "setting ite simplification to " << iteSimp << std::endl; + NodeManager::currentNM()->getOptions()->doITESimp = iteSimp; + } + } void SmtEngine::setInfo(const std::string& key, const SExpr& value) @@ -851,6 +878,18 @@ void SmtEnginePrivate::nonClausalSimplify() { d_assertionsToPreprocess.clear(); } +void SmtEnginePrivate::simpITE() +{ + TimerStat::CodeTimer simpITETimer(d_smt.d_simpITETime); + + Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl; + + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + + d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]); + } +} + void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector& assertions) throw(AssertionException) { @@ -934,6 +973,11 @@ void SmtEnginePrivate::simplifyAssertions() d_assertionsToCheck.swap(d_assertionsToPreprocess); } + if(Options::current()->doITESimp) { + // ite simplification + simpITE(); + } + if(Options::current()->doStaticLearning) { // Perform static learning Trace("simplify") << "SmtEnginePrivate::simplify(): " @@ -1038,8 +1082,17 @@ void SmtEnginePrivate::processAssertions() { // removeITEs(). int realAssertionsEnd = d_assertionsToCheck.size(); - // Remove ITEs, updating d_iteSkolemMap - removeITEs(); + { + TimerStat::CodeTimer codeTimer(d_smt.d_iteRemovalTime); + // Remove ITEs + d_smt.d_numAssertionsPre += d_assertionsToCheck.size(); + // Remove ITEs, updating d_iteSkolemMap + removeITEs(); + d_smt.d_numAssertionsPost += d_assertionsToCheck.size(); + // This may need to be in a try-catch + // block. make regress is passing, so + // skipping for now --K + } // begin: INVARIANT to maintain: no reordering of assertions or // introducing new ones @@ -1057,10 +1110,13 @@ void SmtEnginePrivate::processAssertions() { } } - // Call the theory preprocessors - d_smt.d_theoryEngine->preprocessStart(); - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]); + { + TimerStat::CodeTimer codeTimer(d_smt.d_theoryPreprocessTime); + // Call the theory preprocessors + d_smt.d_theoryEngine->preprocessStart(); + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]); + } } // Push the formula to decision engine @@ -1072,9 +1128,13 @@ void SmtEnginePrivate::processAssertions() { // introducing new ones // Push the formula to SAT - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); + { + TimerStat::CodeTimer codeTimer(d_smt.d_cnfConversionTime); + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); + } } + d_assertionsToCheck.clear(); d_iteSkolemMap.clear(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 43d3e1125..10a37b712 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -229,6 +229,19 @@ class CVC4_PUBLIC SmtEngine { TimerStat d_nonclausalSimplificationTime; /** time spent in static learning */ TimerStat d_staticLearningTime; + /** time spent in simplifying ITEs */ + TimerStat d_simpITETime; + /** time spent removing ITEs */ + TimerStat d_iteRemovalTime; + /** time spent in theory preprocessing */ + TimerStat d_theoryPreprocessTime; + /** time spent converting to CNF */ + TimerStat d_cnfConversionTime; + /** Num of assertions before ite removal */ + IntStat d_numAssertionsPre; + /** Num of assertions after ite removal */ + IntStat d_numAssertionsPost; + /** how the SMT engine got the answer -- SAT solver or DE */ BackedStat d_statResultSource; diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 4a077450c..992796ebb 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -29,7 +29,9 @@ libtheory_la_SOURCES = \ shared_terms_database.h \ shared_terms_database.cpp \ term_registration_visitor.h \ - term_registration_visitor.cpp + term_registration_visitor.cpp \ + ite_simplifier.h \ + ite_simplifier.cpp nodist_libtheory_la_SOURCES = \ rewriter_tables.h \ diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 1dd74f060..f073e67d7 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1129,7 +1129,9 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) if (d_propagateLemmas) { if (d_equalityEngine.areDisequal(i,j)) { Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<mkNode(kind::OR, aj.eqNode(bj), i.eqNode(j)); + Node aj_eq_bj = aj.eqNode(bj); + Node i_eq_j = i.eqNode(j); + Node reason = nm->mkNode(kind::OR, aj_eq_bj, i_eq_j); d_permRef.push_back(reason); if (!ajExists) { preRegisterTerm(aj); @@ -1137,15 +1139,17 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) if (!bjExists) { preRegisterTerm(bj); } - d_equalityEngine.assertEquality(aj.eqNode(bj), true, reason); + d_equalityEngine.assertEquality(aj_eq_bj, true, reason); ++d_numProp; return; } if (bothExist && d_equalityEngine.areDisequal(aj,bj)) { Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj)); + Node aj_eq_bj = aj.eqNode(bj); + Node i_eq_j = i.eqNode(j); + Node reason = nm->mkNode(kind::OR, i_eq_j, aj_eq_bj); d_permRef.push_back(reason); - d_equalityEngine.assertEquality(i.eqNode(j), true, reason); + d_equalityEngine.assertEquality(i_eq_j, true, reason); ++d_numProp; return; } @@ -1168,9 +1172,25 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // TODO: maybe add triggers here if (d_eagerLemmas || bothExist) { - Node eq1 = nm->mkNode(kind::EQUAL, aj, bj); - Node eq2 = nm->mkNode(kind::EQUAL, i, j); - Node lemma = nm->mkNode(kind::OR, eq2, eq1); + + Assert(aj == Rewriter::rewrite(aj)); + Assert(bj == Rewriter::rewrite(bj)); + + // construct lemma + Node eq1 = aj.eqNode(bj); + Node eq1_r = Rewriter::rewrite(eq1); + if (eq1_r == d_true) { + d_equalityEngine.assertEquality(eq1, true, d_true); + return; + } + + Node eq2 = i.eqNode(j); + Node eq2_r = Rewriter::rewrite(eq2); + if (eq2 == d_true) { + d_equalityEngine.assertEquality(eq2, true, d_true); + return; + } + Node lemma = nm->mkNode(kind::OR, eq2_r, eq1_r); Trace("arrays-lem")<<"Arrays::addRowLemma adding "<lemma(lemma); @@ -1211,10 +1231,37 @@ void TheoryArrays::dischargeLemmas() continue; } + Node aj2 = Rewriter::rewrite(aj); + if (aj != aj2) { + d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true); + } + Node bj2 = Rewriter::rewrite(bj); + if (bj != bj2) { + d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true); + } + if (aj2 == bj2) { + d_RowQueue.push(l); + continue; + } + // construct lemma - Node eq1 = nm->mkNode(kind::EQUAL, aj, bj); - Node eq2 = nm->mkNode(kind::EQUAL, i, j); - Node lem = nm->mkNode(kind::OR, eq2, eq1); + Node eq1 = aj2.eqNode(bj2); + Node eq1_r = Rewriter::rewrite(eq1); + if (eq1_r == d_true) { + d_equalityEngine.assertEquality(eq1, true, d_true); + d_RowQueue.push(l); + continue; + } + + Node eq2 = i.eqNode(j); + Node eq2_r = Rewriter::rewrite(eq2); + if (eq2_r == d_true) { + d_equalityEngine.assertEquality(eq2, true, d_true); + d_RowQueue.push(l); + continue; + } + + Node lem = nm->mkNode(kind::OR, eq2_r, eq1_r); Trace("arrays-lem")<<"Arrays::addRowLemma adding "<::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::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) +{ + NodeMap::iterator it; + it = d_simpConstCache.find(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[iteNode] = result; + return result; + } + + if (!containsTermITE(iteNode)) { + Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode)); + d_simpConstCache[iteNode] = n; + return n; + } + + Node iteNode2; + Node simpVar2; + d_simpConstCache.clear(); + Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2); + if (!simpContext2.isNull()) { + Assert(!iteNode2.isNull()); + simpContext2 = simpContext.substitute(simpVar, simpContext2); + d_simpConstCache.clear(); + Node n = simpConstants(simpContext2, iteNode2, simpVar2); + if (n.isNull()) { + return n; + } + d_simpConstCache.clear(); + d_simpConstCache[iteNode] = n; + return n; + } + return Node(); +} + + +Node ITESimplifier::getSimpVar(TypeNode t) +{ + if (t.isInteger()) { + if (d_simpVarInt.isNull()) { + d_simpVarInt = NodeManager::currentNM()->mkVar(t); + } + return d_simpVarInt; + } + if (t.isReal()) { + if (d_simpVarReal.isNull()) { + d_simpVarReal = NodeManager::currentNM()->mkVar(t); + } + return d_simpVarReal; + } + return Node(); +} + + +Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) +{ + NodeMap::iterator it; + it = d_simpConstCache.find(c); + if (it != d_simpConstCache.end()) { + return (*it).second; + } + + if (!containsTermITE(c)) { + d_simpConstCache[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_simpConstCache[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_simpConstCache[c] = result; + return result; +} + + +Node ITESimplifier::simpITEAtom(TNode atom) +{ + if (leavesAreConst(atom)) { + Node iteNode; + Node simpVar; + d_simpConstCache.clear(); + Node simpContext = createSimpContext(atom, iteNode, simpVar); + if (!simpContext.isNull()) { + if (iteNode.isNull()) { + Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext)); + return Rewriter::rewrite(simpContext); + } + d_simpConstCache.clear(); + 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 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& 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& css = cs.getCareSet(); + queue.erase(v); + + done = false; + set::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); + cs2 = getNewSet(); + cs2.getCareSet() = css; + cs2.getCareSet().insert(v[1]); + updateQueue(queue, v[0], cs2); + 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); + cs2 = getNewSet(); + cs2.getCareSet() = css; + cs2.getCareSet().insert(v[1].negate()); + updateQueue(queue, v[0], cs2); + 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 new file mode 100644 index 000000000..8466c5444 --- /dev/null +++ b/src/theory/ite_simplifier.h @@ -0,0 +1,154 @@ +/********************* */ +/*! \file ite_simplifier.h + ** \verbatim + ** Original author: barrett + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 +#include +#include + +#include "expr/node.h" +#include "expr/command.h" +#include "prop/prop_engine.h" +#include "context/cdhashset.h" +#include "theory/theory.h" +#include "theory/substitutions.h" +#include "theory/rewriter.h" +#include "theory/substitutions.h" +#include "theory/shared_terms_database.h" +#include "theory/term_registration_visitor.h" +#include "theory/valuation.h" +#include "util/options.h" +#include "util/stats.h" +#include "util/hash.h" +#include "util/cache.h" +#include "util/ite_removal.h" + +namespace CVC4 { + +class ITESimplifier { + Node d_true; + Node d_false; + + std::hash_map d_containsTermITECache; + bool containsTermITE(TNode e); + + std::hash_map d_leavesConstCache; + bool leavesAreConst(TNode e, theory::TheoryId tid); + bool leavesAreConst(TNode e) + { return leavesAreConst(e, theory::Theory::theoryOf(e)); } + + typedef std::hash_map NodeMap; + typedef std::hash_map TNodeMap; + + NodeMap d_simpConstCache; + Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar); + Node d_simpVarInt; + Node d_simpVarReal; + Node getSimpVar(TypeNode t); + 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 d_careSet; + CareSetPtrVal(ITESimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {} + }; + + std::vector 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& 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 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(true); + d_false = NodeManager::currentNM()->mkConst(false); + } + ~ITESimplifier() {} + +}; + +} + +#endif diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 403c90ced..6edeade8d 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -205,4 +205,3 @@ protected: }; } - diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c19bdda91..77a768152 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -69,6 +69,8 @@ TheoryEngine::TheoryEngine(context::Context* context, } Rewriter::init(); StatisticsRegistry::registerStat(&d_combineTheoriesTime); + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); } TheoryEngine::~TheoryEngine() { @@ -318,7 +320,7 @@ void TheoryEngine::combineTheories() { if (carePair.a.isConst() && carePair.b.isConst()) { // TODO: equality engine should auto-detect these as disequal - d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), NodeManager::currentNM()->mkConst(true)); + d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), d_true); continue; } @@ -332,7 +334,7 @@ void TheoryEngine::combineTheories() { if (isTrivial) { value = normalizedEquality.getConst(); - normalizedEquality = NodeManager::currentNM()->mkConst(true); + normalizedEquality = d_true; } else { d_sharedLiteralsIn[normalizedEquality] = theory::THEORY_LAST; @@ -875,7 +877,7 @@ Node TheoryEngine::explain(ExplainTask toExplain) #endif // No need to explain "true" - explained.insert(ExplainTask(NodeManager::currentNM()->mkConst(true), SHARED_DATABASE_EXPLANATION)); + explained.insert(ExplainTask(d_true, SHARED_DATABASE_EXPLANATION)); while (true) { @@ -1011,3 +1013,12 @@ void TheoryEngine::sharedConflict(TNode conflict) { Debug("theory") << "TheoryEngine::sharedConflict(" << conflict << "): " << fullConflict << std::endl; lemma(fullConflict, true, false); } + + +Node TheoryEngine::ppSimpITE(TNode assertion) +{ + Node result = d_iteSimplifier.simpITE(assertion); + result = d_iteSimplifier.simplifyWithCare(result); + result = Rewriter::rewrite(result); + return result; +} diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2871d5559..bb6c93bd6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -41,7 +41,7 @@ #include "util/stats.h" #include "util/hash.h" #include "util/cache.h" -#include "util/ite_removal.h" +#include "theory/ite_simplifier.h" namespace CVC4 { @@ -123,6 +123,7 @@ class TheoryEngine { SharedTermsDatabase d_sharedTerms; typedef std::hash_map NodeMap; + typedef std::hash_map TNodeMap; /** * Cache for theory-preprocessing of assertions @@ -477,6 +478,9 @@ class TheoryEngine { /** Time spent in theory combination */ TimerStat d_combineTheoriesTime; + Node d_true; + Node d_false; + public: /** Constructs a theory engine */ @@ -733,6 +737,12 @@ private: /** Prints the assertions to the debug stream */ void printAssertions(const char* tag); + /** For preprocessing pass simplifying ITEs */ + ITESimplifier d_iteSimplifier; + +public: + Node ppSimpITE(TNode assertion); + };/* class TheoryEngine */ }/* CVC4 namespace */ diff --git a/src/util/options.cpp b/src/util/options.cpp index 140850a28..7c8a07489 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -83,6 +83,8 @@ Options::Options() : decisionMode(DECISION_STRATEGY_INTERNAL), decisionModeSetByUser(false), doStaticLearning(true), + doITESimp(false), + doITESimpSetByUser(false), interactive(false), interactiveSetByUser(false), perCallResourceLimit(0), @@ -178,6 +180,8 @@ Additional CVC4 options:\n\ --simplification=MODE choose simplification mode, see --simplification=help\n\ --decision=MODE choose decision mode, see --decision=help\n\ --no-static-learning turn off static learning (e.g. diamond-breaking)\n\ + --ite-simp turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ + --no-ite-simp turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ --replay=file replay decisions from file\n\ --replay-log=file log decisions and propagations to file\n\ --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\ @@ -359,6 +363,8 @@ enum OptionValue { SIMPLIFICATION_MODE, DECISION_MODE, NO_STATIC_LEARNING, + ITE_SIMP, + NO_ITE_SIMP, INTERACTIVE, NO_INTERACTIVE, PRODUCE_ASSIGNMENTS, @@ -452,6 +458,8 @@ static struct option cmdlineOptions[] = { { "simplification", required_argument, NULL, SIMPLIFICATION_MODE }, { "decision", required_argument, NULL, DECISION_MODE }, { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING }, + { "ite-simp", no_argument, NULL, ITE_SIMP }, + { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP }, { "interactive", no_argument , NULL, INTERACTIVE }, { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { "produce-models", no_argument , NULL, 'm' }, @@ -762,6 +770,16 @@ throw(OptionException) { doStaticLearning = false; break; + case ITE_SIMP: + doITESimp = true; + doITESimpSetByUser = true; + break; + + case NO_ITE_SIMP: + doITESimp = false; + doITESimpSetByUser = true; + break; + case INTERACTIVE: interactive = true; interactiveSetByUser = true; diff --git a/src/util/options.h b/src/util/options.h index eac09fabf..3b6584727 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -146,6 +146,9 @@ struct CVC4_PUBLIC Options { /** Whether to perform the static learning pass. */ bool doStaticLearning; + /** Whether to do the ite-simplification pass */ + bool doITESimp; + /** Whether we're in interactive mode or not */ bool interactive; @@ -249,6 +252,11 @@ struct CVC4_PUBLIC Options { */ bool ufSymmetryBreakerSetByUser; + /** + * Whether the user explicitly requested ite simplification + */ + bool doITESimpSetByUser; + /** * Whether to do the linear diophantine equation solver * in Arith as described by Griggio JSAT 2012 (on by default).