Add support for str.from_code (#3829)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 29 Feb 2020 06:20:18 +0000 (22:20 -0800)
committerGitHub <noreply@github.com>
Sat, 29 Feb 2020 06:20:18 +0000 (22:20 -0800)
commit31efb570a9d5811fd88a34d4915d7d08c81d13fa
treeb3b553c8ce5075b40f0a8645aac28edb69b1c253
parentb0609b2d70220064a44bc99e396bf0d2d5ade531
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.
15 files changed:
src/api/cvc4cpp.cpp
src/api/cvc4cppkind.h
src/parser/smt2/smt2.cpp
src/printer/smt2/smt2_printer.cpp
src/theory/evaluator.cpp
src/theory/strings/extf_solver.cpp
src/theory/strings/kinds
src/theory/strings/solver_state.cpp
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings_preprocess.cpp
src/theory/strings/theory_strings_rewriter.cpp
src/theory/strings/theory_strings_rewriter.h
test/regress/CMakeLists.txt
test/regress/regress0/strings/from_code.smt2 [new file with mode: 0644]
test/unit/theory/evaluator_white.h