From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 6 Apr 2021 03:37:46 +0000 (-0500)
Subject: Remove stdPrintAscii option (#6280)
X-Git-Tag: cvc5-1.0.0~1964
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=44af184778fbc4bb31c13cb52c20942dc3ef0842;p=cvc5.git

Remove stdPrintAscii option (#6280)

Fixes #4179.
---

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
@@ -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 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)