From: ajreynol Date: Fri, 8 Aug 2014 12:13:49 +0000 (+0200) Subject: Add draft of BV proof signature (incomplete) and example proof. X-Git-Tag: cvc5-1.0.0~6672 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=90217b1d4662c536ba5b3e05f28b1ae636c54342;p=cvc5.git Add draft of BV proof signature (incomplete) and example proof. --- diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf new file mode 100755 index 000000000..86e094efe --- /dev/null +++ b/proofs/signatures/ex_bv.plf @@ -0,0 +1,73 @@ +; a = b ^ a = 00000 ^ b = 11111 is UNSAT + +(check +(% a var_bv +(% b var_bv +(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b))) +(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn)))))))) +(% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn)))))))) +(: (holds cln) + +(decl_bv_atom_var 5 a (\ bv1 (\ ba1 +(decl_bv_atom_var 5 b (\ bv2 (\ ba2 +(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bv3 (\ ba3 +(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bv4 (\ ba4 + +(decl_atom (bblast bv1 4) (\ v1 (\ a1 +(decl_atom (bblast bv2 4) (\ v2 (\ a2 +(decl_atom (bblast bv3 4) (\ v3 (\ a3 +(decl_atom (bblast bv4 4) (\ v4 (\ a4 + +; bitblasting +(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba1 ba2 f1) (\ bf1 +(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba1 ba3 f2) (\ bf2 +(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba2 ba4 f3) (\ bf3 +(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bf4 +(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bf5 + +; CNFication +; a.4 V ~b.4 +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(ast _ _ _ a2 (\ l2 +(clausify_false + (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ bf1))) l1) +))))) (\ C2 + +; ~a.4 V 00000.4 +(satlem _ _ +(ast _ _ _ a1 (\ l1 +(asf _ _ _ a3 (\ l3 +(clausify_false + (contra _ (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ bf2))) l3) +))))) (\ C3 + +; b.4 V ~11111.4 +(satlem _ _ +(asf _ _ _ a2 (\ l2 +(ast _ _ _ a4 (\ l4 +(clausify_false + (contra _ (impl_elim _ _ l4 (iff_elim_2 _ _ (and_elim_1 _ _ bf3))) l2) +))))) (\ C6 + +; ~00000.4 +(satlem _ _ +(ast _ _ _ a3 (\ l3 +(clausify_false + (contra _ l3 (and_elim_1 _ _ bf4)) +))) (\ C7 + +; 11111.4 +(satlem _ _ +(asf _ _ _ a4 (\ l4 +(clausify_false + (contra _ (and_elim_1 _ _ bf5) l4) +))) (\ C8 + + +(satlem_simplify _ _ _ +(R _ _ + (R _ _ (R _ _ C8 C6 v4) C2 v2) + (R _ _ C3 C7 v3) v1) (\ x x)) + +))))))))))))))))))))))))))))))))))))))))))))))))))) \ No newline at end of file diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf new file mode 100755 index 000000000..8c972accf --- /dev/null +++ b/proofs/signatures/th_bv.plf @@ -0,0 +1,125 @@ +;a = b ^ a = 0 ^ b = 1 + +; "bitvec" is a term of type "sort" +(declare BitVec sort) + +; bit type +(declare bit type) +(declare b0 bit) +(declare b1 bit) + +; bit vector type +(declare bv type) +(declare bvn bv) +(declare bvc (! b bit (! v bv bv))) +; a bv constant term +(declare a_bv (! v bv (term BitVec))) + +; calculate the length of a bitvector +(program bv_len ((v bv)) mpz + (match v + (bvn 0) + ((bvc b v') (mp_add (bv_len v') 1)))) + +; a bv variable +(declare var_bv type) +; a bv variable term +(declare a_var_bv (! v var_bv (term BitVec))) + + + +; bit vector operators +(define bvoper (! x (term BitVec) + (! y (term BitVec) + (term BitVec)))) +(declare bvand bvoper) +(declare bvadd bvoper) +;.... + +; variable used for bit-blasting (must be simply-typed) +(declare bbl_var type) + +; all bit-vector terms are mapped with "bv_atom" to: +; - a simply-typed term of type "bbl_var", which is used for bit-blasting +; - a integer size +(declare bv_atom (! x (term BitVec) (! y bbl_var (! n mpz type)))) + +(declare decl_bv_atom_var (! n mpz ; must be specified + (! x var_bv + (! p (! w bbl_var + (! u (bv_atom (a_var_bv x) w n) + (holds cln))) + (holds cln))))) + +(declare decl_bv_atom_const (! n mpz + (! v bv + (! s (^ (bv_len v) n) + (! p (! w bbl_var + (! u (bv_atom (a_bv v) w n) + (holds cln))) + (holds cln)))))) + + +; a predicate to represent the n^th bit of a bitvector term +(declare bblast (! x bbl_var (! n mpz formula))) + +; bit blast constant +(program bblast_const ((x bbl_var) (v bv) (n mpz)) formula + (match v + (bvn (mp_ifneg n true (fail formula))) + ((bvc b v') (let n' (mp_add n (~ 1)) + (let f (match b (b0 (not (bblast x n))) (b1 (bblast x n))) + (mp_ifzero n' f (and f (bblast_const x v' n')))))))) + +(declare bv_bbl_const (! n mpz + (! f formula + (! v bv + (! x bbl_var + (! u (bv_atom (a_bv v) x n) + (! c (^ (bblast_const x v (mp_add n (~ 1))) f) + (th_holds f)))))))) + +; bit blast x = y +(program bblast_eq ((x bbl_var) (y bbl_var) (n mpz)) formula + (let n' (mp_add n (~ 1)) + (let f (iff (bblast x n) (bblast y n)) + (mp_ifzero n' f (and f (bblast_eq x y n')))))) + +(declare bv_bbl_eq (! x (term BitVec) + (! y (term BitVec) + (! n mpz + (! f formula + (! x' bbl_var + (! y' bbl_var + (! ux' (bv_atom x x' n) + (! uy' (bv_atom y y' n) + (! u (th_holds (= BitVec x y)) + (! c (^ (bblast_eq x' y' (mp_add n (~ 1))) f) + (th_holds f)))))))))))) + + +; rewrite rule : +; x + y = y + x +(declare bvadd_symm (! x (term BitVec) + (! y (term BitVec) + (! x' bbl_var + (! y' bbl_var + (! n mpz + (! ux (bv_atom x x' n) + (! uy (bv_atom y y' n) + (th_holds (= BitVec (bvadd x y) (bvadd y x))))))))))) + +(program calc_bvand ((a bv) (b bv)) bv + (match a + (bvn (match b (bvn bvn) (default (fail bv)))) + ((bvc ba a') (match b + ((bvc bb b') (bvc (match ba (b0 b0) (b1 bb)) (calc_bvand a' b'))) + (default (fail bv)))))) + +; rewrite rule (w constants) : +; a & b = c +(declare bvand_const (! c bv + (! a bv + (! b bv + (! u (^ (calc_bvand a b) c) + (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c)))))))) \ No newline at end of file