From 7b0efcd75f471b4252c65b8d18aa4c3266649626 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 7 Nov 2018 17:04:52 -0800
Subject: [PATCH] Evaluator: add support for str.code (#2696)

---
 src/theory/evaluator.cpp           | 15 +++++++++++++++
 test/unit/theory/evaluator_white.h | 24 ++++++++++++++++++++++++
 2 files changed, 39 insertions(+)

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)));
+    }
+  }
 };
-- 
2.30.2