parseDimacs

Mathlib.Tactic.Sat.FromLRAT

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Sat.Parser.parseDimacs

Lean4

/-- Parse a DIMACS format `.cnf` file.
This is not very robust; we assume the file has had comments stripped. -/
def parseDimacs : String.Parser (Nat × Array (Array Int)) := do
  pstring "p cnf" *> ws
  let nvars ← parseNat <* ws
  let nclauses ← parseNat <* ws
  let mut clauses := Array.mkEmpty nclauses
  for _ in [:nclauses]do
    clauses := clauses.push (← parseInts)
  pure (nvars, clauses)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru