This module contains the definition of a generic boolean substructure for SMT problems with BoolExpr. For verification purposes BoolExpr.Sat and BoolExpr.Unsat are provided.

inductive Std.Tactic.BVDecide.Gate : Type

• and : Gate
• xor : Gate
• beq : Gate
• or : Gate

@[instance_reducible]

instance Std.Tactic.BVDecide.instDecidableEqGate : DecidableEq Gate

Equations

• Std.Tactic.BVDecide.instDecidableEqGate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Std.Tactic.BVDecide.instHashableGate.hash : Gate → UInt64

Equations

• Std.Tactic.BVDecide.instHashableGate.hash Std.Tactic.BVDecide.Gate.and = 0
• Std.Tactic.BVDecide.instHashableGate.hash Std.Tactic.BVDecide.Gate.xor = 1
• Std.Tactic.BVDecide.instHashableGate.hash Std.Tactic.BVDecide.Gate.beq = 2
• Std.Tactic.BVDecide.instHashableGate.hash Std.Tactic.BVDecide.Gate.or = 3

@[instance_reducible]

instance Std.Tactic.BVDecide.instHashableGate : Hashable Gate

Equations

• Std.Tactic.BVDecide.instHashableGate = { hash := Std.Tactic.BVDecide.instHashableGate.hash }

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

Equations

• Std.Tactic.BVDecide.Gate.and.toString = "&&"
• Std.Tactic.BVDecide.Gate.xor.toString = "^^"
• Std.Tactic.BVDecide.Gate.beq.toString = "=="
• Std.Tactic.BVDecide.Gate.or.toString = "||"

def Std.Tactic.BVDecide.Gate.eval : Gate → Bool → Bool → Bool

Equations

• Std.Tactic.BVDecide.Gate.and.eval = fun (x1 x2 : Bool) => x1 && x2
• Std.Tactic.BVDecide.Gate.xor.eval = fun (x1 x2 : Bool) => x1 ^^ x2
• Std.Tactic.BVDecide.Gate.beq.eval = fun (x1 x2 : Bool) => x1 == x2
• Std.Tactic.BVDecide.Gate.or.eval = fun (x1 x2 : Bool) => x1 || x2

inductive Std.Tactic.BVDecide.BoolExpr (α : Type) : Type

• literal {α : Type} : α → BoolExpr α
• const {α : Type} : Bool → BoolExpr α
• not {α : Type} : BoolExpr α → BoolExpr α
• gate {α : Type} : Gate → BoolExpr α → BoolExpr α → BoolExpr α
• ite {α : Type} : BoolExpr α → BoolExpr α → BoolExpr α → BoolExpr α

def Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : BoolExpr α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.literal a) (Std.Tactic.BVDecide.BoolExpr.literal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.literal a) (Std.Tactic.BVDecide.BoolExpr.const a_1) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.literal a) a_1.not = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.literal a) (Std.Tactic.BVDecide.BoolExpr.gate a_1 a_2 a_3) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.literal a) (a_1.ite a_2 a_3) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.const a) (Std.Tactic.BVDecide.BoolExpr.literal a_1) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.const a) (Std.Tactic.BVDecide.BoolExpr.const b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.const a) a_1.not = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.const a) (Std.Tactic.BVDecide.BoolExpr.gate a_1 a_2 a_3) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.const a) (a_1.ite a_2 a_3) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq a.not (Std.Tactic.BVDecide.BoolExpr.literal a_1) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq a.not (Std.Tactic.BVDecide.BoolExpr.const a_1) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq a.not b.not = if h : a = b then h ▸ have inst := Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq a a; isTrue ⋯ else isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq a.not (Std.Tactic.BVDecide.BoolExpr.gate a_1 a_2 a_3) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq a.not (a_1.ite a_2 a_3) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.gate a a_1 a_2) (Std.Tactic.BVDecide.BoolExpr.literal a_3) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.gate a a_1 a_2) (Std.Tactic.BVDecide.BoolExpr.const a_3) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.gate a a_1 a_2) a_3.not = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (Std.Tactic.BVDecide.BoolExpr.gate a a_1 a_2) (a_3.ite a_4 a_5) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (a.ite a_1 a_2) (Std.Tactic.BVDecide.BoolExpr.literal a_3) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (a.ite a_1 a_2) (Std.Tactic.BVDecide.BoolExpr.const a_3) = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (a.ite a_1 a_2) a_3.not = isFalse ⋯
• Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq (a.ite a_1 a_2) (Std.Tactic.BVDecide.BoolExpr.gate a_3 a_4 a_5) = isFalse ⋯

@[instance_reducible]

instance Std.Tactic.BVDecide.instDecidableEqBoolExpr {α✝ : Type} [DecidableEq α✝] : DecidableEq (BoolExpr α✝)

Equations

• Std.Tactic.BVDecide.instDecidableEqBoolExpr = Std.Tactic.BVDecide.instDecidableEqBoolExpr.decEq

def Std.Tactic.BVDecide.instHashableBoolExpr.hash {α✝ : Type} [Hashable α✝] : BoolExpr α✝ → UInt64

Equations

• One or more equations did not get rendered due to their size.
• Std.Tactic.BVDecide.instHashableBoolExpr.hash (Std.Tactic.BVDecide.BoolExpr.literal a) = mixHash 0 (hash a)
• Std.Tactic.BVDecide.instHashableBoolExpr.hash (Std.Tactic.BVDecide.BoolExpr.const a) = mixHash 1 (hash a)
• Std.Tactic.BVDecide.instHashableBoolExpr.hash a.not = mixHash 2 (Std.Tactic.BVDecide.instHashableBoolExpr.hash a)

@[instance_reducible]

instance Std.Tactic.BVDecide.instHashableBoolExpr {α✝ : Type} [Hashable α✝] : Hashable (BoolExpr α✝)

Equations

• Std.Tactic.BVDecide.instHashableBoolExpr = { hash := Std.Tactic.BVDecide.instHashableBoolExpr.hash }

def Std.Tactic.BVDecide.BoolExpr.toString {α : Type} [ToString α] : BoolExpr α → String

Equations

• (Std.Tactic.BVDecide.BoolExpr.literal a).toString = toString a
• (Std.Tactic.BVDecide.BoolExpr.const b).toString = toString b
• x_1.not.toString = "!" ++ x_1.toString
• (Std.Tactic.BVDecide.BoolExpr.gate g x_1 y).toString = "(" ++ x_1.toString ++ " " ++ g.toString ++ " " ++ y.toString ++ ")"
• (d.ite l r).toString = "(if " ++ d.toString ++ " " ++ l.toString ++ " " ++ r.toString ++ ")"

@[instance_reducible]

instance Std.Tactic.BVDecide.BoolExpr.instToString {α : Type} [ToString α] : ToString (BoolExpr α)

Equations

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

def Std.Tactic.BVDecide.BoolExpr.eval {α : Type} (a : α → Bool) : BoolExpr α → Bool

Equations

• Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.literal a_1) = a a_1
• Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.const b) = b
• Std.Tactic.BVDecide.BoolExpr.eval a x_1.not = !Std.Tactic.BVDecide.BoolExpr.eval a x_1
• Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.gate g x_1 y) = g.eval (Std.Tactic.BVDecide.BoolExpr.eval a x_1) (Std.Tactic.BVDecide.BoolExpr.eval a y)
• Std.Tactic.BVDecide.BoolExpr.eval a (d.ite l r) = bif Std.Tactic.BVDecide.BoolExpr.eval a d then Std.Tactic.BVDecide.BoolExpr.eval a l else Std.Tactic.BVDecide.BoolExpr.eval a r

@[simp]

theorem Std.Tactic.BVDecide.BoolExpr.eval_literal {α✝ : Type} {a : α✝ → Bool} {l : α✝} : eval a (literal l) = a l

@[simp]

theorem Std.Tactic.BVDecide.BoolExpr.eval_const {α✝ : Type} {a : α✝ → Bool} {b : Bool} : eval a (const b) = b

@[simp]

theorem Std.Tactic.BVDecide.BoolExpr.eval_not {α✝ : Type} {a : α✝ → Bool} {x : BoolExpr α✝} : eval a x.not = !eval a x

@[simp]

theorem Std.Tactic.BVDecide.BoolExpr.eval_gate {α✝ : Type} {a : α✝ → Bool} {g : Gate} {x y : BoolExpr α✝} : eval a (gate g x y) = g.eval (eval a x) (eval a y)

@[simp]

theorem Std.Tactic.BVDecide.BoolExpr.eval_ite {α✝ : Type} {a : α✝ → Bool} {d l r : BoolExpr α✝} : eval a (d.ite l r) = bif eval a d then eval a l else eval a r

def Std.Tactic.BVDecide.BoolExpr.Sat {α : Type} (a : α → Bool) (x : BoolExpr α) : Prop

Equations

• Std.Tactic.BVDecide.BoolExpr.Sat a x = (Std.Tactic.BVDecide.BoolExpr.eval a x = true)

def Std.Tactic.BVDecide.BoolExpr.Unsat {α : Type} (x : BoolExpr α) : Prop

Equations

• x.Unsat = ∀ (f : α → Bool), Std.Tactic.BVDecide.BoolExpr.eval f x = false

theorem Std.Tactic.BVDecide.BoolExpr.sat_and {α : Type} {x y : BoolExpr α} {a : α → Bool} (hx : Sat a x) (hy : Sat a y) : Sat a (gate Gate.and x y)

theorem Std.Tactic.BVDecide.BoolExpr.sat_true {α : Type} {a : α → Bool} : Sat a (const true)