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 f9055f56cd131733578be1aa86620568ae656089..64025fc0468c4f115d4c47163cf0f1e997e6c71b 100644 (file)
--- 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 50f62009acfc4c36c1a22d172943a0dc078b27be..015129f100bfe8f478f381c2c886c8b0c11c468f 100644 (file)
--- 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 27c5a62bd22f2bfc93eec43b517574d7427c743d..ff34fd9a3ed2888685bb6372aba69b236b91ca53 100644 (file)
--- 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 8db344f929b7bcccbe32dbc6deca535204d2b240..2e2481a6e0af3b2591015926a0d5ca63039eb641 100644 (file)
--- 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 38347508cabc7860e9eda2b6bfbec6bbda39dba6..5fc96aa6ea50e199bf4e226087c32706b3f97989 100644 (file)
--- 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 6ac1c5e32ec7fb3d42c4daa6e2fdbcf1568f958e..0e4ccf0f73ce67722349395ee48f99b7b6ef6638 100644 (file)
--- 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 26e6908daf7b9efdbb8ba2ecf7039ede4c7cd9b1..8b44b5cac9b224e82afbe8041e642d5b7c57adef 100644 (file)
--- 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 );
   }