diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-01 08:44:21 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-01 10:44:21 -0500 |
commit | 9ce4c3153d42bc079470b7bd73bf131499b3fcbe (patch) | |
tree | 40a384f74915e2c009bb2a66bd0295e62edcfc2e /proofs | |
parent | 04154c08c1af81bb751376ae9379c071a95c5a3f (diff) |
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
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/signatures/drat.plf | 2 | ||||
-rw-r--r-- | proofs/signatures/drat_test.plf | 434 | ||||
-rw-r--r-- | proofs/signatures/er.plf | 2 | ||||
-rw-r--r-- | proofs/signatures/er_test.plf | 89 | ||||
-rw-r--r-- | proofs/signatures/ex-mem.plf | 62 | ||||
-rw-r--r-- | proofs/signatures/ex_bv.plf | 58 | ||||
-rw-r--r-- | proofs/signatures/example-arrays.plf | 139 | ||||
-rw-r--r-- | proofs/signatures/example-quant.plf | 95 | ||||
-rw-r--r-- | proofs/signatures/example.plf | 116 | ||||
-rw-r--r-- | proofs/signatures/lrat.plf | 2 | ||||
-rw-r--r-- | proofs/signatures/lrat_test.plf | 891 | ||||
-rw-r--r-- | proofs/signatures/smt.plf | 2 | ||||
-rw-r--r-- | proofs/signatures/th_arrays.plf | 2 | ||||
-rw-r--r-- | proofs/signatures/th_base.plf | 2 | ||||
-rw-r--r-- | proofs/signatures/th_lira.plf | 2 | ||||
-rw-r--r-- | proofs/signatures/th_lira_test.plf | 294 | ||||
-rw-r--r-- | proofs/signatures/th_real.plf | 2 |
17 files changed, 8 insertions, 2186 deletions
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) |