Skip to content

Commit

Permalink
Do not mark a few BV rules as fixed point (cvc5#10701)
Browse files Browse the repository at this point in the history
The rules in question are definitely not fixed point rules.

Note that other BV rules that are marked as fixed point currently are not being treated as fixed point since the current reconstruction requires a context to be provided explicitly. I am investigating this separately.
  • Loading branch information
ajreynol authored Apr 29, 2024
1 parent e1190ea commit 7d8f56b
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/theory/bv/rewrites
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@
((xs ?BitVec :list) (ys ?BitVec :list) (zs ?BitVec :list) (x ?BitVec))
(bvand xs x ys x zs)
(bvand xs x ys zs))
(define-rule* bv-and-simplify-2
(define-rule bv-and-simplify-2
((xs ?BitVec :list) (ys ?BitVec :list) (zs ?BitVec :list) (x ?BitVec))
(bvand xs x ys (bvnot x) zs)
(@bv 0 (@bvsize x)))
Expand All @@ -150,7 +150,7 @@
((xs ?BitVec :list) (ys ?BitVec :list) (zs ?BitVec :list) (x ?BitVec))
(bvor xs x ys x zs)
(bvor xs x ys zs))
(define-rule* bv-or-simplify-2
(define-rule bv-or-simplify-2
((xs ?BitVec :list) (ys ?BitVec :list) (zs ?BitVec :list) (x ?BitVec))
(bvor xs x ys (bvnot x) zs)
(bvnot (@bv 0 (@bvsize x))))
Expand All @@ -159,11 +159,11 @@
((xs ?BitVec :list) (ys ?BitVec :list) (zs ?BitVec :list) (x ?BitVec))
(bvxor xs x ys x zs)
(bvxor xs ys zs))
(define-rule* bv-xor-simplify-2
(define-rule bv-xor-simplify-2
((xs ?BitVec :list) (ys ?BitVec :list) (zs ?BitVec :list) (x ?BitVec))
(bvxor xs x ys (bvnot x) zs)
(bvnot (bvxor xs ys zs)))
(define-rule* bv-xor-simplify-3
(define-rule bv-xor-simplify-3
((xs ?BitVec :list) (ys ?BitVec :list) (zs ?BitVec :list) (x ?BitVec))
(bvxor xs (bvnot x) ys x zs)
(bvnot (bvxor xs ys zs)))
Expand Down

0 comments on commit 7d8f56b

Please sign in to comment.