Generalize

ajreynol · Feb 24, 2025 · b60e28c · b60e28c
1 parent 5c3d39a
commit b60e28c
Show file tree

Hide file tree

Showing 2 changed files with 31 additions and 29 deletions.
diff --git a/proofs/eo/cpc/rules/Rewrites.eo b/proofs/eo/cpc/rules/Rewrites.eo
@@ -964,20 +964,20 @@
   :args (x1 amount1 sz1 nm1 rn1)
   :conclusion (= (bvashr x1 (@bv amount1 sz1)) (repeat rn1 (extract nm1 nm1 x1)))
 )
-(declare-rule bv-and-concat-pullup ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (z1 (BitVec @n2)) (ys1 (BitVec @n3) :list) (nxm1 Int) (ny1 Int) (nym1 Int))
-  :premises ((= ny1 (@bvsize y1)) (= nxm1 (- (@bvsize x1) 1)) (= nym1 (- (@bvsize y1) 1)))
-  :args (x1 y1 z1 ys1 nxm1 ny1 nym1)
-  :conclusion (= (bvand x1 (concat ys1 z1 y1)) (concat (bvand (extract nxm1 ny1 x1) ($singleton_elim (concat ys1 z1))) (bvand (extract nym1 0 x1) y1)))
-)
-(declare-rule bv-or-concat-pullup ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (z1 (BitVec @n2)) (ys1 (BitVec @n3) :list) (nxm1 Int) (ny1 Int) (nym1 Int))
-  :premises ((= ny1 (@bvsize y1)) (= nxm1 (- (@bvsize x1) 1)) (= nym1 (- (@bvsize y1) 1)))
-  :args (x1 y1 z1 ys1 nxm1 ny1 nym1)
-  :conclusion (= (bvor x1 (concat ys1 z1 y1)) (concat (bvor (extract nxm1 ny1 x1) ($singleton_elim (concat ys1 z1))) (bvor (extract nym1 0 x1) y1)))
-)
-(declare-rule bv-xor-concat-pullup ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (z1 (BitVec @n2)) (ys1 (BitVec @n3) :list) (nxm1 Int) (ny1 Int) (nym1 Int))
-  :premises ((= ny1 (@bvsize y1)) (= nxm1 (- (@bvsize x1) 1)) (= nym1 (- (@bvsize y1) 1)))
-  :args (x1 y1 z1 ys1 nxm1 ny1 nym1)
-  :conclusion (= (bvxor x1 (concat ys1 z1 y1)) (concat (bvxor (extract nxm1 ny1 x1) ($singleton_elim (concat ys1 z1))) (bvxor (extract nym1 0 x1) y1)))
+(declare-rule bv-and-concat-pullup ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (ys1 (BitVec @n4) :list) (nxm1 Int) (ny1 Int) (nym1 Int))
+  :premises ((= ny1 (@bvsize y1)) (= nxm1 (- (@bvsize ($singleton_elim (bvand xs1 ws1))) 1)) (= nym1 (- (@bvsize y1) 1)))
+  :args (xs1 ws1 y1 z1 ys1 nxm1 ny1 nym1)
+  :conclusion (= ($singleton_elim (bvand xs1 (concat ys1 z1 y1) ws1)) (eo::define ((_let_1 ($singleton_elim (bvand xs1 ws1)))) (concat (bvand (extract nxm1 ny1 _let_1) ($singleton_elim (concat ys1 z1))) (bvand (extract nym1 0 _let_1) y1))))
+)
+(declare-rule bv-or-concat-pullup ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (ys1 (BitVec @n4) :list) (nxm1 Int) (ny1 Int) (nym1 Int))
+  :premises ((= ny1 (@bvsize y1)) (= nxm1 (- (@bvsize ($singleton_elim (bvor xs1 ws1))) 1)) (= nym1 (- (@bvsize y1) 1)))
+  :args (xs1 ws1 y1 z1 ys1 nxm1 ny1 nym1)
+  :conclusion (= ($singleton_elim (bvor xs1 (concat ys1 z1 y1) ws1)) (eo::define ((_let_1 ($singleton_elim (bvor xs1 ws1)))) (concat (bvor (extract nxm1 ny1 _let_1) ($singleton_elim (concat ys1 z1))) (bvor (extract nym1 0 _let_1) y1))))
+)
+(declare-rule bv-xor-concat-pullup ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (ys1 (BitVec @n4) :list) (nxm1 Int) (ny1 Int) (nym1 Int))
+  :premises ((= ny1 (@bvsize y1)) (= nxm1 (- (@bvsize ($singleton_elim (bvxor xs1 ws1))) 1)) (= nym1 (- (@bvsize y1) 1)))
+  :args (xs1 ws1 y1 z1 ys1 nxm1 ny1 nym1)
+  :conclusion (= ($singleton_elim (bvxor xs1 (concat ys1 z1 y1) ws1)) (eo::define ((_let_1 ($singleton_elim (bvxor xs1 ws1)))) (concat (bvxor (extract nxm1 ny1 _let_1) ($singleton_elim (concat ys1 z1))) (bvxor (extract nym1 0 _let_1) y1))))
 )
 (declare-rule bv-bitwise-idemp-1 ((@n0 Int) (x1 (BitVec @n0)))
   :args (x1)

diff --git a/src/theory/bv/rewrites-simplification b/src/theory/bv/rewrites-simplification
@@ -121,41 +121,43 @@
 
 ; AndOrXorConcatPullUp
 (define-cond-rule bv-and-concat-pullup
-  ((x ?BitVec) (y ?BitVec)
+  ((xs ?BitVec :list) (ws ?BitVec :list) (y ?BitVec)
    (z ?BitVec) (ys ?BitVec :list)
    (nxm1 Int) (ny Int) (nym1 Int))
   (def
-    (nx (@bvsize x))
+    (nx (@bvsize (bvand xs ws)))
   )
   (and (= ny (@bvsize y)) (= nxm1 (- nx 1)) (= nym1 (- (@bvsize y) 1)))
-  (bvand x (concat ys z y))
+  (bvand xs (concat ys z y) ws)
   (concat
-    (bvand (extract nxm1 ny x) (concat ys z)) ; Recur on this
-    (bvand (extract nym1 0 x) y)
+    (bvand (extract nxm1 ny (bvand xs ws)) (concat ys z)) ; Recur on this
+    (bvand (extract nym1 0 (bvand xs ws)) y)
   ))
 (define-cond-rule bv-or-concat-pullup
-  ((x ?BitVec) (y ?BitVec)
+  ((xs ?BitVec :list) (ws ?BitVec :list) (y ?BitVec)
    (z ?BitVec) (ys ?BitVec :list)
    (nxm1 Int) (ny Int) (nym1 Int))
   (def
-    (nx (@bvsize x))
+    (nx (@bvsize (bvor xs ws)))
   )
   (and (= ny (@bvsize y)) (= nxm1 (- nx 1)) (= nym1 (- (@bvsize y) 1)))
-  (bvor x (concat ys z y))
+  (bvor xs (concat ys z y) ws)
   (concat
-    (bvor (extract nxm1 ny x) (concat ys z)) ; Recur on this
-    (bvor (extract nym1 0 x) y)
+    (bvor (extract nxm1 ny (bvor xs ws)) (concat ys z)) ; Recur on this
+    (bvor (extract nym1 0 (bvor xs ws)) y)
   ))
 (define-cond-rule bv-xor-concat-pullup
-  ((x ?BitVec) (y ?BitVec) (z ?BitVec) (ys ?BitVec :list) (nxm1 Int) (ny Int) (nym1 Int))
+  ((xs ?BitVec :list) (ws ?BitVec :list) (y ?BitVec)
+   (z ?BitVec) (ys ?BitVec :list)
+   (nxm1 Int) (ny Int) (nym1 Int))
   (def
-    (nx (@bvsize x))
+    (nx (@bvsize (bvxor xs ws)))
   )
   (and (= ny (@bvsize y)) (= nxm1 (- nx 1)) (= nym1 (- (@bvsize y) 1)))
-  (bvxor x (concat ys z y))
+  (bvxor xs (concat ys z y) ws)
   (concat
-    (bvxor (extract nxm1 ny x) (concat ys z)) ; Recur on this
-    (bvxor (extract nym1 0 x) y)
+    (bvxor (extract nxm1 ny (bvxor xs ws)) (concat ys z)) ; Recur on this
+    (bvxor (extract nym1 0 (bvxor xs ws)) y)
   ))