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

Obtain the literal with the largest identifier in c.

Equations

• c.maxLiteral = (List.map (fun (x : Std.Sat.Literal Nat) => x.fst) c).max?

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

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

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

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

Obtain the literal with the largest identifier in f.

Equations

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

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

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

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

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

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

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

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

def Std.Sat.CNF.relabelFin (f : Std.Sat.CNF Nat) : Std.Sat.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.

@[simp]

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