http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
};
const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
+const TheoryId THEORY_SAT_SOLVER = THEORY_LAST;
inline TheoryId& operator ++ (TheoryId& id) {
return id = static_cast<TheoryId>(((int)id) + 1);
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<TNode> 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) */
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<TNode> 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
}
break;
case EQUALITY_FALSE_IN_MODEL:
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl;
+ continue;
break;
default:
break;
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()) {
}
// 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: "<<d_RowQueue.size()<<"\n";
- dischargeLemmas();
- }
+ if(!d_eagerLemmas && fullEffort(e) && !d_conflict) {
+ // generate the lemmas on the worklist
+ Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
+ dischargeLemmas();
}
Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
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)) {
}
}
+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 */
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;
}
};
/** Equaltity engine */
eq::EqualityEngine d_equalityEngine;
- // Are we in conflict?
+ /** Are we in conflict? */
context::CDO<bool> d_conflict;
+ /** Conflict when merging constants */
+ void conflict(TNode a, TNode b);
+
/** The conflict node */
Node d_conflictNode;
}
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 {
}
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 {
}
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);
}
}
// 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<TNode> 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<TNode> 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);
}
}
void TheoryBV::explain(TNode literal, std::vector<TNode>& 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<TNode> assumptions;
// Ask for the explanation
}
inline Node mkAnd(std::vector<TNode>& children) {
- if (children.size() > 1) {
- return NodeManager::currentNM()->mkNode(kind::AND, children);
- } else {
- return children[0];
+ std::set<TNode> 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<TNode>::const_iterator it = distinctChildren.begin();
+ std::set<TNode>::const_iterator it_end = distinctChildren.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+
+ return conjunction;
}
inline Node mkSortedNode(Kind kind, std::vector<Node>& children) {
* 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
** \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);
}
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;
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);
}
}
-
-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<bool>()) {
- // 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
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<TNode>& conjunctions) {
}
return conjunction;
-}/* mkAnd() */
+}
+void SharedTermsDatabase::checkForConflict() {
+ if (d_inConflict) {
+ d_inConflict = false;
+ std::vector<TNode> 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<TNode> 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<TNode> assumptions;
+ d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+ return mkAnd(assumptions);
+}
+
#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:
/** Context-dependent size of the d_addedSharedTerms list */
context::CDO<unsigned> d_addedSharedTermsSize;
- typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
-
/** A map from atoms and subterms to the theories that use it */
+ typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
SharedTermsTheoriesMap d_termsToTheories;
- typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
-
/** Map from term to theories that have already been notified about the shared term */
+ typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> 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<TNode, TNodeHashFunction> 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<theory::TheoryId, TNode, __gnu_cxx::hash<unsigned> > NotifyList;
- typedef context::CDHashMap<TNode, NotifyList*, TNodeHashFunction> 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<NotifyList*> d_allocatedNL;
-
- // Total number of allocated NotifyList* objects
- unsigned d_allocatedNLSize;
-
- // Size of portion of d_allocatedNL that is currently in use
- context::CDO<unsigned> d_allocatedNLNext;
-
/** This method removes all the un-necessary stuff from the maps */
void backtrack();
public:
EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
bool eqNotifyTriggerEquality(TNode equality, bool value) {
- Unreachable();
+ d_sharedTerms.propagateEquality(equality, value);
return true;
}
}
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;
}
};
/** 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<bool> 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.
*/
* 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:
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)
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<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
if (multipleTheories) {
}
}
+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<TNode>::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<Assertion>::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<typename T, bool doAssert>
class scoped_vector_clear {
vector<T>& d_v;
} \
}
- // make sure d_propagatedSharedLiterals is cleared on exit
- scoped_vector_clear<SharedLiteral, true> clear_shared_literals(d_propagatedSharedLiterals);
// Do the checking
try {
// 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;
// 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;
}
}
} catch(const theory::Interrupted&) {
Trace("theory") << "TheoryEngine::check() => conflict" << endl;
}
-}
-
-void TheoryEngine::outputSharedLiterals() {
-
- scoped_vector_clear<SharedLiteral, false> 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;
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<bool>();
- 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);
-
}
}
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")
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<bool>()) {
+ // 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) {
}
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;
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;
}
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<NodeTheoryPair>& 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<TNode> 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<bool>(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<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::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<TNode> satAssertions;
- std::deque<ExplainTask> explainQueue;
- // TODO: benchmark whether this helps
- std::hash_set<ExplainTask, ExplainTaskHashFunction> 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<NodeTheoryPair> 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<Node> 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 <evil laugh>.) --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<TNode>::const_iterator it = satAssertions.begin();
- std::set<TNode>::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) {
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<NodeTheoryPair> 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
}
}
-
-//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);
return result;
}
+void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& 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<bool>()) {
+ ++ i;
+ continue;
+ }
+ if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst<bool>()) {
+ ++ 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<Node>& assertions)
{
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;
}
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;
}
* CVC4.
*/
class TheoryEngine {
+
+ /** Shared terms database can use the internals notify the theories */
+ friend class SharedTermsDatabase;
/** Associated PropEngine engine */
prop::PropEngine* d_propEngine;
*/
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.
*/
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) {
*/
context::CDO<bool> 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.
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<Node, theory::TheoryId, NodeHashFunction> 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<NodeTheoryPair, Node, NodeTheoryPairHashFunction> 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<SharedLiteral> d_propagatedSharedLiterals;
-
- void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory)
- {
- if (literal.getKind() == kind::CONST_BOOLEAN) {
- Assert(!literal.getConst<bool>());
- sharedConflict(original);
- }
- else {
- d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory));
- }
- }
+ typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> PropagationMap;
+ PropagationMap d_propagationMap;
/**
- * Assert the shared literals that are queued up to the theories.
+ * Timestamp of propagations
*/
- void outputSharedLiterals();
+ context::CDO<size_t> d_propagationMapTimestamp;
/**
* Literals that are propagated by the theory. Note that these are TNodes.
/**
* 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
/**
* 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<Node> 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 <evil laugh>.) --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;
*/
bool d_inPreregister;
+ /**
+ * Did the theories get any new facts since the last time we called
+ * check()
+ */
+ context::CDO<bool> 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<NodeTheoryPair>& explanationVector);
+
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);
/**
/** 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;
UnconstrainedSimplifier d_unconstrainedSimp;
public:
+
Node ppSimpITE(TNode assertion);
void ppUnconstrainedSimp(std::vector<Node>& assertions);
push(CONFLICT, n);
}
- void propagate(TNode n)
+ bool propagate(TNode n)
throw(AssertionException) {
push(PROPAGATE, n);
+ return true;
}
void propagateAsDecision(TNode n)
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(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) {
}
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) {
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 {
}
// Add to the use lists
- d_equalityNodes[t1ClassId].usedIn<USE_LIST_FUNCTIONS>(funId, d_useListNodes);
- d_equalityNodes[t2ClassId].usedIn<USE_LIST_FUNCTIONS>(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;
// 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();
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];
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)) {
Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
Assert(triggersFired.empty());
-
+
++ d_stats.mergesCount;
EqualityNodeId class1Id = class1.getFind();
// 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;
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<USE_LIST_FUNCTIONS>();
+ 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();
// 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()));
}
}
}
// Now merge the lists
class1.merge<true>(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();) {
// 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;
}
}
- // 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;
}
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<USE_LIST_FUNCTIONS>(d_useListNodes);
+ getEqualityNode(app.b).removeTopFromUseList(d_useListNodes);
// Remove a from use-list
- getEqualityNode(app.a).removeTopFromUseList<USE_LIST_FUNCTIONS>(d_useListNodes);
+ getEqualityNode(app.a).removeTopFromUseList(d_useListNodes);
}
}
// 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
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;
// Depending on the merge preference (such as size, or being a constant), merge them
std::vector<TriggerId> 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)) {
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) {
// 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<EqualityNodeId> 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
// Get the current node
EqualityNode& currentNode = getEqualityNode(currentId);
// Go through the use-list
- UseListNodeId currentUseId = currentNode.getUseList<USE_LIST_FUNCTIONS>();
+ UseListNodeId currentUseId = currentNode.getUseList();
while (currentUseId != null_uselist_id) {
// Get the node of the use list
UseListNode& useNode = d_useListNodes[currentUseId];
*/
std::vector<bool> 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.
*/
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)
+ {}
};
/**
}
};
-/** 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
/** The use list of this node */
UseListNodeId d_useList;
- /** The list of asserted disequalities that this node appears in */
- UseListNodeId d_diseqList;
-
public:
/**
, d_findId(nodeId)
, d_nextId(nodeId)
, d_useList(null_uselist_id)
- , d_diseqList(null_uselist_id)
{}
/**
* Returns the requested uselist.
*/
- template<UseListType type>
UseListNodeId getUseList() const {
- return type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList;
+ return d_useList;
}
/**
* Note that this node is used in a function application funId, or
* a negatively asserted equality (dis-equality) with funId.
*/
- template<UseListType type, typename memory_class>
+ template<typename memory_class>
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<UseListType type, typename memory_class>
+ template<typename memory_class>
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();
}
};
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;
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];
}
}
- // 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;
}/* 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<TNode> 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<TNode>& assumptions) {
}
}
}/* 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;
+}
}
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 {
}
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 {
}
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;
}
};
/** 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);
void addSharedTerm(TNode n);
void computeCareGraph();
+ void propagate(Effort effort) {}
+
EqualityStatus getEqualityStatus(TNode a, TNode b);
std::string identify() const {
} 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.
--- /dev/null
+topdir = ../../../..
+srcdir = test/regress/regress0/aufbv
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
# 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)
--- /dev/null
+(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]))))))
+)
--- /dev/null
+(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
+)))))))))))))))))))))
--- /dev/null
+(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
+))))))))))))))))))))))))))))
--- /dev/null
+(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
+)))))))))))))))))))))))))))
--- /dev/null
+(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]))
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
# 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)
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 =
--- /dev/null
+(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
+))))))))))))))))))))))))))))))))))))))))
--- /dev/null
+(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
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
# 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
--- /dev/null
+(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
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
--- /dev/null
+(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
+))))))))))))))))))))))))))))))))))))))))
--- /dev/null
+(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
+)))))))))))))))))))))))))))))))
--- /dev/null
+(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
+))))))))))))))))))))))))))))))))))))
--- /dev/null
+(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
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))
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;
}
push(CONFLICT, n);
}
- void propagate(TNode n)
+ bool propagate(TNode n)
throw(AssertionException) {
push(PROPAGATE, n);
+ return true;
}
void propagateAsDecision(TNode n)
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) {
projects / cvc5.git / commitdiff