From 9a33f9bb67f97d2de50da199caa3d5d9229aa7bd Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 7 Jun 2022 00:26:56 +0300 Subject: [PATCH] Disable `lfsc` tester if `proof` tester is disabled. (#8857) This automatically disables the `lfsc` tester for regressions where `proof` tester is disabled. --- test/regress/cli/README.md | 10 +++++++--- .../cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2 | 1 - .../cli/regress0/deep-restart/dd.wrong-sat-020322.smt2 | 1 - test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2 | 1 - .../cli/regress1/datatypes/dt-param-card4-unsat.smt2 | 1 - test/regress/cli/regress1/hole6.cvc.smt2 | 1 - test/regress/cli/regress1/issue3970-nl-ext-purify.smt2 | 1 - test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 | 1 - test/regress/cli/regress1/nl/issue4791-llr.smt2 | 1 - .../cli/regress1/quantifiers/issue4021-ind-opts.smt2 | 1 - test/regress/cli/regress1/sets/sets-disequal.smt2 | 1 - test/regress/cli/regress1/sygus/issue3201.smt2 | 1 - test/regress/cli/regress1/sygus/issue3247.smt2 | 1 - .../cli/regress1/sygus/issue3995-fmf-var-op.smt2 | 1 - test/regress/cli/regress1/sygus/issue4009-qep.smt2 | 1 - .../cli/regress1/sygus/issue4083-var-shadow.smt2 | 1 - .../cli/regress1/sygus/issue4425-sets-sygus-infer.smt2 | 1 - test/regress/cli/regress1/sygus/proj-issue185.smt2 | 1 - test/regress/cli/regress2/fp/issue7056.smt2 | 1 - test/regress/cli/regress2/instance_1444.smtv1.smt2 | 1 - .../cli/regress2/nl/ufnia-factor-open-proof.smt2 | 1 - test/regress/cli/run_regression.py | 2 ++ 22 files changed, 9 insertions(+), 23 deletions(-) diff --git a/test/regress/cli/README.md b/test/regress/cli/README.md index 020b9819b..efb3fc31f 100644 --- a/test/regress/cli/README.md +++ b/test/regress/cli/README.md @@ -124,10 +124,14 @@ excluded by adding the `no-` prefix, e.g. `no-cryptominisat` means that the test is not valid for builds that include CryptoMiniSat support. To disable a specific type of test, the `DISABLE-TESTER` directive can be used. -The following example disables the proof tester for a regression: +The following example disables the abduct tester for a regression: ``` -; DISABLE-TESTER: proof +; DISABLE-TESTER: abduct ``` -Multiple testers can be disabled using multiple `DISABLE-TESTER` directives. +Multiple testers can be disabled using multiple `DISABLE-TESTER` directives. In +general, each `DISABLE-TESTER` directive disables only the specified tester. The +only exception to this rule is the proof tester. Disabling the proof tester, +which directs cvc5 to check generated proofs internally, also disables testers +that check the printed versions of those proofs (e.g., the lfsc tester). diff --git a/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2 b/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2 index d5f2e21d8..4fdea35d4 100644 --- a/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2 +++ b/test/regress/cli/regress0/deep-restart/dd.fuzz21.smtv1.smt2 @@ -2,7 +2,6 @@ ; EXPECT: unsat ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic ALL) (declare-const v (_ BitVec 2)) (declare-const x7 Bool) diff --git a/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2 b/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2 index d39dc8dca..ed8cbf55d 100644 --- a/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2 +++ b/test/regress/cli/regress0/deep-restart/dd.wrong-sat-020322.smt2 @@ -2,7 +2,6 @@ ; EXPECT: unsat ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic ALL) (declare-sort E 0) (declare-fun s () (Seq E)) diff --git a/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2 b/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2 index a6b60b68d..0d36d2037 100644 --- a/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2 +++ b/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2 @@ -2,7 +2,6 @@ ; EXPECT: unsat ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic LRA) (set-info :status unsat) (assert (not (exists ((?X Real)) (>= (/ (- 13) 4) ?X)))) diff --git a/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 b/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 index 84dadda4b..269bc515b 100644 --- a/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 +++ b/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 @@ -1,4 +1,3 @@ -; DISABLE-TESTER: proof ; EXPECT: unsat (set-logic QF_ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress1/hole6.cvc.smt2 b/test/regress/cli/regress1/hole6.cvc.smt2 index 2eecb91cc..f1476c06d 100644 --- a/test/regress/cli/regress1/hole6.cvc.smt2 +++ b/test/regress/cli/regress1/hole6.cvc.smt2 @@ -1,4 +1,3 @@ -; DISABLE-TESTER: proof ; EXPECT: unsat (set-logic ALL) (set-option :incremental false) diff --git a/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2 b/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2 index ef58b42a2..a48660bd8 100644 --- a/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2 +++ b/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2 @@ -2,7 +2,6 @@ ; EXPECT: unsat ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic QF_UFNRA) (set-option :nl-ext-purify true) (set-option :sygus-inference true) diff --git a/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 b/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 index adbc5c216..355343d00 100644 --- a/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 +++ b/test/regress/cli/regress1/nl/approx-sqrt-unsat.smt2 @@ -1,4 +1,3 @@ -; DISABLE-TESTER: proof ; REQUIRES: poly ; COMMAND-LINE: --nl-ext-tplanes ; EXPECT: unsat diff --git a/test/regress/cli/regress1/nl/issue4791-llr.smt2 b/test/regress/cli/regress1/nl/issue4791-llr.smt2 index f11c925f8..fd88a59c0 100644 --- a/test/regress/cli/regress1/nl/issue4791-llr.smt2 +++ b/test/regress/cli/regress1/nl/issue4791-llr.smt2 @@ -2,7 +2,6 @@ ; EXPECT: unsat ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc ; ;!(a,b,c).( 0<=b & 1<=c & 0<=a & 1<=c diff --git a/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 index f8ecd754b..f64ea8e72 100644 --- a/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 @@ -1,6 +1,5 @@ ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic HO_ALL) (set-option :miniscope-quant agg) (set-option :conjecture-gen true) diff --git a/test/regress/cli/regress1/sets/sets-disequal.smt2 b/test/regress/cli/regress1/sets/sets-disequal.smt2 index 4b4785fb6..3acf77108 100644 --- a/test/regress/cli/regress1/sets/sets-disequal.smt2 +++ b/test/regress/cli/regress1/sets/sets-disequal.smt2 @@ -1,4 +1,3 @@ -; DISABLE-TESTER: proof ; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: sat diff --git a/test/regress/cli/regress1/sygus/issue3201.smt2 b/test/regress/cli/regress1/sygus/issue3201.smt2 index 831fce6d4..212fca782 100644 --- a/test/regress/cli/regress1/sygus/issue3201.smt2 +++ b/test/regress/cli/regress1/sygus/issue3201.smt2 @@ -2,7 +2,6 @@ ; COMMAND-LINE: --sygus-inference -q ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic ALL) (declare-fun v () Bool) (assert false) diff --git a/test/regress/cli/regress1/sygus/issue3247.smt2 b/test/regress/cli/regress1/sygus/issue3247.smt2 index a6f3f6951..7e2f439ce 100644 --- a/test/regress/cli/regress1/sygus/issue3247.smt2 +++ b/test/regress/cli/regress1/sygus/issue3247.smt2 @@ -2,7 +2,6 @@ ; COMMAND-LINE: --sygus-inference --strings-exp -q ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic ALL) (declare-fun a () String) (declare-fun b () String) diff --git a/test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2 index 6a41fc7a0..48b4ab38c 100644 --- a/test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2 +++ b/test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2 @@ -2,7 +2,6 @@ ; COMMAND-LINE: --sygus-inference --fmf-bound ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic HO_ALL) (declare-fun a () (_ BitVec 1)) (assert (bvsgt (bvsmod a a) #b0)) diff --git a/test/regress/cli/regress1/sygus/issue4009-qep.smt2 b/test/regress/cli/regress1/sygus/issue4009-qep.smt2 index 8f540bf13..b27901a11 100644 --- a/test/regress/cli/regress1/sygus/issue4009-qep.smt2 +++ b/test/regress/cli/regress1/sygus/issue4009-qep.smt2 @@ -2,7 +2,6 @@ ; COMMAND-LINE: --sygus-inference --sygus-qe-preproc -q ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic ALL) (declare-fun a () Real) (declare-fun b () Real) diff --git a/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 b/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 index 17a9dfa3c..4e867e8aa 100644 --- a/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 +++ b/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 @@ -2,7 +2,6 @@ ; EXPECT: unsat ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic ALL) (set-option :miniscope-quant conj-and-fv) (set-option :sygus-inference true) diff --git a/test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2 b/test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2 index 4e35869b6..466bb7313 100644 --- a/test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2 +++ b/test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2 @@ -2,7 +2,6 @@ ; EXPECT: unsat ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic ALL) (declare-fun a () Int) (declare-fun d () Int) diff --git a/test/regress/cli/regress1/sygus/proj-issue185.smt2 b/test/regress/cli/regress1/sygus/proj-issue185.smt2 index b6228d453..141ab0ae0 100644 --- a/test/regress/cli/regress1/sygus/proj-issue185.smt2 +++ b/test/regress/cli/regress1/sygus/proj-issue185.smt2 @@ -2,7 +2,6 @@ ; EXPECT: unsat ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic ALL) (set-option :sygus-inference true) (set-info :status unsat) diff --git a/test/regress/cli/regress2/fp/issue7056.smt2 b/test/regress/cli/regress2/fp/issue7056.smt2 index 17b439a83..e9283c38b 100644 --- a/test/regress/cli/regress2/fp/issue7056.smt2 +++ b/test/regress/cli/regress2/fp/issue7056.smt2 @@ -1,6 +1,5 @@ ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc ; timeout with unsat cores (set-logic ALL) (set-info :smt-lib-version 2.6) diff --git a/test/regress/cli/regress2/instance_1444.smtv1.smt2 b/test/regress/cli/regress2/instance_1444.smtv1.smt2 index fc4cd5802..3b25eb264 100644 --- a/test/regress/cli/regress2/instance_1444.smtv1.smt2 +++ b/test/regress/cli/regress2/instance_1444.smtv1.smt2 @@ -1,4 +1,3 @@ -; DISABLE-TESTER: lfsc ; DISABLE-TESTER: proof (set-option :incremental false) (set-info :status unsat) diff --git a/test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2 b/test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2 index 52cb8f9e6..5b6c534b1 100644 --- a/test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2 +++ b/test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2 @@ -1,6 +1,5 @@ ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: proof -; DISABLE-TESTER: lfsc (set-logic QF_UFNIA) (set-info :status unsat) (declare-fun p2 (Int) Int) diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py index edaf2005b..87cb2b551 100755 --- a/test/regress/cli/run_regression.py +++ b/test/regress/cli/run_regression.py @@ -613,6 +613,8 @@ def run_regression( return EXIT_FAILURE if disable_tester in testers: testers.remove(disable_tester) + if disable_tester == "proof" and "lfsc" in testers: + testers.remove("lfsc") expected_output = expected_output.strip() expected_error = expected_error.strip() -- 2.30.2