From 31efb570a9d5811fd88a34d4915d7d08c81d13fa Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 28 Feb 2020 22:20:18 -0800 Subject: [PATCH] Add support for str.from_code (#3829) This commit adds support for `str.from_code`. This is work towards supporting the new strings standard. The code currently just does an eager expansion of the operator. The commit also renames `STRING_CODE` to `STRING_TO_CODE` to better reflect the names of the operators in the new standard. --- src/api/cvc4cpp.cpp | 6 +- src/api/cvc4cppkind.h | 15 +++- src/parser/smt2/smt2.cpp | 6 +- src/printer/smt2/smt2_printer.cpp | 6 +- src/theory/evaluator.cpp | 18 ++++- src/theory/strings/extf_solver.cpp | 4 +- src/theory/strings/kinds | 6 +- src/theory/strings/solver_state.cpp | 2 +- src/theory/strings/theory_strings.cpp | 34 +++++++-- .../strings/theory_strings_preprocess.cpp | 18 ++--- .../strings/theory_strings_rewriter.cpp | 45 +++++++++--- src/theory/strings/theory_strings_rewriter.h | 14 +++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/strings/from_code.smt2 | 69 +++++++++++++++++++ test/unit/theory/evaluator_white.h | 4 +- 15 files changed, 204 insertions(+), 44 deletions(-) create mode 100644 test/regress/regress0/strings/from_code.smt2 diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 31453b618..0d24139e8 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -258,7 +258,8 @@ const static std::unordered_map s_kinds{ {STRING_TOLOWER, CVC4::Kind::STRING_TOLOWER}, {STRING_TOUPPER, CVC4::Kind::STRING_TOUPPER}, {STRING_REV, CVC4::Kind::STRING_REV}, - {STRING_CODE, CVC4::Kind::STRING_CODE}, + {STRING_FROM_CODE, CVC4::Kind::STRING_FROM_CODE}, + {STRING_TO_CODE, CVC4::Kind::STRING_TO_CODE}, {STRING_LT, CVC4::Kind::STRING_LT}, {STRING_LEQ, CVC4::Kind::STRING_LEQ}, {STRING_PREFIX, CVC4::Kind::STRING_PREFIX}, @@ -524,7 +525,8 @@ const static std::unordered_map {CVC4::Kind::STRING_TOLOWER, STRING_TOLOWER}, {CVC4::Kind::STRING_TOUPPER, STRING_TOUPPER}, {CVC4::Kind::STRING_REV, STRING_REV}, - {CVC4::Kind::STRING_CODE, STRING_CODE}, + {CVC4::Kind::STRING_FROM_CODE, STRING_FROM_CODE}, + {CVC4::Kind::STRING_TO_CODE, STRING_TO_CODE}, {CVC4::Kind::STRING_LT, STRING_LT}, {CVC4::Kind::STRING_LEQ, STRING_LEQ}, {CVC4::Kind::STRING_PREFIX, STRING_PREFIX}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index eb8575907..d399ad616 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1988,7 +1988,7 @@ enum CVC4_PUBLIC Kind : int32_t */ STRING_REV, /** - * String code. + * String to code. * Returns the code point of a string if it has length one, or returns -1 * otherwise. * Parameters: 1 @@ -1996,7 +1996,18 @@ enum CVC4_PUBLIC Kind : int32_t * Create with: * mkTerm(Kind kind, Term child) */ - STRING_CODE, + STRING_TO_CODE, + /** + * String from code. + * Returns a string containing a single character whose code point matches + * the argument to this function, or the empty string if the argument is + * out-of-bounds. + * Parameters: 1 + * -[1]: Term of Integer sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + STRING_FROM_CODE, /** * String less than. * Returns true if string s1 is (strictly) less than s2 based on a diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ef13d379e..94a273193 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -171,7 +171,9 @@ void Smt2::addStringOperators() { } addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); + addOperator(kind::STRING_FROM_CODE, "str.from_code"); addOperator(kind::STRING_IS_DIGIT, "str.is_digit" ); + // at the moment, we only use this syntax for smt2.6.1 if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1 || getLanguage() == language::input::LANG_SYGUS_V2) @@ -180,7 +182,7 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_STOI, "str.to_int"); addOperator(kind::STRING_IN_REGEXP, "str.in_re"); addOperator(kind::STRING_TO_REGEXP, "str.to_re"); - addOperator(kind::STRING_CODE, "str.to_code"); + addOperator(kind::STRING_TO_CODE, "str.to_code"); addOperator(kind::STRING_STRREPLALL, "str.replace_all"); } else @@ -189,7 +191,7 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_STOI, "str.to.int"); addOperator(kind::STRING_IN_REGEXP, "str.in.re"); addOperator(kind::STRING_TO_REGEXP, "str.to.re"); - addOperator(kind::STRING_CODE, "str.code"); + addOperator(kind::STRING_TO_CODE, "str.code"); addOperator(kind::STRING_STRREPLALL, "str.replaceall"); } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 13a64a2c3..e3a65ca3f 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -656,7 +656,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::STRING_LT: case kind::STRING_ITOS: case kind::STRING_STOI: - case kind::STRING_CODE: + case kind::STRING_FROM_CODE: + case kind::STRING_TO_CODE: case kind::STRING_TO_REGEXP: case kind::REGEXP_CONCAT: case kind::REGEXP_UNION: @@ -1218,7 +1219,8 @@ static string smtKindString(Kind k, Variant v) case kind::STRING_SUFFIX: return "str.suffixof" ; case kind::STRING_LEQ: return "str.<="; case kind::STRING_LT: return "str.<"; - case kind::STRING_CODE: + case kind::STRING_FROM_CODE: return "str.from_code"; + case kind::STRING_TO_CODE: return v == smt2_6_1_variant ? "str.to_code" : "str.code"; case kind::STRING_ITOS: return v == smt2_6_1_variant ? "str.from_int" : "int.to.str"; diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index a3ea768d4..b827912d5 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -18,6 +18,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "theory/strings/theory_strings_utils.h" #include "theory/theory.h" #include "util/integer.h" @@ -605,7 +606,22 @@ EvalResult Evaluator::evalInternal( break; } - case kind::STRING_CODE: + case kind::STRING_FROM_CODE: + { + Integer i = results[currNode[0]].d_rat.getNumerator(); + if (i >= 0 && i < strings::utils::getAlphabetCardinality()) + { + std::vector svec = {i.toUnsignedInt()}; + results[currNode] = EvalResult(String(svec)); + } + else + { + results[currNode] = EvalResult(String("")); + } + break; + } + + case kind::STRING_TO_CODE: { const String& s = results[currNode[0]].d_str; if (s.size() == 1) diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 6ab74cf9a..b04b88b31 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -54,7 +54,7 @@ ExtfSolver::ExtfSolver(context::Context* c, d_extt->addFunctionKind(kind::STRING_STRCTN); d_extt->addFunctionKind(kind::STRING_IN_REGEXP); d_extt->addFunctionKind(kind::STRING_LEQ); - d_extt->addFunctionKind(kind::STRING_CODE); + d_extt->addFunctionKind(kind::STRING_TO_CODE); d_extt->addFunctionKind(kind::STRING_TOLOWER); d_extt->addFunctionKind(kind::STRING_TOUPPER); d_extt->addFunctionKind(kind::STRING_REV); @@ -166,7 +166,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd) // context-dependent because it depends on the polarity of n itself isCd = true; } - else if (k != kind::STRING_CODE) + else if (k != kind::STRING_TO_CODE) { NodeManager* nm = NodeManager::currentNM(); Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 965c56ee4..9d12cd906 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -28,7 +28,8 @@ operator STRING_SUFFIX 2 "string suffixof" operator STRING_IS_DIGIT 1 "string isdigit, returns true if argument is a string of length one that represents a digit" operator STRING_ITOS 1 "integer to string" operator STRING_STOI 1 "string to integer (total function)" -operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise" +operator STRING_TO_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise" +operator STRING_FROM_CODE 1 "string from code, returns a string containing a single character whose code point matches the argument to this function, empty string if the argument is out-of-bounds" operator STRING_TOLOWER 1 "string to lowercase conversion" operator STRING_TOUPPER 1 "string to uppercase conversion" operator STRING_REV 1 "string reverse" @@ -108,7 +109,8 @@ typerule STRING_SUFFIX "SimpleTypeRule" typerule STRING_IS_DIGIT "SimpleTypeRule" typerule STRING_ITOS "SimpleTypeRule" typerule STRING_STOI "SimpleTypeRule" -typerule STRING_CODE "SimpleTypeRule" +typerule STRING_TO_CODE "SimpleTypeRule" +typerule STRING_FROM_CODE "SimpleTypeRule" typerule STRING_TOUPPER "SimpleTypeRule" typerule STRING_TOLOWER "SimpleTypeRule" typerule STRING_REV "SimpleTypeRule" diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 422c9e58b..2b903a8da 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -95,7 +95,7 @@ const context::CDList& SolverState::getDisequalityList() const void SolverState::eqNotifyNewClass(TNode t) { Kind k = t.getKind(); - if (k == STRING_LENGTH || k == STRING_CODE) + if (k == STRING_LENGTH || k == STRING_TO_CODE) { Node r = d_ee.getRepresentative(t[0]); EqcInfo* ei = getOrMakeEqcInfo(r); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index cd1d0cd67..2fbf16552 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -93,7 +93,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); - d_equalityEngine.addFunctionKind(kind::STRING_CODE); + d_equalityEngine.addFunctionKind(kind::STRING_TO_CODE); // extended functions d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); @@ -351,7 +351,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) if (eip && !eip->d_codeTerm.get().isNull()) { // its value must be equal to its code - Node ct = nm->mkNode(kind::STRING_CODE, eip->d_codeTerm.get()); + Node ct = nm->mkNode(kind::STRING_TO_CODE, eip->d_codeTerm.get()); Node ctv = d_valuation.getModelValue(ct); unsigned cvalue = ctv.getConst().getNumerator().toUnsignedInt(); @@ -600,6 +600,26 @@ void TheoryStrings::preRegisterTerm(TNode n) { Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl; + + if (node.getKind() == STRING_FROM_CODE) + { + // str.from_code(t) ---> + // choice k. ite(0 <= t < |A|, t = str.to_code(k), k = "") + NodeManager* nm = NodeManager::currentNM(); + Node t = node[0]; + Node card = nm->mkConst(Rational(utils::getAlphabetCardinality())); + Node cond = + nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card)); + Node k = nm->mkBoundVar(nm->stringType()); + Node bvl = nm->mkNode(BOUND_VAR_LIST, k); + node = nm->mkNode(CHOICE, + bvl, + nm->mkNode(ITE, + cond, + t.eqNode(nm->mkNode(STRING_TO_CODE, k)), + k.eqNode(d_emptyString))); + } + return node; } @@ -734,7 +754,7 @@ void TheoryStrings::conflict(TNode a, TNode b){ void TheoryStrings::eqNotifyNewClass(TNode t){ Kind k = t.getKind(); - if (k == STRING_LENGTH || k == STRING_CODE) + if (k == STRING_LENGTH || k == STRING_TO_CODE) { Trace("strings-debug") << "New length eqc : " << t << std::endl; //we care about the length of this string @@ -940,12 +960,12 @@ void TheoryStrings::checkCodes() Node c = nfe.d_nf[0]; Trace("strings-code-debug") << "Get proxy variable for " << c << std::endl; - Node cc = nm->mkNode(kind::STRING_CODE, c); + Node cc = nm->mkNode(kind::STRING_TO_CODE, c); cc = Rewriter::rewrite(cc); Assert(cc.isConst()); Node cp = d_im.getProxyVariableFor(c); AlwaysAssert(!cp.isNull()); - Node vc = nm->mkNode(STRING_CODE, cp); + Node vc = nm->mkNode(STRING_TO_CODE, cp); if (!d_state.areEqual(cc, vc)) { d_im.sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy"); @@ -957,7 +977,7 @@ void TheoryStrings::checkCodes() EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false); if (ei && !ei->d_codeTerm.get().isNull()) { - Node vc = nm->mkNode(kind::STRING_CODE, ei->d_codeTerm.get()); + Node vc = nm->mkNode(kind::STRING_TO_CODE, ei->d_codeTerm.get()); nconst_codes.push_back(vc); } } @@ -1027,7 +1047,7 @@ void TheoryStrings::registerTerm(Node n, int effort) // for concat/const/replace, introduce proxy var and state length relation d_im.registerLength(n); } - else if (n.getKind() == STRING_CODE) + else if (n.getKind() == STRING_TO_CODE) { d_has_str_code = true; // ite( str.len(s)==1, 0 <= str.code(s) < num_codes, str.code(s)=-1 ) diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 6272ad129..a4b0a6705 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -217,8 +217,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node sx = nm->mkNode(STRING_SUBSTR, itost, x, d_one); Node ux = nm->mkNode(APPLY_UF, u, x); Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne); - Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0"))); - Node c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, sx), c0); + Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); + Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0); Node ten = nm->mkConst(Rational(10)); Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux))); @@ -279,10 +279,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node k = nm->mkSkolem("k", nm->integerType()); Node kc1 = nm->mkNode(GEQ, k, d_zero); Node kc2 = nm->mkNode(LT, k, lens); - Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0"))); + Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); Node codeSk = nm->mkNode( MINUS, - nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, s, k, d_one)), + nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, d_one)), c0); Node ten = nm->mkConst(Rational(10)); Node kc3 = nm->mkNode( @@ -310,7 +310,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node sx = nm->mkNode(STRING_SUBSTR, s, x, d_one); Node ux = nm->mkNode(APPLY_UF, u, x); Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, d_one)); - Node c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, sx), c0); + Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0); Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux))); Node cb = @@ -495,8 +495,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node i = nm->mkBoundVar(nm->integerType()); Node bvi = nm->mkNode(BOUND_VAR_LIST, i); - Node ci = nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, x, i, d_one)); - Node ri = nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, r, i, d_one)); + Node ci = + nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, d_one)); + Node ri = + nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, d_one)); Node lb = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65)); Node ub = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90)); @@ -589,7 +591,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node tb = t[1 - r]; substr[r] = nm->mkNode(STRING_SUBSTR, ta, d_zero, k); code[r] = - nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, ta, k, d_one)); + nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, d_one)); conj.push_back(nm->mkNode(LEQ, k, nm->mkNode(STRING_LENGTH, ta))); } conj.push_back(substr[0].eqNode(substr[1])); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index d8bc7f34f..2c14d5343 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1478,10 +1478,11 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { else if (r.getKind() == REGEXP_RANGE) { // x in re.range( char_i, char_j ) ---> i <= str.code(x) <= j - Node xcode = nm->mkNode(STRING_CODE, x); - retNode = nm->mkNode(AND, - nm->mkNode(LEQ, nm->mkNode(STRING_CODE, r[0]), xcode), - nm->mkNode(LEQ, xcode, nm->mkNode(STRING_CODE, r[1]))); + Node xcode = nm->mkNode(STRING_TO_CODE, x); + retNode = + nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkNode(STRING_TO_CODE, r[0]), xcode), + nm->mkNode(LEQ, xcode, nm->mkNode(STRING_TO_CODE, r[1]))); } else if (r.getKind() == REGEXP_COMPLEMENT) { @@ -1667,7 +1668,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { else if (nk == STRING_IS_DIGIT) { // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57 - Node t = nm->mkNode(STRING_CODE, node[0]); + Node t = nm->mkNode(STRING_TO_CODE, node[0]); retNode = nm->mkNode(AND, nm->mkNode(LEQ, nm->mkConst(Rational(48)), t), nm->mkNode(LEQ, t, nm->mkConst(Rational(57)))); @@ -1709,9 +1710,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = rewriteMembership(node); } - else if (nk == STRING_CODE) + else if (nk == STRING_TO_CODE) { - retNode = rewriteStringCode(node); + retNode = rewriteStringToCode(node); } else if (nk == REGEXP_CONCAT) { @@ -3410,9 +3411,33 @@ Node TheoryStringsRewriter::rewritePrefixSuffix(Node n) return retNode; } -Node TheoryStringsRewriter::rewriteStringCode(Node n) +Node TheoryStringsRewriter::rewriteStringFromCode(Node n) +{ + Assert(n.getKind() == kind::STRING_FROM_CODE); + NodeManager* nm = NodeManager::currentNM(); + + if (n[0].isConst()) + { + Integer i = n[0].getConst().getNumerator(); + Node ret; + if (i >= 0 && i < strings::utils::getAlphabetCardinality()) + { + std::vector svec = {i.toUnsignedInt()}; + ret = nm->mkConst(String(svec)); + } + else + { + ret = nm->mkConst(String("")); + } + return returnRewrite(n, ret, "from-code-eval"); + } + + return n; +} + +Node TheoryStringsRewriter::rewriteStringToCode(Node n) { - Assert(n.getKind() == kind::STRING_CODE); + Assert(n.getKind() == kind::STRING_TO_CODE); if (n[0].isConst()) { CVC4::String s = n[0].getConst(); @@ -3428,7 +3453,7 @@ Node TheoryStringsRewriter::rewriteStringCode(Node n) { ret = NodeManager::currentNM()->mkConst(Rational(-1)); } - return returnRewrite(n, ret, "code-eval"); + return returnRewrite(n, ret, "to-code-eval"); } return n; diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index c9733433c..4accfca39 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -249,12 +249,20 @@ class TheoryStringsRewriter : public TheoryRewriter * Returns the rewritten form of node. */ static Node rewritePrefixSuffix(Node node); - /** rewrite str.code + + /** rewrite str.from_code + * This is the entry point for post-rewriting terms n of the form + * str.from_code( t ) + * Returns the rewritten form of node. + */ + static Node rewriteStringFromCode(Node node); + + /** rewrite str.to_code * This is the entry point for post-rewriting terms n of the form - * str.code( t ) + * str.to_code( t ) * Returns the rewritten form of node. */ - static Node rewriteStringCode(Node node); + static Node rewriteStringToCode(Node node); static Node splitConstant( Node a, Node b, int& index, bool isRev ); /** can constant contain list diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d273b768d..3cbc2953f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -902,6 +902,7 @@ set(regress_0_tests regress0/strings/complement-simple.smt2 regress0/strings/escchar.smt2 regress0/strings/escchar_25.smt2 + regress0/strings/from_code.smt2 regress0/strings/hconst-092618.smt2 regress0/strings/idof-rewrites.smt2 regress0/strings/idof-sem.smt2 diff --git a/test/regress/regress0/strings/from_code.smt2 b/test/regress/regress0/strings/from_code.smt2 new file mode 100644 index 000000000..ecde829ec --- /dev/null +++ b/test/regress/regress0/strings/from_code.smt2 @@ -0,0 +1,69 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +(set-option :incremental true) +(set-logic QF_SLIA) +(declare-const s String) +(declare-const t String) +(declare-const n Int) + +(push) +(assert (not (= (str.to_code (str.from_code (str.to_code s))) (str.to_code s)))) +(check-sat) +(pop) + +(push) +(assert (not (= (str.from_code (str.to_code s)) s))) +(assert (<= (str.len s) 1)) +(check-sat) +(pop) + +(push) +(assert (not (= (str.from_code (str.to_code s)) s))) +(check-sat) +(pop) + +(push) +(assert (not (= (str.from_code (str.to_code (str.from_code n))) (str.from_code n)))) +(check-sat) +(pop) + +(push) +(assert (not (= (str.to_code (str.from_code n)) n))) +(assert (>= n 0)) +(check-sat) +(pop) + +(push) +(assert (not (= (str.to_code (str.from_code n)) n))) +(assert (and (>= n 0) (< n 50))) +(check-sat) +(pop) + +(push) +(assert (not (= (str.to_code (str.from_code n)) n))) +(check-sat) +(pop) + +(push) +(assert (= (str.to_code s) (str.to_code t))) +(assert (= (str.len s) 1)) +(assert (= (str.len t) 1)) +(assert (not (= (str.from_code (str.to_code s)) (str.from_code (str.to_code t))))) +(check-sat) +(pop) + +(push) +(assert (or + (not (= (str.from_code (- 1)) "")) + (not (= (str.from_code 100000000000000000000000) "")) + (not (= (str.from_code 65) "A")))) +(check-sat) +(pop) diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h index cfdab7c9e..c02aaaed8 100644 --- a/test/unit/theory/evaluator_white.h +++ b/test/unit/theory/evaluator_white.h @@ -168,14 +168,14 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite // (str.code "A") ---> 65 { - Node n = d_nm->mkNode(kind::STRING_CODE, a); + Node n = d_nm->mkNode(kind::STRING_TO_CODE, a); Node r = eval.eval(n, args, vals); TS_ASSERT_EQUALS(r, d_nm->mkConst(Rational(65))); } // (str.code "") ---> -1 { - Node n = d_nm->mkNode(kind::STRING_CODE, empty); + Node n = d_nm->mkNode(kind::STRING_TO_CODE, empty); Node r = eval.eval(n, args, vals); TS_ASSERT_EQUALS(r, d_nm->mkConst(Rational(-1))); } -- 2.30.2