From: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri, 18 Nov 2016 23:01:59 +0000 (-0800)
Subject: Add support for set-logic ALL, fix compiler error in GCC 6.1
X-Git-Tag: cvc5-1.0.0~5974
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f98fc506f3cb09a59d8418fd0043e59e4aee57e;p=cvc5.git

Add support for set-logic ALL, fix compiler error in GCC 6.1
---

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index f9055f56c..64025fc04 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -254,7 +254,7 @@ void CommandExecutor::printStatsFilterZeros(std::ostream& out,
     std::getline(iss, statValue, '\n');
 
     double curFloat;
-    bool isFloat = (std::istringstream(statValue) >> curFloat);
+    bool isFloat = static_cast<bool>(std::istringstream(statValue) >> curFloat);
 
     if( (isFloat && curFloat == 0) ||
         statValue == " \"0\"" ||
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 50f62009a..015129f10 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -62,6 +62,8 @@ std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::ne
   logicMap["UFLRA"] = UFLRA;
   logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
   logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
+  logicMap["QF_ALL"] = QF_ALL_SUPPORTED;
+  logicMap["ALL"] = ALL_SUPPORTED;
   return logicMap;
 }
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 27c5a62bd..ff34fd9a3 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -272,7 +272,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd]
       }
       PARSER_STATE->setLogic(name);
       if( PARSER_STATE->sygus() ){
-        cmd->reset(new SetBenchmarkLogicCommand("ALL_SUPPORTED"));
+        cmd->reset(new SetBenchmarkLogicCommand("ALL"));
       }else{
         cmd->reset(new SetBenchmarkLogicCommand(name));
       }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8db344f92..2e2481a6e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -370,7 +370,7 @@ void Smt2::setLogic(std::string name) {
       name = "UFSLIA";
     } else if(name == "SAT") {
       name = "UF";
-    } else if(name == "ALL_SUPPORTED") {
+    } else if(name == "ALL" || name == "ALL_SUPPORTED") {
       //no change
     } else {
       std::stringstream ss;
@@ -456,14 +456,14 @@ void Smt2::checkThatLogicIsSet() {
         setLogic("LIA");
       } else {
         warning("No set-logic command was given before this point.");
-        warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
+        warning("CVC4 will make all theories available.");
         warning("Consider setting a stricter logic for (likely) better performance.");
-        warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
+        warning("To suppress this warning in the future use (set-logic ALL).");
 
-        setLogic("ALL_SUPPORTED");
+        setLogic("ALL");
       }
 
-      Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
+      Command* c = new SetBenchmarkLogicCommand("ALL");
       c->setMuted(true);
       preemptCommand(c);
     }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 38347508c..5fc96aa6e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1645,7 +1645,7 @@ void SmtEngine::setDefaults() {
   // Set decision mode based on logic (if not set by user)
   if(!options::decisionMode.wasSetByUser()) {
     decision::DecisionMode decMode =
-      // ALL_SUPPORTED
+      // ALL
       d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION :
       ( // QF_BV
         (not d_logic.isQuantified() &&
@@ -1676,7 +1676,7 @@ void SmtEngine::setDefaults() {
       );
 
     bool stoponly =
-      // ALL_SUPPORTED
+      // ALL
       d_logic.hasEverything() || d_logic.isTheoryEnabled(THEORY_STRINGS) ? false :
       ( // QF_AUFLIA
         (not d_logic.isQuantified() &&
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 6ac1c5e32..0e4ccf0f7 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -242,9 +242,9 @@ std::string LogicInfo::getLogicString() const {
     qf_all_supported.disableQuantifiers();
     qf_all_supported.lock();
     if(hasEverything()) {
-      d_logicString = "ALL_SUPPORTED";
+      d_logicString = "ALL";
     } else if(*this == qf_all_supported) {
-      d_logicString = "QF_ALL_SUPPORTED";
+      d_logicString = "QF_ALL";
     } else {
       size_t seen = 0; // make sure we support all the active theories
 
@@ -341,11 +341,21 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
     enableEverything();
     disableQuantifiers();
     p += 16;
+  } else if(!strcmp(p, "QF_ALL")) {
+    // the "all theories included" logic, no quantifiers
+    enableEverything();
+    disableQuantifiers();
+    p += 6;
   } else if(!strcmp(p, "ALL_SUPPORTED")) {
     // the "all theories included" logic, with quantifiers
     enableEverything();
     enableQuantifiers();
     p += 13;
+  } else if(!strcmp(p, "ALL")) {
+    // the "all theories included" logic, with quantifiers
+    enableEverything();
+    enableQuantifiers();
+    p += 3;
   } else {
     if(!strncmp(p, "QF_", 3)) {
       disableQuantifiers();
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 26e6908da..8b44b5cac 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -646,12 +646,6 @@ void TheoryStrings::check(Effort e) {
   bool polarity;
   TNode atom;
 
-  /*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;
-  }
-  }*/
-
   if( !done() && !hasTerm( d_emptyString ) ) {
     preRegisterTerm( d_emptyString );
   }