structure BitVec.Literal : Type

A bit-vector literal

• n : Nat

  Size.

• value : BitVec self.n

  Actual value.

instance BitVec.instDecidableEqLiteral : DecidableEq Literal

instance BitVec.instReprLiteral : Repr Literal

def BitVec.fromExpr? (e : Lean.Expr) : Lean.Meta.SimpM (Option Literal)

Try to convert OfNat.ofNat/BitVec.OfNat application into a bitvector literal.

@[inline]

def BitVec.reduceUnary (declName : Lean.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing homogeneous unary bitvector operators.

@[inline]

def BitVec.reduceBin (declName : Lean.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n → BitVec n) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing homogeneous binary bitvector operators.

@[inline]

def BitVec.reduceExtend (declName : Lean.Name) (op : {n : Nat} → (m : Nat) → BitVec n → BitVec m) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Simplification procedure for setWidth, zeroExtend and signExtend on BitVecs.

@[inline]

def BitVec.reduceGetBit (declName : Lean.Name) (op : {n : Nat} → BitVec n → Nat → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing bitvector functions such as getLsb and getMsb.

@[inline]

def BitVec.reduceShift (declName : Lean.Name) (arity : Nat) (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing bitvector functions such as shiftLeft and rotateRight.

@[inline]

def BitVec.reduceShiftWithBitVecLit (declName : Lean.Name) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing x <<< i and x >>> i where i is a bitvector literal, into one that is a natural number literal.

@[inline]

def BitVec.reduceBinPred (declName : Lean.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Helper function for reducing bitvector predicates.

@[inline]

def BitVec.reduceBoolPred (declName : Lean.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def BitVec.reduceNeg : Lean.Meta.Simp.DSimproc

Simplification procedure for negation of BitVecs.

def BitVec.reduceNot : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise not of BitVecs.

def BitVec.reduceAbs : Lean.Meta.Simp.DSimproc

Simplification procedure for absolute value of BitVecs.

def BitVec.reduceAnd : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise and of BitVecs.

def BitVec.reduceOr : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise or of BitVecs.

def BitVec.reduceXOr : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise xor of BitVecs.

def BitVec.reduceAdd : Lean.Meta.Simp.DSimproc

Simplification procedure for addition of BitVecs.

def BitVec.reduceMul : Lean.Meta.Simp.DSimproc

Simplification procedure for multiplication of BitVecs.

def BitVec.reduceSub : Lean.Meta.Simp.DSimproc

Simplification procedure for subtraction of BitVecs.

def BitVec.reduceDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for division of BitVecs.

def BitVec.reduceMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the modulo operation on BitVecs.

def BitVec.reduceUMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the unsigned modulo operation on BitVecs.

def BitVec.reduceUDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned division of BitVecs.

def BitVec.reduceSMTUDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for division of BitVecs using the SMT-LIB conventions.

def BitVec.reduceSMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the signed modulo operation on BitVecs.

def BitVec.reduceSRem : Lean.Meta.Simp.DSimproc

Simplification procedure for signed remainder of BitVecs.

def BitVec.reduceSDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for signed t-division of BitVecs.

def BitVec.reduceSMTSDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for signed division of BitVecs using the SMT-LIB conventions.

def BitVec.reduceGetLsb : Lean.Meta.Simp.DSimproc

Simplification procedure for getLsb (lowest significant bit) on BitVec.

def BitVec.reduceGetMsb : Lean.Meta.Simp.DSimproc

Simplification procedure for getMsb (most significant bit) on BitVec.

def BitVec.reduceGetElem : Lean.Meta.Simp.DSimproc

Simplification procedure for getElem on BitVec.

def BitVec.reduceShiftLeft : Lean.Meta.Simp.DSimproc

Simplification procedure for shift left on BitVec.

def BitVec.reduceUShiftRight : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned shift right on BitVec.

def BitVec.reduceSShiftRight : Lean.Meta.Simp.DSimproc

Simplification procedure for signed shift right on BitVec.

def BitVec.reduceHShiftLeft : Lean.Meta.Simp.DSimproc

Simplification procedure for shift left on BitVec.

def BitVec.reduceHShiftLeft' : Lean.Meta.Simp.DSimproc

Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.

def BitVec.reduceHShiftRight : Lean.Meta.Simp.DSimproc

Simplification procedure for shift right on BitVec.

def BitVec.reduceHShiftRight' : Lean.Meta.Simp.DSimproc

Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.

def BitVec.reduceRotateLeft : Lean.Meta.Simp.DSimproc

Simplification procedure for rotate left on BitVec.

def BitVec.reduceRotateRight : Lean.Meta.Simp.DSimproc

Simplification procedure for rotate right on BitVec.

def BitVec.reduceAppend : Lean.Meta.Simp.DSimproc

Simplification procedure for append on BitVec.

def BitVec.reduceCast : Lean.Meta.Simp.DSimproc

Simplification procedure for casting BitVecs along an equality of the size.

def BitVec.reduceToNat : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.toNat.

def BitVec.reduceToInt : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.toInt.

def BitVec.reduceOfInt : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.ofInt.

def BitVec.reduceOfNat : Lean.Meta.Simp.DSimproc

Simplification procedure for ensuring BitVec.ofNat literals are normalized.

def BitVec.reduceEq : Lean.Meta.Simp.Simproc

Simplification procedure for = on BitVecs.

def BitVec.reduceNe : Lean.Meta.Simp.Simproc

Simplification procedure for ≠ on BitVecs.

def BitVec.reduceBEq : Lean.Meta.Simp.DSimproc

Simplification procedure for == on BitVecs.

def BitVec.reduceBNe : Lean.Meta.Simp.DSimproc

Simplification procedure for != on BitVecs.

def BitVec.reduceLT : Lean.Meta.Simp.Simproc

Simplification procedure for < on BitVecs.

def BitVec.reduceLE : Lean.Meta.Simp.Simproc

Simplification procedure for ≤ on BitVecs.

def BitVec.reduceGT : Lean.Meta.Simp.Simproc

Simplification procedure for > on BitVecs.

def BitVec.reduceGE : Lean.Meta.Simp.Simproc

Simplification procedure for ≥ on BitVecs.

def BitVec.reduceULT : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned less than ult on BitVecs.

def BitVec.reduceULE : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned less than or equal ule on BitVecs.

def BitVec.reduceSLT : Lean.Meta.Simp.DSimproc

Simplification procedure for signed less than slt on BitVecs.

def BitVec.reduceSLE : Lean.Meta.Simp.DSimproc

Simplification procedure for signed less than or equal sle on BitVecs.

def BitVec.reduceSetWidth' : Lean.Meta.Simp.DSimproc

Simplification procedure for setWidth' on BitVecs.

def BitVec.reduceShiftLeftZeroExtend : Lean.Meta.Simp.DSimproc

Simplification procedure for shiftLeftZeroExtend on BitVecs.

def BitVec.reduceExtracLsb' : Lean.Meta.Simp.DSimproc

Simplification procedure for extractLsb' on BitVecs.

def BitVec.reduceReplicate : Lean.Meta.Simp.DSimproc

Simplification procedure for replicate on BitVecs.

def BitVec.reduceSetWidth : Lean.Meta.Simp.DSimproc

Simplification procedure for setWidth on BitVecs.

def BitVec.reduceZeroExtend : Lean.Meta.Simp.DSimproc

Simplification procedure for zeroExtend on BitVecs.

def BitVec.reduceSignExtend : Lean.Meta.Simp.DSimproc

Simplification procedure for signExtend on BitVecs.

def BitVec.reduceAllOnes : Lean.Meta.Simp.DSimproc

Simplification procedure for allOnes

def BitVec.reduceBitVecOfFin : Lean.Meta.Simp.DSimproc

def BitVec.reduceBitVecToFin : Lean.Meta.Simp.DSimproc

@[inline]

def BitVec.reduceShiftShift (declName thmName : Lean.Name) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Helper function for reducing (x <<< i) <<< j (and (x >>> i) >>> j) where i and j are natural number literals.

def BitVec.reduceShiftLeftShiftLeft : Lean.Meta.Simp.Simproc

def BitVec.reduceShiftRightShiftRight : Lean.Meta.Simp.Simproc