summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arrays/theory_arrays.cpp5
-rw-r--r--src/theory/theory.h1
-rw-r--r--src/theory/theory_engine.cpp44
-rw-r--r--src/theory/uf/equality_engine.cpp221
-rw-r--r--src/theory/uf/equality_engine.h42
-rw-r--r--test/regress/regress0/aufbv/dubreva005ue.delta01.smt33
-rw-r--r--test/regress/regress0/aufbv/dubreva005ue.smt223
-rw-r--r--test/regress/regress0/uflia/diseqprop.01.smt19
-rw-r--r--test/regress/regress0/uflia/diseqprop.02.smt20
-rw-r--r--test/regress/regress0/uflia/diseqprop.03.smt20
-rw-r--r--test/regress/regress0/uflia/diseqprop.04.smt20
-rw-r--r--test/regress/regress0/uflia/diseqprop.05.smt20
-rw-r--r--test/regress/regress0/uflia/diseqprop.06.smt21
13 files changed, 620 insertions, 69 deletions
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<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
+ for (; it != it_end; ++ it) {
+ TNode t1 = (*it);
+ context::CDList<TNode>::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<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);
+ 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<EqualityNodeId> 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<EqualityPair> 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<TaggedEquality> 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
+)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback