Merged bit-vector and uf proof branch.

1 files changed, 22 insertions, 21 deletions

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