From fd9e22c4a2e57c3dfeda4de3842a3fb3ca4776ba Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Wed, 6 Jun 2012 06:12:40 +0000 Subject: [PATCH] Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better. http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5 --- src/expr/kind_template.h | 1 + src/theory/arrays/theory_arrays.cpp | 104 +-- src/theory/arrays/theory_arrays.h | 12 +- src/theory/bv/bv_subtheory_eq.cpp | 6 +- src/theory/bv/theory_bv.cpp | 57 +- src/theory/bv/theory_bv_utils.h | 23 +- src/theory/output_channel.h | 3 +- src/theory/shared_terms_database.cpp | 268 ++----- src/theory/shared_terms_database.h | 158 ++-- src/theory/theory_engine.cpp | 757 ++++++++++-------- src/theory/theory_engine.h | 245 ++---- src/theory/theory_test_utils.h | 3 +- src/theory/uf/equality_engine.cpp | 170 +++- src/theory/uf/equality_engine.h | 7 + src/theory/uf/equality_engine_types.h | 37 +- src/theory/uf/theory_uf.cpp | 76 +- src/theory/uf/theory_uf.h | 19 +- src/util/options.cpp | 3 +- test/regress/regress0/aufbv/Makefile | 8 + test/regress/regress0/aufbv/Makefile.am | 5 +- .../regress0/aufbv/no_init_multi_delete14.smt | 670 ++++++++++++++++ ...s_wp_su.set_char_quoting.il.wp.delta01.smt | 28 + .../regress0/aufbv/wchains010ue.delta01.smt | 36 + .../regress0/aufbv/wchains010ue.delta02.smt | 35 + test/regress/regress0/aufbv/wchains010ue.smt | 221 +++++ test/regress/regress0/auflia/Makefile.am | 3 +- test/regress/regress0/bv/Makefile.am | 3 +- test/regress/regress0/bv/bug345.smt | 46 ++ ..._sec2_shifter_mult_bmc15.atlas.delta01.smt | 80 ++ test/regress/regress0/uflia/Makefile.am | 5 + .../regress/regress0/uflia/error0.delta01.smt | 78 ++ .../uflia/xs-09-16-3-4-1-5.delta01.smt | 48 ++ .../uflia/xs-09-16-3-4-1-5.delta02.smt | 40 + .../uflia/xs-09-16-3-4-1-5.delta03.smt | 45 ++ .../uflia/xs-09-16-3-4-1-5.delta04.smt | 67 ++ test/system/boilerplate.cpp | 3 +- test/unit/theory/theory_black.h | 3 +- test/unit/theory/theory_engine_white.h | 2 +- 38 files changed, 2368 insertions(+), 1007 deletions(-) create mode 100644 test/regress/regress0/aufbv/Makefile create mode 100644 test/regress/regress0/aufbv/no_init_multi_delete14.smt create mode 100644 test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt create mode 100644 test/regress/regress0/aufbv/wchains010ue.delta01.smt create mode 100644 test/regress/regress0/aufbv/wchains010ue.delta02.smt create mode 100644 test/regress/regress0/aufbv/wchains010ue.smt create mode 100644 test/regress/regress0/bv/bug345.smt create mode 100644 test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt create mode 100644 test/regress/regress0/uflia/error0.delta01.smt create mode 100644 test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt create mode 100644 test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt create mode 100644 test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt create mode 100644 test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index fb76c1857..74641513b 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -130,6 +130,7 @@ ${theory_enum} }; const TheoryId THEORY_FIRST = static_cast(0); +const TheoryId THEORY_SAT_SOLVER = THEORY_LAST; inline TheoryId& operator ++ (TheoryId& id) { return id = static_cast(((int)id) + 1); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 65e409012..4ba4aeba5 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -319,33 +319,12 @@ bool TheoryArrays::propagate(TNode literal) return false; } - // See if the literal has been asserted already - Node normalized = Rewriter::rewrite(literal); - bool satValue = false; - bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue); - - // If asserted, we're done or in conflict - if (isAsserted) { - if (!satValue) { - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; - std::vector assumptions; - Node negatedLiteral; - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - return false; - } - // Propagate even if already known in SAT - could be a new equation between shared terms - // (terms that weren't shared when the literal was asserted!) + // Propagate away + bool ok = d_out->propagate(literal); + if (!ok) { + d_conflict = true; } - - // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl; - d_literalsToPropagate.push_back(literal); - - return true; + return ok; }/* TheoryArrays::propagate(TNode) */ @@ -479,29 +458,7 @@ void TheoryArrays::preRegisterTerm(TNode node) void TheoryArrays::propagate(Effort e) { - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl; - if (!d_conflict) { - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { - TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl; - bool satValue; - Node normalized = Rewriter::rewrite(literal); - if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { - d_out->propagate(literal); - } else { - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl; - Node negatedLiteral; - std::vector assumptions; - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - break; - } - } - } - + // direct propagation now } @@ -634,6 +591,7 @@ void TheoryArrays::computeCareGraph() break; case EQUALITY_FALSE_IN_MODEL: Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl; + continue; break; default: break; @@ -700,11 +658,21 @@ void TheoryArrays::check(Effort e) { Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl; - // If the assertion doesn't have a literal, it's a shared equality - Assert(assertion.isPreregistered || - ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) || - (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL && - d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1])))); + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + + if (!assertion.isPreregistered) { + if (atom.getKind() == kind::EQUAL) { + if (!d_equalityEngine.hasTerm(atom[0])) { + Assert(atom[0].isConst()); + d_equalityEngine.addTerm(atom[0]); + } + if (!d_equalityEngine.hasTerm(atom[1])) { + Assert(atom[1].isConst()); + d_equalityEngine.addTerm(atom[1]); + } + } + } // Do the work switch (fact.getKind()) { @@ -758,19 +726,10 @@ void TheoryArrays::check(Effort e) { } // If in conflict, output the conflict - if (d_conflict) { - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl; - d_out->conflict(d_conflictNode); - } - else { - // Otherwise we propagate - propagate(e); - - if(!d_eagerLemmas && fullEffort(e) && !d_conflict) { - // generate the lemmas on the worklist - Trace("arrays-lem")<<"Arrays::discharging lemmas: "<getLevel()) << "Arrays::check(): done" << endl; @@ -1138,6 +1097,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) TNode b = lem.second; TNode i = lem.third; TNode j = lem.fourth; + Assert(a.getType().isArray() && b.getType().isArray()); if (d_equalityEngine.areEqual(a,b) || d_equalityEngine.areEqual(i,j)) { @@ -1345,6 +1305,16 @@ void TheoryArrays::dischargeLemmas() } } +void TheoryArrays::conflict(TNode a, TNode b) { + if (Theory::theoryOf(a) == theory::THEORY_BOOL) { + d_conflictNode = explain(a.iffNode(b)); + } else { + d_conflictNode = explain(a.eqNode(b)); + } + d_out->conflict(d_conflictNode); + d_conflict = true; +} + }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index d17caba45..6592e86cf 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -261,11 +261,8 @@ class TheoryArrays : public Theory { bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; - if (Theory::theoryOf(t1) == THEORY_BOOL) { - return d_arrays.propagate(t1.iffNode(t2)); - } else { - return d_arrays.propagate(t1.eqNode(t2)); - } + d_arrays.conflict(t1, t2); + return false; } }; @@ -275,9 +272,12 @@ class TheoryArrays : public Theory { /** Equaltity engine */ eq::EqualityEngine d_equalityEngine; - // Are we in conflict? + /** Are we in conflict? */ context::CDO d_conflict; + /** Conflict when merging constants */ + void conflict(TNode a, TNode b); + /** The conflict node */ Node d_conflictNode; diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp index 807d90137..98678a9b4 100644 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -134,7 +134,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool v } bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) { - BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl; + BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl; if (value) { return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY); } else { @@ -143,7 +143,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool } bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl; + Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl; if (value) { return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY); } else { @@ -152,7 +152,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNod } bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; + Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; if (Theory::theoryOf(t1) == THEORY_BOOL) { return d_bv->storePropagation(t1.iffNode(t2), TheoryBV::SUB_EQUALITY); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 251650bf2..30493737a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -141,58 +141,9 @@ void TheoryBV::propagate(Effort e) { } // go through stored propagations - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); - d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) - { + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - Node normalized = Rewriter::rewrite(literal); - - TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; - bool isSharedLiteral = (atom.getKind() == kind::EQUAL && - (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() && - d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end())); - - // Check if this is a SAT literal - if (d_valuation.isSatLiteral(normalized)) { - bool satValue = false; - if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { - // check if we already propagated the negation - Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal); - if (d_alreadyPropagatedSet.find(negLiteral) != d_alreadyPropagatedSet.end()) { - Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; - // we are in conflict - std::vector assumptions; - explain(literal, assumptions); - explain(negLiteral, assumptions); - setConflict(mkAnd(assumptions)); - return; - } - // If it's not a shared literal and hasn't already been set to true, we propagate the normalized version - // shared literals are handled below - if (!isSharedLiteral && !satValue) { - BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << normalized << std::endl; - d_out->propagate(normalized); - d_alreadyPropagatedSet.insert(normalized); - return; - } - } else { - // - Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; - Node negatedLiteral; - std::vector assumptions; - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - explain(literal, assumptions); - setConflict(mkAnd(assumptions)); - return; - } - } - // Either it was not a SAT literal or it was but it is also shared - in that case we have to propagate the original literal (not the normalized one) - if (isSharedLiteral) { - BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl; - d_out->propagate(literal); - d_alreadyPropagatedSet.insert(literal); - } + d_out->propagate(literal); } } @@ -269,16 +220,18 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) void TheoryBV::explain(TNode literal, std::vector& assumptions) { // Ask the appropriate subtheory for the explanation if (propagatedBy(literal, SUB_EQUALITY)) { + BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl; d_equalitySolver.explain(literal, assumptions); } else { Assert(propagatedBy(literal, SUB_BITBLAST)); + BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl; d_bitblastSolver.explain(literal, assumptions); } } Node TheoryBV::explain(TNode node) { - BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; + BVDebug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl; std::vector assumptions; // Ask for the explanation diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 3736da639..c456ef73f 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -72,11 +72,26 @@ inline Node mkVar(unsigned size) { } inline Node mkAnd(std::vector& children) { - if (children.size() > 1) { - return NodeManager::currentNM()->mkNode(kind::AND, children); - } else { - return children[0]; + std::set distinctChildren; + distinctChildren.insert(children.begin(), children.end()); + + if (children.size() == 0) { + return mkTrue(); + } + + if (children.size() == 1) { + return *children.begin(); } + + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = distinctChildren.begin(); + std::set::const_iterator it_end = distinctChildren.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; } inline Node mkSortedNode(Kind kind, std::vector& children) { diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 71bbefb6a..5c2cedf5b 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -103,8 +103,9 @@ public: * Propagate a theory literal. * * @param n - a theory consequence at the current decision level + * @return false if an immediate conflict was encountered */ - virtual void propagate(TNode n) throw(AssertionException) = 0; + virtual bool propagate(TNode n) throw(AssertionException) = 0; /** * Request that the core make a decision on this atom. The decision diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 0c893482a..b081e27ef 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -15,25 +15,26 @@ ** \todo document this file **/ + #include "theory/shared_terms_database.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4; using namespace theory; -SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context) - : ContextNotifyObj(context), - d_context(context), - d_statSharedTerms("theory::shared_terms", 0), - d_addedSharedTermsSize(context, 0), - d_termsToTheories(context), - d_alreadyNotifiedMap(context), - d_sharedNotify(notify), - d_termToNotifyList(context), - d_allocatedNLSize(0), - d_allocatedNLNext(context, 0), - d_EENotify(*this), - d_equalityEngine(d_EENotify, context, "SharedTermsDatabase") +SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context) +: ContextNotifyObj(context) +, d_context(context) +, d_statSharedTerms("theory::shared_terms", 0) +, d_addedSharedTermsSize(context, 0) +, d_termsToTheories(context) +, d_alreadyNotifiedMap(context) +, d_registeredEqualities(context) +, d_EENotify(*this) +, d_equalityEngine(d_EENotify, context, "SharedTermsDatabase") +, d_theoryEngine(theoryEngine) +, d_inConflict(context, false) { StatisticsRegistry::registerStat(&d_statSharedTerms); } @@ -41,11 +42,15 @@ SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException) { StatisticsRegistry::unregisterStat(&d_statSharedTerms); - for (unsigned i = 0; i < d_allocatedNLSize; ++i) { - d_allocatedNL[i]->deleteSelf(); - } } +void SharedTermsDatabase::addEqualityToPropagate(TNode equality) { + d_registeredEqualities.insert(equality); + d_equalityEngine.addTriggerEquality(equality); + checkForConflict(); +} + + void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) { Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; @@ -57,9 +62,6 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo d_addedSharedTerms.push_back(atom); d_addedSharedTermsSize = d_addedSharedTermsSize + 1; d_termsToTheories[search_pair] = theories; - if (!d_equalityEngine.hasTerm(term)) { - d_equalityEngine.addTriggerTerm(term, THEORY_UF); - } } else { Assert(theories != (*find).second); d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); @@ -120,104 +122,26 @@ Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const { } } - -SharedTermsDatabase::NotifyList* SharedTermsDatabase::getNewNotifyList() +bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNode b, bool value) { - NotifyList* retval; - if (d_allocatedNLSize == d_allocatedNLNext) { - retval = new (true) NotifyList(d_context); - d_allocatedNL.push_back(retval); - d_allocatedNLNext = ++d_allocatedNLSize; - } - else { - retval = d_allocatedNL[d_allocatedNLNext]; - d_allocatedNLNext = d_allocatedNLNext + 1; - } - Assert(retval->empty()); - return retval; -} + Debug("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory << a << "," << b << ", " << (value ? "true" : "false") << ")" << endl; - -void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b) -{ - // Note: a is the new representative - Debug("shared-terms-database") << "SharedTermsDatabase::mergeSharedTerms(" << a << "," << b << ")" << endl; - - NotifyList* pnlLeft = NULL; - NotifyList* pnlRight = NULL; - - TermToNotifyList::iterator it = d_termToNotifyList.find(a); - if (it == d_termToNotifyList.end()) { - pnlLeft = getNewNotifyList(); - d_termToNotifyList[a] = pnlLeft; - } - else { - pnlLeft = (*it).second; - } - it = d_termToNotifyList.find(b); - if (it != d_termToNotifyList.end()) { - pnlRight = (*it).second; + if (d_inConflict) { + return false; } - // Get theories interested in EC for lhs - Theory::Set lhsSet = getNotifiedTheories(a); - Theory::Set rhsSet = getNotifiedTheories(b); - NotifyList::iterator nit; - TNode left, right; - - for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) { - - if (Theory::setContains(currentTheory, rhsSet)) { - right = b; - } - else if (pnlRight != NULL && - ((nit = pnlRight->find(currentTheory)) != pnlRight->end())) { - right = (*nit).second; - } - else { - // no match for right: continue - continue; - } - - if (Theory::setContains(currentTheory, lhsSet)) { - left = a; - } - else if ((nit = pnlLeft->find(currentTheory)) != pnlLeft->end()) { - left = (*nit).second; - } - else { - // no match for left: insert right into left - (*pnlLeft)[currentTheory] = right; - continue; - } - - // New shared equality: notify the client - - // TODO: add propagation of disequalities? - - assertEq(left.eqNode(right), currentTheory); + // Propagate away + Node equality = a.eqNode(b); + if (value) { + d_theoryEngine->assertToTheory(equality, theory, THEORY_BUILTIN); + } else { + d_theoryEngine->assertToTheory(equality.notNode(), theory, THEORY_BUILTIN); } -} - - -void SharedTermsDatabase::assertEq(TNode equality, TheoryId theory) -{ - Debug("shared-terms-database") << "SharedTermsDatabase::assertEq(" << equality << ") to theory " << theory << endl; - Node normalized = Rewriter::rewriteEquality(theory, equality); - if (normalized.getKind() != kind::CONST_BOOLEAN || !normalized.getConst()) { - // Notify client - d_sharedNotify.notify(normalized, equality, theory); - } + // As you were + return true; } - -// term was just part of an assertion that makes it shared for theories -// Let's mark that the set theories has now been notified -// In addition, we make sure the equivalence class containing term knows a -// representative for each theory in theories. -// Finally, if the EC already knows a rep for a theory that was just notified, we -// have to tell the theory that these two terms are equal. void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { // Find out if there are any new theories that were notified about this term @@ -232,87 +156,46 @@ void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { if (newlyNotified == 0) { return; } - + Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl; // First update the set of notified theories for this term d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified); - // Now get the representative of the equivalence class and find out which theories it represents - TNode rep = d_equalityEngine.getRepresentative(term); - if (rep != term) { - alreadyNotified = 0; - theoriesFind = d_alreadyNotifiedMap.find(rep); - if (theoriesFind != d_alreadyNotifiedMap.end()) { - alreadyNotified = (*theoriesFind).second; - } - } - - // For each theory that is newly notified - for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) { - if (Theory::setContains(theory, newlyNotified)) { - - Debug("shared-terms-database") << "SharedTermsDatabase::markNotified: processing theory " << theory << endl; - - if (Theory::setContains(theory, alreadyNotified)) { - // rep represents this theory already, need to assert that term = rep - Assert(rep != term); - assertEq(rep.eqNode(term), theory); - } - else { - // Get the list of terms representing theories for this EC - TermToNotifyList::iterator it = d_termToNotifyList.find(rep); - if (it == d_termToNotifyList.end()) { - // No need to do anything - no list associated with this EC - Assert(term == rep); - } - else { - NotifyList* pnl = (*it).second; - Assert(pnl != NULL); - - // Check if this theory is already represented - NotifyList::iterator nit = pnl->find(theory); - if (nit != pnl->end()) { - // Already have a representative for this theory, assert term equal to it - assertEq((*nit).second.eqNode(term), theory); - } - else { - // if term == rep, no need to do anything, as term will represent the theory via alreadyNotifiedMap - if (term != rep) { - // No term in this EC represents this theory, so add term as a new representative - Debug("shared-terms-database") << "SharedTermsDatabase::markNotified: adding " << term << " to representative " << rep << " for theory " << theory << endl; - (*pnl)[theory] = term; - } - } - } - } - } + // Mark the shared terms in the equality engine + theory::TheoryId currentTheory; + while ((currentTheory = Theory::setPop(newlyNotified)) != THEORY_LAST) { + d_equalityEngine.addTriggerTerm(term, currentTheory); } + + // Check for any conflits + checkForConflict(); } - -bool SharedTermsDatabase::areEqual(TNode a, TNode b) { +bool SharedTermsDatabase::areEqual(TNode a, TNode b) const { return d_equalityEngine.areEqual(a,b); } - -bool SharedTermsDatabase::areDisequal(TNode a, TNode b) { +bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const { return d_equalityEngine.areDisequal(a,b,false); } -void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason) +void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode reason) { - bool negated = literal.getKind() == kind::NOT; - TNode atom = negated ? literal[0] : literal; - if (negated) { - Assert(!d_equalityEngine.areDisequal(atom[0], atom[1],false)); - d_equalityEngine.assertEquality(atom, false, reason); - // !!! need to send this out - } - else { - Assert(!d_equalityEngine.areEqual(atom[0], atom[1])); - d_equalityEngine.assertEquality(atom, true, reason); + Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl; + // Add it to the equality engine + d_equalityEngine.assertEquality(equality, polarity, reason); + // Check for conflict + checkForConflict(); +} + +bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity) { + if (polarity) { + d_theoryEngine->propagate(equality, THEORY_BUILTIN); + } else { + d_theoryEngine->propagate(equality.notNode(), THEORY_BUILTIN); } + return true; } static Node mkAnd(const std::vector& conjunctions) { @@ -335,18 +218,35 @@ static Node mkAnd(const std::vector& conjunctions) { } return conjunction; -}/* mkAnd() */ +} +void SharedTermsDatabase::checkForConflict() { + if (d_inConflict) { + d_inConflict = false; + std::vector assumptions; + d_equalityEngine.explainEquality(d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions); + Node conflict = mkAnd(assumptions); + d_theoryEngine->conflict(conflict, THEORY_BUILTIN); + d_conflictLHS = d_conflictRHS = Node::null(); + } +} -Node SharedTermsDatabase::explain(TNode literal) -{ - std::vector assumptions; - if (literal.getKind() == kind::NOT) { - Assert(literal[0].getKind() == kind::EQUAL); - d_equalityEngine.explainEquality(literal[0][0], literal[0][1], false, assumptions); +bool SharedTermsDatabase::isKnown(TNode literal) const { + bool polarity = literal.getKind() != kind::NOT; + TNode equality = polarity ? literal : literal[0]; + if (polarity) { + return d_equalityEngine.areEqual(equality[0], equality[1]); } else { - Assert(literal.getKind() == kind::EQUAL); - d_equalityEngine.explainEquality(literal[0], literal[1], true, assumptions); + return d_equalityEngine.areDisequal(equality[0], equality[1], false); } - return mkAnd(assumptions); } + +Node SharedTermsDatabase::explain(TNode literal) const { + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + Assert(atom.getKind() == kind::EQUAL); + std::vector assumptions; + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + return mkAnd(assumptions); +} + diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index c044097ff..1a38d7332 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -18,12 +18,14 @@ #include "expr/node.h" #include "theory/theory.h" -#include "context/context.h" -#include "util/stats.h" #include "theory/uf/equality_engine.h" +#include "util/stats.h" +#include "context/cdhashset.h" namespace CVC4 { +class TheoryEngine; + class SharedTermsDatabase : public context::ContextNotifyObj { public: @@ -54,51 +56,20 @@ private: /** Context-dependent size of the d_addedSharedTerms list */ context::CDO d_addedSharedTermsSize; - typedef context::CDHashMap, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; - /** A map from atoms and subterms to the theories that use it */ + typedef context::CDHashMap, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; SharedTermsTheoriesMap d_termsToTheories; - typedef context::CDHashMap AlreadyNotifiedMap; - /** Map from term to theories that have already been notified about the shared term */ + typedef context::CDHashMap AlreadyNotifiedMap; AlreadyNotifiedMap d_alreadyNotifiedMap; -public: - - /** Class for notifications about new shared term equalities */ - class SharedTermsNotifyClass { - public: - SharedTermsNotifyClass() {} - virtual ~SharedTermsNotifyClass() {} - virtual void notify(TNode literal, TNode original, theory::TheoryId theory) = 0; - }; + /** The registered equalities for propagation */ + typedef context::CDHashSet RegisteredEqualitiesSet; + RegisteredEqualitiesSet d_registeredEqualities; private: - // Instance of class to send shared term notifications to - SharedTermsNotifyClass& d_sharedNotify; - - // Type for list of theory, node pairs: theory is theory to be notified, - // node is the representative for this equivalence class known to the - // theory that will be notified - typedef context::CDHashMap > NotifyList; - typedef context::CDHashMap TermToNotifyList; - - // Map from terms (only valid for reps) to their notify lists - // Note that theory, term pairs only need to be in the notify list if the - // representative term is not a valid shared term for the theory. - TermToNotifyList d_termToNotifyList; - - // List of allocated NotifyList* objects - std::vector d_allocatedNL; - - // Total number of allocated NotifyList* objects - unsigned d_allocatedNLSize; - - // Size of portion of d_allocatedNL that is currently in use - context::CDO d_allocatedNLNext; - /** This method removes all the un-necessary stuff from the maps */ void backtrack(); @@ -108,7 +79,7 @@ private: public: EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {} bool eqNotifyTriggerEquality(TNode equality, bool value) { - Unreachable(); + d_sharedTerms.propagateEquality(equality, value); return true; } @@ -118,14 +89,12 @@ private: } bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { - if (value) { - d_sharedTerms.mergeSharedTerms(t1, t2); - } - return true; + return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value); } bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { - return true; + d_sharedTerms.conflict(t1, t2, true); + return false; } }; @@ -135,23 +104,82 @@ private: /** Equality engine */ theory::eq::EqualityEngine d_equalityEngine; - /** Attach a new notify list to an equivalence class representative */ - NotifyList* getNewNotifyList(); + /** + * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with + * the theory. Returns false if there is a direct conflict (via rewrite for example). + */ + bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value); + + /** + * Called from the equality engine when a trigger equality is deduced. + */ + bool propagateEquality(TNode equality, bool polarity); + + /** Theory engine */ + TheoryEngine* d_theoryEngine; + + /** Are we in conflict */ + context::CDO d_inConflict; + + /** Conflicting terms, if any */ + Node d_conflictLHS, d_conflictRHS; + + /** Polarity of the conflict */ + bool d_conflictPolarity; + + /** Called by the equality engine notify to mark the conflict */ + void conflict(TNode lhs, TNode rhs, bool polarity) { + if (!d_inConflict) { + // Only remember it if we're not already in conflict + d_inConflict = true; + d_conflictLHS = lhs; + d_conflictRHS = rhs; + d_conflictPolarity = polarity; + } + } - /** Method called by equalityEngine when a becomes equal to b */ - void mergeSharedTerms(TNode a, TNode b); + /** + * Should be called before any public non-const method in order to + * enqueue the conflict to the theory engine. + */ + void checkForConflict(); public: - SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context); + SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context); ~SharedTermsDatabase() throw(AssertionException); + /** + * Asserts the equality to the shared terms database, + */ + void assertEquality(TNode equality, bool polarity, TNode reason); + + /** + * Return whether the equality is alreday known to the engine + */ + bool isKnown(TNode literal) const; + + /** + * Returns an explanation of the propagation that came from the database. + */ + Node explain(TNode literal) const; + + /** + * Add an equality to propagate. + */ + void addEqualityToPropagate(TNode equality); + /** * Add a shared term to the database. The shared term is a subterm of the atom and * should be associated with the given theory. */ void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories); + /** + * Mark that the given theories have been notified of the given shared term. + */ + void markNotified(TNode term, theory::Theory::Set theories); + /** * Returns true if the atom contains any shared terms, false otherwise. */ @@ -176,26 +204,32 @@ public: * Get the theories that share the term and have been notified already. */ theory::Theory::Set getNotifiedTheories(TNode term) const; - - // Notify theory about a new equality between shared terms - void assertEq(TNode equality, theory::TheoryId theory); - + /** - * Mark that the given theories have been notified of the given shared term. + * Returns true if the term is currently registered as shared with some theory. */ - void markNotified(TNode term, theory::Theory::Set theories); - bool isShared(TNode term) const { - return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end(); + return term.isConst() || d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end(); } - bool areEqual(TNode a, TNode b); - - bool areDisequal(TNode a, TNode b); + /** + * Returns true if the literal is an (dis-)equality with both sides registered as shared with + * some theory. + */ + bool isSharedEquality(TNode literal) const { + TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; + return atom.getKind() == kind::EQUAL && isShared(atom[0]) && isShared(atom[1]); + } - void processSharedLiteral(TNode literal, TNode reason); + /** + * Returns true if the shared terms a and b are known to be equal. + */ + bool areEqual(TNode a, TNode b) const; - Node explain(TNode literal); + /** + * Retursn true if the shared terms a and b are known to be dis-equal. + */ + bool areDisequal(TNode a, TNode b) const; protected: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3e1dc6fe4..ca2460805 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -45,22 +45,22 @@ TheoryEngine::TheoryEngine(context::Context* context, d_context(context), d_userContext(userContext), d_logicInfo(logicInfo), - d_notify(*this), - d_sharedTerms(d_notify, context), + d_sharedTerms(this, context), d_ppCache(), d_possiblePropagations(context), d_hasPropagated(context), d_inConflict(context, false), d_hasShutDown(false), d_incomplete(context, false), - d_sharedLiteralsIn(context), - d_assertedLiteralsOut(context), + d_propagationMap(context), + d_propagationMapTimestamp(context, 0), d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_decisionRequests(context), d_decisionRequestsIndex(context, 0), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_inPreregister(false), + d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), d_unconstrainedSimp(context, logicInfo) @@ -105,6 +105,11 @@ void TheoryEngine::preRegister(TNode preprocessed) { preprocessed = d_preregisterQueue.front(); d_preregisterQueue.pop(); + if (d_logicInfo.isSharingEnabled() && preprocessed.getKind() == kind::EQUAL) { + // When sharing is enabled, we propagate from the shared terms manager also + d_sharedTerms.addEqualityToPropagate(preprocessed); + } + // Pre-register the terms in the atom bool multipleTheories = NodeVisitor::run(d_preRegistrationVisitor, preprocessed); if (multipleTheories) { @@ -148,6 +153,50 @@ void TheoryEngine::printAssertions(const char* tag) { } } +void TheoryEngine::dumpAssertions(const char* tag) { + if (Dump.isOn(tag)) { + Dump(tag) << CommentCommand("Starting completeness check"); + for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { + Theory* theory = d_theoryTable[theoryId]; + if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { + Dump(tag) << CommentCommand("Completeness check"); + Dump(tag) << PushCommand(); + + // Dump the shared terms + if (d_logicInfo.isSharingEnabled()) { + Dump(tag) << CommentCommand("Shared terms"); + context::CDList::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + stringstream ss; + ss << (*it); + Dump(tag) << CommentCommand(ss.str()); + } + } + + // Dump the assertions + Dump(tag) << CommentCommand("Assertions"); + context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (; it != it_end; ++ it) { + // Get the assertion + Node assertionNode = (*it).assertion; + // Purify all the terms + + BoolExpr assertionExpr(assertionNode.toExpr()); + if ((*it).isPreregistered) { + Dump(tag) << CommentCommand("Preregistered"); + } else { + Dump(tag) << CommentCommand("Shared assertion"); + } + Dump(tag) << AssertCommand(assertionExpr); + } + Dump(tag) << CheckSatCommand(); + Dump(tag) << PopCommand(); + } + } + } +} + + template class scoped_vector_clear { vector& d_v; @@ -181,8 +230,6 @@ void TheoryEngine::check(Theory::Effort effort) { } \ } - // make sure d_propagatedSharedLiterals is cleared on exit - scoped_vector_clear clear_shared_literals(d_propagatedSharedLiterals); // Do the checking try { @@ -194,15 +241,25 @@ void TheoryEngine::check(Theory::Effort effort) { // Mark the lemmas flag (no lemmas added) d_lemmasAdded = false; - while (true) { + Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << std::endl; + + // If in full effort, we have a fake new assertion just to jumpstart the checking + if (Theory::fullEffort(effort)) { + d_factsAsserted = true; + } + + // Check until done + while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) { Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl; - Assert(d_propagatedSharedLiterals.empty()); if (Debug.isOn("theory::assertions")) { printAssertions("theory::assertions"); } + // Note that we've discharged all the facts + d_factsAsserted = false; + // Do the checking CVC4_FOR_EACH_THEORY; @@ -217,34 +274,11 @@ void TheoryEngine::check(Theory::Effort effort) { // We are still satisfiable, propagate as much as possible propagate(effort); - // If we have any propagated shared literals, we enqueue them to the theories and re-check - if (d_propagatedSharedLiterals.size() > 0) { - Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl; - outputSharedLiterals(); - continue; - } - - // If we added any lemmas, we're done - if (d_lemmasAdded) { - Debug("theory") << "TheoryEngine::check(" << effort << "): lemmas added, done" << std::endl; - break; - } - - // If in full check and no lemmas added, run the combination - if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled()) { + // We do combination if all has been processed and we are in fullcheck + if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded) { // Do the combination Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << std::endl; combineTheories(); - // If we have any propagated shared literals, we enqueue them to the theories and re-check - if (d_propagatedSharedLiterals.size() > 0) { - Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl; - outputSharedLiterals(); - } else { - // No propagated shared literals, we're either sat, or there are lemmas added - break; - } - } else { - break; } } @@ -253,30 +287,15 @@ void TheoryEngine::check(Theory::Effort effort) { } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => conflict" << endl; } -} - -void TheoryEngine::outputSharedLiterals() { - - scoped_vector_clear clear_shared_literals(d_propagatedSharedLiterals); - - // Assert all the shared literals - for (unsigned i = 0; i < d_propagatedSharedLiterals.size(); ++ i) { - const SharedLiteral& eq = d_propagatedSharedLiterals[i]; - // Check if the theory already got this one - if (d_assertedLiteralsOut.find(eq.toAssert) == d_assertedLiteralsOut.end()) { - Debug("sharing") << "TheoryEngine::outputSharedLiterals(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << std::endl; - Debug("sharing") << "TheoryEngine::outputSharedLiterals(): orignal " << eq.toExplain << std::endl; - d_assertedLiteralsOut[eq.toAssert] = eq.toExplain; - if (eq.toAssert.theory == theory::THEORY_LAST) { - d_propagatedLiterals.push_back(eq.toAssert.node); - } else { - theoryOf(eq.toAssert.theory)->assertFact(eq.toAssert.node, false); - } + + // If fulleffort, check all theories + if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) { + if (!d_inConflict && !d_lemmasAdded) { + dumpAssertions("theory::fullcheck"); } } } - void TheoryEngine::combineTheories() { Debug("sharing") << "TheoryEngine::combineTheories()" << std::endl; @@ -305,44 +324,38 @@ void TheoryEngine::combineTheories() { Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl; - if (d_sharedTerms.areEqual(carePair.a, carePair.b) || - d_sharedTerms.areDisequal(carePair.a, carePair.b)) { - continue; - } - - 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(), d_true); - continue; - } + Assert(!d_sharedTerms.areEqual(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); + Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); + // The equality in question Node equality = carePair.a.eqNode(carePair.b); + + // Normalize the equality Node normalizedEquality = Rewriter::rewrite(equality); - bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN; - bool value; - if (isTrivial || (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value))) { - // Missed propagation! - Debug("sharing") << "TheoryEngine::combineTheories(): has a literal or is trivial" << std::endl; - - if (isTrivial) { - value = normalizedEquality.getConst(); - normalizedEquality = d_true; - } - else { - d_sharedLiteralsIn[normalizedEquality] = theory::THEORY_LAST; - if (!value) normalizedEquality = normalizedEquality.notNode(); - } - if (!value) { - equality = equality.notNode(); + + // Check if the normalized equality already has a value (this also + // covers constants, since they always have values + if (d_propEngine->isSatLiteral(normalizedEquality)) { + bool value; + if (d_propEngine->hasValue(normalizedEquality, value)) { + Assert(equality != normalizedEquality); + Node literal = value ? equality : equality.notNode(); + Node normalizedLiteral = value ? normalizedEquality : normalizedEquality.notNode(); + // We're sending the original literal back, backed by the normalized one + if (markPropagation(literal, normalizedLiteral, /* to */ carePair.theory, /* from */ THEORY_SAT_SOLVER)) { + // We assert it, and we know it's preregistereed if it's the same theory + bool preregistered = Theory::theoryOf(literal) == carePair.theory; + theoryOf(carePair.theory)->assertFact(literal, preregistered); + // Mark that we have more information + d_factsAsserted = true; + continue; + } } - d_sharedTerms.processSharedLiteral(equality, normalizedEquality); - continue; } - - // There is no value, so we need to split on it + + // We need to split on it Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl; lemma(equality.orNode(equality.notNode()), false, false); - } } @@ -363,7 +376,7 @@ void TheoryEngine::propagate(Theory::Effort effort) { for(unsigned i = 0; i < d_possiblePropagations.size(); ++ i) { Node atom = d_possiblePropagations[i]; bool value; - if (d_propEngine->hasValue(atom, value)) continue; + if (!d_propEngine->hasValue(atom, value)) continue; // Doesn't have a value, check it (and the negation) if(d_hasPropagated.find(atom) == d_hasPropagated.end()) { Dump("missed-t-propagations") @@ -662,24 +675,160 @@ Node TheoryEngine::preprocess(TNode assertion) { return d_ppCache[assertion]; } -void TheoryEngine::assertFact(TNode node) -{ - Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; - // Trace("theory::assertions") << "TheoryEngine::assertFact(" << node << "): d_sharedTermsExist = " << (d_sharedTermsExist ? "true" : "false") << std::endl; +bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { + + // What and where we are asserting + NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp); + // What and where it came from + NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp); + + // See if the theory already got this literal + PropagationMap::const_iterator find = d_propagationMap.find(toAssert); + if (find != d_propagationMap.end()) { + // The theory already knows this + Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << std::endl; + return false; + } + + Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp << "] " << assertion << ", " << toTheoryId << " from " << originalAssertion << ", " << fromTheoryId << std::endl; + + // Mark the propagation + d_propagationMap[toAssert] = toExplain; + d_propagationMapTimestamp = d_propagationMapTimestamp + 1; + + return true; +} + + +void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { + + Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << std::endl; + + Assert(toTheoryId != fromTheoryId); + + if (d_inConflict) { + return; + } + + // If sharing is disabled, things are easy + if (!d_logicInfo.isSharingEnabled()) { + if (fromTheoryId == THEORY_SAT_SOLVER) { + // Send to the apropriate theory + theory::Theory* toTheory = theoryOf(toTheoryId); + // We assert it, and we know it's preregistereed + toTheory->assertFact(assertion, true); + // Mark that we have more information + d_factsAsserted = true; + } else { + Assert(toTheoryId == THEORY_SAT_SOLVER); + // Enqueue for propagation to the SAT solver + d_propagatedLiterals.push_back(assertion); + // Check for propositional conflict + bool value; + if (d_propEngine->hasValue(assertion, value) && !value) { + d_inConflict = true; + } + } + return; + } + + // Polarity of the assertion + bool polarity = assertion.getKind() != kind::NOT; + + // Atom of the assertion + TNode atom = polarity ? assertion : assertion[0]; + + // If sending to the shared terms database, it's also simple + if (toTheoryId == THEORY_BUILTIN) { + Assert(atom.getKind() == kind::EQUAL); + if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) { + d_sharedTerms.assertEquality(atom, polarity, assertion); + } + return; + } + + // Things from the SAT solver are already normalized, so they go + // directly to the apropriate theory + if (fromTheoryId == THEORY_SAT_SOLVER) { + // We know that this is normalized, so just send it off to the theory + if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) { + // We assert it, and we know it's preregistereed coming from the SAT solver directly + theoryOf(toTheoryId)->assertFact(assertion, true); + // Mark that we have more information + d_factsAsserted = true; + } + return; + } + + // Propagations to the SAT solver are just enqueued for pickup by + // the SAT solver later + if (toTheoryId == THEORY_SAT_SOLVER) { + if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) { + // Enqueue for propagation to the SAT solver + d_propagatedLiterals.push_back(assertion); + // Check for propositional conflicts + bool value; + if (d_propEngine->hasValue(assertion, value) && !value) { + d_inConflict = true; + } + } + return; + } + + // We are left with internal distribution of shared literals + Assert(atom.getKind() == kind::EQUAL); + Node normalizedAtom = Rewriter::rewriteEquality(toTheoryId, atom); + Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode(); + + // If we normalize to true or false, it's a special case + if (normalizedAtom.isConst()) { + if (polarity == normalizedAtom.getConst()) { + // Trivially true, just ignore + return; + } else { + // Mark the propagation for explanations + if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) { + // Get the explanation (conflict will figure out where it came from) + conflict(normalizedAssertion, toTheoryId); + } else { + Unreachable(); + } + return; + } + } + + // Try and assert + if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) { + // Check if has been pre-registered with the theory + bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAtom) == toTheoryId; + // Assert away + theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered); + d_factsAsserted = true; + } + + return; +} +void TheoryEngine::assertFact(TNode literal) +{ + Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << std::endl; + d_propEngine->checkTime(); + // If we're in conflict, nothing to do + if (d_inConflict) { + return; + } + // Get the atom - bool negated = node.getKind() == kind::NOT; - TNode atom = negated ? node[0] : node; - Theory* theory = theoryOf(atom); + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; if (d_logicInfo.isSharingEnabled()) { - Trace("theory::assertions") << "TheoryEngine::assertFact(" << node << "): hasShared terms = " << (d_sharedTerms.hasSharedTerms(atom) ? "true" : "false") << std::endl; - - // If any shared terms, notify the theories + // If any shared terms, it's time to do sharing work if (d_sharedTerms.hasSharedTerms(atom)) { + // Notify the theories the shared terms SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); for (; it != it_end; ++ it) { @@ -692,48 +841,27 @@ void TheoryEngine::assertFact(TNode node) } d_sharedTerms.markNotified(term, theories); } - if (d_propagatedSharedLiterals.size() > 0) { - Debug("theory") << "TheoryEngine::assertFact: distributing shared literals from new shared terms" << std::endl; - outputSharedLiterals(); - } } - if (atom.getKind() == kind::EQUAL && - d_sharedTerms.isShared(atom[0]) && - d_sharedTerms.isShared(atom[1])) { - Debug("sharing") << "TheoryEngine::assertFact: asserting shared node: " << node << std::endl; - // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain - if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) || - ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) { - Debug("sharing") << "TheoryEngine::assertFact: sharedLiteral already known(" << node << ")" << std::endl; - return; - } - d_sharedLiteralsIn[node] = THEORY_LAST; - d_sharedTerms.processSharedLiteral(node, node); - if (d_propagatedSharedLiterals.size() > 0) { - Debug("theory") << "TheoryEngine::assertFact: distributing shared literals from new assertion" << std::endl; - outputSharedLiterals(); - } - // TODO: have processSharedLiteral propagate disequalities? - if (node.getKind() == kind::EQUAL) { - // Don't have to assert it - this will be taken care of by processSharedLiteral - Assert(d_logicInfo.isTheoryEnabled(theory->getId())); - return; - } - } - // If theory didn't already get this literal, add to the map - NodeTheoryPair ntp(node, theory->getId()); - if (d_assertedLiteralsOut.find(ntp) == d_assertedLiteralsOut.end()) { - d_assertedLiteralsOut[ntp] = Node(); + // If it's an equality, assert it to the shared term manager, even though the terms are not + // yet shared. As the terms become shared later, the shared terms manager will then add them + // to the assert the equality to the interested theories + if (atom.getKind() == kind::EQUAL) { + // Assert it to the the owning theory + assertToTheory(literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); + // Shared terms manager will assert to interested theories directly, as the terms become shared + assertToTheory(literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER); + } else { + // Not an equality, just assert to the appropriate theory + assertToTheory(literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); } + } else { + // Assert the fact to the appropriate theory directly + assertToTheory(literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); } - - // Assert the fact to the appropriate theory and mark it active - theory->assertFact(node, true); - Assert(d_logicInfo.isTheoryEnabled(theory->getId())); } -void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { +bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Debug("theory") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << std::endl; @@ -747,42 +875,26 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { d_hasPropagated.insert(literal); } - bool negated = (literal.getKind() == kind::NOT); - TNode atom = negated ? literal[0] : literal; - bool value; + // Get the atom + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; - if (!d_logicInfo.isSharingEnabled() || atom.getKind() != kind::EQUAL || - !d_sharedTerms.isShared(atom[0]) || !d_sharedTerms.isShared(atom[1])) { - // If not an equality or if an equality between terms that are not both shared, - // it must be a SAT literal so we enqueue it - Assert(d_propEngine->isSatLiteral(literal)); - if (d_propEngine->hasValue(literal, value)) { - // if we are propagting something that already has a sat value we better be the same - Debug("theory") << "literal " << literal << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl; - Assert(value); - } else { - d_propagatedLiterals.push_back(literal); + if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) { + if (d_propEngine->isSatLiteral(literal)) { + // We propagate SAT literals to SAT + assertToTheory(literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); } - } else { - // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain - if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) || - ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) { - Debug("sharing") << "TheoryEngine::propagate: sharedLiteral already known(" << literal << ")" << std::endl; - return; + if (theory != THEORY_BUILTIN) { + // Assert to the shared terms database + assertToTheory(literal, /* to */ THEORY_BUILTIN, /* from */ theory); } - - // Otherwise it is a shared-term (dis-)equality - Node normalizedLiteral = Rewriter::rewrite(literal); - if (d_propEngine->isSatLiteral(normalizedLiteral)) { - // If there is a literal, propagate it to SAT - SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST); - d_propagatedSharedLiterals.push_back(sharedLiteral); - } - // Assert to interested theories - Debug("shared-in") << "TheoryEngine::propagate: asserting shared node: " << literal << std::endl; - d_sharedLiteralsIn[literal] = theory; - d_sharedTerms.processSharedLiteral(literal, literal); + } else { + // Just send off to the SAT solver + Assert(d_propEngine->isSatLiteral(literal)); + assertToTheory(literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); } + + return !d_inConflict; } @@ -809,160 +921,112 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); } -Node TheoryEngine::getExplanation(TNode node) { - Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; +static Node mkExplanation(const std::vector& explanation) { - TNode atom = node.getKind() == kind::NOT ? node[0] : node; - - Node explanation; - - // The theory that has explaining to do - Theory* theory; - - //This is true if atom is a shared assertion - bool sharedLiteral = false; - - AssertedLiteralsOutMap::iterator find; - // "find" will have a value when sharedAssertion is true - if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) { - find = d_assertedLiteralsOut.find(NodeTheoryPair(node, theory::THEORY_LAST)); - sharedLiteral = (find != d_assertedLiteralsOut.end()); + std::set all; + for (unsigned i = 0; i < explanation.size(); ++ i) { + Assert(explanation[i].theory == THEORY_SAT_SOLVER); + all.insert(explanation[i].node); } - // Get the explanation - if(sharedLiteral) { - explanation = explain(ExplainTask((*find).second, SHARED_LITERAL_OUT)); - } else { - theory = theoryOf(atom); - explanation = theory->explain(node); - - // Explain any shared equalities that might be in the explanation - if (d_logicInfo.isSharingEnabled()) { - explanation = explain(ExplainTask(explanation, THEORY_EXPLANATION, theory->getId())); - } + if (all.size() == 0) { + // Normalize to true + return NodeManager::currentNM()->mkConst(true); } - Assert(!explanation.isNull()); - if(Dump.isOn("t-explanations")) { - Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") - << QueryCommand(explanation.impNode(node).toExpr()); + if (all.size() == 1) { + // All the same, or just one + return explanation[0].node; } - Assert(properExplanation(node, explanation)); - Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl; + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } - return explanation; + return conjunction; } -Node TheoryEngine::explain(ExplainTask toExplain) -{ - Debug("theory") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl; - - std::set satAssertions; - std::deque explainQueue; - // TODO: benchmark whether this helps - std::hash_set explained; -#ifdef CVC4_ASSERTIONS - bool value; -#endif - - // No need to explain "true" - explained.insert(ExplainTask(d_true, SHARED_DATABASE_EXPLANATION)); - - while (true) { - - Debug("theory-explain") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl; - - if (explained.find(toExplain) == explained.end()) { +Node TheoryEngine::getExplanation(TNode node) { + Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; - explained.insert(toExplain); + bool polarity = node.getKind() != kind::NOT; + TNode atom = polarity ? node : node[0]; - if (toExplain.node.getKind() == kind::AND) { - for (unsigned i = 0, i_end = toExplain.node.getNumChildren(); i != i_end; ++ i) { - explainQueue.push_back(ExplainTask(toExplain.node[i], toExplain.kind, toExplain.theory)); - } - } - else { - - switch (toExplain.kind) { - - // toExplain.node contains a shared literal sent out from theory engine (before being rewritten) - case SHARED_LITERAL_OUT: { - // Shortcut - see if this came directly from a theory - SharedLiteralsInMap::iterator it = d_sharedLiteralsIn.find(toExplain.node); - if (it != d_sharedLiteralsIn.end()) { - TheoryId id = (*it).second; - if (id == theory::THEORY_LAST) { - Assert(d_propEngine->isSatLiteral(toExplain.node)); - Assert(d_propEngine->hasValue(toExplain.node, value) && value); - satAssertions.insert(toExplain.node); - break; - } - explainQueue.push_back(ExplainTask(theoryOf((*it).second)->explain(toExplain.node), THEORY_EXPLANATION, (*it).second)); - } - // Otherwise, get explanation from shared terms database - else { - explainQueue.push_back(ExplainTask(d_sharedTerms.explain(toExplain.node), SHARED_DATABASE_EXPLANATION)); - } - break; - } + // If we're not in shared mode, explanations are simple + if (!d_logicInfo.isSharingEnabled()) { + Node explanation = theoryOf(atom)->explain(node); + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl; + return explanation; + } - // toExplain.node contains explanation from theory, toExplain.theory contains theory that produced explanation - case THEORY_EXPLANATION: { - AssertedLiteralsOutMap::iterator find = d_assertedLiteralsOut.find(NodeTheoryPair(toExplain.node, toExplain.theory)); - if (find == d_assertedLiteralsOut.end() || (*find).second.isNull()) { - Assert(d_propEngine->isSatLiteral(toExplain.node)); - Assert(d_propEngine->hasValue(toExplain.node, value) && value); - satAssertions.insert(toExplain.node); - } - else { - explainQueue.push_back(ExplainTask((*find).second, SHARED_LITERAL_OUT)); - } - break; - } + // Initial thing to explain + NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp); + Assert(d_propagationMap.find(toExplain) != d_propagationMap.end()); + // Create the workplace for explanations + std::vector explanationVector; + explanationVector.push_back(d_propagationMap[toExplain]); + // Process the explanation + getExplanation(explanationVector); + Node explanation = mkExplanation(explanationVector); + + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl; + + return explanation; +} - // toExplain.node contains an explanation from the shared terms database - // Each literal in the explanation should be in the d_sharedLiteralsIn map - case SHARED_DATABASE_EXPLANATION: { - Assert(d_sharedLiteralsIn.find(toExplain.node) != d_sharedLiteralsIn.end()); - TheoryId id = d_sharedLiteralsIn[toExplain.node]; - if (id == theory::THEORY_LAST) { - Assert(d_propEngine->isSatLiteral(toExplain.node)); - Assert(d_propEngine->hasValue(toExplain.node, value) && value); - satAssertions.insert(toExplain.node); - } - else { - explainQueue.push_back(ExplainTask(theoryOf(id)->explain(toExplain.node), THEORY_EXPLANATION, id)); - } - break; - } - default: - Unreachable(); - } - } - } +theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable) { + if(Dump.isOn("t-lemmas")) { + Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") + << QueryCommand(node.toExpr()); + } - if (explainQueue.empty()) break; + // Share with other portfolio threads + if(Options::current()->lemmaOutputChannel != NULL) { + Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr()); + } - toExplain = explainQueue.front(); - explainQueue.pop_front(); + // Remove the ITEs + std::vector additionalLemmas; + IteSkolemMap iteSkolemMap; + additionalLemmas.push_back(node); + RemoveITE::run(additionalLemmas, iteSkolemMap); + additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); + + // assert to prop engine + d_propEngine->assertLemma(additionalLemmas[0], negated, removable); + for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { + additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); + d_propEngine->assertLemma(additionalLemmas[i], false, removable); } - Assert(satAssertions.size() > 0); - if (satAssertions.size() == 1) { - return *(satAssertions.begin()); + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + if(negated) { + // Can't we just get rid of passing around this 'negated' stuff? + // Is it that hard for the propEngine to figure that out itself? + // (I like the use of triple negation .) --K + additionalLemmas[0] = additionalLemmas[0].notNode(); + negated = false; } + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - // Now build the explanation - NodeBuilder<> conjunction(kind::AND); - std::set::const_iterator it = satAssertions.begin(); - std::set::const_iterator it_end = satAssertions.end(); - while (it != it_end) { - conjunction << *it; - ++ it; + // assert to decision engine + if(!removable) { + d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap); } - return conjunction; + + // Mark that we added some lemmas + d_lemmasAdded = true; + + // Lemma analysis isn't online yet; this lemma may only live for this + // user level. + return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel()); } void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { @@ -974,12 +1038,16 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << CheckSatCommand(conflict.toExpr()); } - + + // In the multiple-theories case, we need to reconstruct the conflict if (d_logicInfo.isSharingEnabled()) { - // In the multiple-theories case, we need to reconstruct the conflict - Node fullConflict = explain(ExplainTask(conflict, THEORY_EXPLANATION, theoryId)); - Assert(properConflict(fullConflict)); - Debug("theory") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): " << fullConflict << std::endl; + // Create the workplace for explanations + std::vector explanationVector; + explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); + // Process the explanation + getExplanation(explanationVector); + Node fullConflict = mkExplanation(explanationVector); + Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << std::endl; lemma(fullConflict, true, false); } else { // When only one theory, the conflict should need no processing @@ -988,24 +1056,6 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } - -//Conflict from shared terms database -void TheoryEngine::sharedConflict(TNode conflict) { - // Mark that we are in conflict - d_inConflict = true; - - if(Dump.isOn("t-conflicts")) { - Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") - << CheckSatCommand(conflict.toExpr()); - } - - Node fullConflict = explain(ExplainTask(d_sharedTerms.explain(conflict), SHARED_DATABASE_EXPLANATION)); - Assert(properConflict(fullConflict)); - Debug("theory") << "TheoryEngine::sharedConflict(" << conflict << "): " << fullConflict << std::endl; - lemma(fullConflict, true, false); -} - - Node TheoryEngine::ppSimpITE(TNode assertion) { Node result = d_iteSimplifier.simpITE(assertion); @@ -1014,6 +1064,77 @@ Node TheoryEngine::ppSimpITE(TNode assertion) return result; } +void TheoryEngine::getExplanation(std::vector& explanationVector) +{ + Assert(explanationVector.size() > 0); + + unsigned i = 0; // Index of the current literal we are processing + unsigned j = 0; // Index of the last literal we are keeping + + while (i < explanationVector.size()) { + + // Get the current literal to explain + NodeTheoryPair toExplain = explanationVector[i]; + + Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << std::endl; + + // If a treu constant or a negation of a false constant we can ignore it + if (toExplain.node.isConst() && toExplain.node.getConst()) { + ++ i; + continue; + } + if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst()) { + ++ i; + continue; + } + + // If from the SAT solver, keep it + if (toExplain.theory == THEORY_SAT_SOLVER) { + explanationVector[j++] = explanationVector[i++]; + continue; + } + + // If an and, expand it + if (toExplain.node.getKind() == kind::AND) { + Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.node << " got from " << toExplain.theory << std::endl; + for (unsigned k = 0; k < toExplain.node.getNumChildren(); ++ k) { + NodeTheoryPair newExplain(toExplain.node[k], toExplain.theory, toExplain.timestamp); + explanationVector.push_back(newExplain); + } + ++ i; + continue; + } + + // See if it was sent to the theory by another theory + PropagationMap::const_iterator find = d_propagationMap.find(toExplain); + if (find != d_propagationMap.end()) { + // There is some propagation, check if its a timely one + if ((*find).second.timestamp < toExplain.timestamp) { + explanationVector.push_back((*find).second); + ++ i; + continue; + } + } + + // It was produced by the theory, so ask for an explanation + Node explanation; + if (toExplain.theory == THEORY_BUILTIN) { + explanation = d_sharedTerms.explain(toExplain.node); + } else { + explanation = theoryOf(toExplain.theory)->explain(toExplain.node); + } + Assert(explanation != toExplain.node, "wansn't sent to you, so why are you explaining it trivially"); + Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << std::endl; + // Mark the explanation + NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); + explanationVector.push_back(newExplain); + ++ i; + } + + // Keep only the relevant literals + explanationVector.resize(j); +} + void TheoryEngine::ppUnconstrainedSimp(vector& assertions) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index bc9f4c889..ed95149b3 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -46,16 +46,19 @@ namespace CVC4 { -// In terms of abstraction, this is below (and provides services to) -// PropEngine. - +/** + * A pair of a theory and a node. This is used to mark the flow of + * propagations between theories. + */ struct NodeTheoryPair { Node node; theory::TheoryId theory; - NodeTheoryPair(TNode node, theory::TheoryId theory) - : node(node), theory(theory) {} + size_t timestamp; + NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp) + : node(node), theory(theory), timestamp(timestamp) {} NodeTheoryPair() : theory(theory::THEORY_LAST) {} + // Comparison doesn't take into account the timestamp bool operator == (const NodeTheoryPair& pair) const { return node == pair.node && theory == pair.theory; } @@ -63,6 +66,7 @@ struct NodeTheoryPair { struct NodeTheoryPairHashFunction { NodeHashFunction hashFunction; + // Hash doesn't take into account the timestamp size_t operator()(const NodeTheoryPair& pair) const { return hashFunction(pair.node)*0x9e3779b9 + pair.theory; } @@ -75,6 +79,9 @@ struct NodeTheoryPairHashFunction { * CVC4. */ class TheoryEngine { + + /** Shared terms database can use the internals notify the theories */ + friend class SharedTermsDatabase; /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; @@ -103,21 +110,6 @@ class TheoryEngine { */ const LogicInfo& d_logicInfo; - // NotifyClass: template helper class for Shared Terms Database - class NotifyClass :public SharedTermsDatabase::SharedTermsNotifyClass { - TheoryEngine& d_theoryEngine; - public: - NotifyClass(TheoryEngine& engine): d_theoryEngine(engine) {} - ~NotifyClass() {} - - void notify(TNode literal, TNode original, theory::TheoryId theory) { - d_theoryEngine.propagateSharedLiteral(literal, original, theory); - } - }; - - // Instance of NotifyClass - NotifyClass d_notify; - /** * The database of shared terms. */ @@ -221,11 +213,11 @@ class TheoryEngine { d_engine->conflict(conflictNode, d_theory); } - void propagate(TNode literal) throw(AssertionException) { + bool propagate(TNode literal) throw(AssertionException) { Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; ++ d_statistics.propagations; d_engine->d_outputChannelUsed = true; - d_engine->propagate(literal, d_theory); + return d_engine->propagate(literal, d_theory); } void propagateAsDecision(TNode literal) throw(AssertionException) { @@ -262,28 +254,11 @@ class TheoryEngine { */ context::CDO d_inConflict; - /** - * Explain the equality literals and push all the explaining literals - * into the builder. All the non-equality literals are pushed to the - * builder. - */ - void explainEqualities(theory::TheoryId theoryId, TNode literals, NodeBuilder<>& builder); - - /** - * Same as above, but just for single equalities. - */ - void explainEquality(theory::TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder); - /** * Called by the theories to notify of a conflict. */ void conflict(TNode conflict, theory::TheoryId theoryId); - /** - * Called by shared terms database to notify of a conflict. - */ - void sharedConflict(TNode conflict); - /** * Debugging flag to ensure that shutdown() is called before the * destructor. @@ -310,63 +285,16 @@ class TheoryEngine { d_propEngine->spendResource(); } - struct SharedLiteral { - /** - * The node/theory pair for the assertion. THEORY_LAST indicates this is a SAT - * literal and should be sent to the SAT solver - */ - NodeTheoryPair toAssert; - /** This is the node that we will use to explain it */ - Node toExplain; - - SharedLiteral(TNode assertion, TNode original, theory::TheoryId receivingTheory) - : toAssert(assertion, receivingTheory), - toExplain(original) - { } - }; - - /** - * Map from nodes to theories. - */ - typedef context::CDHashMap SharedLiteralsInMap; - /** - * All shared literals asserted to theory engine. - * Maps from literal to the theory that sent the literal (THEORY_LAST means sent from SAT). + * Mapping of propagations from recievers to senders. */ - SharedLiteralsInMap d_sharedLiteralsIn; - - /** - * Map from literals asserted by theory engine to literal that can explain - */ - typedef context::CDHashMap AssertedLiteralsOutMap; - - /** - * All literals asserted to theories from theory engine. - * Maps from literal/theory pair to literal that can explain this assertion. - */ - AssertedLiteralsOutMap d_assertedLiteralsOut; - - /** - * Shared literals queud up to be asserted to the individual theories. - */ - std::vector d_propagatedSharedLiterals; - - void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory) - { - if (literal.getKind() == kind::CONST_BOOLEAN) { - Assert(!literal.getConst()); - sharedConflict(original); - } - else { - d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory)); - } - } + typedef context::CDHashMap PropagationMap; + PropagationMap d_propagationMap; /** - * Assert the shared literals that are queued up to the theories. + * Timestamp of propagations */ - void outputSharedLiterals(); + context::CDO d_propagationMapTimestamp; /** * Literals that are propagated by the theory. Note that these are TNodes. @@ -395,8 +323,9 @@ class TheoryEngine { /** * Called by the output channel to propagate literals and facts + * @return false if immediate conflict */ - void propagate(TNode literal, theory::TheoryId theory); + bool propagate(TNode literal, theory::TheoryId theory); /** * Internal method to call the propagation routines and collect the @@ -427,55 +356,8 @@ class TheoryEngine { /** * Adds a new lemma, returning its status. */ - theory::LemmaStatus lemma(TNode node, bool negated, bool removable) { - if(Dump.isOn("t-lemmas")) { - Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") - << QueryCommand(node.toExpr()); - } - - // Share with other portfolio threads - if(Options::current()->lemmaOutputChannel != NULL) { - Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr()); - } - - // Remove the ITEs - std::vector additionalLemmas; - IteSkolemMap iteSkolemMap; - additionalLemmas.push_back(node); - RemoveITE::run(additionalLemmas, iteSkolemMap); - additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); - - // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable); - for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { - additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable); - } - - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - if(negated) { - // Can't we just get rid of passing around this 'negated' stuff? - // Is it that hard for the propEngine to figure that out itself? - // (I like the use of triple negation .) --K - additionalLemmas[0] = additionalLemmas[0].notNode(); - negated = false; - } - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - - // assert to decision engine - if(!removable) - d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap); - - // Mark that we added some lemmas - d_lemmasAdded = true; - - // Lemma analysis isn't online yet; this lemma may only live for this - // user level. - return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel()); - } - + theory::LemmaStatus lemma(TNode node, bool negated, bool removable); + /** Time spent in theory combination */ TimerStat d_combineTheoriesTime; @@ -535,6 +417,45 @@ private: */ bool d_inPreregister; + /** + * Did the theories get any new facts since the last time we called + * check() + */ + context::CDO d_factsAsserted; + + /** + * Assert the formula to the given theory. + * @param assertion the assertion to send (not necesserily normalized) + * @param original the assertion as it was sent in from the propagating theory + * @param toTheoryId the theory to assert to + * @param fromTheoryId the theory that sent it + */ + void assertToTheory(TNode assertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); + + /** + * Marks a theory propagation from a theory to a theory where a + * theory could be the THEORY_SAT_SOLVER for literals coming from + * or being propagated to the SAT solver. If the receiving theory + * already recieved the literal, the method returns false, otherwise + * it returns true. + * + * @param assertion the normalized assertion being sent + * @param originalAssertion the actual assertion that was sent + * @param toTheoryId the theory that is on the receiving end + * @param fromTheoryId the theory that sent the assertino + * @return true if a new assertion, false if theory already got it + */ + bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); + + /** + * Computes the explanation by travarsing the propagation graph and + * asking relevant theories to explain the propagations. Initially + * the explanation vector should contain only the element (node, theory) + * where the node is the one to be explained, and the theory is the + * theory that sent the literal. + */ + void getExplanation(std::vector& explanationVector); + public: /** @@ -657,40 +578,14 @@ public: bool properPropagation(TNode lit) const; bool properExplanation(TNode node, TNode expl) const; - enum ExplainTaskKind { - // Literal sent out from the theory engine - SHARED_LITERAL_OUT, - // Explanation produced by a theory - THEORY_EXPLANATION, - // Explanation produced by the shared terms database - SHARED_DATABASE_EXPLANATION - }; - - struct ExplainTask { - Node node; - ExplainTaskKind kind; - theory::TheoryId theory; - ExplainTask(Node n, ExplainTaskKind k, theory::TheoryId tid = theory::THEORY_LAST) : - node(n), kind(k), theory(tid) {} - bool operator == (const ExplainTask& other) const { - return node == other.node && kind == other.kind && theory == other.theory; - } - }; - - struct ExplainTaskHashFunction { - size_t operator () (const ExplainTask& task) const { - size_t hash = 0; - hash = 0x9e3779b9 + NodeHashFunction().operator()(task.node); - hash ^= 0x9e3779b9 + task.kind + (hash << 6) + (hash >> 2); - hash ^= 0x9e3779b9 + task.theory + (hash << 6) + (hash >> 2); - return hash; - } - }; - + /** + * Returns an explanation of the node propagated to the SAT solver. + */ Node getExplanation(TNode node); - Node explain(ExplainTask toExplain); - + /** + * Returns the value of the given node. + */ Node getValue(TNode node); /** @@ -732,6 +627,9 @@ private: /** Prints the assertions to the debug stream */ void printAssertions(const char* tag); + /** Dump the assertions to the dump */ + void dumpAssertions(const char* tag); + /** For preprocessing pass simplifying ITEs */ ITESimplifier d_iteSimplifier; @@ -739,6 +637,7 @@ private: UnconstrainedSimplifier d_unconstrainedSimp; public: + Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector& assertions); diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index aaf47425b..bf1370090 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -78,9 +78,10 @@ public: push(CONFLICT, n); } - void propagate(TNode n) + bool propagate(TNode n) throw(AssertionException) { push(PROPAGATE, n); + return true; } void propagateAsDecision(TNode n) diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 5093e5a7b..4cd54a2bf 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -62,14 +62,14 @@ void EqualityEngine::init() { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); + d_triggerDatabaseAllocatedSize = 100000; + d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize); + addTerm(d_true); addTerm(d_false); d_trueId = getNodeId(d_true); d_falseId = getNodeId(d_false); - - d_triggerDatabaseAllocatedSize = 100000; - d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize); } EqualityEngine::~EqualityEngine() throw(AssertionException) { @@ -114,7 +114,8 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c } void EqualityEngine::enqueue(const MergeCandidate& candidate) { - d_propagationQueue.push(candidate); + Debug("equality") << "EqualityEngine::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl; + d_propagationQueue.push(candidate); } EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality) { @@ -144,7 +145,15 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId if (isEquality && d_isConstant[t1ClassId] && d_isConstant[t2ClassId]) { if (t1ClassId != t2ClassId) { Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl; + Assert(d_nodes[funId].getKind() == kind::EQUAL); enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); + // Also enqueue the symmetric one + TNode eq = d_nodes[funId]; + Node symmetricEq = eq[1].eqNode(eq[0]); + if (hasTerm(symmetricEq)) { + EqualityNodeId symmFunId = getNodeId(symmetricEq); + enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); + } } } } else { @@ -154,8 +163,8 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId } // Add to the use lists - d_equalityNodes[t1ClassId].usedIn(funId, d_useListNodes); - d_equalityNodes[t2ClassId].usedIn(funId, d_useListNodes); + d_equalityNodes[t1].usedIn(funId, d_useListNodes); + d_equalityNodes[t2].usedIn(funId, d_useListNodes); // Return the new id Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl; @@ -238,6 +247,20 @@ void EqualityEngine::addTerm(TNode t) { // We set this here as this only applies to actual terms, not the // intermediate application terms d_isBoolean[result] = true; + } else if (t.isConst()) { + // Non-Boolean constants are trigger terms for all tags + EqualityNodeId tId = getNodeId(t); + d_newSetTags = 0; + d_newSetTriggersSize = THEORY_LAST; + for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) { + d_newSetTags = Theory::setInsert(currentTheory, d_newSetTags); + d_newSetTriggers[currentTheory] = tId; + } + // Add it to the list for backtracking + d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id)); + d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1; + // Mark the the new set as a trigger + d_nodeIndividualTrigger[tId] = newTriggerTermSet(); } propagate(); @@ -319,15 +342,20 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { assertEqualityInternal(eq, d_false, reason); propagate(); assertEqualityInternal(eq[1].eqNode(eq[0]), d_false, reason); - propagate(); + propagate(); if (d_done) { return; } - // If we are adding a disequality, notify of the shared term representatives + // If both have constant representatives, we don't notify anyone EqualityNodeId a = getNodeId(eq[0]); EqualityNodeId b = getNodeId(eq[1]); + if (isConstant(a) && isConstant(b)) { + return; + } + + // If we are adding a disequality, notify of the shared term representatives EqualityNodeId eqId = getNodeId(eq); TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[a]; TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[b]; @@ -356,6 +384,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { d_deducedDisequalityReasons.push_back(EqualityPair(bSharedId, b)); d_deducedDisequalityReasons.push_back(EqualityPair(eqId, d_falseId)); storePropagatedDisequality(d_nodes[aSharedId], d_nodes[bSharedId], 3); + // We notify even if the it's already been sent (they are not // disequal at assertion, and we need to notify for each tag) if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) { @@ -383,7 +412,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl; Assert(triggersFired.empty()); - + ++ d_stats.mergesCount; EqualityNodeId class1Id = class1.getFind(); @@ -391,6 +420,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Check for constant merges bool isConstant = d_isConstant[class1Id]; + Assert(isConstant || !d_isConstant[class2Id]); // Update class2 representative information Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl; @@ -438,13 +468,13 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl; // Go through the uselist and check for congruences - UseListNodeId currentUseId = currentNode.getUseList(); + UseListNodeId currentUseId = currentNode.getUseList(); while (currentUseId != null_uselist_id) { // Get the node of the use list UseListNode& useNode = d_useListNodes[currentUseId]; // Get the function application EqualityNodeId funId = useNode.getApplicationId(); - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl; + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl; const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; // Check if there is an application with find arguments EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); @@ -460,11 +490,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // There is no representative, so we can add one, we remove this when backtracking storeApplicationLookup(funNormalized, funId); // Now, if we're constant and it's an equality, check if the other guy is also a constant - if (isConstant && funNormalized.isEquality) { - if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) { - // both constants - if (funNormalized.a != funNormalized.b) { - enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); + if (funNormalized.isEquality) { + if (d_isConstant[aNormalized] && d_isConstant[bNormalized] && aNormalized != bNormalized) { + Assert(d_nodes[funId].getKind() == kind::EQUAL); + enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); + // Also enqueue the symmetric one + TNode eq = d_nodes[funId]; + Node symmetricEq = eq[1].eqNode(eq[0]); + if (hasTerm(symmetricEq)) { + EqualityNodeId symmFunId = getNodeId(symmetricEq); + enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); } } } @@ -482,6 +517,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Now merge the lists class1.merge(class2); + // Notify of the constants merge + bool constantMerge = false; + if (isConstant && d_isConstant[class2Id]) { + constantMerge = true; + if (d_performNotify) { + if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) { + return false; + } + } + } + // Go through the triggers and store the dis-equalities unsigned i = 0, j = 0; for (; i < triggersFired.size();) { @@ -543,7 +589,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // copy tag1 EqualityNodeId tag1id = d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++]; // since they are both tagged notify of merge - if (d_performNotify) { + if (d_performNotify && !constantMerge) { EqualityNodeId tag2id = class2triggers.triggers[i2++]; if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) { return false; @@ -566,15 +612,6 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } } - // Notify of the constants merge - if (isConstant && d_isConstant[class2Id]) { - if (d_performNotify) { - if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) { - return false; - } - } - } - // Everything fine return true; } @@ -680,12 +717,12 @@ void EqualityEngine::backtrack() { Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl; d_nodeIds.erase(d_nodes[i]); - const FunctionApplication& app = d_applications[i].normalized; + const FunctionApplication& app = d_applications[i].original; if (app.isApplication()) { // Remove b from use-list - getEqualityNode(app.b).removeTopFromUseList(d_useListNodes); + getEqualityNode(app.b).removeTopFromUseList(d_useListNodes); // Remove a from use-list - getEqualityNode(app.a).removeTopFromUseList(d_useListNodes); + getEqualityNode(app.a).removeTopFromUseList(d_useListNodes); } } @@ -818,8 +855,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // Go through the equality edges of this node EqualityEdgeId currentEdge = d_equalityGraph[currentNode]; - Debug("equality") << "EqualityEngine::getExplanation(): edgesId = " << currentEdge << std::endl; - Debug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl; + if (Debug.isOn("equality")) { + Debug("equality") << "EqualityEngine::getExplanation(): edgesId = " << currentEdge << std::endl; + Debug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl; + } while (currentEdge != null_edge) { // Get the edge @@ -871,8 +910,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << push; // Explain why a is a constant + Assert(isConstant(eq.a)); getExplanation(eq.a, getEqualityNode(eq.a).getFind(), equalities); // Explain why b is a constant + Assert(isConstant(eq.b)); getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities); Debug("equality") << pop; @@ -1062,7 +1103,7 @@ void EqualityEngine::propagate() { // Depending on the merge preference (such as size, or being a constant), merge them std::vector triggers; - if (node2.getSize() > node1.getSize() || d_isConstant[t2classId]) { + if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[t2classId]) { Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl; d_assertedEqualities.push_back(Equality(t2classId, t1classId)); if (!merge(node2, node1, triggers)) { @@ -1222,7 +1263,7 @@ size_t EqualityEngine::getSize(TNode t) void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) { - Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; + Debug("equality::trigger") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; Assert(tag != THEORY_LAST); if (d_done) { @@ -1243,12 +1284,71 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // If the term already is in the equivalence class that a tagged representative, just notify if (d_performNotify) { EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag); - if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) { + if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) { d_done = true; } } } else { + // Check for disequalities by going through the equivalence class looking for equalities in the + // uselists that have been asserted to false. All the representatives appearing on the other + // side of such disequalities, that have the tag on, are put in a set. + std::set disequalSet; + EqualityNodeId currentId = classId; + do { + // Current node + EqualityNode& currentNode = getEqualityNode(currentId); + // Go through the uselist and look for disequalities + UseListNodeId currentUseId = currentNode.getUseList(); + while (!d_done && currentUseId != null_uselist_id) { + // Get the normalized equality + UseListNode& useNode = d_useListNodes[currentUseId]; + EqualityNodeId funId = useNode.getApplicationId(); + const FunctionApplication& fun = d_applications[useNode.getApplicationId()].original; + // Check for asserted disequalities + if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { + // Get the other equality member + EqualityNodeId toCompare = fun.b; + if (toCompare == currentId) { + toCompare = fun.a; + } + // Representative of the other member + EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind(); + Assert(toCompareRep != classId); + // Get the trigger set + TriggerTermSetRef toCompareTriggerSetRef = d_nodeIndividualTrigger[toCompareRep]; + // Only notify if we're not both constants + if ((!d_isConstant[classId] || !d_isConstant[toCompareRep]) && toCompareTriggerSetRef != null_set_id) { + TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef); + if (Theory::setContains(tag, toCompareTriggerSet.tags)) { + // Get the tag representative + EqualityNodeId tagRep = toCompareTriggerSet.getTrigger(tag); + // Propagate the disequality if not already done + if (!disequalSet.count(tagRep) && d_performNotify) { + // Mark as propagated + disequalSet.insert(tagRep); + // Store the propagation + d_deducedDisequalityReasons.push_back(EqualityPair(eqNodeId, currentId)); + d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep)); + d_deducedDisequalityReasons.push_back(EqualityPair(funId, d_falseId)); + storePropagatedDisequality(t, d_nodes[tagRep], 3); + // We don't check if it's been propagated already, as we need one per tag + if (d_performNotify) { + if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[tagRep], false)) { + d_done = true; + } + } + } + } + } + } + // Go to the next one in the use list + currentUseId = useNode.getNext(); + } + // Next in equivalence class + currentId = currentNode.getNext(); + } while (!d_done && currentId != classId); + // Setup the data for the new set if (triggerSetRef != null_set_id) { // Get the existing set @@ -1322,7 +1422,7 @@ void EqualityEngine::getUseListTerms(TNode t, std::set& output) { // Get the current node EqualityNode& currentNode = getEqualityNode(currentId); // Go through the use-list - UseListNodeId currentUseId = currentNode.getUseList(); + UseListNodeId currentUseId = currentNode.getUseList(); while (currentUseId != null_uselist_id) { // Get the node of the use list UseListNode& useNode = d_useListNodes[currentUseId]; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 5ff8ee4dc..f40c79df3 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -344,6 +344,13 @@ private: */ std::vector d_isConstant; + /** + * Returns true if it's a constant + */ + bool isConstant(EqualityNodeId id) const { + return d_isConstant[getEqualityNode(id).getFind()]; + } + /** * Map from ids to wheather they are Boolean. */ diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 0baf70fcf..056ee0b84 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -94,8 +94,9 @@ struct MergeCandidate { EqualityNodeId t1Id, t2Id; MergeReasonType type; TNode reason; - MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason): - t1Id(x), t2Id(y), type(type), reason(reason) {} + MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason) + : t1Id(x), t2Id(y), type(type), reason(reason) + {} }; /** @@ -145,15 +146,6 @@ public: } }; -/** Main types of uselists */ -enum UseListType { - /** Use list of functions where the term appears in */ - USE_LIST_FUNCTIONS, - /** Use list of asserted disequalities */ - USE_LIST_DISEQUALITIES -}; - - /** * Main class for representing nodes in the equivalence class. The * nodes are a circular list, with the representative carrying the @@ -178,9 +170,6 @@ private: /** The use list of this node */ UseListNodeId d_useList; - /** The list of asserted disequalities that this node appears in */ - UseListNodeId d_diseqList; - public: /** @@ -191,15 +180,13 @@ public: , d_findId(nodeId) , d_nextId(nodeId) , d_useList(null_uselist_id) - , d_diseqList(null_uselist_id) {} /** * Returns the requested uselist. */ - template UseListNodeId getUseList() const { - return type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList; + return d_useList; } /** @@ -244,22 +231,20 @@ public: * Note that this node is used in a function application funId, or * a negatively asserted equality (dis-equality) with funId. */ - template + template void usedIn(EqualityNodeId funId, memory_class& memory) { - UseListNodeId& useList = type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList; UseListNodeId newUseId = memory.size(); - memory.push_back(UseListNode(funId, useList)); - useList = newUseId; + memory.push_back(UseListNode(funId, d_useList)); + d_useList = newUseId; } /** * For backtracking: remove the first element from the uselist and pop the memory. */ - template + template void removeTopFromUseList(memory_class& memory) { - UseListNodeId& useList = type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList; - Assert ((int) useList == (int)memory.size() - 1); - useList = memory.back().getNext(); + Assert ((int) d_useList == (int)memory.size() - 1); + d_useList = memory.back().getNext(); memory.pop_back(); } }; @@ -288,7 +273,7 @@ struct FunctionApplication { FunctionApplication(bool isEquality = false, EqualityNodeId a = null_id, EqualityNodeId b = null_id) : isEquality(isEquality), a(a), b(b) {} bool operator == (const FunctionApplication& other) const { - return a == other.a && b == other.b; + return isEquality == other.isEquality && a == other.a && b == other.b; } bool isApplication() const { return a != null_id && b != null_id; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index ae8bdc8da..7583f8ee7 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -70,16 +70,6 @@ void TheoryUF::check(Effort level) { Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl; - // If the assertion doesn't have a literal, it's a shared equality, so we set it up - if (!assertion.isPreregistered) { - Debug("uf") << "TheoryUF::check(): shared equality, setting up " << fact << std::endl; - if (fact.getKind() == kind::NOT) { - preRegisterTerm(fact[0]); - } else { - preRegisterTerm(fact); - } - } - // Do the work bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; @@ -90,31 +80,8 @@ void TheoryUF::check(Effort level) { } } - // If in conflict, output the conflict - if (d_conflict) { - Debug("uf") << "TheoryUF::check(): conflict " << d_conflictNode << std::endl; - d_out->conflict(d_conflictNode); - } - - // Otherwise we propagate in order to detect a weird conflict like - // p, x = y - // p -> f(x) != f(y) -- f(x) = f(y) gets added to the propagation list at preregistration time - // but when f(x) != f(y) is deduced by the sat solver, so it's asserted, and we don't detect the conflict - // until we go through the propagation list - propagate(level); }/* TheoryUF::check() */ -void TheoryUF::propagate(Effort level) { - Debug("uf") << "TheoryUF::propagate()" << std::endl; - if (!d_conflict) { - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { - TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl; - d_out->propagate(literal); - } - } -}/* TheoryUF::propagate(Effort) */ - void TheoryUF::preRegisterTerm(TNode node) { Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl; @@ -143,37 +110,18 @@ void TheoryUF::preRegisterTerm(TNode node) { }/* TheoryUF::preRegisterTerm() */ bool TheoryUF::propagate(TNode literal) { - Debug("uf") << "TheoryUF::propagate(" << literal << ")" << std::endl; - + Debug("uf::propagate") << "TheoryUF::propagate(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("uf") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl; + Debug("uf::propagate") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl; return false; } - - // See if the literal has been asserted already - Node normalized = Rewriter::rewrite(literal); - - // If asserted and is false, we're done or in conflict - // Note that even trivial equalities have a SAT value (i.e. 1 = 2 -> false) - bool satValue = false; - if (d_valuation.hasSatValue(normalized, satValue) && !satValue) { - Debug("uf") << "TheoryUF::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; - std::vector assumptions; - Node negatedLiteral; - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - return false; + // Propagate out + bool ok = d_out->propagate(literal); + if (!ok) { + d_conflict = true; } - - // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("uf") << "TheoryUF::propagate(" << literal << ") => enqueuing for propagation" << std::endl; - d_literalsToPropagate.push_back(literal); - - return true; + return ok; }/* TheoryUF::propagate(TNode) */ void TheoryUF::explain(TNode literal, std::vector& assumptions) { @@ -437,3 +385,13 @@ void TheoryUF::computeCareGraph() { } } }/* TheoryUF::computeCareGraph() */ + +void TheoryUF::conflict(TNode a, TNode b) { + if (Theory::theoryOf(a) == theory::THEORY_BOOL) { + d_conflictNode = explain(a.iffNode(b)); + } else { + d_conflictNode = explain(a.eqNode(b)); + } + d_out->conflict(d_conflictNode); + d_conflict = true; +} diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 1dfcb86f0..0d35d57d8 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -55,7 +55,7 @@ public: } bool eqNotifyTriggerPredicate(TNode predicate, bool value) { - Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl; + Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { return d_uf.propagate(predicate); } else { @@ -64,7 +64,7 @@ public: } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << std::endl; + Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; if (value) { return d_uf.propagate(t1.eqNode(t2)); } else { @@ -73,12 +73,9 @@ public: } bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; - if (Theory::theoryOf(t1) == THEORY_BOOL) { - return d_uf.propagate(t1.iffNode(t2)); - } else { - return d_uf.propagate(t1.eqNode(t2)); - } + Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + d_uf.conflict(t1, t2); + return false; } }; @@ -119,13 +116,15 @@ private: /** Symmetry analyzer */ SymmetryBreaker d_symb; + /** Conflict when merging two constants */ + void conflict(TNode a, TNode b); + public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); void check(Effort); - void propagate(Effort); void preRegisterTerm(TNode term); Node explain(TNode n); @@ -135,6 +134,8 @@ public: void addSharedTerm(TNode n); void computeCareGraph(); + void propagate(Effort effort) {} + EqualityStatus getEqualityStatus(TNode a, TNode b); std::string identify() const { diff --git a/src/util/options.cpp b/src/util/options.cpp index e9ef7d959..e5d91e0d8 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -699,7 +699,8 @@ throw(OptionException) { } else if(!strcmp(optarg, "t-conflicts") || !strcmp(optarg, "t-lemmas") || !strcmp(optarg, "t-explanations") || - !strcmp(optarg, "bv-rewrites")) { + !strcmp(optarg, "bv-rewrites") || + !strcmp(optarg, "theory::fullcheck")) { // These are "non-state-dumping" modes. If state (SAT decisions, // propagations, etc.) is dumped, it will interfere with the validity // of these generated queries. diff --git a/test/regress/regress0/aufbv/Makefile b/test/regress/regress0/aufbv/Makefile new file mode 100644 index 000000000..7dd17882f --- /dev/null +++ b/test/regress/regress0/aufbv/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/aufbv + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index f9ec6b474..9b9820258 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -9,7 +9,10 @@ endif # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - bug00.smt + bug00.smt \ + bug338.smt2 \ + try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \ + wchains010ue.delta01.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/aufbv/no_init_multi_delete14.smt b/test/regress/regress0/aufbv/no_init_multi_delete14.smt new file mode 100644 index 000000000..06071cd32 --- /dev/null +++ b/test/regress/regress0/aufbv/no_init_multi_delete14.smt @@ -0,0 +1,670 @@ +(benchmark no_init_multi_delete14.smt + :source { +The benchmarks come from Bounded Model Checking of software. +Contributed by Lorenzo Platania (c1009@unige.it). +} + :status unknown + :difficulty { unknown } + :category { industrial } + :logic QF_AUFBV + :extrafuns ((main_0_head_0 BitVec[32])) + :extrafuns ((main_0_head_1 BitVec[32])) + :assumption +(= main_0_head_1 bv0[32]) + :extrafuns ((arr_val_0 Array[32:32])) + :extrafuns ((arr_val_1 Array[32:32])) + :assumption +(= arr_val_1 (store arr_val_0 main_0_head_1 bv0[32])) + :extrafuns ((arr_next_0 Array[32:32])) + :extrafuns ((arr_next_1 Array[32:32])) + :assumption +(= arr_next_1 (store arr_next_0 main_0_head_1 (bvneg bv1[32]))) + :extrafuns ((main_0_curr_0 BitVec[32])) + :extrafuns ((main_0_curr_1 BitVec[32])) + :assumption +(= main_0_curr_1 main_0_head_1) + :extrafuns ((main_0_i_0 BitVec[32])) + :extrafuns ((main_0_i_1 BitVec[32])) + :assumption +(= main_0_i_1 bv1[32]) + :extrafuns ((main_0_tmp_0 BitVec[32])) + :extrafuns ((main_0_tmp_1 BitVec[32])) + :assumption +(= main_0_tmp_1 (ite (bvult main_0_i_1 bv13[32]) bv1[32] main_0_tmp_0)) + :extrafuns ((arr_val_2 Array[32:32])) + :assumption +(= arr_val_2 (ite (bvult main_0_i_1 bv13[32]) (store arr_val_1 main_0_tmp_1 main_0_i_1) arr_val_1)) + :extrafuns ((arr_next_2 Array[32:32])) + :assumption +(= arr_next_2 (ite (bvult main_0_i_1 bv13[32]) (store arr_next_1 main_0_curr_1 main_0_tmp_1) arr_next_1)) + :extrafuns ((main_0_curr_2 BitVec[32])) + :assumption +(= main_0_curr_2 (ite (bvult main_0_i_1 bv13[32]) (select arr_next_2 main_0_curr_1) main_0_curr_1)) + :extrafuns ((arr_next_3 Array[32:32])) + :assumption +(= arr_next_3 (ite (bvult main_0_i_1 bv13[32]) (store arr_next_2 main_0_tmp_1 (bvneg bv1[32])) arr_next_2)) + :extrafuns ((main_0_temp_i_0 BitVec[32])) + :extrafuns ((main_0_temp_i_1 BitVec[32])) + :assumption +(= main_0_temp_i_1 (ite (bvult main_0_i_1 bv13[32]) main_0_i_1 main_0_temp_i_0)) + :extrafuns ((main_0_i_2 BitVec[32])) + :assumption +(= main_0_i_2 (ite (bvult main_0_i_1 bv13[32]) (bvadd main_0_i_1 bv1[32]) main_0_i_1)) + :extrafuns ((main_0_tmp_2 BitVec[32])) + :assumption +(= main_0_tmp_2 (ite (bvult main_0_i_2 bv13[32]) bv2[32] main_0_tmp_1)) + :extrafuns ((arr_val_3 Array[32:32])) + :assumption +(= arr_val_3 (ite (bvult main_0_i_2 bv13[32]) (store arr_val_2 main_0_tmp_2 main_0_i_2) arr_val_2)) + :extrafuns ((arr_next_4 Array[32:32])) + :assumption +(= arr_next_4 (ite (bvult main_0_i_2 bv13[32]) (store arr_next_3 main_0_curr_2 main_0_tmp_2) arr_next_3)) + :extrafuns ((main_0_curr_3 BitVec[32])) + :assumption +(= main_0_curr_3 (ite (bvult main_0_i_2 bv13[32]) (select arr_next_4 main_0_curr_2) main_0_curr_2)) + :extrafuns ((arr_next_5 Array[32:32])) + :assumption +(= arr_next_5 (ite (bvult main_0_i_2 bv13[32]) (store arr_next_4 main_0_tmp_2 (bvneg bv1[32])) arr_next_4)) + :extrafuns ((main_0_temp_i_2 BitVec[32])) + :assumption +(= main_0_temp_i_2 (ite (bvult main_0_i_2 bv13[32]) main_0_i_2 main_0_temp_i_1)) + :extrafuns ((main_0_i_3 BitVec[32])) + :assumption +(= main_0_i_3 (ite (bvult main_0_i_2 bv13[32]) (bvadd main_0_i_2 bv1[32]) main_0_i_2)) + :extrafuns ((main_0_tmp_3 BitVec[32])) + :assumption +(= main_0_tmp_3 (ite (bvult main_0_i_3 bv13[32]) bv3[32] main_0_tmp_2)) + :extrafuns ((arr_val_4 Array[32:32])) + :assumption +(= arr_val_4 (ite (bvult main_0_i_3 bv13[32]) (store arr_val_3 main_0_tmp_3 main_0_i_3) arr_val_3)) + :extrafuns ((arr_next_6 Array[32:32])) + :assumption +(= arr_next_6 (ite (bvult main_0_i_3 bv13[32]) (store arr_next_5 main_0_curr_3 main_0_tmp_3) arr_next_5)) + :extrafuns ((main_0_curr_4 BitVec[32])) + :assumption +(= main_0_curr_4 (ite (bvult main_0_i_3 bv13[32]) (select arr_next_6 main_0_curr_3) main_0_curr_3)) + :extrafuns ((arr_next_7 Array[32:32])) + :assumption +(= arr_next_7 (ite (bvult main_0_i_3 bv13[32]) (store arr_next_6 main_0_tmp_3 (bvneg bv1[32])) arr_next_6)) + :extrafuns ((main_0_temp_i_3 BitVec[32])) + :assumption +(= main_0_temp_i_3 (ite (bvult main_0_i_3 bv13[32]) main_0_i_3 main_0_temp_i_2)) + :extrafuns ((main_0_i_4 BitVec[32])) + :assumption +(= main_0_i_4 (ite (bvult main_0_i_3 bv13[32]) (bvadd main_0_i_3 bv1[32]) main_0_i_3)) + :extrafuns ((main_0_tmp_4 BitVec[32])) + :assumption +(= main_0_tmp_4 (ite (bvult main_0_i_4 bv13[32]) bv4[32] main_0_tmp_3)) + :extrafuns ((arr_val_5 Array[32:32])) + :assumption +(= arr_val_5 (ite (bvult main_0_i_4 bv13[32]) (store arr_val_4 main_0_tmp_4 main_0_i_4) arr_val_4)) + :extrafuns ((arr_next_8 Array[32:32])) + :assumption +(= arr_next_8 (ite (bvult main_0_i_4 bv13[32]) (store arr_next_7 main_0_curr_4 main_0_tmp_4) arr_next_7)) + :extrafuns ((main_0_curr_5 BitVec[32])) + :assumption +(= main_0_curr_5 (ite (bvult main_0_i_4 bv13[32]) (select arr_next_8 main_0_curr_4) main_0_curr_4)) + :extrafuns ((arr_next_9 Array[32:32])) + :assumption +(= arr_next_9 (ite (bvult main_0_i_4 bv13[32]) (store arr_next_8 main_0_tmp_4 (bvneg bv1[32])) arr_next_8)) + :extrafuns ((main_0_temp_i_4 BitVec[32])) + :assumption +(= main_0_temp_i_4 (ite (bvult main_0_i_4 bv13[32]) main_0_i_4 main_0_temp_i_3)) + :extrafuns ((main_0_i_5 BitVec[32])) + :assumption +(= main_0_i_5 (ite (bvult main_0_i_4 bv13[32]) (bvadd main_0_i_4 bv1[32]) main_0_i_4)) + :extrafuns ((main_0_tmp_5 BitVec[32])) + :assumption +(= main_0_tmp_5 (ite (bvult main_0_i_5 bv13[32]) bv5[32] main_0_tmp_4)) + :extrafuns ((arr_val_6 Array[32:32])) + :assumption +(= arr_val_6 (ite (bvult main_0_i_5 bv13[32]) (store arr_val_5 main_0_tmp_5 main_0_i_5) arr_val_5)) + :extrafuns ((arr_next_10 Array[32:32])) + :assumption +(= arr_next_10 (ite (bvult main_0_i_5 bv13[32]) (store arr_next_9 main_0_curr_5 main_0_tmp_5) arr_next_9)) + :extrafuns ((main_0_curr_6 BitVec[32])) + :assumption +(= main_0_curr_6 (ite (bvult main_0_i_5 bv13[32]) (select arr_next_10 main_0_curr_5) main_0_curr_5)) + :extrafuns ((arr_next_11 Array[32:32])) + :assumption +(= arr_next_11 (ite (bvult main_0_i_5 bv13[32]) (store arr_next_10 main_0_tmp_5 (bvneg bv1[32])) arr_next_10)) + :extrafuns ((main_0_temp_i_5 BitVec[32])) + :assumption +(= main_0_temp_i_5 (ite (bvult main_0_i_5 bv13[32]) main_0_i_5 main_0_temp_i_4)) + :extrafuns ((main_0_i_6 BitVec[32])) + :assumption +(= main_0_i_6 (ite (bvult main_0_i_5 bv13[32]) (bvadd main_0_i_5 bv1[32]) main_0_i_5)) + :extrafuns ((main_0_tmp_6 BitVec[32])) + :assumption +(= main_0_tmp_6 (ite (bvult main_0_i_6 bv13[32]) bv6[32] main_0_tmp_5)) + :extrafuns ((arr_val_7 Array[32:32])) + :assumption +(= arr_val_7 (ite (bvult main_0_i_6 bv13[32]) (store arr_val_6 main_0_tmp_6 main_0_i_6) arr_val_6)) + :extrafuns ((arr_next_12 Array[32:32])) + :assumption +(= arr_next_12 (ite (bvult main_0_i_6 bv13[32]) (store arr_next_11 main_0_curr_6 main_0_tmp_6) arr_next_11)) + :extrafuns ((main_0_curr_7 BitVec[32])) + :assumption +(= main_0_curr_7 (ite (bvult main_0_i_6 bv13[32]) (select arr_next_12 main_0_curr_6) main_0_curr_6)) + :extrafuns ((arr_next_13 Array[32:32])) + :assumption +(= arr_next_13 (ite (bvult main_0_i_6 bv13[32]) (store arr_next_12 main_0_tmp_6 (bvneg bv1[32])) arr_next_12)) + :extrafuns ((main_0_temp_i_6 BitVec[32])) + :assumption +(= main_0_temp_i_6 (ite (bvult main_0_i_6 bv13[32]) main_0_i_6 main_0_temp_i_5)) + :extrafuns ((main_0_i_7 BitVec[32])) + :assumption +(= main_0_i_7 (ite (bvult main_0_i_6 bv13[32]) (bvadd main_0_i_6 bv1[32]) main_0_i_6)) + :extrafuns ((main_0_tmp_7 BitVec[32])) + :assumption +(= main_0_tmp_7 (ite (bvult main_0_i_7 bv13[32]) bv7[32] main_0_tmp_6)) + :extrafuns ((arr_val_8 Array[32:32])) + :assumption +(= arr_val_8 (ite (bvult main_0_i_7 bv13[32]) (store arr_val_7 main_0_tmp_7 main_0_i_7) arr_val_7)) + :extrafuns ((arr_next_14 Array[32:32])) + :assumption +(= arr_next_14 (ite (bvult main_0_i_7 bv13[32]) (store arr_next_13 main_0_curr_7 main_0_tmp_7) arr_next_13)) + :extrafuns ((main_0_curr_8 BitVec[32])) + :assumption +(= main_0_curr_8 (ite (bvult main_0_i_7 bv13[32]) (select arr_next_14 main_0_curr_7) main_0_curr_7)) + :extrafuns ((arr_next_15 Array[32:32])) + :assumption +(= arr_next_15 (ite (bvult main_0_i_7 bv13[32]) (store arr_next_14 main_0_tmp_7 (bvneg bv1[32])) arr_next_14)) + :extrafuns ((main_0_temp_i_7 BitVec[32])) + :assumption +(= main_0_temp_i_7 (ite (bvult main_0_i_7 bv13[32]) main_0_i_7 main_0_temp_i_6)) + :extrafuns ((main_0_i_8 BitVec[32])) + :assumption +(= main_0_i_8 (ite (bvult main_0_i_7 bv13[32]) (bvadd main_0_i_7 bv1[32]) main_0_i_7)) + :extrafuns ((main_0_tmp_8 BitVec[32])) + :assumption +(= main_0_tmp_8 (ite (bvult main_0_i_8 bv13[32]) bv8[32] main_0_tmp_7)) + :extrafuns ((arr_val_9 Array[32:32])) + :assumption +(= arr_val_9 (ite (bvult main_0_i_8 bv13[32]) (store arr_val_8 main_0_tmp_8 main_0_i_8) arr_val_8)) + :extrafuns ((arr_next_16 Array[32:32])) + :assumption +(= arr_next_16 (ite (bvult main_0_i_8 bv13[32]) (store arr_next_15 main_0_curr_8 main_0_tmp_8) arr_next_15)) + :extrafuns ((main_0_curr_9 BitVec[32])) + :assumption +(= main_0_curr_9 (ite (bvult main_0_i_8 bv13[32]) (select arr_next_16 main_0_curr_8) main_0_curr_8)) + :extrafuns ((arr_next_17 Array[32:32])) + :assumption +(= arr_next_17 (ite (bvult main_0_i_8 bv13[32]) (store arr_next_16 main_0_tmp_8 (bvneg bv1[32])) arr_next_16)) + :extrafuns ((main_0_temp_i_8 BitVec[32])) + :assumption +(= main_0_temp_i_8 (ite (bvult main_0_i_8 bv13[32]) main_0_i_8 main_0_temp_i_7)) + :extrafuns ((main_0_i_9 BitVec[32])) + :assumption +(= main_0_i_9 (ite (bvult main_0_i_8 bv13[32]) (bvadd main_0_i_8 bv1[32]) main_0_i_8)) + :extrafuns ((main_0_tmp_9 BitVec[32])) + :assumption +(= main_0_tmp_9 (ite (bvult main_0_i_9 bv13[32]) bv9[32] main_0_tmp_8)) + :extrafuns ((arr_val_10 Array[32:32])) + :assumption +(= arr_val_10 (ite (bvult main_0_i_9 bv13[32]) (store arr_val_9 main_0_tmp_9 main_0_i_9) arr_val_9)) + :extrafuns ((arr_next_18 Array[32:32])) + :assumption +(= arr_next_18 (ite (bvult main_0_i_9 bv13[32]) (store arr_next_17 main_0_curr_9 main_0_tmp_9) arr_next_17)) + :extrafuns ((main_0_curr_10 BitVec[32])) + :assumption +(= main_0_curr_10 (ite (bvult main_0_i_9 bv13[32]) (select arr_next_18 main_0_curr_9) main_0_curr_9)) + :extrafuns ((arr_next_19 Array[32:32])) + :assumption +(= arr_next_19 (ite (bvult main_0_i_9 bv13[32]) (store arr_next_18 main_0_tmp_9 (bvneg bv1[32])) arr_next_18)) + :extrafuns ((main_0_temp_i_9 BitVec[32])) + :assumption +(= main_0_temp_i_9 (ite (bvult main_0_i_9 bv13[32]) main_0_i_9 main_0_temp_i_8)) + :extrafuns ((main_0_i_10 BitVec[32])) + :assumption +(= main_0_i_10 (ite (bvult main_0_i_9 bv13[32]) (bvadd main_0_i_9 bv1[32]) main_0_i_9)) + :extrafuns ((main_0_tmp_10 BitVec[32])) + :assumption +(= main_0_tmp_10 (ite (bvult main_0_i_10 bv13[32]) bv10[32] main_0_tmp_9)) + :extrafuns ((arr_val_11 Array[32:32])) + :assumption +(= arr_val_11 (ite (bvult main_0_i_10 bv13[32]) (store arr_val_10 main_0_tmp_10 main_0_i_10) arr_val_10)) + :extrafuns ((arr_next_20 Array[32:32])) + :assumption +(= arr_next_20 (ite (bvult main_0_i_10 bv13[32]) (store arr_next_19 main_0_curr_10 main_0_tmp_10) arr_next_19)) + :extrafuns ((main_0_curr_11 BitVec[32])) + :assumption +(= main_0_curr_11 (ite (bvult main_0_i_10 bv13[32]) (select arr_next_20 main_0_curr_10) main_0_curr_10)) + :extrafuns ((arr_next_21 Array[32:32])) + :assumption +(= arr_next_21 (ite (bvult main_0_i_10 bv13[32]) (store arr_next_20 main_0_tmp_10 (bvneg bv1[32])) arr_next_20)) + :extrafuns ((main_0_temp_i_10 BitVec[32])) + :assumption +(= main_0_temp_i_10 (ite (bvult main_0_i_10 bv13[32]) main_0_i_10 main_0_temp_i_9)) + :extrafuns ((main_0_i_11 BitVec[32])) + :assumption +(= main_0_i_11 (ite (bvult main_0_i_10 bv13[32]) (bvadd main_0_i_10 bv1[32]) main_0_i_10)) + :extrafuns ((main_0_tmp_11 BitVec[32])) + :assumption +(= main_0_tmp_11 (ite (bvult main_0_i_11 bv13[32]) bv11[32] main_0_tmp_10)) + :extrafuns ((arr_val_12 Array[32:32])) + :assumption +(= arr_val_12 (ite (bvult main_0_i_11 bv13[32]) (store arr_val_11 main_0_tmp_11 main_0_i_11) arr_val_11)) + :extrafuns ((arr_next_22 Array[32:32])) + :assumption +(= arr_next_22 (ite (bvult main_0_i_11 bv13[32]) (store arr_next_21 main_0_curr_11 main_0_tmp_11) arr_next_21)) + :extrafuns ((main_0_curr_12 BitVec[32])) + :assumption +(= main_0_curr_12 (ite (bvult main_0_i_11 bv13[32]) (select arr_next_22 main_0_curr_11) main_0_curr_11)) + :extrafuns ((arr_next_23 Array[32:32])) + :assumption +(= arr_next_23 (ite (bvult main_0_i_11 bv13[32]) (store arr_next_22 main_0_tmp_11 (bvneg bv1[32])) arr_next_22)) + :extrafuns ((main_0_temp_i_11 BitVec[32])) + :assumption +(= main_0_temp_i_11 (ite (bvult main_0_i_11 bv13[32]) main_0_i_11 main_0_temp_i_10)) + :extrafuns ((main_0_i_12 BitVec[32])) + :assumption +(= main_0_i_12 (ite (bvult main_0_i_11 bv13[32]) (bvadd main_0_i_11 bv1[32]) main_0_i_11)) + :extrafuns ((main_0_tmp_12 BitVec[32])) + :assumption +(= main_0_tmp_12 (ite (bvult main_0_i_12 bv13[32]) bv12[32] main_0_tmp_11)) + :extrafuns ((arr_val_13 Array[32:32])) + :assumption +(= arr_val_13 (ite (bvult main_0_i_12 bv13[32]) (store arr_val_12 main_0_tmp_12 main_0_i_12) arr_val_12)) + :extrafuns ((arr_next_24 Array[32:32])) + :assumption +(= arr_next_24 (ite (bvult main_0_i_12 bv13[32]) (store arr_next_23 main_0_curr_12 main_0_tmp_12) arr_next_23)) + :extrafuns ((main_0_curr_13 BitVec[32])) + :assumption +(= main_0_curr_13 (ite (bvult main_0_i_12 bv13[32]) (select arr_next_24 main_0_curr_12) main_0_curr_12)) + :extrafuns ((arr_next_25 Array[32:32])) + :assumption +(= arr_next_25 (ite (bvult main_0_i_12 bv13[32]) (store arr_next_24 main_0_tmp_12 (bvneg bv1[32])) arr_next_24)) + :extrafuns ((main_0_temp_i_12 BitVec[32])) + :assumption +(= main_0_temp_i_12 (ite (bvult main_0_i_12 bv13[32]) main_0_i_12 main_0_temp_i_11)) + :extrafuns ((main_0_i_13 BitVec[32])) + :assumption +(= main_0_i_13 (ite (bvult main_0_i_12 bv13[32]) (bvadd main_0_i_12 bv1[32]) main_0_i_12)) + :extrafuns ((main_0_tmp_13 BitVec[32])) + :assumption +(= main_0_tmp_13 (ite (bvult main_0_i_13 bv13[32]) bv13[32] main_0_tmp_12)) + :extrafuns ((arr_val_14 Array[32:32])) + :assumption +(= arr_val_14 (ite (bvult main_0_i_13 bv13[32]) (store arr_val_13 main_0_tmp_13 main_0_i_13) arr_val_13)) + :extrafuns ((arr_next_26 Array[32:32])) + :assumption +(= arr_next_26 (ite (bvult main_0_i_13 bv13[32]) (store arr_next_25 main_0_curr_13 main_0_tmp_13) arr_next_25)) + :extrafuns ((main_0_curr_14 BitVec[32])) + :assumption +(= main_0_curr_14 (ite (bvult main_0_i_13 bv13[32]) (select arr_next_26 main_0_curr_13) main_0_curr_13)) + :extrafuns ((arr_next_27 Array[32:32])) + :assumption +(= arr_next_27 (ite (bvult main_0_i_13 bv13[32]) (store arr_next_26 main_0_tmp_13 (bvneg bv1[32])) arr_next_26)) + :extrafuns ((main_0_temp_i_13 BitVec[32])) + :assumption +(= main_0_temp_i_13 (ite (bvult main_0_i_13 bv13[32]) main_0_i_13 main_0_temp_i_12)) + :extrafuns ((main_0_i_14 BitVec[32])) + :assumption +(= main_0_i_14 (ite (bvult main_0_i_13 bv13[32]) (bvadd main_0_i_13 bv1[32]) main_0_i_13)) + :extrafuns ((main_0_tmp_14 BitVec[32])) + :assumption +(= main_0_tmp_14 (ite (bvult main_0_i_14 bv13[32]) bv14[32] main_0_tmp_13)) + :extrafuns ((arr_val_15 Array[32:32])) + :assumption +(= arr_val_15 (ite (bvult main_0_i_14 bv13[32]) (store arr_val_14 main_0_tmp_14 main_0_i_14) arr_val_14)) + :extrafuns ((arr_next_28 Array[32:32])) + :assumption +(= arr_next_28 (ite (bvult main_0_i_14 bv13[32]) (store arr_next_27 main_0_curr_14 main_0_tmp_14) arr_next_27)) + :extrafuns ((main_0_curr_15 BitVec[32])) + :assumption +(= main_0_curr_15 (ite (bvult main_0_i_14 bv13[32]) (select arr_next_28 main_0_curr_14) main_0_curr_14)) + :extrafuns ((arr_next_29 Array[32:32])) + :assumption +(= arr_next_29 (ite (bvult main_0_i_14 bv13[32]) (store arr_next_28 main_0_tmp_14 (bvneg bv1[32])) arr_next_28)) + :extrafuns ((main_0_temp_i_14 BitVec[32])) + :assumption +(= main_0_temp_i_14 (ite (bvult main_0_i_14 bv13[32]) main_0_i_14 main_0_temp_i_13)) + :extrafuns ((main_0_i_15 BitVec[32])) + :assumption +(= main_0_i_15 (ite (bvult main_0_i_14 bv13[32]) (bvadd main_0_i_14 bv1[32]) main_0_i_14)) + :extrafuns ((undefInt_1 BitVec[32])) + :extrafuns ((delete_0_val_0 BitVec[32])) + :extrafuns ((delete_0_val_1 BitVec[32])) + :assumption +(= delete_0_val_1 undefInt_1) + :extrafuns ((delete_0_list_0 BitVec[32])) + :extrafuns ((delete_0_list_1 BitVec[32])) + :assumption +(= delete_0_list_1 main_0_head_1) + :extrafuns ((delete_0_head_0 BitVec[32])) + :extrafuns ((delete_0_head_1 BitVec[32])) + :assumption +(= delete_0_head_1 delete_0_list_1) + :extrafuns ((delete_0_head_2 BitVec[32])) + :assumption +(let (?cvc_0 (select arr_next_29 delete_0_head_1)) (= delete_0_head_2 (ite (and (= (select arr_val_15 delete_0_head_1) delete_0_val_1) (not (= ?cvc_0 (bvneg bv1[32])))) ?cvc_0 delete_0_head_1))) + :extrafuns ((delete_0_head_3 BitVec[32])) + :assumption +(= delete_0_head_3 (ite (and (= (select arr_val_15 delete_0_head_2) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_2) delete_0_head_2)) + :extrafuns ((delete_0_head_4 BitVec[32])) + :assumption +(= delete_0_head_4 (ite (and (= (select arr_val_15 delete_0_head_3) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_3) delete_0_head_3)) + :extrafuns ((delete_0_head_5 BitVec[32])) + :assumption +(= delete_0_head_5 (ite (and (= (select arr_val_15 delete_0_head_4) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_4) delete_0_head_4)) + :extrafuns ((delete_0_head_6 BitVec[32])) + :assumption +(= delete_0_head_6 (ite (and (= (select arr_val_15 delete_0_head_5) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_5) delete_0_head_5)) + :extrafuns ((delete_0_head_7 BitVec[32])) + :assumption +(= delete_0_head_7 (ite (and (= (select arr_val_15 delete_0_head_6) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_6) delete_0_head_6)) + :extrafuns ((delete_0_head_8 BitVec[32])) + :assumption +(= delete_0_head_8 (ite (and (= (select arr_val_15 delete_0_head_7) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_7) delete_0_head_7)) + :extrafuns ((delete_0_head_9 BitVec[32])) + :assumption +(= delete_0_head_9 (ite (and (= (select arr_val_15 delete_0_head_8) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_8) delete_0_head_8)) + :extrafuns ((delete_0_head_10 BitVec[32])) + :assumption +(= delete_0_head_10 (ite (and (= (select arr_val_15 delete_0_head_9) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_9) delete_0_head_9)) + :extrafuns ((delete_0_head_11 BitVec[32])) + :assumption +(= delete_0_head_11 (ite (and (= (select arr_val_15 delete_0_head_10) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_10) delete_0_head_10)) + :extrafuns ((delete_0_head_12 BitVec[32])) + :assumption +(= delete_0_head_12 (ite (and (= (select arr_val_15 delete_0_head_11) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_11) delete_0_head_11)) + :extrafuns ((delete_0_head_13 BitVec[32])) + :assumption +(= delete_0_head_13 (ite (and (= (select arr_val_15 delete_0_head_12) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_12) delete_0_head_12)) + :extrafuns ((delete_0_head_14 BitVec[32])) + :assumption +(= delete_0_head_14 (ite (and (= (select arr_val_15 delete_0_head_13) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_13) delete_0_head_13)) + :extrafuns ((delete_0_head_15 BitVec[32])) + :assumption +(= delete_0_head_15 (ite (and (= (select arr_val_15 delete_0_head_14) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_14) delete_0_head_14)) + :extrafuns ((delete_0_prev_0 BitVec[32])) + :extrafuns ((delete_0_prev_1 BitVec[32])) + :assumption +(= delete_0_prev_1 (ite (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32]))) delete_0_head_15 delete_0_prev_0)) + :extrafuns ((delete_0_curr_0 BitVec[32])) + :extrafuns ((delete_0_curr_1 BitVec[32])) + :assumption +(= delete_0_curr_1 (ite (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32]))) (select arr_next_29 delete_0_head_15) delete_0_curr_0)) + :extrafuns ((arr_next_30 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_30 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (= (select arr_val_15 delete_0_curr_1) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_29 delete_0_prev_1 (select arr_next_29 delete_0_curr_1)) arr_next_29))) + :extrafuns ((delete_0_curr_2 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_2 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (= (select arr_val_15 delete_0_curr_1) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_30 delete_0_curr_1) delete_0_curr_1))) + :extrafuns ((delete_0_prev_2 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_2 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_1) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_2 delete_0_prev_1))) + :extrafuns ((delete_0_curr_3 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_3 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_1) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_30 delete_0_curr_2) delete_0_curr_2))) + :extrafuns ((arr_next_31 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_31 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (= (select arr_val_15 delete_0_curr_3) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_30 delete_0_prev_2 (select arr_next_30 delete_0_curr_3)) arr_next_30))) + :extrafuns ((delete_0_curr_4 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_4 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (= (select arr_val_15 delete_0_curr_3) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_31 delete_0_curr_3) delete_0_curr_3))) + :extrafuns ((delete_0_prev_3 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_3 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_3) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_4 delete_0_prev_2))) + :extrafuns ((delete_0_curr_5 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_5 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_3) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_31 delete_0_curr_4) delete_0_curr_4))) + :extrafuns ((arr_next_32 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_32 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (= (select arr_val_15 delete_0_curr_5) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_31 delete_0_prev_3 (select arr_next_31 delete_0_curr_5)) arr_next_31))) + :extrafuns ((delete_0_curr_6 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_6 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (= (select arr_val_15 delete_0_curr_5) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_32 delete_0_curr_5) delete_0_curr_5))) + :extrafuns ((delete_0_prev_4 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_4 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_5) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_6 delete_0_prev_3))) + :extrafuns ((delete_0_curr_7 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_7 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_5) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_32 delete_0_curr_6) delete_0_curr_6))) + :extrafuns ((arr_next_33 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_33 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (= (select arr_val_15 delete_0_curr_7) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_32 delete_0_prev_4 (select arr_next_32 delete_0_curr_7)) arr_next_32))) + :extrafuns ((delete_0_curr_8 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_8 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (= (select arr_val_15 delete_0_curr_7) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_33 delete_0_curr_7) delete_0_curr_7))) + :extrafuns ((delete_0_prev_5 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_5 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_7) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_8 delete_0_prev_4))) + :extrafuns ((delete_0_curr_9 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_9 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_7) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_33 delete_0_curr_8) delete_0_curr_8))) + :extrafuns ((arr_next_34 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_34 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (= (select arr_val_15 delete_0_curr_9) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_33 delete_0_prev_5 (select arr_next_33 delete_0_curr_9)) arr_next_33))) + :extrafuns ((delete_0_curr_10 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_10 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (= (select arr_val_15 delete_0_curr_9) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_34 delete_0_curr_9) delete_0_curr_9))) + :extrafuns ((delete_0_prev_6 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_6 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_9) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_10 delete_0_prev_5))) + :extrafuns ((delete_0_curr_11 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_11 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_9) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_34 delete_0_curr_10) delete_0_curr_10))) + :extrafuns ((arr_next_35 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_35 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (= (select arr_val_15 delete_0_curr_11) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_34 delete_0_prev_6 (select arr_next_34 delete_0_curr_11)) arr_next_34))) + :extrafuns ((delete_0_curr_12 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_12 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (= (select arr_val_15 delete_0_curr_11) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_35 delete_0_curr_11) delete_0_curr_11))) + :extrafuns ((delete_0_prev_7 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_7 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_11) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_12 delete_0_prev_6))) + :extrafuns ((delete_0_curr_13 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_13 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_11) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_35 delete_0_curr_12) delete_0_curr_12))) + :extrafuns ((arr_next_36 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_36 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (= (select arr_val_15 delete_0_curr_13) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_35 delete_0_prev_7 (select arr_next_35 delete_0_curr_13)) arr_next_35))) + :extrafuns ((delete_0_curr_14 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_14 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (= (select arr_val_15 delete_0_curr_13) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_36 delete_0_curr_13) delete_0_curr_13))) + :extrafuns ((delete_0_prev_8 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_8 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_13) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_14 delete_0_prev_7))) + :extrafuns ((delete_0_curr_15 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_15 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_13) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_36 delete_0_curr_14) delete_0_curr_14))) + :extrafuns ((arr_next_37 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_37 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (= (select arr_val_15 delete_0_curr_15) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_36 delete_0_prev_8 (select arr_next_36 delete_0_curr_15)) arr_next_36))) + :extrafuns ((delete_0_curr_16 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_16 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (= (select arr_val_15 delete_0_curr_15) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_37 delete_0_curr_15) delete_0_curr_15))) + :extrafuns ((delete_0_prev_9 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_9 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_15) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_16 delete_0_prev_8))) + :extrafuns ((delete_0_curr_17 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_17 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_15) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_37 delete_0_curr_16) delete_0_curr_16))) + :extrafuns ((arr_next_38 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_38 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (= (select arr_val_15 delete_0_curr_17) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_37 delete_0_prev_9 (select arr_next_37 delete_0_curr_17)) arr_next_37))) + :extrafuns ((delete_0_curr_18 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_18 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (= (select arr_val_15 delete_0_curr_17) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_38 delete_0_curr_17) delete_0_curr_17))) + :extrafuns ((delete_0_prev_10 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_10 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_17) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_18 delete_0_prev_9))) + :extrafuns ((delete_0_curr_19 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_19 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_17) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_38 delete_0_curr_18) delete_0_curr_18))) + :extrafuns ((arr_next_39 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_39 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (= (select arr_val_15 delete_0_curr_19) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_38 delete_0_prev_10 (select arr_next_38 delete_0_curr_19)) arr_next_38))) + :extrafuns ((delete_0_curr_20 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_20 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (= (select arr_val_15 delete_0_curr_19) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_39 delete_0_curr_19) delete_0_curr_19))) + :extrafuns ((delete_0_prev_11 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_11 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_19) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_20 delete_0_prev_10))) + :extrafuns ((delete_0_curr_21 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_21 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_19) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_39 delete_0_curr_20) delete_0_curr_20))) + :extrafuns ((arr_next_40 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_40 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (= (select arr_val_15 delete_0_curr_21) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_39 delete_0_prev_11 (select arr_next_39 delete_0_curr_21)) arr_next_39))) + :extrafuns ((delete_0_curr_22 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_22 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (= (select arr_val_15 delete_0_curr_21) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_40 delete_0_curr_21) delete_0_curr_21))) + :extrafuns ((delete_0_prev_12 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_12 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_21) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_22 delete_0_prev_11))) + :extrafuns ((delete_0_curr_23 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_23 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_21) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_40 delete_0_curr_22) delete_0_curr_22))) + :extrafuns ((arr_next_41 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_41 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (= (select arr_val_15 delete_0_curr_23) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_40 delete_0_prev_12 (select arr_next_40 delete_0_curr_23)) arr_next_40))) + :extrafuns ((delete_0_curr_24 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_24 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (= (select arr_val_15 delete_0_curr_23) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_41 delete_0_curr_23) delete_0_curr_23))) + :extrafuns ((delete_0_prev_13 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_13 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_23) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_24 delete_0_prev_12))) + :extrafuns ((delete_0_curr_25 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_25 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_23) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_41 delete_0_curr_24) delete_0_curr_24))) + :extrafuns ((arr_next_42 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_42 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (= (select arr_val_15 delete_0_curr_25) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_41 delete_0_prev_13 (select arr_next_41 delete_0_curr_25)) arr_next_41))) + :extrafuns ((delete_0_curr_26 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_26 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (= (select arr_val_15 delete_0_curr_25) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_42 delete_0_curr_25) delete_0_curr_25))) + :extrafuns ((delete_0_prev_14 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_14 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_25) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_26 delete_0_prev_13))) + :extrafuns ((delete_0_curr_27 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_27 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_25) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_42 delete_0_curr_26) delete_0_curr_26))) + :extrafuns ((arr_next_43 Array[32:32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= arr_next_43 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (= (select arr_val_15 delete_0_curr_27) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_42 delete_0_prev_14 (select arr_next_42 delete_0_curr_27)) arr_next_42))) + :extrafuns ((delete_0_curr_28 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_28 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (= (select arr_val_15 delete_0_curr_27) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_43 delete_0_curr_27) delete_0_curr_27))) + :extrafuns ((delete_0_prev_15 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_15 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_27) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_28 delete_0_prev_14))) + :extrafuns ((delete_0_curr_29 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_29 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_27) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_43 delete_0_curr_28) delete_0_curr_28))) + :extrafuns ((delete_return_0 BitVec[32])) + :extrafuns ((delete_return_1 BitVec[32])) + :assumption +(= delete_return_1 delete_0_head_15) + :extrafuns ((main_0_head_2 BitVec[32])) + :assumption +(= main_0_head_2 delete_return_1) + :extrafuns ((main_0_x_0 BitVec[32])) + :extrafuns ((member_0_val_0 BitVec[32])) + :extrafuns ((member_0_val_1 BitVec[32])) + :assumption +(= member_0_val_1 bv0[32]) + :extrafuns ((member_0_head_0 BitVec[32])) + :extrafuns ((member_0_head_1 BitVec[32])) + :assumption +(= member_0_head_1 main_0_head_2) + :extrafuns ((member_0_curr_0 BitVec[32])) + :extrafuns ((member_0_curr_1 BitVec[32])) + :assumption +(= member_0_curr_1 member_0_head_1) + :extrafuns ((member_0_result_0 BitVec[32])) + :extrafuns ((member_0_result_1 BitVec[32])) + :assumption +(= member_0_result_1 (ite (and (not (= member_0_curr_1 (bvneg bv1[32]))) (= (select arr_val_15 member_0_curr_1) member_0_val_1)) bv1[32] member_0_result_0)) + :extrafuns ((member_0_curr_2 BitVec[32])) + :assumption +(flet ($cvc_0 (not (= member_0_curr_1 (bvneg bv1[32])))) (= member_0_curr_2 (ite (and (not (and $cvc_0 (= (select arr_val_15 member_0_curr_1) member_0_val_1))) $cvc_0) (select arr_next_43 member_0_curr_1) member_0_curr_1))) + :extrafuns ((member_0_result_2 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_2 (ite (and (and (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1))) (not (= member_0_curr_2 ?cvc_0))) (= (select arr_val_15 member_0_curr_2) member_0_val_1)) bv1[32] member_0_result_1))) + :extrafuns ((member_0_curr_3 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_2 ?cvc_0))) (= member_0_curr_3 (ite (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_2) member_0_val_1))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_2) member_0_curr_2)))) + :extrafuns ((member_0_result_3 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_3 (ite (and (and (and (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_3 ?cvc_0))) (= (select arr_val_15 member_0_curr_3) member_0_val_1)) bv1[32] member_0_result_2))) + :extrafuns ((member_0_curr_4 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_3 ?cvc_0))) (= member_0_curr_4 (ite (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_3) member_0_val_1))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_3) member_0_curr_3)))) + :extrafuns ((member_0_result_4 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_4 (ite (and (and (and (and (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_4 ?cvc_0))) (= (select arr_val_15 member_0_curr_4) member_0_val_1)) bv1[32] member_0_result_3))) + :extrafuns ((member_0_curr_5 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_4 ?cvc_0))) (= member_0_curr_5 (ite (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_4) member_0_val_1))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_4) member_0_curr_4)))) + :extrafuns ((member_0_result_5 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_5 (ite (and (and (and (and (and (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_5 ?cvc_0))) (= (select arr_val_15 member_0_curr_5) member_0_val_1)) bv1[32] member_0_result_4))) + :extrafuns ((member_0_curr_6 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_5 ?cvc_0))) (= member_0_curr_6 (ite (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_5) member_0_val_1))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_5) member_0_curr_5)))) + :extrafuns ((member_0_result_6 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_6 (ite (and (and (and (and (and (and (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_6 ?cvc_0))) (= (select arr_val_15 member_0_curr_6) member_0_val_1)) bv1[32] member_0_result_5))) + :extrafuns ((member_0_curr_7 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_6 ?cvc_0))) (= member_0_curr_7 (ite (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_6) member_0_val_1))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_6) member_0_curr_6)))) + :extrafuns ((member_0_result_7 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_7 (ite (and (and (and (and (and (and (and (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_7 ?cvc_0))) (= (select arr_val_15 member_0_curr_7) member_0_val_1)) bv1[32] member_0_result_6))) + :extrafuns ((member_0_curr_8 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_7 ?cvc_0))) (= member_0_curr_8 (ite (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_7) member_0_val_1))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_7) member_0_curr_7)))) + :extrafuns ((member_0_result_8 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_8 (ite (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_8 ?cvc_0))) (= (select arr_val_15 member_0_curr_8) member_0_val_1)) bv1[32] member_0_result_7))) + :extrafuns ((member_0_curr_9 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_8 ?cvc_0))) (= member_0_curr_9 (ite (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_8) member_0_val_1))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_8) member_0_curr_8)))) + :extrafuns ((member_0_result_9 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_9 (ite (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_9 ?cvc_0))) (= (select arr_val_15 member_0_curr_9) member_0_val_1)) bv1[32] member_0_result_8))) + :extrafuns ((member_0_curr_10 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_9 ?cvc_0))) (= member_0_curr_10 (ite (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_9) member_0_val_1))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_9) member_0_curr_9)))) + :extrafuns ((member_0_result_10 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_10 (ite (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_10 ?cvc_0))) (= (select arr_val_15 member_0_curr_10) member_0_val_1)) bv1[32] member_0_result_9))) + :extrafuns ((member_0_curr_11 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_10 ?cvc_0))) (= member_0_curr_11 (ite (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_10) member_0_val_1))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_10) member_0_curr_10)))) + :extrafuns ((member_0_result_11 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_11 (ite (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_11 ?cvc_0))) (= (select arr_val_15 member_0_curr_11) member_0_val_1)) bv1[32] member_0_result_10))) + :extrafuns ((member_0_curr_12 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_11 ?cvc_0))) (= member_0_curr_12 (ite (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_11) member_0_val_1))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_11) member_0_curr_11)))) + :extrafuns ((member_0_result_12 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_12 (ite (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_12 ?cvc_0))) (= (select arr_val_15 member_0_curr_12) member_0_val_1)) bv1[32] member_0_result_11))) + :extrafuns ((member_0_curr_13 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_12 ?cvc_0))) (= member_0_curr_13 (ite (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_12) member_0_val_1))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_12) member_0_curr_12)))) + :extrafuns ((member_0_result_13 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_13 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_13 ?cvc_0))) (= (select arr_val_15 member_0_curr_13) member_0_val_1)) bv1[32] member_0_result_12))) + :extrafuns ((member_0_curr_14 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_13 ?cvc_0))) (= member_0_curr_14 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_13) member_0_val_1))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_13) member_0_curr_13)))) + :extrafuns ((member_0_result_14 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_14 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_14 ?cvc_0))) (= (select arr_val_15 member_0_curr_14) member_0_val_1)) bv1[32] member_0_result_13))) + :extrafuns ((member_0_curr_15 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_14 ?cvc_0))) (= member_0_curr_15 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_14) member_0_curr_14)))) + :extrafuns ((member_0_result_15 BitVec[32])) + :assumption +(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_15 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_14 ?cvc_0)) (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) bv0[32] member_0_result_14))) + :extrafuns ((main_0_x_1 BitVec[32])) + :assumption +(= main_0_x_1 member_0_result_15) + :formula +(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (flet ($cvc_2 (not (= member_0_curr_14 ?cvc_0))) (not (and (and (and (and (implies (bvult main_0_i_14 bv13[32]) (not (bvult main_0_i_15 bv13[32]))) (implies (and (= (select arr_val_15 delete_0_head_14) delete_0_val_1) $cvc_1) (not (= (select arr_val_15 delete_0_head_15) delete_0_val_1)))) (implies (and (not (= delete_0_curr_27 ?cvc_0)) $cvc_1) (not (not (= delete_0_curr_29 ?cvc_0))))) (implies (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_2 (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_2) (not (not (= member_0_curr_15 ?cvc_0))))) (= main_0_x_1 bv0[32])))))) +) diff --git a/test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt b/test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt new file mode 100644 index 000000000..028427acc --- /dev/null +++ b/test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt @@ -0,0 +1,28 @@ +(benchmark B_ +:logic QF_AUFBV +:extrafuns ((R_ESP_1_58 BitVec[32])) +:extrafuns ((mem_35_197 Array[32:8])) +:status sat +:formula +(let (?n1 bv0[32]) +(let (?n2 bv0[24]) +(let (?n3 bv1[32]) +(let (?n4 (bvadd ?n3 R_ESP_1_58)) +(let (?n5 bv0[8]) +(let (?n6 (store mem_35_197 ?n4 ?n5)) +(let (?n7 (bvadd ?n3 ?n4)) +(let (?n8 (store ?n6 ?n7 ?n5)) +(let (?n9 (store ?n8 ?n1 ?n5)) +(let (?n10 (select ?n6 R_ESP_1_58)) +(let (?n11 (concat ?n2 ?n10)) +(let (?n12 (bvadd ?n3 ?n11)) +(let (?n13 (select ?n9 ?n12)) +(let (?n14 (concat ?n2 ?n13)) +(let (?n15 (bvxor ?n3 ?n14)) +(let (?n16 (extract[7:0] ?n15)) +(let (?n17 (store ?n9 ?n12 ?n16)) +(let (?n18 (select ?n17 ?n1)) +(let (?n19 (concat ?n2 ?n18)) +(flet ($n20 (= ?n1 ?n19)) +$n20 +))))))))))))))))))))) diff --git a/test/regress/regress0/aufbv/wchains010ue.delta01.smt b/test/regress/regress0/aufbv/wchains010ue.delta01.smt new file mode 100644 index 000000000..28a892e8d --- /dev/null +++ b/test/regress/regress0/aufbv/wchains010ue.delta01.smt @@ -0,0 +1,36 @@ +(benchmark wchains010ue.smt +:logic QF_AUFBV +:extrafuns ((v6 BitVec[32])) +:extrafuns ((a1 Array[32:8])) +:extrafuns ((v15 BitVec[32])) +:status sat +:formula +(let (?n1 bv0[1]) +(let (?n2 (extract[1:0] v6)) +(let (?n3 bv0[2]) +(flet ($n4 (= ?n2 ?n3)) +(let (?n5 bv1[1]) +(let (?n6 (ite $n4 ?n5 ?n1)) +(let (?n7 bv0[8]) +(let (?n8 (store a1 v15 ?n7)) +(let (?n9 bv1[32]) +(let (?n10 (bvadd ?n9 v15)) +(let (?n11 (store ?n8 ?n10 ?n7)) +(let (?n12 bv3[32]) +(let (?n13 (bvadd ?n12 v15)) +(let (?n14 (store ?n11 ?n13 ?n7)) +(let (?n15 (extract[7:0] v6)) +(let (?n16 (store a1 v6 ?n15)) +(let (?n17 (bvadd ?n9 v6)) +(let (?n18 bv1[8]) +(let (?n19 (store ?n16 ?n17 ?n18)) +(let (?n20 (bvadd ?n12 v6)) +(let (?n21 (store ?n19 ?n20 ?n18)) +(flet ($n22 (= ?n14 ?n21)) +(let (?n23 (ite $n22 ?n5 ?n1)) +(let (?n24 (bvnot ?n23)) +(let (?n25 (bvand ?n6 ?n24)) +(flet ($n26 (= ?n1 ?n25)) +(flet ($n27 (not $n26)) +$n27 +)))))))))))))))))))))))))))) diff --git a/test/regress/regress0/aufbv/wchains010ue.delta02.smt b/test/regress/regress0/aufbv/wchains010ue.delta02.smt new file mode 100644 index 000000000..d5ddf6446 --- /dev/null +++ b/test/regress/regress0/aufbv/wchains010ue.delta02.smt @@ -0,0 +1,35 @@ +(benchmark wchains010ue.smt +:logic QF_AUFBV +:extrafuns ((v6 BitVec[32])) +:extrafuns ((v7 BitVec[32])) +:extrafuns ((a1 Array[32:8])) +:status unsat +:formula +(let (?n1 bv0[1]) +(let (?n2 bv0[2]) +(let (?n3 (extract[1:0] v6)) +(flet ($n4 (= ?n2 ?n3)) +(let (?n5 bv1[1]) +(let (?n6 (ite $n4 ?n5 ?n1)) +(let (?n7 (extract[23:16] v6)) +(let (?n8 (store a1 v6 ?n7)) +(let (?n9 bv0[32]) +(let (?n10 bv0[8]) +(let (?n11 (store ?n8 ?n9 ?n10)) +(let (?n12 (extract[23:16] v7)) +(let (?n13 (store ?n11 v7 ?n12)) +(let (?n14 bv1[32]) +(let (?n15 (store ?n13 ?n14 ?n10)) +(let (?n16 (store ?n15 ?n9 ?n10)) +(let (?n17 (store a1 ?n9 ?n10)) +(let (?n18 (store ?n17 v7 ?n12)) +(let (?n19 (store ?n18 ?n14 ?n10)) +(let (?n20 (store ?n19 v6 ?n7)) +(flet ($n21 (= ?n16 ?n20)) +(let (?n22 (ite $n21 ?n5 ?n1)) +(let (?n23 (bvnot ?n22)) +(let (?n24 (bvand ?n6 ?n23)) +(flet ($n25 (= ?n1 ?n24)) +(flet ($n26 (not $n25)) +$n26 +))))))))))))))))))))))))))) diff --git a/test/regress/regress0/aufbv/wchains010ue.smt b/test/regress/regress0/aufbv/wchains010ue.smt new file mode 100644 index 000000000..a4d0f1ddb --- /dev/null +++ b/test/regress/regress0/aufbv/wchains010ue.smt @@ -0,0 +1,221 @@ +(benchmark wchains010ue.smt +:source { +This benchmark generates write chain permutations and tries to show +via extensionality that they are equal. + +Contributed by Armin Biere (armin.biere@jku.at). +} +:status unsat +:category { crafted } +:logic QF_AUFBV +:difficulty { 2 } +:extrafuns ((a1 Array[32:8])) +:extrafuns ((v6 BitVec[32])) +:extrafuns ((v7 BitVec[32])) +:extrafuns ((v8 BitVec[32])) +:extrafuns ((v9 BitVec[32])) +:extrafuns ((v10 BitVec[32])) +:extrafuns ((v11 BitVec[32])) +:extrafuns ((v12 BitVec[32])) +:extrafuns ((v13 BitVec[32])) +:extrafuns ((v14 BitVec[32])) +:extrafuns ((v15 BitVec[32])) +:formula +(let (?e2 bv0[32]) +(let (?e3 bv1[32]) +(let (?e4 bv2[32]) +(let (?e5 bv3[32]) +(let (?e16 (bvadd ?e2 v6)) +(let (?e17 (extract[7:0] v6)) +(let (?e18 (store a1 ?e16 ?e17)) +(let (?e19 (bvadd ?e3 v6)) +(let (?e20 (extract[15:8] v6)) +(let (?e21 (store ?e18 ?e19 ?e20)) +(let (?e22 (bvadd ?e4 v6)) +(let (?e23 (extract[23:16] v6)) +(let (?e24 (store ?e21 ?e22 ?e23)) +(let (?e25 (bvadd ?e5 v6)) +(let (?e26 (extract[31:24] v6)) +(let (?e27 (store ?e24 ?e25 ?e26)) +(let (?e28 (bvadd ?e2 v7)) +(let (?e29 (extract[7:0] v7)) +(let (?e30 (store ?e27 ?e28 ?e29)) +(let (?e31 (bvadd ?e3 v7)) +(let (?e32 (extract[15:8] v7)) +(let (?e33 (store ?e30 ?e31 ?e32)) +(let (?e34 (bvadd ?e4 v7)) +(let (?e35 (extract[23:16] v7)) +(let (?e36 (store ?e33 ?e34 ?e35)) +(let (?e37 (bvadd ?e5 v7)) +(let (?e38 (extract[31:24] v7)) +(let (?e39 (store ?e36 ?e37 ?e38)) +(let (?e40 (bvadd ?e2 v8)) +(let (?e41 (extract[7:0] v8)) +(let (?e42 (store ?e39 ?e40 ?e41)) +(let (?e43 (bvadd ?e3 v8)) +(let (?e44 (extract[15:8] v8)) +(let (?e45 (store ?e42 ?e43 ?e44)) +(let (?e46 (bvadd ?e4 v8)) +(let (?e47 (extract[23:16] v8)) +(let (?e48 (store ?e45 ?e46 ?e47)) +(let (?e49 (bvadd ?e5 v8)) +(let (?e50 (extract[31:24] v8)) +(let (?e51 (store ?e48 ?e49 ?e50)) +(let (?e52 (bvadd ?e2 v9)) +(let (?e53 (extract[7:0] v9)) +(let (?e54 (store ?e51 ?e52 ?e53)) +(let (?e55 (bvadd ?e3 v9)) +(let (?e56 (extract[15:8] v9)) +(let (?e57 (store ?e54 ?e55 ?e56)) +(let (?e58 (bvadd ?e4 v9)) +(let (?e59 (extract[23:16] v9)) +(let (?e60 (store ?e57 ?e58 ?e59)) +(let (?e61 (bvadd ?e5 v9)) +(let (?e62 (extract[31:24] v9)) +(let (?e63 (store ?e60 ?e61 ?e62)) +(let (?e64 (bvadd ?e2 v10)) +(let (?e65 (extract[7:0] v10)) +(let (?e66 (store ?e63 ?e64 ?e65)) +(let (?e67 (bvadd ?e3 v10)) +(let (?e68 (extract[15:8] v10)) +(let (?e69 (store ?e66 ?e67 ?e68)) +(let (?e70 (bvadd ?e4 v10)) +(let (?e71 (extract[23:16] v10)) +(let (?e72 (store ?e69 ?e70 ?e71)) +(let (?e73 (bvadd ?e5 v10)) +(let (?e74 (extract[31:24] v10)) +(let (?e75 (store ?e72 ?e73 ?e74)) +(let (?e76 (bvadd ?e2 v11)) +(let (?e77 (extract[7:0] v11)) +(let (?e78 (store ?e75 ?e76 ?e77)) +(let (?e79 (bvadd ?e3 v11)) +(let (?e80 (extract[15:8] v11)) +(let (?e81 (store ?e78 ?e79 ?e80)) +(let (?e82 (bvadd ?e4 v11)) +(let (?e83 (extract[23:16] v11)) +(let (?e84 (store ?e81 ?e82 ?e83)) +(let (?e85 (bvadd ?e5 v11)) +(let (?e86 (extract[31:24] v11)) +(let (?e87 (store ?e84 ?e85 ?e86)) +(let (?e88 (bvadd ?e2 v12)) +(let (?e89 (extract[7:0] v12)) +(let (?e90 (store ?e87 ?e88 ?e89)) +(let (?e91 (bvadd ?e3 v12)) +(let (?e92 (extract[15:8] v12)) +(let (?e93 (store ?e90 ?e91 ?e92)) +(let (?e94 (bvadd ?e4 v12)) +(let (?e95 (extract[23:16] v12)) +(let (?e96 (store ?e93 ?e94 ?e95)) +(let (?e97 (bvadd ?e5 v12)) +(let (?e98 (extract[31:24] v12)) +(let (?e99 (store ?e96 ?e97 ?e98)) +(let (?e100 (bvadd ?e2 v13)) +(let (?e101 (extract[7:0] v13)) +(let (?e102 (store ?e99 ?e100 ?e101)) +(let (?e103 (bvadd ?e3 v13)) +(let (?e104 (extract[15:8] v13)) +(let (?e105 (store ?e102 ?e103 ?e104)) +(let (?e106 (bvadd ?e4 v13)) +(let (?e107 (extract[23:16] v13)) +(let (?e108 (store ?e105 ?e106 ?e107)) +(let (?e109 (bvadd ?e5 v13)) +(let (?e110 (extract[31:24] v13)) +(let (?e111 (store ?e108 ?e109 ?e110)) +(let (?e112 (bvadd ?e2 v14)) +(let (?e113 (extract[7:0] v14)) +(let (?e114 (store ?e111 ?e112 ?e113)) +(let (?e115 (bvadd ?e3 v14)) +(let (?e116 (extract[15:8] v14)) +(let (?e117 (store ?e114 ?e115 ?e116)) +(let (?e118 (bvadd ?e4 v14)) +(let (?e119 (extract[23:16] v14)) +(let (?e120 (store ?e117 ?e118 ?e119)) +(let (?e121 (bvadd ?e5 v14)) +(let (?e122 (extract[31:24] v14)) +(let (?e123 (store ?e120 ?e121 ?e122)) +(let (?e124 (bvadd ?e2 v15)) +(let (?e125 (extract[7:0] v15)) +(let (?e126 (store ?e123 ?e124 ?e125)) +(let (?e127 (bvadd ?e3 v15)) +(let (?e128 (extract[15:8] v15)) +(let (?e129 (store ?e126 ?e127 ?e128)) +(let (?e130 (bvadd ?e4 v15)) +(let (?e131 (extract[23:16] v15)) +(let (?e132 (store ?e129 ?e130 ?e131)) +(let (?e133 (bvadd ?e5 v15)) +(let (?e134 (extract[31:24] v15)) +(let (?e135 (store ?e132 ?e133 ?e134)) +(let (?e136 (store a1 ?e124 ?e125)) +(let (?e137 (store ?e136 ?e127 ?e128)) +(let (?e138 (store ?e137 ?e130 ?e131)) +(let (?e139 (store ?e138 ?e133 ?e134)) +(let (?e140 (store ?e139 ?e112 ?e113)) +(let (?e141 (store ?e140 ?e115 ?e116)) +(let (?e142 (store ?e141 ?e118 ?e119)) +(let (?e143 (store ?e142 ?e121 ?e122)) +(let (?e144 (store ?e143 ?e100 ?e101)) +(let (?e145 (store ?e144 ?e103 ?e104)) +(let (?e146 (store ?e145 ?e106 ?e107)) +(let (?e147 (store ?e146 ?e109 ?e110)) +(let (?e148 (store ?e147 ?e88 ?e89)) +(let (?e149 (store ?e148 ?e91 ?e92)) +(let (?e150 (store ?e149 ?e94 ?e95)) +(let (?e151 (store ?e150 ?e97 ?e98)) +(let (?e152 (store ?e151 ?e76 ?e77)) +(let (?e153 (store ?e152 ?e79 ?e80)) +(let (?e154 (store ?e153 ?e82 ?e83)) +(let (?e155 (store ?e154 ?e85 ?e86)) +(let (?e156 (store ?e155 ?e64 ?e65)) +(let (?e157 (store ?e156 ?e67 ?e68)) +(let (?e158 (store ?e157 ?e70 ?e71)) +(let (?e159 (store ?e158 ?e73 ?e74)) +(let (?e160 (store ?e159 ?e52 ?e53)) +(let (?e161 (store ?e160 ?e55 ?e56)) +(let (?e162 (store ?e161 ?e58 ?e59)) +(let (?e163 (store ?e162 ?e61 ?e62)) +(let (?e164 (store ?e163 ?e40 ?e41)) +(let (?e165 (store ?e164 ?e43 ?e44)) +(let (?e166 (store ?e165 ?e46 ?e47)) +(let (?e167 (store ?e166 ?e49 ?e50)) +(let (?e168 (store ?e167 ?e28 ?e29)) +(let (?e169 (store ?e168 ?e31 ?e32)) +(let (?e170 (store ?e169 ?e34 ?e35)) +(let (?e171 (store ?e170 ?e37 ?e38)) +(let (?e172 (store ?e171 ?e16 ?e17)) +(let (?e173 (store ?e172 ?e19 ?e20)) +(let (?e174 (store ?e173 ?e22 ?e23)) +(let (?e175 (store ?e174 ?e25 ?e26)) +(let (?e176 (ite (= ?e135 ?e175) bv1[1] bv0[1])) +(let (?e177 (extract[1:0] v6)) +(let (?e178 bv0[2]) +(let (?e179 (ite (= ?e177 ?e178) bv1[1] bv0[1])) +(let (?e180 (bvand (bvnot ?e176) ?e179)) +(let (?e181 (extract[1:0] v7)) +(let (?e182 (ite (= ?e178 ?e181) bv1[1] bv0[1])) +(let (?e183 (bvand ?e180 ?e182)) +(let (?e184 (extract[1:0] v8)) +(let (?e185 (ite (= ?e178 ?e184) bv1[1] bv0[1])) +(let (?e186 (bvand ?e183 ?e185)) +(let (?e187 (extract[1:0] v9)) +(let (?e188 (ite (= ?e178 ?e187) bv1[1] bv0[1])) +(let (?e189 (bvand ?e186 ?e188)) +(let (?e190 (extract[1:0] v10)) +(let (?e191 (ite (= ?e178 ?e190) bv1[1] bv0[1])) +(let (?e192 (bvand ?e189 ?e191)) +(let (?e193 (extract[1:0] v11)) +(let (?e194 (ite (= ?e178 ?e193) bv1[1] bv0[1])) +(let (?e195 (bvand ?e192 ?e194)) +(let (?e196 (extract[1:0] v12)) +(let (?e197 (ite (= ?e178 ?e196) bv1[1] bv0[1])) +(let (?e198 (bvand ?e195 ?e197)) +(let (?e199 (extract[1:0] v13)) +(let (?e200 (ite (= ?e178 ?e199) bv1[1] bv0[1])) +(let (?e201 (bvand ?e198 ?e200)) +(let (?e202 (extract[1:0] v14)) +(let (?e203 (ite (= ?e178 ?e202) bv1[1] bv0[1])) +(let (?e204 (bvand ?e201 ?e203)) +(let (?e205 (extract[1:0] v15)) +(let (?e206 (ite (= ?e178 ?e205) bv1[1] bv0[1])) +(let (?e207 (bvand ?e204 ?e206)) +(not (= ?e207 bv0[1])) +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index 314566f87..f4f5c57b4 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -9,7 +9,8 @@ endif # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - bug336.smt2 + bug330.smt2 \ + bug336.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 5048ca680..07619b965 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -28,7 +28,8 @@ SMT_TESTS = \ fuzz11.smt \ fuzz12.smt \ fuzz13.smt \ - fuzz14.smt + fuzz14.smt \ + calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt # Regression tests for SMT2 inputs SMT2_TESTS = diff --git a/test/regress/regress0/bv/bug345.smt b/test/regress/regress0/bv/bug345.smt new file mode 100644 index 000000000..b836cba2c --- /dev/null +++ b/test/regress/regress0/bv/bug345.smt @@ -0,0 +1,46 @@ +(benchmark B_ +:logic QF_AUFBV +:extrafuns ((mem_35_197 Array[32:8])) +:status unknown +:formula +(let (?n1 bv1[1]) +(let (?n2 bv0[31]) +(let (?n3 bv0[32]) +(let (?n4 bv0[24]) +(let (?n5 (select mem_35_197 ?n3)) +(let (?n6 (concat ?n4 ?n5)) +(flet ($n7 (= ?n3 ?n6)) +(let (?n8 bv0[1]) +(let (?n9 (ite $n7 ?n1 ?n8)) +(let (?n10 (concat ?n2 ?n9)) +(let (?n11 (extract[0:0] ?n10)) +(let (?n12 bv0[8]) +(let (?n13 bv1[32]) +(let (?n14 (select mem_35_197 ?n13)) +(let (?n15 (concat ?n4 ?n14)) +(let (?n16 (extract[7:0] ?n15)) +(flet ($n17 (= ?n12 ?n16)) +(let (?n18 bv1[8]) +(flet ($n19 (= ?n16 ?n18)) +(let (?n20 bv3[8]) +(flet ($n21 (= ?n16 ?n20)) +(let (?n22 (ite $n21 ?n13 ?n3)) +(let (?n23 (ite $n19 ?n3 ?n22)) +(let (?n24 (ite $n17 ?n13 ?n23)) +(let (?n25 (extract[7:0] ?n24)) +(let (?n26 (store mem_35_197 ?n3 ?n25)) +(let (?n27 (concat ?n4 ?n16)) +(let (?n28 (extract[7:0] ?n27)) +(let (?n29 (concat ?n4 ?n28)) +(let (?n30 (extract[7:0] ?n29)) +(let (?n31 (concat ?n4 ?n30)) +(let (?n32 (bvadd ?n6 ?n31)) +(let (?n33 (store ?n26 ?n32 ?n12)) +(let (?n34 (select ?n33 ?n3)) +(let (?n35 (concat ?n4 ?n34)) +(flet ($n36 (= ?n3 ?n35)) +(let (?n37 (ite $n36 ?n1 ?n8)) +(let (?n38 (bvor ?n11 ?n37)) +(flet ($n39 (= ?n1 ?n38)) +$n39 +)))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt b/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt new file mode 100644 index 000000000..467f10c39 --- /dev/null +++ b/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt @@ -0,0 +1,80 @@ +(benchmark B_ +:logic QF_BV +:extrapreds ((UCL_p16)) +:extrapreds ((UCL_p34)) +:status sat +:formula +(let (?n1 bv1[1]) +(let (?n2 bv0[2]) +(let (?n3 bv1[5]) +(let (?n4 bv0[5]) +(let (?n5 bv0[4]) +(let (?n6 bv1[4]) +(let (?n7 (ite UCL_p16 ?n6 ?n5)) +(flet ($n8 (= ?n5 ?n7)) +(let (?n9 bv1[2]) +(let (?n10 (ite $n8 ?n9 ?n2)) +(flet ($n11 (= ?n2 ?n10)) +(flet ($n12 (= ?n9 ?n10)) +(flet ($n13 (or $n11 $n12)) +(let (?n14 (ite $n13 ?n3 ?n4)) +(flet ($n15 (= ?n4 ?n14)) +(let (?n16 (ite $n15 ?n3 ?n4)) +(flet ($n17 (= ?n4 ?n16)) +(let (?n18 (ite UCL_p34 ?n2 ?n9)) +(flet ($n19 (= ?n9 ?n18)) +(let (?n20 (ite $n19 ?n6 ?n5)) +(flet ($n21 (= ?n5 ?n20)) +(let (?n22 (ite $n21 ?n3 ?n4)) +(let (?n23 (bvadd ?n22 ?n16)) +(let (?n24 (bvadd ?n3 ?n23)) +(let (?n25 (ite $n17 ?n24 ?n23)) +(flet ($n26 (= ?n3 ?n25)) +(let (?n27 bv1[6]) +(let (?n28 (concat ?n27 ?n9)) +(let (?n29 bv0[32]) +(let (?n30 (concat ?n28 ?n29)) +(let (?n31 (concat ?n30 ?n29)) +(let (?n32 bv0[72]) +(let (?n33 (ite $n26 ?n31 ?n32)) +(let (?n34 (extract[67:64] ?n33)) +(let (?n35 (extract[3:2] ?n34)) +(flet ($n36 (= ?n2 ?n35)) +(let (?n37 (ite $n36 ?n9 ?n2)) +(flet ($n38 (= ?n2 ?n37)) +(let (?n39 bv0[3]) +(let (?n40 bv1[3]) +(let (?n41 (ite $n38 ?n39 ?n40)) +(let (?n42 (extract[0:0] ?n41)) +(flet ($n43 (= ?n1 ?n42)) +(let (?n44 (ite $n43 ?n9 ?n2)) +(let (?n45 (ite $n12 ?n3 ?n4)) +(flet ($n46 (= ?n4 ?n45)) +(let (?n47 (ite $n8 ?n3 ?n4)) +(flet ($n48 (= ?n4 ?n47)) +(let (?n49 (ite $n48 ?n14 ?n4)) +(flet ($n50 (= ?n4 ?n49)) +(let (?n51 (bvsub ?n4 ?n3)) +(let (?n52 (ite $n50 ?n4 ?n51)) +(flet ($n53 (= ?n4 ?n52)) +(let (?n54 (ite $n53 ?n3 ?n52)) +(let (?n55 (ite $n46 ?n4 ?n54)) +(flet ($n56 (= ?n3 ?n55)) +(let (?n57 (concat ?n6 ?n9)) +(let (?n58 (concat ?n57 ?n2)) +(let (?n59 (concat ?n58 ?n29)) +(let (?n60 (concat ?n59 ?n29)) +(let (?n61 (bvadd ?n45 ?n52)) +(flet ($n62 (= ?n3 ?n61)) +(let (?n63 (ite $n62 ?n32 ?n31)) +(let (?n64 (ite $n56 ?n60 ?n63)) +(let (?n65 (extract[67:64] ?n64)) +(let (?n66 (extract[3:2] ?n65)) +(flet ($n67 (= ?n2 ?n66)) +(let (?n68 (extract[71:68] ?n64)) +(flet ($n69 (= ?n5 ?n68)) +(let (?n70 (ite $n69 ?n2 ?n9)) +(let (?n71 (ite $n67 ?n70 ?n2)) +(flet ($n72 (= ?n44 ?n71)) +$n72 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index 0244d768e..5b095b500 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -14,7 +14,12 @@ MAKEFLAGS = -k # Regression tests for SMT inputs SMT_TESTS = \ xs-09-16-3-4-1-5.smt \ + xs-09-16-3-4-1-5.delta01.smt \ + xs-09-16-3-4-1-5.delta02.smt \ + xs-09-16-3-4-1-5.delta03.smt \ + xs-09-16-3-4-1-5.delta04.smt \ error0.smt2 \ + error0.delta01.smt \ simple_cyclic2.smt2 # Regression tests for SMT2 inputs diff --git a/test/regress/regress0/uflia/error0.delta01.smt b/test/regress/regress0/uflia/error0.delta01.smt new file mode 100644 index 000000000..cc205063c --- /dev/null +++ b/test/regress/regress0/uflia/error0.delta01.smt @@ -0,0 +1,78 @@ +(benchmark B_ +:logic QF_UFLIA +:extrafuns ((format Int Int)) +:extrafuns ((arg1 Int)) +:extrafuns ((fmt1 Int)) +:extrafuns ((s_count Int Int)) +:extrafuns ((fmt0 Int)) +:extrafuns ((x_count Int Int)) +:status sat +:formula +(flet ($n1 true) +(let (?n2 1) +(let (?n3 (~ ?n2)) +(let (?n4 (* ?n3 fmt1)) +(let (?n5 (+ ?n4 fmt0)) +(let (?n6 8) +(let (?n7 (~ ?n6)) +(flet ($n8 (>= ?n5 ?n7)) +(let (?n9 6) +(let (?n10 (x_count ?n9)) +(let (?n11 7) +(let (?n12 (x_count ?n11)) +(let (?n13 (* ?n3 ?n12)) +(let (?n14 (+ ?n10 ?n13)) +(let (?n15 0) +(flet ($n16 (>= ?n14 ?n15)) +(flet ($n17 (>= fmt1 ?n11)) +(flet ($n18 (<= arg1 ?n9)) +(let (?n19 2) +(let (?n20 (~ ?n19)) +(let (?n21 (* ?n3 fmt0)) +(let (?n22 (+ fmt1 ?n20 ?n21)) +(let (?n23 (s_count ?n22)) +(let (?n24 5) +(let (?n25 (s_count ?n24)) +(let (?n26 (* ?n3 ?n25)) +(let (?n27 (+ ?n23 ?n26)) +(flet ($n28 (= ?n15 ?n27)) +(flet ($n29 (not $n28)) +(let (?n30 (~ ?n11)) +(flet ($n31 (<= ?n5 ?n30)) +(flet ($n32 false) +(let (?n33 (+ arg1 ?n21)) +(flet ($n34 (<= ?n33 ?n2)) +(let (?n35 (+ ?n4 arg1)) +(flet ($n36 (<= ?n35 ?n15)) +(flet ($n37 (or $n32 $n32 $n34 $n36)) +(let (?n38 (x_count ?n2)) +(flet ($n39 (>= ?n38 ?n15)) +(let (?n40 (format ?n11)) +(flet ($n41 (<= ?n40 ?n15)) +(let (?n42 (x_count ?n22)) +(let (?n43 (+ ?n13 ?n42)) +(flet ($n44 (= ?n15 ?n43)) +(let (?n45 (s_count ?n9)) +(let (?n46 (* ?n3 ?n45)) +(let (?n47 (+ ?n23 ?n46)) +(flet ($n48 (= ?n15 ?n47)) +(flet ($n49 (or $n32 $n32 $n32 $n32 $n32 $n39 $n44 $n48)) +(let (?n50 (+ ?n2 fmt1)) +(let (?n51 (format ?n50)) +(flet ($n52 (>= ?n51 ?n15)) +(let (?n53 4) +(let (?n54 (format ?n53)) +(flet ($n55 (>= ?n54 ?n15)) +(let (?n56 9) +(let (?n57 (format ?n56)) +(flet ($n58 (<= ?n57 ?n15)) +(let (?n59 (format fmt1)) +(flet ($n60 (>= ?n59 ?n15)) +(let (?n61 12) +(let (?n62 (format ?n61)) +(flet ($n63 (>= ?n62 ?n15)) +(let (?n64 (format arg1)) +(flet ($n65 (= ?n15 ?n64)) +(flet ($n66 (and $n1 $n8 $n16 $n17 $n18 $n29 $n31 $n37 $n39 $n41 $n49 $n52 $n55 $n58 $n60 $n63 $n65)) +$n66 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt new file mode 100644 index 000000000..c7fed0c15 --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt @@ -0,0 +1,48 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((s_count Int Int)) +:extrafuns ((fmt1 Int)) +:extrafuns ((fmt_length Int)) +:status unsat +:formula +(let (?n1 0) +(let (?n2 6) +(let (?n3 (s_count ?n2)) +(flet ($n4 (= ?n1 ?n3)) +(let (?n5 5) +(let (?n6 (s_count ?n5)) +(flet ($n7 (= ?n1 ?n6)) +(let (?n8 4) +(let (?n9 (s_count ?n8)) +(flet ($n10 (= ?n1 ?n9)) +(let (?n11 3) +(let (?n12 (s_count ?n11)) +(flet ($n13 (= ?n1 ?n12)) +(let (?n14 1) +(let (?n15 (s_count ?n1)) +(flet ($n16 (= ?n14 ?n15)) +(let (?n17 (s_count ?n14)) +(flet ($n18 (= ?n1 ?n17)) +(flet ($n19 (and $n16 $n18)) +(let (?n20 2) +(let (?n21 (s_count ?n20)) +(flet ($n22 (= ?n1 ?n21)) +(flet ($n23 (and $n19 $n22)) +(flet ($n24 (and $n13 $n23)) +(flet ($n25 (and $n10 $n24)) +(flet ($n26 (and $n7 $n25)) +(flet ($n27 (and $n4 $n26)) +(let (?n28 9) +(flet ($n29 (= ?n28 fmt_length)) +(flet ($n30 (> fmt1 ?n14)) +(flet ($n31 (< fmt1 fmt_length)) +(flet ($n32 (and $n30 $n31)) +(let (?n33 (- fmt1 ?n20)) +(let (?n34 (s_count ?n33)) +(let (?n35 (+ ?n14 ?n34)) +(flet ($n36 (= ?n1 ?n35)) +(flet ($n37 (and $n32 $n36)) +(flet ($n38 (and $n29 $n37)) +(flet ($n39 (and $n27 $n38)) +$n39 +)))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt new file mode 100644 index 000000000..fb16651ff --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt @@ -0,0 +1,40 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((arg1 Int)) +:extrafuns ((adr_lo Int)) +:extrafuns ((select_format Int Int)) +:extrafuns ((x Int)) +:status sat +:formula +(let (?n1 (select_format arg1)) +(flet ($n2 (= ?n1 adr_lo)) +(let (?n3 0) +(flet ($n4 (= ?n3 x)) +(let (?n5 4) +(let (?n6 (select_format ?n5)) +(flet ($n7 (= adr_lo ?n6)) +(let (?n8 3) +(let (?n9 (select_format ?n8)) +(flet ($n10 (= adr_lo ?n9)) +(let (?n11 2) +(let (?n12 (select_format ?n11)) +(flet ($n13 (= adr_lo ?n12)) +(let (?n14 1) +(let (?n15 (select_format ?n3)) +(flet ($n16 (= ?n14 ?n15)) +(let (?n17 (select_format ?n14)) +(flet ($n18 (= ?n3 ?n17)) +(flet ($n19 (or $n16 $n18)) +(flet ($n20 (or $n13 $n19)) +(flet ($n21 (or $n10 $n20)) +(flet ($n22 (or $n7 $n21)) +(flet ($n23 (or $n4 $n22)) +(flet ($n24 (= adr_lo ?n8)) +(flet ($n25 (< arg1 ?n5)) +(flet ($n26 (>= arg1 ?n3)) +(flet ($n27 (and $n25 $n26)) +(flet ($n28 (and $n24 $n27)) +(flet ($n29 (and $n23 $n28)) +(flet ($n30 (and $n2 $n29)) +$n30 +))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt new file mode 100644 index 000000000..6f65e83ec --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt @@ -0,0 +1,45 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((fmt_length Int)) +:extrafuns ((fmt1 Int)) +:extrafuns ((arg1 Int)) +:extrafuns ((select_format Int Int)) +:status sat +:formula +(let (?n1 1) +(let (?n2 (+ ?n1 fmt1)) +(let (?n3 (select_format ?n2)) +(flet ($n4 (= ?n1 ?n3)) +(let (?n5 (select_format arg1)) +(let (?n6 0) +(flet ($n7 (= ?n5 ?n6)) +(flet ($n8 (and $n4 $n7)) +(let (?n9 7) +(let (?n10 (select_format ?n9)) +(flet ($n11 (= ?n1 ?n10)) +(let (?n12 (select_format ?n6)) +(flet ($n13 (= ?n1 ?n12)) +(let (?n14 (select_format ?n1)) +(flet ($n15 (= ?n1 ?n14)) +(flet ($n16 (or $n13 $n15)) +(let (?n17 5) +(let (?n18 (select_format ?n17)) +(flet ($n19 (= ?n6 ?n18)) +(flet ($n20 (or $n16 $n19)) +(let (?n21 6) +(let (?n22 (select_format ?n21)) +(flet ($n23 (= ?n6 ?n22)) +(flet ($n24 (or $n20 $n23)) +(flet ($n25 (or $n11 $n24)) +(let (?n26 9) +(flet ($n27 (= ?n26 fmt_length)) +(let (?n28 2) +(let (?n29 (- fmt1 ?n28)) +(flet ($n30 (= arg1 ?n29)) +(flet ($n31 (< fmt1 fmt_length)) +(flet ($n32 (and $n30 $n31)) +(flet ($n33 (and $n27 $n32)) +(flet ($n34 (and $n25 $n33)) +(flet ($n35 (and $n8 $n34)) +$n35 +)))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt new file mode 100644 index 000000000..f1212a876 --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt @@ -0,0 +1,67 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((fmt_length Int)) +:extrafuns ((fmt1 Int)) +:extrafuns ((x_count Int Int)) +:extrafuns ((select_format Int Int)) +:extrafuns ((percent Int)) +:extrafuns ((s_count Int Int)) +:status sat +:formula +(let (?n1 1) +(let (?n2 5) +(let (?n3 (x_count ?n2)) +(flet ($n4 (= ?n1 ?n3)) +(let (?n5 4) +(let (?n6 (x_count ?n5)) +(flet ($n7 (= ?n1 ?n6)) +(let (?n8 3) +(let (?n9 (x_count ?n8)) +(let (?n10 2) +(let (?n11 (x_count ?n10)) +(flet ($n12 (= ?n9 ?n11)) +(let (?n13 0) +(let (?n14 (select_format ?n8)) +(flet ($n15 (= ?n13 ?n14)) +(let (?n16 (x_count ?n13)) +(flet ($n17 (= ?n1 ?n16)) +(flet ($n18 (= ?n1 percent)) +(flet ($n19 true) +(let (?n20 (s_count ?n13)) +(flet ($n21 (= ?n13 ?n20)) +(flet ($n22 (if_then_else $n18 $n19 $n21)) +(let (?n23 (select_format ?n10)) +(flet ($n24 (= percent ?n23)) +(flet ($n25 (= ?n1 ?n14)) +(flet ($n26 (and $n24 $n25)) +(flet ($n27 false) +(flet ($n28 (if_then_else $n26 $n27 $n19)) +(flet ($n29 (and $n22 $n28)) +(flet ($n30 (and $n17 $n29)) +(flet ($n31 (= ?n13 percent)) +(flet ($n32 (= ?n13 ?n23)) +(flet ($n33 (and $n31 $n32)) +(let (?n34 (x_count ?n1)) +(flet ($n35 (= ?n13 ?n34)) +(flet ($n36 (= ?n16 ?n34)) +(flet ($n37 (if_then_else $n33 $n35 $n36)) +(flet ($n38 (and $n30 $n37)) +(flet ($n39 (and $n15 $n38)) +(flet ($n40 (and $n12 $n39)) +(flet ($n41 (and $n7 $n40)) +(flet ($n42 (and $n4 $n41)) +(let (?n43 9) +(flet ($n44 (= ?n43 fmt_length)) +(let (?n45 (- fmt1 ?n10)) +(let (?n46 (x_count ?n45)) +(let (?n47 (+ ?n1 ?n46)) +(flet ($n48 (= ?n13 ?n47)) +(flet ($n49 (> fmt1 ?n1)) +(let (?n50 (- fmt_length ?n1)) +(flet ($n51 (< fmt1 ?n50)) +(flet ($n52 (and $n49 $n51)) +(flet ($n53 (and $n48 $n52)) +(flet ($n54 (and $n44 $n53)) +(flet ($n55 (and $n42 $n54)) +$n55 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp index c64c1463e..f1dc77988 100644 --- a/test/system/boilerplate.cpp +++ b/test/system/boilerplate.cpp @@ -31,7 +31,8 @@ int main() { ExprManager em; Options opts; SmtEngine smt(&em); - Result r = smt.query(em.mkConst(true)); + BoolExpr F = em.mkConst(true); + Result r = smt.query(F); return r == Result::VALID ? 0 : 1; } diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 1de3854b9..34536445f 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -57,9 +57,10 @@ public: push(CONFLICT, n); } - void propagate(TNode n) + bool propagate(TNode n) throw(AssertionException) { push(PROPAGATE, n); + return true; } void propagateAsDecision(TNode n) diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index ff6cba936..2d6730949 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -51,7 +51,7 @@ class FakeOutputChannel : public OutputChannel { void conflict(TNode n) throw(AssertionException) { Unimplemented(); } - void propagate(TNode n) throw(AssertionException) { + bool propagate(TNode n) throw(AssertionException) { Unimplemented(); } void propagateAsDecision(TNode n) throw(AssertionException) { -- 2.30.2