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.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f451d12bd7c2178eb1e1947c23158aa1bd5daa3e..918539f4fe98bb62c0c05733bb050eadc5dc4425 100644 (file)
--- 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 ca33b45c54ad42cf35083df7a869a9b79692fe90..a3ee076898e447e7a7929a73e2c83d993171d28e 100644 (file)
--- 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 (file)
index 0000000..3d19a10
--- /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 61b89d9c50b66737f2dfbdb315111a26340cc46a..c7eef8a1df2740bfa4f270ded220b986bd18e5f0 100755 (executable)
--- 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):