add warning for using strings in ALL_SUPPORTED

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4e0ea51a612b8aa0ca569f560e1cbd236246171b..46843b21a26be561aa69d14ef2df61055ba03cff 100644 (file)
--- 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 dbda080cca31a1278541a969545a0a8e65730449..77d4b80d75609a6129e2bda04629812abba7a025 100644 (file)
--- 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 824dbcb37bdbbce63d7d5cd968c5d9456e4ad02c..20c5e90f73dc6ac0e63411f9f0e09ded31708e91 100644 (file)
--- 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 105f8dac3e7d5762d069fcee8e0d97c9d2cc8079..757ec56a26804e4ff38c3b096a4e8c811ad2060a 100644 (file)
--- 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;
                }