diff options
Diffstat (limited to 'proofs')
| -rwxr-xr-x | proofs/signatures/th_arrays.plf | 2 | ||||
| -rw-r--r-- | proofs/signatures/th_bv.plf | 27 | ||||
| -rw-r--r-- | proofs/signatures/th_bv_bitblast.plf | 419 |
3 files changed, 353 insertions, 95 deletions
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf index 5ed3d2f6f..b54a4ed5b 100755 --- a/proofs/signatures/th_arrays.plf +++ b/proofs/signatures/th_arrays.plf @@ -60,4 +60,4 @@ (! u1 (! k (term s1) (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k))))) (holds cln))) - (holds cln))))))) + (holds cln)))))))
\ No newline at end of file diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index c93541085..7f478d823 100644 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -8,7 +8,7 @@ (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)) @@ -21,7 +21,7 @@ (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 (!n mpz sort)) @@ -37,7 +37,7 @@ (declare bvc (! b bit (! v bv bv))) ; calculate the length of a bitvector -;; (program bv_len ((v bv)) mpz +;; (program bv_len ((v bv)) mpz ;; (match v ;; (bvn 0) ;; ((bvc b v') (mp_add (bv_len v') 1)))) @@ -48,7 +48,7 @@ (! n mpz (! v bv (term (BitVec n))))) - + ; a bv variable (declare var_bv type) @@ -61,7 +61,7 @@ ; bit vector binary operators (define bvop2 (! n mpz - (! x (term (BitVec n)) + (! x (term (BitVec n)) (! y (term (BitVec n)) (term (BitVec n)))))) @@ -88,7 +88,7 @@ ; bit vector unary operators (define bvop1 (! n mpz - (! x (term (BitVec n)) + (! x (term (BitVec n)) (term (BitVec n))))) @@ -111,8 +111,8 @@ (! t1 (term (BitVec m)) (! t2 (term (BitVec m')) (term (BitVec n)))))))) - -;; side-condition fails in signature only?? + +;; side-condition fails in signature only?? ;; (! s (^ (mp_add m m') n) ;; (declare repeat bvopp) @@ -147,22 +147,22 @@ (term (BitVec n))))))) - -;; TODO: add checks for valid typing for these operators + +;; 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) +;; (! 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) @@ -171,4 +171,3 @@ (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 index 580b54418..d8ce7be22 100644 --- a/proofs/signatures/th_bv_bitblast.plf +++ b/proofs/signatures/th_bv_bitblast.plf @@ -4,7 +4,7 @@ (declare bbltc (! f formula (! v bblt bblt))) ; calculate the length of a bit-blasted term -(program bblt_len ((v bblt)) mpz +(program bblt_len ((v bblt)) mpz (match v (bbltn 0) ((bbltc b v') (mp_add (bblt_len v') 1)))) @@ -25,6 +25,7 @@ (bblast_term n x y))))) +; Binds a symbol to the bblast_term to be used later on. (declare decl_bblast (! n mpz (! b bblt @@ -46,31 +47,31 @@ ;; BITBLASTING RULES ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST CONSTANT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_const ((v bv) (n mpz)) bblt - (mp_ifneg n (match v (bvn bbltn) + (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 + (mp_ifneg n bbltn (bbltc (bitof x n) (bblast_var x (mp_add n (~ 1)))))) (declare bv_bbl_var (! n mpz @@ -79,18 +80,16 @@ (! 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 + (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 @@ -104,35 +103,93 @@ (! c (^ (bblast_concat xb yb ) rb) (bblast_term n (concat n m m1 x y) rb))))))))))))) - +(declare bv_bbl_concat_alias_1 (! n mpz + (! m mpz + (! m1 mpz + (! x (term (BitVec m)) + (! y (term (BitVec m1)) + (! xb bblt + (! yb bblt + (! rb bblt + (! a (term (BitVec m)) + (! e (th_holds (= _ x a)) + (! 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 a y) rb))))))))))))))) + +(declare bv_bbl_concat_alias_2 (! 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) + (! a (term (BitVec m1)) + (! e (th_holds (= _ y a)) + (! ybb (bblast_term m1 y yb) + (! c (^ (bblast_concat xb yb) rb) + (bblast_term n (concat n m m1 x a) rb))))))))))))))) + +(declare bv_bbl_concat_alias_1_2 (! n mpz + (! m mpz + (! m1 mpz + (! x (term (BitVec m)) + (! y (term (BitVec m1)) + (! xb bblt + (! yb bblt + (! rb bblt + (! a1 (term (BitVec m)) + (! e (th_holds (= _ x a1)) + (! xbb (bblast_term m x xb) + (! a2 (term (BitVec m1)) + (! e (th_holds (= _ y a2)) + (! ybb (bblast_term m1 y yb) + (! c (^ (bblast_concat xb yb) rb) + (bblast_term n (concat n m m1 a1 a2) rb))))))))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST EXTRACT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_extract_rec ((x bblt) (i mpz) (j mpz) (n mpz)) bblt - (match x + (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))) + (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)) + (! 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))))))))))) +(declare bv_bbl_extract_alias (! n mpz + (! i mpz + (! j mpz + (! m mpz + (! x (term (BitVec m)) + (! xb bblt + (! rb bblt + (! a (term (BitVec m)) + (! e (th_holds (= _ x a)) + (! xbb (bblast_term m x xb) + (! c ( ^ (bblast_extract xb i j m) rb) + (bblast_term n (extract n i j m a) rb))))))))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST ZERO/SIGN EXTEND @@ -148,42 +205,50 @@ (declare bv_bbl_zero_extend (! n mpz (! k mpz (! m mpz - (! x (term (BitVec m)) + (! 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)))) + ((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)) + (! 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)))))))))) - - - + +(declare bv_bbl_sign_extend_alias (! n mpz + (! k mpz + (! m mpz + (! x (term (BitVec m)) + (! xb bblt + (! rb bblt + (! a (term (BitVec m)) + (! e (th_holds (= _ x a)) + (! xbb (bblast_term m x xb) + (! c ( ^ (bblast_sextend xb k m) rb) + (bblast_term n (sign_extend n k m a) rb)))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVAND ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvand ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((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)) @@ -199,11 +264,10 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_bvnot ((x bblt)) bblt - (match x - (bbltn bbltn) + (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 @@ -215,15 +279,14 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVOR ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvor ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((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)) @@ -238,15 +301,14 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVXOR ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvxor ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((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)) @@ -262,8 +324,8 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVADD ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; return the carry bit after adding x y + +;; 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 @@ -272,7 +334,7 @@ (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 +;; 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)))) @@ -296,19 +358,19 @@ ;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt ;(match a ; ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) -; ((bbltc ai a') (match b +; ((bbltc ai a') (match b ; (bbltn (fail bblt)) -; ((bbltc bi b') +; ((bbltc bi b') ; (let carry' (or (and ai bi) (and (xor ai bi) carry)) ; (bbltc (xor (xor ai bi) carry) ; (bblast_bvadd_2h a' b' carry')))))))) ;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt -;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +;(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 ret (bblast_bvadd_2h ar br carry) ; (reverseb ret))))) - + (declare bv_bbl_bvadd (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -320,6 +382,18 @@ (! c (^ (bblast_bvadd xb yb false) rb) (bblast_term n (bvadd n x y) rb))))))))))) +(declare bv_bbl_bvadd_alias_1 (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! a (term (BitVec n)) + (! e (th_holds (= _ x a)) + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvadd xb yb false) rb) + (bblast_term n (bvadd n a y) rb))))))))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVNEG @@ -331,8 +405,8 @@ (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 @@ -346,14 +420,14 @@ ;; BITBLAST BVMUL ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + ;; shift add multiplier ;; (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)) @@ -362,7 +436,7 @@ (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 +;; 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)) @@ -371,7 +445,7 @@ (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] @@ -395,19 +469,19 @@ (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) + (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 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 + (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)) @@ -420,18 +494,18 @@ (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 + (match x (bbltn (match y (bbltn f) (default (fail formula)))) - ((bbltc fx x') (match y + ((bbltc fx x') (match y (bbltn (fail formula)) ((bbltc fy y') (bblast_eq_rec x' y' (and (iff fx fy) f))))) (default (fail formula)))) @@ -441,7 +515,23 @@ ((bbltc bx x') (match y ((bbltc by y') (bblast_eq_rec x' y' (iff bx by))) (default (fail formula)))) (default (fail formula)))) - + + +;; TODO: a temporary bypass for rewrites that we don't support yet. As soon +;; as we do, remove this rule. + +(declare bv_bbl_=_false + (! 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) false)))))))))))) + (declare bv_bbl_= (! n mpz (! x (term (BitVec n)) @@ -454,11 +544,110 @@ (! c (^ (bblast_eq bx by) f) (th_holds (iff (= (BitVec n) x y) f)))))))))))) - +(declare bv_bbl_=_swap + (! 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 by bx) f) + (th_holds (iff (= (BitVec n) x y) f)))))))))))) + +(declare bv_bbl_=_alias_1 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a (term (BitVec n)) + (! e (th_holds (= _ x a)) + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) a y) f)))))))))))))) + +(declare bv_bbl_=_alias_1_swap + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a (term (BitVec n)) + (! e (th_holds (= _ x a)) + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq by bx) f) + (th_holds (iff (= (BitVec n) a y) f)))))))))))))) + +(declare bv_bbl_=_alias_2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! a (term (BitVec n)) + (! e (th_holds (= _ y a)) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) x a) f)))))))))))))) + +(declare bv_bbl_=_alias_2_swap + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! a (term (BitVec n)) + (! e (th_holds (= _ y a)) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq by bx) f) + (th_holds (iff (= (BitVec n) x a) f)))))))))))))) + +(declare bv_bbl_=_alias_1_2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a1 (term (BitVec n)) + (! e1 (th_holds (= _ x a1)) + (! bbx (bblast_term n x bx) + (! a2 (term (BitVec n)) + (! e2 (th_holds (= _ y a2)) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) a1 a2) f)))))))))))))))) + +(declare bv_bbl_=_alias_1_2_swap + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a1 (term (BitVec n)) + (! e1 (th_holds (= _ x a1)) + (! bbx (bblast_term n x bx) + (! a2 (term (BitVec n)) + (! e2 (th_holds (= _ y a2)) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq by bx) f) + (th_holds (iff (= (BitVec n) a1 a2) f)))))))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVULT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvult ((x bblt) (y bblt) (n mpz)) formula (match x ( bbltn (fail formula)) @@ -480,10 +669,54 @@ (! c (^ (bblast_bvult bx by (mp_add n (~1))) f) (th_holds (iff (bvult n x y) f)))))))))))) +(declare bv_bbl_bvult_alias_1 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a1 (term (BitVec n)) + (! e1 (th_holds (= _ x a1)) + (! 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 a1 y) f)))))))))))))) + +(declare bv_bbl_bvult_alias_2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! a2 (term (BitVec n)) + (! e2 (th_holds (= _ y a2)) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvult bx by (mp_add n (~1))) f) + (th_holds (iff (bvult n x a2) f)))))))))))))) + +(declare bv_bbl_bvult_alias_1_2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a1 (term (BitVec n)) + (! e1 (th_holds (= _ x a1)) + (! bbx (bblast_term n x bx) + (! a2 (term (BitVec n)) + (! e2 (th_holds (= _ y a2)) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvult bx by (mp_add n (~1))) f) + (th_holds (iff (bvult n a1 a2) f)))))))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVSLT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvslt ((x bblt) (y bblt) (n mpz)) formula (match x ( bbltn (fail formula)) @@ -506,7 +739,34 @@ (! bby (bblast_term n y by) (! c (^ (bblast_bvslt bx by n) f) (th_holds (iff (bvslt n x y) f)))))))))))) - + +(declare bv_bbl_bvslt_alias_1 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a (term (BitVec n)) + (! e (th_holds (= _ x a)) + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvslt bx by n) f) + (th_holds (iff (bvslt n a y) f)))))))))))))) + +(declare bv_bbl_bvslt_alias_2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! a (term (BitVec n)) + (! e (th_holds (= _ y a)) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvslt bx by n) f) + (th_holds (iff (bvslt n x a) f)))))))))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -543,8 +803,8 @@ ;; REWRITE RULES ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - + + ; rewrite rule : ; x + y = y + x (declare bvadd_symm @@ -552,7 +812,7 @@ (! 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)) @@ -564,12 +824,12 @@ ;; (! 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? + + +; necessary? ;; (program calc_bvand ((a bv) (b bv)) bv ;; (match a ;; (bvn (match b (bvn bvn) (default (fail bv)))) @@ -578,7 +838,7 @@ ;; (default (fail bv)))))) ;; ; rewrite rule (w constants) : -;; ; a & b = c +;; ; a & b = c ;; (declare bvand_const (! c bv ;; (! a bv ;; (! b bv @@ -586,7 +846,7 @@ ;; (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c)))))))) -;; making constant bit-vectors +;; making constant bit-vectors (program mk_ones ((n mpz)) bv (mp_ifzero n bvn (bvc b1 (mk_ones (mpz_sub n 1))))) @@ -594,7 +854,7 @@ (mp_ifzero n bvn (bvc b0 (mk_ones (mpz_sub n 1))))) - + ;; (bvxnor a b) => (bvnot (bvxor a b)) ;; (declare bvxnor_elim ;; (! n mpz @@ -621,7 +881,7 @@ ;; (! rwb (rw_term _ b (a_bv _ zero_bits)) ;; (rw_term _ (bvxor _ a b) ;; a')))))))))) - + ;; ;; (bvxor a 11) => (bvnot a) ;; (declare bvxor_one ;; (! n mpz @@ -635,7 +895,7 @@ ;; (rw_term _ (bvxor _ a b) ;; (bvnot _ a'))))))))))) - + ;; ;; (bvnot (bvnot a)) => a ;; (declare bvnot_idemp ;; (! n mpz @@ -644,4 +904,3 @@ ;; (! rwa (rw_term _ a a') ;; (rw_term _ (bvnot _ (bvnot _ a)) ;; a')))))) - |