diff options
Diffstat (limited to 'test/signatures/lrat_test.plf')
| -rw-r--r-- | test/signatures/lrat_test.plf | 892 |
1 files changed, 892 insertions, 0 deletions
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)) + )) + )))))))) + )))) +) |