diff options
author | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 09:43:52 -0700 |
---|---|---|
committer | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 09:43:52 -0700 |
commit | dea679ce032c130d210d54c2e5482f95db1ff04a (patch) | |
tree | 6c36f68150172b20717f7d504274ab0bf82791b0 /proofs/signatures/th_bv.plf | |
parent | d95fe7675e20eaee86b8e804469e6db83265a005 (diff) |
A few more minor updates to match google repository with CVC4 repository
(mostly whitespace differences).
Diffstat (limited to 'proofs/signatures/th_bv.plf')
-rwxr-xr-x | proofs/signatures/th_bv.plf | 288 |
1 files changed, 144 insertions, 144 deletions
diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index 3fb9d1356..0fb50f8cf 100755 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -1,145 +1,145 @@ -; "bitvec" is a term of type "sort"
-(declare BitVec sort)
-
-; bit type
-(declare bit type)
-(declare b0 bit)
-(declare b1 bit)
-
-; bit vector type
-(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))))
-
-; 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)
+; "bitvec" is a term of type "sort" +(declare BitVec sort) + +; bit type +(declare bit type) +(declare b0 bit) +(declare b1 bit) + +; bit vector type +(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)))) + +; 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 |