diff options
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 31 | ||||
| -rw-r--r-- | src/theory/logic_info.cpp | 4 | ||||
| -rw-r--r-- | test/regress/regress0/expect/scrub.09.p | 2 | ||||
| -rw-r--r-- | test/regress/regress0/nl/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/nl/all-logic.smt2 | 8 |
6 files changed, 30 insertions, 20 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)) { 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) |