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

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

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

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.BoolExpr.toString {α : Type} [ToString α] : BoolExpr α → String

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

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

@[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

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

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)