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

diff --git a/proofs/signatures/example.plf b/proofs/signatures/example.plf
index 5df1f31c3..ab690eb51 100755
--- a/proofs/signatures/example.plf
+++ b/proofs/signatures/example.plf
@@ -1,116 +1,116 @@
-; 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))

-

-))))))))))))))))))))))))))

-)
\ No newline at end of file
+; 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))
+
+))))))))))))))))))))))))))
+)