path: root/src/theory/rewriter/rules/basic.rules

/******************************************************************************
 * Core
 ******************************************************************************/

/* ConcatFlatten: FLATTEN IMPLICIT */

(define-rule ConcatExtractMerge ((i Int :const) (n Int :const) (m Int :const) (o Int :const) (p Int :const) (q Int :const) (r Int :const) (x (_ BitVec i)) (xs (_ BitVec n) :list) (ys (_ BitVec m) :list))
  (concat xs ((_ extract o p) x) ((_ extract q r) x) ys)
  (cond
    ((= p (+ q 1)) (concat xs ((_ extract o r) x) ys)))
)

/*
(define-rule ConcatConstantMerge ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (q Int :const) (r Int :const) (xs (_ BitVec n) :list) (ys (_ BitVec m) :list))
  (concat xs (_ bv o p) (_ bv q r) ys)
  (concat xs (concat (_ bv o p) (_ bv q r)) ys))
*/

(define-rule ExtractWhole ((i Int :const) (n Int :const) (x (_ BitVec n)))
  ((_ extract i 0) x)
  (cond 
    ((= i (- n 1)) x)))

/* ExtractConcat */

(define-rule ExtractExtract ((i Int :const) (j Int :const) (k Int :const) (l Int :const) (x (_ BitVec n)))
  ((_ extract i j) ((_ extract k l) x))
  ((_ extract (+ k j) (+ l j)) x))

(define-rule SimplifyEq ((x (_ BitVec n)))
  (= x x)
  true)

/******************************************************************************
 * Normalization
 ******************************************************************************/

(define-rule ExtractBitwiseAnd ((n Int :const) (i Int :const) (j Int :const) (xs (_ BitVec n) :list))
  ((_ extract i j) (bvand xs))
  (bvand (map (lambda (x (_ BitVec n)) ((_ extract i j) x)) xs)))

(define-rule ExtractBitwiseOr ((n Int :const) (i Int :const) (j Int :const) (xs (_ BitVec n) :list))
  ((_ extract i j) (bvor xs))
  (bvor (map (lambda (x (_ BitVec n)) ((_ extract i j) x)) xs)))

(define-rule ExtractBitwiseXor ((n Int :const) (i Int :const) (j Int :const) (xs (_ BitVec n) :list))
  ((_ extract i j) (bvxor xs))
  (bvxor (map (lambda (x (_ BitVec n)) ((_ extract i j) x)) xs)))

(define-rule ExtractNot ((i Int :const) (j Int :const) (x (_ BitVec n)))
  ((_ extract i j) (bvnot x))
  (bvnot ((_ extract i j) x)))

(define-rule ExtractSignExtend ((i Int :const) (j Int :const) (k Int :const) (n Int :const) (x (_ BitVec n)))
  ((_ extract i j) ((_ sign_extend k) x))
  (cond
    ((< i n) ((_ extract i j) x))
    ((and (< j n) (>= i n)) ((_ sign_extend (+ (- i n) 1)) ((_ extract (- n 1) j) x)))
    (true ((_ repeat (+ (- i j) 1)) ((_ extract (- n 1) (- n 1)) x)))))

(define-rule ExtractArithAdd ((n Int :const) (i Int :const) (xs (_ BitVec n) :list))
  ((_ extract i 0) (bvadd xs))
  (bvadd (map (lambda (x (_ BitVec n)) ((_ extract i 0) x)) xs)))

(define-rule ExtractArithMul ((n Int :const) (i Int :const) (xs (_ BitVec n) :list))
  ((_ extract i 0) (bvmul xs))
  (bvmul (map (lambda (x (_ BitVec n)) ((_ extract i 0) x)) xs)))

(define-rule MultDistribConstAdd ((n Int :const) (c (_ BitVec n) :const) (xs (_ BitVec n) :list))
  (bvmul c (bvadd xs))
  (bvadd (map (lambda (y (_ BitVec n)) (bvmul y c)) xs)))

(define-rule MultDistribConstSub ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvmul c (bvsub x y))
  (bvsub (bvmul x c) (bvmul y c)))

(define-rule MultDistribConstNeg ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)))
  (bvmul c (bvneg x))
  (bvneg (bvmul x c)))

(define-rule MultDistribAdd ((n Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
  (bvmul x (bvadd xs))
  (bvadd (map (lambda (y (_ BitVec n)) (bvmul y x)) xs)))

(define-rule MultDistribSub ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)) (z (_ BitVec n)) (xs (_ BitVec n) :list))
  (bvmul x (bvsub y z))
  (bvsub (bvmul x y) (bvmul x z)))

(define-rule NegMult ((n Int :const) (c (_ BitVec n) :const) (xs (_ BitVec n) :list))
  (bvneg (bvmul c xs))
  (bvmul (bvneg c) xs))

(define-rule NegSub ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvneg (bvsub x y))
  (bvsub y x))

(define-rule NegPlus ((n Int :const) (xs (_ BitVec n) :list))
  (bvneg (bvadd xs))
  (bvadd (map (lambda (x (_ BitVec n)) (bvneg x)) xs)))

(define-rule AndSimplifyRmDups ((x (_ BitVec n)) (xs (_ BitVec n) :list))
  (bvand x x xs)
  (bvand x xs))

(define-rule AndSimplifySimpConsts ((n Int :const) (i (_ BitVec n) :const) (j (_ BitVec n) :const) (xs (_ BitVec n) :list))
  (bvand i j xs)
  (bvand (bvand i j) xs))

(define-rule AndSimplifyZero ((n Int :const) (xs (_ BitVec n) :list))
  (bvand (_ bv 0 n) xs)
  (_ bv 0 n))

(define-rule AndSimplifyRmOnes ((n Int :const) (xs (_ BitVec n) :list))
  (bvand (bvnot (_ bv 0 n)) xs)
  (bvand xs))

(define-rule AndSimplifyCancel ((n Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
  (bvand x (bvnot x) xs)
  (_ bv 0 n))

(define-rule OrSimplifyRmDups ((x (_ BitVec n)) (xs (_ BitVec n) :list))
  (bvor x x xs)
  (bvor x xs))

(define-rule OrSimplifySimpConsts ((n Int :const) (c1 (_ BitVec n) :const) (c2 (_ BitVec n) :const) (xs (_ BitVec n) :list))
  (bvor c1 c2 xs)
  (bvor (bvor c1 c2) xs))

(define-rule OrSimplifyOnes ((n Int :const) (xs (_ BitVec n) :list))
  (bvand (bvnot (_ bv 0 n)) xs)
  (bvnot (_ bv 0 n)))

(define-rule OrSimplifyRmZeros ((n Int :const) (xs (_ BitVec n) :list))
  (bvand (_ bv 0 n) xs)
  (bvand xs))

(define-rule OrSimplifyCancel ((n Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
  (bvand x (bvnot x) xs)
  (bvnot (_ bv 0 n)))

(define-rule XorSimplifyRmDups ((n Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
  (bvxor x x xs)
  (bvxor (_ bv 0 n) xs))

(define-rule XorSimplifySimpConsts ((n Int :const) (c1 (_ BitVec n) :const) (c2 (_ BitVec n) :const) (xs (_ BitVec n) :list))
  (bvxor c1 c2 xs)
  (bvxor (bvxor c1 c2) xs))

(define-rule XorSimplifyCancel ((n Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
  (bvand x (bvnot x) xs)
  (bvxor (bvnot (_ bv 0 n)) xs))

/******************************************************************************
 * Operator Elimination
 ******************************************************************************/

(define-rule UgtEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
    (bvugt x y)
    (bvult y x))

(define-rule UgeEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
    (bvuge x y)
    (bvule y x))

(define-rule SgtEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
    (bvsgt x y)
    (bvslt y x))

(define-rule SgeEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
    (bvsge x y)
    (bvsle y x))

(define-rule SltEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
    (bvslt x y)
    (let ((pow_two (bvshl (_ bv 1 n) (_ bv (- n 1) n))))
      (bvult (bvadd x pow_two) (bvadd y pow_two))))

(define-rule SleEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
    (bvsle x y)
    (not (bvslt y x)))

(define-rule UleEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
    (bvule x y)
    (not (bvult y x)))

(define-rule CompEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
   (bvcomp x y)
   (ite (= x y) (_ bv 1 1) (_ bv 0 1)))

(define-rule SubEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
    (bvsub x y)
    (bvadd x (bvneg y)))

/* RepeatEliminate: Worth it? */

(define-rule RotateLeftEliminate ((i Int :const) (n Int :const) (x (_ BitVec n)))
    ((_ rotate_left i) x)
    (cond
      ((= i 0) x)
      (concat ((_ extract (- n (+ 1 i)) 0) x) ((_ extract (- n 1) (- n i)) x))))

(define-rule RotateRightEliminate ((i Int :const) (n Int :const) (x (_ BitVec n)))
    ((_ rotate_right i) x)
    (cond
      ((= i 0) x)
      (concat ((_ extract (- i 1) 0) x) ((_ extract (- n 1) i) x))))

/* BVToNatEliminate: COMPLEX */

/* IntToBVEliminate: COMPLEX */

(define-rule NandEliminate ((x (_ BitVec n)) (y (_ BitVec n)))
    (bvnand x y)
    (bvnot (bvand x y)))

(define-rule NorEliminate ((x (_ BitVec n)) (y (_ BitVec n)))
    (bvnor x y)
    (bvnot (bvor x y)))

(define-rule XnorEliminate ((x (_ BitVec n)) (y (_ BitVec n)))
    (bvxnor x y)
    (bvnot (bvxor x y)))

(define-rule SdivEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvsdiv x y)
  (let ((x_lt_0 (= ((_ extract (- n 1) (- n 1)) x) (_ bv 1 1)))
        (y_lt_0 (= ((_ extract (- n 1) (- n 1)) y) (_ bv 1 1)))
        (abs_x (ite x_lt_0 (bvneg x) x))
        (abs_y (ite y_lt_0 (bvneg y) y))
        (x_udiv_y (bvudiv abs_x abs_y)))
    (ite (xor x_lt_0 y_lt_0)
      (bvneg x_udiv_y)
      x_udiv_y)))

(define-rule SremEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvsrem x y)
  (let ((x_lt_0 (= ((_ extract (- n 1) (- n 1)) x) (_ bv 1 1)))
        (y_lt_0 (= ((_ extract (- n 1) (- n 1)) y) (_ bv 1 1)))
        (abs_x (ite x_lt_0 (bvneg x) x))
        (abs_y (ite y_lt_0 (bvneg y) y))
        (x_urem_y (bvurem abs_x abs_y)))
    (ite x_lt_0
      (bvneg x_urem_y)
      x_urem_y)))

(define-rule SmodEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvsmod x y)
  (let ((msb_x ((_ extract (- n 1) (- n 1)) x))
        (msb_y ((_ extract (- n 1) (- n 1)) y))
        (x_lt_0 (= msb_x (_ bv 1 1)))
        (y_lt_0 (= msb_y (_ bv 1 1)))
        (abs_x (ite x_lt_0 (bvneg x) x))
        (abs_y (ite y_lt_0 (bvneg y) y))
        (x_urem_y (bvurem abs_x abs_y)))
    (ite (= x_urem_y (_ bv 0 n))
      x_urem_y
      (ite (and (= msb_x (_ bv 0 1)) (= msb_y (_ bv 0 1)))
        x_urem_y
        (ite (and (= msb_x (_ bv 1 1)) (= msb_y (_ bv 0 1)))
          (bvadd (bvneg x_urem_y) y)
          (ite (and (= msb_x (_ bv 0 1)) (= msb_y (_ bv 1 1)))
            (bvadd x_urem_y y)
            (bvneg x_urem_y)))))))

(define-rule ZeroExtendEliminate ((i Int :const) (x (_ BitVec n)))
  ((_ zero_extend i) x)
  (cond
    ((= i 0) x)
    (concat (_ bv 0 i) x)))

(define-rule SignExtendEliminate ((i Int :const) (n Int :const) (x (_ BitVec n)))
  ((_ sign_extend i) x)
  (cond
    ((= i 0) x)
    (concat ((_ repeat i) ((_ extract (- n 1) (- n 1)) x)) x)))

(define-rule RedorEliminate ((n Int :const) (x (_ BitVec n)))
    (bvredor x)
    (not (= x (_ bv 0 n))))

(define-rule RedandEliminate ((n Int :const) (x (_ BitVec n)))
    (bvredand x)
    (= x (bvnot (_ bv 0 n))))

/******************************************************************************
 * Simplification
 ******************************************************************************/

(define-rule BvIteConstCond ((m (_ BitVec 1) :const) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvite m x y)
  (cond
    ((= m (_ bv 1 1)) x)
    y))

(define-rule BvIteEqualChildren ((c (_ BitVec 1)) (x (_ BitVec m)))
  (bvite c x x)
  x)

(define-rule BvIteConstChildren ((n (_ BitVec 1) :const) (m (_ BitVec 1) :const) (c (_ BitVec 1)))
  (bvite c n m)
  (cond
    ((and (= n (_ bv 1 1)) (= m (_ bv 0 1))) c)
    (true (bvnot c))))

(define-rule BvIteEqualCondThen ((c (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)) (z (_ BitVec n)))
  (bvite c (bvite c x y) z)
  (bvite c x z))

(define-rule BvIteEqualCondElse ((c (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)) (z (_ BitVec n)))
  (bvite c x (bvite c y z))
  (bvite c x z))

(define-rule BvIteMergeThenIf ((c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvite c0 (bvite c1 x y) x)
  (bvite (bvand c0 (bvnot c1)) y x))

(define-rule BvIteMergeElseIf ((c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvite c0 (bvite c1 x y) y)
  (bvite (bvand c0 c1) x y))

(define-rule BvIteMergeThenElse ((c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvite c0 x (bvite c1 x y))
  (bvite (bvand (bvnot c0) (bvnot c1)) y x))

(define-rule BvIteMergeElseElse ((c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvite c0 x (bvite c1 y x))
  (bvite (bvand (bvnot c0) c1) y x))

(define-rule BvComp ((n (_ BitVec 1) :const) (x (_ BitVec 1)))
  (bvcomp n x)
  (cond
    ((= n (_ bv 0 1)) (bvnot x))
    x))

(define-rule ShlByConst ((n Int :const) (m Int :const) (x (_ BitVec m)))
  (bvshl x (_ bv n m))
  (cond
    ((= n 0) x)
    ((>= n m) (_ bv 0 m))
    (concat ((_ extract (- m (+ n 1)) 0) x) (_ bv 0 n))))

(define-rule LshrByConst ((n Int :const) (m Int :const) (x (_ BitVec m)))
  (bvlshr x (_ bv n m))
  (cond
    ((= n 0) x)
    ((>= n m) (_ bv 0 m))
    (concat (_ bv 0 n) ((_ extract (- m 1) n) x))))

(define-rule AshrByConst ((n Int :const) (m Int :const) (x (_ BitVec m)))
  (bvashr x (_ bv n m))
  (cond
    ((= n 0) x)
    ((>= n m) ((_ repeat m) ((_ extract (- m 1) (- m 1)) x)))
    (concat ((_ repeat n) ((_ extract (- m 1) (- m 1)) x)) ((_ extract (- m 1) n) x))))

/*
(define-rule AndPullUp ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (i Int :const) (xs (_ BitVec m) :list) (ys (_ BitVec o) :list) (zs (_ BitVec p) :list))
  (bvand (concat xs (_ bv i n) ys) zs)
  (cond
    ((or (= i 0) (= i 1) (= (_ bv i n) (bvnot (_ bv 0 n))))
      (concat
        (bvand ((_ extract (- p 1) (+ n o)) (bvand zs)) (concat xs))
        (bvand ((_ extract (- (+ n o) 1) o) (bvand zs)) (_ bv i n))
        (bvand ((_ extract (- o 1) 0) (bvand zs)) (concat ys))))))

(define-rule OrPullUp ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (i Int :const) (xs (_ BitVec m) :list) (ys (_ BitVec o) :list) (zs (_ BitVec p) :list))
  (bvor (concat xs (_ bv i n) ys) zs)
  (cond
    ((or (= i 0) (= i 1) (= (_ bv i n) (bvnot (_ bv 0 n))))
      (concat
        (bvor ((_ extract (- p 1) (+ n o)) (bvor zs)) (concat xs))
        (bvor ((_ extract (- (+ n o) 1) o) (bvor zs)) (_ bv i n))
        (bvor ((_ extract (- o 1) 0) (bvor zs)) (concat ys))))))

(define-rule XorPullUp ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (i Int :const) (xs (_ BitVec m) :list) (ys (_ BitVec o) :list) (zs (_ BitVec p) :list))
  (bvxor (concat xs (_ bv i n) ys) zs)
  (cond
    ((or (= i 0) (= i 1) (= (_ bv i n) (bvnot (_ bv 0 n))))
      (concat
        (bvxor ((_ extract (- p 1) (+ n o)) (bvxor zs)) (concat xs))
        (bvxor ((_ extract (- (+ n o) 1) o) (bvxor zs)) (_ bv i n))
        (bvxor ((_ extract (- o 1) 0) (bvxor zs)) (concat ys))))))
*/

(define-rule XorOne ((n Int :const) (xs (_ BitVec n) :list))
  (bvxor (bvnot (_ bv 0 n)) xs)
  (bvxor xs))

(define-rule XorZero ((n Int :const) (xs (_ BitVec n) :list))
  (bvxor (_ bv 0 n) xs)
  (bvxor xs))

(define-rule NotXor ((x (_ BitVec n)) (xs (_ BitVec n) :list))
  (bvnot (bvxor x xs))
  (bvxor (bvnot x) xs))

(define-rule NotIdemp ((x (_ BitVec n)))
    (bvnot (bvnot x))
    x)

(define-rule LtSelfUlt ((x (_ BitVec n)))
    (bvult x x)
    false)

(define-rule LtSelfSlt ((x (_ BitVec n)))
    (bvslt x x)
    false)

(define-rule LteSelfUle ((x (_ BitVec n)))
    (bvule x x)
    true)

(define-rule LteSelfSle ((x (_ BitVec n)))
    (bvsle x x)
    true)

(define-rule ZeroUlt ((n Int :const) (x (_ BitVec n)))
    (bvult (_ bv 0 n) x)
    (not (= (_ bv 0 n) x)))

(define-rule UltZero ((n Int :const) (x (_ BitVec n)))
    (bvult x (_ bv 0 n))
    false)

(define-rule UltOne ((n Int :const) (x (_ BitVec n)))
    (bvult x (_ bv 1 n))
    (= x (_ bv 0 n)))

(define-rule SltZero ((n Int :const) (x (_ BitVec n)))
    (bvslt x (_ bv 0 n))
    (= ((_ extract (- n 1) (- n 1)) x) (_ bv 1 1)))

/* Note: Duplicate of LtSelfUlt */
(define-rule UltSelf ((x (_ BitVec n)))
    (bvult x x)
    false)

(define-rule UleZero ((n Int :const) (x (_ BitVec n)))
    (bvule x (_ bv 0 n))
    (= x (_ bv 0 n)))

/* Note: Duplicate of LteSelfUle */
(define-rule UleSelf ((x (_ BitVec n)))
    (bvule x x)
    true)

(define-rule ZeroUle ((n Int :const) (x (_ BitVec n)))
    (bvule (_ bv 0 n) x)
    true)

(define-rule NotUlt ((x (_ BitVec n)) (y (_ BitVec n)))
    (not (bvult x y))
    (bvule y x))

(define-rule UleMax ((n Int :const) (x (_ BitVec n)))
    (bvult x (bvnot (_ bv 0 n)))
    true)

(define-rule NotUle ((x (_ BitVec n)) (y (_ BitVec n)))
    (not (bvule x y))
    (bvult y x))

/*
(define-rule MultPowX ((n Int :const) (c Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
    (bvmul (_ bv c n) xs)
    (cond 
      ((>= (pow2 c) n) (_ bv 0 n))
      ((< 0 (pow2 c)) (concat ((_ extract (- n (+ (pow2 c) 1)) 0) (bvmul xs)) (_ bv 0 (pow2 c))))))
*/

/* TODO: make pow2 neg */
/*
(define-rule MultPowXNeg ((n Int :const) (c Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
    (bvmul (_ bv c n) xs)
    (cond 
      ((>= (pow2 c) n) (_ bv 0 n))
      ((< 0 (pow2 c)) (concat ((_ extract (- n (+ (pow2 c) 1)) 0) (bvneg (bvmul xs))) (_ bv 0 (pow2 c))))))

(define-rule ExtractMultLeadingBit ((n1 Int :const) (n2 Int :const) (n3 Int :const) (n4 Int :const) (i Int :const) (j Int :const) (c1 Int :const) (c2 Int :const) (xs (_ BitVec n3) :list) (ys (_ BitVec n4) :list))
  ((_ extract i j) (bvmul (concat (_ bv c1 n1) xs) (concat (_ bv c2 n2) ys)))
  (cond
    ((< (- (+ n1 n1 n3 n3) (+ (- n1 (bits c1)) (- n2 (bits c2)))) j) (_ bv 0 (+ n1 n3)))))
*/

(define-rule NegIdemp ((n Int :const) (x (_ BitVec n)))
    (bvneg (bvneg x))
    x)

/* UdivPow2 */
(define-rule UdivPowX ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)))
    (bvudiv x c)
    (cond 
      ((< 0 (pow2 c)) ((_ extract (- n 1) (pow2 c)) x))))

/* TODO: make pow2 neg */
/*
(define-rule UdivPowXNeg ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
    (bvudiv x (_ bv c n))
    (cond 
      ((< 0 (pow2 c)) (bvneg ((_ extract (- n 1) (pow2 c)) x)))))
*/

(define-rule UdivZero ((n Int :const) (x (_ BitVec n)))
    (bvudiv x (_ bv 0 n))
    (bvnot (_ bv 0 n)))

(define-rule UdivOne ((n Int :const) (x (_ BitVec n)))
    (bvudiv x (_ bv 1 n))
    x)

/* UremPow2 */
(define-rule UremPowX ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)))
    (bvurem x c)
    (cond 
      ((< 0 (pow2 c)) ((_ extract (- (pow2 c) 1) 0) x))))

(define-rule UremOne ((n Int :const) (x (_ BitVec n)))
    (bvudiv x (_ bv 1 n))
    (_ bv 0 n))

(define-rule UremSelf ((n Int :const) (x (_ BitVec n)))
    (bvudiv x x)
    (_ bv 0 n))

(define-rule ShiftZeroShl ((n Int :const) (x (_ BitVec n)))
    (bvshl (_ bv 0 n) x)
    (_ bv 0 n))

(define-rule ShiftZeroLshr ((n Int :const) (x (_ BitVec n)))
    (bvlshr (_ bv 0 n) x)
    (_ bv 0 n))

(define-rule ShiftZeroAshr ((n Int :const) (x (_ BitVec n)))
    (bvashr (_ bv 0 n) x)
    (_ bv 0 n))

(define-rule MergeSignExtendSign ((i Int :const) (j Int :const) (n Int :const) (x (_ BitVec n)))
  ((_ sign_extend i) ((_ sign_extend j) x))
  ((_ sign_extend (+ i j)) x))

(define-rule MergeSignExtendZero ((i Int :const) (j Int :const) (n Int :const) (x (_ BitVec n)))
  ((_ sign_extend i) ((_ zero_extend j) x))
  (cond
    ((= j 0) ((_ sign_extend i) x))
    (true ((_ zero_extend (+ i j)) x))))

(define-rule ZeroExtendEqConst ((i Int :const) (n Int :const) (m Int :const) (x (_ BitVec n)))
  (= ((_ zero_extend i) x) (_ bv m n))
  (cond
    ((= ((_ extract (- (+ n m) 1) n) (_ bv m n)) (_ bv 0 n)) (= x ((_ extract (- n 1) 0) (_ bv m n))))
    false))

(define-rule UltPlusOne ( (n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvult x (bvadd y (_ bv 1 n)))
  (and (bvult (bvnot y) x) (not (= y (bvnot (_ bv 0 n))))))

/*
(define-rule MultSltMult ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
  (bvslt (bvmul ) (bvmul ))
  (and (bvult (bvnot y) x) (not (= y (bvnot (_ bv 0 n))))))
*/

/******************************************************************************
 * Experimental
 ******************************************************************************/

/*
(define-rule LteSelfUle ((x (_ BitVec n)))
    (bvule x x)
    true)

(define-rule NegIdemp ((n Int :const) (x (_ BitVec n)))
    (bvneg (bvneg x))
    x)

(define-rule ZeroExtendEliminate ((i Int :const) (x (_ BitVec n)))
  ((_ zero_extend i) x)
  (cond
    ((= i 0) x)
    (concat (_ bv 0 i) x)))


(define-rule UleMax ((n Int :const) (x (_ BitVec n)))
    (bvule x (bvnot (_ bv 0 n)))
    true)

(define-rule AndCancel ((x Bool) (xs Bool :list))
    (and x (not x) xs)
    false)

(define-rule AndRemDups ((x Bool) (xs Bool :list))
    (and x x xs)
    (and xs))

(define-rule IffTrue ((x Bool))
  (= true x)
  x)

(define-rule IffFalse ((x Bool))
  (= true x)
  (not x))

(define-rule IffSelf ((x Bool))
  (= x x)
  true)

(define-rule IffCancel ((x Bool))
  (= x (not x))
  false)
*/

/* Double eq rules */


/*
(define-rule XorTrue ((x Bool))
  (xor true x)
  (not x))

(define-rule XorFalse ((x Bool))
  (xor false x)
  x)

(define-rule XorSelf ((x Bool))
  (xor x x)
  false)

(define-rule XorSelfNeg ((x Bool))
  (xor x (not x))
  true)
*/

/*
(define-rule IffCancel ((x Bool) (xs (List Bool)))
    (and x (not x) xs)
    false)

(define-rule IffCancel ((x Bool) (xs Bool :list))
    (and x (not x) xs)
    false)

; (declare-const x Bool)
; (declare-const xs Bool)
; (assert (not (= (and x (not x) xs) false)))
; (check-sat)
;
; ^^^
; Make argument for why it is sufficient to only check this form

; :list/:multiple

(define-rule IffCancel ((x Bool))
    (! and x x :binary)
    x)

; (and t t s u)
; (and t (and t (and s u)))
; (and (and (and t t) s) u)

; have an attribute for fixed number of children

(define-rule IffCancelTwo ((x Bool))
    (= (not x) x)
    false)

; (declare-rule ...)
; (define-strategy
; ...
; )
*/