NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const;
NodeTemplate<true> notNode() const;
+ NodeTemplate<true> negate() const;
template <bool ref_count2>
NodeTemplate<true> andNode(const NodeTemplate<ref_count2>& right) const;
template <bool ref_count2>
return NodeManager::currentNM()->mkNode(kind::NOT, *this);
}
+template <bool ref_count>
+NodeTemplate<true> NodeTemplate<ref_count>::negate() const {
+ assertTNodeNotExpired();
+ return (getKind() == kind::NOT) ? NodeTemplate<true>(d_nv->getChild(0)) : NodeManager::currentNM()->mkNode(kind::NOT, *this);
+}
+
template <bool ref_count>
template <bool ref_count2>
NodeTemplate<true>
template <bool ref_count>
inline Node
NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
+ if (node == *this) {
+ return replacement;
+ }
std::hash_map<TNode, TNode, TNodeHashFunction> cache;
return substitute(node, replacement, cache);
}
Node
NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+ Assert(node != *this);
+
+ if (getNumChildren() == 0) {
+ return *this;
+ }
+
// in cache?
typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
if(i != cache.end()) {
// put in cache
Node n = nb;
+ Assert(node != n);
cache[*this] = n;
return n;
}
*/
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
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);
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
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;
} 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)
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<Node>& assertions)
throw(AssertionException) {
d_assertionsToCheck.swap(d_assertionsToPreprocess);
}
+ if(Options::current()->doITESimp) {
+ // ite simplification
+ simpITE();
+ }
+
if(Options::current()->doStaticLearning) {
// Perform static learning
Trace("simplify") << "SmtEnginePrivate::simplify(): "
// 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
}
}
- // 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
// 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();
}
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<std::string> d_statResultSource;
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 \
if (d_propagateLemmas) {
if (d_equalityEngine.areDisequal(i,j)) {
Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
- Node reason = nm->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);
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 ("<<i<<", "<<j<<")\n";
- Node reason = nm->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;
}
// 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<<"\n";
d_RowAlreadyAdded.insert(lem);
d_out->lemma(lemma);
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 "<<lem<<"\n";
d_RowAlreadyAdded.insert(l);
// non-Boolean-valued ITEs should have been removed in place of
// a variable
// rewrite simple cases of ITE
- if(n[0] == tt) {
- // ITE true x y
- return RewriteResponse(REWRITE_AGAIN, n[1]);
- } else if(n[0] == ff) {
- // ITE false x y
- return RewriteResponse(REWRITE_AGAIN, n[2]);
- } else if(n[1] == n[2]) {
- // ITE c x x
+ if (n[0].isConst()) {
+ if (n[0] == tt) {
+ // ITE true x y
+ return RewriteResponse(REWRITE_AGAIN, n[1]);
+ } else {
+ Assert(n[0] == ff);
+ // ITE false x y
+ return RewriteResponse(REWRITE_AGAIN, n[2]);
+ }
+ } else if (n[1].isConst()) {
+ if (n[1] == tt && n[2] == ff) {
+ return RewriteResponse(REWRITE_AGAIN, n[0]);
+ }
+ else if (n[1] == ff && n[2] == tt) {
+ return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+ }
+ }
+ if (n[1] == n[2]) {
return RewriteResponse(REWRITE_AGAIN, n[1]);
+ // 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));
}
break;
}
--- /dev/null
+/********************* */
+/*! \file ite_simplifier.cpp
+ ** \verbatim
+ ** Original author: barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** 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 "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)
+{
+ 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<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);
+ 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);
+}
+
--- /dev/null
+/********************* */
+/*! \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 <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/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<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;
+
+ 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<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() {}
+
+};
+
+}
+
+#endif
}
Rewriter::init();
StatisticsRegistry::registerStat(&d_combineTheoriesTime);
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
}
TheoryEngine::~TheoryEngine() {
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<bool>(true));
+ d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), d_true);
continue;
}
if (isTrivial) {
value = normalizedEquality.getConst<bool>();
- normalizedEquality = NodeManager::currentNM()->mkConst<bool>(true);
+ normalizedEquality = d_true;
}
else {
d_sharedLiteralsIn[normalizedEquality] = theory::THEORY_LAST;
#endif
// No need to explain "true"
- explained.insert(ExplainTask(NodeManager::currentNM()->mkConst<bool>(true), SHARED_DATABASE_EXPLANATION));
+ explained.insert(ExplainTask(d_true, SHARED_DATABASE_EXPLANATION));
while (true) {
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;
+}
#include "util/stats.h"
#include "util/hash.h"
#include "util/cache.h"
-#include "util/ite_removal.h"
+#include "theory/ite_simplifier.h"
namespace CVC4 {
SharedTermsDatabase d_sharedTerms;
typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
/**
* Cache for theory-preprocessing of assertions
/** Time spent in theory combination */
TimerStat d_combineTheoriesTime;
+ Node d_true;
+ Node d_false;
+
public:
/** Constructs a theory engine */
/** 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 */
decisionMode(DECISION_STRATEGY_INTERNAL),
decisionModeSetByUser(false),
doStaticLearning(true),
+ doITESimp(false),
+ doITESimpSetByUser(false),
interactive(false),
interactiveSetByUser(false),
perCallResourceLimit(0),
--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\
SIMPLIFICATION_MODE,
DECISION_MODE,
NO_STATIC_LEARNING,
+ ITE_SIMP,
+ NO_ITE_SIMP,
INTERACTIVE,
NO_INTERACTIVE,
PRODUCE_ASSIGNMENTS,
{ "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' },
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;
/** 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;
*/
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).
projects / cvc5.git / commitdiff