Use STRING_NTH in strings reductions and eliminate STRING_TO_CODE (#8851)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 7 Jun 2022 00:49:15 +0000 (19:49 -0500)
committerGitHub <noreply@github.com>
Tue, 7 Jun 2022 00:49:15 +0000 (00:49 +0000)
commite8c3db9e0e904beaacfbe3328bc9625b09952bdf
tree4ff8386a1e7e1f1b20531d7af5738e706a9f7e6f
parent2c03f4bc6910c6f95a42902c2f489c96f502f9e1
Use STRING_NTH in strings reductions and eliminate STRING_TO_CODE (#8851)

This updates our string reductions for `to_lower`, `to_upper`, `from_int`, `to_int` to use STRING_NTH instead of STRING_TO_CODE applied to STRING_SUBSTR.

It optionally replaces STRING_TO_CODE with STRING_NTH during preprocessing (true by default).

This is work towards efficient support for `to_lower`/`to_upper`.
20 files changed:
src/options/strings_options.toml
src/theory/strings/arith_entail.cpp
src/theory/strings/core_solver.cpp
src/theory/strings/term_registry.cpp
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/strings/theory_strings_preprocess.cpp
src/theory/strings/theory_strings_preprocess.h
test/api/cpp/proj-issue334.cpp
test/regress/cli/CMakeLists.txt
test/regress/cli/regress0/arith/projissue469-int-equality.smt2
test/regress/cli/regress0/strings/issue5771-eager-pp.smt2
test/regress/cli/regress0/strings/issue5816-re-kind.smt2
test/regress/cli/regress0/strings/issue8722-learned-rew.smt2
test/regress/cli/regress0/strings/model-code-point.smt2
test/regress/cli/regress1/decision/jh-test1.smt2
test/regress/cli/regress1/strings/cee-norn-aes-trivially.smt2
test/regress/cli/regress1/strings/str-code-sat.smt2
test/regress/cli/regress1/strings/to_upper_12.smt2 [new file with mode: 0644]
test/regress/cli/regress1/strings/to_upper_over_concat.smt2 [new file with mode: 0644]