From 7b9b6b9cfbe813812b0de7ba20f2c1d8cc060e63 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 16 Apr 2018 12:12:24 -0500 Subject: Make 256 the default cardinality for strings (#1783) --- src/theory/strings/regexp_operation.cpp | 7 ++++--- src/theory/strings/theory_strings.cpp | 10 +++++----- src/theory/strings/theory_strings_type_rules.h | 8 ++++++-- 3 files changed, 15 insertions(+), 10 deletions(-) (limited to 'src/theory') 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{})), - 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(); -- cgit v1.2.3