From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 3 Oct 2019 22:23:58 +0000 (-0700)
Subject: Disable proofs for unsupported logics (#3327)
X-Git-Tag: cvc5-1.0.0~3916
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=167947ab81094de28251bb885c8cf84e7168c43b;p=cvc5.git

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 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):