structure Std.Sat.CNF.Clause (α : Type u) : Type u

A clause in a CNF.

The literal (i, b) is satisfied if the assignment to i agrees with b.

• atoms : Array α
• polarities : ByteArray
• size_polarities : self.polarities.size = self.atoms.size
• isBool_polarities (i : Nat) (h : i < self.polarities.size) : self.polarities[i] = 0 ∨ self.polarities[i] = 1

structure Std.Sat.CNF (α : Type u) : Type u

A CNF formula.

Literals are identified by members of α.

• clauses : Array (Clause α)

@[instance_reducible]

instance Std.Sat.CNF.Clause.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Clause α)

Equations

• c1.instDecidableEq c2 = if h : c1.atoms = c2.atoms ∧ c1.polarities = c2.polarities then isTrue ⋯ else isFalse ⋯

@[inline]

def Std.Sat.CNF.Clause.empty {α : Type u_1} : Clause α

Equations

• Std.Sat.CNF.Clause.empty = { atoms := #[], polarities := ByteArray.empty, size_polarities := ⋯, isBool_polarities := Std.Sat.CNF.Clause.empty._proof_2✝ }

@[instance_reducible]

instance Std.Sat.CNF.Clause.instInhabited {α : Type u_1} : Inhabited (Clause α)

Equations

• Std.Sat.CNF.Clause.instInhabited = { default := Std.Sat.CNF.Clause.empty }

@[inline]

def Std.Sat.CNF.Clause.size {α : Type u_1} (c : Clause α) : Nat

Equations

• c.size = c.atoms.size

theorem Std.Sat.CNF.Clause.Internal.size_eq_size_atoms {α : Type u_1} {c : Clause α} : c.size = c.atoms.size

theorem Std.Sat.CNF.Clause.Internal.size_eq_size_polarities {α : Type u_1} {c : Clause α} : c.size = c.polarities.size

@[simp]

theorem Std.Sat.CNF.Clause.size_empty {α : Type u_1} : empty.size = 0

@[inline]

def Std.Sat.CNF.Clause.add {α : Type u_1} (c : Clause α) (atom : α) (pol : Bool) : Clause α

Equations

• c.add atom pol = { atoms := c.atoms.push atom, polarities := c.polarities.push (if pol = true then 1 else 0), size_polarities := ⋯, isBool_polarities := ⋯ }

@[simp]

theorem Std.Sat.CNF.Clause.add_ne_empty {α : Type u_1} (c : Clause α) (atom : α) (pol : Bool) : c.add atom pol ≠ empty

@[simp]

theorem Std.Sat.CNF.Clause.Internal.atoms_add {α : Type u_1} {atom : α} {pol : Bool} {c : Clause α} : (c.add atom pol).atoms = c.atoms.push atom

@[simp]

theorem Std.Sat.CNF.Clause.size_add {α : Type u_1} (c : Clause α) (atom : α) (pol : Bool) : (c.add atom pol).size = c.size + 1

def Std.Sat.CNF.Clause.polarity {α : Type u_1} (c : Clause α) (i : Nat) : Bool

The polarity of the literal at index i of c; false if i is out of bounds.

Equations

• c.polarity i = if h : i < c.polarities.size then c.polarities[i] == 1 else false

theorem Std.Sat.CNF.Clause.Internal.polarity_eq_data {α : Type u_1} {c : Clause α} {i : Nat} : c.polarity i = (c.polarities.data[i]?.getD 0 == 1)

theorem Std.Sat.CNF.Clause.Internal.polarity_eq_getElem {α : Type u_1} {c : Clause α} {i : Nat} (h : i < c.polarities.size) : c.polarity i = (c.polarities[i] == 1)

@[simp]

theorem Std.Sat.CNF.Clause.polarity_empty {α : Type u_1} {i : Nat} : empty.polarity i = false

theorem Std.Sat.CNF.Clause.polarity_add {α : Type u_1} {atom : α} {pol : Bool} {c : Clause α} {i : Nat} : (c.add atom pol).polarity i = if i = c.size then pol else c.polarity i

def Std.Sat.CNF.Clause.literals {α : Type u_1} (c : Clause α) : List (Literal α)

The literals of a Clause as a list of atom/polarity pairs, used to state specifications. This function runs in O(n) and allocates all of the List and the Literal objects fresh. For this reason it is not useful for performance sensitive contexts.

Equations

• c.literals = List.map (fun (x : α × Nat) => match x with | (x, i) => (x, c.polarity i)) c.atoms.toList.zipIdx

@[simp]

theorem Std.Sat.CNF.Clause.literals_empty {α : Type u_1} : empty.literals = []

@[simp]

theorem Std.Sat.CNF.Clause.literals_add {α : Type u_1} {atom : α} {pol : Bool} {c : Clause α} : (c.add atom pol).literals = c.literals ++ [(atom, pol)]

theorem Std.Sat.CNF.Clause.length_literals {α : Type u_1} {c : Clause α} : c.literals.length = c.size

theorem Std.Sat.CNF.Clause.Internal.map_fst_literals {α : Type u_1} {c : Clause α} : List.map Prod.fst c.literals = c.atoms.toList

theorem Std.Sat.CNF.Clause.Internal.getElem_literals {α : Type u_1} {c : Clause α} {i : Nat} (h : i < c.literals.length) : c.literals[i] = (c.atoms[i], c.polarity i)

theorem Std.Sat.CNF.Clause.ext {α : Type u_1} {c1 c2 : Clause α} (h : c1.literals = c2.literals) : c1 = c2

def Std.Sat.CNF.Clause.ofLiterals {α : Type u_1} (l : List (Literal α)) : Clause α

Build a Clause from a list of literals.

Equations

• Std.Sat.CNF.Clause.ofLiterals l = List.foldl (fun (c : Std.Sat.CNF.Clause α) (x : Std.Sat.Literal α) => match x with | (atom, pol) => c.add atom pol) Std.Sat.CNF.Clause.empty l

theorem Std.Sat.CNF.Clause.literals_foldl_add {α : Type u_1} {l : List (Literal α)} {init : Clause α} : (List.foldl (fun (c : Clause α) (x : Literal α) => match x with | (atom, pol) => c.add atom pol) init l).literals = init.literals ++ l

@[simp]

theorem Std.Sat.CNF.Clause.literals_ofLiterals {α : Type u_1} {l : List (Literal α)} : (ofLiterals l).literals = l

@[simp]

theorem Std.Sat.CNF.Clause.ofLiterals_literals {α : Type u_1} {c : Clause α} : ofLiterals c.literals = c

@[simp]

theorem Std.Sat.CNF.Clause.literals_eq_nil_iff {α : Type u_1} {c : Clause α} : c.literals = [] ↔ c = empty

theorem Std.Sat.CNF.Clause.exists_eq_add_of_ne_empty {α : Type u_1} {c : Clause α} (h : c ≠ empty) : ∃ (c' : Clause α), ∃ (atom : α), ∃ (pol : Bool), c = c'.add atom pol

@[instance_reducible]

instance Std.Sat.CNF.Clause.instMembershipLiteral {α : Type u_1} : Membership (Literal α) (Clause α)

Equations

• Std.Sat.CNF.Clause.instMembershipLiteral = { mem := fun (clause : Std.Sat.CNF.Clause α) (lit : Std.Sat.Literal α) => lit ∈ clause.literals }

theorem Std.Sat.CNF.Clause.mem_literals_iff {α : Type u_1} {c : Clause α} {l : Literal α} : l ∈ c.literals ↔ l ∈ c

theorem Std.Sat.CNF.Clause.Internal.getElem_mem {α : Type u_1} {c : Clause α} {i : Nat} (h : i < c.atoms.size) : (c.atoms[i], c.polarity i) ∈ c

theorem Std.Sat.CNF.Clause.Internal.mem_iff_exists_getElem {α : Type u_1} {c : Clause α} {l : Literal α} : l ∈ c ↔ ∃ (i : Nat), ∃ (h : i < c.atoms.size), (c.atoms[i], c.polarity i) = l

theorem Std.Sat.CNF.Clause.ne_of_mem_of_negate_mem {α : Type u_1} {l l' : Literal α} {c : Clause α} (h1 : l ∈ c) (h2 : ¬l' ∈ c) (h3 : ¬l'.negate ∈ c) : l.fst ≠ l'.fst

@[inline]

def Std.Sat.CNF.Clause.contains {α : Type u_1} [BEq α] (c : Clause α) (lit : Literal α) : Bool

Equations

• c.contains lit = Std.Sat.CNF.Clause.contains.go✝ c lit 0

theorem Std.Sat.CNF.Clause.contains_iff_mem {α : Type u_1} [BEq α] [LawfulBEq α] {c : Clause α} {lit : Literal α} : c.contains lit = true ↔ lit ∈ c

@[instance_reducible]

instance Std.Sat.CNF.Clause.instDecidableMemLiteralOfDecidableEq {α : Type u_1} [DecidableEq α] {lit : Literal α} {c : Clause α} : Decidable (lit ∈ c)

Equations

• Std.Sat.CNF.Clause.instDecidableMemLiteralOfDecidableEq = decidable_of_iff (c.contains lit = true) ⋯

@[inline]

unsafe def Std.Sat.CNF.Clause.forIn'ImplUnsafe {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (c : Clause α) (b : β) (f : (l : Literal α) → l ∈ c → β → m (ForInStep β)) : m β

See comment at Array.forIn'Unsafe.

Equations

• c.forIn'ImplUnsafe b f = Std.Sat.CNF.Clause.forIn'ImplUnsafe.loop✝ c f c.atoms.usize 0 b

@[implemented_by Std.Sat.CNF.Clause.forIn'ImplUnsafe]

def Std.Sat.CNF.Clause.forIn'Impl {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (c : Clause α) (b : β) (f : (l : Literal α) → l ∈ c → β → m (ForInStep β)) : m β

Reference implementation for forIn' on Clause, iterating directly over the packed representation without materializing literals.

Equations

• c.forIn'Impl b f = Std.Sat.CNF.Clause.forIn'Impl.go✝ c f 0 b

@[instance_reducible]

instance Std.Sat.CNF.Clause.instForIn'LiteralInferInstanceMembershipOfMonad {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] : ForIn' m (Clause α) (Literal α) inferInstance

Equations

• Std.Sat.CNF.Clause.instForIn'LiteralInferInstanceMembershipOfMonad = { forIn' := fun {β : Type ?u.3} => Std.Sat.CNF.Clause.forIn'Impl }

@[simp]

theorem Std.Sat.CNF.Clause.not_mem_empty {α : Type u_1} {l : Literal α} : ¬l ∈ empty

@[simp]

theorem Std.Sat.CNF.Clause.mem_add {α : Type u_1} {atom : α} {pol : Bool} {c : Clause α} {l1 : Literal α} : l1 ∈ c.add atom pol ↔ l1 = (atom, pol) ∨ l1 ∈ c

theorem Std.Sat.CNF.Clause.forIn'_eq_forIn'_literals {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {c : Clause α} {init : β} {f : (l : Literal α) → l ∈ c → β → m (ForInStep β)} : forIn' c init f = forIn' c.literals init fun (l : Literal α) (h : l ∈ c.literals) (b : β) => f l ⋯ b

@[inline]

def Std.Sat.CNF.Clause.erase {α : Type u_1} [BEq α] (c : Clause α) (lit : Literal α) : Clause α

Erase all occurrences of lit from c.

Equations

• c.erase lit = Std.Sat.CNF.Clause.erase.go✝ c lit 0 Std.Sat.CNF.Clause.empty

@[simp]

theorem Std.Sat.CNF.Clause.literals_erase {α : Type u_1} [BEq α] [LawfulBEq α] {c : Clause α} {lit : Literal α} : (c.erase lit).literals = List.filter (fun (l : Literal α) => l != lit) c.literals

@[simp]

theorem Std.Sat.CNF.Clause.mem_erase_iff {α : Type u_1} {lit lit' : Literal α} [BEq α] [LawfulBEq α] {c : Clause α} : lit' ∈ c.erase lit ↔ lit ≠ lit' ∧ lit' ∈ c

def Std.Sat.CNF.Clause.append {α : Type u_1} (c1 c2 : Clause α) : Clause α

The disjunction of two clauses, obtained by concatenating their literals.

Equations

• c1.append c2 = { atoms := c1.atoms ++ c2.atoms, polarities := c1.polarities ++ c2.polarities, size_polarities := ⋯, isBool_polarities := ⋯ }

@[instance_reducible]

instance Std.Sat.CNF.Clause.instAppend {α : Type u_1} : Append (Clause α)

Equations

• Std.Sat.CNF.Clause.instAppend = { append := Std.Sat.CNF.Clause.append }

@[simp]

theorem Std.Sat.CNF.Clause.Internal.atoms_append {α : Type u_1} {c1 c2 : Clause α} : (c1 ++ c2).atoms = c1.atoms ++ c2.atoms

@[simp]

theorem Std.Sat.CNF.Clause.Internal.polarities_append {α : Type u_1} {c1 c2 : Clause α} : (c1 ++ c2).polarities = c1.polarities ++ c2.polarities

theorem Std.Sat.CNF.Clause.polarity_append {α : Type u_1} {c1 c2 : Clause α} {i : Nat} : (c1 ++ c2).polarity i = if i < c1.size then c1.polarity i else c2.polarity (i - c1.size)

@[simp]

theorem Std.Sat.CNF.Clause.size_append {α : Type u_1} {c1 c2 : Clause α} : (c1 ++ c2).size = c1.size + c2.size

@[simp]

theorem Std.Sat.CNF.Clause.literals_append {α : Type u_1} {c1 c2 : Clause α} : (c1 ++ c2).literals = c1.literals ++ c2.literals

@[simp]

theorem Std.Sat.CNF.Clause.empty_append {α : Type u_1} {c : Clause α} : empty ++ c = c

@[simp]

theorem Std.Sat.CNF.Clause.append_empty {α : Type u_1} {c : Clause α} : c ++ empty = c

@[simp]

theorem Std.Sat.CNF.Clause.append_assoc {α : Type u_1} {c1 c2 c3 : Clause α} : c1 ++ c2 ++ c3 = c1 ++ (c2 ++ c3)

@[simp]

theorem Std.Sat.CNF.Clause.append_add {α : Type u_1} {atom : α} {pol : Bool} {c1 c2 : Clause α} : c1 ++ c2.add atom pol = (c1 ++ c2).add atom pol

theorem Std.Sat.CNF.Clause.ofLiterals_append {α : Type u_1} {l1 l2 : List (Literal α)} : ofLiterals (l1 ++ l2) = ofLiterals l1 ++ ofLiterals l2

@[simp]

theorem Std.Sat.CNF.Clause.append_eq_empty_iff {α : Type u_1} {c1 c2 : Clause α} : c1 ++ c2 = empty ↔ c1 = empty ∧ c2 = empty

@[simp]

theorem Std.Sat.CNF.Clause.mem_append {α : Type u_1} {c1 c2 : Clause α} {l : Literal α} : l ∈ c1 ++ c2 ↔ l ∈ c1 ∨ l ∈ c2

@[inline]

def Std.Sat.CNF.empty {α : Type u_1} : CNF α

Equations

• Std.Sat.CNF.empty = { clauses := #[] }

@[inline]

def Std.Sat.CNF.emptyWithCapacity {α : Type u_1} (n : Nat) : CNF α

Equations

• Std.Sat.CNF.emptyWithCapacity n = { clauses := Array.emptyWithCapacity n }

@[inline]

def Std.Sat.CNF.add {α : Type u_1} (f : CNF α) (c : Clause α) : CNF α

Equations

• f.add c = { clauses := f.clauses.push c }

@[inline]

def Std.Sat.CNF.append {α : Type u_1} (f1 f2 : CNF α) : CNF α

Equations

• f1.append f2 = { clauses := f1.clauses ++ f2.clauses }

@[instance_reducible]

instance Std.Sat.CNF.instAppend {α : Type u_1} : Append (CNF α)

Equations

• Std.Sat.CNF.instAppend = { append := Std.Sat.CNF.append }

def Std.Sat.CNF.Clause.VarMem {α : Type u_1} (v : α) (c : Clause α) : Prop

Variable v occurs in Clause c.

Equations

• Std.Sat.CNF.Clause.VarMem v c = (v ∈ c.atoms)

@[instance_reducible]

instance Std.Sat.CNF.Clause.instDecidableVarMemOfDecidableEq {α : Type u_1} {v : α} {c : Clause α} [DecidableEq α] : Decidable (VarMem v c)

Equations

• Std.Sat.CNF.Clause.instDecidableVarMemOfDecidableEq = { decide := decide (Array.elem v c.atoms = true), reflects_decide := ⋯ }

theorem Std.Sat.CNF.Clause.VarMem_iff_exists_mem_literals {α : Type u_1} {v : α} {c : Clause α} : VarMem v c ↔ ∃ (pol : Bool), (v, pol) ∈ c.literals

@[simp]

theorem Std.Sat.CNF.Clause.not_VarMem_empty {α : Type u_1} {v : α} : ¬VarMem v empty

theorem Std.Sat.CNF.Clause.VarMem_add_self {α : Type u_1} {atom : α} {pol : Bool} {c : Clause α} : VarMem atom (c.add atom pol)

theorem Std.Sat.CNF.Clause.VarMem_add_ne_self {α : Type u_1} {pol : Bool} {c : Clause α} {atom1 atom2 : α} (h : atom1 ≠ atom2) : VarMem atom1 (c.add atom2 pol) ↔ VarMem atom1 c

@[simp]

theorem Std.Sat.CNF.Clause.VarMem_add {α : Type u_1} {atom : α} {c : Clause α} {pol : Bool} {v : α} : VarMem v (c.add atom pol) ↔ v = atom ∨ VarMem v c

@[simp]

theorem Std.Sat.CNF.Clause.VarMem_append {α : Type u_1} {v : α} {c1 c2 : Clause α} : VarMem v (c1 ++ c2) ↔ VarMem v c1 ∨ VarMem v c2

theorem Std.Sat.CNF.Clause.inductionOn {α : Type u_1} {motive : Clause α → Prop} (empty : motive empty) (add : ∀ (c : Clause α) (atom : α) (pol : Bool), motive c → motive (c.add atom pol)) (c : Clause α) : motive c

def Std.Sat.CNF.Mem {α : Type u_1} (f : CNF α) (c : Clause α) : Prop

Clause c occurs in CNF formula f.

Equations

• f.Mem c = (c ∈ f.clauses)

@[instance_reducible]

instance Std.Sat.CNF.instMembershipClause {α : Type u_1} : Membership (Clause α) (CNF α)

Equations

• Std.Sat.CNF.instMembershipClause = { mem := Std.Sat.CNF.Mem }

@[instance_reducible]

instance Std.Sat.CNF.instDecidableMemClauseOfDecidableEq {α : Type u_1} {c : Clause α} {f : CNF α} [DecidableEq α] : Decidable (c ∈ f)

Equations

• Std.Sat.CNF.instDecidableMemClauseOfDecidableEq = { decide := decide (Array.elem c f.clauses = true), reflects_decide := ⋯ }

theorem Std.Sat.CNF.Internal.mem_iff {α : Type u_1} {c : Clause α} {f : CNF α} : c ∈ f ↔ c ∈ f.clauses

theorem Std.Sat.CNF.Internal.clauses_append {α : Type u_1} {f1 f2 : CNF α} : (f1 ++ f2).clauses = f1.clauses ++ f2.clauses

@[simp]

theorem Std.Sat.CNF.not_mem_empty {α : Type u_1} {c : Clause α} : ¬c ∈ empty

@[simp]

theorem Std.Sat.CNF.mem_add {α : Type u_1} {f : CNF α} {c1 c2 : Clause α} : c1 ∈ f.add c2 ↔ c1 = c2 ∨ c1 ∈ f

@[simp]

theorem Std.Sat.CNF.mem_append {α : Type u_1} {f1 f2 : CNF α} {c : Clause α} : c ∈ f1 ++ f2 ↔ c ∈ f1 ∨ c ∈ f2

def Std.Sat.CNF.VarMem {α : Type u_1} (v : α) (f : CNF α) : Prop

Variable v occurs in CNF formula f.

Equations

• Std.Sat.CNF.VarMem v f = ∃ (c : Std.Sat.CNF.Clause α), c ∈ f.clauses ∧ Std.Sat.CNF.Clause.VarMem v c

@[instance_reducible]

instance Std.Sat.CNF.instDecidableVarMemOfDecidableEq {α : Type u_1} {v : α} {f : CNF α} [DecidableEq α] : Decidable (VarMem v f)

Equations

• Std.Sat.CNF.instDecidableVarMemOfDecidableEq = { decide := decide (∃ (i : Nat), ∃ (h : i < f.clauses.size), Std.Sat.CNF.Clause.VarMem v f.clauses[i]), reflects_decide := ⋯ }

theorem Std.Sat.CNF.Internal.any_not_isEmpty_iff_exists_mem {α : Type u_1} {f : CNF α} : (f.clauses.any fun (c : Clause α) => !c.literals.isEmpty) = true ↔ ∃ (v : α), VarMem v f

theorem Std.Sat.CNF.Internal.any_atoms_size_ne_zero_iff_exists_mem {α : Type u_1} {f : CNF α} : (f.clauses.any fun (c : Clause α) => c.atoms.size != 0) = true ↔ ∃ (v : α), VarMem v f

@[instance_reducible]

instance Std.Sat.CNF.instDecidableExistsVarMemOfDecidableEq {α : Type u_1} {f : CNF α} [DecidableEq α] : Decidable (∃ (v : α), VarMem v f)

Equations

• Std.Sat.CNF.instDecidableExistsVarMemOfDecidableEq = decidable_of_iff ((f.clauses.any fun (c : Std.Sat.CNF.Clause α) => c.atoms.size != 0) = true) ⋯

theorem Std.Sat.CNF.not_VarMem_empty {α : Type u_1} {v : α} : ¬VarMem v empty

theorem Std.Sat.CNF.VarMem_add {α : Type u_1} {v : α} {c : Clause α} {f : CNF α} : VarMem v (f.add c) ↔ Clause.VarMem v c ∨ VarMem v f

theorem Std.Sat.CNF.VarMem_of {α✝ : Type u_1} {f : CNF α✝} {c : Clause α✝} {v : α✝} (h : c ∈ f) (w : Clause.VarMem v c) : VarMem v f

theorem Std.Sat.CNF.Internal.ext_iff {α : Type u_1} {f1 f2 : CNF α} : f1 = f2 ↔ f1.clauses = f2.clauses

@[simp]

theorem Std.Sat.CNF.append_empty {α : Type u_1} {f : CNF α} : f ++ empty = f

@[simp]

theorem Std.Sat.CNF.empty_append {α : Type u_1} {f : CNF α} : empty ++ f = f

@[simp]

theorem Std.Sat.CNF.append_assoc {α : Type u_1} {f1 f2 f3 : CNF α} : f1 ++ f2 ++ f3 = f1 ++ (f2 ++ f3)

@[simp]

theorem Std.Sat.CNF.emptyWithCapacity_eq_empty {α : Type u_1} (n : Nat) : emptyWithCapacity n = empty

@[simp]

theorem Std.Sat.CNF.VarMem_append {α : Type u_1} {v : α} {f1 f2 : CNF α} : VarMem v (f1 ++ f2) ↔ VarMem v f1 ∨ VarMem v f2