diff options
Diffstat (limited to 'src/theory/evaluator.cpp')
-rw-r--r-- | src/theory/evaluator.cpp | 18 |
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) |