diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-05 18:29:34 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-23 13:21:47 -0500 |
commit | ff7d33c2f75668fde0f149943e3cf1bedad1102f (patch) | |
tree | b2533c2a7bf09602d567379ea1dc3bacc9f059c3 /proofs/signatures/smt.plf | |
parent | b2bb2138543e75f64c3a794df940a221e4b5a97b (diff) |
Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
Diffstat (limited to 'proofs/signatures/smt.plf')
-rwxr-xr-x | proofs/signatures/smt.plf | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 75bfc442f..67ce3988a 100755 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -31,7 +31,7 @@ (! t1 (term (arrow s1 s2)) (! t2 (term s1) (term s2)))))) - + (declare ite (! s sort (! f formula (! t1 (term s) @@ -102,7 +102,7 @@ (! f formula (! u (th_holds f) (th_holds (not (not f)))))) - + (declare not_not_elim (! f formula (! u (th_holds (not (not f))) @@ -116,14 +116,14 @@ (! u1 (th_holds (not f1)) (! u2 (th_holds (or f1 f2)) (th_holds f2)))))) - + (declare or_elim_2 (! f1 formula (! f2 formula (! u1 (th_holds (not f2)) (! u2 (th_holds (or f1 f2)) (th_holds f1)))))) - + ;; and elimination (declare and_elim_1 @@ -131,13 +131,13 @@ (! f2 formula (! u (th_holds (and f1 f2)) (th_holds f1))))) - + (declare and_elim_2 (! f1 formula (! f2 formula (! u (th_holds (and f1 f2)) (th_holds f2))))) - + ;; not impl elimination (declare not_impl_elim_1 @@ -145,18 +145,18 @@ (! f2 formula (! u (th_holds (not (impl f1 f2))) (th_holds f1))))) - + (declare not_impl_elim_2 (! f1 formula (! f2 formula (! u (th_holds (not (impl f1 f2))) (th_holds (not f2)))))) - + ;; impl elimination (declare impl_intro (! f1 formula (! f2 formula - (! i1 (! u (th_holds f1) + (! i1 (! u (th_holds f1) (th_holds f2)) (th_holds (impl f1 f2)))))) @@ -164,9 +164,9 @@ (! f1 formula (! f2 formula (! u1 (th_holds f1) - (! u2 (th_holds (impl f1 f2)) + (! u2 (th_holds (impl f1 f2)) (th_holds f2)))))) - + ;; iff elimination (declare iff_elim_1 @@ -174,7 +174,7 @@ (! f2 formula (! u1 (th_holds (iff f1 f2)) (th_holds (impl f1 f2)))))) - + (declare iff_elim_2 (! f1 formula (! f2 formula @@ -204,7 +204,7 @@ (! u1 (th_holds a) (! u2 (th_holds (ifte a b c)) (th_holds b))))))) - + (declare ite_elim_2 (! a formula (! b formula @@ -212,7 +212,7 @@ (! u1 (th_holds (not a)) (! u2 (th_holds (ifte a b c)) (th_holds c))))))) - + (declare ite_elim_3 (! a formula (! b formula @@ -220,7 +220,7 @@ (! u1 (th_holds (not b)) (! u2 (th_holds (ifte a b c)) (th_holds c))))))) - + (declare ite_elim_2n (! a formula (! b formula @@ -236,7 +236,7 @@ (! u1 (th_holds a) (! u2 (th_holds (not (ifte a b c))) (th_holds (not b)))))))) - + (declare not_ite_elim_2 (! a formula (! b formula @@ -244,7 +244,7 @@ (! u1 (th_holds (not a)) (! u2 (th_holds (not (ifte a b c))) (th_holds (not c)))))))) - + (declare not_ite_elim_3 (! a formula (! b formula @@ -252,7 +252,7 @@ (! u1 (th_holds b) (! u2 (th_holds (not (ifte a b c))) (th_holds (not c)))))))) - + (declare not_ite_elim_2n (! a formula (! b formula @@ -260,9 +260,9 @@ (! u1 (th_holds a) (! u2 (th_holds (not (ifte (not a) b c))) (th_holds (not c)))))))) - - - + + + ;; How to do CNF for disjunctions of theory literals. ;; ;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))). @@ -287,7 +287,7 @@ ;; (contra _ ;; (or_elim_1 _ _ l{n-1} ;; ... -;; (or_elim_1 _ _ l2 +;; (or_elim_1 _ _ l2 ;; (or_elim_1 _ _ l1 A))))) ln) ;; ;;))))))) (\ C @@ -305,9 +305,9 @@ ;;(clausify_false ;; ;; (contra _ l3 -;; (or_elim_1 _ _ l2 +;; (or_elim_1 _ _ l2 ;; (or_elim_1 _ _ (not_not_intro l1) A)))) ;; ;;))))))) (\ C ;; -;; C should be the clause (~v1 V v2 V ~v3 )
\ No newline at end of file +;; C should be the clause (~v1 V v2 V ~v3 ) |