diff options
Diffstat (limited to 'src/lfsc/tests/signatures/th_bv_bitblast.plf')
| -rw-r--r-- | src/lfsc/tests/signatures/th_bv_bitblast.plf | 671 |
1 files changed, 671 insertions, 0 deletions
diff --git a/src/lfsc/tests/signatures/th_bv_bitblast.plf b/src/lfsc/tests/signatures/th_bv_bitblast.plf new file mode 100644 index 0000000..ebb412f --- /dev/null +++ b/src/lfsc/tests/signatures/th_bv_bitblast.plf @@ -0,0 +1,671 @@ +; 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))))) + + +; Binds a symbol to the bblast_term to be used later on. +(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)))))))) + +(declare decl_bblast_with_alias + (! n mpz + (! b bblt + (! t (term (BitVec n)) + (! a (term (BitVec n)) + (! bb (bblast_term n t b) + (! e (th_holds (= _ t a)) + (! s (^ (bblt_len b) n) + (! u (! v (bblast_term n a 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))))))) + + +(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)) + + +; AJR: use this version? +;(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 +; (bbltn (fail bblt)) +; ((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 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)) + (! 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 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)))) + + +;; 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)) + (! 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)))))))))))) + +(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)))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; 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')))))) |