summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arrays/theory_arrays.cpp209
-rw-r--r--src/theory/strings/sequences_rewriter.cpp6
-rw-r--r--src/theory/strings/strings_entail.cpp125
-rw-r--r--src/theory/strings/strings_entail.h12
-rw-r--r--src/theory/theory_proof_step_buffer.cpp114
-rw-r--r--src/theory/theory_proof_step_buffer.h23
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress0/strings/issue5090.smt232
8 files changed, 347 insertions, 175 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3dc19d39b..28953ab05 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -643,115 +643,131 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
return;
}
Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
- switch (node.getKind()) {
- case kind::EQUAL:
+ Kind nk = node.getKind();
+ if (nk == kind::EQUAL)
+ {
// Add the trigger for equality
// NOTE: note that if the equality is true or false already, it might not be added
d_equalityEngine->addTriggerPredicate(node);
- break;
- case kind::SELECT: {
+ return;
+ }
+ else if (d_equalityEngine->hasTerm(node))
+ {
// Invariant: array terms should be preregistered before being added to the equality engine
- if (d_equalityEngine->hasTerm(node))
+ Assert(nk != kind::SELECT
+ || d_isPreRegistered.find(node) != d_isPreRegistered.end());
+ return;
+ }
+ // add to equality engine and the may equality engine
+ TypeNode nodeType = node.getType();
+ if (nodeType.isArray())
+ {
+ // index type should not be an array, otherwise we throw a logic exception
+ if (nodeType.getArrayIndexType().isArray())
{
- Assert(d_isPreRegistered.find(node) != d_isPreRegistered.end());
- return;
+ std::stringstream ss;
+ ss << "Arrays cannot be indexed by array types, offending array type is "
+ << nodeType;
+ throw LogicException(ss.str());
}
- // Reads
- TNode store = d_equalityEngine->getRepresentative(node[0]);
-
- // The may equal needs the store
- d_mayEqualEqualityEngine.addTerm(store);
+ d_mayEqualEqualityEngine.addTerm(node);
+ }
+ d_equalityEngine->addTerm(node);
- if (node.getType().isArray())
- {
- d_mayEqualEqualityEngine.addTerm(node);
- d_equalityEngine->addTerm(node);
- }
- else
+ switch (node.getKind())
+ {
+ case kind::SELECT:
{
- d_equalityEngine->addTerm(node);
- }
- Assert((d_isPreRegistered.insert(node), true));
+ // Reads
+ TNode store = d_equalityEngine->getRepresentative(node[0]);
- Assert(d_equalityEngine->getRepresentative(store) == store);
- d_infoMap.addIndex(store, node[1]);
+ // The may equal needs the store
+ d_mayEqualEqualityEngine.addTerm(store);
- // Synchronize d_constReadsContext with SAT context
- Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel());
- while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) {
- d_constReadsContext->push();
- }
+ Assert((d_isPreRegistered.insert(node), true));
- // Record read in sharing data structure
- TNode index = d_equalityEngine->getRepresentative(node[1]);
- if (!options::arraysWeakEquivalence() && index.isConst()) {
- CTNodeList* temp;
- CNodeNListMap::iterator it = d_constReads.find(index);
- if (it == d_constReads.end()) {
- temp = new(true) CTNodeList(d_constReadsContext);
- d_constReads[index] = temp;
+ Assert(d_equalityEngine->getRepresentative(store) == store);
+ d_infoMap.addIndex(store, node[1]);
+
+ // Synchronize d_constReadsContext with SAT context
+ Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel());
+ while (d_constReadsContext->getLevel() < getSatContext()->getLevel())
+ {
+ d_constReadsContext->push();
}
- else {
- temp = (*it).second;
+
+ // Record read in sharing data structure
+ TNode index = d_equalityEngine->getRepresentative(node[1]);
+ if (!options::arraysWeakEquivalence() && index.isConst())
+ {
+ CTNodeList* temp;
+ CNodeNListMap::iterator it = d_constReads.find(index);
+ if (it == d_constReads.end())
+ {
+ temp = new (true) CTNodeList(d_constReadsContext);
+ d_constReads[index] = temp;
+ }
+ else
+ {
+ temp = (*it).second;
+ }
+ temp->push_back(node);
+ d_constReadsList.push_back(node);
+ }
+ else
+ {
+ d_reads.push_back(node);
}
- temp->push_back(node);
- d_constReadsList.push_back(node);
- }
- else {
- d_reads.push_back(node);
- }
- checkRowForIndex(node[1], store);
- break;
- }
- case kind::STORE: {
- if (d_equalityEngine->hasTerm(node))
- {
+ checkRowForIndex(node[1], store);
break;
}
- d_equalityEngine->addTerm(node);
-
- TNode a = d_equalityEngine->getRepresentative(node[0]);
+ case kind::STORE:
+ {
+ TNode a = d_equalityEngine->getRepresentative(node[0]);
- if (node.isConst()) {
- // Can't use d_mayEqualEqualityEngine to merge node with a because they are both constants,
- // so just set the default value manually for node.
- Assert(a == node[0]);
- d_mayEqualEqualityEngine.addTerm(node);
- Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
- Assert(d_mayEqualEqualityEngine.getRepresentative(a) == a);
- DefValMap::iterator it = d_defValues.find(a);
- Assert(it != d_defValues.end());
- d_defValues[node] = (*it).second;
- }
- else {
- d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true);
- Assert(d_mayEqualEqualityEngine.consistent());
- }
+ if (node.isConst())
+ {
+ // Can't use d_mayEqualEqualityEngine to merge node with a because they
+ // are both constants, so just set the default value manually for node.
+ Assert(a == node[0]);
+ d_mayEqualEqualityEngine.addTerm(node);
+ Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
+ Assert(d_mayEqualEqualityEngine.getRepresentative(a) == a);
+ DefValMap::iterator it = d_defValues.find(a);
+ Assert(it != d_defValues.end());
+ d_defValues[node] = (*it).second;
+ }
+ else
+ {
+ d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true);
+ Assert(d_mayEqualEqualityEngine.consistent());
+ }
- TNode i = node[1];
- TNode v = node[2];
- NodeManager* nm = NodeManager::currentNM();
- Node ni = nm->mkNode(kind::SELECT, node, i);
- if (!d_equalityEngine->hasTerm(ni))
- {
- preRegisterTermInternal(ni);
- }
+ TNode i = node[1];
+ TNode v = node[2];
+ NodeManager* nm = NodeManager::currentNM();
+ Node ni = nm->mkNode(kind::SELECT, node, i);
+ if (!d_equalityEngine->hasTerm(ni))
+ {
+ preRegisterTermInternal(ni);
+ }
- // Apply RIntro1 Rule
- d_equalityEngine->assertEquality(
- ni.eqNode(v), true, d_true, theory::eq::MERGED_THROUGH_ROW1);
+ // Apply RIntro1 Rule
+ d_equalityEngine->assertEquality(
+ ni.eqNode(v), true, d_true, theory::eq::MERGED_THROUGH_ROW1);
- d_infoMap.addStore(node, node);
- d_infoMap.addInStore(a, node);
- d_infoMap.setModelRep(node, node);
+ d_infoMap.addStore(node, node);
+ d_infoMap.addInStore(a, node);
+ d_infoMap.setModelRep(node, node);
- //Add-Store for Weak Equivalence
- if (options::arraysWeakEquivalence()) {
- Assert(weakEquivGetRep(node[0]) == weakEquivGetRep(a));
- Assert(weakEquivGetRep(node) == node);
- d_infoMap.setWeakEquivPointer(node, node[0]);
- d_infoMap.setWeakEquivIndex(node, node[1]);
+ // Add-Store for Weak Equivalence
+ if (options::arraysWeakEquivalence())
+ {
+ Assert(weakEquivGetRep(node[0]) == weakEquivGetRep(a));
+ Assert(weakEquivGetRep(node) == node);
+ d_infoMap.setWeakEquivPointer(node, node[0]);
+ d_infoMap.setWeakEquivIndex(node, node[1]);
#ifdef CVC4_ASSERTIONS
checkWeakEquiv(false);
#endif
@@ -761,33 +777,18 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
break;
}
case kind::STORE_ALL: {
- if (d_equalityEngine->hasTerm(node))
- {
- break;
- }
ArrayStoreAll storeAll = node.getConst<ArrayStoreAll>();
Node defaultValue = storeAll.getValue();
if (!defaultValue.isConst()) {
throw LogicException("Array theory solver does not yet support non-constant default values for arrays");
}
d_infoMap.setConstArr(node, node);
- d_mayEqualEqualityEngine.addTerm(node);
Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
- d_equalityEngine->addTerm(node);
d_defValues[node] = defaultValue;
break;
}
default:
- // Variables etc
- if (node.getType().isArray()) {
- // The may equal needs the node
- d_mayEqualEqualityEngine.addTerm(node);
- d_equalityEngine->addTerm(node);
- }
- else {
- d_equalityEngine->addTerm(node);
- }
-
+ // Variables etc, already processed above
break;
}
// Invariant: preregistered terms are exactly the terms in the equality engine
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 29c0aa2d5..eb59813b0 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -463,7 +463,8 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
// (= (str.++ "A" x y) (str.++ x "AB" z)) --->
// (and (= (str.++ "A" x) (str.++ x "A")) (= y (str.++ "B" z)))
std::vector<Node> rpfxv1;
- if (StringsEntail::stripSymbolicLength(pfxv1, rpfxv1, 1, lenPfx0))
+ if (StringsEntail::stripSymbolicLength(
+ pfxv1, rpfxv1, 1, lenPfx0, true))
{
std::vector<Node> sfxv0(v0.begin() + i, v0.end());
pfxv1.insert(pfxv1.end(), v1.begin() + j, v1.end());
@@ -490,7 +491,8 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
// (= (str.++ x "AB" z) (str.++ "A" x y)) --->
// (and (= (str.++ x "A") (str.++ "A" x)) (= (str.++ "B" z) y))
std::vector<Node> rpfxv0;
- if (StringsEntail::stripSymbolicLength(pfxv0, rpfxv0, 1, lenPfx1))
+ if (StringsEntail::stripSymbolicLength(
+ pfxv0, rpfxv0, 1, lenPfx1, true))
{
pfxv0.insert(pfxv0.end(), v0.begin() + i, v0.end());
std::vector<Node> sfxv1(v1.begin() + j, v1.end());
diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index b2c2c3cd3..0d7866ca2 100644
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -111,95 +111,92 @@ bool StringsEntail::canConstantContainList(Node c,
bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1,
std::vector<Node>& nr,
int dir,
- Node& curr)
+ Node& curr,
+ bool strict)
{
Assert(dir == 1 || dir == -1);
Assert(nr.empty());
NodeManager* nm = NodeManager::currentNM();
Node zero = nm->mkConst(CVC4::Rational(0));
bool ret = false;
- bool success;
+ bool success = true;
unsigned sindex = 0;
- do
+ while (success && curr != zero && sindex < n1.size())
{
Assert(!curr.isNull());
success = false;
- if (curr != zero && sindex < n1.size())
+ unsigned sindex_use = dir == 1 ? sindex : ((n1.size() - 1) - sindex);
+ if (n1[sindex_use].isConst())
{
- unsigned sindex_use = dir == 1 ? sindex : ((n1.size() - 1) - sindex);
- if (n1[sindex_use].isConst())
+ // could strip part of a constant
+ Node lowerBound = ArithEntail::getConstantBound(Rewriter::rewrite(curr));
+ if (!lowerBound.isNull())
{
- // could strip part of a constant
- Node lowerBound =
- ArithEntail::getConstantBound(Rewriter::rewrite(curr));
- if (!lowerBound.isNull())
+ Assert(lowerBound.isConst());
+ Rational lbr = lowerBound.getConst<Rational>();
+ if (lbr.sgn() > 0)
{
- Assert(lowerBound.isConst());
- Rational lbr = lowerBound.getConst<Rational>();
- if (lbr.sgn() > 0)
+ Assert(ArithEntail::check(curr, true));
+ Node s = n1[sindex_use];
+ size_t slen = Word::getLength(s);
+ Node ncl = nm->mkConst(CVC4::Rational(slen));
+ Node next_s = nm->mkNode(MINUS, lowerBound, ncl);
+ next_s = Rewriter::rewrite(next_s);
+ Assert(next_s.isConst());
+ // we can remove the entire constant
+ if (next_s.getConst<Rational>().sgn() >= 0)
{
- Assert(ArithEntail::check(curr, true));
- Node s = n1[sindex_use];
- size_t slen = Word::getLength(s);
- Node ncl = nm->mkConst(CVC4::Rational(slen));
- Node next_s = nm->mkNode(MINUS, lowerBound, ncl);
- next_s = Rewriter::rewrite(next_s);
- Assert(next_s.isConst());
- // we can remove the entire constant
- if (next_s.getConst<Rational>().sgn() >= 0)
+ curr = Rewriter::rewrite(nm->mkNode(MINUS, curr, ncl));
+ success = true;
+ sindex++;
+ }
+ else
+ {
+ // we can remove part of the constant
+ // lower bound minus the length of a concrete string is negative,
+ // hence lowerBound cannot be larger than long max
+ Assert(lbr < Rational(String::maxSize()));
+ curr = Rewriter::rewrite(nm->mkNode(MINUS, curr, lowerBound));
+ uint32_t lbsize = lbr.getNumerator().toUnsignedInt();
+ Assert(lbsize < slen);
+ if (dir == 1)
{
- curr = Rewriter::rewrite(nm->mkNode(MINUS, curr, ncl));
- success = true;
- sindex++;
+ // strip partially from the front
+ nr.push_back(Word::prefix(s, lbsize));
+ n1[sindex_use] = Word::suffix(s, slen - lbsize);
}
else
{
- // we can remove part of the constant
- // lower bound minus the length of a concrete string is negative,
- // hence lowerBound cannot be larger than long max
- Assert(lbr < Rational(String::maxSize()));
- curr = Rewriter::rewrite(nm->mkNode(MINUS, curr, lowerBound));
- uint32_t lbsize = lbr.getNumerator().toUnsignedInt();
- Assert(lbsize < slen);
- if (dir == 1)
- {
- // strip partially from the front
- nr.push_back(Word::prefix(s, lbsize));
- n1[sindex_use] = Word::suffix(s, slen - lbsize);
- }
- else
- {
- // strip partially from the back
- nr.push_back(Word::suffix(s, lbsize));
- n1[sindex_use] = Word::prefix(s, slen - lbsize);
- }
- ret = true;
+ // strip partially from the back
+ nr.push_back(Word::suffix(s, lbsize));
+ n1[sindex_use] = Word::prefix(s, slen - lbsize);
}
- Assert(ArithEntail::check(curr));
- }
- else
- {
- // we cannot remove the constant
+ ret = true;
}
+ Assert(ArithEntail::check(curr));
}
- }
- else
- {
- Node next_s = NodeManager::currentNM()->mkNode(
- MINUS,
- curr,
- NodeManager::currentNM()->mkNode(STRING_LENGTH, n1[sindex_use]));
- next_s = Rewriter::rewrite(next_s);
- if (ArithEntail::check(next_s))
+ else
{
- success = true;
- curr = next_s;
- sindex++;
+ // we cannot remove the constant
}
}
}
- } while (success);
- if (sindex > 0)
+ else
+ {
+ Node next_s = NodeManager::currentNM()->mkNode(
+ MINUS,
+ curr,
+ NodeManager::currentNM()->mkNode(STRING_LENGTH, n1[sindex_use]));
+ next_s = Rewriter::rewrite(next_s);
+ if (ArithEntail::check(next_s))
+ {
+ success = true;
+ curr = next_s;
+ sindex++;
+ }
+ }
+ }
+ if (sindex > 0 && (!strict || curr == zero))
{
if (dir == 1)
{
diff --git a/src/theory/strings/strings_entail.h b/src/theory/strings/strings_entail.h
index 3eb77c5f5..6d16842cd 100644
--- a/src/theory/strings/strings_entail.h
+++ b/src/theory/strings/strings_entail.h
@@ -67,10 +67,11 @@ class StringsEntail
/** strip symbolic length
*
- * This function strips off components of n1 whose length is less than
- * or equal to argument curr, and stores them in nr. The direction
- * dir determines whether the components are removed from the start
- * or end of n1.
+ * This function strips off components of n1 whose length is less than or
+ * equal to argument curr, and stores them in nr. The direction dir
+ * determines whether the components are removed from the start or end of n1.
+ * If `strict` is set to true, then the function only returns true if full
+ * length `curr` can be stripped.
*
* In detail, this function updates n1 to n1' such that:
* If dir=1,
@@ -107,7 +108,8 @@ class StringsEntail
static bool stripSymbolicLength(std::vector<Node>& n1,
std::vector<Node>& nr,
int dir,
- Node& curr);
+ Node& curr,
+ bool strict = false);
/** component contains
* This function is used when rewriting str.contains( t1, t2 ), where
* n1 is the vector form of t1
diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/theory/theory_proof_step_buffer.cpp
index 8a518b49a..97936011b 100644
--- a/src/theory/theory_proof_step_buffer.cpp
+++ b/src/theory/theory_proof_step_buffer.cpp
@@ -90,5 +90,119 @@ Node TheoryProofStepBuffer::applyPredElim(Node src,
return srcRew;
}
+Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n)
+{
+ if (n.getKind() != kind::OR)
+ {
+ return elimDoubleNegLit(n);
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<Node> children{n.begin(), n.end()};
+ std::vector<Node> childrenEqs;
+ // eliminate double neg for each lit. Do it first because it may expose
+ // duplicates
+ bool hasDoubleNeg = false;
+ for (unsigned i = 0; i < children.size(); ++i)
+ {
+ if (children[i].getKind() == kind::NOT
+ && children[i][0].getKind() == kind::NOT)
+ {
+ hasDoubleNeg = true;
+ childrenEqs.push_back(children[i].eqNode(children[i][0][0]));
+ addStep(PfRule::MACRO_SR_PRED_INTRO,
+ {},
+ {childrenEqs.back()},
+ childrenEqs.back());
+ // update child
+ children[i] = children[i][0][0];
+ }
+ else
+ {
+ childrenEqs.push_back(children[i].eqNode(children[i]));
+ addStep(PfRule::REFL, {}, {children[i]}, childrenEqs.back());
+ }
+ }
+ if (hasDoubleNeg)
+ {
+ Node oldn = n;
+ n = nm->mkNode(kind::OR, children);
+ // Create a congruence step to justify replacement of each doubly negated
+ // literal. This is done to avoid having to use MACRO_SR_PRED_TRANSFORM
+ // from the old clause to the new one, which, under the standard rewriter,
+ // may not hold. An example is
+ //
+ // ---------------------------------------------------------------------
+ // (or (or (not x2) x1 x2) (not (not x2))) = (or (or (not x2) x1 x2) x2)
+ //
+ // which fails due to factoring not happening after flattening.
+ //
+ // Using congruence only the
+ //
+ // ------------------ MACRO_SR_PRED_INTRO
+ // (not (not t)) = t
+ //
+ // steps are added, which, since double negation is eliminated in a
+ // pre-rewrite in the Boolean rewriter, will always hold under the
+ // standard rewriter.
+ Node congEq = oldn.eqNode(n);
+ addStep(PfRule::CONG,
+ childrenEqs,
+ {ProofRuleChecker::mkKindNode(kind::OR)},
+ congEq);
+ // add an equality resolution step to derive normalize clause
+ addStep(PfRule::EQ_RESOLVE, {oldn, congEq}, {}, n);
+ }
+ children.clear();
+ // remove duplicates while keeping the order of children
+ std::unordered_set<TNode, TNodeHashFunction> clauseSet;
+ unsigned size = n.getNumChildren();
+ for (unsigned i = 0; i < size; ++i)
+ {
+ if (clauseSet.count(n[i]))
+ {
+ continue;
+ }
+ children.push_back(n[i]);
+ clauseSet.insert(n[i]);
+ }
+ // if factoring changed
+ if (children.size() < size)
+ {
+ Node factored = children.empty()
+ ? nm->mkConst<bool>(false)
+ : children.size() == 1 ? children[0]
+ : nm->mkNode(kind::OR, children);
+ // don't overwrite what already has a proof step to avoid cycles
+ addStep(PfRule::FACTORING, {n}, {}, factored);
+ n = factored;
+ }
+ // nothing to order
+ if (children.size() < 2)
+ {
+ return n;
+ }
+ // order
+ std::sort(children.begin(), children.end());
+ Node ordered = nm->mkNode(kind::OR, children);
+ // if ordering changed
+ if (ordered != n)
+ {
+ // don't overwrite what already has a proof step to avoid cycles
+ addStep(PfRule::REORDERING, {n}, {ordered}, ordered);
+ }
+ return ordered;
+}
+
+Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
+{
+ // eliminate double neg
+ if (n.getKind() == kind::NOT && n[0].getKind() == kind::NOT)
+ {
+ addStep(PfRule::MACRO_SR_PRED_TRANSFORM, {n}, {n[0][0]}, n[0][0]);
+ return n[0][0];
+ }
+ return n;
+}
+
} // namespace theory
} // namespace CVC4
diff --git a/src/theory/theory_proof_step_buffer.h b/src/theory/theory_proof_step_buffer.h
index 55b4ee1c0..554d7656a 100644
--- a/src/theory/theory_proof_step_buffer.h
+++ b/src/theory/theory_proof_step_buffer.h
@@ -73,6 +73,29 @@ class TheoryProofStepBuffer : public ProofStepBuffer
MethodId ids = MethodId::SB_DEFAULT,
MethodId idr = MethodId::RW_REWRITE);
//---------------------------- end utilities builtin proof rules
+
+ //---------------------------- utility methods for normalizing clauses
+ /**
+ * Normalizes a non-unit clause (an OR node) according to factoring and
+ * reordering, i.e. removes duplicates and reorders literals (according to
+ * node ids). Moreover it eliminates double negations, which can be done also
+ * for unit clauses (a arbitrary Boolean node). All normalization steps are
+ * tracked via proof steps added to this proof step buffer.
+ *
+ * @param n the clause to be normalized
+ * @return the normalized clause node
+ */
+ Node factorReorderElimDoubleNeg(Node n);
+
+ /**
+ * Eliminates double negation of a literal if it has the form
+ * (not (not t))
+ * If the elimination happens, a step is added to this proof step buffer.
+ *
+ * @param n the node to have the top-level double negation eliminated
+ * @return the normalized clause node
+ */
+ Node elimDoubleNegLit(Node n);
};
} // namespace theory
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c6f3b85f5..5f9465562 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -988,6 +988,7 @@ set(regress_0_tests
regress0/strings/issue4674-recomp-nf.smt2
regress0/strings/issue4820.smt2
regress0/strings/issue4915.smt2
+ regress0/strings/issue5090.smt2
regress0/strings/itos-entail.smt2
regress0/strings/large-model.smt2
regress0/strings/leadingzero001.smt2
diff --git a/test/regress/regress0/strings/issue5090.smt2 b/test/regress/regress0/strings/issue5090.smt2
new file mode 100644
index 000000000..44a57d4d2
--- /dev/null
+++ b/test/regress/regress0/strings/issue5090.smt2
@@ -0,0 +1,32 @@
+; COMMAND-LINE: --strings-exp --incremental
+(set-logic QF_S)
+(declare-const Str0 String)
+(declare-const Str1 String)
+(declare-const Str2 String)
+(declare-const Str3 String)
+(declare-const Str4 String)
+(declare-const Str5 String)
+(declare-const Str6 String)
+(declare-const Str7 String)
+(declare-const Str8 String)
+(declare-const Str9 String)
+(declare-const Str10 String)
+(declare-const Str11 String)
+(declare-const Str12 String)
+(declare-const Str13 String)
+(declare-const Str14 String)
+(declare-const Str15 String)
+(declare-const Str16 String)
+(declare-const Str17 String)
+(declare-const Str18 String)
+(declare-const Str19 String)
+(assert (str.in_re Str19(re.opt (str.to_re Str10))))
+(assert (str.in_re Str9(re.opt (str.to_re Str18))))
+(assert (str.in_re (str.replace Str12 "jkngjj" Str14)(re.opt (str.to_re (str.++ Str13 "spifluyxzmbznnejkmfajdisgnyfeogvtwxuclzmrlmjmmwhly" Str5 Str19 "rsjusudbyjoyfpwbpasemhhxoayzouhoaekszsvhbsmnysbcih")))))
+(assert (str.in_re Str13(re.opt (str.to_re Str3))))
+(push 1)
+(assert (str.in_re (str.++ Str12 (str.++ Str5 Str16 Str13) (str.++ Str5 "tqckdn" "hvhftx" (str.replace Str12 "jkngjj" Str14)) "trcuij" "ovnscketrkugxyqewkvuvondgahkfzwczexnyiziwhyqlomqie")(re.opt (str.to_re Str8))))
+(push 1)
+(assert (str.in_re (str.++ Str13 (str.++ Str5 Str16 Str13))(re.++ (str.to_re (str.++ Str5 Str16 Str13)) (str.to_re "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs" ))))
+(set-info :status sat)
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback