From 167947ab81094de28251bb885c8cf84e7168c43b Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 3 Oct 2019 15:23:58 -0700 Subject: [PATCH] Disable proofs for unsupported logics (#3327) This commit makes CVC4 complain if the user asked for proofs for an unsupported logic (in this contest, ALL is considered unsupported). Changes in the regression script are introduced as well, in order to only request proofs for regressions in supported logics. --- src/smt/smt_engine.cpp | 12 +++----- test/regress/CMakeLists.txt | 1 + test/regress/regress0/proof_no_support.smt2 | 21 ++++++++++++++ test/regress/run_regression.py | 32 +++++++++++++++++++++ 4 files changed, 58 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress0/proof_no_support.smt2 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): -- 2.30.2