diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-01 08:44:21 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-01 10:44:21 -0500 |
commit | 9ce4c3153d42bc079470b7bd73bf131499b3fcbe (patch) | |
tree | 40a384f74915e2c009bb2a66bd0295e62edcfc2e /test/signatures/example-quant.plf | |
parent | 04154c08c1af81bb751376ae9379c071a95c5a3f (diff) |
Add testing infrastructure for LFSC signatures (#4678)
This commit adds testing infrastructure for LFSC signatures that is
enabled when CVC4 is configured with LFSC. The testing infrastructure
adopts run_test.py from https://github.com/CVC4/LFSC with minor
modifications (mainly adding support for a list of include directories
that are searched to resolve *.plf dependencies). The commit uses the
existing examples and test files from proofs/signatures as the initial
set of tests.
Co-authored-by: Alex Ozdemir aozdemir@hmc.edu
Diffstat (limited to 'test/signatures/example-quant.plf')
-rw-r--r-- | test/signatures/example-quant.plf | 95 |
1 files changed, 95 insertions, 0 deletions
diff --git a/test/signatures/example-quant.plf b/test/signatures/example-quant.plf new file mode 100644 index 000000000..611fd182c --- /dev/null +++ b/test/signatures/example-quant.plf @@ -0,0 +1,95 @@ +; Deps: sat.plf smt.plf th_base.plf th_quant.plf + +; -------------------------------------------------------------------------------- +; literals : +; L1 : forall x. x != x +; L2 : t = t + +; input : +; L1 + +; (instantiation) lemma : +; L1 => L2 + +; theory conflicts : +; ~L2 + + +; With the theory lemma, the input is unsatisfiable. +; -------------------------------------------------------------------------------- + + +; (0) -------------------- term declarations ----------------------------------- + +(check +(% s sort +(% t (term s) + + +; (1) -------------------- input formula ----------------------------------- + +(% x (term s) +(% A1 (th_holds (forall _ x (not (= _ x x)))) + + + +; (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 ...) + + +; instantiation lemma +(inst _ _ _ t (not (= _ t t)) A1 (\ A2 + + + + +; (4) -------------------- map theory literals to boolean variables +; --- maps all theory literals involved in proof to boolean literals + +(decl_atom (forall _ x (not (= _ x x))) (\ v1 (\ a1 +(decl_atom (= _ t t) (\ v2 (\ a2 + + + + +; (5) -------------------- theory conflicts --------------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(asf _ _ _ a2 (\ l2 +(clausify_false + + (contra _ (refl _ t) l2) + +))) (\ CT1 +; CT1 is the clause ( v2 ) + + +; (6) -------------------- clausification ----------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(ast _ _ _ a2 (\ l2 +(clausify_false + + (contra _ l2 A2) + +))) (\ C1 +; C1 is the clause ( ~v2 ) + + +; (7) -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ CT1 C1 v2) + +(\ x x)) + +)))))))))))))))))) |