; Deps: th_base.plf
;;;; 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 (!n mpz sort))

; bit type
(declare bit type)
(declare b0 bit)
(declare b1 bit)

; bit vector type used for constants
(declare bv type)
(declare bvn bv)
(declare bvc (! b bit (! v bv bv)))

; calculate the length of a bitvector
;; (program bv_len ((v bv)) mpz
;;   (match v
;;     (bvn 0)
;;     ((bvc b v') (mp_add (bv_len v') 1))))


; a bv constant term
(declare a_bv
	 (! n mpz
	 (! v bv
	    (term (BitVec n)))))

(program bv_constants_are_disequal ((x bv) (y bv)) formula
  (match x
      (bvn (fail formula))
      ((bvc bx x')
        (match y
          (bvn (fail formula))
          ((bvc by y') (match bx
                             (b0 (match by (b0 (bv_constants_are_disequal x' y')) (b1 (true))))
                             (b1 (match by (b0 (true)) (b1 (bv_constants_are_disequal x' y'))))
          ))
      ))
))

(declare bv_disequal_constants
	 (! n mpz
	 (! x bv
	 (! y bv
	 (! c (^ (bv_constants_are_disequal x y) true)
  	   (th_holds (not (= (BitVec n) (a_bv n x) (a_bv n y)))))))))

; a bv variable
(declare var_bv type)
; a bv variable term
(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 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)

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