From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 22 Jan 2014 19:40:54 +0000 (-0600)
Subject: add warning for using strings in ALL_SUPPORTED
X-Git-Tag: cvc5-1.0.0~7136
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fffb74dbd0ee96b636fb494e843dd760b1a13149;p=cvc5.git

add warning for using strings in ALL_SUPPORTED
---

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;
 		}