inductive Blaster.Options.ExpectedResult : Type

Expected solve result

• ExpectedValid : ExpectedResult
• ExpectedFalsified : ExpectedResult
• ExpectedUndetermined : ExpectedResult

def Blaster.Options.instReprExpectedResult.repr : ExpectedResult → Nat → Std.Format

Equations

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

instance Blaster.Options.instReprExpectedResult : Repr ExpectedResult

Equations

• Blaster.Options.instReprExpectedResult = { reprPrec := Blaster.Options.instReprExpectedResult.repr }

instance Blaster.Options.instDecidableEqExpectedResult : DecidableEq ExpectedResult

Equations

• Blaster.Options.instDecidableEqExpectedResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Blaster.Options.isExpectedValid : ExpectedResult → Bool

Equations

• Blaster.Options.isExpectedValid Blaster.Options.ExpectedResult.ExpectedValid = true
• Blaster.Options.isExpectedValid x✝ = false

def Blaster.Options.isExpectedFalsified : ExpectedResult → Bool

Equations

• Blaster.Options.isExpectedFalsified Blaster.Options.ExpectedResult.ExpectedFalsified = true
• Blaster.Options.isExpectedFalsified x✝ = false

def Blaster.Options.isExpectedUndetermined : ExpectedResult → Bool

Equations

• Blaster.Options.isExpectedUndetermined Blaster.Options.ExpectedResult.ExpectedUndetermined = true
• Blaster.Options.isExpectedUndetermined x✝ = false

structure Blaster.Options.BlasterOptions : Type

Type introducing the options passed on to the solver.

• unfoldDepth : Nat

  The number of unfolding steps to be considered when unfolding a recursive function. It is set to 100 by default.

• timeout : Option Nat

  The solving timeout in seconds. It is set to 'none' by default (i.e., unlimited).

• verbose : Nat

  The verbosity level. It is set to zero by default (i.e., no verbosity). - Verbosity Level 0 - Description: Default verbosity level that only displays the solve result. - Usage: This level is to be used when you do not want any extra output during the execution of commands. - Verbosity Level 1 - Description: In addition to Level 0, displays solving progression (e.g., tactics applied or BMC step) - Usage: This level is useful mainly when you want to display the different solving steps. - Verbosity Level 2 - Description: In addition to Level 1, displays solving statistics provided by the backend SMT solver. - Usage: This level is useful only for the tool maintainer. - Verbosity Level 3 - Description: In addition to Level 2, displays the rewriting rules applied on the theorems to be solved. - Usage: This level is to be used mainly for debugging purposes. TODO: This description will be updated as new functionalities are introduced.

• onlySmtLib : Bool

  When set to true, only perform translation to smt-lib without invoking the backend smt solver.

• onlyOptimize : Bool

  When set to true, only perform optimization on the lean specification and do not translate to smt-lib.

• dumpSmtLib : Bool

  When set to true, dump the smt query to stdout.

• generateCex : Bool

  When set to true, generate the counterexample produced for a falsified theorem when the backend SMT solver is invoked.

• randomSeed : Option Nat

  Seed for the random number generator used in the solver. It is set to none by default (i.e., no seed).

• solveResult : ExpectedResult

  When set to true, trigger an error if the #solve command does not return a Falsified status.

• maxDepth : Nat

  Maximum analysis depth to be considered when performing BMC and K-Induction. It is set to 10 by default.

instance Blaster.Options.instReprBlasterOptions : Repr BlasterOptions

Equations

• Blaster.Options.instReprBlasterOptions = { reprPrec := Blaster.Options.instReprBlasterOptions.repr }

def Blaster.Options.instReprBlasterOptions.repr : BlasterOptions → Nat → Std.Format

Equations

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

instance Blaster.Options.instInhabitedBlasterOptions : Inhabited BlasterOptions

Equations

• Blaster.Options.instInhabitedBlasterOptions = { default := { } }