diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-05 22:37:46 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-06 03:37:46 +0000 |
| commit | 44af184778fbc4bb31c13cb52c20942dc3ef0842 (patch) | |
| tree | 47f0d4fd6aaf0bd806289e141ba6f2e813b1d220 | |
| parent | d2e454e0dfc06e16fe0a4228168b21cf1311fc35 (diff) | |
Remove stdPrintAscii option (#6280)
Fixes #4179.
| -rw-r--r-- | src/options/strings_options.toml | 9 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 8 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_utils.cpp | 5 | ||||
| -rw-r--r-- | test/regress/regress1/strings/re-unsound-080718.smt2 | 2 |
4 files changed, 1 insertions, 23 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 75da2a35b..208b4483f 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -11,15 +11,6 @@ header = "options/strings_options.h" help = "experimental features in the theory of strings" [[option]] - name = "stdPrintASCII" - category = "regular" - long = "strings-print-ascii" - type = "bool" - default = "false" - read_only = true - help = "the alphabet contains only printable characters from the standard extended ASCII" - -[[option]] name = "stringFMF" category = "regular" long = "strings-fmf" diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 0892af4de..4baabec69 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -340,14 +340,6 @@ public: if(ch[0] > ch[1]) { throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range"); } - unsigned maxCh = options::stdPrintASCII() ? 127 : 255; - if (ch[1] > maxCh) - { - std::stringstream ss; - ss << "expecting characters whose code point is less than or equal to " - << maxCh; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } } return nodeManager->regExpType(); } diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 510214e0f..8a2f3fe62 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -33,11 +33,6 @@ namespace utils { uint32_t getAlphabetCardinality() { - if (options::stdPrintASCII()) - { - Assert(128 <= String::num_codes()); - return 128; - } // 3*16^4 = 196608 values in the SMT-LIB standard for Unicode strings Assert(196608 <= String::num_codes()); return 196608; diff --git a/test/regress/regress1/strings/re-unsound-080718.smt2 b/test/regress/regress1/strings/re-unsound-080718.smt2 index 552a0a706..3c9d2ac8f 100644 --- a/test/regress/regress1/strings/re-unsound-080718.smt2 +++ b/test/regress/regress1/strings/re-unsound-080718.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-print-ascii --strings-exp +; COMMAND-LINE: --strings-exp ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic ALL) |