# 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()
-; Depends on lrat.plf
+; Deps: lrat.plf
;
; Implementation of DRAT checking.
;
+++ /dev/null
-;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)))
-
-; Depends on sat.plf
+; Deps: sat.plf
; This file exists to support the **definition introduction** (or **extension**)
; rule in the paper:
+++ /dev/null
-; 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
- ))))))))))))))))
- )))
- )
- ))
- )
- )
- ))))))))
- ))))
-)
+++ /dev/null
-(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))
-
-)))))))))))))))))))))))))))
+++ /dev/null
-; (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))
-
-)))))))))))))))))))))))))))))))))))))))))))))
+++ /dev/null
-; 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))
-
-)))))))))))))))))))))))))))
+++ /dev/null
-; 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))
-
-))))))))))))))))))
+++ /dev/null
-; 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))
-
-))))))))))))))))))))))))))
-)
; 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:
+++ /dev/null
-(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))
- ))
- ))))))))
- ))))
-)
; SMT syntax and semantics (not theory-specific)
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; depends on sat.plf
+; Deps: sat.plf
(declare formula type)
(declare th_holds (! f formula type))
; Theory of Arrays
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; depends on : th_base.plf
+; Deps: th_base.plf
; sorts
; Theory of Equality and Congruence Closure
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; depends on : smt.plf
+; Deps: smt.plf
; sorts :
-; 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.
+++ /dev/null
-; 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)))))
- )))
- )))
- )))
- ))
-)
-; Depends On: th_smt.plf
+; Deps: smt.plf
(declare Real sort)
(define arithpred_Real (! x (term Real)
add_subdirectory(java)
endif()
endif()
+
+if(LFSC_BINARY)
+ add_subdirectory(signatures)
+endif()
--- /dev/null
+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()
--- /dev/null
+# 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.
--- /dev/null
+; 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)))
+
--- /dev/null
+; 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
+ ))))))))))))))))
+ )))
+ )
+ ))
+ )
+ )
+ ))))))))
+ ))))
+)
--- /dev/null
+; 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))
+
+)))))))))))))))))))))))))))
--- /dev/null
+; 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))
+
+)))))))))))))))))))))))))))))))))))))))))))))
--- /dev/null
+; 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))
+
+)))))))))))))))))))))))))))
--- /dev/null
+; 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))
+
+))))))))))))))))))
--- /dev/null
+; 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))
+
+))))))))))))))))))))))))))
+)
--- /dev/null
+; 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))
+ ))
+ ))))))))
+ ))))
+)
--- /dev/null
+#!/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())
--- /dev/null
+; 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)))))
+ )))
+ )))
+ )))
+ ))
+)
projects / cvc5.git / commitdiff