diff options
Diffstat (limited to 'proofs/signatures/ex_bv.plf')
-rw-r--r--[-rwxr-xr-x] | proofs/signatures/ex_bv.plf | 43 |
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 +))))))))))))))))))))))))))))))))))))))))))))) |