From: Andrew Reynolds Date: Tue, 7 Jun 2022 00:49:15 +0000 (-0500) Subject: Use STRING_NTH in strings reductions and eliminate STRING_TO_CODE (#8851) X-Git-Tag: cvc5-1.0.1~64 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8c3db9e0e904beaacfbe3328bc9625b09952bdf;p=cvc5.git Use STRING_NTH in strings reductions and eliminate STRING_TO_CODE (#8851) This updates our string reductions for `to_lower`, `to_upper`, `from_int`, `to_int` to use STRING_NTH instead of STRING_TO_CODE applied to STRING_SUBSTR. It optionally replaces STRING_TO_CODE with STRING_NTH during preprocessing (true by default). This is work towards efficient support for `to_lower`/`to_upper`. --- diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index c5cb6aa22..7407bcdf1 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -242,3 +242,11 @@ name = "Strings Theory" type = "uint64_t" default = "65536" help = "The maximum size of string values in models" + +[[option]] + name = "stringsCodeElim" + category = "expert" + long = "strings-code-elim" + type = "bool" + default = "true" + help = "eliminate code points during preprocessing" diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 0212ce686..3fb4ec305 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -865,7 +865,7 @@ Node ArithEntail::getConstantBoundLength(TNode s, bool isLower) const size_t len = Word::getLength(s); ret = nm->mkConstInt(Rational(len)); } - else if (sk == SEQ_UNIT) + else if (sk == SEQ_UNIT || sk == STRING_UNIT) { ret = nm->mkConstInt(1); } diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index baa08c1ca..8c74af50f 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -2447,19 +2447,9 @@ void CoreSolver::processDeqExtensionality(Node n1, Node n2) TypeNode intType = nm->integerType(); Node k = sc->mkSkolemFun(SkolemFunId::STRINGS_DEQ_DIFF, intType, n1, n2); Node deq = eq.negate(); - Node ss1, ss2; - if (n1.getType().isString()) - { - // substring of length 1 - ss1 = nm->mkNode(STRING_SUBSTR, n1, k, d_one); - ss2 = nm->mkNode(STRING_SUBSTR, n2, k, d_one); - } - else - { - // as an optimization, for sequences, use seq.nth - ss1 = nm->mkNode(SEQ_NTH, n1, k); - ss2 = nm->mkNode(SEQ_NTH, n2, k); - } + // use seq.nth instead of substr + Node ss1 = nm->mkNode(SEQ_NTH, n1, k); + Node ss2 = nm->mkNode(SEQ_NTH, n2, k); // disequality between nth/substr Node conc1 = ss1.eqNode(ss2).negate(); diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index e30750474..b85e3460b 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -99,6 +99,26 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard) Node code_range = mkCodeRange(t, alphaCard); lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1); } + else if (tk == SEQ_NTH) + { + if (t[0].getType().isString()) + { + Node s = t[0]; + Node n = t[1]; + // start point is greater than or equal zero + Node c1 = nm->mkNode(GEQ, n, nm->mkConstInt(0)); + // start point is less than end of string + Node c2 = nm->mkNode(GT, nm->mkNode(STRING_LENGTH, s), n); + // check whether this application of seq.nth is defined. + Node cond = nm->mkNode(AND, c1, c2); + Node code_range = mkCodeRange(t, alphaCard); + // the lemma for `seq.nth` + lemma = nm->mkNode(ITE, cond, code_range, t.eqNode(nm->mkConstInt(Rational(-1)))); + // IF: n >=0 AND n < len( s ) + // THEN: 0 <= (seq.nth s n) < |A| + // ELSE: (seq.nth s n) = -1 + } + } else if (tk == STRING_INDEXOF || tk == STRING_INDEXOF_RE) { // (and diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5858af78e..f371516b6 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -89,6 +89,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_stringsFmf(env, valuation, d_termReg), d_strat(d_env), d_absModelCounter(0), + d_strGapModelCounter(0), d_cpacb(*this) { d_termReg.finishInit(&d_im); @@ -140,6 +141,7 @@ void TheoryStrings::finishInit() d_equalityEngine->addFunctionKind(kind::STRING_IN_REGEXP, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_TO_CODE, eagerEval); d_equalityEngine->addFunctionKind(kind::SEQ_UNIT, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_UNIT, false); // `seq.nth` is not always defined, and so we do not evaluate it eagerly. d_equalityEngine->addFunctionKind(kind::SEQ_NTH, false); // extended functions @@ -162,6 +164,7 @@ void TheoryStrings::finishInit() // memberships are not relevant for model building d_valuation.setIrrelevantKind(kind::STRING_IN_REGEXP); + d_valuation.setIrrelevantKind(kind::STRING_LEQ); // seq nth doesn't always evaluate d_valuation.setUnevaluatedKind(SEQ_NTH); } @@ -209,6 +212,8 @@ void TheoryStrings::presolve() { bool TheoryStrings::collectModelValues(TheoryModel* m, const std::set& termSet) { + d_absModelCounter = 0; + d_strGapModelCounter = 0; if (TraceIsOn("strings-debug-model")) { Trace("strings-debug-model") @@ -447,15 +452,17 @@ bool TheoryStrings::collectModelInfoType( } // is it an equivalence class with a seq.unit term? Node assignedValue; - if (nfe.d_nf[0].getKind() == SEQ_UNIT) + if (nfe.d_nf[0].getKind() == SEQ_UNIT + || nfe.d_nf[0].getKind() == STRING_UNIT) { - Node argVal; if (nfe.d_nf[0][0].getType().isStringLike()) { // By this point, we should have assigned model values for the // elements of this sequence type because of the check in the // beginning of this method - argVal = m->getRepresentative(nfe.d_nf[0][0]); + Node argVal = m->getRepresentative(nfe.d_nf[0][0]); + Assert(nfe.d_nf[0].getKind() == SEQ_UNIT); + assignedValue = utils::mkUnit(eqc.getType(), argVal); } else { @@ -463,10 +470,9 @@ bool TheoryStrings::collectModelInfoType( // value of this term, since it might not be available yet, as // it may belong to a theory that has not built its model yet. // Hence, we assign a (non-constant) skeleton (seq.unit argVal). - argVal = nfe.d_nf[0][0]; + assignedValue = nfe.d_nf[0]; } - Assert(!argVal.isNull()) << "No value for " << nfe.d_nf[0][0]; - assignedValue = rewrite(nm->mkNode(SEQ_UNIT, argVal)); + assignedValue = rewrite(assignedValue); Trace("strings-model") << "-> assign via seq.unit: " << assignedValue << std::endl; } @@ -492,7 +498,7 @@ bool TheoryStrings::collectModelInfoType( } else if (options().strings.seqArray != options::SeqArrayMode::NONE) { - TypeNode etype = eqc.getType().getSequenceElementType(); + TypeNode eqcType = eqc.getType(); // determine skeleton based on the write model, if it exists const std::map& writeModel = d_asolver.getWriteModel(eqc); Trace("strings-model") @@ -520,7 +526,7 @@ bool TheoryStrings::collectModelInfoType( continue; } usedWrites.insert(ivalue); - Node wsunit = nm->mkNode(SEQ_UNIT, w.second); + Node wsunit = utils::mkUnit(eqcType, w.second); writes.emplace_back(ivalue, wsunit); } // sort based on index value @@ -547,6 +553,8 @@ bool TheoryStrings::collectModelInfoType( } if (nextIndex > currIndex) { + Trace("strings-model") << "Make skeleton from " << currIndex + << " ... " << nextIndex << std::endl; // allocate arbitrary value to fill gap Assert(conSeq != nullptr); Node base = eqc; @@ -746,18 +754,20 @@ Node TheoryStrings::mkSkeletonFor(Node c) NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); BoundVarManager* bvm = nm->getBoundVarManager(); + TypeNode tn = c.getType(); + Assert(tn.isSequence()); Assert(c.getKind() == CONST_SEQUENCE); const Sequence& sn = c.getConst(); const std::vector& snvec = sn.getVec(); std::vector skChildren; - TypeNode etn = c.getType().getSequenceElementType(); + TypeNode etn = tn.getSequenceElementType(); for (const Node& snv : snvec) { Assert(snv.getType() == etn); Node v = bvm->mkBoundVar(snv, etn); // use a skolem, not a bound variable Node kv = sm->mkPurifySkolem(v, "smv"); - skChildren.push_back(nm->mkNode(SEQ_UNIT, kv)); + skChildren.push_back(utils::mkUnit(tn, kv)); } return utils::mkConcat(skChildren, c.getType()); } @@ -766,23 +776,42 @@ Node TheoryStrings::mkSkeletonFromBase(Node r, size_t currIndex, size_t nextIndex) { + Assert(nextIndex > currIndex); Assert(!r.isNull()); - Assert(r.getType().isSequence()); NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - std::vector cacheVals; - cacheVals.push_back(r); + TypeNode tn = r.getType(); std::vector skChildren; - TypeNode etn = r.getType().getSequenceElementType(); - for (size_t i = currIndex; i < nextIndex; i++) + if (tn.isSequence()) { - cacheVals.push_back(nm->mkConstInt(Rational(currIndex))); - Node kv = sm->mkSkolemFunction( - SkolemFunId::SEQ_MODEL_BASE_ELEMENT, etn, cacheVals); - skChildren.push_back(nm->mkNode(SEQ_UNIT, kv)); - cacheVals.pop_back(); + std::vector cacheVals; + cacheVals.push_back(r); + TypeNode etn = tn.getSequenceElementType(); + for (size_t i = currIndex; i < nextIndex; i++) + { + cacheVals.push_back(nm->mkConstInt(Rational(currIndex))); + Node kv = sm->mkSkolemFunction( + SkolemFunId::SEQ_MODEL_BASE_ELEMENT, etn, cacheVals); + skChildren.push_back(utils::mkUnit(tn, kv)); + cacheVals.pop_back(); + } } - return utils::mkConcat(skChildren, r.getType()); + else + { + // allocate a unique symbolic (unspecified) string of length one, and + // repeat it (nextIndex-currIndex) times. + // Notice that this is guaranteed to be a unique (unspecified) character, + // since the only existing str.unit terms originate from our reductions, + // and hence are only applied to non-negative arguments. If the user + // was able to give arbitrary constraints over str.unit terms, then this + // construction would require a character not used in the model value of + // any other string. + d_strGapModelCounter++; + Node symChar = + utils::mkUnit(tn, nm->mkConstInt(-Rational(d_strGapModelCounter))); + skChildren.resize(nextIndex - currIndex, symChar); + } + return utils::mkConcat(skChildren, tn); } ///////////////////////////////////////////////////////////////////////////// @@ -1150,7 +1179,8 @@ void TheoryStrings::checkRegisterTermsNormalForms() TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector& lems) { Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; - if (atom.getKind() == EQUAL) + Kind ak = atom.getKind(); + if (ak == EQUAL) { // always apply aggressive equality rewrites here Node ret = d_rewriter.rewriteEqualityExt(atom); @@ -1159,7 +1189,7 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector& lems) return TrustNode::mkTrustRewrite(atom, ret, nullptr); } } - if (atom.getKind() == STRING_FROM_CODE) + if (ak == STRING_FROM_CODE) { // str.from_code(t) ---> ite(0 <= t < |A|, t = str.to_code(k), k = "") NodeManager* nm = NodeManager::currentNM(); @@ -1176,10 +1206,20 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector& lems) lems.push_back(SkolemLemma(tnk, k)); return TrustNode::mkTrustRewrite(atom, k, nullptr); } + else if (ak == STRING_TO_CODE && options().strings.stringsCodeElim) + { + // str.to_code(t) ---> ite(str.len(t) = 1, str.nth(t,0), -1) + NodeManager* nm = NodeManager::currentNM(); + Node t = atom[0]; + Node cond = nm->mkNode(EQUAL, nm->mkNode(STRING_LENGTH, t), d_one); + Node ret = nm->mkNode(ITE, cond, nm->mkNode(SEQ_NTH, t, d_zero), d_neg_one); + return TrustNode::mkTrustRewrite(atom, ret, nullptr); + } + TrustNode ret; Node atomRet = atom; if (options().strings.regExpElim != options::RegExpElimMode::OFF - && atom.getKind() == STRING_IN_REGEXP) + && ak == STRING_IN_REGEXP) { // aggressive elimination of regular expression membership ret = d_regexp_elim.eliminateTrusted(atomRet); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index eb58b026b..e700cc4f9 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -313,6 +313,12 @@ class TheoryStrings : public Theory { * we have built, so that unique debug names can be assigned. */ size_t d_absModelCounter; + /** + * For model building, a counter on the number of gaps constructed for + * string terms due to array reasoning. This is to allocate unique unspecified + * characters. + */ + size_t d_strGapModelCounter; /** The care pair argument callback, used for theory combination */ CarePairArgumentCallback d_cpacb; };/* class TheoryStrings */ diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 97ab305a8..284788637 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -358,11 +358,10 @@ Node StringsPreprocess::reduce(Node t, Node xPlusOne = nm->mkNode(ADD, x, one); Node xbv = nm->mkNode(BOUND_VAR_LIST, x); Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, leni)); - Node sx = nm->mkNode(STRING_SUBSTR, itost, x, one); Node ux = nm->mkNode(APPLY_UF, u, x); Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne); Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); - Node c = nm->mkNode(SUB, nm->mkNode(STRING_TO_CODE, sx), c0); + Node c = nm->mkNode(SUB, mkCodePointAtIndex(itost, x), c0); Node ten = nm->mkConstInt(Rational(10)); Node eq = ux1.eqNode(nm->mkNode(ADD, c, nm->mkNode(MULT, ten, ux))); @@ -427,10 +426,7 @@ Node StringsPreprocess::reduce(Node t, Node kc1 = nm->mkNode(GEQ, k, zero); Node kc2 = nm->mkNode(LT, k, lens); Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); - Node codeSk = nm->mkNode( - SUB, - nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)), - c0); + Node codeSk = nm->mkNode(SUB, mkCodePointAtIndex(s, k), c0); Node ten = nm->mkConstInt(Rational(10)); Node kc3 = nm->mkNode( OR, nm->mkNode(LT, codeSk, zero), nm->mkNode(GEQ, codeSk, ten)); @@ -455,10 +451,9 @@ Node StringsPreprocess::reduce(Node t, Node x = SkolemCache::mkIndexVar(t); Node xbv = nm->mkNode(BOUND_VAR_LIST, x); Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, lens)); - Node sx = nm->mkNode(STRING_SUBSTR, s, x, one); Node ux = nm->mkNode(APPLY_UF, u, x); Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(ADD, x, one)); - Node c = nm->mkNode(SUB, nm->mkNode(STRING_TO_CODE, sx), c0); + Node c = nm->mkNode(SUB, mkCodePointAtIndex(s, x), c0); Node eq = ux1.eqNode(nm->mkNode(ADD, c, nm->mkNode(MULT, ten, ux))); Node cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten)); @@ -513,7 +508,7 @@ Node StringsPreprocess::reduce(Node t, // nodes for the case where `seq.nth` is defined. Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre"); Node sk2 = sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); - Node unit = nm->mkNode(SEQ_UNIT, skt); + Node unit = utils::mkUnit(s.getType(), skt); Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, unit, sk2)); // length of first skolem is second argument Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); @@ -528,7 +523,7 @@ Node StringsPreprocess::reduce(Node t, // n >=0 AND n < len( s ) // IMPLIES: s = sk1 ++ unit(skt) ++ sk2 AND // len( sk1 ) = n AND - // ( len( sk2 ) = len( s )- (n+1) + // len( sk2 ) = len( s )- (n+1) asserts.push_back(lemma); retNode = skt; } @@ -856,8 +851,8 @@ Node StringsPreprocess::reduce(Node t, Node i = SkolemCache::mkIndexVar(t); Node bvi = nm->mkNode(BOUND_VAR_LIST, i); - Node ci = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, one)); - Node ri = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, one)); + Node ci = mkCodePointAtIndex(x, i); + Node ri = mkCodePointAtIndex(r, i); Node lb = nm->mkConstInt(Rational(t.getKind() == STRING_TO_UPPER ? 97 : 65)); @@ -1067,6 +1062,13 @@ Node StringsPreprocess::simplifyRec(Node t, std::vector& asserts) return retNode; } } +Node StringsPreprocess::mkCodePointAtIndex(Node x, Node i) +{ + // we use (SEQ_NTH, x, i) instead of + // (STRING_TO_CODE, (STRING_SUBSTR, x, i, 1)) + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(SEQ_NTH, x, i); +} Node StringsPreprocess::processAssertion(Node n, std::vector& asserts) { diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 3c60d3910..e1b2e852b 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -91,6 +91,10 @@ class StringsPreprocess { * visited stores a cache of previous results. */ Node simplifyRec(Node t, std::vector& asserts); + /** + * Makes the term returning the code point of string x at point i. + */ + static Node mkCodePointAtIndex(Node x, Node i); }; } // namespace strings diff --git a/test/api/cpp/proj-issue334.cpp b/test/api/cpp/proj-issue334.cpp index 652a050ce..c6b0c22d1 100644 --- a/test/api/cpp/proj-issue334.cpp +++ b/test/api/cpp/proj-issue334.cpp @@ -22,6 +22,7 @@ int main(void) { Solver slv; slv.setOption("produce-unsat-cores", "true"); + slv.setOption("strings-exp", "true"); Sort s1 = slv.mkBitVectorSort(1); Sort s2 = slv.mkFloatingPointSort(8, 24); Term val = slv.mkBitVector(32, "10000000110010111010111011000101", 2); diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 2e961af07..ec6772707 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2696,6 +2696,8 @@ set(regress_1_tests regress1/strings/strip-endpt-sound.smt2 regress1/strings/substr001.smt2 regress1/strings/tolower-find.smt2 + regress1/strings/to_upper_12.smt2 + regress1/strings/to_upper_over_concat.smt2 regress1/strings/timeout-no-resp.smt2 regress1/strings/type002.smt2 regress1/strings/type003.smt2 diff --git a/test/regress/cli/regress0/arith/projissue469-int-equality.smt2 b/test/regress/cli/regress0/arith/projissue469-int-equality.smt2 index e8bffa564..9171cc385 100644 --- a/test/regress/cli/regress0/arith/projissue469-int-equality.smt2 +++ b/test/regress/cli/regress0/arith/projissue469-int-equality.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --strings-exp ; EXPECT: sat (set-logic ALL) (set-option :nl-ext-ent-conf true) diff --git a/test/regress/cli/regress0/strings/issue5771-eager-pp.smt2 b/test/regress/cli/regress0/strings/issue5771-eager-pp.smt2 index c3049e72f..8c4fc8a65 100644 --- a/test/regress/cli/regress0/strings/issue5771-eager-pp.smt2 +++ b/test/regress/cli/regress0/strings/issue5771-eager-pp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-strings-lazy-pp +; COMMAND-LINE: --no-strings-lazy-pp --strings-exp ; EXPECT: sat (set-logic ALL) (declare-fun a () Int) diff --git a/test/regress/cli/regress0/strings/issue5816-re-kind.smt2 b/test/regress/cli/regress0/strings/issue5816-re-kind.smt2 index a1e7eb7f4..be1f47e75 100644 --- a/test/regress/cli/regress0/strings/issue5816-re-kind.smt2 +++ b/test/regress/cli/regress0/strings/issue5816-re-kind.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-strings-code-elim +; EXPECT: sat (set-logic ALL) (set-info :status sat) (declare-const x String) diff --git a/test/regress/cli/regress0/strings/issue8722-learned-rew.smt2 b/test/regress/cli/regress0/strings/issue8722-learned-rew.smt2 index ed1d73035..03cae69d2 100644 --- a/test/regress/cli/regress0/strings/issue8722-learned-rew.smt2 +++ b/test/regress/cli/regress0/strings/issue8722-learned-rew.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --learned-rewrite +; COMMAND-LINE: --learned-rewrite --strings-exp ; EXPECT: sat (set-logic ALL) (declare-const a String) diff --git a/test/regress/cli/regress0/strings/model-code-point.smt2 b/test/regress/cli/regress0/strings/model-code-point.smt2 index 86cb24fc7..84d1c342b 100644 --- a/test/regress/cli/regress0/strings/model-code-point.smt2 +++ b/test/regress/cli/regress0/strings/model-code-point.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6 --produce-models +; COMMAND-LINE: --lang=smt2.6 --produce-models --no-strings-code-elim ; EXPECT: sat ; EXPECT: ((x "\u{a}")) ; EXPECT: ((y "\u{7f}")) diff --git a/test/regress/cli/regress1/decision/jh-test1.smt2 b/test/regress/cli/regress1/decision/jh-test1.smt2 index 31b72e787..999e03a77 100644 --- a/test/regress/cli/regress1/decision/jh-test1.smt2 +++ b/test/regress/cli/regress1/decision/jh-test1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --decision=justification +; COMMAND-LINE: --decision=justification --no-strings-code-elim ; EXPECT: sat (set-logic ALL) (declare-const size4 String) diff --git a/test/regress/cli/regress1/strings/cee-norn-aes-trivially.smt2 b/test/regress/cli/regress1/strings/cee-norn-aes-trivially.smt2 index 2f8d9904d..5d59358c8 100644 --- a/test/regress/cli/regress1/strings/cee-norn-aes-trivially.smt2 +++ b/test/regress/cli/regress1/strings/cee-norn-aes-trivially.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --arith-eq-solver --ee-mode=distributed -; COMMAND-LINE: --arith-eq-solver --ee-mode=central +; COMMAND-LINE: --arith-eq-solver --ee-mode=distributed --strings-exp +; COMMAND-LINE: --arith-eq-solver --ee-mode=central --strings-exp ; EXPECT: unsat (set-logic ALL) (declare-fun v () String) diff --git a/test/regress/cli/regress1/strings/str-code-sat.smt2 b/test/regress/cli/regress1/strings/str-code-sat.smt2 index 7345e25bb..3ae0de6a8 100644 --- a/test/regress/cli/regress1/strings/str-code-sat.smt2 +++ b/test/regress/cli/regress1/strings/str-code-sat.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-strings-code-elim +; EXPECT: sat (set-logic QF_SLIA) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/cli/regress1/strings/to_upper_12.smt2 b/test/regress/cli/regress1/strings/to_upper_12.smt2 new file mode 100644 index 000000000..293195c97 --- /dev/null +++ b/test/regress/cli/regress1/strings/to_upper_12.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp --seq-array=lazy +; EXPECT: sat +(set-logic QF_SLIA) +(declare-const X String) +(assert (= (str.to_upper X) (str.to_lower X))) +(assert (>= (str.len X) 12)) +(check-sat) diff --git a/test/regress/cli/regress1/strings/to_upper_over_concat.smt2 b/test/regress/cli/regress1/strings/to_upper_over_concat.smt2 new file mode 100644 index 000000000..57a370f36 --- /dev/null +++ b/test/regress/cli/regress1/strings/to_upper_over_concat.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --strings-exp --seq-array=lazy +; EXPECT: sat +(set-logic QF_SLIA) +(declare-const x String) +(declare-const y String) +(declare-const z String) +(declare-const w String) +(assert (not (= (str.to_upper x) (str.to_lower x)))) +(assert (or (= x (str.++ y z)) (= x (str.++ y w)))) +(assert (not (= y ""))) +(assert (not (= z ""))) +(assert (= (str.to_upper y) (str.to_lower y))) +(assert (= (str.to_upper z) (str.to_lower z))) +(assert (> (str.len x) 2)) +(check-sat)