From 327fe83f2e0533d53902645364180bc51ff20dcc Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 29 Mar 2019 00:02:03 -0500 Subject: [PATCH] removing deprecated rewriting signature / example (#2906) --- proofs/signatures/core_rewrites.plf | 123 ---------------------------- proofs/signatures/ex_bv_rewrite.plf | 41 ---------- 2 files changed, 164 deletions(-) delete mode 100644 proofs/signatures/core_rewrites.plf delete mode 100644 proofs/signatures/ex_bv_rewrite.plf diff --git a/proofs/signatures/core_rewrites.plf b/proofs/signatures/core_rewrites.plf deleted file mode 100644 index ca2c1fa03..000000000 --- a/proofs/signatures/core_rewrites.plf +++ /dev/null @@ -1,123 +0,0 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;; 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_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 -- 2.30.2