diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-03-29 00:02:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-29 00:02:03 -0500 |
| commit | 327fe83f2e0533d53902645364180bc51ff20dcc (patch) | |
| tree | e8bfbcad00a10cacc60e19d1b66b7dfc46a51684 /proofs/signatures/ex_bv_rewrite.plf | |
| parent | a1decafaf4c7c46a4eda3d816e9a8799b4c96ad3 (diff) | |
removing deprecated rewriting signature / example (#2906)
Diffstat (limited to 'proofs/signatures/ex_bv_rewrite.plf')
| -rw-r--r-- | proofs/signatures/ex_bv_rewrite.plf | 41 |
1 files changed, 0 insertions, 41 deletions
diff --git a/proofs/signatures/ex_bv_rewrite.plf b/proofs/signatures/ex_bv_rewrite.plf deleted file mode 100644 index fbe593502..000000000 --- a/proofs/signatures/ex_bv_rewrite.plf +++ /dev/null @@ -1,41 +0,0 @@ -(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 |