buildConj

Mathlib.Tactic.Sat.FromLRAT

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

Lean4

/-- Constructs the formula expression from the input CNF, as a balanced tree of `Fmla.and` nodes. -/
partial def buildConj (arr : Array (Array Int)) (start stop : Nat) : Expr :=
  match stop - start with
  | 0 => panic! "empty"
  | 1 => mkApp (mkConst ``Sat.Fmla.one) (buildClause arr[start]!)
  | len =>
    let mid := start + len / 2
    mkApp2 (mkConst ``Sat.Fmla.and) (buildConj arr start mid) (buildConj arr mid stop)

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

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

Разделы

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

Аффилиация

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