; Deps: th_base.plf th_bv.plf
; 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) 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) 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 conjunction (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))))))))))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST BVCOMP
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(program bblast_bvcomp ((x bblt) (y bblt) (n mpz)) bblt
  (match x ((bbltc bx x') (match y ((bbltc by y')
  	   	                      (bbltc (bblast_eq_rec x' y' (iff bx by)) bbltn))
                                   (default (fail bblt))))
           (default (fail bblt))
	   ))

(declare bv_bbl_bvcomp (! 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_bvcomp xb yb n) rb)
                              (bblast_term 1 (bvcomp n x y) rb)))))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;;           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'))))))