Fix a memory leak in LFSC proof checker. Largest QF_UF proof from Morgan (problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory. Add example test proof.

1 files changed, 68 insertions, 0 deletions

diff --git a/proofs/signatures/ex-mem.plf b/proofs/signatures/ex-mem.plf
new file mode 100755
index 000000000..12c4c3e16
--- /dev/null
+++ b/proofs/signatures/ex-mem.plf
@@ -0,0 +1,68 @@
+; AJR : proof used for testing memory use of theory lemmas
+
+(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 a))
+(% A3 (th_holds (not (= s a a)))
+
+; ------------------- 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 a) (\ v2 (\ a2
+(decl_atom (= s a a) (\ v3 (\ a3
+
+; --------------------------- proof of theory lemma ---------------------------------------------
+
+(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3  (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT1
+(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3  (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT2
+(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3  (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT3
+;...add copies here...
+
+; -------------------- 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))
+
+)))))))))))))))))))))))))))))
+))