From: Andrew Reynolds Date: Thu, 13 Mar 2014 14:58:07 +0000 (-0500) Subject: Add working example of LFSC proof with quantifiers. Update quantifiers signature... X-Git-Tag: cvc5-1.0.0~7019 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b2c656543cc4ee7051ff00211a56f45331a763c;p=cvc5.git Add working example of LFSC proof with quantifiers. Update quantifiers signature to avoid dependent types in side condition. --- diff --git a/proofs/signatures/example-quant.plf b/proofs/signatures/example-quant.plf new file mode 100755 index 000000000..086633be9 --- /dev/null +++ b/proofs/signatures/example-quant.plf @@ -0,0 +1,95 @@ +; to check, run : lfsc sat.plf smt.plf th_base.plf example.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)) + +)))))))))))))))))) diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf index d18812380..98b53e43d 100755 --- a/proofs/signatures/th_quant.plf +++ b/proofs/signatures/th_quant.plf @@ -3,39 +3,69 @@ (! f formula formula)))) -(program instantiate ((f formula) (t term) (k term)) - (do (markvar t) - (let f1 (inst_f f t) - (do (markvar t) f1)))) +(program eqterm ((n1 term) (n2 term)) bool + (do (markvar n1) + (let s (ifmarked n2 tt ff) + (do (markvar n1) s)))) -(program instantiate_f ((f formula) (k term)) formula - (match f - ((and f1 f2) (and (instantiate_f f1 t) (instantiate_f f2 t))) - ((or f1 f2) (or (instantiate_f f1 t) (instantiate_f f2 t))) - ((impl f1 f2) (impl (instantiate_f f1 t) (instantiate_f f2 t))) - ((not f1) (not (instantiate_f f1 t))) - ((iff f1 f2) (iff (instantiate_f f1 t) (instantiate_f f2 t))) - ((xor f1 f2) (xor (instantiate_f f1 t) (instantiate_f f2 t))) - ((ifte f1 f2 f3) (ifte (instantiate_f f1 t) (instantiate_f f2 t) (instantiate_f f3 t))) - ((= s t1 t2) (= s (inst_t t1 t) (inst_t t2 t))) - ((forall t1 f1) (forall t1 (instantiate_f f1 t))) - (default f))) - -(program instantiate_t ((t term) (k term)) formula +(program is_inst_t ((ti term) (t term) (k term)) bool (match t - ((apply s1 s2 t1 t2) (apply s1 s2 t1 (instantiate_t t2 t))) - (default (ifmarked t k t)))) + ((apply s1 s2 t1 t2) + (match ti + ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff))) + (default ff))) + (default + (match ti + ((apply si1 si2 ti1 ti2) ff) + (default (eqterm ti (ifmarked t k t))))))) + +(program is_inst_f ((fi formula) (f formula) (k term)) bool + (match f + ((and f1 f2) (match fi + ((and fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff))) + (default ff))) + ((or f1 f2) (match fi + ((or fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff))) + (default ff))) + ((impl f1 f2) (match fi + ((impl fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff))) + (default ff))) + ((not f1) (match fi + ((not fi1) (is_inst_f fi1 f1 k)) + (default ff))) + ((iff f1 f2) (match fi + ((iff fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff))) + (default ff))) + ((xor f1 f2) (match fi + ((xor fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff))) + (default ff))) + ((ifte f1 f2 f3) (match fi + ((ifte fi1 fi2 fi3) (match (is_inst_f fi1 f1 k) + (tt (match (is_inst_f fi2 f2 k) (tt (is_inst_f fi3 f3 k)) (ff ff))) + (ff ff))) + (default ff))) + ((= s t1 t2) (match fi + ((= s ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff))) + (default ff))) + ((forall s t1 f1) (match fi + ((forall s ti1 fi1) (is_inst_f fi1 f1 k)) + (default ff))) + (default ff))) +(program is_inst ((fi formula) (f formula) (t term) (k term)) bool + (do (markvar t) + (let f1 (is_inst_f fi f k) + (do (markvar t) f1)))) (declare skolem (! s sort (! t (term s) (! f formula (! p (th_holds (not (forall s t f))) - (! u (! f1 formula - (! k (term s) - (! r (^ (instantiate f t k) f1) - (! p1 (th_holds (not f1)) + (! u (! k (term s) + (! fi formula + (! p1 (th_holds (not fi)) + (! r (^ (is_inst fi f t k) tt) (holds cln))))) (holds cln))))))) @@ -43,10 +73,10 @@ (! s sort (! t (term s) (! f formula - (! f1 formula - (! p (th_holds (forall s t f)) (! k (term s) - (! r (^ (instantiate f t k) f1) - (! u (! p1 (th_holds f1) + (! fi formula + (! p (th_holds (forall s t f)) + (! r (^ (is_inst fi f t k) tt) + (! u (! p1 (th_holds fi) (holds cln)) (holds cln)))))))))) \ No newline at end of file