structure Validator.BDD (n : ℕ) : Type

• vars : STRIPS.VarSet n
• bdd : BDD
• nvars_prop : (bdd self).nvars = n
• vars_prop (i : Fin n) : (bdd self).DependsOn ↑i → i ∈ vars self

@[implicit_reducible]

instance Validator.BDD.instFormula {n : ℕ} : Formula n (BDD n)

Equations

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

@[implicit_reducible]

instance Validator.BDD.instTop {n : ℕ} : Formula.Top n (BDD n)

Equations

• Validator.BDD.instTop = { top := { vars := ∅, bdd := Validator.BDD.top_bdd✝ n, nvars_prop := ⋯, vars_prop := ⋯ }, models_top := ⋯ }

@[implicit_reducible]

instance Validator.BDD.instBot {n : ℕ} : Formula.Bot n (BDD n)

Equations

• Validator.BDD.instBot = { bot := { vars := ∅, bdd := Validator.BDD.bot_bdd✝ n, nvars_prop := ⋯, vars_prop := ⋯ }, vars_bot := ⋯, models_bot := ⋯ }

@[implicit_reducible]

instance Validator.BDD.instConsistency {n : ℕ} : Formula.Consistency n (BDD n)

Equations

• Validator.BDD.instConsistency = { consistent := fun (φ : Validator.BDD n) => decide ¬(Validator.BDD.bdd✝ φ).SemanticEquiv (BDD.const false), consistent_iff := ⋯ }

@[implicit_reducible]

instance Validator.BDD.instBoundedConjuction {n : ℕ} : Formula.BoundedConjuction n (BDD n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.BDD.instBoundedDisjunction {n : ℕ} : Formula.BoundedDisjunction n (BDD n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.BDD.instSententialEntailment {n : ℕ} : Formula.SententialEntailment n (BDD n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.BDD.instClausalEntailment {n : ℕ} : Formula.ClausalEntailment n (BDD n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.BDD.instImplicant {n : ℕ} : Formula.Implicant n (BDD n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Validator.BDD.instOfPartialModel {n : ℕ} : Formula.OfPartialModel n (BDD n)

Equations

• Validator.BDD.instOfPartialModel = { ofPartialModel := fun (M : Validator.Formula.PartialModel n) => Validator.BDD.ofCube✝ M.toCube, vars_ofPartialModel := ⋯, models_ofPartialModel := ⋯ }

@[implicit_reducible]

instance Validator.BDD.instRename {n : ℕ} : Formula.Rename n (BDD n)

Equations

• One or more equations did not get rendered due to their size.

def Validator.BDD.parseBDD {n : ℕ} (h : IO.FS.Handle) : IO { B : BDD (2 * n) // (Formula.vars B).IsUnprimed }

Equations

• One or more equations did not get rendered due to their size.