diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-18 11:35:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-18 11:35:24 -0500 |
commit | d091aa8d85e6336b469c312b9cc4c4e426a82094 (patch) | |
tree | 174c3fbcac3b81b27d1efb49b411490a3142d4ea | |
parent | 15128d91b6bdbff4141417855743f910950f9cc8 (diff) | |
parent | e040d5e9e9d8c01138b4b961a1118b7342735d87 (diff) |
Merge branch 'master' into fixNightlyCompfixNightlyComp
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 209 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 6 | ||||
-rw-r--r-- | src/theory/strings/strings_entail.cpp | 125 | ||||
-rw-r--r-- | src/theory/strings/strings_entail.h | 12 | ||||
-rw-r--r-- | src/theory/theory_proof_step_buffer.cpp | 114 | ||||
-rw-r--r-- | src/theory/theory_proof_step_buffer.h | 23 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/issue5090.smt2 | 32 |
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) |