diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 14 | ||||
| -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 |
4 files changed, 15 insertions, 10 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4e0ea51a6..46843b21a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -950,20 +950,14 @@ void SmtEngine::setLogicInternal() throw() { d_logic.enableQuantifiers(); d_logic.lock(); Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; - //exception - //throw OptionException("The string-exp option requires quantifier option. One suggestion is UFSLIA."); } if(! options::finiteModelFind.wasSetByUser()) { - //exception - throw OptionException("The string-exp option requires finite-model-find option."); - //options::finiteModelFind.set( true ); - //Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl; + options::finiteModelFind.set( true ); + Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl; } if(! options::fmfBoundInt.wasSetByUser()) { - //exception - throw OptionException("The string-exp option requires fmf-bound-int option."); - //options::fmfBoundInt.set( true ); - //Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; + options::fmfBoundInt.set( true ); + Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } if(! options::stringFMF.wasSetByUser()) { options::stringFMF.set( true ); 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; } |