diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-22 13:40:54 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-22 13:40:54 -0600 |
| commit | fffb74dbd0ee96b636fb494e843dd760b1a13149 (patch) | |
| tree | 693cfca9982ce0257fd132e956b32f7f681954db /src/theory/strings | |
| parent | 3da57075e8f810773ae95aadadc5408e0a537f02 (diff) | |
add warning for using strings in ALL_SUPPORTED
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 1 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 1 |
3 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index dbda080cc..77d4b80d7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -63,6 +63,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); + d_all_warning = true; d_regexp_incomplete = false; d_opt_regexp_gcd = true; } @@ -415,6 +416,14 @@ void TheoryStrings::check(Effort e) { bool polarity; TNode atom; + if(d_all_warning) { + if(getLogicInfo().hasEverything()) { + WarningOnce() << "WARNING: strings not supported in default configuration (ALL_SUPPORTED).\n" + << "To suppress this warning in the future use proper logic symbol, e.g. (set-logic QF_S)." << std::endl; + } + d_all_warning = false; + } + if( !done() && !hasTerm( d_emptyString ) ) { preRegisterTerm( d_emptyString ); } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 824dbcb37..20c5e90f7 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -115,6 +115,7 @@ private: Node d_false; Node d_zero; // Options + bool d_all_warning; bool d_opt_fmf; bool d_opt_regexp_gcd; // Helper functions diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 105f8dac3..757ec56a2 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -145,6 +145,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) ); lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem ); + new_nodes.push_back( lem ); d_cache[t] = t; retNode = t; } |