From: Andres Noetzli Date: Wed, 1 Jul 2020 15:44:21 +0000 (-0700) Subject: Add testing infrastructure for LFSC signatures (#4678) X-Git-Tag: cvc5-1.0.0~3155 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9ce4c3153d42bc079470b7bd73bf131499b3fcbe;p=cvc5.git Add testing infrastructure for LFSC signatures (#4678) This commit adds testing infrastructure for LFSC signatures that is enabled when CVC4 is configured with LFSC. The testing infrastructure adopts run_test.py from https://github.com/CVC4/LFSC with minor modifications (mainly adding support for a list of include directories that are searched to resolve *.plf dependencies). The commit uses the existing examples and test files from proofs/signatures as the initial set of tests. Co-authored-by: Alex Ozdemir aozdemir@hmc.edu --- diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake index 6135c7891..786af14be 100644 --- a/cmake/FindLFSC.cmake +++ b/cmake/FindLFSC.cmake @@ -3,15 +3,17 @@ # LFSC_INCLUDE_DIR - the LFSC include directory # LFSC_LIBRARIES - Libraries needed to use LFSC +find_program(LFSC_BINARY NAMES lfscc) find_path(LFSC_INCLUDE_DIR NAMES lfscc.h) find_library(LFSC_LIBRARIES NAMES lfscc) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(LFSC DEFAULT_MSG - LFSC_INCLUDE_DIR LFSC_LIBRARIES) + LFSC_BINARY LFSC_INCLUDE_DIR LFSC_LIBRARIES) -mark_as_advanced(LFSC_INCLUDE_DIR LFSC_LIBRARIES) -if(LFSC_LIBRARIES) +mark_as_advanced(LFSC_BINARY LFSC_INCLUDE_DIR LFSC_LIBRARIES) +if(LFSC_FOUND) + message(STATUS "Found LFSC include dir: ${LFSC_INCLUDE_DIR}") message(STATUS "Found LFSC libs: ${LFSC_LIBRARIES}") endif() diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index 2f70bbfbd..ad3c8ec8d 100644 --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -1,4 +1,4 @@ -; Depends on lrat.plf +; Deps: lrat.plf ; ; Implementation of DRAT checking. ; diff --git a/proofs/signatures/drat_test.plf b/proofs/signatures/drat_test.plf deleted file mode 100644 index 2ede6df34..000000000 --- a/proofs/signatures/drat_test.plf +++ /dev/null @@ -1,434 +0,0 @@ -;depends on drat.plf -(declare TestSuccess type) - -; Test for clause_eq -(declare test_clause_eq - (! a clause - (! b clause - (! result bool - (! (^ - (bool_and - (bool_eq (clause_eq a b) result) - (bool_and - (bool_eq (clause_eq b a) result) - (bool_and - (bool_eq (clause_eq a a) tt) - (bool_eq (clause_eq b b) tt)))) - tt) - TestSuccess))))) - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (neg b) cln)) - (@ c2 (clc (pos a) (clc (neg b) cln)) - (: TestSuccess - (test_clause_eq c1 c2 tt))))))) - -(check - (% a var - (% b var - (@ c1 (clc (neg a) (clc (neg b) cln)) - (@ c2 (clc (pos a) (clc (neg b) cln)) - (: TestSuccess - (test_clause_eq c1 c2 ff))))))) - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (pos b) cln)) - (@ c2 (clc (pos a) (clc (neg b) cln)) - (: TestSuccess - (test_clause_eq c1 c2 ff))))))) - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (pos a) cln)) - (@ c2 (clc (pos a) (clc (neg b) cln)) - (: TestSuccess - (test_clause_eq c1 c2 ff))))))) - -(check - (% a var - (% b var - (@ c1 (clc (neg b) (clc (pos a) (clc (neg a) cln))) - (@ c1 (clc (neg a) (clc (neg b) (clc (pos a) cln))) - (: TestSuccess - (test_clause_eq c1 c2 ff))))))) - - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (pos a) (clc (neg b) cln))) - (@ c2 (clc (pos a) (clc (neg b) cln)) - (: TestSuccess - (test_clause_eq c1 c2 tt))))))) - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (pos a) (clc (neg b) cln))) - (@ c2 (clc (pos a) (clc (neg b) (clc (neg b) cln))) - (: TestSuccess - (test_clause_eq c1 c2 tt))))))) - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (pos a) (clc (neg a) cln))) - (@ c2 (clc (pos a) (clc (neg a) (clc (neg a) cln))) - (: TestSuccess - (test_clause_eq c1 c2 tt))))))) - -(check - (% a var - (% b var - (@ c1 cln - (@ c2 (clc (pos a) (clc (neg a) (clc (neg a) cln))) - (: TestSuccess - (test_clause_eq c1 c2 ff))))))) - -(declare check_rat - (! f cnf - (! c clause - (! b bool - (! sc (^ (is_rat f c) b) - bottom))))) - -(declare trust_cnf (! f cnf (cnf_holds f))) - -; RAT Test 1 -; Formula: (-p, -a) ^ (-p, b) ^( b, c) ^ (-c, a) -; Candidate RAT: (p, a) -; Answer: true -(check - (% va var - (% vb var - (% vc var - (% vp var - (check_rat - (cnfc (clc (neg vp) (clc (neg va) cln)) - (cnfc (clc (neg vp) (clc (pos vb) cln)) - (cnfc (clc (pos vb) (clc (pos vc) cln)) - (cnfc (clc (neg vc) (clc (pos va) cln)) cnfn)))) - (clc (pos vp) (clc (pos va) cln)) - tt)))))) - -; RAT Test 2 -; Formula: -; p cnf 4 8 -; 1 2 -3 0 -; -1 -2 3 0 -; 2 3 -4 0 -; -2 -3 4 0 -; -1 -3 -4 0 -; 1 3 4 0 -; -1 2 4 0 -; 1 -2 -4 0 -; Candidate RAT: -1 -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (check_rat - (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - cnfn)))))))) - (clc (neg v1) cln) - tt)))))) - -; RAT Test 3 -; Formula: -; p cnf 4 9 -; 1 2 -3 0 -; -1 -2 3 0 -; 2 3 -4 0 -; -2 -3 4 0 -; -1 -3 -4 0 -; 1 3 4 0 -; -1 2 4 0 -; 1 -2 -4 0 -; -1 0 -; Candidate RAT: 2 -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (check_rat - (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (cnfc (clc (neg v1) cln) - cnfn))))))))) - (clc (pos v2) cln) - tt)))))) - -; RAT Test 4 -; Formula: -; p cnf 4 2 -; 2 -3 0 -; 1 -4 0 -; Candidate RAT: 3 -; Answer: false -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (check_rat - (cnfc (clc (pos v2) (clc (neg v3) cln)) - (cnfc (clc (pos v1) (clc (neg v4) cln)) cnfn)) - (clc (pos v3) cln) - ff)))))) - - -; DRAT Test 1 (from Example 1 @ https://www.cs.utexas.edu/~marijn/drat-trim/) -; without deletions -; Formula: -; p cnf 4 8 -; 1 2 -3 0 -; -1 -2 3 0 -; 2 3 -4 0 -; -2 -3 4 0 -; -1 -3 -4 0 -; 1 3 4 0 -; -1 2 4 0 -; 1 -2 -4 -; Proof: -; -1 0 -; 2 0 -; 0 -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (: - (holds cln) - (drat_proof_of_bottom _ - (trust_cnf (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - cnfn))))))))) - (DRATProofa (clc (neg v1) cln) - (DRATProofa (clc (pos v2) cln) - (DRATProofa cln - DRATProofn)))))))))) - - -; DRAT Test 2 (from Example 1 @ https://www.cs.utexas.edu/~marijn/drat-trim/) -; with deletions -; Formula: -; p cnf 4 8 -; 1 2 -3 0 -; -1 -2 3 0 -; 2 3 -4 0 -; -2 -3 4 0 -; -1 -3 -4 0 -; 1 3 4 0 -; -1 2 4 0 -; 1 -2 -4 -; Proof: -; -1 0 -; d -1 -2 3 0 -; d -1 -3 -4 0 -; d -1 2 4 0 -; 2 0 -; d 1 2 -3 0 -; d 2 3 -4 0 -; 0 -(check - (% v1 var (% v2 var (% v3 var (% v4 var - (: (holds cln) - (drat_proof_of_bottom _ - (trust_cnf - (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - cnfn))))))))) - (DRATProofa (clc (neg v1) cln) - (DRATProofd (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (DRATProofd (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (DRATProofd (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (DRATProofa (clc (pos v2) cln) - (DRATProofd (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (DRATProofd (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (DRATProofa cln - DRATProofn))))))))))))))) - -; ===================================== ; -; Test Suite from "Two Flavors of DRAT" ; -; ===================================== ; - -; The paper includes a number of proofs which explore specified and operational -; DRAT validity. - -; Our test predicate for asserting the specified and operational validity of -; DRAT proofs -(declare spec_oper_test - (! f cnf - (! proof DRATProof - (! spec_validity bool - (! oper_validity bool - (! sc (^ (bool_and - (bool_eq (is_specified_drat_proof f proof) spec_validity) - (bool_eq (is_operational_drat_proof f proof) oper_validity) - ) tt) - TestSuccess)))))) - - -(declare x var) -(declare y var) -(declare z var) -(declare w var) -(define ex_1_formula - (cnfc (clc (pos x) (clc (pos y) (clc (pos z) cln))) - (cnfc (clc (neg x) (clc (pos y) (clc (pos z) cln))) - (cnfc (clc (pos x) (clc (neg y) (clc (pos z) cln))) - (cnfc (clc (neg x) (clc (neg y) (clc (pos z) cln))) - (cnfc (clc (pos x) (clc (pos y) (clc (neg z) cln))) - (cnfc (clc (neg x) (clc (pos y) (clc (neg z) cln))) - (cnfc (clc (pos x) (clc (neg y) (clc (neg z) cln))) - (cnfc (clc (neg x) (clc (neg y) (clc (neg z) cln))) - cnfn))))))))) - -; Spec-valid, operationally-invalid -(define ex_1_pf_pi - (DRATProofa (clc (pos x) (clc (pos y) cln)) - (DRATProofa (clc (pos x) cln) - (DRATProofa (clc (pos w) (clc (neg x) cln)) - (DRATProofd (clc (pos w) (clc (neg x) cln)) - (DRATProofa (clc (neg w) (clc (neg x) cln)) - (DRATProofa (clc (pos w) (clc (pos x) cln)) - (DRATProofa (clc (pos y) (clc (pos w) cln)) - (DRATProofa cln - DRATProofn))))))))) - -(check - (: TestSuccess - (spec_oper_test ex_1_formula ex_1_pf_pi tt ff))) - -; Spec-invalid, operationally valid -(define ex_1_pf_sigma - (DRATProofa (clc (pos x) (clc (pos y) cln)) - (DRATProofa (clc (pos x) cln) - (DRATProofd (clc (pos x) cln) - (DRATProofa (clc (pos w) (clc (neg y) cln)) - (DRATProofa (clc (neg w) (clc (neg y) cln)) - (DRATProofa (clc (pos w) cln) - (DRATProofa cln - DRATProofn)))))))) - -(check - (: TestSuccess - (spec_oper_test ex_1_formula ex_1_pf_sigma ff tt))) - -(declare x1 var) -(declare x2 var) -(declare x3 var) -(declare x4 var) -(declare x5 var) -(declare x6 var) -(declare x7 var) -(declare x8 var) -(declare x9 var) -(declare x10 var) - -(define ex_2_formula - (cnfc (clc (pos x1) cln) - (cnfc (clc (neg x1) (clc (pos x2) cln)) - (cnfc (clc (neg x1) (clc (neg x2) (clc (pos x3) cln))) - (cnfc (clc (neg x1) (clc (neg x3) (clc (pos x4) cln))) - (cnfc (clc (pos x5) (clc (pos x6) cln)) - (cnfc (clc (neg x2) (clc (neg x5) (clc (pos x7) cln))) - (cnfc (clc (neg x1) (clc (neg x5) (clc (pos x6) cln))) - (cnfc (clc (neg x5) (clc (neg x6) (clc (pos x4) cln))) - (cnfc (clc (neg x3) (clc (neg x6) (clc (pos x8) cln))) - (cnfc (clc (neg x6) (clc (neg x4) (clc (pos x3) cln))) - (cnfc (clc (neg x8) (clc (pos x5) cln)) - (cnfc (clc (neg x3) (clc (pos x9) (clc (pos x10) cln))) - (cnfc (clc (neg x4) (clc (neg x9) (clc (pos x10) cln))) - (cnfc (clc (neg x10) (clc (pos x9) cln)) - (cnfc (clc (neg x9) (clc (pos x7) cln)) - (cnfc (clc (neg x7) (clc (neg x8) (clc (neg x9) (clc (neg x10) cln)))) - cnfn))))))))))))))))) - -; Spec-valid, operationally-valid -(define ex_2_pf_tau - (DRATProofa (clc (pos x5) cln) - (DRATProofa (clc (pos x4) cln) - (DRATProofa (clc (pos x9) cln) - (DRATProofa cln - DRATProofn))))) - -(check - (: TestSuccess - (spec_oper_test ex_2_formula ex_2_pf_tau tt tt))) - -; Spec-valid, operationally unspecified in the paper, but its operationally valid. -(define ex_3_pf_tau_prime - (DRATProofa (clc (pos x5) cln) - (DRATProofd (clc (neg x1) (clc (pos x2) cln)) - (DRATProofa (clc (pos x9) cln) - (DRATProofa cln - DRATProofn))))) - -(check - (: TestSuccess - (spec_oper_test ex_2_formula ex_3_pf_tau_prime tt tt))) - -; Spec-invalid, operationally-invalid -(define ex_4_pf_pi_prime - (DRATProofa (clc (pos x) (clc (pos y) cln)) - (DRATProofa (clc (pos x) cln) - (DRATProofa (clc (pos w) (clc (neg x) cln)) - (DRATProofa (clc (neg w) (clc (neg x) cln)) - (DRATProofa (clc (pos w) (clc (pos x) cln)) - (DRATProofa (clc (pos y) (clc (pos w) cln)) - (DRATProofa cln - DRATProofn)))))))) - -(check - (: TestSuccess - (spec_oper_test ex_1_formula ex_4_pf_pi_prime ff ff))) - - -; Spec-valid, operationally valid -(define ex_5_pf_sigma_prime - (DRATProofa (clc (pos x) (clc (pos y) cln)) - (DRATProofa (clc (pos x) cln) - (DRATProofa (clc (pos w) (clc (neg y) cln)) - (DRATProofa (clc (neg w) (clc (neg y) cln)) - (DRATProofa (clc (pos w) cln) - (DRATProofa cln - DRATProofn))))))) - -(check - (: TestSuccess - (spec_oper_test ex_1_formula ex_5_pf_sigma_prime tt tt))) - diff --git a/proofs/signatures/er.plf b/proofs/signatures/er.plf index 9fcc9d4e8..6a8a059a2 100644 --- a/proofs/signatures/er.plf +++ b/proofs/signatures/er.plf @@ -1,4 +1,4 @@ -; Depends on sat.plf +; Deps: sat.plf ; This file exists to support the **definition introduction** (or **extension**) ; rule in the paper: diff --git a/proofs/signatures/er_test.plf b/proofs/signatures/er_test.plf deleted file mode 100644 index 1b5117a70..000000000 --- a/proofs/signatures/er_test.plf +++ /dev/null @@ -1,89 +0,0 @@ -; Depends on er.plf - -; This is a circuitous proof that uses the definition introduction and -; unrolling rules -(check - (% v1 var - (% v2 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) cln))) - (% pf_c2 (holds (clc (neg v1) (clc (pos v2) cln))) - (% pf_c3 (holds (clc (pos v1) (clc (neg v2) cln))) - (% pf_c4 (holds (clc (neg v1) (clc (neg v2) cln))) - (: (holds cln) - (decl_definition - (neg v1) - (clc (neg v2) cln) - (\ v3 - (\ def3 - (clausify_definition _ _ _ def3 _ - (\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln))) - (\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln))) - (\ pf_cnf ; type: (common_tail_cnf (clc (neg v2) cln) (clc (neg v3) (clc (neg v1) cln))) - (@ pf_c7 (common_tail_cnf_prove_head _ _ _ pf_cnf) - ; Clauses - (satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1) (\ pf_c8 ; v2 - (satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2) (\ pf_c9 ; v3 - (satlem_simplify _ _ _ (R _ _ pf_c9 pf_c7 v3) (\ pf_c10 ; ~v2 ~v1 - (satlem_simplify _ _ _ (Q _ _ pf_c10 pf_c8 v2) (\ pf_c11 ; ~v1 - (satlem_simplify _ _ _ (Q _ _ pf_c11 pf_c3 v1) (\ pf_c12 ; ~v2 - (satlem_simplify _ _ _ (Q _ _ pf_c12 pf_c8 v2) (\ pf_c13 ; empty - pf_c13 - )) - )) - )) - )) - )) - )) - ) - ))) - ) - )) - ) - ) - )))) - )) -) - -; This is a test of ER proof produced by drat2er on Example 1 from: -; https://www.cs.utexas.edu/~marijn/drat-trim/ -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) - (: (holds cln) - (decl_definition - (neg v1) - cln - (\ v5 - (\ def1 - (clausify_definition _ _ _ def1 _ - (\ pf_c9 ; type: (holds (clc (pos def1v) cln)) - (\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln))) - (\ idc0 ; type: (common_tail_cnf cln _) - (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11 - (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12 - (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13 - (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c2 pf_c5 v3) pf_c8 v1) (\ pf_c14 - (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c2 v2) pf_c6 v1) (\ pf_c15 - (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c5 v4) pf_c1 v1) (\ pf_c16 - (satlem_simplify _ _ _ (R _ _ (Q _ _ pf_c3 pf_c15 v4) pf_c16 v3) (\ pf_c17 - (satlem_simplify _ _ _ (Q _ _ (R _ _ (Q _ _ pf_c4 pf_c15 v3) pf_c14 v4) pf_c17 v2) (\ pf_c18 - pf_c18 - )))))))))))))))) - ))) - ) - )) - ) - ) - )))))))) - )))) -) diff --git a/proofs/signatures/ex-mem.plf b/proofs/signatures/ex-mem.plf deleted file mode 100644 index 7e143c5b6..000000000 --- a/proofs/signatures/ex-mem.plf +++ /dev/null @@ -1,62 +0,0 @@ -(check -(% s sort -(% a (term s) -(% b (term s) -(% c (term s) -(% f (term (arrow s s)) - -; -------------------- declaration of input formula ----------------------------------- - -(% A1 (th_holds (= s a b)) -(% A2 (th_holds (= s b c)) -(% A3 (th_holds (not (= s a c))) - -; ------------------- specify that the following is a proof of the empty clause ----------------- - -(: (holds cln) - -; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------ - -(decl_atom (= s a b) (\ v1 (\ a1 -(decl_atom (= s b c) (\ v2 (\ a2 -(decl_atom (= s a c) (\ v3 (\ a3 - -; --------------------------- proof of theory lemma --------------------------------------------- - -(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3 (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT1 - -; -------------------- clausification of input formulas ----------------------------------------- - -(satlem _ _ -(asf _ _ _ a1 (\ l1 -(clausify_false - (contra _ A1 l1) -))) (\ C1 -; C1 is the clause ( v1 ) - -(satlem _ _ -(asf _ _ _ a2 (\ l2 -(clausify_false - (contra _ A2 l2) -))) (\ C2 -; C2 is the clause ( v2 ) - -(satlem _ _ -(ast _ _ _ a3 (\ l3 -(clausify_false - (contra _ l3 A3) -))) (\ C3 -; C3 is the clause ( ~v3 ) - - -; -------------------- resolution proof ------------------------------------------------------------ - -(satlem_simplify _ _ _ - -(R _ _ -(R _ _ C2 -(R _ _ C1 CT1 v1) v2) C3 v3) - -(\ x x)) - -))))))))))))))))))))))))))) diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf deleted file mode 100644 index 332d7765c..000000000 --- a/proofs/signatures/ex_bv.plf +++ /dev/null @@ -1,58 +0,0 @@ -; (a = b) ^ (a = b & 00000) ^ (b = 11111) is UNSAT - -(check -(% a var_bv -(% b var_bv -(% f1 (th_holds (= (BitVec 4) (a_var_bv _ a) (a_var_bv _ b))) -(% f2 (th_holds (= (BitVec 4) (a_var_bv _ a) (bvand 4 (a_var_bv 4 b) (a_bv _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))) -(% f3 (th_holds (= (BitVec 4) (a_var_bv _ b) (a_bv _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn)))))))) -(: (holds cln) - -;; (decl_bv_term_var 5 a (\ ba1 -;; (decl_bv_term_var 5 b (\ ba2 -;; (decl_bv_term_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3 -;; (decl_bv_term_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4 - -(decl_atom (bitof a 4) (\ v1 (\ a1 -(decl_atom (bitof b 4) (\ v2 (\ a2 - -; bitblasting terms -(decl_bblast _ _ _ (bv_bbl_var 4 a _ ) (\ bt1 -(decl_bblast _ _ _ (bv_bbl_var 4 b _ ) (\ bt2 -(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bt3 -(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bt4 -(decl_bblast _ _ _ (bv_bbl_bvand 4 _ _ _ _ _ bt1 bt3) (\ bt5 - -; bitblasting formulas -(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt1 bt2) (\ bf1 -(th_let_pf _ (bv_bbl_bvult _ _ _ _ _ _ bt1 bt5) (\ bf2 -(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt2 bt4) (\ bf3 - -; CNFication -; a.4 V ~b.4 -(satlem _ _ -(asf _ _ _ a1 (\ l1 -(ast _ _ _ a2 (\ l2 -(clausify_false - trust -))))) (\ C2 - -; ~a.4 -(satlem _ _ -(ast _ _ _ a1 (\ l1 -(clausify_false - trust -))) (\ C3 - -; b.4 -(satlem _ _ -(asf _ _ _ a2 (\ l2 -(clausify_false - trust -))) (\ C6 - - -(satlem_simplify _ _ _ -(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x)) - -))))))))))))))))))))))))))))))))))))))))))))) diff --git a/proofs/signatures/example-arrays.plf b/proofs/signatures/example-arrays.plf deleted file mode 100644 index 03dc0831c..000000000 --- a/proofs/signatures/example-arrays.plf +++ /dev/null @@ -1,139 +0,0 @@ -; to check, run : lfscc sat.plf smt.plf th_base.plf th_arrays.plf example-arrays.plf - -; -------------------------------------------------------------------------------- -; literals : -; L1 : a = write( a, i, read( a, i ) -; L2 : read( a, k ) = read( write( a, i, read( a, i ) ), k ) -; L3 : i = k - -; input : -; ~L1 - -; (extenstionality) lemma : -; L1 or ~L2 - -; theory conflicts : -; L2 or ~L3 -; L2 or L3 - - -; With the theory lemma, the input is unsatisfiable. -; -------------------------------------------------------------------------------- - - -; (0) -------------------- term declarations ----------------------------------- - -(check -(% I sort -(% E sort -(% a (term (Array I E)) -(% i (term I) - - -; (1) -------------------- input formula ----------------------------------- - -(% A1 (th_holds (not (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))) - - - - -; (2) ------------------- specify that the following is a proof of the empty clause ----------------- - -(: (holds cln) - - - - -; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF ----------------- -; --- these should introduce (th_holds ...) - - -; extensionality lemma : notice this also introduces skolem k -(ext _ _ a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)) (\ k (\ A2 - - - - -; (4) -------------------- map theory literals to boolean variables -; --- maps all theory literals involved in proof to boolean literals - -(decl_atom (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1 -(decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2 -(decl_atom (= I i k) (\ v3 (\ a3 - - - -; (5) -------------------- theory conflicts --------------------------------------------- -; --- these should introduce (holds ...) - -(satlem _ _ -(asf _ _ _ a3 (\ l3 -(asf _ _ _ a2 (\ l2 -(clausify_false - - ; use read over write rule "row" - (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2) - -))))) (\ CT1 -; CT1 is the clause ( v2 V v3 ) - -(satlem _ _ -(ast _ _ _ a3 (\ l3 -(asf _ _ _ a2 (\ l2 -(clausify_false - - ; use read over write rule "row1" - (contra _ (symm _ _ _ - (trans _ _ _ _ - (symm _ _ _ (cong _ _ _ _ _ _ - (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))) - l3)) - (trans _ _ _ _ - (row1 _ _ a i (apply _ _ (apply _ _ (read I E) a) i)) - (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3) - ))) - l2) - -))))) (\ CT2 -; CT2 is the clause ( v2 V ~v3 ) - - -; (6) -------------------- clausification ----------------------------------------- -; --- these should introduce (holds ...) - -(satlem _ _ -(ast _ _ _ a1 (\ l1 -(clausify_false - -; input formula A1 is ( ~a1 ) -; the following is a proof of a1 ^ ( ~a1 ) => false - - (contra _ l1 A1) - -))) (\ C1 -; C1 is the clause ( ~v1 ) - - -(satlem _ _ -(asf _ _ _ a1 (\ l1 -(ast _ _ _ a2 (\ l2 -(clausify_false - -; lemma A2 is ( a1 V ~a2 ) -; the following is a proof of ~a1 ^ a2 ^ ( a1 V ~a2 ) => false - - (contra _ l2 (or_elim_1 _ _ l1 A2)) - -))))) (\ C2 -; C2 is the clause ( v1 V ~v2 ) - - -; (7) -------------------- resolution proof ------------------------------------------------------------ - -(satlem_simplify _ _ _ - -(R _ _ (R _ _ CT1 CT2 v3) (R _ _ C2 C1 v1) v2) - -(\ x x)) - -))))))))))))))))))))))))))) diff --git a/proofs/signatures/example-quant.plf b/proofs/signatures/example-quant.plf deleted file mode 100644 index 086633be9..000000000 --- a/proofs/signatures/example-quant.plf +++ /dev/null @@ -1,95 +0,0 @@ -; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf - -; -------------------------------------------------------------------------------- -; literals : -; L1 : forall x. x != x -; L2 : t = t - -; input : -; L1 - -; (instantiation) lemma : -; L1 => L2 - -; theory conflicts : -; ~L2 - - -; With the theory lemma, the input is unsatisfiable. -; -------------------------------------------------------------------------------- - - -; (0) -------------------- term declarations ----------------------------------- - -(check -(% s sort -(% t (term s) - - -; (1) -------------------- input formula ----------------------------------- - -(% x (term s) -(% A1 (th_holds (forall _ x (not (= _ x x)))) - - - -; (2) ------------------- specify that the following is a proof of the empty clause ----------------- - -(: (holds cln) - - - -; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF ----------------- -; --- these should introduce (th_holds ...) - - -; instantiation lemma -(inst _ _ _ t (not (= _ t t)) A1 (\ A2 - - - - -; (4) -------------------- map theory literals to boolean variables -; --- maps all theory literals involved in proof to boolean literals - -(decl_atom (forall _ x (not (= _ x x))) (\ v1 (\ a1 -(decl_atom (= _ t t) (\ v2 (\ a2 - - - - -; (5) -------------------- theory conflicts --------------------------------------------- -; --- these should introduce (holds ...) - -(satlem _ _ -(asf _ _ _ a2 (\ l2 -(clausify_false - - (contra _ (refl _ t) l2) - -))) (\ CT1 -; CT1 is the clause ( v2 ) - - -; (6) -------------------- clausification ----------------------------------------- -; --- these should introduce (holds ...) - -(satlem _ _ -(ast _ _ _ a2 (\ l2 -(clausify_false - - (contra _ l2 A2) - -))) (\ C1 -; C1 is the clause ( ~v2 ) - - -; (7) -------------------- resolution proof ------------------------------------------------------------ - -(satlem_simplify _ _ _ - -(R _ _ CT1 C1 v2) - -(\ x x)) - -)))))))))))))))))) diff --git a/proofs/signatures/example.plf b/proofs/signatures/example.plf deleted file mode 100644 index ab690eb51..000000000 --- a/proofs/signatures/example.plf +++ /dev/null @@ -1,116 +0,0 @@ -; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf - -; -------------------------------------------------------------------------------- -; input : -; ( a = b ) -; ( b = f(c) ) -; ( a != f(c) V a != b ) - -; theory lemma (by transitivity) : -; ( a != b V b != f(c) V a = f(c) ) - - -; With the theory lemma, the input is unsatisfiable. -; -------------------------------------------------------------------------------- - - - -(check -(% s sort -(% a (term s) -(% b (term s) -(% c (term s) -(% f (term (arrow s s)) - -; -------------------- declaration of input formula ----------------------------------- - -(% A1 (th_holds (= s a b)) -(% A2 (th_holds (= s b (apply _ _ f c))) -(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b)))) - - -; ------------------- specify that the following is a proof of the empty clause ----------------- - -(: (holds cln) - -; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------ - -(decl_atom (= s a b) (\ v1 (\ a1 -(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2 -(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3 - - -; --------------------------- proof of theory lemma --------------------------------------------- - -(satlem _ _ -(ast _ _ _ a1 (\ l1 -(ast _ _ _ a2 (\ l2 -(asf _ _ _ a3 (\ l3 -(clausify_false - -; this should be a proof of l1 ^ l2 ^ ~l3 => false -; this is done by theory proof rules (currently just use "trust") - - trust - -))))))) (\ CT -; CT is the clause ( ~v1 V ~v2 V v3 ) - -; -------------------- clausification of input formulas ----------------------------------------- - -(satlem _ _ -(asf _ _ _ a1 (\ l1 -(clausify_false - -; input formula A1 is ( ~l1 ) -; the following should be a proof of l1 ^ ( ~l1 ) => false -; this is done by natural deduction rules - - (contra _ A1 l1) - -))) (\ C1 -; C1 is the clause ( v1 ) - - -(satlem _ _ -(asf _ _ _ a2 (\ l2 -(clausify_false - -; input formula A2 is ( ~l2 ) -; the following should be a proof of l2 ^ ( ~l2 ) => false -; this is done by natural deduction rules - - (contra _ A2 l2) - -))) (\ C2 -; C2 is the clause ( v2 ) - - -(satlem _ _ -(ast _ _ _ a3 (\ l3 -(ast _ _ _ a1 (\ l1 -(clausify_false - -; input formula A3 is ( ~a3 V ~a1 ) -; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false -; this is done by natural deduction rules - - (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3)) - -))))) (\ C3 -; C3 is the clause ( ~v3 V ~v1 ) - - - -; -------------------- resolution proof ------------------------------------------------------------ - -(satlem_simplify _ _ _ - -(R _ _ C1 -(R _ _ C2 -(R _ _ CT C3 v3) v2) v1) - -(\ x x)) - -)))))))))))))))))))))))))) -) diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf index d16791624..b5d46be43 100644 --- a/proofs/signatures/lrat.plf +++ b/proofs/signatures/lrat.plf @@ -2,7 +2,7 @@ ; LRAT format detailed in "Efficient Certified RAT Verification" ; Link: https://www.cs.utexas.edu/~marijn/publications/lrat.pdf ; Author: aozdemir -; Depends On: sat.plf, smt.plf +; Deps: sat.plf smt.plf ; A general note about the design of the side conditions: diff --git a/proofs/signatures/lrat_test.plf b/proofs/signatures/lrat_test.plf deleted file mode 100644 index 0663a08f7..000000000 --- a/proofs/signatures/lrat_test.plf +++ /dev/null @@ -1,891 +0,0 @@ -(declare test_clause_append - (! c1 clause - (! c2 clause - (! cr clause - (! sc (^ (clause_append c1 c2) cr) type))))) - -; Test passes if the (test_clause_append ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (test_clause_append - (clc (pos v1) (clc (neg v2) cln)) - (clc (pos v3) (clc (neg v2) cln)) - (clc (pos v1) (clc (neg v2) (clc (pos v3) (clc (neg v2) cln)))) - ) - ))) -) - -; Test passes if the (test_clause_append ...) application is well-typed. -(check - (% v2 var - (% v3 var - (test_clause_append - cln - (clc (pos v3) (clc (neg v2) cln)) - (clc (pos v3) (clc (neg v2) cln)) - ) - )) -) - -; Test passes if the (test_clause_append ...) application is well-typed. -(check - (% v2 var - (% v3 var - (test_clause_append - (clc (pos v3) (clc (neg v2) cln)) - cln - (clc (pos v3) (clc (neg v2) cln)) - ) - )) -) - -(declare test_CMap_remove_many - (! is CIList - (! cs CMap - (! csr CMap - (! sc (^ (CMap_remove_many is cs) csr) type))))) - -; Test passes if the (test_CMap_remove_many ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v4) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v3) cln)) - (@ c4 (clc (neg v3) (clc (neg v4) cln)) - (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) - (@ cs_out (CMapc 3 c2 (CMapc 5 c3 CMapn)) - (@ is_in (CIListc 0 (CIListc 4 (CIListc 6 CIListn))) - (test_CMap_remove_many - is_in - cs_in - cs_out - ) - ))) - )))) - )))) -) - -; Test passes if the (test_CMap_remove_many ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v4) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v3) cln)) - (@ c4 (clc (neg v3) (clc (neg v4) cln)) - (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) - (@ cs_out (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) - (@ is_in (CIListc 4 CIListn) - (test_CMap_remove_many - is_in - cs_in - cs_out - ) - ))) - )))) - )))) -) - -(declare test_clause_remove_all - (! l lit - (! c clause - (! c' clause - (! sc (^ (clause_remove_all l c) c') type))))) - -; Test passes if the (test_clause_remove_all ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v4) (clc (neg v2) (clc (neg v2) (clc (pos v2) (clc (pos v1) cln))))) - (@ c2 (clc (pos v4) (clc (pos v2) (clc (pos v1) cln))) - (test_clause_remove_all - (neg v2) - c1 - c2 - ) - )) - )))) -) - -(declare test_collect_resolution_targets - (! cs CMap - (! c clause - (! is CIList - (! sc (^ (collect_resolution_targets cs c) is) type))))) - -; Test passes if the (test_collect_resolution_targets ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v3) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v3) cln)) - (@ c4 (clc (neg v3) (clc (pos v3) cln)) - (@ ct (clc (neg v3) (clc (neg v4) cln)) - (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) - (@ is_out (CIListc 0 (CIListc 4 (CIListc 5 (CIListc 6 CIListn)))) - (test_collect_resolution_targets - cs_in - ct - is_out - ) - ))) - )))) - )))) -) - -(declare test_resolution_targets_match - (! c CIList - (! g RATHints - (! ans bool - (! sc (^ (resolution_targets_match c g) ans) type))))) - -; Test passes if the (test_resolution_targets_match ...) application is well-typed. -(check - (@ idxs_in (CIListc 0 (CIListc 4 (CIListc 5 (CIListc 6 CIListn)))) - (@ hints_in - (RATHintsc 0 Tracen - (RATHintsc 4 Tracen - (RATHintsc 5 Tracen - (RATHintsc 6 Tracen - RATHintsn)))) - (test_resolution_targets_match - idxs_in - hints_in - tt - ) - )) -) - -; Test passes if the (test_resolution_targets_match ...) application is well-typed. -(check - (@ idxs_in (CIListc 0 (CIListc 2 (CIListc 5 (CIListc 6 CIListn)))) - (@ hints_in - (RATHintsc 0 Tracen - (RATHintsc 4 Tracen - (RATHintsc 5 Tracen - (RATHintsc 6 Tracen - RATHintsn)))) - (test_resolution_targets_match - idxs_in - hints_in - ff - ) - )) -) - -(declare test_is_at_trace - (! cs CMap - (! c clause - (! t Trace - (! r UPResult - (! sc (^ (is_at_trace cs c t) r) type)))))) - -; Test passes if the (test_is_at_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v3) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v1) cln)) - (@ c4 (clc (neg v3) (clc (pos v2) cln)) - (@ cs (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) - (@ c (clc (neg v3) cln) - (@ t (Tracec 3 (Tracec 5 (Tracec 6 Tracen))) - (test_is_at_trace - cs - c - t - UPR_Bottom - ) - ))) - )))) - )))) -) - -; Test passes if the (test_is_at_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v3) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v1) cln)) - (@ c4 (clc (neg v3) (clc (pos v2) cln)) - (@ cs (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) - (@ c (clc (neg v3) cln) - (@ t (Tracec 3 (Tracec 5 Tracen)) - (test_is_at_trace - cs - c - t - UPR_Ok - ) - ))) - )))) - )))) -) - -; Test passes if the (test_is_at_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v3) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v1) cln)) - (@ c4 (clc (neg v3) (clc (pos v2) cln)) - (@ cs (CMapc 1 c1 (CMapc 2 c2 (CMapc 3 c3 (CMapc 4 c4 CMapn)))) - (@ c (clc (neg v3) cln) - (@ t (Tracec 2 (Tracec 1 Tracen)) - (test_is_at_trace - cs - c - t - UPR_Broken - ) - ))) - )))) - )))) -) - -(declare test_is_rat_trace (! cs CMap - (! c clause - (! t Trace - (! h RATHints - (! r UPResult - (! sc (^ (is_rat_trace cs c t h) r) type))))))) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 CMapn)))))))) - (@ c (clc (pos v1) cln) - (@ t Tracen - (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) - RATHintsn))) - (test_is_rat_trace - cs - c - t - h - UPR_Bottom - ) - )))) - )))))))) - )))) -) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 CMapn)))))))) - (@ c (clc (pos v1) cln) - (@ t Tracen - (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - RATHintsn)) - (test_is_rat_trace - cs - c - t - h - UPR_Broken - ) - )))) - )))))))) - )))) -) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 CMapn)))))))) - (@ c (clc (pos v1) cln) - (@ t Tracen - (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 3 (Tracec 1 Tracen)) - RATHintsn))) - (test_is_rat_trace - cs - c - t - h - UPR_Broken - ) - )))) - )))))))) - )))) -) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 CMapn)))))))) - (@ c (clc (pos v1) cln) - (@ t Tracen - (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 3 Tracen) - RATHintsn))) - (test_is_rat_trace - cs - c - t - h - UPR_Broken - ) - )))) - )))))))) - )))) -) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ c9 (clc (pos v1) cln) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 - (CMapc 9 c9 - CMapn))))))))) - (@ c (clc (pos v2) cln) - (@ t (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - (@ h RATHintsn - (test_is_rat_trace - cs - c - t - h - UPR_Bottom - ) - )))) - ))))))))) - )))) -) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ c9 (clc (pos v1) cln) - (@ c10 (clc (pos v2) cln) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 - (CMapc 9 c9 - (CMapc 10 c10 - CMapn)))))))))) - (@ c cln - (@ t (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - (@ h RATHintsn - (test_is_rat_trace - cs - c - t - h - UPR_Bottom - ) - )))) - )))))))))) - )))) -) - -(declare test_is_lrat_proof_of_bottom - (! f CMap - (! p LRATProof - (! r bool - (! sc (^ (is_lrat_proof_of_bottom f p) r) type))))) - -; Test passes if the (test_is_lrat_proof_of_bottom ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 - CMapn)))))))) - (@ p - (LRATProofa 9 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) - (LRATProofa 10 - (clc (pos v2) cln) - (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 11 - cln - (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn))))) - (test_is_lrat_proof_of_bottom - cs - p - tt - ) - )) - )))))))) - )))) -) - -; Test passes if the (test_is_lrat_proof_of_bottom ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 - CMapn)))))))) - (@ p - (LRATProofa 9 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) - (LRATProofa 10 - (clc (pos v2) cln) - (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 11 - cln - (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 Tracen)))) - RATHintsn - LRATProofn))))) - (test_is_lrat_proof_of_bottom - cs - p - ff - ) - )) - )))))))) - )))) -) - -; Proof from Figure 2 of "Efficient Certified RAT Verification" -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) - (@ pf_cmap - (CMapc_proof 1 _ _ _ pf_c1 - (CMapc_proof 2 _ _ _ pf_c2 - (CMapc_proof 3 _ _ _ pf_c3 - (CMapc_proof 4 _ _ _ pf_c4 - (CMapc_proof 5 _ _ _ pf_c5 - (CMapc_proof 6 _ _ _ pf_c6 - (CMapc_proof 7 _ _ _ pf_c7 - (CMapc_proof 8 _ _ _ pf_c8 - CMapn_proof)))))))) - (@ lrat_proof_witness - (LRATProofa 9 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) - (LRATProofa 10 - (clc (pos v2) cln) - (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 11 - cln - (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn))))) - (: - (holds cln) - (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) - )) - )))))))) - )))) -) - -; Proof from Figure 2 of "Efficient Certified RAT Verification" -; With duplicates -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (pos v3) (clc (pos v3) (clc (neg v4) cln)))))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) (clc (neg v4) cln))))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v3) (clc (pos v4) cln))))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v2) (clc (neg v4) cln))))) - (@ pf_cmap - (CMapc_proof 1 _ _ _ pf_c1 - (CMapc_proof 2 _ _ _ pf_c2 - (CMapc_proof 3 _ _ _ pf_c3 - (CMapc_proof 4 _ _ _ pf_c4 - (CMapc_proof 5 _ _ _ pf_c5 - (CMapc_proof 6 _ _ _ pf_c6 - (CMapc_proof 7 _ _ _ pf_c7 - (CMapc_proof 8 _ _ _ pf_c8 - CMapn_proof)))))))) - (@ lrat_proof_witness - (LRATProofa 9 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) - (LRATProofa 10 - (clc (pos v2) cln) - (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 11 - cln - (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn))))) - (: - (holds cln) - (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) - )) - )))))))) - )))) -) - -; Clauses 1 and 9 are identical. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) - (% pf_c9 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (@ pf_cmap - (CMapc_proof 1 _ _ _ pf_c1 - (CMapc_proof 2 _ _ _ pf_c2 - (CMapc_proof 3 _ _ _ pf_c3 - (CMapc_proof 4 _ _ _ pf_c4 - (CMapc_proof 5 _ _ _ pf_c5 - (CMapc_proof 6 _ _ _ pf_c6 - (CMapc_proof 7 _ _ _ pf_c7 - (CMapc_proof 8 _ _ _ pf_c8 - (CMapc_proof 9 _ _ _ pf_c9 - CMapn_proof))))))))) - (@ lrat_proof_witness - (LRATProofa 10 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 9 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 (CIListc 9 CIListn)))) - (LRATProofa 11 - (clc (pos v2) cln) - (Tracec 10 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 12 - cln - (Tracec 10 (Tracec 11 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn))))) - (: - (holds cln) - (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) - )) - ))))))))) - )))) -) - -; Clauses 1 and 9 are logically identical, but the literals have been reordered. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) - (% pf_c9 (holds (clc (neg v3) (clc (pos v2) (clc (pos v1) cln)))) - (@ pf_cmap - (CMapc_proof 1 _ _ _ pf_c1 - (CMapc_proof 2 _ _ _ pf_c2 - (CMapc_proof 3 _ _ _ pf_c3 - (CMapc_proof 4 _ _ _ pf_c4 - (CMapc_proof 5 _ _ _ pf_c5 - (CMapc_proof 6 _ _ _ pf_c6 - (CMapc_proof 7 _ _ _ pf_c7 - (CMapc_proof 8 _ _ _ pf_c8 - (CMapc_proof 9 _ _ _ pf_c9 - CMapn_proof))))))))) - (@ lrat_proof_witness - (LRATProofa 10 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 9 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 (CIListc 9 CIListn)))) - (LRATProofa 11 - (clc (pos v2) cln) - (Tracec 10 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 12 - cln - (Tracec 10 (Tracec 11 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn))))) - (: - (holds cln) - (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) - )) - ))))))))) - )))) -) - -; Proof from Figure 1 of "Efficient Certified RAT Verification" -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) - (@ pf_cmap - (CMapc_proof 1 _ _ _ pf_c1 - (CMapc_proof 2 _ _ _ pf_c2 - (CMapc_proof 3 _ _ _ pf_c3 - (CMapc_proof 4 _ _ _ pf_c4 - (CMapc_proof 5 _ _ _ pf_c5 - (CMapc_proof 6 _ _ _ pf_c6 - (CMapc_proof 7 _ _ _ pf_c7 - (CMapc_proof 8 _ _ _ pf_c8 - CMapn_proof)))))))) - (@ lrat_proof_witness - (LRATProofa 9 - (clc (pos v1) (clc (pos v2) cln)) - (Tracec 1 (Tracec 6 (Tracec 3 Tracen))) - RATHintsn - (LRATProofd (CIListc 1 CIListn) - (LRATProofa 10 - (clc (pos v1) (clc (pos v3) cln)) - (Tracec 9 (Tracec 8 (Tracec 6 Tracen))) - RATHintsn - (LRATProofd (CIListc 6 CIListn) - (LRATProofa 11 - (clc (pos v1) cln) - (Tracec 10 (Tracec 9 (Tracec 4 (Tracec 8 Tracen)))) - RATHintsn - (LRATProofd (CIListc 8 (CIListc 9 (CIListc 10 CIListn))) - (LRATProofa 12 - (clc (pos v2) cln) - (Tracec 11 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 13 - cln - (Tracec 11 (Tracec 12 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn - ))))))))) - (: - (holds cln) - (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) - )) - )))))))) - )))) -) diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 57dc5bd1e..9f6e71986 100644 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -3,7 +3,7 @@ ; SMT syntax and semantics (not theory-specific) ; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; depends on sat.plf +; Deps: sat.plf (declare formula type) (declare th_holds (! f formula type)) diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf index acfbd2f3b..5517d9a4f 100644 --- a/proofs/signatures/th_arrays.plf +++ b/proofs/signatures/th_arrays.plf @@ -3,7 +3,7 @@ ; Theory of Arrays ; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; depends on : th_base.plf +; Deps: th_base.plf ; sorts diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf index d6b283752..d5182007e 100644 --- a/proofs/signatures/th_base.plf +++ b/proofs/signatures/th_base.plf @@ -5,7 +5,7 @@ ; Theory of Equality and Congruence Closure ; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; depends on : smt.plf +; Deps: smt.plf ; sorts : diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf index 70cdfc733..af326bf27 100644 --- a/proofs/signatures/th_lira.plf +++ b/proofs/signatures/th_lira.plf @@ -1,4 +1,4 @@ -; Depends on th_real.plf, th_int.plf, smt.plf, sat.plf +; Deps: th_real.plf th_int.plf smt.plf sat.plf ; Some axiom arguments are marked "; Omit", because they can be deduced from ; other arguments and should be replaced with a "_" when invoking the axiom. diff --git a/proofs/signatures/th_lira_test.plf b/proofs/signatures/th_lira_test.plf deleted file mode 100644 index 91d626bba..000000000 --- a/proofs/signatures/th_lira_test.plf +++ /dev/null @@ -1,294 +0,0 @@ -; Depends On: th_lira.plf -;; Proof (from predicates on linear polynomials) that the following imply bottom -; -; -x - 1/2 y + 2 >= 0 -; x + y - 8 >= 0 -; x - y + 0 >= 0 -; -(check - ; Variables - (% x real_var - (% y real_var - ; linear combinations - (@ m1 (lc_cons (~ 1/1) (av_from_real x) (lc_cons (~ 1/2) (av_from_real y) lc_null)) - (@ m2 (lc_cons 1/1 (av_from_real x) (lc_cons 1/1 (av_from_real y) lc_null)) - (@ m3 (lc_cons 1/1 (av_from_real x) (lc_cons (~ 1/1) (av_from_real y) lc_null)) - ; affine functions - (@ p1 (aff_cons 2/1 m1) - (@ p2 (aff_cons (~ 8/1) m2) - (@ p3 (aff_cons 0/1 m3) - ; Proofs of affine bounds - (% pf_nonneg_1 (th_holds (bounded_aff p1 bound_non_neg)) - (% pf_nonneg_2 (th_holds (bounded_aff p2 bound_non_neg)) - (% pf_nonneg_3 (th_holds (bounded_aff p3 bound_non_neg)) - (: - (th_holds false) - (bounded_aff_contra _ _ - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 4/1 pf_nonneg_1) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 3/1 pf_nonneg_2) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 pf_nonneg_3) - bounded_aff_ax_0_>=_0))))) - ))))) - )))) - )) -) - -;; Proof (from predicates on real terms) that the following imply bottom -; -; -x - 1/2 y >= 2 -; x + y >= 8 -; x - y >= 0 -; -(check - ; Declarations - ; Variables - (% x real_var - (% y real_var - ; real predicates - (@ f1 (>=_Real (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (*_Real (a_real (~ 1/2)) (term_real_var y))) (a_real (~ 2/1))) - (@ f2 (>=_Real (+_Real (*_Real (a_real 1/1) (term_real_var x)) (*_Real (a_real 1/1) (term_real_var y))) (a_real 8/1)) - (@ f3 (>=_Real (+_Real (*_Real (a_real 1/1) (term_real_var x)) (*_Real (a_real (~ 1/1)) (term_real_var y))) (a_real 0/1)) - ; proof of real predicates - (% pf_f1 (th_holds f1) - (% pf_f2 (th_holds f2) - (% pf_f3 (th_holds f3) - - - ; Normalization - ; real term -> linear polynomial normalization witnesses - (@ n1 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) - (is_aff_mul_c_L _ _ _ (~ 1/2) (is_aff_var_real y))) - (is_aff_const (~ 2/1))) - pf_f1) - (@ n2 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real x)) - (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real y))) - (is_aff_const 8/1)) - pf_f2) - (@ n3 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real x)) - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real y))) - (is_aff_const 0/1)) - pf_f3) - - ; derivation of a contradiction using farkas coefficients - (: - (th_holds false) - (bounded_aff_contra _ _ - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 4/1 n1) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 3/1 n2) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n3) - bounded_aff_ax_0_>=_0))))) - ))) - ))) - ))) - )) -) - -;; Term proof, 2 premises of the form (>=), one of the form (not >=) -;; Proof (from predicates on real terms) that the following imply bottom -; -; -x + y >= 2 -; x + y >= 2 -; not[ y >= -2] => [y < -2] => [-y > 2] -; -(check - ; Declarations - ; Variables - (% x real_var - (% y real_var - ; real predicates - (@ f1 (>=_Real - (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (term_real_var y)) - (a_real 2/1)) - (@ f2 (>=_Real - (+_Real (term_real_var x) (term_real_var y)) - (a_real 2/1)) - (@ f3 (not (>=_Real (term_real_var y) (a_real (~ 2/1)))) - - ; Normalization - ; proof of real predicates - (% pf_f1 (th_holds f1) - (% pf_f2 (th_holds f2) - (% pf_f3 (th_holds f3) - ; real term -> linear polynomial normalization witnesses - (@ n1 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) - (is_aff_var_real y)) - (is_aff_const 2/1)) - pf_f1) - (@ n2 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_var_real x) - (is_aff_var_real y)) - (is_aff_const 2/1)) - pf_f2) - (@ n3 (aff_>_from_term _ _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_var_real y) - (is_aff_const (~ 2/1))) - pf_f3) - - ; derivation of a contradiction using farkas coefficients - (: - (th_holds false) - (bounded_aff_contra _ _ - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n1) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n2) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 2/1 n3) - bounded_aff_ax_0_>=_0))))) - ))) - ))) - ))) - )) -) - -;; Term proof, 2 premises of the form (>=), one of the form (not >=) -;; x is a real, -;; y is an integer -;; Proof (from predicates on real terms) that the following imply bottom -; -; -x + y >= 2 -; x + y >= 2 -; not[ y >= -2] => [y < -2] => [-y > 2] -; -(check - ; Declarations - ; Variables - (% x real_var - (% y int_var - ; real predicates - (@ f1 (>=_Real - (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (term_int_to_real (term_int_var y))) - (a_real 2/1)) - (@ f2 (>=_Real - (+_Real (term_real_var x) (term_int_to_real (term_int_var y))) - (a_real 2/1)) - (@ f3 (not (>=_IntReal (term_int_var y) (a_real (~ 2/1)))) - - ; Normalization - ; proof of real predicates - (% pf_f1 (th_holds f1) - (% pf_f2 (th_holds f2) - (% pf_f3 (th_holds f3) - ; real term -> linear polynomial normalization witnesses - (@ n1 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) - (is_aff_var_int y)) - (is_aff_const 2/1)) - (pf_reified_arith_pred _ _ pf_f1)) - (@ n2 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_var_real x) - (is_aff_var_int y)) - (is_aff_const 2/1)) - (pf_reified_arith_pred _ _ pf_f2)) - (@ n3 (aff_>_from_term _ _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_var_int y) - (is_aff_const (~ 2/1))) - (pf_reified_arith_pred _ _ pf_f3)) - - ; derivation of a contradiction using farkas coefficients - (: - (th_holds false) - (bounded_aff_contra _ _ - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n1) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n2) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 2/1 n3) - bounded_aff_ax_0_>=_0))))) - ))) - ))) - ))) - )) -) - -;; Term proof, 2 premises of the form (>=), one of the form (not >=) -;; x is a real, -;; y is an integer, and needs tightening -;; Proof (from predicates on real terms) that the following imply bottom -; -; -x >= -1/2 -; x + y >= 0 -; not[ y >= 0] => [y < 0] => [-y >= 1] -; -(check - ; Declarations - ; Variables - (% x real_var - (% y int_var - ; real predicates - (@ f1 (>=_Real - (*_Real (a_real (~ 1/1)) (term_real_var x)) - (a_real (~ 1/2))) - (@ f2 (>=_Real - (+_Real (term_real_var x) (term_int_to_real (term_int_var y))) - (a_real 0/1)) - (@ f3 (not (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (term_int_to_real (a_int 0)))) - - ; Normalization - ; proof of real predicates - (% pf_f1 (th_holds f1) - (% pf_f2 (th_holds f2) - (% pf_f3 (th_holds f3) - ; real term -> linear polynomial normalization witnesses - (@ n1 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) - (is_aff_const (~ 1/2))) - (pf_reified_arith_pred _ _ pf_f1)) - (@ n2 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_var_real x) - (is_aff_var_int y)) - (is_aff_const 0/1)) - (pf_reified_arith_pred _ _ pf_f2)) - (@ n3 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_int y)) - (is_aff_const 1/1)) - (pf_reified_arith_pred _ _ - (tighten_not_>=_IntInt _ _ _ _ (check_neg_of_greatest_integer_below_int 1 0) pf_f3))) - - ; derivation of a contradiction using farkas coefficients - (: - (th_holds false) - (bounded_aff_contra _ _ - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n1) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n2) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n3) - bounded_aff_ax_0_>=_0))))) - ))) - ))) - ))) - )) -) diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf index 112328b63..dfedb28ed 100644 --- a/proofs/signatures/th_real.plf +++ b/proofs/signatures/th_real.plf @@ -1,4 +1,4 @@ -; Depends On: th_smt.plf +; Deps: smt.plf (declare Real sort) (define arithpred_Real (! x (term Real) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index ad946e3ca..52a999c1b 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -31,3 +31,7 @@ if(ENABLE_UNIT_TESTING) add_subdirectory(java) endif() endif() + +if(LFSC_BINARY) + add_subdirectory(signatures) +endif() diff --git a/test/signatures/CMakeLists.txt b/test/signatures/CMakeLists.txt new file mode 100644 index 000000000..64da9fad2 --- /dev/null +++ b/test/signatures/CMakeLists.txt @@ -0,0 +1,33 @@ +set(lfsc_test_file_list + drat_test.plf + er_test.plf + example-arrays.plf + example.plf + example-quant.plf + ex_bv.plf + ex-mem.plf + lrat_test.plf + th_lira_test.plf +) + +set(test_script ${CMAKE_CURRENT_LIST_DIR}/run_test.py) + +macro(lfsc_test file) + set(test_name "signatures/${file}") + add_test( + NAME "${test_name}" + COMMAND + "${PYTHON_EXECUTABLE}" + "${test_script}" + "${LFSC_BINARY}" + "${CMAKE_CURRENT_LIST_DIR}/${file}" + "${CMAKE_SOURCE_DIR}/proofs/signatures" + WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR} + ) + + set_tests_properties("${test_name}" PROPERTIES LABELS "signatures") +endmacro() + +foreach(file ${lfsc_test_file_list}) + lfsc_test(${file}) +endforeach() diff --git a/test/signatures/README.md b/test/signatures/README.md new file mode 100644 index 000000000..4ac8cb131 --- /dev/null +++ b/test/signatures/README.md @@ -0,0 +1,32 @@ +# Signature Tests + +This directory contains tests of our LFSC proof signatures. To run just the +tests in this directory, the test label `signatures` can be used (`ctest -L +signatures`). + +## Adding a New Signature Test + +To add a new signature test file, add the file to git, for example: + +``` +git add test/signatures/new_signature_test.plf +``` + +Also add it to [CMakeLists.txt](CMakeLists.txt) in this directory and declare +the dependencies of the test as explained below. + +The signature tests are prefixed with `signatures/`, so the test for +`example.plf` will have the name `signatures/example.plf`. + +## Test Dependencies + +Tests can declare the signature files that they depend on using the `; Deps:` +directive followed by a space-separated list of files. For example: + +``` +; Deps: sat.plf smt.plf +``` + +indicates that the test depends on `sat.plf` and `smt.plf`. The run script +automatically searches for the listed files in `proofs/signatures` as well as +the directory of the test input. diff --git a/test/signatures/drat_test.plf b/test/signatures/drat_test.plf new file mode 100644 index 000000000..e5335a6bb --- /dev/null +++ b/test/signatures/drat_test.plf @@ -0,0 +1,434 @@ +; Deps: drat.plf +(declare TestSuccess type) + +; Test for clause_eq +(declare test_clause_eq + (! a clause + (! b clause + (! result bool + (! (^ + (bool_and + (bool_eq (clause_eq a b) result) + (bool_and + (bool_eq (clause_eq b a) result) + (bool_and + (bool_eq (clause_eq a a) tt) + (bool_eq (clause_eq b b) tt)))) + tt) + TestSuccess))))) + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (neg b) cln)) + (@ c2 (clc (pos a) (clc (neg b) cln)) + (: TestSuccess + (test_clause_eq c1 c2 tt))))))) + +(check + (% a var + (% b var + (@ c1 (clc (neg a) (clc (neg b) cln)) + (@ c2 (clc (pos a) (clc (neg b) cln)) + (: TestSuccess + (test_clause_eq c1 c2 ff))))))) + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (pos b) cln)) + (@ c2 (clc (pos a) (clc (neg b) cln)) + (: TestSuccess + (test_clause_eq c1 c2 ff))))))) + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (pos a) cln)) + (@ c2 (clc (pos a) (clc (neg b) cln)) + (: TestSuccess + (test_clause_eq c1 c2 ff))))))) + +(check + (% a var + (% b var + (@ c1 (clc (neg b) (clc (pos a) (clc (neg a) cln))) + (@ c1 (clc (neg a) (clc (neg b) (clc (pos a) cln))) + (: TestSuccess + (test_clause_eq c1 c2 ff))))))) + + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (pos a) (clc (neg b) cln))) + (@ c2 (clc (pos a) (clc (neg b) cln)) + (: TestSuccess + (test_clause_eq c1 c2 tt))))))) + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (pos a) (clc (neg b) cln))) + (@ c2 (clc (pos a) (clc (neg b) (clc (neg b) cln))) + (: TestSuccess + (test_clause_eq c1 c2 tt))))))) + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (pos a) (clc (neg a) cln))) + (@ c2 (clc (pos a) (clc (neg a) (clc (neg a) cln))) + (: TestSuccess + (test_clause_eq c1 c2 tt))))))) + +(check + (% a var + (% b var + (@ c1 cln + (@ c2 (clc (pos a) (clc (neg a) (clc (neg a) cln))) + (: TestSuccess + (test_clause_eq c1 c2 ff))))))) + +(declare check_rat + (! f cnf + (! c clause + (! b bool + (! sc (^ (is_rat f c) b) + bottom))))) + +(declare trust_cnf (! f cnf (cnf_holds f))) + +; RAT Test 1 +; Formula: (-p, -a) ^ (-p, b) ^( b, c) ^ (-c, a) +; Candidate RAT: (p, a) +; Answer: true +(check + (% va var + (% vb var + (% vc var + (% vp var + (check_rat + (cnfc (clc (neg vp) (clc (neg va) cln)) + (cnfc (clc (neg vp) (clc (pos vb) cln)) + (cnfc (clc (pos vb) (clc (pos vc) cln)) + (cnfc (clc (neg vc) (clc (pos va) cln)) cnfn)))) + (clc (pos vp) (clc (pos va) cln)) + tt)))))) + +; RAT Test 2 +; Formula: +; p cnf 4 8 +; 1 2 -3 0 +; -1 -2 3 0 +; 2 3 -4 0 +; -2 -3 4 0 +; -1 -3 -4 0 +; 1 3 4 0 +; -1 2 4 0 +; 1 -2 -4 0 +; Candidate RAT: -1 +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (check_rat + (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + cnfn)))))))) + (clc (neg v1) cln) + tt)))))) + +; RAT Test 3 +; Formula: +; p cnf 4 9 +; 1 2 -3 0 +; -1 -2 3 0 +; 2 3 -4 0 +; -2 -3 4 0 +; -1 -3 -4 0 +; 1 3 4 0 +; -1 2 4 0 +; 1 -2 -4 0 +; -1 0 +; Candidate RAT: 2 +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (check_rat + (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (cnfc (clc (neg v1) cln) + cnfn))))))))) + (clc (pos v2) cln) + tt)))))) + +; RAT Test 4 +; Formula: +; p cnf 4 2 +; 2 -3 0 +; 1 -4 0 +; Candidate RAT: 3 +; Answer: false +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (check_rat + (cnfc (clc (pos v2) (clc (neg v3) cln)) + (cnfc (clc (pos v1) (clc (neg v4) cln)) cnfn)) + (clc (pos v3) cln) + ff)))))) + + +; DRAT Test 1 (from Example 1 @ https://www.cs.utexas.edu/~marijn/drat-trim/) +; without deletions +; Formula: +; p cnf 4 8 +; 1 2 -3 0 +; -1 -2 3 0 +; 2 3 -4 0 +; -2 -3 4 0 +; -1 -3 -4 0 +; 1 3 4 0 +; -1 2 4 0 +; 1 -2 -4 +; Proof: +; -1 0 +; 2 0 +; 0 +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (: + (holds cln) + (drat_proof_of_bottom _ + (trust_cnf (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + cnfn))))))))) + (DRATProofa (clc (neg v1) cln) + (DRATProofa (clc (pos v2) cln) + (DRATProofa cln + DRATProofn)))))))))) + + +; DRAT Test 2 (from Example 1 @ https://www.cs.utexas.edu/~marijn/drat-trim/) +; with deletions +; Formula: +; p cnf 4 8 +; 1 2 -3 0 +; -1 -2 3 0 +; 2 3 -4 0 +; -2 -3 4 0 +; -1 -3 -4 0 +; 1 3 4 0 +; -1 2 4 0 +; 1 -2 -4 +; Proof: +; -1 0 +; d -1 -2 3 0 +; d -1 -3 -4 0 +; d -1 2 4 0 +; 2 0 +; d 1 2 -3 0 +; d 2 3 -4 0 +; 0 +(check + (% v1 var (% v2 var (% v3 var (% v4 var + (: (holds cln) + (drat_proof_of_bottom _ + (trust_cnf + (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + cnfn))))))))) + (DRATProofa (clc (neg v1) cln) + (DRATProofd (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (DRATProofd (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (DRATProofd (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (DRATProofa (clc (pos v2) cln) + (DRATProofd (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (DRATProofd (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (DRATProofa cln + DRATProofn))))))))))))))) + +; ===================================== ; +; Test Suite from "Two Flavors of DRAT" ; +; ===================================== ; + +; The paper includes a number of proofs which explore specified and operational +; DRAT validity. + +; Our test predicate for asserting the specified and operational validity of +; DRAT proofs +(declare spec_oper_test + (! f cnf + (! proof DRATProof + (! spec_validity bool + (! oper_validity bool + (! sc (^ (bool_and + (bool_eq (is_specified_drat_proof f proof) spec_validity) + (bool_eq (is_operational_drat_proof f proof) oper_validity) + ) tt) + TestSuccess)))))) + + +(declare x var) +(declare y var) +(declare z var) +(declare w var) +(define ex_1_formula + (cnfc (clc (pos x) (clc (pos y) (clc (pos z) cln))) + (cnfc (clc (neg x) (clc (pos y) (clc (pos z) cln))) + (cnfc (clc (pos x) (clc (neg y) (clc (pos z) cln))) + (cnfc (clc (neg x) (clc (neg y) (clc (pos z) cln))) + (cnfc (clc (pos x) (clc (pos y) (clc (neg z) cln))) + (cnfc (clc (neg x) (clc (pos y) (clc (neg z) cln))) + (cnfc (clc (pos x) (clc (neg y) (clc (neg z) cln))) + (cnfc (clc (neg x) (clc (neg y) (clc (neg z) cln))) + cnfn))))))))) + +; Spec-valid, operationally-invalid +(define ex_1_pf_pi + (DRATProofa (clc (pos x) (clc (pos y) cln)) + (DRATProofa (clc (pos x) cln) + (DRATProofa (clc (pos w) (clc (neg x) cln)) + (DRATProofd (clc (pos w) (clc (neg x) cln)) + (DRATProofa (clc (neg w) (clc (neg x) cln)) + (DRATProofa (clc (pos w) (clc (pos x) cln)) + (DRATProofa (clc (pos y) (clc (pos w) cln)) + (DRATProofa cln + DRATProofn))))))))) + +(check + (: TestSuccess + (spec_oper_test ex_1_formula ex_1_pf_pi tt ff))) + +; Spec-invalid, operationally valid +(define ex_1_pf_sigma + (DRATProofa (clc (pos x) (clc (pos y) cln)) + (DRATProofa (clc (pos x) cln) + (DRATProofd (clc (pos x) cln) + (DRATProofa (clc (pos w) (clc (neg y) cln)) + (DRATProofa (clc (neg w) (clc (neg y) cln)) + (DRATProofa (clc (pos w) cln) + (DRATProofa cln + DRATProofn)))))))) + +(check + (: TestSuccess + (spec_oper_test ex_1_formula ex_1_pf_sigma ff tt))) + +(declare x1 var) +(declare x2 var) +(declare x3 var) +(declare x4 var) +(declare x5 var) +(declare x6 var) +(declare x7 var) +(declare x8 var) +(declare x9 var) +(declare x10 var) + +(define ex_2_formula + (cnfc (clc (pos x1) cln) + (cnfc (clc (neg x1) (clc (pos x2) cln)) + (cnfc (clc (neg x1) (clc (neg x2) (clc (pos x3) cln))) + (cnfc (clc (neg x1) (clc (neg x3) (clc (pos x4) cln))) + (cnfc (clc (pos x5) (clc (pos x6) cln)) + (cnfc (clc (neg x2) (clc (neg x5) (clc (pos x7) cln))) + (cnfc (clc (neg x1) (clc (neg x5) (clc (pos x6) cln))) + (cnfc (clc (neg x5) (clc (neg x6) (clc (pos x4) cln))) + (cnfc (clc (neg x3) (clc (neg x6) (clc (pos x8) cln))) + (cnfc (clc (neg x6) (clc (neg x4) (clc (pos x3) cln))) + (cnfc (clc (neg x8) (clc (pos x5) cln)) + (cnfc (clc (neg x3) (clc (pos x9) (clc (pos x10) cln))) + (cnfc (clc (neg x4) (clc (neg x9) (clc (pos x10) cln))) + (cnfc (clc (neg x10) (clc (pos x9) cln)) + (cnfc (clc (neg x9) (clc (pos x7) cln)) + (cnfc (clc (neg x7) (clc (neg x8) (clc (neg x9) (clc (neg x10) cln)))) + cnfn))))))))))))))))) + +; Spec-valid, operationally-valid +(define ex_2_pf_tau + (DRATProofa (clc (pos x5) cln) + (DRATProofa (clc (pos x4) cln) + (DRATProofa (clc (pos x9) cln) + (DRATProofa cln + DRATProofn))))) + +(check + (: TestSuccess + (spec_oper_test ex_2_formula ex_2_pf_tau tt tt))) + +; Spec-valid, operationally unspecified in the paper, but its operationally valid. +(define ex_3_pf_tau_prime + (DRATProofa (clc (pos x5) cln) + (DRATProofd (clc (neg x1) (clc (pos x2) cln)) + (DRATProofa (clc (pos x9) cln) + (DRATProofa cln + DRATProofn))))) + +(check + (: TestSuccess + (spec_oper_test ex_2_formula ex_3_pf_tau_prime tt tt))) + +; Spec-invalid, operationally-invalid +(define ex_4_pf_pi_prime + (DRATProofa (clc (pos x) (clc (pos y) cln)) + (DRATProofa (clc (pos x) cln) + (DRATProofa (clc (pos w) (clc (neg x) cln)) + (DRATProofa (clc (neg w) (clc (neg x) cln)) + (DRATProofa (clc (pos w) (clc (pos x) cln)) + (DRATProofa (clc (pos y) (clc (pos w) cln)) + (DRATProofa cln + DRATProofn)))))))) + +(check + (: TestSuccess + (spec_oper_test ex_1_formula ex_4_pf_pi_prime ff ff))) + + +; Spec-valid, operationally valid +(define ex_5_pf_sigma_prime + (DRATProofa (clc (pos x) (clc (pos y) cln)) + (DRATProofa (clc (pos x) cln) + (DRATProofa (clc (pos w) (clc (neg y) cln)) + (DRATProofa (clc (neg w) (clc (neg y) cln)) + (DRATProofa (clc (pos w) cln) + (DRATProofa cln + DRATProofn))))))) + +(check + (: TestSuccess + (spec_oper_test ex_1_formula ex_5_pf_sigma_prime tt tt))) + diff --git a/test/signatures/er_test.plf b/test/signatures/er_test.plf new file mode 100644 index 000000000..671efdb46 --- /dev/null +++ b/test/signatures/er_test.plf @@ -0,0 +1,89 @@ +; Deps: er.plf + +; This is a circuitous proof that uses the definition introduction and +; unrolling rules +(check + (% v1 var + (% v2 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) cln))) + (% pf_c2 (holds (clc (neg v1) (clc (pos v2) cln))) + (% pf_c3 (holds (clc (pos v1) (clc (neg v2) cln))) + (% pf_c4 (holds (clc (neg v1) (clc (neg v2) cln))) + (: (holds cln) + (decl_definition + (neg v1) + (clc (neg v2) cln) + (\ v3 + (\ def3 + (clausify_definition _ _ _ def3 _ + (\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln))) + (\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln))) + (\ pf_cnf ; type: (common_tail_cnf (clc (neg v2) cln) (clc (neg v3) (clc (neg v1) cln))) + (@ pf_c7 (common_tail_cnf_prove_head _ _ _ pf_cnf) + ; Clauses + (satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1) (\ pf_c8 ; v2 + (satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2) (\ pf_c9 ; v3 + (satlem_simplify _ _ _ (R _ _ pf_c9 pf_c7 v3) (\ pf_c10 ; ~v2 ~v1 + (satlem_simplify _ _ _ (Q _ _ pf_c10 pf_c8 v2) (\ pf_c11 ; ~v1 + (satlem_simplify _ _ _ (Q _ _ pf_c11 pf_c3 v1) (\ pf_c12 ; ~v2 + (satlem_simplify _ _ _ (Q _ _ pf_c12 pf_c8 v2) (\ pf_c13 ; empty + pf_c13 + )) + )) + )) + )) + )) + )) + ) + ))) + ) + )) + ) + ) + )))) + )) +) + +; This is a test of ER proof produced by drat2er on Example 1 from: +; https://www.cs.utexas.edu/~marijn/drat-trim/ +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) + (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) + (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) + (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) + (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) + (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) + (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) + (: (holds cln) + (decl_definition + (neg v1) + cln + (\ v5 + (\ def1 + (clausify_definition _ _ _ def1 _ + (\ pf_c9 ; type: (holds (clc (pos def1v) cln)) + (\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln))) + (\ idc0 ; type: (common_tail_cnf cln _) + (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11 + (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12 + (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13 + (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c2 pf_c5 v3) pf_c8 v1) (\ pf_c14 + (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c2 v2) pf_c6 v1) (\ pf_c15 + (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c5 v4) pf_c1 v1) (\ pf_c16 + (satlem_simplify _ _ _ (R _ _ (Q _ _ pf_c3 pf_c15 v4) pf_c16 v3) (\ pf_c17 + (satlem_simplify _ _ _ (Q _ _ (R _ _ (Q _ _ pf_c4 pf_c15 v3) pf_c14 v4) pf_c17 v2) (\ pf_c18 + pf_c18 + )))))))))))))))) + ))) + ) + )) + ) + ) + )))))))) + )))) +) diff --git a/test/signatures/ex-mem.plf b/test/signatures/ex-mem.plf new file mode 100644 index 000000000..87d1053c4 --- /dev/null +++ b/test/signatures/ex-mem.plf @@ -0,0 +1,64 @@ +; Deps: sat.plf smt.plf th_base.plf + +(check +(% s sort +(% a (term s) +(% b (term s) +(% c (term s) +(% f (term (arrow s s)) + +; -------------------- declaration of input formula ----------------------------------- + +(% A1 (th_holds (= s a b)) +(% A2 (th_holds (= s b c)) +(% A3 (th_holds (not (= s a c))) + +; ------------------- specify that the following is a proof of the empty clause ----------------- + +(: (holds cln) + +; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------ + +(decl_atom (= s a b) (\ v1 (\ a1 +(decl_atom (= s b c) (\ v2 (\ a2 +(decl_atom (= s a c) (\ v3 (\ a3 + +; --------------------------- proof of theory lemma --------------------------------------------- + +(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3 (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT1 + +; -------------------- clausification of input formulas ----------------------------------------- + +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(clausify_false + (contra _ A1 l1) +))) (\ C1 +; C1 is the clause ( v1 ) + +(satlem _ _ +(asf _ _ _ a2 (\ l2 +(clausify_false + (contra _ A2 l2) +))) (\ C2 +; C2 is the clause ( v2 ) + +(satlem _ _ +(ast _ _ _ a3 (\ l3 +(clausify_false + (contra _ l3 A3) +))) (\ C3 +; C3 is the clause ( ~v3 ) + + +; -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ +(R _ _ C2 +(R _ _ C1 CT1 v1) v2) C3 v3) + +(\ x x)) + +))))))))))))))))))))))))))) diff --git a/test/signatures/ex_bv.plf b/test/signatures/ex_bv.plf new file mode 100644 index 000000000..a4f5ad816 --- /dev/null +++ b/test/signatures/ex_bv.plf @@ -0,0 +1,60 @@ +; Deps: sat.plf smt.plf th_base.plf th_bv.plf th_bv_bitblast.plf + +; (a = b) ^ (a = b & 00000) ^ (b = 11111) is UNSAT + +(check +(% a var_bv +(% b var_bv +(% f1 (th_holds (= (BitVec 4) (a_var_bv _ a) (a_var_bv _ b))) +(% f2 (th_holds (= (BitVec 4) (a_var_bv _ a) (bvand 4 (a_var_bv 4 b) (a_bv _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))) +(% f3 (th_holds (= (BitVec 4) (a_var_bv _ b) (a_bv _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn)))))))) +(: (holds cln) + +;; (decl_bv_term_var 5 a (\ ba1 +;; (decl_bv_term_var 5 b (\ ba2 +;; (decl_bv_term_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3 +;; (decl_bv_term_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4 + +(decl_atom (bitof a 4) (\ v1 (\ a1 +(decl_atom (bitof b 4) (\ v2 (\ a2 + +; bitblasting terms +(decl_bblast _ _ _ (bv_bbl_var 4 a _ ) (\ bt1 +(decl_bblast _ _ _ (bv_bbl_var 4 b _ ) (\ bt2 +(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bt3 +(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bt4 +(decl_bblast _ _ _ (bv_bbl_bvand 4 _ _ _ _ _ bt1 bt3) (\ bt5 + +; bitblasting formulas +(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt1 bt2) (\ bf1 +(th_let_pf _ (bv_bbl_bvult _ _ _ _ _ _ bt1 bt5) (\ bf2 +(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt2 bt4) (\ bf3 + +; CNFication +; a.4 V ~b.4 +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(ast _ _ _ a2 (\ l2 +(clausify_false + trust +))))) (\ C2 + +; ~a.4 +(satlem _ _ +(ast _ _ _ a1 (\ l1 +(clausify_false + trust +))) (\ C3 + +; b.4 +(satlem _ _ +(asf _ _ _ a2 (\ l2 +(clausify_false + trust +))) (\ C6 + + +(satlem_simplify _ _ _ +(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x)) + +))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/signatures/example-arrays.plf b/test/signatures/example-arrays.plf new file mode 100644 index 000000000..0e840274f --- /dev/null +++ b/test/signatures/example-arrays.plf @@ -0,0 +1,139 @@ +; Deps: sat.plf smt.plf th_base.plf th_arrays.plf + +; -------------------------------------------------------------------------------- +; literals : +; L1 : a = write( a, i, read( a, i ) +; L2 : read( a, k ) = read( write( a, i, read( a, i ) ), k ) +; L3 : i = k + +; input : +; ~L1 + +; (extenstionality) lemma : +; L1 or ~L2 + +; theory conflicts : +; L2 or ~L3 +; L2 or L3 + + +; With the theory lemma, the input is unsatisfiable. +; -------------------------------------------------------------------------------- + + +; (0) -------------------- term declarations ----------------------------------- + +(check +(% I sort +(% E sort +(% a (term (Array I E)) +(% i (term I) + + +; (1) -------------------- input formula ----------------------------------- + +(% A1 (th_holds (not (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))) + + + + +; (2) ------------------- specify that the following is a proof of the empty clause ----------------- + +(: (holds cln) + + + + +; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF ----------------- +; --- these should introduce (th_holds ...) + + +; extensionality lemma : notice this also introduces skolem k +(ext _ _ a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)) (\ k (\ A2 + + + + +; (4) -------------------- map theory literals to boolean variables +; --- maps all theory literals involved in proof to boolean literals + +(decl_atom (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1 +(decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2 +(decl_atom (= I i k) (\ v3 (\ a3 + + + +; (5) -------------------- theory conflicts --------------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(asf _ _ _ a3 (\ l3 +(asf _ _ _ a2 (\ l2 +(clausify_false + + ; use read over write rule "row" + (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2) + +))))) (\ CT1 +; CT1 is the clause ( v2 V v3 ) + +(satlem _ _ +(ast _ _ _ a3 (\ l3 +(asf _ _ _ a2 (\ l2 +(clausify_false + + ; use read over write rule "row1" + (contra _ (symm _ _ _ + (trans _ _ _ _ + (symm _ _ _ (cong _ _ _ _ _ _ + (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))) + l3)) + (trans _ _ _ _ + (row1 _ _ a i (apply _ _ (apply _ _ (read I E) a) i)) + (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3) + ))) + l2) + +))))) (\ CT2 +; CT2 is the clause ( v2 V ~v3 ) + + +; (6) -------------------- clausification ----------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(ast _ _ _ a1 (\ l1 +(clausify_false + +; input formula A1 is ( ~a1 ) +; the following is a proof of a1 ^ ( ~a1 ) => false + + (contra _ l1 A1) + +))) (\ C1 +; C1 is the clause ( ~v1 ) + + +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(ast _ _ _ a2 (\ l2 +(clausify_false + +; lemma A2 is ( a1 V ~a2 ) +; the following is a proof of ~a1 ^ a2 ^ ( a1 V ~a2 ) => false + + (contra _ l2 (or_elim_1 _ _ l1 A2)) + +))))) (\ C2 +; C2 is the clause ( v1 V ~v2 ) + + +; (7) -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ (R _ _ CT1 CT2 v3) (R _ _ C2 C1 v1) v2) + +(\ x x)) + +))))))))))))))))))))))))))) diff --git a/test/signatures/example-quant.plf b/test/signatures/example-quant.plf new file mode 100644 index 000000000..611fd182c --- /dev/null +++ b/test/signatures/example-quant.plf @@ -0,0 +1,95 @@ +; Deps: sat.plf smt.plf th_base.plf th_quant.plf + +; -------------------------------------------------------------------------------- +; literals : +; L1 : forall x. x != x +; L2 : t = t + +; input : +; L1 + +; (instantiation) lemma : +; L1 => L2 + +; theory conflicts : +; ~L2 + + +; With the theory lemma, the input is unsatisfiable. +; -------------------------------------------------------------------------------- + + +; (0) -------------------- term declarations ----------------------------------- + +(check +(% s sort +(% t (term s) + + +; (1) -------------------- input formula ----------------------------------- + +(% x (term s) +(% A1 (th_holds (forall _ x (not (= _ x x)))) + + + +; (2) ------------------- specify that the following is a proof of the empty clause ----------------- + +(: (holds cln) + + + +; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF ----------------- +; --- these should introduce (th_holds ...) + + +; instantiation lemma +(inst _ _ _ t (not (= _ t t)) A1 (\ A2 + + + + +; (4) -------------------- map theory literals to boolean variables +; --- maps all theory literals involved in proof to boolean literals + +(decl_atom (forall _ x (not (= _ x x))) (\ v1 (\ a1 +(decl_atom (= _ t t) (\ v2 (\ a2 + + + + +; (5) -------------------- theory conflicts --------------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(asf _ _ _ a2 (\ l2 +(clausify_false + + (contra _ (refl _ t) l2) + +))) (\ CT1 +; CT1 is the clause ( v2 ) + + +; (6) -------------------- clausification ----------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(ast _ _ _ a2 (\ l2 +(clausify_false + + (contra _ l2 A2) + +))) (\ C1 +; C1 is the clause ( ~v2 ) + + +; (7) -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ CT1 C1 v2) + +(\ x x)) + +)))))))))))))))))) diff --git a/test/signatures/example.plf b/test/signatures/example.plf new file mode 100644 index 000000000..775557fa6 --- /dev/null +++ b/test/signatures/example.plf @@ -0,0 +1,116 @@ +; Deps: sat.plf smt.plf th_base.plf + +; -------------------------------------------------------------------------------- +; input : +; ( a = b ) +; ( b = f(c) ) +; ( a != f(c) V a != b ) + +; theory lemma (by transitivity) : +; ( a != b V b != f(c) V a = f(c) ) + + +; With the theory lemma, the input is unsatisfiable. +; -------------------------------------------------------------------------------- + + + +(check +(% s sort +(% a (term s) +(% b (term s) +(% c (term s) +(% f (term (arrow s s)) + +; -------------------- declaration of input formula ----------------------------------- + +(% A1 (th_holds (= s a b)) +(% A2 (th_holds (= s b (apply _ _ f c))) +(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b)))) + + +; ------------------- specify that the following is a proof of the empty clause ----------------- + +(: (holds cln) + +; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------ + +(decl_atom (= s a b) (\ v1 (\ a1 +(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2 +(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3 + + +; --------------------------- proof of theory lemma --------------------------------------------- + +(satlem _ _ +(ast _ _ _ a1 (\ l1 +(ast _ _ _ a2 (\ l2 +(asf _ _ _ a3 (\ l3 +(clausify_false + +; this should be a proof of l1 ^ l2 ^ ~l3 => false +; this is done by theory proof rules (currently just use "trust") + + trust + +))))))) (\ CT +; CT is the clause ( ~v1 V ~v2 V v3 ) + +; -------------------- clausification of input formulas ----------------------------------------- + +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(clausify_false + +; input formula A1 is ( ~l1 ) +; the following should be a proof of l1 ^ ( ~l1 ) => false +; this is done by natural deduction rules + + (contra _ A1 l1) + +))) (\ C1 +; C1 is the clause ( v1 ) + + +(satlem _ _ +(asf _ _ _ a2 (\ l2 +(clausify_false + +; input formula A2 is ( ~l2 ) +; the following should be a proof of l2 ^ ( ~l2 ) => false +; this is done by natural deduction rules + + (contra _ A2 l2) + +))) (\ C2 +; C2 is the clause ( v2 ) + + +(satlem _ _ +(ast _ _ _ a3 (\ l3 +(ast _ _ _ a1 (\ l1 +(clausify_false + +; input formula A3 is ( ~a3 V ~a1 ) +; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false +; this is done by natural deduction rules + + (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3)) + +))))) (\ C3 +; C3 is the clause ( ~v3 V ~v1 ) + + + +; -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ C1 +(R _ _ C2 +(R _ _ CT C3 v3) v2) v1) + +(\ x x)) + +)))))))))))))))))))))))))) +) diff --git a/test/signatures/lrat_test.plf b/test/signatures/lrat_test.plf new file mode 100644 index 000000000..466216ff9 --- /dev/null +++ b/test/signatures/lrat_test.plf @@ -0,0 +1,892 @@ +; Deps: lrat.plf +(declare test_clause_append + (! c1 clause + (! c2 clause + (! cr clause + (! sc (^ (clause_append c1 c2) cr) type))))) + +; Test passes if the (test_clause_append ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (test_clause_append + (clc (pos v1) (clc (neg v2) cln)) + (clc (pos v3) (clc (neg v2) cln)) + (clc (pos v1) (clc (neg v2) (clc (pos v3) (clc (neg v2) cln)))) + ) + ))) +) + +; Test passes if the (test_clause_append ...) application is well-typed. +(check + (% v2 var + (% v3 var + (test_clause_append + cln + (clc (pos v3) (clc (neg v2) cln)) + (clc (pos v3) (clc (neg v2) cln)) + ) + )) +) + +; Test passes if the (test_clause_append ...) application is well-typed. +(check + (% v2 var + (% v3 var + (test_clause_append + (clc (pos v3) (clc (neg v2) cln)) + cln + (clc (pos v3) (clc (neg v2) cln)) + ) + )) +) + +(declare test_CMap_remove_many + (! is CIList + (! cs CMap + (! csr CMap + (! sc (^ (CMap_remove_many is cs) csr) type))))) + +; Test passes if the (test_CMap_remove_many ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v4) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v3) cln)) + (@ c4 (clc (neg v3) (clc (neg v4) cln)) + (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) + (@ cs_out (CMapc 3 c2 (CMapc 5 c3 CMapn)) + (@ is_in (CIListc 0 (CIListc 4 (CIListc 6 CIListn))) + (test_CMap_remove_many + is_in + cs_in + cs_out + ) + ))) + )))) + )))) +) + +; Test passes if the (test_CMap_remove_many ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v4) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v3) cln)) + (@ c4 (clc (neg v3) (clc (neg v4) cln)) + (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) + (@ cs_out (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) + (@ is_in (CIListc 4 CIListn) + (test_CMap_remove_many + is_in + cs_in + cs_out + ) + ))) + )))) + )))) +) + +(declare test_clause_remove_all + (! l lit + (! c clause + (! c' clause + (! sc (^ (clause_remove_all l c) c') type))))) + +; Test passes if the (test_clause_remove_all ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v4) (clc (neg v2) (clc (neg v2) (clc (pos v2) (clc (pos v1) cln))))) + (@ c2 (clc (pos v4) (clc (pos v2) (clc (pos v1) cln))) + (test_clause_remove_all + (neg v2) + c1 + c2 + ) + )) + )))) +) + +(declare test_collect_resolution_targets + (! cs CMap + (! c clause + (! is CIList + (! sc (^ (collect_resolution_targets cs c) is) type))))) + +; Test passes if the (test_collect_resolution_targets ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v3) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v3) cln)) + (@ c4 (clc (neg v3) (clc (pos v3) cln)) + (@ ct (clc (neg v3) (clc (neg v4) cln)) + (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) + (@ is_out (CIListc 0 (CIListc 4 (CIListc 5 (CIListc 6 CIListn)))) + (test_collect_resolution_targets + cs_in + ct + is_out + ) + ))) + )))) + )))) +) + +(declare test_resolution_targets_match + (! c CIList + (! g RATHints + (! ans bool + (! sc (^ (resolution_targets_match c g) ans) type))))) + +; Test passes if the (test_resolution_targets_match ...) application is well-typed. +(check + (@ idxs_in (CIListc 0 (CIListc 4 (CIListc 5 (CIListc 6 CIListn)))) + (@ hints_in + (RATHintsc 0 Tracen + (RATHintsc 4 Tracen + (RATHintsc 5 Tracen + (RATHintsc 6 Tracen + RATHintsn)))) + (test_resolution_targets_match + idxs_in + hints_in + tt + ) + )) +) + +; Test passes if the (test_resolution_targets_match ...) application is well-typed. +(check + (@ idxs_in (CIListc 0 (CIListc 2 (CIListc 5 (CIListc 6 CIListn)))) + (@ hints_in + (RATHintsc 0 Tracen + (RATHintsc 4 Tracen + (RATHintsc 5 Tracen + (RATHintsc 6 Tracen + RATHintsn)))) + (test_resolution_targets_match + idxs_in + hints_in + ff + ) + )) +) + +(declare test_is_at_trace + (! cs CMap + (! c clause + (! t Trace + (! r UPResult + (! sc (^ (is_at_trace cs c t) r) type)))))) + +; Test passes if the (test_is_at_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v3) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v1) cln)) + (@ c4 (clc (neg v3) (clc (pos v2) cln)) + (@ cs (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) + (@ c (clc (neg v3) cln) + (@ t (Tracec 3 (Tracec 5 (Tracec 6 Tracen))) + (test_is_at_trace + cs + c + t + UPR_Bottom + ) + ))) + )))) + )))) +) + +; Test passes if the (test_is_at_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v3) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v1) cln)) + (@ c4 (clc (neg v3) (clc (pos v2) cln)) + (@ cs (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) + (@ c (clc (neg v3) cln) + (@ t (Tracec 3 (Tracec 5 Tracen)) + (test_is_at_trace + cs + c + t + UPR_Ok + ) + ))) + )))) + )))) +) + +; Test passes if the (test_is_at_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v3) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v1) cln)) + (@ c4 (clc (neg v3) (clc (pos v2) cln)) + (@ cs (CMapc 1 c1 (CMapc 2 c2 (CMapc 3 c3 (CMapc 4 c4 CMapn)))) + (@ c (clc (neg v3) cln) + (@ t (Tracec 2 (Tracec 1 Tracen)) + (test_is_at_trace + cs + c + t + UPR_Broken + ) + ))) + )))) + )))) +) + +(declare test_is_rat_trace (! cs CMap + (! c clause + (! t Trace + (! h RATHints + (! r UPResult + (! sc (^ (is_rat_trace cs c t h) r) type))))))) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 CMapn)))))))) + (@ c (clc (pos v1) cln) + (@ t Tracen + (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) + RATHintsn))) + (test_is_rat_trace + cs + c + t + h + UPR_Bottom + ) + )))) + )))))))) + )))) +) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 CMapn)))))))) + (@ c (clc (pos v1) cln) + (@ t Tracen + (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + RATHintsn)) + (test_is_rat_trace + cs + c + t + h + UPR_Broken + ) + )))) + )))))))) + )))) +) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 CMapn)))))))) + (@ c (clc (pos v1) cln) + (@ t Tracen + (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 3 (Tracec 1 Tracen)) + RATHintsn))) + (test_is_rat_trace + cs + c + t + h + UPR_Broken + ) + )))) + )))))))) + )))) +) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 CMapn)))))))) + (@ c (clc (pos v1) cln) + (@ t Tracen + (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 3 Tracen) + RATHintsn))) + (test_is_rat_trace + cs + c + t + h + UPR_Broken + ) + )))) + )))))))) + )))) +) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ c9 (clc (pos v1) cln) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 + (CMapc 9 c9 + CMapn))))))))) + (@ c (clc (pos v2) cln) + (@ t (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + (@ h RATHintsn + (test_is_rat_trace + cs + c + t + h + UPR_Bottom + ) + )))) + ))))))))) + )))) +) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ c9 (clc (pos v1) cln) + (@ c10 (clc (pos v2) cln) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 + (CMapc 9 c9 + (CMapc 10 c10 + CMapn)))))))))) + (@ c cln + (@ t (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + (@ h RATHintsn + (test_is_rat_trace + cs + c + t + h + UPR_Bottom + ) + )))) + )))))))))) + )))) +) + +(declare test_is_lrat_proof_of_bottom + (! f CMap + (! p LRATProof + (! r bool + (! sc (^ (is_lrat_proof_of_bottom f p) r) type))))) + +; Test passes if the (test_is_lrat_proof_of_bottom ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 + CMapn)))))))) + (@ p + (LRATProofa 9 + (clc (pos v1) cln) + Tracen + (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) + RATHintsn))) + (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) + (LRATProofa 10 + (clc (pos v2) cln) + (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 11 + cln + (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + RATHintsn + LRATProofn))))) + (test_is_lrat_proof_of_bottom + cs + p + tt + ) + )) + )))))))) + )))) +) + +; Test passes if the (test_is_lrat_proof_of_bottom ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 + CMapn)))))))) + (@ p + (LRATProofa 9 + (clc (pos v1) cln) + Tracen + (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) + RATHintsn))) + (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) + (LRATProofa 10 + (clc (pos v2) cln) + (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 11 + cln + (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 Tracen)))) + RATHintsn + LRATProofn))))) + (test_is_lrat_proof_of_bottom + cs + p + ff + ) + )) + )))))))) + )))) +) + +; Proof from Figure 2 of "Efficient Certified RAT Verification" +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) + (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) + (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) + (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) + (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) + (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) + (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) + (@ pf_cmap + (CMapc_proof 1 _ _ _ pf_c1 + (CMapc_proof 2 _ _ _ pf_c2 + (CMapc_proof 3 _ _ _ pf_c3 + (CMapc_proof 4 _ _ _ pf_c4 + (CMapc_proof 5 _ _ _ pf_c5 + (CMapc_proof 6 _ _ _ pf_c6 + (CMapc_proof 7 _ _ _ pf_c7 + (CMapc_proof 8 _ _ _ pf_c8 + CMapn_proof)))))))) + (@ lrat_proof_witness + (LRATProofa 9 + (clc (pos v1) cln) + Tracen + (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) + RATHintsn))) + (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) + (LRATProofa 10 + (clc (pos v2) cln) + (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 11 + cln + (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + RATHintsn + LRATProofn))))) + (: + (holds cln) + (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) + )) + )))))))) + )))) +) + +; Proof from Figure 2 of "Efficient Certified RAT Verification" +; With duplicates +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))) + (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) + (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (pos v3) (clc (pos v3) (clc (neg v4) cln)))))) + (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) + (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) (clc (neg v4) cln))))) + (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v3) (clc (pos v4) cln))))) + (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) + (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v2) (clc (neg v4) cln))))) + (@ pf_cmap + (CMapc_proof 1 _ _ _ pf_c1 + (CMapc_proof 2 _ _ _ pf_c2 + (CMapc_proof 3 _ _ _ pf_c3 + (CMapc_proof 4 _ _ _ pf_c4 + (CMapc_proof 5 _ _ _ pf_c5 + (CMapc_proof 6 _ _ _ pf_c6 + (CMapc_proof 7 _ _ _ pf_c7 + (CMapc_proof 8 _ _ _ pf_c8 + CMapn_proof)))))))) + (@ lrat_proof_witness + (LRATProofa 9 + (clc (pos v1) cln) + Tracen + (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) + RATHintsn))) + (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) + (LRATProofa 10 + (clc (pos v2) cln) + (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 11 + cln + (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + RATHintsn + LRATProofn))))) + (: + (holds cln) + (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) + )) + )))))))) + )))) +) + +; Clauses 1 and 9 are identical. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) + (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) + (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) + (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) + (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) + (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) + (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) + (% pf_c9 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (@ pf_cmap + (CMapc_proof 1 _ _ _ pf_c1 + (CMapc_proof 2 _ _ _ pf_c2 + (CMapc_proof 3 _ _ _ pf_c3 + (CMapc_proof 4 _ _ _ pf_c4 + (CMapc_proof 5 _ _ _ pf_c5 + (CMapc_proof 6 _ _ _ pf_c6 + (CMapc_proof 7 _ _ _ pf_c7 + (CMapc_proof 8 _ _ _ pf_c8 + (CMapc_proof 9 _ _ _ pf_c9 + CMapn_proof))))))))) + (@ lrat_proof_witness + (LRATProofa 10 + (clc (pos v1) cln) + Tracen + (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 9 Tracen)) + RATHintsn))) + (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 (CIListc 9 CIListn)))) + (LRATProofa 11 + (clc (pos v2) cln) + (Tracec 10 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 12 + cln + (Tracec 10 (Tracec 11 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + RATHintsn + LRATProofn))))) + (: + (holds cln) + (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) + )) + ))))))))) + )))) +) + +; Clauses 1 and 9 are logically identical, but the literals have been reordered. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) + (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) + (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) + (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) + (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) + (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) + (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) + (% pf_c9 (holds (clc (neg v3) (clc (pos v2) (clc (pos v1) cln)))) + (@ pf_cmap + (CMapc_proof 1 _ _ _ pf_c1 + (CMapc_proof 2 _ _ _ pf_c2 + (CMapc_proof 3 _ _ _ pf_c3 + (CMapc_proof 4 _ _ _ pf_c4 + (CMapc_proof 5 _ _ _ pf_c5 + (CMapc_proof 6 _ _ _ pf_c6 + (CMapc_proof 7 _ _ _ pf_c7 + (CMapc_proof 8 _ _ _ pf_c8 + (CMapc_proof 9 _ _ _ pf_c9 + CMapn_proof))))))))) + (@ lrat_proof_witness + (LRATProofa 10 + (clc (pos v1) cln) + Tracen + (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 9 Tracen)) + RATHintsn))) + (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 (CIListc 9 CIListn)))) + (LRATProofa 11 + (clc (pos v2) cln) + (Tracec 10 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 12 + cln + (Tracec 10 (Tracec 11 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + RATHintsn + LRATProofn))))) + (: + (holds cln) + (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) + )) + ))))))))) + )))) +) + +; Proof from Figure 1 of "Efficient Certified RAT Verification" +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) + (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) + (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) + (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) + (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) + (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) + (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) + (@ pf_cmap + (CMapc_proof 1 _ _ _ pf_c1 + (CMapc_proof 2 _ _ _ pf_c2 + (CMapc_proof 3 _ _ _ pf_c3 + (CMapc_proof 4 _ _ _ pf_c4 + (CMapc_proof 5 _ _ _ pf_c5 + (CMapc_proof 6 _ _ _ pf_c6 + (CMapc_proof 7 _ _ _ pf_c7 + (CMapc_proof 8 _ _ _ pf_c8 + CMapn_proof)))))))) + (@ lrat_proof_witness + (LRATProofa 9 + (clc (pos v1) (clc (pos v2) cln)) + (Tracec 1 (Tracec 6 (Tracec 3 Tracen))) + RATHintsn + (LRATProofd (CIListc 1 CIListn) + (LRATProofa 10 + (clc (pos v1) (clc (pos v3) cln)) + (Tracec 9 (Tracec 8 (Tracec 6 Tracen))) + RATHintsn + (LRATProofd (CIListc 6 CIListn) + (LRATProofa 11 + (clc (pos v1) cln) + (Tracec 10 (Tracec 9 (Tracec 4 (Tracec 8 Tracen)))) + RATHintsn + (LRATProofd (CIListc 8 (CIListc 9 (CIListc 10 CIListn))) + (LRATProofa 12 + (clc (pos v2) cln) + (Tracec 11 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 13 + cln + (Tracec 11 (Tracec 12 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + RATHintsn + LRATProofn + ))))))))) + (: + (holds cln) + (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) + )) + )))))))) + )))) +) diff --git a/test/signatures/run_test.py b/test/signatures/run_test.py new file mode 100755 index 000000000..ac14267e9 --- /dev/null +++ b/test/signatures/run_test.py @@ -0,0 +1,123 @@ +#!/usr/bin/env python + +import argparse +import re +import os.path +import sys +import subprocess + + +class TestConfiguration(object): + """Represents a test to run.""" + def __init__(self): + """Initialized from program arguments. + Exists with code 2 and prints usage message on invalid arguments.""" + parser = argparse.ArgumentParser( + description='Runs `lfscc on a test file.') + parser.add_argument('lfscc_binary') + parser.add_argument('input') + parser.add_argument('include_dirs', nargs='*') + args = parser.parse_args() + + self.lfscc = args.lfscc_binary + self.dep_graph = DepGraph(args.input, args.include_dirs) + + +class DepGraph(object): + """Represents a dependency graph of LFSC input files""" + def __init__(self, root_path, include_dirs): + """Creates a dependency graph rooted a `root_path`. + Computes a root-last topological sort. + Exits with exitcode 1 on cyclic dependencies""" + + # Root of the graph + self._r = root_path + + # Nodes (paths) that have been visited + self._visited = set() + + # Nodes (paths) that have been ordered + self._ordered_set = set() + + # The order of nodes (paths). Root is last. + self._ordered_paths = [] + + self.include_dirs = include_dirs + + # Start DFS topo-order + self._visit(root_path) + + def _visit(self, p): + """Puts the descendents of p in the order, parent-last""" + node = TestFile(p, self.include_dirs) + self._visited.add(p) + for n in node.dep_paths: + if n not in self._ordered_set: + if n in self._visited: + # Our child is is an ancestor our ours!? + print("{} and {} are in a dependency cycle".format(p, n)) + sys.exit(1) + else: + self._visit(n) + self._ordered_paths.append(p) + self._ordered_set.add(p) + + def getPathsInOrder(self): + return self._ordered_paths + + +class TestFile(object): + """Represents a testable input file to LFSC""" + def __init__(self, path, include_dirs): + """Read the file at `path` and determine its immediate dependencies""" + self.path = path + self._get_config_map() + self.deps = self.config_map['deps'].split() if ( + 'deps' in self.config_map) else [] + self.dir = os.path.dirname(self.path) + self.dep_paths = [] + include_paths = include_dirs + [self.dir] + for dep in self.deps: + found_dep = False + for include_path in include_paths: + dep_path = os.path.join(include_path, dep) + if os.path.isfile(dep_path): + self.dep_paths.append(dep_path) + found_dep = True + break + assert found_dep + + def _get_comment_lines(self): + """Return an iterator over comment lines, ;'s included""" + with open(self.path, 'r') as test_file: + return (line for line in test_file.readlines() if \ + re.match(r'^\s*;.*$', line) is not None) + + def _get_config_map(self): + """Populate self.config_map. + Config variables are set using the syntax + ; Var Name Spaces Okay: space separated values""" + m = {} + for l in self._get_comment_lines(): + match = re.match(r'^.*;\s*(\w+(?:\s+\w+)*)\s*:(.*)$', l) + if match is not None: + m[match.group(1).replace(' ', '').lower()] = match.group(2) + self.config_map = m + + +def main(): + configuration = TestConfiguration() + cmd = [configuration.lfscc] + configuration.dep_graph.getPathsInOrder() + result = subprocess.Popen(cmd, + stderr=subprocess.STDOUT, + stdout=subprocess.PIPE) + code = result.wait() + if 0 != code: + stdout = result.stdout.read() + if stdout: + print(stdout.decode()) + return code + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/test/signatures/th_lira_test.plf b/test/signatures/th_lira_test.plf new file mode 100644 index 000000000..d1fbe59f4 --- /dev/null +++ b/test/signatures/th_lira_test.plf @@ -0,0 +1,294 @@ +; Deps: th_lira.plf +;; Proof (from predicates on linear polynomials) that the following imply bottom +; +; -x - 1/2 y + 2 >= 0 +; x + y - 8 >= 0 +; x - y + 0 >= 0 +; +(check + ; Variables + (% x real_var + (% y real_var + ; linear combinations + (@ m1 (lc_cons (~ 1/1) (av_from_real x) (lc_cons (~ 1/2) (av_from_real y) lc_null)) + (@ m2 (lc_cons 1/1 (av_from_real x) (lc_cons 1/1 (av_from_real y) lc_null)) + (@ m3 (lc_cons 1/1 (av_from_real x) (lc_cons (~ 1/1) (av_from_real y) lc_null)) + ; affine functions + (@ p1 (aff_cons 2/1 m1) + (@ p2 (aff_cons (~ 8/1) m2) + (@ p3 (aff_cons 0/1 m3) + ; Proofs of affine bounds + (% pf_nonneg_1 (th_holds (bounded_aff p1 bound_non_neg)) + (% pf_nonneg_2 (th_holds (bounded_aff p2 bound_non_neg)) + (% pf_nonneg_3 (th_holds (bounded_aff p3 bound_non_neg)) + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 4/1 pf_nonneg_1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 3/1 pf_nonneg_2) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 pf_nonneg_3) + bounded_aff_ax_0_>=_0))))) + ))))) + )))) + )) +) + +;; Proof (from predicates on real terms) that the following imply bottom +; +; -x - 1/2 y >= 2 +; x + y >= 8 +; x - y >= 0 +; +(check + ; Declarations + ; Variables + (% x real_var + (% y real_var + ; real predicates + (@ f1 (>=_Real (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (*_Real (a_real (~ 1/2)) (term_real_var y))) (a_real (~ 2/1))) + (@ f2 (>=_Real (+_Real (*_Real (a_real 1/1) (term_real_var x)) (*_Real (a_real 1/1) (term_real_var y))) (a_real 8/1)) + (@ f3 (>=_Real (+_Real (*_Real (a_real 1/1) (term_real_var x)) (*_Real (a_real (~ 1/1)) (term_real_var y))) (a_real 0/1)) + ; proof of real predicates + (% pf_f1 (th_holds f1) + (% pf_f2 (th_holds f2) + (% pf_f3 (th_holds f3) + + + ; Normalization + ; real term -> linear polynomial normalization witnesses + (@ n1 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) + (is_aff_mul_c_L _ _ _ (~ 1/2) (is_aff_var_real y))) + (is_aff_const (~ 2/1))) + pf_f1) + (@ n2 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real x)) + (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real y))) + (is_aff_const 8/1)) + pf_f2) + (@ n3 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real x)) + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real y))) + (is_aff_const 0/1)) + pf_f3) + + ; derivation of a contradiction using farkas coefficients + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 4/1 n1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 3/1 n2) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n3) + bounded_aff_ax_0_>=_0))))) + ))) + ))) + ))) + )) +) + +;; Term proof, 2 premises of the form (>=), one of the form (not >=) +;; Proof (from predicates on real terms) that the following imply bottom +; +; -x + y >= 2 +; x + y >= 2 +; not[ y >= -2] => [y < -2] => [-y > 2] +; +(check + ; Declarations + ; Variables + (% x real_var + (% y real_var + ; real predicates + (@ f1 (>=_Real + (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (term_real_var y)) + (a_real 2/1)) + (@ f2 (>=_Real + (+_Real (term_real_var x) (term_real_var y)) + (a_real 2/1)) + (@ f3 (not (>=_Real (term_real_var y) (a_real (~ 2/1)))) + + ; Normalization + ; proof of real predicates + (% pf_f1 (th_holds f1) + (% pf_f2 (th_holds f2) + (% pf_f3 (th_holds f3) + ; real term -> linear polynomial normalization witnesses + (@ n1 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) + (is_aff_var_real y)) + (is_aff_const 2/1)) + pf_f1) + (@ n2 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_var_real x) + (is_aff_var_real y)) + (is_aff_const 2/1)) + pf_f2) + (@ n3 (aff_>_from_term _ _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_var_real y) + (is_aff_const (~ 2/1))) + pf_f3) + + ; derivation of a contradiction using farkas coefficients + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n2) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 2/1 n3) + bounded_aff_ax_0_>=_0))))) + ))) + ))) + ))) + )) +) + +;; Term proof, 2 premises of the form (>=), one of the form (not >=) +;; x is a real, +;; y is an integer +;; Proof (from predicates on real terms) that the following imply bottom +; +; -x + y >= 2 +; x + y >= 2 +; not[ y >= -2] => [y < -2] => [-y > 2] +; +(check + ; Declarations + ; Variables + (% x real_var + (% y int_var + ; real predicates + (@ f1 (>=_Real + (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (term_int_to_real (term_int_var y))) + (a_real 2/1)) + (@ f2 (>=_Real + (+_Real (term_real_var x) (term_int_to_real (term_int_var y))) + (a_real 2/1)) + (@ f3 (not (>=_IntReal (term_int_var y) (a_real (~ 2/1)))) + + ; Normalization + ; proof of real predicates + (% pf_f1 (th_holds f1) + (% pf_f2 (th_holds f2) + (% pf_f3 (th_holds f3) + ; real term -> linear polynomial normalization witnesses + (@ n1 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) + (is_aff_var_int y)) + (is_aff_const 2/1)) + (pf_reified_arith_pred _ _ pf_f1)) + (@ n2 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_var_real x) + (is_aff_var_int y)) + (is_aff_const 2/1)) + (pf_reified_arith_pred _ _ pf_f2)) + (@ n3 (aff_>_from_term _ _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_var_int y) + (is_aff_const (~ 2/1))) + (pf_reified_arith_pred _ _ pf_f3)) + + ; derivation of a contradiction using farkas coefficients + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n2) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 2/1 n3) + bounded_aff_ax_0_>=_0))))) + ))) + ))) + ))) + )) +) + +;; Term proof, 2 premises of the form (>=), one of the form (not >=) +;; x is a real, +;; y is an integer, and needs tightening +;; Proof (from predicates on real terms) that the following imply bottom +; +; -x >= -1/2 +; x + y >= 0 +; not[ y >= 0] => [y < 0] => [-y >= 1] +; +(check + ; Declarations + ; Variables + (% x real_var + (% y int_var + ; real predicates + (@ f1 (>=_Real + (*_Real (a_real (~ 1/1)) (term_real_var x)) + (a_real (~ 1/2))) + (@ f2 (>=_Real + (+_Real (term_real_var x) (term_int_to_real (term_int_var y))) + (a_real 0/1)) + (@ f3 (not (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (term_int_to_real (a_int 0)))) + + ; Normalization + ; proof of real predicates + (% pf_f1 (th_holds f1) + (% pf_f2 (th_holds f2) + (% pf_f3 (th_holds f3) + ; real term -> linear polynomial normalization witnesses + (@ n1 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) + (is_aff_const (~ 1/2))) + (pf_reified_arith_pred _ _ pf_f1)) + (@ n2 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_var_real x) + (is_aff_var_int y)) + (is_aff_const 0/1)) + (pf_reified_arith_pred _ _ pf_f2)) + (@ n3 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_int y)) + (is_aff_const 1/1)) + (pf_reified_arith_pred _ _ + (tighten_not_>=_IntInt _ _ _ _ (check_neg_of_greatest_integer_below_int 1 0) pf_f3))) + + ; derivation of a contradiction using farkas coefficients + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n2) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n3) + bounded_aff_ax_0_>=_0))))) + ))) + ))) + ))) + )) +)