def Blaster.Syntax.solveOption.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.solveOption : Category

#blaster is a Lean4 command that optimizes a lean theorem and calls the backend Smt solver on the remaining unsolved goals.

Options:

• unfold-depth: specifying the number of unfolding to be performed on recursive functions (default: 100)
• timeout: specifying the timeout (in second) to be used for the backend smt solver (defaut: ∞)
• verbose: activating debug info (default: 0)
• only-smt-lib: only translating unsolved goals to smt-lib without invoking the backend solver (default: 0)
• only-optimize: only perform optimization on lean specification and do not translate to smt-lib (default: 0)
• dump-smt-lib: display the smt lib query to stdout (default: 0)
• random-seed: seed for the random number generator (default: none)
• gen-cex: generate counterexample for falsified theorems (default: 1)
• solve-result: specify the expected result from the #blaster command, i.e., 0 for 'Valid', 1 for 'Falsified' and 2 for 'Undetermined'. (default: 0)

Examples:

• #blaster [∀ x y : Nat, x + y ≥ x]
• #blaster (only-optimize: 1) (verbose: 1) [∀ x y : Nat, x + y ≥ x]
• #blaster [add_nat_ge_left]

Equations

• Lean.Parser.Category.solveOption = { }

def Blaster.Syntax.«solveOption(unfold-depth:_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.«solveOption(timeout:_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.«solveOption(verbose:_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.«solveOption(only-smt-lib:_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.«solveOption(only-optimize:_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.«solveOption(dump-smt-lib:_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.«solveOption(gen-cex:_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.«solveOption(solve-result:_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.«solveOption(max-depth:_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.«solveOption(random-seed:_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.solveTerm : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.solve : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

Individual Parsing Functions

def Blaster.Syntax.parseUnfoldDepth {m : Type → Type u_1} [Monad m] (sOpts : Options.BlasterOptions) : Lean.TSyntax `solveOption → m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.parseMaxDepth {m : Type → Type u_1} [Monad m] (sOpts : Options.BlasterOptions) : Lean.TSyntax `solveOption → m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.parseTimeout {m : Type → Type u_1} [Monad m] (sOpts : Options.BlasterOptions) : Lean.TSyntax `solveOption → m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.parseVerbose {m : Type → Type u_1} [Monad m] (sOpts : Options.BlasterOptions) : Lean.TSyntax `solveOption → m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.parseSmtLib {m : Type → Type u_1} [MonadExceptOf Lean.Exception m] [Monad m] (sOpts : Options.BlasterOptions) : Lean.TSyntax `solveOption → m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.parseOptimize {m : Type → Type u_1} [MonadExceptOf Lean.Exception m] [Monad m] (sOpts : Options.BlasterOptions) : Lean.TSyntax `solveOption → m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.parseDumpSmt {m : Type → Type u_1} [MonadExceptOf Lean.Exception m] [Monad m] (sOpts : Options.BlasterOptions) : Lean.TSyntax `solveOption → m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.parseGenCex {m : Type → Type u_1} [MonadExceptOf Lean.Exception m] [Monad m] (sOpts : Options.BlasterOptions) : Lean.TSyntax `solveOption → m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.parseRandomSeed {m : Type → Type u_1} [Monad m] (sOpts : Options.BlasterOptions) : Lean.TSyntax `solveOption → m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.parseSolveResult {m : Type → Type u_1} [MonadExceptOf Lean.Exception m] [Monad m] (sOpts : Options.BlasterOptions) : Lean.TSyntax `solveOption → m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

Generic Parser for All Options

def Blaster.Syntax.parseSolveOption {m : Type → Type u_1} [MonadExceptOf Lean.Exception m] [Monad m] (sOpts : Options.BlasterOptions) (opt : Lean.TSyntax `solveOption) : m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

Process Multiple Options

def Blaster.Syntax.parseSolveOptions {m : Type → Type u_1} [MonadExceptOf Lean.Exception m] [Monad m] (opts : Array Lean.Syntax) (sOpts : Options.BlasterOptions) : m Options.BlasterOptions

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.parseTerm {m : Type → Type u_1} [MonadExceptOf Lean.Exception m] [Monad m] : Lean.TSyntax `Blaster.solveTerm → m Lean.Syntax

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Syntax.commandInvoker (f : Options.BlasterOptions → Lean.Syntax → Lean.Elab.TermElabM Unit) : Lean.Elab.Command.CommandElab

Equations

• One or more equations did not get rendered due to their size.

Implementation of solve command

def Blaster.Syntax.solveImp : Lean.Elab.Command.CommandElab

Equations

• Blaster.Syntax.solveImp = Blaster.Syntax.commandInvoker Blaster.Smt.command