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.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 31453b618bfa86448b42a35759f2beee743cfc09..0d24139e814d0c3991475cfe31f801217881e6a0 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -258,7 +258,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> 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, Kind, CVC4::kind::KindHashFunction>
         {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 eb85759076fdddc0601a5dba1238fe0c3d40f60f..d399ad616f1aa132480b09d98546c46cf954709c 100644 (file)
--- 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 ef13d379e9ec80166f820b961fa93ea1b607ed1f..94a27319309c05d697a77ee9f0cd4ba43803adcb 100644 (file)
--- 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 13a64a2c378efe82feba98a9abfaf0c2219509f3..e3a65ca3f78c0e4736a661ef4cf00b11f921b6a4 100644 (file)
--- 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 a3ea768d415c0b078c5975de133f48b85593e10b..b827912d58a5d608edcd1a4eed3fab17b9d10176 100644 (file)
--- 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<unsigned> 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 6ab74cf9ad6dde4dc7921e37969fa9f42aaa8960..b04b88b31280f303865085badf5c2d4a900ded14 100644 (file)
--- 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 965c56ee40b003111254da8813617a660a733c65..9d12cd906e4f10cb936ded35de7b140aa60666fc 100644 (file)
--- 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<RBool, AString, AString>"
 typerule STRING_IS_DIGIT "SimpleTypeRule<RBool, AString>"
 typerule STRING_ITOS "SimpleTypeRule<RString, AInteger>"
 typerule STRING_STOI "SimpleTypeRule<RInteger, AString>"
-typerule STRING_CODE "SimpleTypeRule<RInteger, AString>"
+typerule STRING_TO_CODE "SimpleTypeRule<RInteger, AString>"
+typerule STRING_FROM_CODE "SimpleTypeRule<RString, AInteger>"
 typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
 typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
 typerule STRING_REV "SimpleTypeRule<RString, AString>"

diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 422c9e58bd51231c8c33fac499cc5dc0c79d19ba..2b903a8da33b47a799342696eba8bf8b01eeffcb 100644 (file)
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -95,7 +95,7 @@ const context::CDList<Node>& 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 cd1d0cd677f4f329c48f0245c38ad320cf01d409..2fbf1655253ca4d68d2c109a13ffb8c1ed0c57e7 100644 (file)
--- 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<Rational>().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 6272ad1291ddc6e89a1666160c2b8d95542578e4..a4b0a6705c3e9532048a53540b15777859b2f931 100644 (file)
--- 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 d8bc7f34f5548874f252daf9e45122852f73ac55..2c14d5343977a3c081ad0358729d21e710fb043f 100644 (file)
--- 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<Rational>().getNumerator();
+    Node ret;
+    if (i >= 0 && i < strings::utils::getAlphabetCardinality())
+    {
+      std::vector<unsigned> 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<String>();
@@ -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 c9733433c1bec8e9feaaff28fa9cfb4d58657077..4accfca3994239980c1aa1b95aa27025eb803ab3 100644 (file)
--- 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 d273b768d4bec75eae217089cf40c11cd7d3846f..3cbc2953f2d32e06bfa5b3dd6a076759f192c2c7 100644 (file)
--- 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 (file)
index 0000000..ecde829
--- /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 cfdab7c9eb127d81af008848259ef5ed16731785..c02aaaed8c74149faf73381d854f406d10772711 100644 (file)
--- 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)));
     }