Remove stdPrintAscii option (#6280)

Fixes #4179.

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 75da2a35b07576c6ea2d5ac2d3e86d9e0ab49030..208b4483fe094cb73e8df1107ab885d1fcfa73c4 100644 (file)
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -10,15 +10,6 @@ header = "options/strings_options.h"
   default    = "false"
   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"

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 0892af4de920e8a983cea022fde7eb0753f6ae65..4baabec69aef1be936057c4bbbbad168c01d5cfe 100644 (file)
--- 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 510214e0f04b95ee288aed59331f60d0d5b88354..8a2f3fe629004bf0f3ac6281df36e1660446d5a6 100644 (file)
--- 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 552a0a7067e1da4ae75b8ccae067e5e30e88a685..3c9d2ac8f6b0de0b65991a9be5740158140054dc 100644 (file)
--- 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)