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.

source
inductive Std.Tactic.BVDecide.Gate :
Type

- and : Gate
- xor : Gate
- beq : Gate
- or : Gate

Instances For

source
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 = "||"

Instances For

source
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

Instances For

source
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 α

Instances For

source
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 ++ ")"

Instances For

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

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

source
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

Instances For

source
@[simp]
theorem Std.Tactic.BVDecide.BoolExpr.eval_literal {α✝ : Type} {a : α✝ → Bool} {l : α✝} :
eval a (literal l) = a l
source
@[simp]
theorem Std.Tactic.BVDecide.BoolExpr.eval_const {α✝ : Type} {a : α✝ → Bool} {b : Bool} :
eval a (const b) = b
source
@[simp]
theorem Std.Tactic.BVDecide.BoolExpr.eval_not {α✝ : Type} {a : α✝ → Bool} {x : BoolExpr α✝} :
eval a x.not = !eval a x
source
@[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)
source
@[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
source
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)

Instances For

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

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

Instances For

source
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)
source
theorem Std.Tactic.BVDecide.BoolExpr.sat_true {α : Type} {a : α → Bool} :
Sat a (const true)