diff options
Diffstat (limited to 'test/signatures/example-arrays.plf')
-rw-r--r-- | test/signatures/example-arrays.plf | 139 |
1 files changed, 139 insertions, 0 deletions
diff --git a/test/signatures/example-arrays.plf b/test/signatures/example-arrays.plf new file mode 100644 index 000000000..0e840274f --- /dev/null +++ b/test/signatures/example-arrays.plf @@ -0,0 +1,139 @@ +; Deps: sat.plf smt.plf th_base.plf th_arrays.plf + +; -------------------------------------------------------------------------------- +; literals : +; L1 : a = write( a, i, read( a, i ) +; L2 : read( a, k ) = read( write( a, i, read( a, i ) ), k ) +; L3 : i = k + +; input : +; ~L1 + +; (extenstionality) lemma : +; L1 or ~L2 + +; theory conflicts : +; L2 or ~L3 +; L2 or L3 + + +; With the theory lemma, the input is unsatisfiable. +; -------------------------------------------------------------------------------- + + +; (0) -------------------- term declarations ----------------------------------- + +(check +(% I sort +(% E sort +(% a (term (Array I E)) +(% i (term I) + + +; (1) -------------------- input formula ----------------------------------- + +(% A1 (th_holds (not (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))) + + + + +; (2) ------------------- specify that the following is a proof of the empty clause ----------------- + +(: (holds cln) + + + + +; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF ----------------- +; --- these should introduce (th_holds ...) + + +; extensionality lemma : notice this also introduces skolem k +(ext _ _ a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)) (\ k (\ A2 + + + + +; (4) -------------------- map theory literals to boolean variables +; --- maps all theory literals involved in proof to boolean literals + +(decl_atom (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1 +(decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2 +(decl_atom (= I i k) (\ v3 (\ a3 + + + +; (5) -------------------- theory conflicts --------------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(asf _ _ _ a3 (\ l3 +(asf _ _ _ a2 (\ l2 +(clausify_false + + ; use read over write rule "row" + (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2) + +))))) (\ CT1 +; CT1 is the clause ( v2 V v3 ) + +(satlem _ _ +(ast _ _ _ a3 (\ l3 +(asf _ _ _ a2 (\ l2 +(clausify_false + + ; use read over write rule "row1" + (contra _ (symm _ _ _ + (trans _ _ _ _ + (symm _ _ _ (cong _ _ _ _ _ _ + (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))) + l3)) + (trans _ _ _ _ + (row1 _ _ a i (apply _ _ (apply _ _ (read I E) a) i)) + (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3) + ))) + l2) + +))))) (\ CT2 +; CT2 is the clause ( v2 V ~v3 ) + + +; (6) -------------------- clausification ----------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(ast _ _ _ a1 (\ l1 +(clausify_false + +; input formula A1 is ( ~a1 ) +; the following is a proof of a1 ^ ( ~a1 ) => false + + (contra _ l1 A1) + +))) (\ C1 +; C1 is the clause ( ~v1 ) + + +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(ast _ _ _ a2 (\ l2 +(clausify_false + +; lemma A2 is ( a1 V ~a2 ) +; the following is a proof of ~a1 ^ a2 ^ ( a1 V ~a2 ) => false + + (contra _ l2 (or_elim_1 _ _ l1 A2)) + +))))) (\ C2 +; C2 is the clause ( v1 V ~v2 ) + + +; (7) -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ (R _ _ CT1 CT2 v3) (R _ _ C2 C1 v1) v2) + +(\ x x)) + +))))))))))))))))))))))))))) |