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

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 )