def Std.Sat.CNF.Clause.maxLiteral (c : Clause Nat) : Option Nat

Obtain the literal with the largest identifier in c.

Equations

• c.maxLiteral = c.atoms.max?

theorem Std.Sat.CNF.Clause.of_maxLiteral_eq_some {maxLit : Nat} (c : Clause Nat) (h : c.maxLiteral = some maxLit) (lit : Nat) : VarMem lit c → lit ≤ maxLit

theorem Std.Sat.CNF.Clause.maxLiteral_eq_some_of_mem {l : Nat} (c : Clause Nat) (h : VarMem l c) : ∃ (maxLit : Nat), c.maxLiteral = some maxLit

theorem Std.Sat.CNF.Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) (lit : Nat) : ¬VarMem lit c

def Std.Sat.CNF.maxLiteral (f : CNF Nat) : Option Nat

Obtain the literal with the largest identifier in f.

Equations

• f.maxLiteral = (Array.filterMap Std.Sat.CNF.Clause.maxLiteral f.clauses).max?

theorem Std.Sat.CNF.of_maxLiteral_eq_some' {maxLit localMax : Nat} (f : CNF Nat) (h : f.maxLiteral = some maxLit) (clause : Clause Nat) : clause ∈ f → clause.maxLiteral = some localMax → localMax ≤ maxLit

theorem Std.Sat.CNF.of_maxLiteral_eq_some {maxLit : Nat} (f : CNF Nat) (h : f.maxLiteral = some maxLit) (lit : Nat) : VarMem lit f → lit ≤ maxLit

theorem Std.Sat.CNF.of_maxLiteral_eq_none (f : CNF Nat) (h : f.maxLiteral = none) (lit : Nat) : ¬VarMem lit f

def Std.Sat.CNF.numLiterals (f : CNF Nat) : Nat

An upper bound for the amount of distinct literals in f.

Equations

• f.numLiterals = match f.maxLiteral with | none => 0 | some n => n + 1

theorem Std.Sat.CNF.lt_numLiterals {v : Nat} {f : CNF Nat} (h : VarMem v f) : v < f.numLiterals

theorem Std.Sat.CNF.numLiterals_pos {v : Nat} {f : CNF Nat} (h : VarMem v f) : 0 < f.numLiterals

def Std.Sat.CNF.relabelFin (f : CNF Nat) : CNF (Fin f.numLiterals)

Relabel f to a CNF formula with a known upper bound for its literals.

This operation might be useful when e.g. using the literals to index into an array of known size without conducting bounds checks.

Equations

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

@[simp]

theorem Std.Sat.CNF.unsat_relabelFin {f : CNF Nat} : f.relabelFin.Unsat ↔ f.Unsat