From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 5 Jul 2017 20:01:23 +0000 (-0500)
Subject: Non-linear supported in ALL logics. Minor fixes for set logic with sygus.
X-Git-Tag: cvc5-1.0.0~5748
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b329aff2cdee935377cbe88c289d083fb10c2af8;p=cvc5.git

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 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)) {
diff --git a/test/regress/regress0/expect/scrub.09.p b/test/regress/regress0/expect/scrub.09.p
index ee765a91a..0297b1155 100644
--- 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 0da1816b0..53e04a1ef 100644
--- 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
index 000000000..700e5d919
--- /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)