Documentation

Trestle.Data.Cnf.Basic

def Trestle.Clause.toPropFun {L : Type u} {ν : Type v} [LitVar L ν] (C : Clause L) :

Model.PropFun ν

Equations

C.toPropFun = Trestle.Model.PropFun.any (Multiset.map Trestle.LitVar.toPropFun ↑C.toList)

Instances For

instance Trestle.Clause.instCoeToPropFun {L : Type u} {ν : Type v} [LitVar L ν] :

CoeHead (Clause L) (Model.PropFun ν)

Equations

Trestle.Clause.instCoeToPropFun = { coe := Trestle.Clause.toPropFun }

theorem Trestle.Clause.mem_semVars_toPropFun {L : Type u} {ν : Type v} [LitVar L ν] [DecidableEq ν] (x : ν) (C : Clause L) :

x ∈ C.toPropFun.semVars → ∃ l ∈ C, LitVar.toVar l = x

theorem Trestle.Clause.satisfies_iff {L : Type u} {ν : Type v} [LitVar L ν] {τ : Model.PropAssignment ν} {C : Clause L} :

τ ⊨ C.toPropFun ↔ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l

theorem Trestle.Clause.tautology_iff {L : Type u} {ν : Type v} [LitVar L ν] [DecidableEq ν] [LawfulLitVar L ν] (C : Clause L) :

C.toPropFun = ⊤ ↔ ∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂

@[simp]

theorem Trestle.Clause.toPropFun_or {L : Type u} {ν : Type v} [LitVar L ν] (c1 c2 : Clause L) :

(c1.or c2).toPropFun = c1.toPropFun ⊔ c2.toPropFun

@[simp]

theorem Trestle.Clause.toPropFun_map {L : Type u} {ν : Type v} [LitVar L ν] {L' : Type u_1} {ν' : Type u_2} [LitVar L' ν'] [LawfulLitVar L' ν'] (f : ν → ν') (c : Clause L) :

(map L' f c).toPropFun = Model.PropFun.map f c.toPropFun

@[simp]

theorem Trestle.Clause.toPropFun_empty {L : Type u} {ν : Type v} [LitVar L ν] :

toPropFun #[] = ⊥

@[simp]

theorem Trestle.Clause.toPropFun_nil {L : Type u} {ν : Type v} [LitVar L ν] :

toPropFun { toList := [] } = ⊥

@[simp]

theorem Trestle.Clause.toPropFun_cons {L : Type u} {ν : Type v} [LitVar L ν] (l : L) (C : List L) :

toPropFun { toList := l :: C } = LitVar.toPropFun l ⊔ toPropFun { toList := C }

CNF #

def Trestle.Cnf.toPropFun {L : Type u} {ν : Type v} [LitVar L ν] (φ : Cnf L) :

Model.PropFun ν

Equations

φ.toPropFun = Trestle.Model.PropFun.all ↑(List.map Trestle.Clause.toPropFun φ.toList)

Instances For

theorem Trestle.Cnf.semVars_toPropFun {L : Type u} {ν : Type v} [LitVar L ν] {v : ν} [DecidableEq ν] (F : Cnf L) :

v ∈ F.toPropFun.semVars → ∃ C ∈ F, ∃ l ∈ C, LitVar.toVar l = v

instance Trestle.Cnf.instCoeHeadPropFun {L : Type u} {ν : Type v} [LitVar L ν] :

CoeHead (Cnf L) (Model.PropFun ν)

Equations

Trestle.Cnf.instCoeHeadPropFun = { coe := Trestle.Cnf.toPropFun }

theorem Trestle.Cnf.mem_semVars_toPropFun {L : Type u} {ν : Type v} [LitVar L ν] [DecidableEq ν] (x : ν) (F : Cnf L) :

x ∈ F.toPropFun.semVars → ∃ C ∈ F, x ∈ C.toPropFun.semVars

theorem Trestle.Cnf.satisfies_iff {L : Type u} {ν : Type v} [LitVar L ν] {τ : Model.PropAssignment ν} {φ : Cnf L} :

τ ⊨ φ.toPropFun ↔ ∀ C ∈ φ, τ ⊨ C.toPropFun

@[simp]

theorem Trestle.Cnf.toPropFun_addClause {L : Type u} {ν : Type v} [LitVar L ν] (C : Clause L) (f : Cnf L) :

(f.addClause C).toPropFun = f.toPropFun ⊓ C.toPropFun

@[simp]

theorem Trestle.Cnf.toPropFun_and {L : Type u} {ν : Type v} [LitVar L ν] (f1 f2 : Cnf L) :

(f1.and f2).toPropFun = f1.toPropFun ⊓ f2.toPropFun

@[simp]

theorem Trestle.Cnf.toPropFun_not {L : Type u} {ν : Type v} [LitVar L ν] (c : Clause L) [LawfulLitVar L ν] :

(not c).toPropFun = c.toPropFunᶜ

@[simp]

theorem Trestle.Cnf.toPropFun_any {L : Type u} {ν : Type v} [LitVar L ν] (ls : Array L) :

(any ls).toPropFun = Model.PropFun.any ↑(List.map LitVar.toPropFun ls.toList)

@[simp]

theorem Trestle.Cnf.toPropFun_all {L : Type u} {ν : Type v} [LitVar L ν] (ls : Array L) :

(all ls).toPropFun = Model.PropFun.all ↑(List.map LitVar.toPropFun ls.toList)

Satisfiability #

@[reducible, inline]

abbrev Trestle.Cnf.Sat {L : Type u} {ν : Type v} [LitVar L ν] (f : Cnf L) :

Equations

f.Sat = f.toPropFun.Sat

Instances For

def Trestle.Cube.toPropFun {L : Type u_1} {ν : Type u_2} [LitVar L ν] (C : Cube L) :

Model.PropFun ν

Equations

C.toPropFun = Trestle.Model.PropFun.all (Multiset.map Trestle.LitVar.toPropFun ↑C.toList)

Instances For

instance Trestle.Cube.instCoeHeadPropFun {L : Type u_1} {ν : Type u_2} [LitVar L ν] :

CoeHead (Cube L) (Model.PropFun ν)

Equations

Trestle.Cube.instCoeHeadPropFun = { coe := Trestle.Cube.toPropFun }

theorem Trestle.Cube.mem_semVars_toPropFun {L : Type u_2} {ν : Type u_1} [LitVar L ν] [DecidableEq ν] (x : ν) (C : Cube L) :

x ∈ C.toPropFun.semVars → ∃ l ∈ C.toArray, LitVar.toVar l = x

theorem Trestle.Cube.satisfies_iff {L : Type u_2} {ν : Type u_1} [LitVar L ν] {τ : Model.PropAssignment ν} {C : Cube L} :

τ ⊨ C.toPropFun ↔ ∀ l ∈ C.toArray, τ ⊨ LitVar.toPropFun l

theorem Trestle.Cube.empty_iff {L : Type u_2} {ν : Type u_1} [LitVar L ν] [DecidableEq ν] [LawfulLitVar L ν] (C : Cube L) :

C.toPropFun = ⊥ ↔ ∃ l₁ ∈ C.toArray, ∃ l₂ ∈ C.toArray, l₁ = -l₂

@[simp]

theorem Trestle.Cube.toPropFun_and {L : Type u_1} {ν : Type u_2} [LitVar L ν] (c1 c2 : Cube L) :

(c1.and c2).toPropFun = c1.toPropFun ⊓ c2.toPropFun

@[simp]

theorem Trestle.Cube.toPropFun_map {L : Type u_3} {ν : Type u_4} [LitVar L ν] {L' : Type u_1} {ν' : Type u_2} [LitVar L' ν'] [LawfulLitVar L' ν'] (f : ν → ν') (c : Cube L) :

(map L' f c).toPropFun = Model.PropFun.map f c.toPropFun