Skip to content

Commit

Permalink
More
Browse files Browse the repository at this point in the history
ajreynol committed Nov 19, 2024
1 parent 979ef5e commit 7cf2e76
Showing 3 changed files with 22 additions and 5 deletions.
6 changes: 4 additions & 2 deletions include/cvc5/cvc5_proof_rule.h
Original file line number Diff line number Diff line change
@@ -3171,8 +3171,10 @@ enum ENUM(ProofRewriteRule)
EVALUE(BOOL_XOR_ELIM),
/** Auto-generated from RARE rule bool-not-xor-elim */
EVALUE(BOOL_NOT_XOR_ELIM),
/** Auto-generated from RARE rule bool-not-eq-elim */
EVALUE(BOOL_NOT_EQ_ELIM),
/** Auto-generated from RARE rule bool-not-eq-elim1 */
EVALUE(BOOL_NOT_EQ_ELIM1),
/** Auto-generated from RARE rule bool-not-eq-elim2 */
EVALUE(BOOL_NOT_EQ_ELIM2),
/** Auto-generated from RARE rule ite-neg-branch */
EVALUE(ITE_NEG_BRANCH),
/** Auto-generated from RARE rule ite-then-true */
18 changes: 16 additions & 2 deletions proofs/eo/cpc/rules/Rewrites.eo
Original file line number Diff line number Diff line change
@@ -341,10 +341,14 @@
:args (x1 y1)
:conclusion (= (not (xor x1 y1)) (= x1 y1))
)
(declare-rule bool-not-eq-elim ((x1 Bool) (y1 Bool))
(declare-rule bool-not-eq-elim1 ((x1 Bool) (y1 Bool))
:args (x1 y1)
:conclusion (= (not (= x1 y1)) (= (not x1) y1))
)
(declare-rule bool-not-eq-elim2 ((x1 Bool) (y1 Bool))
:args (x1 y1)
:conclusion (= (not (= x1 y1)) (= x1 (not y1)))
)
(declare-rule ite-neg-branch ((c1 Bool) (x1 Bool) (y1 Bool))
:premises ((= (not y1) x1))
:args (c1 x1 y1)
@@ -457,11 +461,21 @@
:args (x1 y1 xs1 i1 j1)
:conclusion (= (extract j1 i1 (concat x1 xs1 y1)) (extract j1 i1 ($singleton_elim (concat xs1 y1))))
)
(declare-rule bv-eq-extract-elim ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (i1 Int) (j1 Int) (wm1 Int) (jp1 Int) (im1 Int))
(declare-rule bv-eq-extract-elim1 ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (i1 Int) (j1 Int) (wm1 Int) (jp1 Int) (im1 Int))
:premises ((= wm1 (- (@bvsize x1) 1)) (= jp1 (+ j1 1)) (= im1 (- i1 1)))
:args (x1 y1 i1 j1 wm1 jp1 im1)
:conclusion (= (= (extract j1 i1 x1) y1) (= x1 (concat (extract wm1 jp1 x1) y1 (extract im1 0 x1))))
)
(declare-rule bv-eq-extract-elim2 ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (j1 Int) (wm1 Int) (jp1 Int))
:premises ((= wm1 (- (@bvsize x1) 1)) (= jp1 (+ j1 1)))
:args (x1 y1 j1 wm1 jp1)
:conclusion (= (= (extract j1 0 x1) y1) (= x1 (concat (extract wm1 jp1 x1) y1)))
)
(declare-rule bv-eq-extract-elim3 ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (i1 Int) (j1 Int) (im1 Int))
:premises ((= j1 (- (@bvsize x1) 1)) (= im1 (- i1 1)))
:args (x1 y1 i1 j1 im1)
:conclusion (= (= (extract j1 i1 x1) y1) (= x1 (concat y1 (extract im1 0 x1))))
)
(declare-rule bv-extract-bitwise-and ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (i1 Int) (j1 Int))
:args (x1 y1 i1 j1)
:conclusion (= (extract j1 i1 (bvand x1 y1)) (bvand (extract j1 i1 x1) (extract j1 i1 y1)))
3 changes: 2 additions & 1 deletion src/theory/booleans/rewrites
Original file line number Diff line number Diff line change
@@ -49,7 +49,8 @@
(define-rule bool-xor-elim ((x Bool) (y Bool)) (xor x y) (= (not x) y))
(define-rule bool-not-xor-elim ((x Bool) (y Bool)) (not (xor x y)) (= x y))

(define-rule bool-not-eq-elim ((x Bool) (y Bool)) (not (= x y)) (= (not x) y))
(define-rule bool-not-eq-elim1 ((x Bool) (y Bool)) (not (= x y)) (= (not x) y))
(define-rule bool-not-eq-elim2 ((x Bool) (y Bool)) (not (= x y)) (= x (not y)))

(define-cond-rule ite-neg-branch ((c Bool) (x Bool) (y Bool)) (= (not y) x) (ite c x y) (= c x))

0 comments on commit 7cf2e76

Please sign in to comment.