Lean4
/-- Core of `fromLRAT`. Constructs the context and main proof definitions,
but not the reification theorem. Returns:
* `nvars`: the number of variables specified in the CNF file
* `ctx`: The abbreviated formula, a constant like `foo.ctx_1`
* `ctx'`: The definitional expansion of the formula, a tree of `Fmla.and` nodes
* `proof`: A proof of `ctx.proof []`
-/
def fromLRATAux (cnf lrat : String) (name : Name) : MetaM (Nat × Expr × Expr × Expr) := do
let Parsec.ParseResult.success _ (nvars, arr) := Parser.parseDimacs cnf.mkIterator |
throwError"parse CNF failed"
if arr.isEmpty then
throwError"empty CNF"
let ctx' := buildConj arr 0 arr.size
let ctxName ← mkAuxDeclName (name ++ `ctx)
addDecl <|
Declaration.defnDecl
{ name := ctxName
levelParams := []
type := mkConst ``Sat.Fmla
value := ctx'
hints := ReducibilityHints.regular 0
safety := DefinitionSafety.safe }
let ctx := mkConst ctxName
let Parsec.ParseResult.success _ steps := Parser.parseLRAT lrat.mkIterator |
throwError"parse LRAT failed"
let proof ← buildProof arr ctx ctx' steps
let declName ← mkAuxDeclName (name ++ `proof)
addDecl <|
Declaration.thmDecl
{ name := declName
levelParams := []
type := mkApp2 (mkConst ``Sat.Fmla.proof) ctx (buildClause #[])
value := proof }
return (nvars, ctx, ctx', mkConst declName)
