support for code.strcodeString

5 files changed, 71 insertions, 24 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 4e90d1583..98db9b6b6 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -28,6 +28,7 @@ operator STRING_SUFFIX 2 "string suffixof"
 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 CODE_STRING 1 "code to string"
 operator STRING_TOLOWER 1 "string to lowercase conversion"
 operator STRING_TOUPPER 1 "string to uppercase conversion"
 
@@ -102,6 +103,7 @@ typerule STRING_SUFFIX "SimpleTypeRule<RBool, AString, AString>"
 typerule STRING_ITOS "SimpleTypeRule<RString, AInteger>"
 typerule STRING_STOI "SimpleTypeRule<RInteger, AString>"
 typerule STRING_CODE "SimpleTypeRule<RInteger, AString>"
+typerule CODE_STRING "SimpleTypeRule<RString, AInteger>"
 typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
 typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9fad39b6b..232f24e0c 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -126,6 +126,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
   getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP);
   getExtTheory()->addFunctionKind(kind::STRING_LEQ);
   getExtTheory()->addFunctionKind(kind::STRING_CODE);
+  getExtTheory()->addFunctionKind(kind::CODE_STRING);
   getExtTheory()->addFunctionKind(kind::STRING_TOLOWER);
   getExtTheory()->addFunctionKind(kind::STRING_TOUPPER);
 
@@ -134,6 +135,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
   d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
   d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
   d_equalityEngine.addFunctionKind(kind::STRING_CODE);
+  d_equalityEngine.addFunctionKind(kind::CODE_STRING);
 
   // extended functions
   d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
@@ -436,7 +438,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
     Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF
            || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL
            || k == STRING_STRREPLALL || k == STRING_LEQ || k == STRING_TOLOWER
-           || k == STRING_TOUPPER);
+           || k == STRING_TOUPPER || k == CODE_STRING);
     std::vector<Node> new_nodes;
     Node res = d_preproc.simplify(n, new_nodes);
     Assert(res != n);
@@ -2579,7 +2581,18 @@ void TheoryStrings::checkCodes()
         Node vc = nm->mkNode(STRING_CODE, cp);
         if (!d_state.areEqual(cc, vc))
         {
-          d_im.sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy");
+          Node rcs = Rewriter::rewrite(nm->mkNode(CODE_STRING, cc));
+          Node inf = cc.eqNode(vc);
+
+          if (c.getConst<String>().size() == 1)
+          {
+            inf = nm->mkNode(
+                AND,
+                inf,
+                nm->mkNode(CODE_STRING, vc).eqNode(getProxyVariableFor(rcs)));
+          }
+
+          d_im.sendInference(d_empty_vec, inf, "Code_Proxy");
         }
         const_codes.push_back(vc);
       }
@@ -2598,27 +2611,16 @@ void TheoryStrings::checkCodes()
       return;
     }
     // now, ensure that str.code is injective
-    std::vector<Node> cmps;
-    cmps.insert(cmps.end(), const_codes.rbegin(), const_codes.rend());
-    cmps.insert(cmps.end(), nconst_codes.rbegin(), nconst_codes.rend());
-    for (unsigned i = 0, num_ncc = nconst_codes.size(); i < num_ncc; i++)
+    for (const Node& c : nconst_codes)
     {
-      Node c1 = nconst_codes[i];
-      cmps.pop_back();
-      for (const Node& c2 : cmps)
+      Node codeStr = nm->mkNode(CODE_STRING, c);
+      if (!d_state.areEqual(codeStr, c[0]) && !d_state.areEqual(c, d_neg_one))
       {
-        Trace("strings-code-debug")
-            << "Compare codes : " << c1 << " " << c2 << std::endl;
-        if (!d_state.areDisequal(c1, c2) && !d_state.areEqual(c1, d_neg_one))
-        {
-          Node eq_no = c1.eqNode(d_neg_one);
-          Node deq = c1.eqNode(c2).negate();
-          Node eqn = c1[0].eqNode(c2[0]);
-          // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
-          Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn);
-          d_im.sendPhaseRequirement(deq, false);
-          d_im.sendInference(d_empty_vec, inj_lem, "Code_Inj");
-        }
+        Node eq_no = c.eqNode(d_neg_one);
+        Node inv = nm->mkNode(EQUAL, codeStr, c[0]);
+        // str.code(x) == -1 V code.str(str.code(x)) == x
+        Node inj_lem = nm->mkNode(kind::OR, eq_no, inv);
+        d_im.sendInference(d_empty_vec, inj_lem, "Code_Inj");
       }
     }
   }
@@ -4107,6 +4109,21 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
     Trace("strings-assert") << "(assert " << lem << ")" << std::endl;
     d_out->lemma(lem);
   }
+  else if (n.getKind() == CODE_STRING)
+  {
+    d_has_str_code = true;
+    // ite( str.len(s)==1, 0 <= str.code(s) < num_codes, str.code(s)=-1 )
+    Node code_len = utils::mkNLength(n).eqNode(d_one);
+    Node code_range = nm->mkNode(
+        AND,
+        nm->mkNode(GEQ, n[0], d_zero),
+        nm->mkNode(LT, n[0], nm->mkConst(Rational(CVC4::String::num_codes()))));
+    Node lem = nm->mkNode(
+        ITE, code_range, code_len, n.eqNode(nm->mkConst(String(""))));
+    Trace("strings-lemma") << "Strings::Lemma CODE : " << lem << std::endl;
+    Trace("strings-assert") << "(assert " << lem << ")" << std::endl;
+    d_out->lemma(lem);
+  }
   else if (n.getKind() == STRING_STRIDOF)
   {
     Node len = utils::mkNLength(n[0]);
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 1e5b2a65a..aeff40ccd 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1686,6 +1686,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
   {
     retNode = rewriteStringCode(node);
   }
+  else if (nk == CODE_STRING)
+  {
+    retNode = rewriteCodeString(node);
+  }
   else if (nk == REGEXP_CONCAT)
   {
     retNode = rewriteConcatRegExp(node);
@@ -3353,6 +3357,32 @@ Node TheoryStringsRewriter::rewriteStringCode(Node n)
   return n;
 }
 
+Node TheoryStringsRewriter::rewriteCodeString(Node n)
+{
+  Assert(n.getKind() == kind::CODE_STRING);
+  if (n[0].isConst())
+  {
+    Rational r = n[0].getConst<Rational>();
+    Node ret;
+    if (r.sgn() >= 0 && r < Rational(CVC4::String::num_codes()))
+    {
+      Assert(r.getDenominator() == 1);
+      Integer i = r.getNumerator();
+      std::vector<unsigned> vec;
+      vec.push_back(CVC4::String::convertCodeToUnsignedInt(i.toUnsignedInt()));
+      Assert(vec.size() == 1);
+      ret = NodeManager::currentNM()->mkConst(String(vec));
+    }
+    else
+    {
+      ret = NodeManager::currentNM()->mkConst(String(""));
+    }
+    return returnRewrite(n, ret, "code-eval");
+  }
+
+  return n;
+}
+
 Node TheoryStringsRewriter::splitConstant( Node a, Node b, int& index, bool isRev ) {
   Assert(a.isConst() && b.isConst());
   index = a.getConst<String>().size() <= b.getConst<String>().size() ? 1 : 0;
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index b19d49e67..8edbedf8e 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -251,6 +251,7 @@ class TheoryStringsRewriter {
    * Returns the rewritten form of node.
    */
   static Node rewriteStringCode(Node node);
+  static Node rewriteCodeString(Node node);
 
   static Node splitConstant( Node a, Node b, int& index, bool isRev );
   /** can constant contain list
diff --git a/test/regress/regress1/strings/issue2981.smt2 b/test/regress/regress1/strings/issue2981.smt2
index 78cdb2a8c..425060936 100644
--- a/test/regress/regress1/strings/issue2981.smt2
+++ b/test/regress/regress1/strings/issue2981.smt2
@@ -3,9 +3,6 @@
 (set-option :strings-exp true)
 (set-info :status sat)
 (declare-const x String)
-(declare-const y String)
-(declare-const m String)
-(declare-const n String)
 (assert (str.in.re x (re.+ (re.range "0" "9"))))
 (assert (= 0 (str.to.int x)))                   
 (assert (not (= x "")))