diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-02-28 22:20:18 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-28 22:20:18 -0800 |
commit | 31efb570a9d5811fd88a34d4915d7d08c81d13fa (patch) | |
tree | b3b553c8ce5075b40f0a8645aac28edb69b1c253 /src/theory/evaluator.cpp | |
parent | b0609b2d70220064a44bc99e396bf0d2d5ade531 (diff) |
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.
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) |