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.

1 files changed, 17 insertions, 1 deletions

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<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)