A few more minor updates to match google repository with CVC4 repository

(mostly whitespace differences).

2 files changed, 200 insertions, 200 deletions

diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf
index 02cadaeab..ae585e455 100755
--- a/proofs/signatures/ex_bv.plf
+++ b/proofs/signatures/ex_bv.plf
@@ -1,57 +1,57 @@
-; a = b ^ a = 00000 ^ b = 11111 is UNSAT

-

-(check

-(% a var_bv

-(% b var_bv

-(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b)))

-(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))

-(% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))

-(: (holds cln)

-

-(decl_bv_atom_var 5 a (\ ba1

-(decl_bv_atom_var 5 b (\ ba2

-(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3

-(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4

-

-(decl_atom (bblast a 4) (\ v1 (\ a1

-(decl_atom (bblast b 4) (\ v2 (\ a2

-

-; bitblasting terms

-(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1

-(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2

-(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3

-(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4

-

-; bitblasting formulas

-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1

-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ bf2

-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt2 bt4) (\ bf3

-

-; CNFication

-; a.4 V ~b.4

-(satlem _ _

-(asf _ _ _ a1 (\ l1

-(ast _ _ _ a2 (\ l2

-(clausify_false

-  (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f1 bf1)))) l1)   ; notice at the intermost we impl_elim, which converts from atom to bit-blasting representation

-))))) (\ C2

-

-; ~a.4

-(satlem _ _

-(ast _ _ _ a1 (\ l1

-(clausify_false

-  (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))

-))) (\ C3

-

-; b.4 

-(satlem _ _

-(asf _ _ _ a2 (\ l2

-(clausify_false

-  (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)

-))) (\ C6

-

-

-(satlem_simplify _ _ _ 

-(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))

-

+; a = b ^ a = 00000 ^ b = 11111 is UNSAT
+
+(check
+(% a var_bv
+(% b var_bv
+(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b)))
+(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))
+(% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))
+(: (holds cln)
+
+(decl_bv_atom_var 5 a (\ ba1
+(decl_bv_atom_var 5 b (\ ba2
+(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3
+(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4
+
+(decl_atom (bblast a 4) (\ v1 (\ a1
+(decl_atom (bblast b 4) (\ v2 (\ a2
+
+; bitblasting terms
+(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1
+(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2
+(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3
+(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4
+
+; bitblasting formulas
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ bf2
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt2 bt4) (\ bf3
+
+; CNFication
+; a.4 V ~b.4
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(ast _ _ _ a2 (\ l2
+(clausify_false
+  (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f1 bf1)))) l1)   ; notice at the intermost we impl_elim, which converts from atom to bit-blasting representation
+))))) (\ C2
+
+; ~a.4
+(satlem _ _
+(ast _ _ _ a1 (\ l1
+(clausify_false
+  (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))
+))) (\ C3
+
+; b.4 
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+  (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)
+))) (\ C6
+
+
+(satlem_simplify _ _ _ 
+(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))
+
 )))))))))))))))))))))))))))))))))))))))))))
\ No newline at end of file
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