From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Mon, 24 Jan 2022 18:34:14 +0000 (-0600) Subject: Enable dump tester. (#7884) X-Git-Tag: cvc5-1.0.0~516 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0bab2e969c3557596516f3460eede4f28e468a1;p=cvc5.git Enable dump tester. (#7884) This PR enables the dump tester, a parse-print-parse test for cvc5, on CI. It also includes some changes that reduce the number of regressions that fail with this tester. --- diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 59a26838e..f79085f82 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -15,7 +15,7 @@ jobs: check-examples: true store-to-release: true exclude_regress: 3-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct + run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump - name: macos:production os: macos-11 @@ -25,7 +25,7 @@ jobs: check-examples: true store-to-release: true exclude_regress: 3-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct + run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump - name: ubuntu:production-clang os: ubuntu-18.04 @@ -34,14 +34,14 @@ jobs: cache-key: productionclang check-examples: true exclude_regress: 3-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct + run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump - name: ubuntu:production-dbg os: ubuntu-18.04 config: production --auto-download --assertions --tracing --unit-testing --java-bindings --editline cache-key: dbg exclude_regress: 3-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct --tester proof + run_regression_args: --tester base --tester model --tester synth --tester abduct --tester proof --tester dump - name: ubuntu:production-dbg-clang os: ubuntu-latest @@ -49,7 +49,7 @@ jobs: config: production --auto-download --assertions --tracing --cln --gpl cache-key: dbgclang exclude_regress: 3-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct --tester unsat-core + run_regression_args: --tester base --tester model --tester synth --tester abduct --tester unsat-core --tester dump name: ${{ matrix.name }} runs-on: ${{ matrix.os }} diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 218ab554d..44629652d 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -207,6 +207,7 @@ bool solverInvoke(api::Solver* solver, // commands. We invoke define-fun commands because they add function names // to the symbol table. if (solver->getOptionInfo("parse-only").boolValue() + && dynamic_cast(cmd) == nullptr && dynamic_cast(cmd) == nullptr && dynamic_cast(cmd) == nullptr) { diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index e576f2e71..418828382 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -162,9 +162,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) { if (!solver->getOptionInfo("incremental").setByUser) { - cmd.reset(new SetOptionCommand("incremental", "true")); - cmd->setMuted(true); - pExecutor->doCommand(cmd); + solver->setOption("incremental", "true"); } InteractiveShell shell(pExecutor->getSolver(), pExecutor->getSymbolManager(), @@ -202,9 +200,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) { if (!solver->getOptionInfo("incremental").setByUser) { - cmd.reset(new SetOptionCommand("incremental", "false")); - cmd->setMuted(true); - pExecutor->doCommand(cmd); + solver->setOption("incremental", "false"); } ParserBuilder parserBuilder( diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 634eb3655..8eed51baa 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -504,6 +504,11 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) Parser::addOperator(api::APPLY_UF); } + if (d_logic.isHigherOrder()) + { + addOperator(api::HO_APPLY, "@"); + } + if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) { if(d_logic.areIntegersUsed()) { defineType("Int", d_solver->getIntegerSort(), true, true); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index fd7825ac1..067cf27fe 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -292,7 +292,12 @@ void Smt2Printer::toStream(std::ostream& out, ArrayStoreAll asa = n.getConst(); out << "((as const "; toStreamType(out, asa.getType()); - out << ") " << asa.getValue() << ")"; + out << ") "; + toStreamCastToType(out, + asa.getValue(), + toDepth < 0 ? toDepth : toDepth - 1, + asa.getType().getArrayConstituentType()); + out << ")"; break; } @@ -592,6 +597,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::HO_APPLY: if (!options::flattenHOChains()) { + out << smtKindString(k, d_variant) << ' '; break; } // collapse "@" chains, i.e. @@ -759,7 +765,7 @@ void Smt2Printer::toStream(std::ostream& out, if (op.getIndices().empty()) { // e.g. (tuple_project tuple) - out << "project " << n[0] << ")"; + out << "tuple_project " << n[0] << ")"; } else { @@ -863,7 +869,7 @@ void Smt2Printer::toStream(std::ostream& out, { out << "(! "; annot << ":no-pattern "; - toStream(annot, nc, toDepth, nullptr); + toStream(annot, nc[0], toDepth, nullptr); annot << ") "; } } @@ -1226,6 +1232,9 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::FORALL: return "forall"; case kind::EXISTS: return "exists"; + // HO + case kind::HO_APPLY: return "@"; + default: ; /* fall through */ } @@ -1481,7 +1490,7 @@ void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out, TypeNode range, Node formula) const { - out << "(define-fun " << id << " ("; + out << "(define-fun " << cvc5::quoteSymbol(id) << " ("; if (!formals.empty()) { vector::const_iterator i = formals.cbegin(); diff --git a/test/regress/regress0/bv/issue-4075.smt2 b/test/regress/regress0/bv/issue-4075.smt2 index 083fbf897..31066e3f8 100644 --- a/test/regress/regress0/bv/issue-4075.smt2 +++ b/test/regress/regress0/bv/issue-4075.smt2 @@ -1,5 +1,6 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition -; EXPECT: (error "Parse Error: issue-4075.smt2:11.26: expecting number of repeats > 0 +; EXPECT: (error "Parse Error: issue-4075.smt2:12.26: expecting number of repeats > 0 ; EXPECT: ; EXPECT: (simplify ((_ repeat 0) b)) ; EXPECT: ^ diff --git a/test/regress/regress0/bv/issue-4130.smt2 b/test/regress/regress0/bv/issue-4130.smt2 index 4c7daab57..0f0894596 100644 --- a/test/regress/regress0/bv/issue-4130.smt2 +++ b/test/regress/regress0/bv/issue-4130.smt2 @@ -1,5 +1,6 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition -; EXPECT: (error "Parse Error: issue-4130.smt2:10.39: expecting bit-width > 0 +; EXPECT: (error "Parse Error: issue-4130.smt2:11.39: expecting bit-width > 0 ; EXPECT: ; EXPECT: (assert (and (= a (bv2nat ((_ int2bv 0) a))))) ; EXPECT: ^ diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 b/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 index 7d5495fcc..6a20d7607 100644 --- a/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 +++ b/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 @@ -1,5 +1,4 @@ ; COMMAND-LINE: -o raw-benchmark -; EXPECT: (set-option :incremental false) ; EXPECT: (set-logic ALL) ; EXPECT: (declare-datatypes ((nat 0)) (((succ (pred nat)) (zero)))) ; EXPECT: (declare-fun x () nat) diff --git a/test/regress/regress0/fp/issue-5524.smt2 b/test/regress/regress0/fp/issue-5524.smt2 index 3902f9c37..3e9696871 100644 --- a/test/regress/regress0/fp/issue-5524.smt2 +++ b/test/regress/regress0/fp/issue-5524.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --bv-solver=bitblast ; EXPECT: unsat -(set-logic QF_FP) +(set-logic QF_FPLRA) (declare-fun fpv5 () Float32) (assert (fp.eq (fp.mul RTP fpv5 fpv5) ((_ to_fp 8 24) RTN 0.04))) (check-sat) diff --git a/test/regress/regress0/ho/issue4477.smt2 b/test/regress/regress0/ho/issue4477.smt2 index 7162d260c..2b0ff115e 100644 --- a/test/regress/regress0/ho/issue4477.smt2 +++ b/test/regress/regress0/ho/issue4477.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition ; SCRUBBER: grep -o "Symbol '->' not declared" ; EXPECT: Symbol '->' not declared diff --git a/test/regress/regress0/issue1063-overloading-dt-cons.smt2 b/test/regress/regress0/issue1063-overloading-dt-cons.smt2 index a77fcdd22..82afaa3be 100644 --- a/test/regress/regress0/issue1063-overloading-dt-cons.smt2 +++ b/test/regress/regress0/issue1063-overloading-dt-cons.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/regress0/options/didyoumean.smt2 b/test/regress/regress0/options/didyoumean.smt2 index 100e1e6fb..43c4d5903 100644 --- a/test/regress/regress0/options/didyoumean.smt2 +++ b/test/regress/regress0/options/didyoumean.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition ; COMMAND-LINE: --input-agnuage ; ERROR-SCRUBBER: grep -o "--[a-zA-Z-]+" diff --git a/test/regress/regress0/options/help.smt2 b/test/regress/regress0/options/help.smt2 index 038619c5e..3f0cd4a14 100644 --- a/test/regress/regress0/options/help.smt2 +++ b/test/regress/regress0/options/help.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; COMMAND-LINE: --help ; SCRUBBER: grep -o "usage: cvc5" ; EXPECT: usage: cvc5 diff --git a/test/regress/regress0/options/named_muted.smt2 b/test/regress/regress0/options/named_muted.smt2 index 7026298c6..9105f79a1 100644 --- a/test/regress/regress0/options/named_muted.smt2 +++ b/test/regress/regress0/options/named_muted.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; COMMAND-LINE: --print-success ; EXPECT: success ; EXPECT: success diff --git a/test/regress/regress0/parser/bv_nat.smt2 b/test/regress/regress0/parser/bv_nat.smt2 index 14a150b4f..c2954dfad 100644 --- a/test/regress/regress0/parser/bv_nat.smt2 +++ b/test/regress/regress0/parser/bv_nat.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition ; EXPECT: sat ; EXPECT: not declared diff --git a/test/regress/regress0/parser/force_logic_set_logic.smt2 b/test/regress/regress0/parser/force_logic_set_logic.smt2 index 1bab02ef9..9c931f560 100644 --- a/test/regress/regress0/parser/force_logic_set_logic.smt2 +++ b/test/regress/regress0/parser/force_logic_set_logic.smt2 @@ -1,6 +1,7 @@ ; This regression ensures that we detect repeated set-logic commands even when ; --force-logic is used. +; DISABLE-TESTER: dump ; COMMAND-LINE: --force-logic="QF_BV" ; SCRUBBER: grep -o "Only one set-logic is allowed." ; EXPECT: Only one set-logic is allowed. diff --git a/test/regress/regress0/parser/issue6908-get-value-uc.smt2 b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 index ab7615809..722d4308e 100644 --- a/test/regress/regress0/parser/issue6908-get-value-uc.smt2 +++ b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; COMMAND-LINE: --produce-models ; EXPECT: sat ; EXPECT: (((f (as @a0 Foo)) 3)) diff --git a/test/regress/regress0/parser/linear_arithmetic_err1.smt2 b/test/regress/regress0/parser/linear_arithmetic_err1.smt2 index f031cded8..89e4f98f9 100644 --- a/test/regress/regress0/parser/linear_arithmetic_err1.smt2 +++ b/test/regress/regress0/parser/linear_arithmetic_err1.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition ; COMMAND-LINE: --strict-parsing ; SCRUBBER: grep -o "Symbol 'div' not declared as a variable" diff --git a/test/regress/regress0/parser/linear_arithmetic_err2.smt2 b/test/regress/regress0/parser/linear_arithmetic_err2.smt2 index adaa0aff4..17926f0c6 100644 --- a/test/regress/regress0/parser/linear_arithmetic_err2.smt2 +++ b/test/regress/regress0/parser/linear_arithmetic_err2.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition ; COMMAND-LINE: --strict-parsing ; SCRUBBER: grep -o "Symbol 'mod' not declared as a variable" diff --git a/test/regress/regress0/parser/linear_arithmetic_err3.smt2 b/test/regress/regress0/parser/linear_arithmetic_err3.smt2 index d875e4cbe..811a162b5 100644 --- a/test/regress/regress0/parser/linear_arithmetic_err3.smt2 +++ b/test/regress/regress0/parser/linear_arithmetic_err3.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition ; COMMAND-LINE: --strict-parsing ; SCRUBBER: grep -o "Symbol 'abs' not declared as a variable" diff --git a/test/regress/regress0/parser/named-attr-error.smt2 b/test/regress/regress0/parser/named-attr-error.smt2 index 2b925b8ce..86ba69638 100644 --- a/test/regress/regress0/parser/named-attr-error.smt2 +++ b/test/regress/regress0/parser/named-attr-error.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition ; SCRUBBER: grep -o "Cannot name a term in a binder" ; EXPECT: Cannot name a term in a binder diff --git a/test/regress/regress0/parser/shadow_fun_symbol_all.smt2 b/test/regress/regress0/parser/shadow_fun_symbol_all.smt2 index 7df6f5f12..19aa2eb23 100644 --- a/test/regress/regress0/parser/shadow_fun_symbol_all.smt2 +++ b/test/regress/regress0/parser/shadow_fun_symbol_all.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; EXPECT: Symbol `sin' is shadowing a theory function symbol ; SCRUBBER: grep -o "Symbol \`sin' is shadowing a theory function symbol" ; EXIT: 1 diff --git a/test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2 b/test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2 index 1c83f3c54..1f168053b 100644 --- a/test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2 +++ b/test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; EXPECT: Symbol `exp' is shadowing a theory function symbol ; SCRUBBER: grep -o "Symbol \`exp' is shadowing a theory function symbol" ; EXIT: 1 diff --git a/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 b/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 index 5dd51dc0c..5852266c2 100644 --- a/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 +++ b/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition ; EXPECT: Quantifier used in non-quantified logic ; SCRUBBER: grep -o "Quantifier used in non-quantified logic" diff --git a/test/regress/regress0/sygus/issue5512-vvv.sy b/test/regress/regress0/sygus/issue5512-vvv.sy index 333c0dd5a..0fbcc6d03 100644 --- a/test/regress/regress0/sygus/issue5512-vvv.sy +++ b/test/regress/regress0/sygus/issue5512-vvv.sy @@ -1,3 +1,4 @@ +; DISABLE-TESTER: dump ; COMMAND-LINE: -vvv --sygus-out=status --check-synth-sol --check-abducts ; ERROR-SCRUBBER: sed -e 's/.*//g' ; SCRUBBER: sed -e 's/.*//g' diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy index cf8e4da31..90eeb3e74 100644 --- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy +++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy @@ -1,6 +1,7 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 -; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:78.19: number of arguments does not match the constructor type +; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:79.19: number of arguments does not match the constructor type ; EXPECT-ERROR: ; EXPECT-ERROR: (Op2 ) ; EXPECT-ERROR: ^ diff --git a/test/regress/regress1/arrayinuf_error.smt2 b/test/regress/regress1/arrayinuf_error.smt2 index bc89dd0eb..6ff64e9cc 100644 --- a/test/regress/regress1/arrayinuf_error.smt2 +++ b/test/regress/regress1/arrayinuf_error.smt2 @@ -1,5 +1,6 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition -; EXPECT: (error "Parse Error: arrayinuf_error.smt2:8.21: Symbol 'Array' not declared as a type +; EXPECT: (error "Parse Error: arrayinuf_error.smt2:9.21: Symbol 'Array' not declared as a type ; EXPECT: ; EXPECT: (declare-fun a (Array Bool Bool)) ; EXPECT: ^ diff --git a/test/regress/regress1/errorcrash.smt2 b/test/regress/regress1/errorcrash.smt2 index 78df4324e..d42727f0d 100644 --- a/test/regress/regress1/errorcrash.smt2 +++ b/test/regress/regress1/errorcrash.smt2 @@ -1,6 +1,7 @@ +; DISABLE-TESTER: dump ; REQUIRES: no-competition ; EXIT: 1 -; EXPECT: (error "Parse Error: errorcrash.smt2:6.29: Symbol 'Array' not declared as a type") +; EXPECT: (error "Parse Error: errorcrash.smt2:7.29: Symbol 'Array' not declared as a type") (set-logic QF_UF) (declare-sort U 0) (declare-fun x () (Array U U)) diff --git a/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 index 3ab7495ea..1fa6225c7 100644 --- a/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 +++ b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.6) -(set-logic FP) +(set-logic FPLRA) (set-info :status unsat) (declare-fun c_main_~E0~7 () (_ FloatingPoint 11 53)) (declare-fun c_main_~S~7 () (_ FloatingPoint 11 53)) diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 3c0c974e2..362af1730 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -50,7 +50,7 @@ class Tester: if exit_status == STATUS_TIMEOUT: exit_code = EXIT_SKIP if g_args.skip_timeout else EXIT_FAILURE print("Timeout - Flags: {}".format(benchmark_info.command_line_args)) - elif output != benchmark_info.expected_output: + elif benchmark_info.compare_outputs and output != benchmark_info.expected_output: exit_code = EXIT_FAILURE print("not ok - Flags: {}".format(benchmark_info.command_line_args)) print() @@ -66,7 +66,7 @@ class Tester: print_colored(Color.YELLOW, error) print("=" * 80) print() - elif error != benchmark_info.expected_error: + elif benchmark_info.compare_outputs and error != benchmark_info.expected_error: exit_code = EXIT_FAILURE print( "not ok - Differences between expected and actual output on stderr - Flags: {}".format( @@ -245,12 +245,11 @@ class AbductTester(Tester): class DumpTester(Tester): def applies(self, benchmark_info): - return benchmark_info.expected_exit_status == EXIT_OK + return benchmark_info.benchmark_ext != ".p" def run(self, benchmark_info): ext_to_lang = { ".smt2": "smt2", - ".p": "tptp", ".sy": "sygus", } @@ -285,7 +284,8 @@ class DumpTester(Tester): "--lang={}".format(ext_to_lang[benchmark_info.benchmark_ext]), ], benchmark_basename=tmpf.name, - expected_output="", + expected_exit_status=0, + compare_outputs=False, ) ) os.remove(tmpf.name) @@ -329,6 +329,7 @@ BenchmarkInfo = collections.namedtuple( "expected_error", "expected_exit_status", "command_line_args", + "compare_outputs", ], ) @@ -624,6 +625,7 @@ def run_regression( expected_error=expected_error, expected_exit_status=expected_exit_status, command_line_args=all_args, + compare_outputs=True, ) for tester_name, tester in g_testers.items(): if tester_name in testers and tester.applies(benchmark_info):