diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-27 09:01:38 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-27 09:01:38 -0500 |
| commit | 27ac2ce712b0bcfdef83e2d44dd210f667ab7959 (patch) | |
| tree | a64febad63c37b641eaaacf4ad79007888aa43f9 /test/regress/CMakeLists.txt | |
| parent | fa2ba76ef83497108942ebb91cdb07fdfeed505b (diff) | |
Support unicode internal representation and escape sequences (#3852)
Work towards support for the strings standard.
This updates the string solver and parser such that:
The internal representation of strings is vectors of code points,
Generation of the previous internal representation of strings has been relegated to the type enumerator. This is the code that ensures that "A" is the first character chosen for values of strings in models,
The previous ad-hoc escape sequence handling is moved from the String class to the parser. It will live there for at least one version of CVC4, until we no longer support non-smt-lib complaint escape sequences or non-printable characters in strings,
Handle unicode escape sequences according to the SMT-LIB standard in String,
Simplify a number of calls to String utility functions, since the conversion between the previous internal format and code points is now unnecessary,
Fixed a bug in the handling of TO_CODE: it should be based on the alphabet cardinality, not the number of internal code points.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8fab16b44..8382e40fc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -922,6 +922,7 @@ set(regress_0_tests regress0/strings/escchar.smt2 regress0/strings/escchar_25.smt2 regress0/strings/from_code.smt2 + regress0/strings/gen-esc-seq.smt2 regress0/strings/hconst-092618.smt2 regress0/strings/idof-rewrites.smt2 regress0/strings/idof-sem.smt2 @@ -939,6 +940,8 @@ set(regress_0_tests regress0/strings/leadingzero001.smt2 regress0/strings/loop001.smt2 regress0/strings/model001.smt2 + regress0/strings/model-code-point.smt2 + regress0/strings/model-friendly.smt2 regress0/strings/ncontrib-rewrites.smt2 regress0/strings/norn-31.smt2 regress0/strings/norn-simp-rew.smt2 @@ -967,6 +970,7 @@ set(regress_0_tests regress0/strings/tolower-rrs.smt2 regress0/strings/tolower-simple.smt2 regress0/strings/type001.smt2 + regress0/strings/unicode-esc.smt2 regress0/strings/unsound-0908.smt2 regress0/strings/unsound-repl-rewrite.smt2 regress0/sygus/General_plus10.sy |