Non-linear supported in ALL logics. Minor fixes for set logic with sygus.

3 files changed, 19 insertions, 18 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e693f1d57..1b96d9bd3 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"));
+        cmd->reset(new SetBenchmarkLogicCommand(PARSER_STATE->getLogic().getLogicString()));
       }else{
         cmd->reset(new SetBenchmarkLogicCommand(name));
       }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index ebe730e29..1a7388473 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -354,22 +354,23 @@ void Smt2::resetAssertions() {
 
 void Smt2::setLogic(std::string name) {
   if(sygus()) {
+    // sygus by default requires UF, datatypes, and LIA
     if(name == "Arrays") {
-      name = "AUF";
+      name = "AUFDTLIA";
     } else if(name == "Reals") {
-      name = "UFLRA";
+      name = "UFDTLIRA";
     } else if(name == "LIA") {
-      name = "UFLIA";
+      name = "UFDTLIA";
     } else if(name == "LRA") {
-      name = "UFLRA";
+      name = "UFDTLIRA";
     } else if(name == "LIRA") {
-      name = "UFLIRA";
+      name = "UFDTLIRA";
     } else if(name == "BV") {
-      name = "UFBV";
+      name = "UFDTBVLIA";
     } else if(name == "SLIA") {
-      name = "UFSLIA";
+      name = "UFDTSLIA";
     } else if(name == "SAT") {
-      name = "UF";
+      name = "UFDTLIA";
     } else if(name == "ALL" || name == "ALL_SUPPORTED") {
       //no change
     } else {
@@ -452,16 +453,12 @@ void Smt2::checkThatLogicIsSet() {
     if(strictModeEnabled()) {
       parseError("set-logic must appear before this point.");
     } else {
-      if(sygus()) {
-        setLogic("LIA");
-      } else {
-        warning("No set-logic command was given before this point.");
-        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).");
+      warning("No set-logic command was given before this point.");
+      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).");
 
-        setLogic("ALL");
-      }
+      setLogic("ALL");
 
       Command* c = new SetBenchmarkLogicCommand("ALL");
       c->setMuted(true);
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 0e4ccf0f7..6f519c15f 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -340,21 +340,25 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
     // the "all theories included" logic, no quantifiers
     enableEverything();
     disableQuantifiers();
+    arithNonLinear();
     p += 16;
   } else if(!strcmp(p, "QF_ALL")) {
     // the "all theories included" logic, no quantifiers
     enableEverything();
     disableQuantifiers();
+    arithNonLinear();
     p += 6;
   } else if(!strcmp(p, "ALL_SUPPORTED")) {
     // the "all theories included" logic, with quantifiers
     enableEverything();
     enableQuantifiers();
+    arithNonLinear();
     p += 13;
   } else if(!strcmp(p, "ALL")) {
     // the "all theories included" logic, with quantifiers
     enableEverything();
     enableQuantifiers();
+    arithNonLinear();
     p += 3;
   } else {
     if(!strncmp(p, "QF_", 3)) {