inductive Blaster.Smt.Result : Type

Result of an Smt query.

• Valid : Result
• Falsified (cex : List String) : Result
• Undetermined : Result

instance Blaster.Smt.instReprResult : Repr Result

Equations

• Blaster.Smt.instReprResult = { reprPrec := Blaster.Smt.instReprResult.repr }

def Blaster.Smt.instReprResult.repr : Result → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.instReprResult.repr Blaster.Smt.Result.Valid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Blaster.Smt.Result.Valid")).group prec✝

def Blaster.Smt.toResult (e : Lean.Expr) : Result

Equations

• Blaster.Smt.toResult (Lean.Expr.const `True us) = Blaster.Smt.Result.Valid
• Blaster.Smt.toResult (Lean.Expr.const `False us) = Blaster.Smt.Result.Falsified []
• Blaster.Smt.toResult e = Blaster.Smt.Result.Undetermined

def Blaster.Smt.isValidResult (r : Result) : Bool

Equations

• Blaster.Smt.isValidResult Blaster.Smt.Result.Valid = true
• Blaster.Smt.isValidResult r = false

def Blaster.Smt.isFalsifiedResult (r : Result) : Bool

Equations

• Blaster.Smt.isFalsifiedResult (Blaster.Smt.Result.Falsified cex) = true
• Blaster.Smt.isFalsifiedResult r = false

def Blaster.Smt.isUndeterminedResult (r : Result) : Bool

Equations

• Blaster.Smt.isUndeterminedResult Blaster.Smt.Result.Undetermined = true
• Blaster.Smt.isUndeterminedResult r = false

def Blaster.Smt.falsifiedError (r : Result) : String

Equations

• Blaster.Smt.falsifiedError r = toString "Falsified result expected but got " ++ toString (reprStr r)

def Blaster.Smt.blankRef : Optimize.TranslateEnvT Lean.Syntax

Equations

• Blaster.Smt.blankRef = do let pos ← Lean.getRefPos pure (Lean.Syntax.atom (Lean.SourceInfo.original "".toSubstring pos " ".toSubstring pos) "")

def Blaster.Smt.logResult (r : Result) (isCTI : Bool := false) (indLabel : String := "") (cexLabel : String := "Counterexample") : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.Smt.logResult.dumpCex (cexLabel : String) (f : Lean.MessageData → Lean.MetaM Unit) (failure : String) (cex : List String) : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.Smt.createBlasterProcess : IO (IO.Process.Child { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped })

Spawn a z3 process w.r.t. the provided solver options.

Equations

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

def Blaster.Smt.updateTranslateCache (a : Lean.Expr) (b : SmtTerm) : Optimize.TranslateEnvT Unit

Update translation cache with a := b.

Equations

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

def Blaster.Smt.withTranslateEnvCache (a : Lean.Expr) (f : Unit → Optimize.TranslateEnvT SmtTerm) : Optimize.TranslateEnvT SmtTerm

Return b if a := b is already in the translation cache. Otherwise, the following actions are performed:

• execute b ← fun ()
• update cache with a := b
• return b

Equations

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

def Blaster.Smt.checkCancelTk? : Optimize.TranslateEnvT Unit

Check if cancel token has been triggered and kill corresponding running Solver instance (if necessary).

Equations

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

def Blaster.Smt.getOutputModel (h : IO.FS.Handle) (proof : Bool := false) : Optimize.TranslateEnvT String

Retrieve model output from h when a counterexample is generated. NOTE: A model output starts with "(" and ends with ")\n"

Equations

• Blaster.Smt.getOutputModel h proof = Blaster.Smt.getOutputModel.loop h proof ""

partial def Blaster.Smt.getOutputModel.loop (h : IO.FS.Handle) (proof : Bool) (acc : String) : Optimize.TranslateEnvT String

def Blaster.Smt.getOutputProof (h : IO.FS.Handle) : Optimize.TranslateEnvT String

Retrieve proof output for an unsat result. NOTE: A proof output starts with "(proof" and ends with ")\n\n".

Equations

• Blaster.Smt.getOutputProof h = Blaster.Smt.getOutputModel h true

def Blaster.Smt.getErrorMsg (h : IO.FS.Handle) : IO String

Retrieve error msg from 'h'. NOTE: An error msg starts with "(error" and ends with ")\n".

Equations

• Blaster.Smt.getErrorMsg h = h.getLine

def Blaster.Smt.getOutputEval (h : IO.FS.Handle) : IO String

Retrieve an eval output from h after execution (eval t) NOTE: An eval output may either correspond to a scalar value or to an inductive datatype one. In the latter case it's provided within parenthesis. The number of opening and closing parenthesis should tally to stop reading from h.

Equations

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

def Blaster.Smt.getOutputEval.tallyParenthesis (s : String) (tally : Int) : Int

Equations

• Blaster.Smt.getOutputEval.tallyParenthesis s tally = String.foldr (fun (c : Char) (acc : Int) => match c with | '(' => acc + 1 | ')' => acc - 1 | x => acc) tally s

partial def Blaster.Smt.getOutputEval.getIndValue (h : IO.FS.Handle) (acc : String) (tally : Int) : IO String

def Blaster.Smt.storeCommand (c : SmtCommand) : Optimize.TranslateEnvT Unit

Push smt command c in the translation environment only when sOpts.dumpSmtLib is set

Equations

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

def Blaster.Smt.isSmtProcSet : Optimize.TranslateEnvT Bool

Return true when the smtProc has been initialized

Equations

• Blaster.Smt.isSmtProcSet = do let __do_lift ← get pure __do_lift.smtEnv.smtProc.isSome

def Blaster.Smt.trySubmitCommand! (c : SmtCommand) (checkSuccess : Bool := true) : Optimize.TranslateEnvT Unit

Push smt command c in the translation environment only when sOpts.dumpSmtLib is set. The command is piped to the backend solver if the corresponding process has been created. An error is triggered when the checkSuccess flag is set and not success output is produced. NOTE: The checkSuccess is to be set only for Smt command that are NOT expected to produce any output.

Equations

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

def Blaster.Smt.submitCommand (c : SmtCommand) : Optimize.TranslateEnvT Unit

Same as trySubmitCommand! but with flag checkSuccess set to false.

Equations

• Blaster.Smt.submitCommand c = Blaster.Smt.trySubmitCommand! c false

def Blaster.Smt.declareConst (id : SmtSymbol) (t : SortExpr) : Optimize.TranslateEnvT Unit

Declare a free variable with name id and sort t.

Equations

• Blaster.Smt.declareConst id t = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.declareConst id t)

def Blaster.Smt.declareDataType (nm : SmtSymbol) (decl : SmtDatatypeDecl) : Optimize.TranslateEnvT Unit

Declare an inductive datatype in Smt lib with name nm and body decl.

Equations

• Blaster.Smt.declareDataType nm decl = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.declareDataType nm decl)

def Blaster.Smt.declareMutualDataTypes (nms : Array SmtSortDecl) (decls : Array SmtDatatypeDecl) : Optimize.TranslateEnvT Unit

Declare mutual inductive datatypes in Smt lib with names nms and bodies decls. An error is triggered if nms.size ≠ decls.size.

Equations

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

def Blaster.Smt.declareFun (nm : SmtSymbol) (args : Array SortExpr) (rt : SortExpr) : Optimize.TranslateEnvT Unit

Declare an uninterpreted function with name nm, arguments args and return type rt.

Equations

• Blaster.Smt.declareFun nm args rt = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.declareFun nm args rt)

def Blaster.Smt.defineFun (nm : SmtSymbol) (args : SortedVars) (rt : SortExpr) (b : SmtTerm) (isRec : Bool := false) : Optimize.TranslateEnvT Unit

Define a function with name nm, parameters args, return type rt, body b with isRec flag set to false by default.

Equations

• Blaster.Smt.defineFun nm args rt b isRec = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.defineFun isRec nm args rt b)

def Blaster.Smt.defineMutualFuns (decls : Array SmtFunDecl) (bs : Array SmtTerm) : Optimize.TranslateEnvT Unit

Define mutually recursive functions with declarations decls and bodies bs. An error is triggered if decls.size ≠ bs.size.

Equations

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

def Blaster.Smt.declareSort (nm : SmtSymbol) (n : Nat) : Optimize.TranslateEnvT Unit

Declare a sort with name nm and arity n.

Equations

• Blaster.Smt.declareSort nm n = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.declareSort nm n)

def Blaster.Smt.defineSort (nm : SmtSymbol) (args : Option (Array SmtSymbol)) (b : SortExpr) : Optimize.TranslateEnvT Unit

Define a sort with name nm, optional parameters args and body b.

Equations

• Blaster.Smt.defineSort nm args b = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.defineSort nm args b)

def Blaster.Smt.assertTerm (p : SmtTerm) : Optimize.TranslateEnvT Unit

Assert a proposition p.

Equations

• Blaster.Smt.assertTerm p = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.assertTerm p)

def Blaster.Smt.fvarIdToSmtSymbol (v : Lean.FVarId) : Optimize.TranslateEnvT SmtSymbol

Create an Smt symbol from a free variable v. If v already exists in the free variables cache return the same smt symbol. Otherwise:

• Increment the free variable index
• Insert v in cache
• return the smt symbol corresponding to the new index

Equations

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

Create an Smt term from a free variable.

def Blaster.Smt.fvarIdToSmtTerm (v : Lean.FVarId) : Optimize.TranslateEnvT SmtTerm

Equations

• Blaster.Smt.fvarIdToSmtTerm v = do let __do_lift ← Blaster.Smt.fvarIdToSmtSymbol v pure (Blaster.Smt.smtSimpleVarId __do_lift)

def Blaster.Smt.definePredQualifier (s : SmtSymbol) (t : SortExpr) (assertFlag : Option Bool) : Optimize.TranslateEnvT Unit

Given s and smt symbol t and smt sort and optional assertFlag boolean value, perform the following:

• When assertFlag = some b:
  • define smt predicate (define-fun s ((@x t)) Bool b)
• Otherwise:
  • declare smt predicate (declare-fun s ((t)) Bool) Assume that s is defined as @is{xxx}

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.definePredQualifier s t none = Blaster.Smt.declareFun s #[t] Blaster.Smt.boolSort

def Blaster.Smt.defineTypeSort (isTypeSym : SmtSymbol) : Optimize.TranslateEnvT Unit

Perform the following actions:

• Declare smt universal sort (declare-sort @@Type 0)
• Define smt predicate (define-fun @isType ((@x @@Type)) Bool true) Assume isTypeSym := @isType

Equations

• Blaster.Smt.defineTypeSort isTypeSym = do Blaster.Smt.declareSort Blaster.Smt.typeSymbol 0 Blaster.Smt.definePredQualifier isTypeSym Blaster.Smt.typeSort (some true)

def Blaster.Smt.defineEmptySort (isEmptySym : SmtSymbol) : Optimize.TranslateEnvT Unit

Perform the following actions:

• Declare Empty sort in Smt Lib
• Define smt predicate (define-fun @isEmpty ((@x Empty)) Bool false) Assume isEmptySym := @isEmpty

Equations

• Blaster.Smt.defineEmptySort isEmptySym = do Blaster.Smt.declareSort Blaster.Smt.emptySymbol 0 Blaster.Smt.definePredQualifier isEmptySym Blaster.Smt.emptySort (some false)

def Blaster.Smt.definePEmptySort (isPEmptySym : SmtSymbol) : Optimize.TranslateEnvT Unit

Perform the following actions:

• Declare PEmpty sort in Smt Lib
• Define smt predicate (define-fun @isPEmpty ((@x PEmpty)) Bool false) Assume isPEmptySym := @isPEmpty

Equations

• Blaster.Smt.definePEmptySort isPEmptySym = do Blaster.Smt.declareSort Blaster.Smt.pemptySymbol 0 Blaster.Smt.definePredQualifier isPEmptySym Blaster.Smt.pemptySort (some false)

def Blaster.Smt.definePropSort (isPropSym : SmtSymbol) : Optimize.TranslateEnvT Unit

Perform the following actions:

• Define Prop sort in Smt Lib, which is an alias to Bool Smt Sort
• Define smt predicate (define-fun @isProp ((@x Prop)) Bool true) Assume isPropSym := @isProp

Equations

• Blaster.Smt.definePropSort isPropSym = do Blaster.Smt.defineSort Blaster.Smt.propSymbol none Blaster.Smt.boolSort Blaster.Smt.definePredQualifier isPropSym Blaster.Smt.propSort (some true)

def Blaster.Smt.defineNatSort (isNatSym : SmtSymbol) : Optimize.TranslateEnvT Unit

Perform the following actions:

• Define Nat sort in Smt Lib, which is an alias to Int Smt Sort
• Define smt predicate (define-fun @isNat ((@x Nat)) Bool (<= 0 @x)) to qualify quantifiers on Nat Assume isNatSym := @isNat

Equations

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

def Blaster.Smt.defineNatSub : Optimize.TranslateEnvT Unit

Define Nat.sub Smt function, i.e., @Nat.sub x y := (ite (< x y) 0 (- x y))

Equations

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

def Blaster.Smt.defineIntEDiv : Optimize.TranslateEnvT Unit

Define Int.ediv Smt function, i.e., @Int.ediv x y := (ite (= 0 y) 0 (div x y))

Equations

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

def Blaster.Smt.defineIntEMod : Optimize.TranslateEnvT Unit

Define Int.emod Smt function, i.e., @Int.emod x y := (ite (= 0 y) x (mod x y))

Equations

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

def Blaster.Smt.defineIntTDiv : Optimize.TranslateEnvT Unit

Define Int.tdiv Smt function, i.e., @Int.tdiv x y := (ite (= 0 y) 0 (ite (<= 0 x) (div x y) (- (div (- x) y))))

Equations

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

def Blaster.Smt.defineIntTMod : Optimize.TranslateEnvT Unit

Define Int.tmod Smt function, i.e., @Int.tmod x y := (ite (= 0 y) x (ite (<= 0 x) (mod x y) (- (mod (- x) y))))

Equations

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

def Blaster.Smt.defineIntFDiv : Optimize.TranslateEnvT Unit

Define Int.fdiv Smt function, i.e., @Int.fdiv x y := (ite (= 0 y) 0 (ite (< y 0) (div (-x) (- y)) (div x y)))

Equations

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

def Blaster.Smt.defineIntFMod : Optimize.TranslateEnvT Unit

Define Int.fmod Smt function, i.e., @Int.fmod x y := (ite (= 0 y) x (ite (< y 0) (- (mod (- x) y)) (mod x y)))

Equations

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

def Blaster.Smt.defineIntPow : Optimize.TranslateEnvT Unit

Define Int.pow Smt function as follows: (define-fun-rec @Int.pow ((@x Int)(@y Nat)) Int (ite (= 0 @y) 1 (* @x (@Int.pow @x (@Nat.sub @y 1)))))

Equations

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

def Blaster.Smt.defineNatPow : Optimize.TranslateEnvT Unit

Define Nat.pow Smt function as follows: (define-fun-rec @Nat.pow ((@x Nat)(@y Nat)) Nat (ite (= 0 @y) 1 (* @x (@Nat.pow @x (@Nat.sub @y 1)))))

Equations

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

def Blaster.Smt.defineInttoNat : Optimize.TranslateEnvT Unit

Define Int.toNat Smt function, i.e., Int.toNat x := (ite (<= 0 x) x else 0)

Equations

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

def Blaster.Smt.evalTerm (t : SmtTerm) : Optimize.TranslateEnvT String

Try to retrieve to evaluate term t when a sat result is obtained and dump result to stdout. TODO: We need to define the Smt-lib syntax and term elaborator to parse produced value and generate the corresponding Lean representation. This will also be helpful when writing the test cases to validate the Smt-Lib translation. Do nothing if the Smt process is not defined.

Equations

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

def Blaster.Smt.getModel : Optimize.TranslateEnvT (List String)

Try to retrieve the model when a sat result is obtained and dump result to stdout. Do nothing when:

• No solver instance is defined
• Option solverOptions.generateCex is set to false TODO: We need to define the Smt-lib syntax and term elaborator to parse produced model and generate the corresponding Lean representation. This will also be helpful when writing the test cases to validate the Smt-Lib translation.

Equations

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

def Blaster.Smt.getModel.genCexAtStep (cex : Array String) (vars : List (SmtSymbol × Lean.Name)) : Optimize.TranslateEnvT (Array String)

Equations

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

def Blaster.Smt.getModel.getVarValue (v : SmtSymbol × Lean.Name) : Optimize.TranslateEnvT String

Equations

• Blaster.Smt.getModel.getVarValue v = do let __do_lift ← Blaster.Smt.evalTerm (Blaster.Smt.smtSimpleVarId v.fst) pure (toString v.snd ++ toString ": " ++ toString __do_lift)

def Blaster.Smt.getSatResult (p : IO.Process.Child { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped }) : Optimize.TranslateEnvT Result

Retrieve sat result from h. An error is triggered when an unexpected check-sat result is obtained. Function can be called only after a check-sat

Equations

• Blaster.Smt.getSatResult p = do let res ← liftM (IO.FS.Handle.getLine p.stdout).asTask Blaster.Smt.getSatResult.waitForResult res

partial def Blaster.Smt.getSatResult.waitForResult (res : Task (Except IO.Error String)) : Optimize.TranslateEnvT Result

def Blaster.Smt.checkSat : Optimize.TranslateEnvT Result

Check satisfiability of current Smt query and return the result. An error is triggered when an unexpected check-sat result is obtained. Return Undetermined when the Smt process is not defined.

Equations

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

def Blaster.Smt.checkSatAssuming (args : Array SmtTerm) : Optimize.TranslateEnvT Result

Check satisfiability of current Smt query by assuming the provided terms and return the result. An error is triggered when an unexpected check-sat result is obtained. Return Undetermined when the Smt process is not defined.

Equations

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

def Blaster.Smt.getProof : Optimize.TranslateEnvT String

Try to retrieve the proof artifact when a unsat result is obtained and dump result to stdout. TODO: We need to define the Smt-lib syntax and term elaborator to parse and reconstruct the proof in Lean. This will also be helpful when writing the test cases to validate the Smt-Lib translation. Do nothing if the Smt process is not defined.

Equations

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

def Blaster.Smt.exitSmt : Optimize.TranslateEnvT UInt32

Try to terminate the Smt process. Do nothing if Smt process is not defined.

Equations

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

def Blaster.Smt.setLogicAll : Optimize.TranslateEnvT Unit

Set the Smt logic to ALL.

Equations

• Blaster.Smt.setLogicAll = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setLogic "ALL")

def Blaster.Smt.setProduceProofs (b : Bool) : Optimize.TranslateEnvT Unit

Set Smt produce-proofs option to b.

Equations

• Blaster.Smt.setProduceProofs b = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":produce-proofs" (toString b))

def Blaster.Smt.setProduceModels (b : Bool) : Optimize.TranslateEnvT Unit

Set Smt produce-models option to b.

Equations

• Blaster.Smt.setProduceModels b = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":produce-models" (toString b))

def Blaster.Smt.setMbqi (b : Bool) : Optimize.TranslateEnvT Unit

Set Smt smt.mbqi option to b.

Equations

• Blaster.Smt.setMbqi b = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":smt.mbqi" (toString b))

def Blaster.Smt.setPullNestedQuantifiers (b : Bool) : Optimize.TranslateEnvT Unit

Set Smt smt.pull-nested-quantifiers option to b.

Equations

• Blaster.Smt.setPullNestedQuantifiers b = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":smt.pull-nested-quantifiers" (toString b))

def Blaster.Smt.setPrintSuccess (b : Bool) : Optimize.TranslateEnvT Unit

Set Smt print-success option to b.

Equations

• Blaster.Smt.setPrintSuccess b = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":print-success" (toString b))

def Blaster.Smt.setRandomSeed (n : Option Nat) : Optimize.TranslateEnvT Unit

Set Smt smt.random-seed option to n or none.

Equations

• Blaster.Smt.setRandomSeed (some idx) = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":smt.random-seed" (toString idx))
• Blaster.Smt.setRandomSeed none = pure ()

def Blaster.Smt.setAutoConfig (b : Bool) : Optimize.TranslateEnvT Unit

Set Smt auto_config option to b.

Equations

• Blaster.Smt.setAutoConfig b = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":auto_config" (toString b))

def Blaster.Smt.setCaseSplit (n : Nat) : Optimize.TranslateEnvT Unit

Set Smt smt.case_split to n, with n ∈ [0..6].

Equations

• Blaster.Smt.setCaseSplit n = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":smt.case_split" (toString n))

def Blaster.Smt.setQiEagerThreshold (n : Nat) : Optimize.TranslateEnvT Unit

Set Smt smt.qi.eager_threshold to n.

Equations

• Blaster.Smt.setQiEagerThreshold n = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":smt.qi.eager_threshold" (toString n))

def Blaster.Smt.setDelayUnits (b : Bool) : Optimize.TranslateEnvT Unit

Set Smt smt.delay_units to b.

Equations

• Blaster.Smt.setDelayUnits b = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":smt.delay_units" (toString b))

def Blaster.Smt.setMacroFinder (b : Bool) : Optimize.TranslateEnvT Unit

Set Smt smt.macro_finder option to b.

Equations

• Blaster.Smt.setMacroFinder b = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":smt.macro_finder" (toString b))

def Blaster.Smt.setRelevancy (n : Nat) : Optimize.TranslateEnvT Unit

Set Smt smt.relevancy option to i.

Equations

• Blaster.Smt.setRelevancy n = Blaster.Smt.trySubmitCommand! (Blaster.Smt.SmtCommand.setOption ":smt.relevancy" (toString n))

def Blaster.Smt.setTimeout : Optimize.TranslateEnvT Unit

Set Smt timeout when option is specified.

Equations

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

def Blaster.Smt.setDefaultSmtOptions (sOpts : Options.BlasterOptions) : Optimize.TranslateEnvT Unit

Set the default Smt options, i.e.:

• (set-option :print-success true)
• (set-option :produce-models true)
• (set-option :produce-proofs true)
• (set-option :smt-pull-nested-quantifiers true)
• (set-option :smt-mbqi true)
• (set-option :auto_config false)
• (set-option :smt.random-seed n) when n is provided in solver options
• (set-option :smt.macro_finder true)

Equations

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

def Blaster.Smt.setBlasterProcess : Optimize.TranslateEnvT Unit

Perform the following actions:

• when option only-smt-lib is set to false:
  • Spawn the backend solver process and update TranslateEnv
  • set the default smt solver options by emitting the corresponding commands
• when option only-smt-lib is set to true:
  • only add the solver options to the list of smt commands.

Equations

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