def Trestle.IVar : Type

The implementation type of DIMACS variables (hence the "I" in IVar).

In DIMACS, variables are represented by strictly positive integers. We attach the positivity-hypothesis as a subtype here.

This type is the exact same as the one for PNat in Mathlib (see Data.PNat.Defs.lean). We redefine it here to avoid the dependency on Mathlib, and also in case we want to change the backing type to UInt64 in the future.

Equations

• Trestle.IVar = { n : Nat // 0 < n }

instance Trestle.instIVarDecidableEq : DecidableEq IVar

Equations

• Trestle.instIVarDecidableEq a b = a.instDecidableEq b

instance Trestle.instIVarRepr : Repr IVar

Equations

• Trestle.instIVarRepr = instReprSubtype

def Trestle.ILit : Type

The implementation type of DIMACS literals (hence the "I" in ILit).

In DIMACS, literals are non-zero integers, with negative numbers variables with an optional negation. We represent them as integers, with the invariant that they are non-zero.

Equations

• Trestle.ILit = { i : Int // i ≠ 0 }

instance Trestle.instILitDecidableEq : DecidableEq ILit

Equations

• Trestle.instILitDecidableEq a b = a.instDecidableEq b

instance Trestle.instILitRepr : Repr ILit

Equations

• Trestle.instILitRepr = instReprSubtype

index

@[always_inline]

def Trestle.IVar.index (v : IVar) : Nat

Converts an IVar into a 0-indexed Nat.

DIMACS variables are 1-indexed, but arrays are 0-indexed, so index subtracts one and does the coercion.

Equations

• v.index = v.val - 1

@[always_inline]

def Trestle.IVar.ofIndex (n : Nat) : IVar

Converts a 0-indexed Nat into an IVar.

Equations

• Trestle.IVar.ofIndex n = ⟨n + 1, ⋯⟩

@[simp]

theorem Trestle.IVar.ofIndex_inj (n m : Nat) : ofIndex n = ofIndex m ↔ n = m

@[simp]

theorem Trestle.IVar.ofIndex_index (v : IVar) : ofIndex v.index = v

@[simp]

theorem Trestle.IVar.index_ofIndex (i : Nat) : (ofIndex i).index = i

instance Trestle.IVar.instInhabited : Inhabited IVar

Equations

• Trestle.IVar.instInhabited = { default := ⟨1, Trestle.IVar.instInhabited._proof_1⟩ }

def Trestle.IVar.toString : IVar → String

Equations

• Trestle.IVar.toString ⟨n, property⟩ = toString "" ++ toString n ++ toString ""

instance Trestle.IVar.instToString : ToString IVar

Equations

• Trestle.IVar.instToString = { toString := Trestle.IVar.toString }

instance Trestle.IVar.instHashable : Hashable IVar

Equations

• Trestle.IVar.instHashable = { hash := fun (v : Trestle.IVar) => hash v.val }

instance Trestle.IVar.instOrd : Ord IVar

Equations

• Trestle.IVar.instOrd = { compare := fun (a b : Trestle.IVar) => compare a.val b.val }

instance Trestle.IVar.instLT : LT IVar

Equations

• Trestle.IVar.instLT = { lt := fun (a b : Trestle.IVar) => a.val < b.val }

theorem Trestle.IVar.lt_def (a b : IVar) : (a < b) = (a.val < b.val)

@[simp]

theorem Trestle.IVar.lt_ofIndex (a b : Nat) : ofIndex a < ofIndex b ↔ a < b

instance Trestle.IVar.instLE : LE IVar

Equations

• Trestle.IVar.instLE = { le := fun (a b : Trestle.IVar) => a.val ≤ b.val }

theorem Trestle.IVar.le_def (a b : IVar) : (a ≤ b) = (a.val ≤ b.val)

@[simp]

theorem Trestle.IVar.le_refl (a : IVar) : a ≤ a

@[simp]

theorem Trestle.IVar.le_ofIndex (a b : Nat) : ofIndex a ≤ ofIndex b ↔ a ≤ b

instance Trestle.IVar.instHAddNat : HAdd IVar Nat IVar

Equations

• Trestle.IVar.instHAddNat = { hAdd := fun (v : Trestle.IVar) (off : Nat) => ⟨v.val + off, ⋯⟩ }

@[simp]

theorem Trestle.IVar.val_addNat (v : IVar) (x : Nat) : (v + x).val = v.val + x

@[simp]

theorem Trestle.IVar.index_addNat (v : IVar) (x : Nat) : (v + x).index = v.index + x

theorem Trestle.IVar.add_lt_of_pos {x : Nat} (pos : 0 < x) (v : IVar) : v < v + x

@[simp]

theorem Trestle.IVar.add_lt_add_left (v : IVar) (x y : Nat) : v + x < v + y ↔ x < y

def Trestle.IVar.max : IVar → IVar → IVar

Equations

• Trestle.IVar.max ⟨v₁, property⟩ ⟨v₂, property_1⟩ = ⟨max v₁ v₂, ⋯⟩

def Trestle.IVar.toPosILit : IVar → ILit

Equations

• Trestle.IVar.toPosILit ⟨n, property⟩ = ⟨Int.ofNat n, ⋯⟩

def Trestle.IVar.toNegILit : IVar → ILit

Equations

• Trestle.IVar.toNegILit ⟨n, property⟩ = ⟨-Int.ofNat n, ⋯⟩

instance Trestle.IVar.instCoeIVar : Coe IVar ILit

Equations

• Trestle.IVar.instCoeIVar = { coe := fun (v : Trestle.IVar) => v.toPosILit }

instance Trestle.IVar.instOfNat {n : Nat} : OfNat IVar (n + 1)

Equations

• Trestle.IVar.instOfNat = { ofNat := ⟨n + 1, ⋯⟩ }

instance Trestle.ILit.instInhabited : Inhabited ILit

Equations

• Trestle.ILit.instInhabited = { default := ⟨1, Trestle.ILit.instInhabited._proof_1⟩ }

instance Trestle.ILit.instHashable : Hashable ILit

Equations

• Trestle.ILit.instHashable = { hash := fun (v : Trestle.ILit) => hash v.val }

instance Trestle.ILit.instOrd : Ord ILit

Equations

• Trestle.ILit.instOrd = { compare := fun (a b : Trestle.ILit) => compare a.val b.val }

instance Trestle.ILit.instCoeInt : Coe ILit Int

Equations

• Trestle.ILit.instCoeInt = { coe := fun (v : Trestle.ILit) => v.val }

def Trestle.ILit.toString : ILit → String

Equations

• Trestle.ILit.toString ⟨l, property⟩ = toString "" ++ toString l ++ toString ""

instance Trestle.ILit.instToString : ToString ILit

Equations

• Trestle.ILit.instToString = { toString := Trestle.ILit.toString }

def Trestle.ILit.toIVar : ILit → IVar

Equations

• Trestle.ILit.toIVar ⟨l, property⟩ = ⟨l.natAbs, ⋯⟩

instance Trestle.ILit.instCoeToIVar : Coe ILit IVar

Equations

• Trestle.ILit.instCoeToIVar = { coe := fun (v : Trestle.ILit) => v.toIVar }

def Trestle.ILit.ofIVar : IVar → ILit

Equations

• Trestle.ILit.ofIVar ⟨n, property⟩ = ⟨Int.ofNat n, ⋯⟩

instance Trestle.ILit.instCoeOfIVar : Coe IVar ILit

Equations

• Trestle.ILit.instCoeOfIVar = { coe := fun (v : Trestle.IVar) => Trestle.ILit.ofIVar v }

instance Trestle.ILit.instOfNat {n : Nat} : OfNat ILit (n + 1)

Equations

• Trestle.ILit.instOfNat = { ofNat := ⟨↑n + 1, ⋯⟩ }

def Trestle.ILit.toNat : ILit → Nat

Equations

• Trestle.ILit.toNat ⟨l, property⟩ = l.natAbs

def Trestle.ILit.polarity : ILit → Bool

Returns true iff the literal is positive.

Equations

• Trestle.ILit.polarity ⟨l, property⟩ = decide (l > 0)

def Trestle.ILit.negate : ILit → ILit

Equations

• Trestle.ILit.negate ⟨l, property⟩ = ⟨-l, ⋯⟩

instance Trestle.ILit.instLitVar : LitVar ILit IVar

Equations

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

instance Trestle.ILit.instNeg : Neg ILit

Equations

• Trestle.ILit.instNeg = { neg := Trestle.LitVar.negate }

theorem Trestle.ILit.polarity_eq {l₁ l₂ : ILit} : LitVar.polarity l₁ = LitVar.polarity l₂ ↔ (0 < l₁.val ↔ 0 < l₂.val)

instance Trestle.ILit.instLawfulLitVar : LawfulLitVar ILit IVar

index

@[always_inline]

def Trestle.ILit.index (l : ILit) : Nat

Converts an ILit into a 0-indexed Nat.

DIMACS literals are 1-indexed (ignoring sign), but arrays are 0-indexed, so index subtracts one and does the coercion.

Equations

• l.index = l.val.natAbs - 1

@[always_inline]

def Trestle.ILit.ofIndex (n : Nat) : ILit

Converts a 0-indexed Nat into an ILit.

Equations

• Trestle.ILit.ofIndex n = ⟨↑n + 1, ⋯⟩

theorem Trestle.ILit.index_def (l : ILit) : l.index = l.toIVar.index

@[simp]

theorem Trestle.ILit.ofIndex_def (n : Nat) : ofIndex n = ofIVar (IVar.ofIndex n)

@[reducible, inline]

abbrev Trestle.IClause : Type

Equations

• Trestle.IClause = Trestle.Clause Trestle.ILit

@[reducible, inline]

abbrev Trestle.ICnf : Type

Equations

• Trestle.ICnf = Trestle.Cnf Trestle.ILit

@[reducible, inline]

abbrev Trestle.ICube : Type

Equations

• Trestle.ICube = Trestle.Cube Trestle.ILit

def Trestle.IClause.maxVar (C : IClause) : Nat

Finds the maximum DIMACS variable in a clause. If the clause is empty, then 0 is returned.

Equations

• C.maxVar = Array.foldl max 0 (Array.map Trestle.ILit.toNat C)

def Trestle.ICnf.maxVar (F : ICnf) : Nat

Finds the maximum DIMACS variable in the CNF. If there are no variables in the formula, then 0 is returned.

Equations

• F.maxVar = Array.foldl max 0 (Array.map Trestle.IClause.maxVar F)