@[reducible, inline]

abbrev Trestle.Clause (L : Type u) : Type u

A disjunction of literals

Equations

• Trestle.Clause L = Array L

@[reducible, inline]

abbrev Trestle.Cnf (L : Type u) : Type u

A conjunction of clauses

Equations

• Trestle.Cnf L = Array (Trestle.Clause L)

def Trestle.Cube (L : Type u) : Type u

A conjunction of literals. The implementation is identical to clauses, but the interpretation is different.

Equations

• Trestle.Cube L = Array L

instance Trestle.Clause.instToString {L : Type u_1} [ToString L] : ToString (Clause L)

Equations

• Trestle.Clause.instToString = { toString := fun (C : Trestle.Clause L) => toString "(" ++ toString (" ∨ ".intercalate (Array.map toString C).toList) ++ toString ")" }

def Trestle.Clause.or {L : Type u} (c1 c2 : Clause L) : Clause L

Equations

• c1.or c2 = c1 ++ c2

def Trestle.Clause.negate {L : Type u} {ν : Type v} [LitVar L ν] (c : Clause L) : Cube L

Equations

• c.negate = Array.map (fun (x : L) => -x) c

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

Equations

• Trestle.Clause.map L' f c = Array.map (Trestle.LitVar.map f) c

instance Trestle.Cnf.instToString {L : Type u_1} [ToString L] : ToString (Cnf L)

Equations

• Trestle.Cnf.instToString = { toString := fun (C : Trestle.Cnf L) => toString "" ++ toString (" ∧ ".intercalate (Array.map toString C).toList) ++ toString "" }

def Trestle.Cnf.addClause {L : Type u} (f : Cnf L) (C : Clause L) : Cnf L

Equations

• f.addClause C = Array.push f C

def Trestle.Cnf.and {L : Type u} (f1 f2 : Cnf L) : Cnf L

Equations

• f1.and f2 = f1 ++ f2

def Trestle.Cnf.not {L : Type u} {ν : Type v} [LitVar L ν] (c : Clause L) : Cnf L

Equations

• Trestle.Cnf.not c = Array.map (fun (l : L) => #[-l]) c

def Trestle.Cnf.any {L : Type u} (ls : Array L) : Cnf L

Equations

• Trestle.Cnf.any ls = #[ls]

def Trestle.Cnf.all {L : Type u} (ls : Array L) : Cnf L

Equations

• Trestle.Cnf.all ls = Array.map (fun (l : L) => #[l]) ls

instance Trestle.Cube.instToString {L : Type u_1} [ToString L] : ToString (Cube L)

Equations

• Trestle.Cube.instToString = { toString := fun (C : Trestle.Cube L) => toString "(" ++ toString (" ∧ ".intercalate (Array.map toString C).toList) ++ toString ")" }

@[reducible, inline]

abbrev Trestle.Cube.toArray {L : Type u} (c : Cube L) : Array L

Equations

• c.toArray = c

instance Trestle.Cube.instCoeHeadArray {L : Type u} : CoeHead (Cube L) (Array L)

Equations

• Trestle.Cube.instCoeHeadArray = { coe := Trestle.Cube.toArray }

def Trestle.Cube.and {L : Type u} (c1 c2 : Cube L) : Cube L

Equations

• c1.and c2 = c1.toArray ++ c2.toArray

def Trestle.Cube.map {L : Type u} {ν : Type v} [LitVar L ν] {ν' : Type u_1} (L' : Type u_2) [LitVar L' ν'] (f : ν → ν') (c : Cube L) : Cube L'

Equations

• Trestle.Cube.map L' f c = Array.map (Trestle.LitVar.map f) c

def Trestle.Cube.negate {L : Type u} {ν : Type v} [LitVar L ν] (c : Cube L) : Clause L

Equations

• c.negate = Array.map (fun (x : L) => -x) c

@[reducible, inline]

abbrev Trestle.Cubing (L : Type u_1) : Type u_1

Equations

• Trestle.Cubing L = List (Trestle.Cube L)

def Trestle.Cubing.unit {L : Type u_1} : Cubing L

Equations

• Trestle.Cubing.unit = [#[]]

def Trestle.Cubing.prod {L : Type u_1} (c1 c2 : Cubing L) : Cubing L

Equations

• c1.prod c2 = List.map (fun (x : Trestle.Cube L × Trestle.Cube L) => match x with | (a, b) => a.and b) (List.product c1 c2)