diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-16 12:12:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-16 12:12:24 -0500 |
| commit | 7b9b6b9cfbe813812b0de7ba20f2c1d8cc060e63 (patch) | |
| tree | e7c93bcb8d0b04461f0ea42036d8d2f3f2912e5f /src/theory/strings/theory_strings.cpp | |
| parent | 353bccac179f9673583c3ce559c720751ae3fa96 (diff) | |
Make 256 the default cardinality for strings (#1783)
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
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; - } } |