From: Dejan Jovanović Date: Thu, 7 Jun 2012 07:11:24 +0000 (+0000) Subject: fixing some bugs in propagation of disequalities X-Git-Tag: cvc5-1.0.0~8114 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=49dd14da8d872403b4d772a2d49224e4d6bda227;p=cvc5.git fixing some bugs in propagation of disequalities still doesnt fix the wrong answers thought :( --- diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4ba4aeba5..91bbae2f4 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -581,8 +581,8 @@ void TheoryArrays::computeCareGraph() Assert(false); break; case EQUALITY_FALSE_AND_PROPAGATED: - // TODO: eventually this should be an Assert(false), but for now, disequalities are not propagated - continue; + // Should have been propagated to us + Assert(false); break; case EQUALITY_FALSE: case EQUALITY_TRUE: @@ -591,7 +591,6 @@ void TheoryArrays::computeCareGraph() break; case EQUALITY_FALSE_IN_MODEL: Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl; - continue; break; default: break; diff --git a/src/theory/theory.h b/src/theory/theory.h index 36255d1d6..020a2b194 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -447,6 +447,7 @@ public: * the actual computation, and use addCarePair to add pairs to the care graph. */ void getCareGraph(CareGraph& careGraph) { + Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl; TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime); d_careGraph = &careGraph; computeCareGraph(); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ca2460805..a7b13dc2f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -190,6 +190,44 @@ void TheoryEngine::dumpAssertions(const char* tag) { Dump(tag) << AssertCommand(assertionExpr); } Dump(tag) << CheckSatCommand(); + + // Check for any missed propagations of shared terms + if (d_logicInfo.isSharingEnabled()) { + Dump(tag) << CommentCommand("Shared term equalities"); + context::CDList::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); + for (; it != it_end; ++ it) { + TNode t1 = (*it); + context::CDList::const_iterator it2 = it; + for (++ it2; it2 != it_end; ++ it2) { + TNode t2 = (*it2); + if (t1.getType() == t2.getType()) { + Node equality = t1.eqNode(t2); + if (d_sharedTerms.isKnown(equality)) { + continue; + } + Node disequality = equality.notNode(); + if (d_sharedTerms.isKnown(disequality)) { + continue; + } + + // Check equality + Dump(tag) << PushCommand(); + BoolExpr eqExpr(equality.toExpr()); + Dump(tag) << AssertCommand(eqExpr); + Dump(tag) << CheckSatCommand(); + Dump(tag) << PopCommand(); + + // Check disequality + Dump(tag) << PushCommand(); + BoolExpr diseqExpr(disequality.toExpr()); + Dump(tag) << AssertCommand(diseqExpr); + Dump(tag) << CheckSatCommand(); + Dump(tag) << PopCommand(); + } + } + } + } + Dump(tag) << PopCommand(); } } @@ -316,6 +354,8 @@ void TheoryEngine::combineTheories() { // Call on each parametric theory to give us its care graph CVC4_FOR_EACH_THEORY; + Debug("sharing") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << std::endl; + // Now add splitters for the ones we are interested in CareGraph::const_iterator care_it = careGraph.begin(); CareGraph::const_iterator care_it_end = careGraph.end(); @@ -328,7 +368,7 @@ void TheoryEngine::combineTheories() { 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); + Node equality = Rewriter::rewriteEquality(carePair.theory, carePair.a.eqNode(carePair.b)); // Normalize the equality Node normalizedEquality = Rewriter::rewrite(equality); @@ -349,6 +389,8 @@ void TheoryEngine::combineTheories() { // Mark that we have more information d_factsAsserted = true; continue; + } else { + Unreachable(); } } } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 4cd54a2bf..c5ccaaeea 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -351,14 +351,16 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { // 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)) { + EqualityNodeId aClassId = getEqualityNode(a).getFind(); + EqualityNodeId bClassId = getEqualityNode(b).getFind(); + if (d_isConstant[aClassId] && d_isConstant[bClassId]) { 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]; + TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[aClassId]; + TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[bClassId]; if (aTriggerRef != +null_set_id && bTriggerRef != +null_set_id) { // The sets of trigger terms TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef); @@ -419,8 +421,31 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect EqualityNodeId class2Id = class2.getFind(); // Check for constant merges - bool isConstant = d_isConstant[class1Id]; - Assert(isConstant || !d_isConstant[class2Id]); + bool class1isConstant = d_isConstant[class1Id]; + bool class2isConstant = d_isConstant[class2Id]; + Assert(class1isConstant || !class2isConstant, "Should always merge into constants"); + + // Trigger set of class 1 + TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id]; + Theory::Set class1Tags = class1triggerRef == null_set_id ? 0 : getTriggerTermSet(class1triggerRef).tags; + // Trigger set of class 2 + TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id]; + Theory::Set class2Tags = class2triggerRef == null_set_id ? 0 : getTriggerTermSet(class2triggerRef).tags; + + // Disequalities coming from class2 + TaggedEqualitiesSet class2disequalitiesToNotify; + // Disequalities coming from class1 + TaggedEqualitiesSet class1disequalitiesToNotify; + + // Individual tags + Theory::Set class1OnlyTags = Theory::setDifference(class1Tags, class2Tags); + Theory::Set class2OnlyTags = Theory::setDifference(class2Tags, class1Tags); + + // Only get disequalities if they are not both constant + if (!class1isConstant || !class2isConstant) { + getDisequalities(!class1isConstant, class2Id, class1OnlyTags, class2disequalitiesToNotify); + getDisequalities(!class2isConstant, class1Id, class2OnlyTags, class1disequalitiesToNotify); + } // Update class2 representative information Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl; @@ -519,7 +544,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Notify of the constants merge bool constantMerge = false; - if (isConstant && d_isConstant[class2Id]) { + if (class1isConstant && d_isConstant[class2Id]) { constantMerge = true; if (d_performNotify) { if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) { @@ -547,10 +572,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } triggersFired.resize(j); + // Go through the trigger term disequalities and propagate + if (!propagateTriggerTermDisequalities(class1OnlyTags, class1triggerRef, class2disequalitiesToNotify)) { + return false; + } + if (!propagateTriggerTermDisequalities(class2OnlyTags, class2triggerRef, class1disequalitiesToNotify)) { + return false; + } + // Notify the trigger term merges - TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id]; if (class2triggerRef != +null_set_id) { - TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id]; if (class1triggerRef == +null_set_id) { // If class1 doesn't have individual triggers, but class2 does, mark it d_nodeIndividualTrigger[class1Id] = class2triggerRef; @@ -1293,61 +1324,9 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // Check for disequalities by going through the equivalence class looking for equalities in the // uselists that have been asserted to false. All the representatives appearing on the other // side of such disequalities, that have the tag on, are put in a set. - std::set disequalSet; - EqualityNodeId currentId = classId; - do { - // Current node - EqualityNode& currentNode = getEqualityNode(currentId); - // Go through the uselist and look for disequalities - UseListNodeId currentUseId = currentNode.getUseList(); - while (!d_done && currentUseId != null_uselist_id) { - // Get the normalized equality - UseListNode& useNode = d_useListNodes[currentUseId]; - EqualityNodeId funId = useNode.getApplicationId(); - const FunctionApplication& fun = d_applications[useNode.getApplicationId()].original; - // Check for asserted disequalities - if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { - // Get the other equality member - EqualityNodeId toCompare = fun.b; - if (toCompare == currentId) { - toCompare = fun.a; - } - // Representative of the other member - EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind(); - Assert(toCompareRep != classId); - // Get the trigger set - TriggerTermSetRef toCompareTriggerSetRef = d_nodeIndividualTrigger[toCompareRep]; - // Only notify if we're not both constants - if ((!d_isConstant[classId] || !d_isConstant[toCompareRep]) && toCompareTriggerSetRef != null_set_id) { - TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef); - if (Theory::setContains(tag, toCompareTriggerSet.tags)) { - // Get the tag representative - EqualityNodeId tagRep = toCompareTriggerSet.getTrigger(tag); - // Propagate the disequality if not already done - if (!disequalSet.count(tagRep) && d_performNotify) { - // Mark as propagated - disequalSet.insert(tagRep); - // Store the propagation - d_deducedDisequalityReasons.push_back(EqualityPair(eqNodeId, currentId)); - d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep)); - d_deducedDisequalityReasons.push_back(EqualityPair(funId, d_falseId)); - storePropagatedDisequality(t, d_nodes[tagRep], 3); - // We don't check if it's been propagated already, as we need one per tag - if (d_performNotify) { - if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[tagRep], false)) { - d_done = true; - } - } - } - } - } - } - // Go to the next one in the use list - currentUseId = useNode.getNext(); - } - // Next in equivalence class - currentId = currentNode.getNext(); - } while (!d_done && currentId != classId); + TaggedEqualitiesSet disequalitiesToNotify; + Theory::Set tags = Theory::setInsert(tag); + getDisequalities(!d_isConstant[classId], classId, tags, disequalitiesToNotify); // Setup the data for the new set if (triggerSetRef != null_set_id) { @@ -1378,7 +1357,10 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) d_triggerTermSetUpdates.push_back(TriggerSetUpdate(classId, triggerSetRef)); d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1; // Mark the the new set as a trigger - d_nodeIndividualTrigger[classId] = newTriggerTermSet(); + d_nodeIndividualTrigger[classId] = triggerSetRef = newTriggerTermSet(); + + // Propagate trigger term disequalities we remembered + propagateTriggerTermDisequalities(tags, triggerSetRef, disequalitiesToNotify); } } @@ -1497,6 +1479,117 @@ bool EqualityEngine::storePropagatedDisequality(TNode lhs, TNode rhs, unsigned r } } +void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out) { + // Must be empty on input + Assert(out.size() == 0); + // The class we are looking for, shouldn't have any of the tags we are looking for already set + Assert(d_nodeIndividualTrigger[classId] == null_set_id || Theory::setIntersection(getTriggerTermSet(d_nodeIndividualTrigger[classId]).tags, inputTags) == 0); + + if (inputTags == 0) { + return; + } + + // Set of already (through disequalities) visited equivalence classes + std::set alreadyVisited; + + // Go through the equivalence class + EqualityNodeId currentId = classId; + do { + // Current node in the equivalence class + EqualityNode& currentNode = getEqualityNode(currentId); + + // Go through the uselist and look for disequalities + UseListNodeId currentUseId = currentNode.getUseList(); + while (currentUseId != null_uselist_id) { + UseListNode& useListNode = d_useListNodes[currentUseId]; + EqualityNodeId funId = useListNode.getApplicationId(); + const FunctionApplication& fun = d_applications[useListNode.getApplicationId()].original; + // If it's an equality asserted to false, we do the work + if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { + // Get the other equality member + bool lhs = false; + EqualityNodeId toCompare = fun.b; + if (toCompare == currentId) { + toCompare = fun.a; + lhs = true; + } + // Representative of the other member + EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind(); + Assert(toCompareRep != classId, "Otherwise we are in conflict"); + // Check if we already have this one + if (alreadyVisited.count(toCompareRep) == 0) { + // Mark as visited + alreadyVisited.insert(toCompareRep); + // Get the trigger set + TriggerTermSetRef toCompareTriggerSetRef = d_nodeIndividualTrigger[toCompareRep]; + // We only care if we're not both constants and there are trigger terms in the other class + if ((allowConstants || !d_isConstant[toCompareRep]) && toCompareTriggerSetRef != null_set_id) { + // Tags of the other gey + TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef); + // We only care if there are things in inputTags that is also in toCompareTags + Theory::Set commonTags = Theory::setIntersection(inputTags, toCompareTriggerSet.tags); + if (commonTags) { + out.push_back(TaggedEquality(funId, toCompareTriggerSetRef, lhs)); + } + } + } + } + // Go to the next one in the use list + currentUseId = useListNode.getNext(); + } + // Next in equivalence class + currentId = currentNode.getNext(); + } while (!d_done && currentId != classId); + +} + +bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify) { + + // No tags, no food + if (!tags) { + return !d_done; + } + + Assert(triggerSetRef != null_set_id); + + // This is the class trigger set + const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); + // Go throught the disequalities and notify + TaggedEqualitiesSet::const_iterator it = disequalitiesToNotify.begin(); + TaggedEqualitiesSet::const_iterator it_end = disequalitiesToNotify.end(); + for (; !d_done && it != it_end; ++ it) { + // The information about the equality that is asserted to false + const TaggedEquality& disequalityInfo = *it; + const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.triggerSetRef); + Theory::Set commonTags = Theory::setIntersection(disequalityTriggerSet.tags, tags); + Assert(commonTags); + // This is the actual function + const FunctionApplication& fun = d_applications[disequalityInfo.equalityId].original; + // Figure out who we are comparing to in the original equality + EqualityNodeId toCompare = disequalityInfo.lhs ? fun.a : fun.b; + EqualityNodeId myCompare = disequalityInfo.lhs ? fun.b : fun.a; + // Go through the tags, and add the disequalities + TheoryId currentTag; + while (!d_done && ((currentTag = Theory::setPop(commonTags)) != THEORY_LAST)) { + // Get the tag representative + EqualityNodeId tagRep = disequalityTriggerSet.getTrigger(currentTag); + EqualityNodeId myRep = triggerSet.getTrigger(currentTag); + // Store the propagation + d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep)); + d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep)); + d_deducedDisequalityReasons.push_back(EqualityPair(disequalityInfo.equalityId, d_falseId)); + storePropagatedDisequality(d_nodes[myRep], 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(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) { + d_done = true; + } + } + } + } + + return !d_done; +} } // Namespace uf } // Namespace theory diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f40c79df3..5935ddc1f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -520,8 +520,48 @@ private: */ std::vector d_deducedDisequalityReasons; - + /** + * Stores a propagated disequality for explanation purpooses and remembers the reasons. + */ bool storePropagatedDisequality(TNode lhs, TNode rhs, unsigned reasonsCount) const; + + /** + * An equality tagged with a set of tags. + */ + struct TaggedEquality { + /** Id of the equality */ + EqualityNodeId equalityId; + /** TriggerSet reference for the class of one of the sides */ + TriggerTermSetRef triggerSetRef; + /** Is trigger equivalent to the lhs (rhs otherwise) */ + bool lhs; + + TaggedEquality(EqualityNodeId equalityId = null_id, TriggerTermSetRef triggerSetRef = null_set_id, bool lhs = true) + : equalityId(equalityId), triggerSetRef(triggerSetRef), lhs(lhs) {} + }; + + /** A map from equivalence class id's to tagged equalities */ + typedef std::vector TaggedEqualitiesSet; + + /** + * Returns a set of equalities that have been asserted false where one side of the equality + * belongs to the given equivalence class. The equalities are restricted to the ones where + * one side of the equality is in the tags set, but the other one isn't. Each returned + * dis-equality is associated with the tags that are the subset of the input tags, such that + * exactly one side of the equality is not in the set yet. + * + * @param classId the equivalence class to search + * @param inputTags the tags to filter the equalities + * @param out the output equalities, as described above + */ + void getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out); + + /** + * Propagates the remembered disequalities with given tags the original triggers for those tags, + * and the set of disequalities produced by above. + */ + bool propagateTriggerTermDisequalities(Theory::Set tags, + TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify); public: diff --git a/test/regress/regress0/aufbv/dubreva005ue.delta01.smt b/test/regress/regress0/aufbv/dubreva005ue.delta01.smt new file mode 100644 index 000000000..4f2f91e71 --- /dev/null +++ b/test/regress/regress0/aufbv/dubreva005ue.delta01.smt @@ -0,0 +1,33 @@ +(benchmark dubreva005ue.smt +:logic QF_AUFBV +:extrafuns ((a1 Array[32:8])) +:status unsat +:formula +(let (?n1 bv0[1]) +(let (?n2 bv0[32]) +(let (?n3 bv1[8]) +(let (?n4 (store a1 ?n2 ?n3)) +(let (?n5 (select a1 ?n2)) +(let (?n6 (bvnot ?n3)) +(let (?n7 (bvand ?n5 ?n6)) +(let (?n8 (bvnot ?n7)) +(let (?n9 (bvand ?n3 ?n8)) +(let (?n10 (store ?n4 ?n2 ?n9)) +(let (?n11 (select ?n10 ?n2)) +(let (?n12 (store a1 ?n2 ?n11)) +(let (?n13 (select ?n12 ?n2)) +(let (?n14 (store a1 ?n2 ?n13)) +(let (?n15 (select ?n14 ?n2)) +(let (?n16 (store a1 ?n2 ?n15)) +(let (?n17 (select ?n16 ?n2)) +(let (?n18 (store a1 ?n2 ?n17)) +(let (?n19 (select ?n18 ?n2)) +(let (?n20 (store a1 ?n2 ?n19)) +(flet ($n21 (= ?n4 ?n20)) +(let (?n22 bv1[1]) +(let (?n23 (ite $n21 ?n22 ?n1)) +(let (?n24 (bvnot ?n23)) +(flet ($n25 (= ?n1 ?n24)) +(flet ($n26 (not $n25)) +$n26 +))))))))))))))))))))))))))) diff --git a/test/regress/regress0/aufbv/dubreva005ue.smt b/test/regress/regress0/aufbv/dubreva005ue.smt new file mode 100644 index 000000000..b3a88073f --- /dev/null +++ b/test/regress/regress0/aufbv/dubreva005ue.smt @@ -0,0 +1,223 @@ +(benchmark dubreva005ue.smt +:source { +We reverse an array of length 5 twice in memory at 5 positions. +We show via extensionality that memory has to be equal. + +In one case swapping elements is done via XOR in the following way: +x ^= y; +y ^= x; +x ^= y; +In the other case the elements are just swapped. + +Contributed by Robert Brummayer (robert.brummayer@gmail.com). +} +:status unsat +:category { crafted } +:logic QF_AUFBV +:difficulty { 2 } +:extrafuns ((a1 Array[32:8])) +:extrafuns ((start1 BitVec[32])) +:extrafuns ((start2 BitVec[32])) +:extrafuns ((start3 BitVec[32])) +:extrafuns ((start4 BitVec[32])) +:extrafuns ((start5 BitVec[32])) +:formula +(let (?e3 bv4[32]) +(let (?e4 bv1[32]) +(let (?e5 (bvadd start1 ?e3)) +(let (?e6 (select a1 start1)) +(let (?e7 (select a1 ?e5)) +(let (?e8 (store a1 ?e5 ?e6)) +(let (?e9 (store ?e8 start1 ?e7)) +(let (?e10 (bvadd (bvnot ?e4) ?e4)) +(let (?e11 (bvadd ?e5 ?e10)) +(let (?e12 (bvadd start1 ?e4)) +(let (?e13 (select ?e9 ?e12)) +(let (?e14 (select ?e9 ?e11)) +(let (?e15 (store ?e9 ?e11 ?e13)) +(let (?e16 (store ?e15 ?e12 ?e14)) +(let (?e17 (bvand (bvnot ?e6) (bvnot ?e7))) +(let (?e18 (bvand ?e6 ?e7)) +(let (?e19 (bvand (bvnot ?e17) (bvnot ?e18))) +(let (?e20 (store a1 start1 ?e19)) +(let (?e21 (bvand (bvnot ?e7) (bvnot ?e19))) +(let (?e22 (bvand ?e7 ?e19)) +(let (?e23 (bvand (bvnot ?e21) (bvnot ?e22))) +(let (?e24 (store ?e20 ?e5 ?e23)) +(let (?e25 (bvand (bvnot ?e19) (bvnot ?e23))) +(let (?e26 (bvand ?e19 ?e23)) +(let (?e27 (bvand (bvnot ?e25) (bvnot ?e26))) +(let (?e28 (store ?e24 start1 ?e27)) +(let (?e29 (select ?e28 ?e12)) +(let (?e30 (select ?e28 ?e11)) +(let (?e31 (bvand (bvnot ?e29) (bvnot ?e30))) +(let (?e32 (bvand ?e29 ?e30)) +(let (?e33 (bvand (bvnot ?e31) (bvnot ?e32))) +(let (?e34 (store ?e28 ?e12 ?e33)) +(let (?e35 (bvand (bvnot ?e30) (bvnot ?e33))) +(let (?e36 (bvand ?e30 ?e33)) +(let (?e37 (bvand (bvnot ?e35) (bvnot ?e36))) +(let (?e38 (store ?e34 ?e11 ?e37)) +(let (?e39 (bvand (bvnot ?e33) (bvnot ?e37))) +(let (?e40 (bvand ?e33 ?e37)) +(let (?e41 (bvand (bvnot ?e39) (bvnot ?e40))) +(let (?e42 (store ?e38 ?e12 ?e41)) +(let (?e44 (bvadd ?e3 start2)) +(let (?e45 (select ?e16 start2)) +(let (?e46 (select ?e16 ?e44)) +(let (?e47 (store ?e16 ?e44 ?e45)) +(let (?e48 (store ?e47 start2 ?e46)) +(let (?e49 (bvadd ?e10 ?e44)) +(let (?e50 (bvadd ?e4 start2)) +(let (?e51 (select ?e48 ?e50)) +(let (?e52 (select ?e48 ?e49)) +(let (?e53 (store ?e48 ?e49 ?e51)) +(let (?e54 (store ?e53 ?e50 ?e52)) +(let (?e55 (select ?e42 start2)) +(let (?e56 (select ?e42 ?e44)) +(let (?e57 (bvand (bvnot ?e55) (bvnot ?e56))) +(let (?e58 (bvand ?e55 ?e56)) +(let (?e59 (bvand (bvnot ?e57) (bvnot ?e58))) +(let (?e60 (store ?e42 start2 ?e59)) +(let (?e61 (bvand (bvnot ?e56) (bvnot ?e59))) +(let (?e62 (bvand ?e56 ?e59)) +(let (?e63 (bvand (bvnot ?e61) (bvnot ?e62))) +(let (?e64 (store ?e60 ?e44 ?e63)) +(let (?e65 (bvand (bvnot ?e59) (bvnot ?e63))) +(let (?e66 (bvand ?e59 ?e63)) +(let (?e67 (bvand (bvnot ?e65) (bvnot ?e66))) +(let (?e68 (store ?e64 start2 ?e67)) +(let (?e69 (select ?e68 ?e50)) +(let (?e70 (select ?e68 ?e49)) +(let (?e71 (bvand (bvnot ?e69) (bvnot ?e70))) +(let (?e72 (bvand ?e69 ?e70)) +(let (?e73 (bvand (bvnot ?e71) (bvnot ?e72))) +(let (?e74 (store ?e68 ?e50 ?e73)) +(let (?e75 (bvand (bvnot ?e70) (bvnot ?e73))) +(let (?e76 (bvand ?e70 ?e73)) +(let (?e77 (bvand (bvnot ?e75) (bvnot ?e76))) +(let (?e78 (store ?e74 ?e49 ?e77)) +(let (?e79 (bvand (bvnot ?e73) (bvnot ?e77))) +(let (?e80 (bvand ?e73 ?e77)) +(let (?e81 (bvand (bvnot ?e79) (bvnot ?e80))) +(let (?e82 (store ?e78 ?e50 ?e81)) +(let (?e84 (bvadd ?e3 start3)) +(let (?e85 (select ?e54 start3)) +(let (?e86 (select ?e54 ?e84)) +(let (?e87 (store ?e54 ?e84 ?e85)) +(let (?e88 (store ?e87 start3 ?e86)) +(let (?e89 (bvadd ?e10 ?e84)) +(let (?e90 (bvadd ?e4 start3)) +(let (?e91 (select ?e88 ?e90)) +(let (?e92 (select ?e88 ?e89)) +(let (?e93 (store ?e88 ?e89 ?e91)) +(let (?e94 (store ?e93 ?e90 ?e92)) +(let (?e95 (select ?e82 start3)) +(let (?e96 (select ?e82 ?e84)) +(let (?e97 (bvand (bvnot ?e95) (bvnot ?e96))) +(let (?e98 (bvand ?e95 ?e96)) +(let (?e99 (bvand (bvnot ?e97) (bvnot ?e98))) +(let (?e100 (store ?e82 start3 ?e99)) +(let (?e101 (bvand (bvnot ?e96) (bvnot ?e99))) +(let (?e102 (bvand ?e96 ?e99)) +(let (?e103 (bvand (bvnot ?e101) (bvnot ?e102))) +(let (?e104 (store ?e100 ?e84 ?e103)) +(let (?e105 (bvand (bvnot ?e99) (bvnot ?e103))) +(let (?e106 (bvand ?e99 ?e103)) +(let (?e107 (bvand (bvnot ?e105) (bvnot ?e106))) +(let (?e108 (store ?e104 start3 ?e107)) +(let (?e109 (select ?e108 ?e90)) +(let (?e110 (select ?e108 ?e89)) +(let (?e111 (bvand (bvnot ?e109) (bvnot ?e110))) +(let (?e112 (bvand ?e109 ?e110)) +(let (?e113 (bvand (bvnot ?e111) (bvnot ?e112))) +(let (?e114 (store ?e108 ?e90 ?e113)) +(let (?e115 (bvand (bvnot ?e110) (bvnot ?e113))) +(let (?e116 (bvand ?e110 ?e113)) +(let (?e117 (bvand (bvnot ?e115) (bvnot ?e116))) +(let (?e118 (store ?e114 ?e89 ?e117)) +(let (?e119 (bvand (bvnot ?e113) (bvnot ?e117))) +(let (?e120 (bvand ?e113 ?e117)) +(let (?e121 (bvand (bvnot ?e119) (bvnot ?e120))) +(let (?e122 (store ?e118 ?e90 ?e121)) +(let (?e124 (bvadd ?e3 start4)) +(let (?e125 (select ?e94 start4)) +(let (?e126 (select ?e94 ?e124)) +(let (?e127 (store ?e94 ?e124 ?e125)) +(let (?e128 (store ?e127 start4 ?e126)) +(let (?e129 (bvadd ?e10 ?e124)) +(let (?e130 (bvadd ?e4 start4)) +(let (?e131 (select ?e128 ?e130)) +(let (?e132 (select ?e128 ?e129)) +(let (?e133 (store ?e128 ?e129 ?e131)) +(let (?e134 (store ?e133 ?e130 ?e132)) +(let (?e135 (select ?e122 start4)) +(let (?e136 (select ?e122 ?e124)) +(let (?e137 (bvand (bvnot ?e135) (bvnot ?e136))) +(let (?e138 (bvand ?e135 ?e136)) +(let (?e139 (bvand (bvnot ?e137) (bvnot ?e138))) +(let (?e140 (store ?e122 start4 ?e139)) +(let (?e141 (bvand (bvnot ?e136) (bvnot ?e139))) +(let (?e142 (bvand ?e136 ?e139)) +(let (?e143 (bvand (bvnot ?e141) (bvnot ?e142))) +(let (?e144 (store ?e140 ?e124 ?e143)) +(let (?e145 (bvand (bvnot ?e139) (bvnot ?e143))) +(let (?e146 (bvand ?e139 ?e143)) +(let (?e147 (bvand (bvnot ?e145) (bvnot ?e146))) +(let (?e148 (store ?e144 start4 ?e147)) +(let (?e149 (select ?e148 ?e130)) +(let (?e150 (select ?e148 ?e129)) +(let (?e151 (bvand (bvnot ?e149) (bvnot ?e150))) +(let (?e152 (bvand ?e149 ?e150)) +(let (?e153 (bvand (bvnot ?e151) (bvnot ?e152))) +(let (?e154 (store ?e148 ?e130 ?e153)) +(let (?e155 (bvand (bvnot ?e150) (bvnot ?e153))) +(let (?e156 (bvand ?e150 ?e153)) +(let (?e157 (bvand (bvnot ?e155) (bvnot ?e156))) +(let (?e158 (store ?e154 ?e129 ?e157)) +(let (?e159 (bvand (bvnot ?e153) (bvnot ?e157))) +(let (?e160 (bvand ?e153 ?e157)) +(let (?e161 (bvand (bvnot ?e159) (bvnot ?e160))) +(let (?e162 (store ?e158 ?e130 ?e161)) +(let (?e164 (bvadd ?e3 start5)) +(let (?e165 (select ?e134 start5)) +(let (?e166 (select ?e134 ?e164)) +(let (?e167 (store ?e134 ?e164 ?e165)) +(let (?e168 (store ?e167 start5 ?e166)) +(let (?e169 (bvadd ?e10 ?e164)) +(let (?e170 (bvadd ?e4 start5)) +(let (?e171 (select ?e168 ?e170)) +(let (?e172 (select ?e168 ?e169)) +(let (?e173 (store ?e168 ?e169 ?e171)) +(let (?e174 (store ?e173 ?e170 ?e172)) +(let (?e175 (select ?e162 start5)) +(let (?e176 (select ?e162 ?e164)) +(let (?e177 (bvand (bvnot ?e175) (bvnot ?e176))) +(let (?e178 (bvand ?e175 ?e176)) +(let (?e179 (bvand (bvnot ?e177) (bvnot ?e178))) +(let (?e180 (store ?e162 start5 ?e179)) +(let (?e181 (bvand (bvnot ?e176) (bvnot ?e179))) +(let (?e182 (bvand ?e176 ?e179)) +(let (?e183 (bvand (bvnot ?e181) (bvnot ?e182))) +(let (?e184 (store ?e180 ?e164 ?e183)) +(let (?e185 (bvand (bvnot ?e179) (bvnot ?e183))) +(let (?e186 (bvand ?e179 ?e183)) +(let (?e187 (bvand (bvnot ?e185) (bvnot ?e186))) +(let (?e188 (store ?e184 start5 ?e187)) +(let (?e189 (select ?e188 ?e170)) +(let (?e190 (select ?e188 ?e169)) +(let (?e191 (bvand (bvnot ?e189) (bvnot ?e190))) +(let (?e192 (bvand ?e189 ?e190)) +(let (?e193 (bvand (bvnot ?e191) (bvnot ?e192))) +(let (?e194 (store ?e188 ?e170 ?e193)) +(let (?e195 (bvand (bvnot ?e190) (bvnot ?e193))) +(let (?e196 (bvand ?e190 ?e193)) +(let (?e197 (bvand (bvnot ?e195) (bvnot ?e196))) +(let (?e198 (store ?e194 ?e169 ?e197)) +(let (?e199 (bvand (bvnot ?e193) (bvnot ?e197))) +(let (?e200 (bvand ?e193 ?e197)) +(let (?e201 (bvand (bvnot ?e199) (bvnot ?e200))) +(let (?e202 (store ?e198 ?e170 ?e201)) +(let (?e203 (ite (= ?e174 ?e202) bv1[1] bv0[1])) +(not (= (bvnot ?e203) bv0[1])) +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/diseqprop.01.smt b/test/regress/regress0/uflia/diseqprop.01.smt new file mode 100644 index 000000000..93544639e --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.01.smt @@ -0,0 +1,19 @@ +(benchmark test +:logic QF_UFLIA +:extrafuns ((f Int Int)) +:extrafuns ((x1 Int)) +:extrafuns ((y1 Int)) +:extrafuns ((x2 Int)) +:extrafuns ((y2 Int)) + +:extrafuns ((a Int)) +:extrafuns ((b Int)) + +:assumption (not (= x2 y2)) +:assumption (= x1 x2) +:assumption (= y1 y2) + +:assumption (= (f x1) (f y1)) + +:formula true +) diff --git a/test/regress/regress0/uflia/diseqprop.02.smt b/test/regress/regress0/uflia/diseqprop.02.smt new file mode 100644 index 000000000..3d34c6e80 --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.02.smt @@ -0,0 +1,20 @@ +(benchmark test +:logic QF_UFLIA +:extrafuns ((f Int Int)) +:extrafuns ((x1 Int)) +:extrafuns ((y1 Int)) +:extrafuns ((x2 Int)) +:extrafuns ((y2 Int)) + +:extrafuns ((a Int)) +:extrafuns ((b Int)) + +:assumption (= x1 x2) +:assumption (= y1 y2) + +:assumption (= (f x1) (f y1)) + +:assumption (not (= x2 y2)) + +:formula true +) diff --git a/test/regress/regress0/uflia/diseqprop.03.smt b/test/regress/regress0/uflia/diseqprop.03.smt new file mode 100644 index 000000000..80c4eb822 --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.03.smt @@ -0,0 +1,20 @@ +(benchmark test +:logic QF_UFLIA +:extrafuns ((f Int Int)) +:extrafuns ((x1 Int)) +:extrafuns ((y1 Int)) +:extrafuns ((x2 Int)) +:extrafuns ((y2 Int)) + +:extrafuns ((a Int)) +:extrafuns ((b Int)) + +:assumption (= x1 x2) + +:assumption (= (f x1) (f y1)) + +:assumption (not (= x2 y2)) +:assumption (= y1 y2) + +:formula true +) diff --git a/test/regress/regress0/uflia/diseqprop.04.smt b/test/regress/regress0/uflia/diseqprop.04.smt new file mode 100644 index 000000000..f07a0f373 --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.04.smt @@ -0,0 +1,20 @@ +(benchmark test +:logic QF_UFLIA +:extrafuns ((f Int Int)) +:extrafuns ((x1 Int)) +:extrafuns ((y1 Int)) +:extrafuns ((x2 Int)) +:extrafuns ((y2 Int)) + +:extrafuns ((a Int)) +:extrafuns ((b Int)) + +:assumption (= y1 y2) + +:assumption (= (f x1) (f y1)) + +:assumption (not (= x2 y2)) +:assumption (= x1 x2) + +:formula true +) diff --git a/test/regress/regress0/uflia/diseqprop.05.smt b/test/regress/regress0/uflia/diseqprop.05.smt new file mode 100644 index 000000000..5510e57c9 --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.05.smt @@ -0,0 +1,20 @@ +(benchmark test +:logic QF_UFLIA +:extrafuns ((f Int Int)) +:extrafuns ((x1 Int)) +:extrafuns ((y1 Int)) +:extrafuns ((x2 Int)) +:extrafuns ((y2 Int)) + +:extrafuns ((a Int)) +:extrafuns ((b Int)) + +:assumption (= x1 x2) +:assumption (= y1 y2) + +:assumption (= (f x1) (f y1)) +:assumption (= x2 1) +:assumption (= y2 2) + +:formula true +) diff --git a/test/regress/regress0/uflia/diseqprop.06.smt b/test/regress/regress0/uflia/diseqprop.06.smt new file mode 100644 index 000000000..b27a5a73c --- /dev/null +++ b/test/regress/regress0/uflia/diseqprop.06.smt @@ -0,0 +1,21 @@ +(benchmark test +:logic QF_UFLIA +:extrafuns ((f Int Int)) +:extrafuns ((x1 Int)) +:extrafuns ((y1 Int)) +:extrafuns ((x2 Int)) +:extrafuns ((y2 Int)) + +:extrafuns ((a Int)) +:extrafuns ((b Int)) + +:assumption (= x1 x2) +:assumption (= y1 y2) + +:assumption (= x2 1) +:assumption (= y2 2) + +:assumption (= (f x1) (f y1)) + +:formula true +)