Documentation

Validator.StateSetFormalism.Bdd

structure Validator.BDD (n : ℕ) :

vars : VarSet' n

Instances For

instance Validator.instDecidableEqBDD {n✝ : ℕ} :

DecidableEq (BDD n✝)

Equations

Validator.instDecidableEqBDD = Validator.instDecidableEqBDD.decEq

def Validator.instDecidableEqBDD.decEq {n✝ : ℕ} (x✝ x✝¹ : BDD n✝) :

Decidable (x✝ = x✝¹)

Equations

Validator.instDecidableEqBDD.decEq { vars := a } { vars := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

def Validator.instReprBDD.repr {n✝ : ℕ} :

BDD n✝ → ℕ → Std.Format

Equations

Validator.instReprBDD.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "vars" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.vars)).group) " }"

Instances For

instance Validator.instReprBDD {n✝ : ℕ} :

Repr (BDD n✝)

Equations

Validator.instReprBDD = { reprPrec := Validator.instReprBDD.repr }

def Validator.BDD.models {n : ℕ} (φ : BDD n) :

Formula.Models n

Equations

φ.models = sorry

Instances For

instance Validator.BDD.instFormula {n : ℕ} :

Formula n (BDD n)

Equations

Validator.BDD.instFormula = { vars := fun (φ : Validator.BDD n) => φ.vars, models := Validator.BDD.models, models_equiv_right := ⋯ }

instance Validator.BDD.instTop {n : ℕ} :

Formula.Top n (BDD n)

Equations

Validator.BDD.instTop = { top := sorry, top_correct := ⋯ }

instance Validator.BDD.instBot {n : ℕ} :

Formula.Bot n (BDD n)

Equations

Validator.BDD.instBot = { bot := sorry, bot_correct := ⋯ }

instance Validator.BDD.instClausalEntailment {n : ℕ} :

Formula.ClausalEntailment n (BDD n)

Equations

Validator.BDD.instClausalEntailment = { entails := sorry, entails_correct := ⋯ }

instance Validator.BDD.instImplicant {n : ℕ} :

Formula.Implicant n (BDD n)

Equations

Validator.BDD.instImplicant = { entails := fun (δ : Validator.Formula.Cube n) (φ : Validator.BDD n) => sorry, entails_correct := ⋯ }

instance Validator.BDD.instSententialEntailment {n : ℕ} :

Formula.SententialEntailment n (BDD n)

Equations

Validator.BDD.instSententialEntailment = { entails := sorry, entails_correct := ⋯ }

instance Validator.BDD.instBoundedConjuction {n : ℕ} :

Formula.BoundedConjuction n (BDD n)

Equations

Validator.BDD.instBoundedConjuction = { and := sorry, and_correct := ⋯ }

instance Validator.BDD.instBoundedDisjunction {n : ℕ} :

Formula.BoundedDisjunction n (BDD n)

Equations

Validator.BDD.instBoundedDisjunction = { or := sorry, or_correct := ⋯ }

instance Validator.BDD.instOfPartialModel {n : ℕ} :

Formula.OfPartialModel n (BDD n)

Equations

Validator.BDD.instOfPartialModel = { ofPartialModel := sorry, ofPartialModel_correct := ⋯ }

instance Validator.BDD.instRename {n : ℕ} :

Formula.Rename n (BDD n)

Equations

Validator.BDD.instRename = { rename := sorry, rename_correct := ⋯ }