Merged bit-vector and uf proof branch.

10 files changed, 1071 insertions, 178 deletions

diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am
index 9e8063bf2..82d8c2caa 100644
--- a/proofs/signatures/Makefile.am
+++ b/proofs/signatures/Makefile.am
@@ -3,7 +3,7 @@
 # add support for more theories, just list them here in the same order
 # you would to the LFSC proof-checker binary.
 #
-CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf
+CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf
 
 noinst_LTLIBRARIES = libsignatures.la
 
diff --git a/proofs/signatures/core_rewrites.plf b/proofs/signatures/core_rewrites.plf
new file mode 100644
index 000000000..ca2c1fa03
--- /dev/null
+++ b/proofs/signatures/core_rewrites.plf
@@ -0,0 +1,123 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;; Rewrite rules
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; t rewrites to t'
+(declare rw_term
+	 (! s sort
+	 (! t (term s)
+	 (! t' (term s)
+	 type))))
+
+(declare rw_formula
+	 (! f formula
+	 (! f' formula
+	 type)))
+
+ 
+(declare apply_rw_formula
+	 (! f formula
+	 (! f' formula
+	 (! rw (rw_formula f f')
+	 (! fh (th_holds f)
+	 (th_holds f'))))))
+	 
+     
+;; Identity rewrite rules	 
+(declare rw_term_id
+	 (! s sort
+	 (! t (term s)
+	 (rw_term s t t))))
+
+(declare rw_term_trans
+	 (! s sort
+	 (! t1 (term s)
+	 (! t2 (term s)
+	 (! t3 (term s)
+	 (! rw12 (rw_term _ t1 t2)
+	 (! rw23 (rw_term _ t2 t3)
+	 (rw_term s t1 t3))))))))
+	 
+;; rw_symmetry
+	 
+(declare rw_formula_trans
+	 (! f1 formula
+ 	 (! f2 formula
+	 (! f3 formula
+	 (! rw1 (rw_formula f1 f2)
+	 (! rw2 (rw_formula f2 f3)
+	 (rw_formula f1 f3)))))))
+
+	 
+(declare rw_op1_id
+	 (! s sort
+	 (! a (term s)
+	 (! a' (term s)
+	 (! rw (rw_term _ a a')
+	 (! op term_op1
+	    (rw_term _ (op _ a) (op _ a'))))))))
+
+(declare rw_op2_id
+	 (! s sort
+	 (! a (term s)
+	 (! a' (term s)
+	 (! b (term s)
+	 (! b' (term s)
+	 (! rw (rw_term _ a a')
+	 (! rw (rw_term _ b b')
+	 (! op term_op2
+	    (rw_term _ (op _ a b) (op _ a' b')))))))))))
+
+(declare rw_pred1_id
+	 (! s sort
+	 (! a (term s)
+	 (! a' (term s)
+	 (! rw (rw_term _ a a')
+	 (! op op_pred1
+	    (rw_formula (op _ a) (op _ a'))))))))
+	    
+(declare rw_pred2_id
+	 (! s sort
+	 (! a (term s)
+	 (! a' (term s)
+	 (! b (term s)
+	 (! b' (term s)
+	 (! rw (rw_term _ a a')
+	 (! rw (rw_term _ b b')
+	 (! op op_pred2
+	    (rw_formula (op _ a b) (op _ a' b')))))))))))
+
+(declare rw_eq_id
+	 (! s sort
+	 (! a (term s)
+	 (! a' (term s)
+	 (! b (term s)
+	 (! b' (term s)
+	 (! rw (rw_term _ a a')
+	 (! rw (rw_term _ b b')
+	    (rw_formula (= s a b) (= s a' b'))))))))))
+
+(declare rw_formula_op1_id
+	 (! f formula
+	 (! f' formula
+	 (! frw (rw_formula f f')
+	 (! op formula_op1
+	    (rw_formula (op f) (op f')))))))
+
+(declare rw_formula_op2_id
+	 (! f1 formula
+	 (! f1' formula
+	 (! f2 formula
+	 (! f2' formula
+	 (! frw1 (rw_formula f1 f1')
+ 	 (! frw2 (rw_formula f2 f2')	
+	 (! op formula_op2
+	    (rw_formula (op f1 f2) (op f1' f2'))))))))))
+
+
+(apply_rw_formula
+	(! f formula
+	(! f' formula
+	(! r (rw_formula f f')
+	(! h (th_holds f)
+	   (th_holds f'))))))
\ No newline at end of file
diff --git a/proofs/signatures/ex-mem.plf b/proofs/signatures/ex-mem.plf
index 12c4c3e16..7e143c5b6 100755
--- a/proofs/signatures/ex-mem.plf
+++ b/proofs/signatures/ex-mem.plf
@@ -1,5 +1,3 @@
-; AJR : proof used for testing memory use of theory lemmas
-
 (check
 (% s sort
 (% a (term s)
@@ -10,8 +8,8 @@
 ; -------------------- declaration of input formula -----------------------------------
 
 (% A1 (th_holds (= s a b))
-(% A2 (th_holds (= s b a))
-(% A3 (th_holds (not (= s a a)))
+(% A2 (th_holds (= s b c))
+(% A3 (th_holds (not (= s a c)))
 
 ; ------------------- specify that the following is a proof of the empty clause -----------------
 
@@ -20,15 +18,12 @@
 ; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------
 
 (decl_atom (= s a b) (\ v1 (\ a1
-(decl_atom (= s b a) (\ v2 (\ a2
-(decl_atom (= s a a) (\ v3 (\ a3
+(decl_atom (= s b c) (\ v2 (\ a2
+(decl_atom (= s a c) (\ v3 (\ a3
 
 ; --------------------------- proof of theory lemma ---------------------------------------------
 
 (satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3  (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT1
-(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3  (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT2
-(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3  (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT3
-;...add copies here...
 
 ; -------------------- clausification of input formulas -----------------------------------------
 
@@ -64,5 +59,4 @@
 
 (\ x x))
 
-)))))))))))))))))))))))))))))
-))
+)))))))))))))))))))))))))))
diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf
index ae585e455..58494e793 100755..100644
--- a/proofs/signatures/ex_bv.plf
+++ b/proofs/signatures/ex_bv.plf
@@ -1,31 +1,32 @@
-; a = b ^ a = 00000 ^ b = 11111 is UNSAT
+; (a = b) ^ (a = b & 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))))))))
+(% f1 (th_holds (= (BitVec 4) (a_var_bv _ a) (a_var_bv _ b)))
+(% f2 (th_holds (= (BitVec 4) (a_var_bv _ a) (bvand 4 (a_var_bv 4 b) (a_bv _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn)))))))))
+(% f3 (th_holds (= (BitVec 4) (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_bv_term_var 5 a (\ ba1
+;; (decl_bv_term_var 5 b (\ ba2
+;; (decl_bv_term_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3
+;; (decl_bv_term_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
+(decl_atom (bitof a 4) (\ v1 (\ a1
+(decl_atom (bitof 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
+(decl_bblast _ _ _ (bv_bbl_var 4 a _ ) (\ bt1
+(decl_bblast _ _ _ (bv_bbl_var 4 b _ ) (\ bt2
+(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bt3
+(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bt4
+(decl_bblast _ _ _ (bv_bbl_bvand 4 _ _ _ _ _ bt1 bt3) (\ bt5
 
 ; 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
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ bt1 bt2) (\ bf1
+(th_let_pf _ (bv_bbl_bvult _ _ _ _ _ _ bt1 bt5) (\ bf2
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ bt2 bt4) (\ bf3
 
 ; CNFication
 ; a.4 V ~b.4
@@ -33,25 +34,25 @@
 (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
+  trust
 ))))) (\ C2
 
 ; ~a.4
 (satlem _ _
 (ast _ _ _ a1 (\ l1
 (clausify_false
-  (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))
+  trust
 ))) (\ C3
 
 ; b.4 
 (satlem _ _
 (asf _ _ _ a2 (\ l2
 (clausify_false
-  (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)
+  trust
 ))) (\ C6
 
 
 (satlem_simplify _ _ _ 
 (R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))
 
-)))))))))))))))))))))))))))))))))))))))))))
\ No newline at end of file
+)))))))))))))))))))))))))))))))))))))))))))))
diff --git a/proofs/signatures/ex_bv_rewrite.plf b/proofs/signatures/ex_bv_rewrite.plf
new file mode 100644
index 000000000..fbe593502
--- /dev/null
+++ b/proofs/signatures/ex_bv_rewrite.plf
@@ -0,0 +1,41 @@
+(check
+(% x var_bv
+(% y var_bv
+(% a var_bv
+(% A0 (th_holds true)
+(% A1 (th_holds
+      (= (BitVec 1) (a_var_bv 1 x)
+      	 	    (bvnot 1  (bvxnor 1 (bvxor 1 (a_var_bv 1 a) (a_bv 1 (bvc b1 bvn)))
+					(bvxor 1 (a_var_bv 1 a) (a_bv 1 (bvc b0 bvn))) ))))
+(: (th_holds
+      (= (BitVec 1) (a_var_bv 1 x)
+      	 	    (bvxor 1 (bvnot 1 (a_var_bv 1 a)) (a_var_bv 1 a))))
+
+;; print rewritten assertions
+
+(@ ones (a_bv 1 (bvc b1 bvn))
+(@ zero (a_bv 1 (bvc b0 bvn))
+(@ xorone (bvxor 1 (a_var_bv 1 a) ones)
+(@ xorzero (bvxor 1 (a_var_bv 1 a) zero)
+(@ t1 (bvxor 1 xorone xorzero)
+(@ t2 (bvxnor 1 xorone xorzero)
+(@ t3 (bvnot 1 t2)
+(@ t4 (bvnot 1 t1)
+(@ t5 (bvxor 1 (bvnot 1 (a_var_bv 1 a)) (a_var_bv 1 a))
+;; adding identity rewrite proofs
+(@ xor_onerw (rw_term_id 1 xorone)
+(@ xor_zerorw (rw_term_id 1 xorzero)
+(@ rw1 (xnor_elim 1 _ _ _ _ xor_onerw xor_zerorw) ;; bvxnor t1 t2 -> bvnot (bvxor t1 t2)
+(@ rw2 (xor_zero 1 _ _ _ _ (rw_term_id 1 (a_var_bv 1 a)) (rw_term_id 1 zero))
+(@ rw3 (xor_one 1  _ _ _ _ (rw_term_id 1 (a_var_bv 1 a)) (rw_term_id 1 ones))
+(@ rw4 (rw_bvop2_id 1 _ _ _ _ rw3 rw2 bvxor) ;; bvxor t1 t2 -> bvxor t1' t2'
+(@ rw5 (rw_bvop1_id 1 _ _ rw4 bvnot) ;; bvnot (bvxor t1 t2) -> bvnot (bvxor t1' t2')
+(@ rw6 (rw_term_trans 1  _ _ _ rw1 rw5) ;; bvxnor t1 t2 -> bvnot (bvxor t1' t2')
+(@ rw7 (rw_bvop1_id 1 _ _ rw6 bvnot) ;; (bvnot (bvxnor t1 t2)) ->(bvnot (bvnot (bvxor t1' t2')))
+(@ rw8 (not_idemp 1 _ _ (rw_term_id 1 t5)) ;; (bvnot (bvnot (bvxor t1' t2'))) -> bvxor t1' t2'
+(@ rw9 (rw_term_trans 1 _ _ _ rw7 rw8) ;; (bvnot (bvxnor t1 t2)) -> (bvxor t1' t2')
+(@ rw10 (rw_term_id 1 (a_var_bv 1 x))
+(@ rw11 (rw_eq_id 1 _ _ _ _ rw10 rw9) ;;  x = t1 => x = t'
+(apply_rw_formula _ _ rw11 A1)
+
+)))))))))))))))))))))))))))))
\ No newline at end of file
diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf
index 5e2f1cc44..b95caa8fd 100755
--- a/proofs/signatures/sat.plf
+++ b/proofs/signatures/sat.plf
@@ -14,7 +14,7 @@
 
 ; constructs for general clauses for R, Q, satlem
 
-(declare concat (! c1 clause (! c2 clause clause)))
+(declare concat_cl (! c1 clause (! c2 clause clause)))
 (declare clr (! l lit (! c clause clause)))
 
 ; code to check resolutions
@@ -49,7 +49,7 @@
             (match m
               (tt (do (ifmarked4 v v (markvar4 v)) c'))
               (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))
-    ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))
+    ((concat_cl c1 c2) (append (simplify_clause c1) (simplify_clause c2)))
     ((clr l c1)
       (match l
         ; set mark 1 to indicate we should remove v, and fail if
@@ -81,14 +81,14 @@
            (! u1 (holds c1)
            (! u2 (holds c2)
            (! n var
-            (holds (concat (clr (pos n) c1)
+            (holds (concat_cl (clr (pos n) c1)
                      (clr (neg n) c2)))))))))
 
 (declare Q (! c1 clause (! c2 clause
            (! u1 (holds c1)
            (! u2 (holds c2)
            (! n var
-            (holds (concat (clr (neg n) c1)
+            (holds (concat_cl (clr (neg n) c1)
                      (clr (pos n) c2)))))))))
 
 (declare satlem_simplify
@@ -115,13 +115,13 @@
 ;
 ; (check
 ;   (% v1 var
-;   (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
+;   (% u1 (holds (concat_cl (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
 ;                    (clc (pos v1) (clc (pos v1) cln))))
 ;    (satlem _ _ _ u1 (\ x x))))))
 
 
 ;(check
 ;   (% v1 var
-;   (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)
+;   (% u1 (holds (clr (neg v1) (concat_cl (clc (neg v1) cln)
 ;                                      (clr (neg v1) (clc (neg v1) cln)))))
 ;    (satlem _ _ _ u1 (\ x x))))))
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index 62cdf3f94..fa89a457f 100755
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -11,13 +11,29 @@
 ; standard logic definitions
 (declare true formula)
 (declare false formula)
-(declare not (! f formula formula))
-(declare and (! f1 formula (! f2 formula formula)))
-(declare or (! f1 formula (! f2 formula formula)))
-(declare impl (! f1 formula (! f2 formula formula)))
-(declare iff (! f1 formula (! f2 formula formula)))
-(declare xor (! f1 formula (! f2 formula formula)))
-(declare ifte (! b formula (! f1 formula (! f2 formula formula))))
+
+(define formula_op1
+	(! f formula
+	formula))
+
+(define formula_op2
+	(! f1 formula
+	(! f2 formula
+	   formula)))
+	
+(define formula_op3
+	(! f1 formula
+	(! f2 formula
+	(! f3 formula
+	   formula))))
+	   
+(declare not formula_op1)
+(declare and formula_op2)
+(declare or formula_op2)
+(declare impl formula_op2)
+(declare iff formula_op2)
+(declare xor formula_op2)
+(declare ifte formula_op3)
 
 ; terms
 (declare sort type)
@@ -46,6 +62,19 @@
 (declare Bool sort)				; the special sort for predicates
 (declare p_app (! x (term Bool) formula))	; propositional application of term
 
+; boolean terms
+(declare t_true (term Bool))
+(declare t_false (term Bool))
+(declare t_t_neq_f
+ (th_holds (not (= Bool t_true t_false))))
+(declare pred_eq_t
+ (! x (term Bool)
+ (! u (th_holds (p_app x))
+   (th_holds (= Bool x t_true)))))
+(declare pred_eq_f
+ (! x (term Bool)
+ (! u (th_holds (not (p_app x)))
+   (th_holds (= Bool x t_false)))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;
@@ -54,8 +83,12 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ; binding between an LF var and an (atomic) formula
+
 (declare atom (! v var (! p formula type)))
 
+; binding between two LF vars
+(declare bvatom (! sat_v var (! bv_v var type)))
+
 (declare decl_atom
   (! f formula
   (! u (! v var
@@ -63,6 +96,19 @@
          (holds cln)))
     (holds cln))))
 
+;; declare atom enhanced with mapping
+;; between SAT prop variable and BVSAT prop variable
+(declare decl_bvatom
+  (! f formula
+  (! u (! v var
+       (! bv_v var
+       (! a (atom v f)
+       (! bva (atom bv_v f)
+       (! vbv (bvatom v bv_v)
+         (holds cln))))))
+    (holds cln))))
+    
+    
 ; clausify a formula directly
 (declare clausify_form
   (! f formula
@@ -88,13 +134,18 @@
   (! u2 (! v (th_holds f) (holds cln))
     (holds cln)))))
 
-
+  
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;
 ; Natural deduction rules : used for CNF
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+;; for eager bit-blasting
+(declare iff_symm
+	(! f formula
+	   (th_holds (iff f f))))
+
 
 ;; contradiction
 
@@ -291,8 +342,33 @@
   (! u (! o (th_holds (not f))
          (holds C))
     (holds (clc (pos v) C))))))))
-    
 
+;; Bitvector lemma constructors to assume
+;; the unit clause containing the assumptions
+;; it also requires the mapping between bv_v and v
+;; The resolution proof proving false will use bv_v as the definition clauses use bv_v
+;; but the Problem clauses in the main SAT solver will use v so the learned clause is in terms of v
+(declare bv_asf
+  (! v var
+  (! bv_v var
+  (! f formula
+  (! C clause
+  (! r (atom v f) ;; passed in
+  (! x (bvatom v bv_v) ; establishes the equivalence of v to bv_
+  (! u (! o (holds (clc (neg bv_v) cln)) ;; l binding to be used in proof
+         (holds C))
+    (holds (clc (pos v) C))))))))))
+    
+(declare bv_ast
+  (! v var
+  (! bv_v var	
+  (! f formula
+  (! C clause
+  (! r (atom v f)       ; this is specified
+  (! x (bvatom v bv_v) ; establishes the equivalence of v to bv_v
+  (! u (! o (holds (clc (pos bv_v) cln))
+         (holds C))
+    (holds (clc (neg v) C))))))))))
 
 
 ;; Example:
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
index 0c6b16048..8334f51de 100755
--- a/proofs/signatures/th_arrays.plf
+++ b/proofs/signatures/th_arrays.plf
@@ -3,7 +3,7 @@
 ; Theory of Arrays
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; depdends on : th_base.plf
+; depends on : th_base.plf
 
 ; sorts
 
diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf
index 0fb50f8cf..c93541085 100755..100644
--- a/proofs/signatures/th_bv.plf
+++ b/proofs/signatures/th_bv.plf
@@ -1,145 +1,174 @@
+;;;; 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 sort)
+(declare BitVec (!n mpz sort))
 
 ; bit type
 (declare bit type)
 (declare b0 bit)
 (declare b1 bit)
 
-; bit vector type
+; bit vector type used for constants
 (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))))
+;; (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)))))
+	 
 
 ; 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
+(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 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)
+(declare concat 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)
+
diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf
new file mode 100644
index 000000000..8e8c51857
--- /dev/null
+++ b/proofs/signatures/th_bv_bitblast.plf
@@ -0,0 +1,629 @@
+; 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)))))
+
+
+(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))))))))
+
+
+; 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)))))))
+				
+				
+(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 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))
+
+;; (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))))
+	
+(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))))))))))))
+
+			 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; 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'))))))
+