From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Thu, 21 Apr 2022 06:45:04 +0000 (-0500) Subject: Add tester for LFSC printer. (#8606) X-Git-Tag: cvc5-1.0.1~233 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=017507462863ff79583df3ce5eb2b24ad0c75611;p=cvc5.git Add tester for LFSC printer. (#8606) This adds an option to check the LFSC proofs generated by `cvc5` for unsat benchmarks. This does not enable the tester in CI as it fails for many benchmarks. --- diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index ca74fc74f..8dcc979d4 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -3201,7 +3201,10 @@ macro(cvc5_add_regression_test level file) add_test(${file} ${run_regress_script} ${RUN_REGRESSION_ARGS} - ${path_to_cvc5}/cvc5 ${CMAKE_CURRENT_LIST_DIR}/${file}) + --lfsc-binary ${CMAKE_SOURCE_DIR}/deps/bin/lfscc + --lfsc-sig-dir ${CMAKE_SOURCE_DIR}/proofs/lfsc/signatures + ${path_to_cvc5}/cvc5 + ${CMAKE_CURRENT_LIST_DIR}/${file}) set_tests_properties(${file} PROPERTIES LABELS "regress${level}") # For CMake 3.9.0 and newer, skipped tests do not count as a failure anymore: diff --git a/test/regress/cli/regress0/bv/div_mod.cvc.smt2 b/test/regress/cli/regress0/bv/div_mod.cvc.smt2 index be61e155a..b35a8b6d6 100644 --- a/test/regress/cli/regress0/bv/div_mod.cvc.smt2 +++ b/test/regress/cli/regress0/bv/div_mod.cvc.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; EXPECT: unsat (set-logic ALL) (set-option :incremental false) diff --git a/test/regress/cli/regress0/bv/fuzz15.delta01.smtv1.smt2 b/test/regress/cli/regress0/bv/fuzz15.delta01.smtv1.smt2 index f16084981..22ca98ba5 100644 --- a/test/regress/cli/regress0/bv/fuzz15.delta01.smtv1.smt2 +++ b/test/regress/cli/regress0/bv/fuzz15.delta01.smtv1.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-option :incremental false) (set-info :status unsat) (set-logic QF_BV) diff --git a/test/regress/cli/regress0/bv/fuzz38.delta01.smtv1.smt2 b/test/regress/cli/regress0/bv/fuzz38.delta01.smtv1.smt2 index cc5d99e18..0c4f1c197 100644 --- a/test/regress/cli/regress0/bv/fuzz38.delta01.smtv1.smt2 +++ b/test/regress/cli/regress0/bv/fuzz38.delta01.smtv1.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-option :incremental false) (set-info :status unsat) (set-logic QF_BV) diff --git a/test/regress/cli/regress0/fp/issue-5524.smt2 b/test/regress/cli/regress0/fp/issue-5524.smt2 index 3e9696871..f5f2024c0 100644 --- a/test/regress/cli/regress0/fp/issue-5524.smt2 +++ b/test/regress/cli/regress0/fp/issue-5524.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --bv-solver=bitblast ; EXPECT: unsat (set-logic QF_FPLRA) diff --git a/test/regress/cli/regress0/fp/rti_3_5_bug.smt2 b/test/regress/cli/regress0/fp/rti_3_5_bug.smt2 index 724e08b8c..c2144dfc4 100644 --- a/test/regress/cli/regress0/fp/rti_3_5_bug.smt2 +++ b/test/regress/cli/regress0/fp/rti_3_5_bug.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --fp-exp ; EXPECT: unsat diff --git a/test/regress/cli/regress0/fp/word-blast.smt2 b/test/regress/cli/regress0/fp/word-blast.smt2 index 65290a3b3..1e8ae7320 100644 --- a/test/regress/cli/regress0/fp/word-blast.smt2 +++ b/test/regress/cli/regress0/fp/word-blast.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --fp-lazy-wb ; EXPECT: unsat (set-logic QF_BVFP) diff --git a/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2 b/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2 index 0d36d2037..a6b60b68d 100644 --- a/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2 +++ b/test/regress/cli/regress0/quantifiers/lra-triv-gn.smt2 @@ -2,6 +2,7 @@ ; 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/regress0/seq/seq-types.smt2 b/test/regress/cli/regress0/seq/seq-types.smt2 index 3facf688a..f8d8aa8b3 100644 --- a/test/regress/cli/regress0/seq/seq-types.smt2 +++ b/test/regress/cli/regress0/seq/seq-types.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --strings-exp ;EXPECT: unsat (set-logic ALL) diff --git a/test/regress/cli/regress1/aufbv/bug348.smtv1.smt2 b/test/regress/cli/regress1/aufbv/bug348.smtv1.smt2 index a1fc92d77..b5c99bd9f 100644 --- a/test/regress/cli/regress1/aufbv/bug348.smtv1.smt2 +++ b/test/regress/cli/regress1/aufbv/bug348.smtv1.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --bv-solver=bitblast (set-option :incremental false) (set-info :status unsat) diff --git a/test/regress/cli/regress1/auflia/bug330.smt2 b/test/regress/cli/regress1/auflia/bug330.smt2 index ada1fd8d5..13b052821 100644 --- a/test/regress/cli/regress1/auflia/bug330.smt2 +++ b/test/regress/cli/regress1/auflia/bug330.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-logic QF_AUFLIA) (set-info :source | Translated from old SVC processor verification benchmarks. Contact Clark diff --git a/test/regress/cli/regress1/bv/divtest.smt2 b/test/regress/cli/regress1/bv/divtest.smt2 index fe91cb87b..c3c3ad7be 100644 --- a/test/regress/cli/regress1/bv/divtest.smt2 +++ b/test/regress/cli/regress1/bv/divtest.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-logic QF_BV) (set-info :status unsat) (declare-fun x1 () (_ BitVec 12)) diff --git a/test/regress/cli/regress1/bv/fuzz38.smtv1.smt2 b/test/regress/cli/regress1/bv/fuzz38.smtv1.smt2 index d9f6d46b2..68af8acfc 100644 --- a/test/regress/cli/regress1/bv/fuzz38.smtv1.smt2 +++ b/test/regress/cli/regress1/bv/fuzz38.smtv1.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-option :incremental false) (set-info :status unsat) (set-logic QF_BV) diff --git a/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2 b/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2 index 8d79f91e2..06ff3aa27 100644 --- a/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2 +++ b/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-option :incremental false) (set-info :status unsat) (set-logic QF_BV) diff --git a/test/regress/cli/regress1/bv/proj-issue438-prerewrite-fixed-point-original.smt2 b/test/regress/cli/regress1/bv/proj-issue438-prerewrite-fixed-point-original.smt2 index 62d769bc2..f34d04427 100644 --- a/test/regress/cli/regress1/bv/proj-issue438-prerewrite-fixed-point-original.smt2 +++ b/test/regress/cli/regress1/bv/proj-issue438-prerewrite-fixed-point-original.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-logic QF_BV) (declare-const T (_ BitVec 1)) (assert (and (bvsle (_ bv0 32) (bvadd (bvadd (_ bv1 32) (_ bv0 32)) ((_ zero_extend 24) ((_ extract 15 8) (bvshl ((_ zero_extend 24) ((_ extract 15 8) (bvsub (bvxor ((_ zero_extend 24) ((_ extract 15 8) (bvsub ((_ zero_extend 24) ((_ extract 7 0) (bvxor (bvadd ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) (bvsub (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) ((_ extract 15 8) (bvsub (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvsub (bvxor (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (bvxor (_ bv0 8) ((_ extract 7 0) ((_ extract 7 0) (bvxor (bvadd (_ bv0 32) ((_ zero_extend 24) ((_ extract 15 8) (bvsub ((_ zero_extend 24) ((_ extract 7 0) (bvsub (bvxor ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) (bvshl ((_ zero_extend 24) (bvxor (bvxor (_ bv0 8) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (_ bv0 8) ((_ extract 7 0) (bvxor (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (_ bv0 8) ((_ extract 7 0) (bvsub (_ bv0 32) ((_ zero_extend 24) ((_ zero_extend 7) T))))))) (_ bv0 32)))))))) (_ bv0 8))) (_ bv0 32))))) (_ bv0 32)) (_ bv1 32)))) (_ bv1 32))))) (_ bv0 32))))) (_ bv0 8)))))) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)))) (_ bv0 32)) (_ bv1 32))))))) (_ bv0 32)) (_ bv0 32))))) (_ bv0 32)) (_ bv0 32)))) (_ bv1 32)))) (_ bv0 32)) (_ bv1 32)))) (_ bv1 32)))))) (= (_ bv0 32) (bvxor (_ bv0 32) (bvadd (bvadd (_ bv1 32) (_ bv0 32)) ((_ zero_extend 24) ((_ extract 15 8) (bvshl ((_ zero_extend 24) ((_ extract 15 8) (bvsub (bvxor ((_ zero_extend 24) ((_ extract 15 8) (bvsub ((_ zero_extend 24) ((_ extract 7 0) (bvxor (bvadd ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) (bvsub (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) ((_ extract 15 8) (bvsub (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvsub (bvxor (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (bvxor (_ bv0 8) ((_ extract 7 0) ((_ extract 7 0) (bvxor (bvadd (_ bv0 32) ((_ zero_extend 24) ((_ extract 15 8) (bvsub ((_ zero_extend 24) ((_ extract 7 0) (bvsub (bvxor ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) (bvshl ((_ zero_extend 24) (bvxor (bvxor (_ bv0 8) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (_ bv0 8) ((_ extract 7 0) (bvxor (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (_ bv0 8) ((_ extract 7 0) (bvsub (_ bv0 32) ((_ zero_extend 24) ((_ zero_extend 7) T))))))) (_ bv0 32)))))))) (_ bv0 8))) (_ bv0 32))))) (_ bv0 32)) (_ bv1 32)))) (_ bv1 32))))) (_ bv0 32))))) (_ bv0 8)))))) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)))) (_ bv0 32)) (_ bv1 32))))))) (_ bv0 32)) (_ bv0 32))))) (_ bv0 32)) (_ bv0 32)))) (_ bv1 32)))) (_ bv0 32)) (_ bv1 32)))) (_ bv1 32))))))))) diff --git a/test/regress/cli/regress1/bvdiv2.smt2 b/test/regress/cli/regress1/bvdiv2.smt2 index 67d583c76..251b76c03 100644 --- a/test/regress/cli/regress1/bvdiv2.smt2 +++ b/test/regress/cli/regress1/bvdiv2.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.6) (set-info :category "crafted") diff --git a/test/regress/cli/regress1/fp/rti_3_5_bug_report.smt2 b/test/regress/cli/regress1/fp/rti_3_5_bug_report.smt2 index 6c0b68c95..146942cec 100644 --- a/test/regress/cli/regress1/fp/rti_3_5_bug_report.smt2 +++ b/test/regress/cli/regress1/fp/rti_3_5_bug_report.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --fp-exp ; EXPECT: unsat diff --git a/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2 b/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2 index a48660bd8..ef58b42a2 100644 --- a/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2 +++ b/test/regress/cli/regress1/issue3970-nl-ext-purify.smt2 @@ -2,6 +2,7 @@ ; 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/quantifiers/NUM878.smt2 b/test/regress/cli/regress1/quantifiers/NUM878.smt2 index 6f26e7af2..93261330e 100644 --- a/test/regress/cli/regress1/quantifiers/NUM878.smt2 +++ b/test/regress/cli/regress1/quantifiers/NUM878.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --cegqi-bv ; EXPECT: unsat (set-logic BV) diff --git a/test/regress/cli/regress1/quantifiers/inst-max-level-segf.smt2 b/test/regress/cli/regress1/quantifiers/inst-max-level-segf.smt2 index 47cfae0ef..9bb21cae8 100644 --- a/test/regress/cli/regress1/quantifiers/inst-max-level-segf.smt2 +++ b/test/regress/cli/regress1/quantifiers/inst-max-level-segf.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --inst-max-level=0 --simplification=none ; EXPECT: unsat (set-logic UF) diff --git a/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 index f64ea8e72..f8ecd754b 100644 --- a/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 @@ -1,5 +1,6 @@ ; 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/quantifiers/qbv-test-invert-bvcomp.smt2 b/test/regress/cli/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 index ed9c9880f..f0eab9503 100644 --- a/test/regress/cli/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 +++ b/test/regress/cli/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: unsat (set-logic BV) diff --git a/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 b/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 index 97af47a37..eeba7883b 100644 --- a/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 +++ b/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --strings-exp --seq-array=eager ; EXPECT: unsat (set-logic ALL) diff --git a/test/regress/cli/regress1/quantifiers/tpp-unit-fail-qbv.smt2 b/test/regress/cli/regress1/quantifiers/tpp-unit-fail-qbv.smt2 index 2ef929551..0b46717ec 100644 --- a/test/regress/cli/regress1/quantifiers/tpp-unit-fail-qbv.smt2 +++ b/test/regress/cli/regress1/quantifiers/tpp-unit-fail-qbv.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-logic BV) (set-info :status unsat) (declare-fun t () (_ BitVec 4)) diff --git a/test/regress/cli/regress1/sets/comp-intersect.smt2 b/test/regress/cli/regress1/sets/comp-intersect.smt2 index 5f6f7576b..4f1de2e35 100644 --- a/test/regress/cli/regress1/sets/comp-intersect.smt2 +++ b/test/regress/cli/regress1/sets/comp-intersect.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --sets-ext ; EXPECT: unsat (set-logic ALL) diff --git a/test/regress/cli/regress1/sets/comp-odd.smt2 b/test/regress/cli/regress1/sets/comp-odd.smt2 index 5d2a65619..05450865a 100644 --- a/test/regress/cli/regress1/sets/comp-odd.smt2 +++ b/test/regress/cli/regress1/sets/comp-odd.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --sets-ext ; EXPECT: unsat (set-logic ALL) diff --git a/test/regress/cli/regress1/sets/comp-pos-member.smt2 b/test/regress/cli/regress1/sets/comp-pos-member.smt2 index fdd5926b6..34c4d2870 100644 --- a/test/regress/cli/regress1/sets/comp-pos-member.smt2 +++ b/test/regress/cli/regress1/sets/comp-pos-member.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --sets-ext --full-saturate-quant ; EXPECT: unsat (set-logic ALL) diff --git a/test/regress/cli/regress1/sets/comp-positive.smt2 b/test/regress/cli/regress1/sets/comp-positive.smt2 index 6f8e3e1ab..be28deda1 100644 --- a/test/regress/cli/regress1/sets/comp-positive.smt2 +++ b/test/regress/cli/regress1/sets/comp-positive.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --sets-ext ; EXPECT: unsat (set-logic ALL) diff --git a/test/regress/cli/regress1/sygus/issue3201.smt2 b/test/regress/cli/regress1/sygus/issue3201.smt2 index 212fca782..831fce6d4 100644 --- a/test/regress/cli/regress1/sygus/issue3201.smt2 +++ b/test/regress/cli/regress1/sygus/issue3201.smt2 @@ -2,6 +2,7 @@ ; 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 7e2f439ce..a6f3f6951 100644 --- a/test/regress/cli/regress1/sygus/issue3247.smt2 +++ b/test/regress/cli/regress1/sygus/issue3247.smt2 @@ -2,6 +2,7 @@ ; 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 48b4ab38c..6a41fc7a0 100644 --- a/test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2 +++ b/test/regress/cli/regress1/sygus/issue3995-fmf-var-op.smt2 @@ -2,6 +2,7 @@ ; 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 b27901a11..8f540bf13 100644 --- a/test/regress/cli/regress1/sygus/issue4009-qep.smt2 +++ b/test/regress/cli/regress1/sygus/issue4009-qep.smt2 @@ -2,6 +2,7 @@ ; 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 4e867e8aa..17a9dfa3c 100644 --- a/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 +++ b/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 @@ -2,6 +2,7 @@ ; 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 466bb7313..4e35869b6 100644 --- a/test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2 +++ b/test/regress/cli/regress1/sygus/issue4425-sets-sygus-infer.smt2 @@ -2,6 +2,7 @@ ; 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 141ab0ae0..b6228d453 100644 --- a/test/regress/cli/regress1/sygus/proj-issue185.smt2 +++ b/test/regress/cli/regress1/sygus/proj-issue185.smt2 @@ -2,6 +2,7 @@ ; 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/bug349.smtv1.smt2 b/test/regress/cli/regress2/bug349.smtv1.smt2 index ffbd7f331..f8375a3ae 100644 --- a/test/regress/cli/regress2/bug349.smtv1.smt2 +++ b/test/regress/cli/regress2/bug349.smtv1.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc ; COMMAND-LINE: --bv-solver=bitblast (set-option :incremental false) (set-info :status unsat) diff --git a/test/regress/cli/regress2/fp/issue7056.smt2 b/test/regress/cli/regress2/fp/issue7056.smt2 index e419a5a6f..17b439a83 100644 --- a/test/regress/cli/regress2/fp/issue7056.smt2 +++ b/test/regress/cli/regress2/fp/issue7056.smt2 @@ -1,5 +1,6 @@ -; DISABLE-TESTER: proof ; 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 3b25eb264..fc4cd5802 100644 --- a/test/regress/cli/regress2/instance_1444.smtv1.smt2 +++ b/test/regress/cli/regress2/instance_1444.smtv1.smt2 @@ -1,3 +1,4 @@ +; 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 0f67a5a5d..720b2e075 100644 --- a/test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2 +++ b/test/regress/cli/regress2/nl/ufnia-factor-open-proof.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-logic QF_UFNIA) (set-info :status unsat) (declare-fun p2 (Int) Int) diff --git a/test/regress/cli/regress2/ooo.tag10.smt2 b/test/regress/cli/regress2/ooo.tag10.smt2 index 2d5cb3b37..45a1bb08b 100644 --- a/test/regress/cli/regress2/ooo.tag10.smt2 +++ b/test/regress/cli/regress2/ooo.tag10.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: lfsc (set-logic QF_UFIDL) (set-info :source | UCLID benchmark suite. See UCLID project: http://www.cs.cmu.edu/~uclid diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py index af46438ec..dca1af1d1 100755 --- a/test/regress/cli/run_regression.py +++ b/test/regress/cli/run_regression.py @@ -44,15 +44,26 @@ class Tester: def applies(self, benchmark_info): return True + def check_exit_status(self, name, expected_exit_status, exit_status, output, error, flags): + if exit_status == STATUS_TIMEOUT: + print("Timeout ({}) - Flags: {}".format(name, flags)) + return EXIT_SKIP if g_args.skip_timeout else EXIT_FAILURE + elif exit_status != expected_exit_status: + print('not ok ({}) - Expected exit status "{}" but got "{}" - Flags: {}'.format( + name, expected_exit_status, exit_status, flags)) + print() + print_outputs(output, error) + return EXIT_FAILURE + return None + def run(self, benchmark_info): - exit_code = EXIT_OK output, error, exit_status = run_benchmark(benchmark_info) - if exit_status == STATUS_TIMEOUT: - exit_code = EXIT_SKIP if g_args.skip_timeout else EXIT_FAILURE - print("Timeout - Flags: {}".format(benchmark_info.command_line_args)) - elif benchmark_info.compare_outputs and output != benchmark_info.expected_output: - exit_code = EXIT_FAILURE - print("not ok - Flags: {}".format(benchmark_info.command_line_args)) + exit_code = self.check_exit_status( + "cvc5", benchmark_info.expected_exit_status, exit_status, output, error, benchmark_info.command_line_args) + if exit_code: + return exit_code + if benchmark_info.compare_outputs and output != benchmark_info.expected_output: + print("not ok (cvc5) - Flags: {}".format(benchmark_info.command_line_args)) print() print("Standard output difference") print("=" * 80) @@ -62,14 +73,11 @@ class Tester: print() if error: print("Error output") - print("=" * 80) - print_colored(Color.YELLOW, error) - print("=" * 80) - print() - elif benchmark_info.compare_outputs and error != benchmark_info.expected_error: - exit_code = EXIT_FAILURE + print_segment(Color.YELLOW, error) + return EXIT_FAILURE + if benchmark_info.compare_outputs and error != benchmark_info.expected_error: print( - "not ok - Differences between expected and actual output on stderr - Flags: {}".format( + "not ok (cvc5) - Differences between expected and actual output on stderr - Flags: {}".format( benchmark_info.command_line_args ) ) @@ -79,30 +87,9 @@ class Tester: print_diff(error, benchmark_info.expected_error) print("=" * 80) print() - elif exit_status != benchmark_info.expected_exit_status: - exit_code = EXIT_FAILURE - print( - 'not ok - Expected exit status "{}" but got "{}" - Flags: {}'.format( - benchmark_info.expected_exit_status, - exit_status, - benchmark_info.command_line_args, - ) - ) - print() - print("Output:") - print("=" * 80) - print_colored(Color.BLUE, output) - print("=" * 80) - print() - print() - print("Error output:") - print("=" * 80) - print_colored(Color.YELLOW, error) - print("=" * 80) - print() - else: - print("ok - Flags: {}".format(benchmark_info.command_line_args)) - return exit_code + return EXIT_FAILURE + print("ok - Flags: {}".format(benchmark_info.command_line_args)) + return EXIT_OK ################################################################################ @@ -165,11 +152,68 @@ class ProofTester(Tester): def run(self, benchmark_info): return super().run( benchmark_info._replace( - command_line_args=benchmark_info.command_line_args + ["--check-proofs", "--proof-granularity=theory-rewrite"] + command_line_args=benchmark_info.command_line_args + + ["--check-proofs", "--proof-granularity=theory-rewrite"] ) ) +class LfscTester(Tester): + def applies(self, benchmark_info): + return ( + benchmark_info.benchmark_ext != ".sy" + and benchmark_info.expected_output.strip() == "unsat" + ) + + def run(self, benchmark_info): + with tempfile.NamedTemporaryFile() as tmpf: + proof_args = [ + "--dump-proofs", + "--proof-format=lfsc", + "--proof-granularity=theory-rewrite", + ] + output, error, exit_status = run_process( + [benchmark_info.cvc5_binary] + + benchmark_info.command_line_args + + proof_args + + [benchmark_info.benchmark_basename], + benchmark_info.benchmark_dir, + benchmark_info.timeout, + ) + tmpf.write(output.strip("unsat\n".encode())) + tmpf.flush() + output, error = output.decode(), error.decode() + exit_code = self.check_exit_status( + "cvc5", EXIT_OK, exit_status, output, error, benchmark_info.command_line_args) + if exit_code: + return exit_code + if "check" not in output: + print('not ok (cvc5) - Empty proof - Flags: {}'.format(exit_status, + benchmark_info.command_line_args)) + print() + print_outputs(output, error) + return EXIT_FAILURE + output, error, exit_status = run_process( + [benchmark_info.lfsc_binary] + + benchmark_info.lfsc_sigs + [tmpf.name], + benchmark_info.benchmark_dir, + timeout=benchmark_info.timeout, + ) + output, error = output.decode(), error.decode() + exit_code = self.check_exit_status( + "lfsc", EXIT_OK, exit_status, output, error, benchmark_info.command_line_args) + if exit_code: + return exit_code + if "success" not in output: + print( + "not ok (lfsc) - Unexpected output - Flags: {}".format(benchmark_info.command_line_args)) + print() + print_outputs(output, error) + return EXIT_FAILURE + print("ok - Flags: {}".format(benchmark_info.command_line_args)) + return EXIT_OK + + class ModelTester(Tester): def __init__(self): pass @@ -288,6 +332,7 @@ g_testers = { "base": BaseTester(), "unsat-core": UnsatCoreTester(), "proof": ProofTester(), + "lfsc": LfscTester(), "model": ModelTester(), "synth": SynthTester(), "abduct": AbductTester(), @@ -313,6 +358,8 @@ BenchmarkInfo = collections.namedtuple( "error_scrubber", "timeout", "cvc5_binary", + "lfsc_binary", + "lfsc_sigs", "benchmark_dir", "benchmark_basename", "benchmark_ext", @@ -347,6 +394,24 @@ def print_colored(color, text): print(color + line + Color.ENDC) +def print_segment(color, text): + """Prints colored `text` inside a border.""" + print("=" * 80) + for line in text.splitlines(): + print(color + line + Color.ENDC) + print("=" * 80) + print() + + +def print_outputs(stdout, stderr): + """Prints standard output and error.""" + print("Output:") + print_segment(Color.BLUE, stdout) + print() + print("Error output:") + print_segment(Color.YELLOW, stderr) + + def print_diff(actual, expected): """Prints the difference between `actual` and `expected`.""" @@ -372,8 +437,8 @@ def run_process(args, cwd, timeout, s_input=None): cmd = " ".join([shlex.quote(a) for a in args]) if isinstance(args, list) else args - out = "" - err = "" + out = bytes() + err = bytes() exit_status = STATUS_TIMEOUT try: # Instead of setting shell=True, we explicitly call bash. Using @@ -471,6 +536,8 @@ def run_regression( testers, wrapper, cvc5_binary, + lfsc_binary, + lfsc_sigs, benchmark_path, timeout, ): @@ -611,6 +678,8 @@ def run_regression( error_scrubber=error_scrubber, timeout=timeout, cvc5_binary=cvc5_binary, + lfsc_binary=lfsc_binary, + lfsc_sigs=lfsc_sigs, benchmark_dir=benchmark_dir, benchmark_basename=benchmark_basename, benchmark_ext=benchmark_ext, @@ -656,6 +725,8 @@ def main(): parser.add_argument("--use-skip-return-code", action="store_true") parser.add_argument("--skip-timeout", action="store_true") parser.add_argument("--tester", choices=g_testers.keys(), action="append") + parser.add_argument("--lfsc-binary", default="") + parser.add_argument("--lfsc-sig-dir", default="") parser.add_argument("wrapper", nargs="*") parser.add_argument("cvc5_binary") parser.add_argument("benchmark") @@ -668,6 +739,7 @@ def main(): g_args = parser.parse_args(argv) cvc5_binary = os.path.abspath(g_args.cvc5_binary) + lfsc_binary = os.path.abspath(g_args.lfsc_binary) wrapper = g_args.wrapper if os.environ.get("VALGRIND") == "1" and not wrapper: @@ -679,10 +751,24 @@ def main(): if not testers: testers = g_default_testers + lfsc_sigs = [] + if not g_args.lfsc_sig_dir == "": + lfsc_sig_dir = os.path.abspath(g_args.lfsc_sig_dir) + # `os.listdir` would be more appropriate if lfsc did not force us to + # list the signatures in order. + lfsc_sigs = ["core_defs", "util_defs", "theory_def", "nary_programs", + "boolean_programs", "boolean_rules", "cnf_rules", + "equality_rules", "arith_programs", "arith_rules", + "strings_programs", "strings_rules", "quantifiers_rules"] + lfsc_sigs = [os.path.join(lfsc_sig_dir, sig + ".plf") + for sig in lfsc_sigs] + return run_regression( testers, wrapper, cvc5_binary, + lfsc_binary, + lfsc_sigs, g_args.benchmark, timeout, )