structure Trestle.Encode.EncCNF.State (ν : Type u) : Type u

State for an encoding.

We need to parameterize by literal type L (and variable ν), because otherwise we need to prove everywhere that clauses are "within range"

• nextVar : IVar
• cnf : RichCnf
• vMap : ν → IVar
• vNames : Batteries.RBMap IVar String compare

theorem Trestle.Encode.EncCNF.State.ext {ν : Type u} {x y : State ν} (nextVar : x.nextVar = y.nextVar) (cnf : x.cnf = y.cnf) (vMap : x.vMap = y.vMap) (vNames : x.vNames = y.vNames) : x = y

theorem Trestle.Encode.EncCNF.State.ext_iff {ν : Type u} {x y : State ν} : x = y ↔ x.nextVar = y.nextVar ∧ x.cnf = y.cnf ∧ x.vMap = y.vMap ∧ x.vNames = y.vNames

def Trestle.Encode.EncCNF.State.toPropFun {ν : Type u_1} (s : State ν) : Model.PropFun IVar

Equations

• s.toPropFun = Trestle.Cnf.toPropFun s.cnf.toICnf

def Trestle.Encode.EncCNF.State.new {ν : Type u_1} (nextVar : IVar) (f : ν → IVar) (vNames : List (ν × String)) : State ν

Equations

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

def Trestle.Encode.EncCNF.State.addClause {ν : Type u_1} (C : Clause (Literal ν)) (s : State ν) : State ν

Equations

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

@[simp]

theorem Trestle.Encode.EncCNF.State.toPropFun_addClause {ν : Type u_1} (C : Clause (Literal ν)) (s : State ν) : (addClause C s).toPropFun = s.toPropFun ⊓ Model.PropFun.map s.vMap C.toPropFun

def Trestle.Encode.EncCNF.State.addComment {ν : Type u_1} (comment : String) (s : State ν) : State ν

Equations

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

@[simp]

theorem Trestle.Encode.EncCNF.State.toPropFun_addComment {ν : Type u_1} (comment : String) (s : State ν) : (addComment comment s).toPropFun = s.toPropFun

structure Trestle.Encode.EncCNF.LawfulState (ν : Type u_1) extends Trestle.Encode.EncCNF.State ν : Type u_1

Lawfulness conditions on encoding state.

• nextVar : IVar
• cnf : RichCnf
• vMap : ν → IVar
• vNames : Batteries.RBMap IVar String compare
• cnfVarsLt (c : Clause ILit) : c ∈ self.cnf.toICnf → ∀ l ∈ c, LitVar.toVar l < self.nextVar
• vMapLt (v : ν) : self.vMap v < self.nextVar
• vMapInj : Function.Injective self.vMap

theorem Trestle.Encode.EncCNF.LawfulState.ext {ν : Type u_1} {x y : LawfulState ν} (nextVar : x.nextVar = y.nextVar) (cnf : x.cnf = y.cnf) (vMap : x.vMap = y.vMap) (vNames : x.vNames = y.vNames) : x = y

theorem Trestle.Encode.EncCNF.LawfulState.ext_iff {ν : Type u_1} {x y : LawfulState ν} : x = y ↔ x.nextVar = y.nextVar ∧ x.cnf = y.cnf ∧ x.vMap = y.vMap ∧ x.vNames = y.vNames

instance Trestle.Encode.EncCNF.LawfulState.instCoeState {ν : Type u_1} : Coe (LawfulState ν) (State ν)

Equations

• Trestle.Encode.EncCNF.LawfulState.instCoeState = { coe := Trestle.Encode.EncCNF.LawfulState.toState }

theorem Trestle.Encode.EncCNF.LawfulState.semVars_toPropFun_cnf_lt {ν : Type u_1} (s : LawfulState ν) (v : IVar) : v ∈ s.toPropFun.semVars → v < s.nextVar

noncomputable def Trestle.Encode.EncCNF.LawfulState.interp {ν : Type u_1} (s : LawfulState ν) : Model.PropAssignment ν → Prop

The interpretation of an EncCNF state is the formula's interpretation, but with all temporaries existentially quantified away.

Equations

• s.interp τ = ∃ (σ : Trestle.Model.PropAssignment Trestle.IVar), τ = Trestle.Model.PropAssignment.map s.vMap σ ∧ σ ⊨ s.toPropFun

def Trestle.Encode.EncCNF.LawfulState.new {ν : Type u_1} (nextVar : IVar) (f : ν ↪ IVar) (h : ∀ (v : ν), f v < nextVar) (names : List (ν × String)) : LawfulState ν

Equations

• Trestle.Encode.EncCNF.LawfulState.new nextVar f h names = { toState := Trestle.Encode.EncCNF.State.new nextVar (⇑f) names, cnfVarsLt := ⋯, vMapLt := h, vMapInj := ⋯ }

@[simp]

theorem Trestle.Encode.EncCNF.LawfulState.interp_new {ν : Type u_1} (vars : IVar) (f : ν ↪ IVar) (h : ∀ (v : ν), f v < vars) (names : List (ν × String)) : (new vars f h names).interp = fun (x : Model.PropAssignment ν) => True

@[simp]

theorem Trestle.Encode.EncCNF.LawfulState.toState_new {ν : Type u_1} (vars : IVar) (f : ν ↪ IVar) (h : ∀ (v : ν), f v < vars) (names : List (ν × String)) : (new vars f h names).toState = State.new vars (⇑f) names

def Trestle.Encode.EncCNF.LawfulState.addClause {ν : Type u_1} (C : Clause (Literal ν)) : LawfulState ν → LawfulState ν

Equations

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

@[simp]

theorem Trestle.Encode.EncCNF.LawfulState.interp_addClause {ν : Type u_1} (C : Clause (Literal ν)) (s : LawfulState ν) : (addClause C s).interp = fun (τ : Model.PropAssignment ν) => s.interp τ ∧ τ ⊨ C.toPropFun

def Trestle.Encode.EncCNF.LawfulState.addComment {ν : Type u_1} (comm : String) : LawfulState ν → LawfulState ν

Equations

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

@[simp]

theorem Trestle.Encode.EncCNF.LawfulState.interp_addComment {ν : Type u_1} (comm : String) (s : LawfulState ν) : (addComment comm s).interp = s.interp

@[simp]

theorem Trestle.Encode.EncCNF.LawfulState.vMap_addComment {ν : Type u_1} (comm : String) (s : LawfulState ν) : (addComment comm s).vMap = s.vMap

def Trestle.Encode.EncCNF (ν α : Type u_1) : Type u_1

Encoding monad.

This requires quite a few invariants to be held. It receives and produces lawful states, and nextVar is nondecreasing.

Equations

• Trestle.Encode.EncCNF ν α = { sa : StateM (Trestle.Encode.EncCNF.LawfulState ν) α // ∀ (s : Trestle.Encode.EncCNF.LawfulState ν), s.nextVar ≤ (sa s).2.nextVar }

instance Trestle.Encode.EncCNF.instMonad {ν : Type u_1} : Monad (EncCNF ν)

Equations

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

instance Trestle.Encode.EncCNF.instLawfulMonad {ν : Type u_1} : LawfulMonad (EncCNF ν)

def Trestle.Encode.EncCNF.run {ν α : Type u_1} [IndexType ν] [LawfulIndexType ν] (e : EncCNF ν α) (names : List (ν × String) := []) : α × LawfulState ν

Equations

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

def Trestle.Encode.EncCNF.runUnit {ν : Type} [IndexType ν] [LawfulIndexType ν] (e : EncCNF ν Unit) (names : List (ν × String) := []) : LawfulState ν

Equations

• e.runUnit names = (e.run names).2

def Trestle.Encode.EncCNF.toRichCnf {ν α : Type u_1} [IndexType ν] [LawfulIndexType ν] (e : EncCNF ν α) : RichCnf

Equations

• e.toRichCnf = e.run.2.cnf

def Trestle.Encode.EncCNF.toICnf {ν α : Type u_1} [IndexType ν] [LawfulIndexType ν] (e : EncCNF ν α) : ICnf

Equations

• e.toICnf = e.run.2.cnf.toICnf

def Trestle.Encode.EncCNF.addClause {ν : Type} (C : Clause (Literal ν)) : EncCNF ν Unit

Equations

• Trestle.Encode.EncCNF.addClause C = ⟨fun (s : Trestle.Encode.EncCNF.LawfulState ν) => ((), Trestle.Encode.EncCNF.LawfulState.addClause C s), ⋯⟩

def Trestle.Encode.EncCNF.addComment {ν : Type} (comm : String) : EncCNF ν Unit

Equations

• Trestle.Encode.EncCNF.addComment comm = ⟨fun (s : Trestle.Encode.EncCNF.LawfulState ν) => ((), Trestle.Encode.EncCNF.LawfulState.addComment comm s), ⋯⟩

def Trestle.Encode.EncCNF.newCtx {ν α : Type} (name : String) (inner : EncCNF ν α) : EncCNF ν α

Equations

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

def Trestle.Encode.EncCNF.unit {ν : Type} (l : Literal ν) : EncCNF ν Unit

Equations

• Trestle.Encode.EncCNF.unit l = Trestle.Encode.EncCNF.addClause #[l]

def Trestle.Encode.EncCNF.blockAssn {ν : Type} [BEq ν] [Hashable ν] (a : HashAssn (Literal ν)) : EncCNF ν Unit

Equations

• Trestle.Encode.EncCNF.blockAssn a = Trestle.Encode.EncCNF.addClause (Array.map (fun (x : Trestle.Literal ν) => -x) a.toLitArray)

def Trestle.Encode.EncCNF.addAssn {ν : Type} [BEq ν] [Hashable ν] (a : HashAssn (Literal ν)) : EncCNF ν Unit

Equations

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

Temporaries

def Trestle.Encode.EncCNF.State.withTemps {ν : Type u_1} {ι : Type u_2} [IndexType ι] (s : State ν) (names : Option (ι → String)) : State (ν ⊕ ι)

Equations

• One or more equations did not get rendered due to their size.
• s.withTemps none = { nextVar := s.nextVar + Trestle.IndexType.card ι, cnf := s.cnf, vMap := Trestle.Encode.EncCNF.State.withTemps.vMap s.vMap s.nextVar, vNames := s.vNames }

def Trestle.Encode.EncCNF.State.withTemps.vMap {ν : Type u_1} {ι : Type u_2} [IndexType ι] (vMap : ν → IVar) (nextVar : IVar) (x : ν ⊕ ι) : IVar

Equations

• Trestle.Encode.EncCNF.State.withTemps.vMap vMap nextVar (Sum.inl v) = vMap v
• Trestle.Encode.EncCNF.State.withTemps.vMap vMap nextVar (Sum.inr i) = nextVar + ↑(Trestle.IndexType.toFin i)

@[simp]

theorem Trestle.Encode.EncCNF.State.cnf_withTemps {ν : Type u_2} {ι : Type u_1} {names : Option (ι → String)} [IndexType ι] (s : State ν) : (s.withTemps names).cnf = s.cnf

def Trestle.Encode.EncCNF.LawfulState.withTemps {ν : Type u_1} {ι : Type u_2} [IndexType ι] [LawfulIndexType ι] (s : LawfulState ν) (names : Option (ι → String)) : LawfulState (ν ⊕ ι)

Equations

• s.withTemps names = { toState := s.withTemps names, cnfVarsLt := ⋯, vMapLt := ⋯, vMapInj := ⋯ }

@[simp]

theorem Trestle.Encode.EncCNF.LawfulState.vMap_withTemps {ν : Type u_2} {ι : Type u_1} {names : Option (ι → String)} [IndexType ι] [LawfulIndexType ι] (s : LawfulState ν) : (s.withTemps names).vMap = State.withTemps.vMap s.vMap s.nextVar

@[simp]

theorem Trestle.Encode.EncCNF.LawfulState.interp_withTemps {ν : Type u_2} {ι : Type u_1} {names : Option (ι → String)} [IndexType ι] [LawfulIndexType ι] (s : LawfulState ν) : (s.withTemps names).interp = fun (τ : Model.PropAssignment (ν ⊕ ι)) => s.interp (Model.PropAssignment.map Sum.inl τ)

def Trestle.Encode.EncCNF.State.withoutTemps {ν : Type u_1} {ι : Type u_2} (vMap : ν → IVar) (s : State (ν ⊕ ι)) : State ν

Equations

• Trestle.Encode.EncCNF.State.withoutTemps vMap s = { nextVar := s.nextVar, cnf := s.cnf, vMap := vMap, vNames := s.vNames }

@[simp]

theorem Trestle.Encode.EncCNF.State.vMap_withoutTemps {ν : Type u_2} {ι : Type u_1} {vm : ν → IVar} (s : State (ν ⊕ ι)) : (withoutTemps vm s).vMap = vm

def Trestle.Encode.EncCNF.LawfulState.withoutTemps {ν : Type u_1} {ι : Type u_2} (s : LawfulState (ν ⊕ ι)) (vMap : ν → IVar) (vMapLt : ∀ (v : ν), vMap v < s.nextVar) (vMapInj : Function.Injective vMap) : LawfulState ν

Equations

• s.withoutTemps vMap vMapLt vMapInj = { toState := Trestle.Encode.EncCNF.State.withoutTemps vMap s.toState, cnfVarsLt := ⋯, vMapLt := ⋯, vMapInj := ⋯ }

@[simp]

theorem Trestle.Encode.EncCNF.LawfulState.vMap_withoutTemps {ν : Type u_2} {ι : Type u_1} (s : LawfulState (ν ⊕ ι)) {vMap : ν → IVar} {vMapLt : ∀ (v : ν), vMap v < s.nextVar} {vMapInj : Function.Injective vMap} : (s.withoutTemps vMap vMapLt vMapInj).vMap = vMap

theorem Trestle.Encode.EncCNF.LawfulState.interp_withoutTemps {ν : Type u_2} {ι : Type u_1} (s : LawfulState (ν ⊕ ι)) {vMap : ν → IVar} {vMapLt : ∀ (v : ν), vMap v < s.nextVar} {vMapInj : Function.Injective vMap} (h : vMap = s.vMap ∘ Sum.inl) : (s.withoutTemps vMap vMapLt vMapInj).interp = fun (τ : Model.PropAssignment ν) => ∃ (σ : Model.PropAssignment (ν ⊕ ι)), τ = Model.PropAssignment.map Sum.inl σ ∧ s.interp σ

def Trestle.Encode.EncCNF.nextVar_mono_of_eq {ν α : Type u_1} {s : LawfulState ν} {a : α} {s' : LawfulState ν} {e : EncCNF ν α} (h : ↑e s = (a, s')) : s.nextVar ≤ s'.nextVar

Equations

• ⋯ = ⋯

def Trestle.Encode.EncCNF.withTemps {ν α : Type (max u_1 u_2)} (ι : Type u_2) [IndexType ι] [LawfulIndexType ι] (e : EncCNF (ν ⊕ ι) α) (names : Option (ι → String) := none) : EncCNF ν α

Equations

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