diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /proofs/signatures | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'proofs/signatures')
-rw-r--r-- | proofs/signatures/Makefile.am | 2 | ||||
-rw-r--r-- | proofs/signatures/core_rewrites.plf | 123 | ||||
-rwxr-xr-x | proofs/signatures/ex-mem.plf | 16 | ||||
-rw-r--r--[-rwxr-xr-x] | proofs/signatures/ex_bv.plf | 43 | ||||
-rw-r--r-- | proofs/signatures/ex_bv_rewrite.plf | 41 | ||||
-rwxr-xr-x | proofs/signatures/sat.plf | 12 | ||||
-rwxr-xr-x | proofs/signatures/smt.plf | 94 | ||||
-rwxr-xr-x | proofs/signatures/th_arrays.plf | 2 | ||||
-rw-r--r--[-rwxr-xr-x] | proofs/signatures/th_bv.plf | 287 | ||||
-rw-r--r-- | proofs/signatures/th_bv_bitblast.plf | 629 |
10 files changed, 1071 insertions, 178 deletions
diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am index 9e8063bf2..82d8c2caa 100644 --- a/proofs/signatures/Makefile.am +++ b/proofs/signatures/Makefile.am @@ -3,7 +3,7 @@ # add support for more theories, just list them here in the same order # you would to the LFSC proof-checker binary. # -CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf +CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf noinst_LTLIBRARIES = libsignatures.la diff --git a/proofs/signatures/core_rewrites.plf b/proofs/signatures/core_rewrites.plf new file mode 100644 index 000000000..ca2c1fa03 --- /dev/null +++ b/proofs/signatures/core_rewrites.plf @@ -0,0 +1,123 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;; Rewrite rules +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; t rewrites to t' +(declare rw_term + (! s sort + (! t (term s) + (! t' (term s) + type)))) + +(declare rw_formula + (! f formula + (! f' formula + type))) + + +(declare apply_rw_formula + (! f formula + (! f' formula + (! rw (rw_formula f f') + (! fh (th_holds f) + (th_holds f')))))) + + +;; Identity rewrite rules +(declare rw_term_id + (! s sort + (! t (term s) + (rw_term s t t)))) + +(declare rw_term_trans + (! s sort + (! t1 (term s) + (! t2 (term s) + (! t3 (term s) + (! rw12 (rw_term _ t1 t2) + (! rw23 (rw_term _ t2 t3) + (rw_term s t1 t3)))))))) + +;; rw_symmetry + +(declare rw_formula_trans + (! f1 formula + (! f2 formula + (! f3 formula + (! rw1 (rw_formula f1 f2) + (! rw2 (rw_formula f2 f3) + (rw_formula f1 f3))))))) + + +(declare rw_op1_id + (! s sort + (! a (term s) + (! a' (term s) + (! rw (rw_term _ a a') + (! op term_op1 + (rw_term _ (op _ a) (op _ a')))))))) + +(declare rw_op2_id + (! s sort + (! a (term s) + (! a' (term s) + (! b (term s) + (! b' (term s) + (! rw (rw_term _ a a') + (! rw (rw_term _ b b') + (! op term_op2 + (rw_term _ (op _ a b) (op _ a' b'))))))))))) + +(declare rw_pred1_id + (! s sort + (! a (term s) + (! a' (term s) + (! rw (rw_term _ a a') + (! op op_pred1 + (rw_formula (op _ a) (op _ a')))))))) + +(declare rw_pred2_id + (! s sort + (! a (term s) + (! a' (term s) + (! b (term s) + (! b' (term s) + (! rw (rw_term _ a a') + (! rw (rw_term _ b b') + (! op op_pred2 + (rw_formula (op _ a b) (op _ a' b'))))))))))) + +(declare rw_eq_id + (! s sort + (! a (term s) + (! a' (term s) + (! b (term s) + (! b' (term s) + (! rw (rw_term _ a a') + (! rw (rw_term _ b b') + (rw_formula (= s a b) (= s a' b')))))))))) + +(declare rw_formula_op1_id + (! f formula + (! f' formula + (! frw (rw_formula f f') + (! op formula_op1 + (rw_formula (op f) (op f'))))))) + +(declare rw_formula_op2_id + (! f1 formula + (! f1' formula + (! f2 formula + (! f2' formula + (! frw1 (rw_formula f1 f1') + (! frw2 (rw_formula f2 f2') + (! op formula_op2 + (rw_formula (op f1 f2) (op f1' f2')))))))))) + + +(apply_rw_formula + (! f formula + (! f' formula + (! r (rw_formula f f') + (! h (th_holds f) + (th_holds f'))))))
\ No newline at end of file diff --git a/proofs/signatures/ex-mem.plf b/proofs/signatures/ex-mem.plf index 12c4c3e16..7e143c5b6 100755 --- a/proofs/signatures/ex-mem.plf +++ b/proofs/signatures/ex-mem.plf @@ -1,5 +1,3 @@ -; AJR : proof used for testing memory use of theory lemmas - (check (% s sort (% a (term s) @@ -10,8 +8,8 @@ ; -------------------- declaration of input formula ----------------------------------- (% A1 (th_holds (= s a b)) -(% A2 (th_holds (= s b a)) -(% A3 (th_holds (not (= s a a))) +(% A2 (th_holds (= s b c)) +(% A3 (th_holds (not (= s a c))) ; ------------------- specify that the following is a proof of the empty clause ----------------- @@ -20,15 +18,12 @@ ; ---------- 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 +(decl_atom (= s b c) (\ v2 (\ a2 +(decl_atom (= s a c) (\ 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 ----------------------------------------- @@ -64,5 +59,4 @@ (\ x x)) -))))))))))))))))))))))))))))) -)) +))))))))))))))))))))))))))) diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf index ae585e455..58494e793 100755..100644 --- a/proofs/signatures/ex_bv.plf +++ b/proofs/signatures/ex_bv.plf @@ -1,31 +1,32 @@ -; a = b ^ a = 00000 ^ b = 11111 is UNSAT +; (a = b) ^ (a = b & 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)))))))) +(% f1 (th_holds (= (BitVec 4) (a_var_bv _ a) (a_var_bv _ b))) +(% f2 (th_holds (= (BitVec 4) (a_var_bv _ a) (bvand 4 (a_var_bv 4 b) (a_bv _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))) +(% f3 (th_holds (= (BitVec 4) (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 (\ ba1 -(decl_bv_atom_var 5 b (\ ba2 -(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3 -(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4 +;; (decl_bv_term_var 5 a (\ ba1 +;; (decl_bv_term_var 5 b (\ ba2 +;; (decl_bv_term_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3 +;; (decl_bv_term_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4 -(decl_atom (bblast a 4) (\ v1 (\ a1 -(decl_atom (bblast b 4) (\ v2 (\ a2 +(decl_atom (bitof a 4) (\ v1 (\ a1 +(decl_atom (bitof b 4) (\ v2 (\ a2 ; bitblasting terms -(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1 -(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2 -(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3 -(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4 +(decl_bblast _ _ _ (bv_bbl_var 4 a _ ) (\ bt1 +(decl_bblast _ _ _ (bv_bbl_var 4 b _ ) (\ bt2 +(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bt3 +(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bt4 +(decl_bblast _ _ _ (bv_bbl_bvand 4 _ _ _ _ _ bt1 bt3) (\ bt5 ; bitblasting formulas -(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1 -(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ bf2 -(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt2 bt4) (\ bf3 +(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ bt1 bt2) (\ bf1 +(th_let_pf _ (bv_bbl_bvult _ _ _ _ _ _ bt1 bt5) (\ bf2 +(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ bt2 bt4) (\ bf3 ; CNFication ; a.4 V ~b.4 @@ -33,25 +34,25 @@ (asf _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (clausify_false - (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f1 bf1)))) l1) ; notice at the intermost we impl_elim, which converts from atom to bit-blasting representation + trust ))))) (\ C2 ; ~a.4 (satlem _ _ (ast _ _ _ a1 (\ l1 (clausify_false - (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2)))) + trust ))) (\ C3 ; b.4 (satlem _ _ (asf _ _ _ a2 (\ l2 (clausify_false - (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2) + trust ))) (\ C6 (satlem_simplify _ _ _ (R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x)) -)))))))))))))))))))))))))))))))))))))))))))
\ No newline at end of file +))))))))))))))))))))))))))))))))))))))))))))) diff --git a/proofs/signatures/ex_bv_rewrite.plf b/proofs/signatures/ex_bv_rewrite.plf new file mode 100644 index 000000000..fbe593502 --- /dev/null +++ b/proofs/signatures/ex_bv_rewrite.plf @@ -0,0 +1,41 @@ +(check +(% x var_bv +(% y var_bv +(% a var_bv +(% A0 (th_holds true) +(% A1 (th_holds + (= (BitVec 1) (a_var_bv 1 x) + (bvnot 1 (bvxnor 1 (bvxor 1 (a_var_bv 1 a) (a_bv 1 (bvc b1 bvn))) + (bvxor 1 (a_var_bv 1 a) (a_bv 1 (bvc b0 bvn))) )))) +(: (th_holds + (= (BitVec 1) (a_var_bv 1 x) + (bvxor 1 (bvnot 1 (a_var_bv 1 a)) (a_var_bv 1 a)))) + +;; print rewritten assertions + +(@ ones (a_bv 1 (bvc b1 bvn)) +(@ zero (a_bv 1 (bvc b0 bvn)) +(@ xorone (bvxor 1 (a_var_bv 1 a) ones) +(@ xorzero (bvxor 1 (a_var_bv 1 a) zero) +(@ t1 (bvxor 1 xorone xorzero) +(@ t2 (bvxnor 1 xorone xorzero) +(@ t3 (bvnot 1 t2) +(@ t4 (bvnot 1 t1) +(@ t5 (bvxor 1 (bvnot 1 (a_var_bv 1 a)) (a_var_bv 1 a)) +;; adding identity rewrite proofs +(@ xor_onerw (rw_term_id 1 xorone) +(@ xor_zerorw (rw_term_id 1 xorzero) +(@ rw1 (xnor_elim 1 _ _ _ _ xor_onerw xor_zerorw) ;; bvxnor t1 t2 -> bvnot (bvxor t1 t2) +(@ rw2 (xor_zero 1 _ _ _ _ (rw_term_id 1 (a_var_bv 1 a)) (rw_term_id 1 zero)) +(@ rw3 (xor_one 1 _ _ _ _ (rw_term_id 1 (a_var_bv 1 a)) (rw_term_id 1 ones)) +(@ rw4 (rw_bvop2_id 1 _ _ _ _ rw3 rw2 bvxor) ;; bvxor t1 t2 -> bvxor t1' t2' +(@ rw5 (rw_bvop1_id 1 _ _ rw4 bvnot) ;; bvnot (bvxor t1 t2) -> bvnot (bvxor t1' t2') +(@ rw6 (rw_term_trans 1 _ _ _ rw1 rw5) ;; bvxnor t1 t2 -> bvnot (bvxor t1' t2') +(@ rw7 (rw_bvop1_id 1 _ _ rw6 bvnot) ;; (bvnot (bvxnor t1 t2)) ->(bvnot (bvnot (bvxor t1' t2'))) +(@ rw8 (not_idemp 1 _ _ (rw_term_id 1 t5)) ;; (bvnot (bvnot (bvxor t1' t2'))) -> bvxor t1' t2' +(@ rw9 (rw_term_trans 1 _ _ _ rw7 rw8) ;; (bvnot (bvxnor t1 t2)) -> (bvxor t1' t2') +(@ rw10 (rw_term_id 1 (a_var_bv 1 x)) +(@ rw11 (rw_eq_id 1 _ _ _ _ rw10 rw9) ;; x = t1 => x = t' +(apply_rw_formula _ _ rw11 A1) + +)))))))))))))))))))))))))))))
\ No newline at end of file diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf index 5e2f1cc44..b95caa8fd 100755 --- a/proofs/signatures/sat.plf +++ b/proofs/signatures/sat.plf @@ -14,7 +14,7 @@ ; constructs for general clauses for R, Q, satlem -(declare concat (! c1 clause (! c2 clause clause))) +(declare concat_cl (! c1 clause (! c2 clause clause))) (declare clr (! l lit (! c clause clause))) ; code to check resolutions @@ -49,7 +49,7 @@ (match m (tt (do (ifmarked4 v v (markvar4 v)) c')) (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c'))))))))) - ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2))) + ((concat_cl c1 c2) (append (simplify_clause c1) (simplify_clause c2))) ((clr l c1) (match l ; set mark 1 to indicate we should remove v, and fail if @@ -81,14 +81,14 @@ (! u1 (holds c1) (! u2 (holds c2) (! n var - (holds (concat (clr (pos n) c1) + (holds (concat_cl (clr (pos n) c1) (clr (neg n) c2))))))))) (declare Q (! c1 clause (! c2 clause (! u1 (holds c1) (! u2 (holds c2) (! n var - (holds (concat (clr (neg n) c1) + (holds (concat_cl (clr (neg n) c1) (clr (pos n) c2))))))))) (declare satlem_simplify @@ -115,13 +115,13 @@ ; ; (check ; (% v1 var -; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln)))))) +; (% u1 (holds (concat_cl (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln)))))) ; (clc (pos v1) (clc (pos v1) cln)))) ; (satlem _ _ _ u1 (\ x x)))))) ;(check ; (% v1 var -; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln) +; (% u1 (holds (clr (neg v1) (concat_cl (clc (neg v1) cln) ; (clr (neg v1) (clc (neg v1) cln))))) ; (satlem _ _ _ u1 (\ x x)))))) diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 62cdf3f94..fa89a457f 100755 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -11,13 +11,29 @@ ; standard logic definitions (declare true formula) (declare false formula) -(declare not (! f formula formula)) -(declare and (! f1 formula (! f2 formula formula))) -(declare or (! f1 formula (! f2 formula formula))) -(declare impl (! f1 formula (! f2 formula formula))) -(declare iff (! f1 formula (! f2 formula formula))) -(declare xor (! f1 formula (! f2 formula formula))) -(declare ifte (! b formula (! f1 formula (! f2 formula formula)))) + +(define formula_op1 + (! f formula + formula)) + +(define formula_op2 + (! f1 formula + (! f2 formula + formula))) + +(define formula_op3 + (! f1 formula + (! f2 formula + (! f3 formula + formula)))) + +(declare not formula_op1) +(declare and formula_op2) +(declare or formula_op2) +(declare impl formula_op2) +(declare iff formula_op2) +(declare xor formula_op2) +(declare ifte formula_op3) ; terms (declare sort type) @@ -46,6 +62,19 @@ (declare Bool sort) ; the special sort for predicates (declare p_app (! x (term Bool) formula)) ; propositional application of term +; boolean terms +(declare t_true (term Bool)) +(declare t_false (term Bool)) +(declare t_t_neq_f + (th_holds (not (= Bool t_true t_false)))) +(declare pred_eq_t + (! x (term Bool) + (! u (th_holds (p_app x)) + (th_holds (= Bool x t_true))))) +(declare pred_eq_f + (! x (term Bool) + (! u (th_holds (not (p_app x))) + (th_holds (= Bool x t_false))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; @@ -54,8 +83,12 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; binding between an LF var and an (atomic) formula + (declare atom (! v var (! p formula type))) +; binding between two LF vars +(declare bvatom (! sat_v var (! bv_v var type))) + (declare decl_atom (! f formula (! u (! v var @@ -63,6 +96,19 @@ (holds cln))) (holds cln)))) +;; declare atom enhanced with mapping +;; between SAT prop variable and BVSAT prop variable +(declare decl_bvatom + (! f formula + (! u (! v var + (! bv_v var + (! a (atom v f) + (! bva (atom bv_v f) + (! vbv (bvatom v bv_v) + (holds cln)))))) + (holds cln)))) + + ; clausify a formula directly (declare clausify_form (! f formula @@ -88,13 +134,18 @@ (! u2 (! v (th_holds f) (holds cln)) (holds cln))))) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; ; Natural deduction rules : used for CNF ; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; for eager bit-blasting +(declare iff_symm + (! f formula + (th_holds (iff f f)))) + ;; contradiction @@ -291,8 +342,33 @@ (! u (! o (th_holds (not f)) (holds C)) (holds (clc (pos v) C)))))))) - +;; Bitvector lemma constructors to assume +;; the unit clause containing the assumptions +;; it also requires the mapping between bv_v and v +;; The resolution proof proving false will use bv_v as the definition clauses use bv_v +;; but the Problem clauses in the main SAT solver will use v so the learned clause is in terms of v +(declare bv_asf + (! v var + (! bv_v var + (! f formula + (! C clause + (! r (atom v f) ;; passed in + (! x (bvatom v bv_v) ; establishes the equivalence of v to bv_ + (! u (! o (holds (clc (neg bv_v) cln)) ;; l binding to be used in proof + (holds C)) + (holds (clc (pos v) C)))))))))) + +(declare bv_ast + (! v var + (! bv_v var + (! f formula + (! C clause + (! r (atom v f) ; this is specified + (! x (bvatom v bv_v) ; establishes the equivalence of v to bv_v + (! u (! o (holds (clc (pos bv_v) cln)) + (holds C)) + (holds (clc (neg v) C)))))))))) ;; Example: diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf index 0c6b16048..8334f51de 100755 --- a/proofs/signatures/th_arrays.plf +++ b/proofs/signatures/th_arrays.plf @@ -3,7 +3,7 @@ ; Theory of Arrays ; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; depdends on : th_base.plf +; depends on : th_base.plf ; sorts diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index 0fb50f8cf..c93541085 100755..100644 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -1,145 +1,174 @@ +;;;; TEMPORARY: + +(declare trust-bad (th_holds false)) + +; helper stuff +(program mpz_sub ((x mpz) (y mpz)) mpz + (mp_add x (mp_mul (~1) y))) + +(program mp_ispos ((x mpz)) formula + (mp_ifneg x false true)) + +(program mpz_eq ((x mpz) (y mpz)) formula + (mp_ifzero (mpz_sub x y) true false)) + +(program mpz_lt ((x mpz) (y mpz)) formula + (mp_ifneg (mpz_sub x y) true false)) + +(program mpz_lte ((x mpz) (y mpz)) formula + (mp_ifneg (mpz_sub x y) true (mpz_eq x y))) + +(program mpz_ ((x mpz) (y mpz)) formula + (mp_ifzero (mpz_sub x y) true false)) + + ; "bitvec" is a term of type "sort" -(declare BitVec sort) +; (declare BitVec sort) +(declare BitVec (!n mpz sort)) ; bit type (declare bit type) (declare b0 bit) (declare b1 bit) -; bit vector type +; bit vector type used for constants (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)))) +;; (program bv_len ((v bv)) mpz +;; (match v +;; (bvn 0) +;; ((bvc b v') (mp_add (bv_len v') 1)))) + + +; a bv constant term +(declare a_bv + (! n mpz + (! v bv + (term (BitVec n))))) + ; 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) -;.... - -; all bit-vector terms are mapped with "bv_atom" to: -; - a simply-typed term of type "var_bv", which is necessary for bit-blasting -; - a integer size -(declare bv_atom (! x (term BitVec) (! y var_bv (! n mpz type)))) - -(declare decl_bv_atom_var (! n mpz ; must be specified - (! x var_bv - (! p (! u (bv_atom (a_var_bv x) x n) - (holds cln)) - (holds cln))))) - -(declare decl_bv_atom_const (! n mpz - (! v bv - (! s (^ (bv_len v) n) - (! p (! w var_bv - (! u (bv_atom (a_bv v) w n) - (holds cln))) - (holds cln)))))) - - -; other terms here? - - -; bit blasted terms -(declare bblt type) -(declare bbltn bblt) -(declare bbltc (! f formula (! v bblt bblt))) - -; (bblast_term x y) means term x corresponds to bit level interpretation y -(declare bblast_term (! x (term BitVec) (! y bblt formula))) - -; a predicate to represent the n^th bit of a bitvector term -(declare bblast (! x var_bv (! n mpz formula))) - - -; bit blast constant -(program bblast_const ((v bv) (n mpz)) bblt - (mp_ifneg n (match v (bvn bbltn) - (default (fail bblt))) - (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1))))) - (default (fail bblt))))) - -(declare bv_bbl_const (! n mpz - (! v bv - (! x var_bv - (! f bblt - (! u (bv_atom (a_bv v) x n) - (! c (^ (bblast_const v (mp_add n (~ 1))) f) - (th_holds (bblast_term (a_bv v) f))))))))) - -; bit blast variable -(program bblast_var ((x var_bv) (n mpz)) bblt - (mp_ifneg n bbltn - (bbltc (bblast x n) (bblast_var x (mp_add n (~ 1)))))) - -(declare bv_bbl_var (! n mpz - (! x var_bv - (! f bblt - (! u (bv_atom (a_var_bv x) x n) - (! c (^ (bblast_var x (mp_add n (~ 1))) f) - (th_holds (bblast_term (a_var_bv x) f)))))))) - -; bit blast x = y -; for x,y of size n, it will return a conjuction (x.{n-1} = y.{n-1} ^ ( ... ^ (x.0 = y.0 ^ true))) -(program bblast_eq ((x bblt) (y bblt)) formula - (match x - (bbltn (match y (bbltn true) (default (fail formula)))) - ((bbltc fx x') (match y - (bbltn (fail formula)) - ((bbltc fy y') (and (iff fx fy) (bblast_eq x' y'))))))) - -(declare bv_bbl_eq (! x (term BitVec) - (! y (term BitVec) - (! fx bblt - (! fy bblt - (! f formula - (! ux (th_holds (bblast_term x fx)) - (! uy (th_holds (bblast_term y fy)) - (! c (^ (bblast_eq fx fy) f) - (th_holds (impl (= BitVec x y) f))))))))))) - - -; rewrite rule : -; x + y = y + x -(declare bvadd_symm (! x (term BitVec) - (! y (term BitVec) - (! x' var_bv - (! y' var_bv - (! n mpz - (! ux (bv_atom x x' n) - (! uy (bv_atom y y' n) - (th_holds (= BitVec (bvadd x y) (bvadd y x))))))))))) - - - -; necessary? -(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 +(declare a_var_bv + (! n mpz + (! v var_bv + (term (BitVec n))))) + +; bit vector binary operators +(define bvop2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (term (BitVec n)))))) + +(declare bvand bvop2) +(declare bvor bvop2) +(declare bvor bvop2) +(declare bvxor bvop2) +(declare bvnand bvop2) +(declare bvnor bvop2) +(declare bvxnor bvop2) +(declare bvmul bvop2) +(declare bvadd bvop2) +(declare bvsub bvop2) +(declare bvudiv bvop2) +(declare bvurem bvop2) +(declare bvsdiv bvop2) +(declare bvsrem bvop2) +(declare bvsmod bvop2) +(declare bvshl bvop2) +(declare bvlshr bvop2) +(declare bvashr bvop2) +(declare concat bvop2) + +; bit vector unary operators +(define bvop1 + (! n mpz + (! x (term (BitVec n)) + (term (BitVec n))))) + + +(declare bvneg bvop1) +(declare bvnot bvop1) +(declare rotate_left bvop1) +(declare rotate_right bvop1) + +(declare bvcomp + (! n mpz + (! t1 (term (BitVec n)) + (! t2 (term (BitVec n)) + (term (BitVec 1)))))) + + +(declare concat + (! n mpz + (! m mpz + (! m' mpz + (! t1 (term (BitVec m)) + (! t2 (term (BitVec m')) + (term (BitVec n)))))))) + +;; side-condition fails in signature only?? +;; (! s (^ (mp_add m m') n) + +;; (declare repeat bvopp) + +(declare extract + (! n mpz + (! i mpz + (! j mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n)))))))) + +(declare zero_extend + (! n mpz + (! i mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n))))))) + +(declare sign_extend + (! n mpz + (! i mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n))))))) + +(declare repeat + (! n mpz + (! i mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n))))))) + + + +;; TODO: add checks for valid typing for these operators +;; (! c1 (^ (mpz_lte i j) +;; (! c2 (^ (mpz_lt i n) true) +;; (! c3 (^ (mp_ifneg i false true) true) +;; (! c4 (^ (mp_ifneg j false true) true) +;; (! s (^ (mp_add (mpz_sub i j) 1) m) + + +; bit vector predicates +(define bvpred + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + formula)))) + +(declare bvult bvpred) +(declare bvule bvpred) +(declare bvugt bvpred) +(declare bvuge bvpred) +(declare bvslt bvpred) +(declare bvsle bvpred) +(declare bvsgt bvpred) +(declare bvsge bvpred) + diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf new file mode 100644 index 000000000..8e8c51857 --- /dev/null +++ b/proofs/signatures/th_bv_bitblast.plf @@ -0,0 +1,629 @@ +; bit blasted terms as list of formulas +(declare bblt type) +(declare bbltn bblt) +(declare bbltc (! f formula (! v bblt bblt))) + +; calculate the length of a bit-blasted term +(program bblt_len ((v bblt)) mpz + (match v + (bbltn 0) + ((bbltc b v') (mp_add (bblt_len v') 1)))) + + +; (bblast_term x y) means term y corresponds to bit level interpretation x +(declare bblast_term + (! n mpz + (! x (term (BitVec n)) + (! y bblt + type)))) + +; FIXME: for unsupported bit-blast terms +(declare trust_bblast_term + (! n mpz + (! x (term (BitVec n)) + (! y bblt + (bblast_term n x y))))) + + +(declare decl_bblast + (! n mpz + (! b bblt + (! t (term (BitVec n)) + (! bb (bblast_term n t b) + (! s (^ (bblt_len b) n) + (! u (! v (bblast_term n t b) (holds cln)) + (holds cln)))))))) + + +; a predicate to represent the n^th bit of a bitvector term +(declare bitof + (! x var_bv + (! n mpz formula))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; BITBLASTING RULES +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST CONSTANT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_const ((v bv) (n mpz)) bblt + (mp_ifneg n (match v (bvn bbltn) + (default (fail bblt))) + (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1))))) + (default (fail bblt))))) + +(declare bv_bbl_const (! n mpz + (! f bblt + (! v bv + (! c (^ (bblast_const v (mp_add n (~ 1))) f) + (bblast_term n (a_bv n v) f)))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST VARIABLE +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_var ((x var_bv) (n mpz)) bblt + (mp_ifneg n bbltn + (bbltc (bitof x n) (bblast_var x (mp_add n (~ 1)))))) + +(declare bv_bbl_var (! n mpz + (! x var_bv + (! f bblt + (! c (^ (bblast_var x (mp_add n (~ 1))) f) + (bblast_term n (a_var_bv n x) f)))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST CONCAT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_concat ((x bblt) (y bblt)) bblt + (match x + (bbltn (match y ((bbltc by y') (bbltc by (bblast_concat x y'))) + (bbltn bbltn))) + ((bbltc bx x') (bbltc bx (bblast_concat x' y))))) + + +(declare bv_bbl_concat (! n mpz + (! m mpz + (! m1 mpz + (! x (term (BitVec m)) + (! y (term (BitVec m1)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term m x xb) + (! ybb (bblast_term m1 y yb) + (! c (^ (bblast_concat xb yb ) rb) + (bblast_term n (concat n m m1 x y) rb))))))))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST EXTRACT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_extract_rec ((x bblt) (i mpz) (j mpz) (n mpz)) bblt + (match x + ((bbltc bx x') (mp_ifneg (mpz_sub (mpz_sub j n) 1) + (mp_ifneg (mpz_sub (mpz_sub n i) 1) + (bbltc bx (bblast_extract_rec x' i j (mpz_sub n 1))) + (bblast_extract_rec x' i j (mpz_sub n 1))) + + bbltn)) + (bbltn bbltn))) + +(program bblast_extract ((x bblt) (i mpz) (j mpz) (n mpz)) bblt + (bblast_extract_rec x i j (mpz_sub n 1))) + +(declare bv_bbl_extract (! n mpz + (! i mpz + (! j mpz + (! m mpz + (! x (term (BitVec m)) + (! xb bblt + (! rb bblt + (! xbb (bblast_term m x xb) + (! c ( ^ (bblast_extract xb i j m) rb) + (bblast_term n (extract n i j m x) rb))))))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST ZERO/SIGN EXTEND +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program extend_rec ((x bblt) (i mpz) (b formula)) bblt + (mp_ifneg i x + (bbltc b (extend_rec x (mpz_sub i 1) b))))) + +(program bblast_zextend ((x bblt) (i mpz)) bblt + (extend_rec x (mpz_sub i 1) false)) + +(declare bv_bbl_zero_extend (! n mpz + (! k mpz + (! m mpz + (! x (term (BitVec m)) + (! xb bblt + (! rb bblt + (! xbb (bblast_term m x xb) + (! c ( ^ (bblast_zextend xb k m) rb) + (bblast_term n (zero_extend n k m x) rb)))))))))) + + +(program bblast_sextend ((x bblt) (i mpz)) bblt + (match x (bbltn (fail bblt)) + ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb)))) + +(declare bv_bbl_sign_extend (! n mpz + (! k mpz + (! m mpz + (! x (term (BitVec m)) + (! xb bblt + (! rb bblt + (! xbb (bblast_term m x xb) + (! c ( ^ (bblast_sextend xb k m) rb) + (bblast_term n (sign_extend n k m x) rb)))))))))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVAND +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvand ((x bblt) (y bblt)) bblt + (match x + (bbltn (match y (bbltn bbltn) (default (fail bblt)))) + ((bbltc bx x') (match y + (bbltn (fail bblt)) + ((bbltc by y') (bbltc (and bx by) (bblast_bvand x' y'))))))) + + +(declare bv_bbl_bvand (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvand xb yb ) rb) + (bblast_term n (bvand n x y) rb))))))))))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVNOT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvnot ((x bblt)) bblt + (match x + (bbltn bbltn) + ((bbltc bx x') (bbltc (not bx) (bblast_bvnot x'))))) + + +(declare bv_bbl_bvnot (! n mpz + (! x (term (BitVec n)) + (! xb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! c (^ (bblast_bvnot xb ) rb) + (bblast_term n (bvnot n x) rb)))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVOR +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvor ((x bblt) (y bblt)) bblt + (match x + (bbltn (match y (bbltn bbltn) (default (fail bblt)))) + ((bbltc bx x') (match y + (bbltn (fail bblt)) + ((bbltc by y') (bbltc (or bx by) (bblast_bvor x' y'))))))) + + +(declare bv_bbl_bvor (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvor xb yb ) rb) + (bblast_term n (bvor n x y) rb))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVXOR +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvxor ((x bblt) (y bblt)) bblt + (match x + (bbltn (match y (bbltn bbltn) (default (fail bblt)))) + ((bbltc bx x') (match y + (bbltn (fail bblt)) + ((bbltc by y') (bbltc (xor bx by) (bblast_bvxor x' y'))))))) + + +(declare bv_bbl_bvxor (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvxor xb yb ) rb) + (bblast_term n (bvxor n x y) rb))))))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVADD +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; return the carry bit after adding x y +;; FIXME: not the most efficient thing in the world +(program bblast_bvadd_carry ((a bblt) (b bblt) (carry formula)) formula +(match a + ( bbltn (match b (bbltn carry) (default (fail formula)))) + ((bbltc ai a') (match b + (bbltn (fail formula)) + ((bbltc bi b') (or (and ai bi) (and (xor ai bi) (bblast_bvadd_carry a' b' carry)))))))) + +;; ripple carry adder where carry is the initial carry bit +(program bblast_bvadd ((a bblt) (b bblt) (carry formula)) bblt +(match a + ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) + ((bbltc ai a') (match b + (bbltn (fail bblt)) + ((bbltc bi b') (bbltc (xor (xor ai bi) (bblast_bvadd_carry a' b' carry)) + (bblast_bvadd a' b' carry))))))) + + +(declare bv_bbl_bvadd (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvadd xb yb false) rb) + (bblast_term n (bvadd n x y) rb))))))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVNEG +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_zero ((n mpz)) bblt +(mp_ifzero n bbltn + (bbltc false (bblast_zero (mp_add n (~1)))))) + +(program bblast_bvneg ((x bblt) (n mpz)) bblt + (bblast_bvadd (bblast_bvnot x) (bblast_zero n) true)) + + +(declare bv_bbl_bvneg (! n mpz + (! x (term (BitVec n)) + (! xb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! c (^ (bblast_bvneg xb n) rb) + (bblast_term n (bvneg n x) rb)))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVMUL +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;; shift add multiplier + +(program reverse_help ((x bblt) (acc bblt)) bblt +(match x + (bbltn acc) + ((bbltc xi x') (reverse_help x' (bbltc xi acc))))) + + +(program reverseb ((x bblt)) bblt + (reverse_help x bbltn)) + +;; (program concat ((a bblt) (b bblt)) bblt +;; (match a (bbltn b) +;; ((bbltc ai a') (bbltc ai (concat a' b))))) + + +(program top_k_bits ((a bblt) (k mpz)) bblt + (mp_ifzero k bbltn + (match a (bbltn (fail bblt)) + ((bbltc ai a') (bbltc ai (top_k_bits a' (mpz_sub k 1))))))) + +(program bottom_k_bits ((a bblt) (k mpz)) bblt + (reverseb (top_k_bits (reverseb a) k))) + +;; assumes the least signigicant bit is at the beginning of the list +(program k_bit ((a bblt) (k mpz)) formula +(mp_ifneg k (fail formula) +(match a (bbltn (fail formula)) + ((bbltc ai a') (mp_ifzero k ai (k_bit a' (mpz_sub k 1))))))) + +(program and_with_bit ((a bblt) (bt formula)) bblt +(match a (bbltn bbltn) + ((bbltc ai a') (bbltc (and bt ai) (and_with_bit a' bt))))) + +;; a is going to be the current result +;; carry is going to be false initially +;; b is the and of a and b[k] +;; res is going to be bbltn initially +(program mult_step_k_h ((a bblt) (b bblt) (res bblt) (carry formula) (k mpz)) bblt +(match a + (bbltn (match b (bbltn res) (default (fail bblt)))) + ((bbltc ai a') + (match b (bbltn (fail bblt)) + ((bbltc bi b') + (mp_ifneg (mpz_sub k 1) + (let carry_out (or (and ai bi) (and (xor ai bi) carry)) + (let curr (xor (xor ai bi) carry) + (mult_step_k_h a' b' (bbltc curr res) carry_out (mpz_sub k 1)))) + (mult_step_k_h a' b (bbltc ai res) carry (mpz_sub k 1)) +)))))) + +;; assumes that a, b and res have already been reversed +(program mult_step ((a bblt) (b bblt) (res bblt) (n mpz) (k mpz)) bblt +(let k' (mpz_sub n k ) +(let ak (top_k_bits a k') +(let b' (and_with_bit ak (k_bit b k)) + (mp_ifzero (mpz_sub k' 1) + (mult_step_k_h res b' bbltn false k) + (let res' (mult_step_k_h res b' bbltn false k) + (mult_step a b (reverseb res') n (mp_add k 1)))))))) + + +(program bblast_bvmul ((a bblt) (b bblt) (n mpz)) bblt +(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +(let br (reverseb b) ;; from the least significant bit up +(let res (and_with_bit ar (k_bit br 0)) + (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step + res + (mult_step ar br res n 1)))))) + +(declare bv_bbl_bvmul (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvmul xb yb n) rb) + (bblast_term n (bvmul n x y) rb))))))))))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST EQUALS +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; bit blast x = y +; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1}))) +; f is the accumulator formula that builds the equality in the right order +(program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula + (match x + (bbltn (match y (bbltn f) (default (fail formula)))) + ((bbltc fx x') (match y + (bbltn (fail formula)) + ((bbltc fy y') (bblast_eq_rec x' y' (and (iff fx fy) f))))) + (default (fail formula)))) + +(program bblast_eq ((x bblt) (y bblt)) formula + (match x + ((bbltc bx x') (match y ((bbltc by y') (bblast_eq_rec x' y' (iff bx by))) + (default (fail formula)))) + (default (fail formula)))) + +(declare bv_bbl_= + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) x y) f)))))))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVULT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvult ((x bblt) (y bblt) (n mpz)) formula +(match x + ( bbltn (fail formula)) + ((bbltc xi x') (match y + (bbltn (fail formula)) + ((bbltc yi y') (mp_ifzero n + (and (not xi) yi) + (or (and (iff xi yi) (bblast_bvult x' y' (mp_add n (~1)))) (and (not xi) yi)))))))) + +(declare bv_bbl_bvult + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvult bx by (mp_add n (~1))) f) + (th_holds (iff (bvult n x y) f)))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVSLT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvslt ((x bblt) (y bblt) (n mpz)) formula +(match x + ( bbltn (fail formula)) + ((bbltc xi x') (match y + (bbltn (fail formula)) + ((bbltc yi y') (mp_ifzero (mpz_sub n 1) + (and xi (not yi)) + (or (and (iff xi yi) + (bblast_bvult x' y' (mpz_sub n 2))) + (and xi (not yi))))))))) + +(declare bv_bbl_bvslt + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvslt bx by n) f) + (th_holds (iff (bvslt n x y) f)))))))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; BITBLASTING CONNECTORS +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +; bit-blasting connections + +(declare intro_assump_t + (! f formula + (! v var + (! C clause + (! h (th_holds f) + (! a (atom v f) + (! u (! unit (holds (clc (pos v) cln)) + (holds C)) + (holds C)))))))) + +(declare intro_assump_f + (! f formula + (! v var + (! C clause + (! h (th_holds (not f)) + (! a (atom v f) + (! u (! unit (holds (clc (neg v) cln)) + (holds C)) + (holds C)))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; REWRITE RULES +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +; rewrite rule : +; x + y = y + x +(declare bvadd_symm + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (th_holds (= (BitVec n) (bvadd _ x y) (bvadd _ y x))))))) + +;; (declare bvcrazy_rewrite +;; (! n mpz +;; (! x (term (BitVec n)) +;; (! y (term (BitVec n)) +;; (! xn bv_poly +;; (! yn bv_poly +;; (! hxn (bv_normalizes x xn) +;; (! hyn (bv_normalizes y yn) +;; (! s (^ (rewrite_scc xn yn) true) +;; (! u (! x (term (BitVec n)) (holds cln)) +;; (holds cln))))))))))) + +;; (th_holds (= (BitVec n) (bvadd x y) (bvadd y x))))))) + + + +; necessary? +;; (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)))))))) + + +;; making constant bit-vectors +(program mk_ones ((n mpz)) bv + (mp_ifzero n bvn (bvc b1 (mk_ones (mpz_sub n 1))))) + +(program mk_zero ((n mpz)) bv + (mp_ifzero n bvn (bvc b0 (mk_ones (mpz_sub n 1))))) + + + +;; (bvxnor a b) => (bvnot (bvxor a b)) +;; (declare bvxnor_elim +;; (! n mpz +;; (! a (term (BitVec n)) +;; (! b (term (BitVec n)) +;; (! a' (term (BitVec n)) +;; (! b' (term (BitVec n)) +;; (! rwa (rw_term _ a a') +;; (! rwb (rw_term _ b b') +;; (rw_term n (bvxnor _ a b) +;; (bvnot _ (bvxor _ a' b'))))))))))) + + + +;; ;; (bvxor a 0) => a +;; (declare bvxor_zero +;; (! n mpz +;; (! zero_bits bv +;; (! sc (^ (mk_zero n) zero_bits) +;; (! a (term (BitVec n)) +;; (! b (term (BitVec n)) +;; (! a' (term (BitVec n)) +;; (! rwa (rw_term _ a a') +;; (! rwb (rw_term _ b (a_bv _ zero_bits)) +;; (rw_term _ (bvxor _ a b) +;; a')))))))))) + +;; ;; (bvxor a 11) => (bvnot a) +;; (declare bvxor_one +;; (! n mpz +;; (! one_bits bv +;; (! sc (^ (mk_ones n) one_bits) +;; (! a (term (BitVec n)) +;; (! b (term (BitVec n)) +;; (! a' (term (BitVec n)) +;; (! rwa (rw_term _ a a') +;; (! rwb (rw_term _ b (a_bv _ one_bits)) +;; (rw_term _ (bvxor _ a b) +;; (bvnot _ a'))))))))))) + + +;; ;; (bvnot (bvnot a)) => a +;; (declare bvnot_idemp +;; (! n mpz +;; (! a (term (BitVec n)) +;; (! a' (term (BitVec n)) +;; (! rwa (rw_term _ a a') +;; (rw_term _ (bvnot _ (bvnot _ a)) +;; a')))))) + |