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, 107 insertions, 107 deletions

diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf
index e66990de4..7b0b086dc 100755
--- a/proofs/signatures/th_base.plf
+++ b/proofs/signatures/th_base.plf
@@ -1,107 +1,107 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

-;

-; Atomization / Clausification

-;

-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

- 

-; binding between an LF var and an (atomic) formula

-(declare atom (! v var (! p formula type)))

-

-(declare decl_atom

-  (! f formula

-  (! u (! v var 

-       (! a (atom v f)

-         (holds cln)))

-    (holds cln))))

-    

-; direct clausify

-(declare clausify_form

-  (! f formula

-  (! v var

-  (! a (atom v f)

-  (! u (th_holds f)

-    (holds (clc (pos v) cln)))))))

-    

-(declare clausify_form_not

-  (! f formula

-  (! v var

-  (! a (atom v f)

-  (! u (th_holds (not f))

-    (holds (clc (neg v) cln)))))))

-

-(declare clausify_false

-  (! u (th_holds false)

-    (holds cln)))

-

-    

-(declare th_let_pf

-  (! f formula

-  (! u (th_holds f)

-  (! u2 (! v (th_holds f) (holds cln))

-    (holds cln)))))

-

-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

-;

-; Theory reasoning

-; - make a series of assumptions and then derive a contradiction (or false)

-; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"

-; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"

-;

-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

-

-(declare ast

-  (! v var

-  (! f formula

-  (! C clause

-  (! r (atom v f)       ;this is specified

-  (! u (! o (th_holds f)

-         (holds C))

-    (holds (clc (neg v) C))))))))

-

-(declare asf

-  (! v var

-  (! f formula

-  (! C clause

-  (! r (atom v f)

-  (! u (! o (th_holds (not f))

-         (holds C))

-    (holds (clc (pos v) C))))))))

-

-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

-;

-; Theory of Equality and Congruence Closure

-;

-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

-

-; temporary : 

-(declare trust (th_holds false))

-

-(declare refl

-  (! s sort

-  (! t (term s)

-    (th_holds (= s t t)))))

-

-(declare symm (! s sort

-              (! x (term s)

-              (! y (term s)

-              (! u (th_holds (= _ x y))

-                (th_holds (= _ y x)))))))

-

-(declare trans (! s sort

-               (! x (term s)

-               (! y (term s)

-               (! z (term s)

-               (! u (th_holds (= _ x y))

-               (! u (th_holds (= _ y z))

-                 (th_holds (= _ x z)))))))))

-

-(declare cong (! s1 sort

-              (! s2 sort

-              (! a1 (term (arrow s1 s2))

-              (! b1 (term (arrow s1 s2))

-              (! a2 (term s1)

-              (! b2 (term s1)

-              (! u1 (th_holds (= _ a1 b1))

-              (! u2 (th_holds (= _ a2 b2))

-                (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))

-                

+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Atomization / Clausification
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; binding between an LF var and an (atomic) formula
+(declare atom (! v var (! p formula type)))
+
+(declare decl_atom
+  (! f formula
+  (! u (! v var
+       (! a (atom v f)
+         (holds cln)))
+    (holds cln))))
+
+; direct clausify
+(declare clausify_form
+  (! f formula
+  (! v var
+  (! a (atom v f)
+  (! u (th_holds f)
+    (holds (clc (pos v) cln)))))))
+
+(declare clausify_form_not
+  (! f formula
+  (! v var
+  (! a (atom v f)
+  (! u (th_holds (not f))
+    (holds (clc (neg v) cln)))))))
+
+(declare clausify_false
+  (! u (th_holds false)
+    (holds cln)))
+
+
+(declare th_let_pf
+  (! f formula
+  (! u (th_holds f)
+  (! u2 (! v (th_holds f) (holds cln))
+    (holds cln)))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Theory reasoning
+; - make a series of assumptions and then derive a contradiction (or false)
+; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
+; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(declare ast
+  (! v var
+  (! f formula
+  (! C clause
+  (! r (atom v f)       ;this is specified
+  (! u (! o (th_holds f)
+         (holds C))
+    (holds (clc (neg v) C))))))))
+
+(declare asf
+  (! v var
+  (! f formula
+  (! C clause
+  (! r (atom v f)
+  (! u (! o (th_holds (not f))
+         (holds C))
+    (holds (clc (pos v) C))))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Theory of Equality and Congruence Closure
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; temporary :
+(declare trust (th_holds false))
+
+(declare refl
+  (! s sort
+  (! t (term s)
+    (th_holds (= s t t)))))
+
+(declare symm (! s sort
+              (! x (term s)
+              (! y (term s)
+              (! u (th_holds (= _ x y))
+                (th_holds (= _ y x)))))))
+
+(declare trans (! s sort
+               (! x (term s)
+               (! y (term s)
+               (! z (term s)
+               (! u (th_holds (= _ x y))
+               (! u (th_holds (= _ y z))
+                 (th_holds (= _ x z)))))))))
+
+(declare cong (! s1 sort
+              (! s2 sort
+              (! a1 (term (arrow s1 s2))
+              (! b1 (term (arrow s1 s2))
+              (! a2 (term s1)
+              (! b2 (term s1)
+              (! u1 (th_holds (= _ a1 b1))
+              (! u2 (th_holds (= _ a2 b2))
+                (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))
+