Evaluator: add support for str.code (#2696)

2 files changed, 39 insertions, 0 deletions

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 25e20451a..0a0176f25 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -441,6 +441,21 @@ EvalResult Evaluator::evalInternal(TNode n,
           break;
         }
 
+        case kind::STRING_CODE:
+        {
+          const String& s = results[currNode[0]].d_str;
+          if (s.size() == 1)
+          {
+            results[currNode] = EvalResult(
+                Rational(String::convertUnsignedIntToCode(s.getVec()[0])));
+          }
+          else
+          {
+            results[currNode] = EvalResult(Rational(-1));
+          }
+          break;
+        }
+
         case kind::CONST_BITVECTOR:
           results[currNode] = EvalResult(currNodeVal.getConst<BitVector>());
           break;
diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
index 73556c388..9dc6f9520 100644
--- a/test/unit/theory/evaluator_white.h
+++ b/test/unit/theory/evaluator_white.h
@@ -156,4 +156,28 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
       TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
     }
   }
+
+  void testCode()
+  {
+    Node a = d_nm->mkConst(String("A"));
+    Node empty = d_nm->mkConst(String(""));
+
+    std::vector<Node> args;
+    std::vector<Node> vals;
+    Evaluator eval;
+
+    // (str.code "A") ---> 65
+    {
+      Node n = d_nm->mkNode(kind::STRING_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 r = eval.eval(n, args, vals);
+      TS_ASSERT_EQUALS(r, d_nm->mkConst(Rational(-1)));
+    }
+  }
 };