diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 12 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/proof_no_support.smt2 | 21 | ||||
| -rwxr-xr-x | test/regress/run_regression.py | 32 |
4 files changed, 58 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f451d12bd..918539f4f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2238,6 +2238,10 @@ void SmtEngine::setDefaults() { if (options::proof()) { + if (d_logic > LogicInfo("QF_AUFBVLRA")) { + throw OptionException( + "Proofs are only supported for sub-logics of QF_AUFBVLIA."); + } if (options::bitvectorAlgebraicSolver()) { if (options::bitvectorAlgebraicSolver.wasSetByUser()) @@ -4494,14 +4498,6 @@ void SmtEngine::checkProof() std::string logicString = d_logic.getLogicString(); - if (!(d_logic <= LogicInfo("QF_AUFBVLRA"))) - { - // This logic is not yet supported - Notice() << "Notice: no proof-checking for " << logicString << " proofs yet" - << endl; - return; - } - std::stringstream pfStream; pfStream << proof::plf_signatures << endl; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ca33b45c5..a3ee07689 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -598,6 +598,7 @@ set(regress_0_tests regress0/printer/empty_symbol_name.smt2 regress0/printer/let_shadowing.smt2 regress0/printer/tuples_and_records.cvc + regress0/proof_no_support.smt2 regress0/push-pop/boolean/fuzz_12.smt2 regress0/push-pop/boolean/fuzz_13.smt2 regress0/push-pop/boolean/fuzz_14.smt2 diff --git a/test/regress/regress0/proof_no_support.smt2 b/test/regress/regress0/proof_no_support.smt2 new file mode 100644 index 000000000..3d19a109e --- /dev/null +++ b/test/regress/regress0/proof_no_support.smt2 @@ -0,0 +1,21 @@ +;COMMAND-LINE: --check-proofs +;EXIT: 1 +;EXPECT: (error "Error in option parsing: Proofs are only supported for sub-logics of QF_AUFBVLIA.") +(set-logic ALL) + +(declare-const a Int) + +(assert (and + (= + a + (* a a) + ) + (not (= a 0)) + (not (= a 1)) + ) +) + +(check-sat) + + + diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 61b89d9c5..c7eef8a1d 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -79,6 +79,30 @@ def get_cvc4_features(cvc4_binary): return features +def logic_supported_with_proofs(logic): + assert logic is None or isinstance(logic, str) + return logic in [ + #single theories + "QF_BV", + "QF_UF", + "QF_A", + "QF_LRA", + #two theories + "QF_UFBV", + "QF_UFLRA", + "QF_AUF", + "QF_ALRA", + "QF_ABV", + "QF_BVLRA" + #three theories + "QF_AUFBV", + "QF_ABVLRA", + "QF_UFBVLRA", + "QF_AUFLRA", + #four theories + "QF_AUFBVLRA" + ] + def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc4_binary, command_line, benchmark_dir, benchmark_filename, timeout): """Runs CVC4 on the file `benchmark_filename` in the directory @@ -151,12 +175,14 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper, benchmark_dir = os.path.dirname(benchmark_path) comment_char = '%' status_regex = None + logic_regex = None status_to_output = lambda s: s if benchmark_ext == '.smt': status_regex = r':status\s*(sat|unsat)' comment_char = ';' elif benchmark_ext == '.smt2': status_regex = r'set-info\s*:status\s*(sat|unsat)' + logic_regex = r'\(\s*set-logic\s*(.*)\)' comment_char = ';' elif benchmark_ext == '.cvc': pass @@ -185,6 +211,7 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper, expected_exit_status = None command_lines = [] requires = [] + logic = None for line in benchmark_lines: # Skip lines that do not start with a comment character. if line[0] != comment_char: @@ -223,6 +250,10 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper, sys.exit('Cannot determine status of "{}"'.format(benchmark_path)) if expected_exit_status is None: expected_exit_status = 0 + if logic_regex: + logic_match = re.findall(logic_regex, benchmark_content) + if logic_match and len(logic_match) == 1: + logic = logic_match[0] if 'CVC4_REGRESSION_ARGS' in os.environ: basic_command_line_args += shlex.split( @@ -284,6 +315,7 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper, '--check-proofs' not in all_args and \ '--incremental' not in all_args and \ '--unconstrained-simp' not in all_args and \ + logic_supported_with_proofs(logic) and \ not cvc4_binary.endswith('pcvc4'): extra_command_line_args = ['--check-proofs'] if unsat_cores and re.search(r'^(unsat|valid)$', expected_output): |