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

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e693f1d57c16437f8a94d9357f247a647e1139ee..1b96d9bd387b121b79e293cdda9f78f9c4405419 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"));
+        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 ebe730e299980c8ee2fc10d52aa831fc5d1c9da1..1a73884734d1a6556b9c519caf7de83188d8c0ee 100644 (file)
--- 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 0e4ccf0f73ce67722349395ee48f99b7b6ef6638..6f519c15fe5772e006e3659ef787ab98417ff524 100644 (file)
--- 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)) {

diff --git a/test/regress/regress0/expect/scrub.09.p b/test/regress/regress0/expect/scrub.09.p
index ee765a91a643c569fb66ce77c8c91be4a07af702..0297b115561314d24546210a70a6544d52510cd4 100644 (file)
--- a/test/regress/regress0/expect/scrub.09.p
+++ b/test/regress/regress0/expect/scrub.09.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --cegqi-si=all --no-dump-synth
+% COMMAND-LINE: 
 % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
 % EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 % EXPECT: The fact in question: TERM

diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am
index 0da1816b0ccf5662748e3bb1e630c9392c6c2d10..53e04a1ef07ca1ac7cc797d031fe261f2ca8d9c5 100644 (file)
--- a/test/regress/regress0/nl/Makefile.am
+++ b/test/regress/regress0/nl/Makefile.am
@@ -48,7 +48,8 @@ TESTS =       \
   disj-eval.smt2 \
   bug698.smt2  \
   real-div-ufnra.smt2 \
-  div-mod-partial.smt2
+  div-mod-partial.smt2 \
+  all-logic.smt2
 
 # unsolved : garbage_collect.cvc
 

diff --git a/test/regress/regress0/nl/all-logic.smt2 b/test/regress/regress0/nl/all-logic.smt2
new file mode 100644 (file)
index 0000000..700e5d9
--- /dev/null
+++ b/test/regress/regress0/nl/all-logic.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-fun x () Real)
+
+(assert (< (* x x) 0.0))
+
+(check-sat)