This module contains the definition of the BitVec fragment that bv_decide internally operates on as BVLogicalExpr. The preprocessing steps of bv_decide reduce all supported BitVec operations to the ones provided in this file. For verification purposes BVLogicalExpr.Sat and BVLogicalExpr.Unsat are provided.

structure Std.Tactic.BVDecide.BVBit : Type

The variable definition used by the bitblaster.

• var : Nat

  A numeric identifier for the BitVec variable.

• w : Nat

  The width of the BitVec variable.

• idx : Fin self.w

  The bit that we take out of the BitVec variable by getLsb.

instance Std.Tactic.BVDecide.instHashableBVBit : Hashable BVBit

Equations

• Std.Tactic.BVDecide.instHashableBVBit = { hash := Std.Tactic.BVDecide.hashBVBit✝ }

instance Std.Tactic.BVDecide.instDecidableEqBVBit : DecidableEq BVBit

Equations

• Std.Tactic.BVDecide.instDecidableEqBVBit = Std.Tactic.BVDecide.decEqBVBit✝

instance Std.Tactic.BVDecide.instReprBVBit : Repr BVBit

Equations

• Std.Tactic.BVDecide.instReprBVBit = { reprPrec := Std.Tactic.BVDecide.reprBVBit✝ }

instance Std.Tactic.BVDecide.instToStringBVBit : ToString BVBit

Equations

• Std.Tactic.BVDecide.instToStringBVBit = { toString := fun (b : Std.Tactic.BVDecide.BVBit) => toString "x" ++ toString b.var ++ toString "[" ++ toString ↑b.idx ++ toString "]" }

instance Std.Tactic.BVDecide.instInhabitedBVBit : Inhabited BVBit

Equations

• Std.Tactic.BVDecide.instInhabitedBVBit = { default := Std.Tactic.BVDecide.BVBit.mk 0 0 }

inductive Std.Tactic.BVDecide.BVBinOp : Type

All supported binary operations on BVExpr.

• and : BVBinOp

  Bitwise and.

• or : BVBinOp

  Bitwise or.

• xor : BVBinOp

  Bitwise xor.

• add : BVBinOp

  Addition.

• mul : BVBinOp

  Multiplication.

• udiv : BVBinOp

  Unsigned division.

• umod : BVBinOp

  Unsigned modulo.

def Std.Tactic.BVDecide.BVBinOp.toString : BVBinOp → String

Equations

• Std.Tactic.BVDecide.BVBinOp.and.toString = "&&"
• Std.Tactic.BVDecide.BVBinOp.or.toString = "||"
• Std.Tactic.BVDecide.BVBinOp.xor.toString = "^"
• Std.Tactic.BVDecide.BVBinOp.add.toString = "+"
• Std.Tactic.BVDecide.BVBinOp.mul.toString = "*"
• Std.Tactic.BVDecide.BVBinOp.udiv.toString = "/ᵤ"
• Std.Tactic.BVDecide.BVBinOp.umod.toString = "%ᵤ"

instance Std.Tactic.BVDecide.BVBinOp.instToString : ToString BVBinOp

Equations

• Std.Tactic.BVDecide.BVBinOp.instToString = { toString := Std.Tactic.BVDecide.BVBinOp.toString }

def Std.Tactic.BVDecide.BVBinOp.eval {w : Nat} : BVBinOp → BitVec w → BitVec w → BitVec w

The semantics for BVBinOp.

Equations

• Std.Tactic.BVDecide.BVBinOp.and.eval = fun (x1 x2 : BitVec w) => x1 &&& x2
• Std.Tactic.BVDecide.BVBinOp.or.eval = fun (x1 x2 : BitVec w) => x1 ||| x2
• Std.Tactic.BVDecide.BVBinOp.xor.eval = fun (x1 x2 : BitVec w) => x1 ^^^ x2
• Std.Tactic.BVDecide.BVBinOp.add.eval = fun (x1 x2 : BitVec w) => x1 + x2
• Std.Tactic.BVDecide.BVBinOp.mul.eval = fun (x1 x2 : BitVec w) => x1 * x2
• Std.Tactic.BVDecide.BVBinOp.udiv.eval = fun (x1 x2 : BitVec w) => x1 / x2
• Std.Tactic.BVDecide.BVBinOp.umod.eval = fun (x1 x2 : BitVec w) => x1 % x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_and {w : Nat} : and.eval = fun (x1 x2 : BitVec w) => x1 &&& x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_or {w : Nat} : or.eval = fun (x1 x2 : BitVec w) => x1 ||| x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_xor {w : Nat} : xor.eval = fun (x1 x2 : BitVec w) => x1 ^^^ x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_add {w : Nat} : add.eval = fun (x1 x2 : BitVec w) => x1 + x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_mul {w : Nat} : mul.eval = fun (x1 x2 : BitVec w) => x1 * x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_udiv {w : Nat} : udiv.eval = fun (x1 x2 : BitVec w) => x1 / x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_umod {w : Nat} : umod.eval = fun (x1 x2 : BitVec w) => x1 % x2

inductive Std.Tactic.BVDecide.BVUnOp : Type

All supported unary operators on BVExpr.

• not : BVUnOp

  Bitwise not.

• shiftLeftConst (n : Nat) : BVUnOp

  Shifting left by a constant value.

  This operation has a dedicated constant representation as shiftLeft can take Nat as a shift amount. We can obviously not bitblast a Nat but still want to support the case where the user shifts by a constant Nat value.

• shiftRightConst (n : Nat) : BVUnOp

  Shifting right by a constant value.

  This operation has a dedicated constant representation as shiftRight can take Nat as a shift amount. We can obviously not bitblast a Nat but still want to support the case where the user shifts by a constant Nat value.

• rotateLeft (n : Nat) : BVUnOp

  Rotating left by a constant value.

• rotateRight (n : Nat) : BVUnOp

  Rotating right by a constant value.

• arithShiftRightConst (n : Nat) : BVUnOp

  Arithmetic shift right by a constant value.

  This operation has a dedicated constant representation as shiftRight can take Nat as a shift amount. We can obviously not bitblast a Nat but still want to support the case where the user shifts by a constant Nat value.

def Std.Tactic.BVDecide.BVUnOp.toString : BVUnOp → String

Equations

• Std.Tactic.BVDecide.BVUnOp.not.toString = "~"
• (Std.Tactic.BVDecide.BVUnOp.shiftLeftConst n).toString = toString "<< " ++ toString n ++ toString ""
• (Std.Tactic.BVDecide.BVUnOp.shiftRightConst n).toString = toString ">> " ++ toString n ++ toString ""
• (Std.Tactic.BVDecide.BVUnOp.rotateLeft n).toString = toString "rotL " ++ toString n ++ toString ""
• (Std.Tactic.BVDecide.BVUnOp.rotateRight n).toString = toString "rotR " ++ toString n ++ toString ""
• (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n).toString = toString ">>a " ++ toString n ++ toString ""

instance Std.Tactic.BVDecide.BVUnOp.instToString : ToString BVUnOp

Equations

• Std.Tactic.BVDecide.BVUnOp.instToString = { toString := Std.Tactic.BVDecide.BVUnOp.toString }

def Std.Tactic.BVDecide.BVUnOp.eval {w : Nat} : BVUnOp → BitVec w → BitVec w

The semantics for BVUnOp.

Equations

• Std.Tactic.BVDecide.BVUnOp.not.eval = fun (x : BitVec w) => ~~~x
• (Std.Tactic.BVDecide.BVUnOp.shiftLeftConst n).eval = fun (x : BitVec w) => x <<< n
• (Std.Tactic.BVDecide.BVUnOp.shiftRightConst n).eval = fun (x : BitVec w) => x >>> n
• (Std.Tactic.BVDecide.BVUnOp.rotateLeft n).eval = fun (x : BitVec w) => x.rotateLeft n
• (Std.Tactic.BVDecide.BVUnOp.rotateRight n).eval = fun (x : BitVec w) => x.rotateRight n
• (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n).eval = fun (x : BitVec w) => x.sshiftRight n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_not {w : Nat} : not.eval = fun (x : BitVec w) => ~~~x

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_shiftLeftConst {n w : Nat} : (shiftLeftConst n).eval = fun (x : BitVec w) => x <<< n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_shiftRightConst {n w : Nat} : (shiftRightConst n).eval = fun (x : BitVec w) => x >>> n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_rotateLeft {n w : Nat} : (rotateLeft n).eval = fun (x : BitVec w) => x.rotateLeft n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_rotateRight {n w : Nat} : (rotateRight n).eval = fun (x : BitVec w) => x.rotateRight n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_arithShiftRightConst {n w : Nat} : (arithShiftRightConst n).eval = fun (x : BitVec w) => x.sshiftRight n

inductive Std.Tactic.BVDecide.BVExpr : Nat → Type

All supported expressions involving BitVec and operations on them.

• var {w : Nat} (idx : Nat) : BVExpr w

  A BitVec variable, referred to through an index.

• const {w : Nat} (val : BitVec w) : BVExpr w

  A constant BitVec value.

• zeroExtend {w : Nat} (v : Nat) (expr : BVExpr w) : BVExpr v

  zero extend a BitVec by some constant amount.

• extract {w : Nat} (start len : Nat) (expr : BVExpr w) : BVExpr len

  Extract a slice from a BitVec.

• bin {w : Nat} (lhs : BVExpr w) (op : BVBinOp) (rhs : BVExpr w) : BVExpr w

  A binary operation on two BVExpr.

• un {w : Nat} (op : BVUnOp) (operand : BVExpr w) : BVExpr w

  A unary operation on two BVExpr.

• append {l r : Nat} (lhs : BVExpr l) (rhs : BVExpr r) : BVExpr (l + r)

  Concatenate two bit vectors.

• replicate {w : Nat} (n : Nat) (expr : BVExpr w) : BVExpr (w * n)

  Concatenate a bit vector with itself n times.

• signExtend {w : Nat} (v : Nat) (expr : BVExpr w) : BVExpr v

  sign extend a BitVec by some constant amount.

• shiftLeft {m n : Nat} (lhs : BVExpr m) (rhs : BVExpr n) : BVExpr m

  shift left by another BitVec expression. For constant shifts there exists a BVUnop.

• shiftRight {m n : Nat} (lhs : BVExpr m) (rhs : BVExpr n) : BVExpr m

  shift right by another BitVec expression. For constant shifts there exists a BVUnop.

• arithShiftRight {m n : Nat} (lhs : BVExpr m) (rhs : BVExpr n) : BVExpr m

  shift right arithmetically by another BitVec expression. For constant shifts there exists a BVUnop.

def Std.Tactic.BVDecide.BVExpr.toString {w : Nat} : BVExpr w → String

Equations

• (Std.Tactic.BVDecide.BVExpr.var idx).toString = toString "var" ++ toString idx ++ toString ""
• (Std.Tactic.BVDecide.BVExpr.const val).toString = toString val
• (Std.Tactic.BVDecide.BVExpr.zeroExtend w expr).toString = toString "(zext " ++ toString w ++ toString " " ++ toString expr.toString ++ toString ")"
• (Std.Tactic.BVDecide.BVExpr.extract start w expr).toString = toString "" ++ toString expr.toString ++ toString "[" ++ toString start ++ toString ", " ++ toString w ++ toString "]"
• (lhs.bin op rhs).toString = toString "(" ++ toString lhs.toString ++ toString " " ++ toString op.toString ++ toString " " ++ toString rhs.toString ++ toString ")"
• (Std.Tactic.BVDecide.BVExpr.un op operand).toString = toString "(" ++ toString op.toString ++ toString " " ++ toString operand.toString ++ toString ")"
• (lhs.append rhs).toString = toString "(" ++ toString lhs.toString ++ toString " ++ " ++ toString rhs.toString ++ toString ")"
• (Std.Tactic.BVDecide.BVExpr.replicate n expr).toString = toString "(replicate " ++ toString n ++ toString " " ++ toString expr.toString ++ toString ")"
• (Std.Tactic.BVDecide.BVExpr.signExtend w expr).toString = toString "(sext " ++ toString w ++ toString " " ++ toString expr.toString ++ toString ")"
• (lhs.shiftLeft rhs).toString = toString "(" ++ toString lhs.toString ++ toString " << " ++ toString rhs.toString ++ toString ")"
• (lhs.shiftRight rhs).toString = toString "(" ++ toString lhs.toString ++ toString " >> " ++ toString rhs.toString ++ toString ")"
• (lhs.arithShiftRight rhs).toString = toString "(" ++ toString lhs.toString ++ toString " >>a " ++ toString rhs.toString ++ toString ")"

instance Std.Tactic.BVDecide.BVExpr.instToString {w : Nat} : ToString (BVExpr w)

Equations

• Std.Tactic.BVDecide.BVExpr.instToString = { toString := Std.Tactic.BVDecide.BVExpr.toString }

structure Std.Tactic.BVDecide.BVExpr.PackedBitVec : Type

Pack a BitVec with its width into a single parameter-less structure.

• w : Nat
• bv : BitVec self.w

@[reducible, inline]

abbrev Std.Tactic.BVDecide.BVExpr.Assignment : Type

The notion of variable assignments for BVExpr.

Equations

• Std.Tactic.BVDecide.BVExpr.Assignment = Lean.RArray Std.Tactic.BVDecide.BVExpr.PackedBitVec

def Std.Tactic.BVDecide.BVExpr.Assignment.get (assign : Assignment) (idx : Nat) : PackedBitVec

Get the value of a BVExpr.var from an Assignment.

Equations

• assign.get idx = Lean.RArray.get assign idx

def Std.Tactic.BVDecide.BVExpr.eval {w : Nat} (assign : Assignment) : BVExpr w → BitVec w

The semantics for BVExpr.

Equations

• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.var idx) = if h : (assign.get idx).w = w then h ▸ (assign.get idx).bv else BitVec.truncate w (assign.get idx).bv
• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.const val) = val
• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.zeroExtend w expr) = BitVec.zeroExtend w (Std.Tactic.BVDecide.BVExpr.eval assign expr)
• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.extract start w expr) = BitVec.extractLsb' start w (Std.Tactic.BVDecide.BVExpr.eval assign expr)
• Std.Tactic.BVDecide.BVExpr.eval assign (lhs.bin op rhs) = op.eval (Std.Tactic.BVDecide.BVExpr.eval assign lhs) (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.un op operand) = op.eval (Std.Tactic.BVDecide.BVExpr.eval assign operand)
• Std.Tactic.BVDecide.BVExpr.eval assign (lhs.append rhs) = Std.Tactic.BVDecide.BVExpr.eval assign lhs ++ Std.Tactic.BVDecide.BVExpr.eval assign rhs
• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.replicate n expr) = BitVec.replicate n (Std.Tactic.BVDecide.BVExpr.eval assign expr)
• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.signExtend w expr) = BitVec.signExtend w (Std.Tactic.BVDecide.BVExpr.eval assign expr)
• Std.Tactic.BVDecide.BVExpr.eval assign (lhs.shiftLeft rhs) = Std.Tactic.BVDecide.BVExpr.eval assign lhs <<< Std.Tactic.BVDecide.BVExpr.eval assign rhs
• Std.Tactic.BVDecide.BVExpr.eval assign (lhs.shiftRight rhs) = Std.Tactic.BVDecide.BVExpr.eval assign lhs >>> Std.Tactic.BVDecide.BVExpr.eval assign rhs
• Std.Tactic.BVDecide.BVExpr.eval assign (lhs.arithShiftRight rhs) = (Std.Tactic.BVDecide.BVExpr.eval assign lhs).sshiftRight' (Std.Tactic.BVDecide.BVExpr.eval assign rhs)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_var {assign : Assignment} {w idx : Nat} : eval assign (var idx) = BitVec.truncate w (assign.get idx).bv

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_const {assign : Assignment} {w✝ : Nat} {val : BitVec w✝} : eval assign (const val) = val

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_zeroExtend {assign : Assignment} {v a✝ : Nat} {expr : BVExpr a✝} : eval assign (zeroExtend v expr) = BitVec.zeroExtend v (eval assign expr)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_extract {assign : Assignment} {start len a✝ : Nat} {expr : BVExpr a✝} : eval assign (extract start len expr) = BitVec.extractLsb' start len (eval assign expr)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_bin {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {op : BVBinOp} {rhs : BVExpr a✝} : eval assign (lhs.bin op rhs) = op.eval (eval assign lhs) (eval assign rhs)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_un {assign : Assignment} {op : BVUnOp} {a✝ : Nat} {operand : BVExpr a✝} : eval assign (un op operand) = op.eval (eval assign operand)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_append {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} : eval assign (lhs.append rhs) = eval assign lhs ++ eval assign rhs

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_replicate {assign : Assignment} {n a✝ : Nat} {expr : BVExpr a✝} : eval assign (replicate n expr) = BitVec.replicate n (eval assign expr)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_signExtend {assign : Assignment} {v a✝ : Nat} {expr : BVExpr a✝} : eval assign (signExtend v expr) = BitVec.signExtend v (eval assign expr)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_shiftLeft {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} : eval assign (lhs.shiftLeft rhs) = eval assign lhs <<< eval assign rhs

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_shiftRight {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} : eval assign (lhs.shiftRight rhs) = eval assign lhs >>> eval assign rhs

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_arithShiftRight {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} : eval assign (lhs.arithShiftRight rhs) = (eval assign lhs).sshiftRight' (eval assign rhs)

inductive Std.Tactic.BVDecide.BVBinPred : Type

Supported binary predicates on BVExpr.

• eq : BVBinPred

  Equality.

• ult : BVBinPred

  Unsigned Less Than

def Std.Tactic.BVDecide.BVBinPred.toString : BVBinPred → String

Equations

• Std.Tactic.BVDecide.BVBinPred.eq.toString = "=="
• Std.Tactic.BVDecide.BVBinPred.ult.toString = "<u"

instance Std.Tactic.BVDecide.BVBinPred.instToString : ToString BVBinPred

Equations

• Std.Tactic.BVDecide.BVBinPred.instToString = { toString := Std.Tactic.BVDecide.BVBinPred.toString }

def Std.Tactic.BVDecide.BVBinPred.eval {w : Nat} : BVBinPred → BitVec w → BitVec w → Bool

The semantics for BVBinPred.

Equations

• Std.Tactic.BVDecide.BVBinPred.eq.eval = fun (x1 x2 : BitVec w) => x1 == x2
• Std.Tactic.BVDecide.BVBinPred.ult.eval = BitVec.ult

@[simp]

theorem Std.Tactic.BVDecide.BVBinPred.eval_eq {w : Nat} : eq.eval = fun (x1 x2 : BitVec w) => x1 == x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinPred.eval_ult {w : Nat} : ult.eval = BitVec.ult

inductive Std.Tactic.BVDecide.BVPred : Type

Supported predicates on BVExpr.

• bin {w : Nat} (lhs : BVExpr w) (op : BVBinPred) (rhs : BVExpr w) : BVPred

  A binary predicate on BVExpr.

• getLsbD {w : Nat} (expr : BVExpr w) (idx : Nat) : BVPred

  Getting a constant LSB from a BitVec.

structure Std.Tactic.BVDecide.BVPred.ExprPair : Type

Pack two BVExpr of equivalent width into one parameter-less structure.

• w : Nat
• lhs : BVExpr self.w
• rhs : BVExpr self.w

def Std.Tactic.BVDecide.BVPred.toString : BVPred → String

Equations

• One or more equations did not get rendered due to their size.
• (Std.Tactic.BVDecide.BVPred.getLsbD expr idx).toString = toString "" ++ toString expr.toString ++ toString "[" ++ toString idx ++ toString "]"

instance Std.Tactic.BVDecide.BVPred.instToString : ToString BVPred

Equations

• Std.Tactic.BVDecide.BVPred.instToString = { toString := Std.Tactic.BVDecide.BVPred.toString }

def Std.Tactic.BVDecide.BVPred.eval (assign : BVExpr.Assignment) : BVPred → Bool

The semantics for BVPred.

Equations

• Std.Tactic.BVDecide.BVPred.eval assign (Std.Tactic.BVDecide.BVPred.bin lhs op rhs) = op.eval (Std.Tactic.BVDecide.BVExpr.eval assign lhs) (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
• Std.Tactic.BVDecide.BVPred.eval assign (Std.Tactic.BVDecide.BVPred.getLsbD expr idx) = (Std.Tactic.BVDecide.BVExpr.eval assign expr).getLsbD idx

@[simp]

theorem Std.Tactic.BVDecide.BVPred.eval_bin {assign : BVExpr.Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {op : BVBinPred} {rhs : BVExpr a✝} : eval assign (bin lhs op rhs) = op.eval (BVExpr.eval assign lhs) (BVExpr.eval assign rhs)

@[simp]

theorem Std.Tactic.BVDecide.BVPred.eval_getLsbD {assign : BVExpr.Assignment} {a✝ : Nat} {expr : BVExpr a✝} {idx : Nat} : eval assign (getLsbD expr idx) = (BVExpr.eval assign expr).getLsbD idx

@[reducible, inline]

abbrev Std.Tactic.BVDecide.BVLogicalExpr : Type

Boolean substructure of problems involving predicates on BitVec as atoms.

Equations

• Std.Tactic.BVDecide.BVLogicalExpr = Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred

def Std.Tactic.BVDecide.BVLogicalExpr.eval (assign : BVExpr.Assignment) (expr : BVLogicalExpr) : Bool

The semantics of boolean problems involving BitVec predicates as atoms.

Equations

• Std.Tactic.BVDecide.BVLogicalExpr.eval assign expr = Std.Tactic.BVDecide.BoolExpr.eval (fun (x : Std.Tactic.BVDecide.BVPred) => Std.Tactic.BVDecide.BVPred.eval assign x) expr

@[simp]

theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_literal {assign : BVExpr.Assignment} {pred : BVPred} : eval assign (BoolExpr.literal pred) = BVPred.eval assign pred

@[simp]

theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_const {assign : BVExpr.Assignment} {b : Bool} : eval assign (BoolExpr.const b) = b

@[simp]

theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_not {assign : BVExpr.Assignment} {x : BoolExpr BVPred} : eval assign x.not = !eval assign x

@[simp]

theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_gate {assign : BVExpr.Assignment} {g : Gate} {x y : BoolExpr BVPred} : eval assign (BoolExpr.gate g x y) = g.eval (eval assign x) (eval assign y)

@[simp]

theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_ite {assign : BVExpr.Assignment} {d l r : BoolExpr BVPred} : eval assign (d.ite l r) = bif eval assign d then eval assign l else eval assign r

def Std.Tactic.BVDecide.BVLogicalExpr.Sat (x : BVLogicalExpr) (assign : BVExpr.Assignment) : Prop

Equations

• x.Sat assign = (Std.Tactic.BVDecide.BVLogicalExpr.eval assign x = true)

def Std.Tactic.BVDecide.BVLogicalExpr.Unsat (x : BVLogicalExpr) : Prop

Equations

• x.Unsat = ∀ (f : Std.Tactic.BVDecide.BVExpr.Assignment), Std.Tactic.BVDecide.BVLogicalExpr.eval f x = false

theorem Std.Tactic.BVDecide.BVLogicalExpr.sat_and {x y : BVLogicalExpr} {assign : BVExpr.Assignment} (hx : x.Sat assign) (hy : y.Sat assign) : Sat (BoolExpr.gate Gate.and x y) assign

theorem Std.Tactic.BVDecide.BVLogicalExpr.sat_true {assign : BVExpr.Assignment} : Sat (BoolExpr.const true) assign