Make 256 the default cardinality for strings (#1783)

4 files changed, 19 insertions, 15 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 06edb53ed..a6e7aa412 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -22,14 +22,13 @@ header = "options/strings_options.h"
   help       = "the strategy of LB rule application: 0-lazy, 1-eager, 2-no"
 
 [[option]]
-  name       = "stdASCII"
+  name       = "stdPrintASCII"
   category   = "regular"
-  long       = "strings-std-ascii"
+  long       = "strings-print-ascii"
   type       = "bool"
-  default    = "true"
-  predicates = ["unsignedLessEqual2"]
+  default    = "false"
   read_only  = true
-  help       = "the alphabet contains only characters from the standard ASCII or the extended one"
+  help       = "the alphabet contains only printable characters from the standard extended ASCII"
 
 [[option]]
   name       = "stringFMF"
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index a8fd08792..f9db44102 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -24,7 +24,7 @@ namespace theory {
 namespace strings {
 
 RegExpOpr::RegExpOpr()
-    : d_lastchar(options::stdASCII() ? '\x7f' : '\xff'),
+    : d_lastchar(options::stdPrintASCII() ? '\x7f' : '\xff'),
       d_emptyString(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
       d_true(NodeManager::currentNM()->mkConst(true)),
       d_false(NodeManager::currentNM()->mkConst(false)),
@@ -39,8 +39,9 @@ RegExpOpr::RegExpOpr()
       d_char_end(),
       d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA,
                                                std::vector<Node>{})),
-      d_sigma_star(
-          NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma)) {}
+      d_sigma_star(NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma))
+{
+}
 
 RegExpOpr::~RegExpOpr() {}
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index fe6f7ea77..c780caca2 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -143,7 +143,11 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 
-  d_card_size = 128;
+  d_card_size = 256;
+  if (options::stdPrintASCII())
+  {
+    d_card_size = 128;
+  }
 }
 
 TheoryStrings::~TheoryStrings() {
@@ -450,10 +454,6 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) {
 
 void TheoryStrings::presolve() {
   Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl;
-
-  if(!options::stdASCII()) {
-    d_card_size = 256;
-  }
 }
 
 
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index da1b71fff..03267abcd 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -361,8 +361,12 @@ public:
       if(ch[0] > ch[1]) {
         throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
       }
-      if(options::stdASCII() && ch[1] > '\x7f') {
-        throw TypeCheckingExceptionPrivate(n, "expecting standard ASCII characters in regexp range, or please set the option strings-std-ascii to be false");
+      if (options::stdPrintASCII() && ch[1] > '\x7f')
+      {
+        throw TypeCheckingExceptionPrivate(n,
+                                           "expecting standard ASCII "
+                                           "characters in regexp range when "
+                                           "strings-print-ascii is true");
       }
     }
     return nodeManager->regExpType();