Lean4
/-- Build the main proof of `⊢ ctx.proof []` using the LRAT proof trace.
* `arr`: The input CNF
* `ctx`: The abbreviated formula, a constant like `foo.ctx_1`
* `ctx'`: The definitional expansion of the formula, a tree of `Fmla.and` nodes
* `steps`: The input LRAT proof trace
-/
partial def buildProof (arr : Array (Array Int)) (ctx ctx' : Expr) (steps : Array LRATStep) : MetaM Expr := do
let p := mkApp (mkConst ``Sat.Fmla.subsumes_self) ctx
let mut db := (buildClauses arr ctx 0 arr.size ctx' p default).2
for step in steps do
match step with
| LRATStep.del ds =>
db := ds.foldl (·.erase ·) db
| LRATStep.add i ns pf =>
let e := buildClause ns
match buildProofStep db ns pf ctx e with
| Except.ok proof =>
if ns.isEmpty then
return proof
db := db.insert i { lits := ns, expr := e, proof }
| Except.error msg =>
throwError
throwError"failed to prove empty clause"
