diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-19 09:03:18 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-19 09:03:33 -0500 |
commit | 3d645cc84b733042833d6617e5ccfac214e62a75 (patch) | |
tree | de89a7dca8c0cd0de642775925b18bb99cfd6f1b /proofs/signatures/ex-mem.plf | |
parent | f6ea27043d68169f392b30885f5b71eefe84e01e (diff) |
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.
Diffstat (limited to 'proofs/signatures/ex-mem.plf')
-rwxr-xr-x | proofs/signatures/ex-mem.plf | 68 |
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)) + +))))))))))))))))))))))))))))) +)) |