def Blaster.Smt.funNameToSmtSymbol (funName : Lean.Name) : SmtSymbol

Generate an smt symbol from a given function name.

Equations

• Blaster.Smt.funNameToSmtSymbol funName = Blaster.Smt.mkNormalSymbol (toString "@" ++ toString funName)

def Blaster.Smt.fullyAppliedConst : Lean.NameHashSet

list of Lean operators expected to be fully applied at translation phase.

Equations

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

def Blaster.Smt.isArrowPropType (e : Lean.Expr) : Bool

Return true when e corresponds to one of the following:

• e := Prop; or
• e := α₁ → ... → αₙ → Prop; Assume that e does not contain any let expression.

Equations

• Blaster.Smt.isArrowPropType e = e.getForallBody.isProp

def Blaster.Smt.isInductivePredicate (indName : Lean.Name) : Optimize.TranslateEnvT Bool

Return true when indName corresponds to an inductive predicate.

Equations

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

def Blaster.Smt.updateFunInstCacheBase (f : Lean.Expr) (sid : SmtQualifiedIdent) : Optimize.TranslateEnvT Unit

Given f x₁ ... xₙ a function instance and sid a unique smt identifier for f x₁ ... xₙ, add entry f x₁ ... xₙ := sid to funInstCache.

Equations

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

def Blaster.Smt.updateFunInstCache (f : Lean.Expr) (sid : SmtSymbol) : Optimize.TranslateEnvT SmtQualifiedIdent

Same as updateFunInstCacheBase but accepts an SmtSymbol as argument and returns the SmtQualifiedIdent instance added to funInstCache.

Equations

• Blaster.Smt.updateFunInstCache f sid = do Blaster.Smt.updateFunInstCacheBase f (Blaster.Smt.SmtQualifiedIdent.SimpleIdent sid) pure (Blaster.Smt.SmtQualifiedIdent.SimpleIdent sid)

def Blaster.Smt.translateNatSub (n : Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Perform the following actions:

• Return SimpleIdent "Nat.sub" when entry n := SimpleIdent "Nat.sub" exists in funInstCache
• Otherwise:
  • define Nat sort (if necessary)
  • define Nat.sub Smt function (i.e., see defineNatSub)
  • add entry n := SimpleIdent "Nat.sub" to funInstCache
  • return SimpleIdent "Nat.sub" Assume that n := Expr.const ``Nat.sub [].

Equations

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

def Blaster.Smt.translateIntEDiv (f : Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Perform the following actions:

• Return SimpleIdent "@Int.ediv" when entry f := SimpleIdent "@Int.ediv" exists in funInstCache
• Otherwise:
  • define @Int.ediv Smt function (i.e., see defineIntEDiv)
  • add entry f := SimpleIdent "@Int.ediv" to funInstCache
  • add entry f' := SimpleIdent "@Int.ediv" to funInstCache with: - f' := Expr.const Nat.div _ if f := Expr.const ``Int.ediv _- f' := Expr.const@Int.ediv _ otherwise
  • return SimpleIdent "@Int.ediv" Assume that f := Expr.const ``Int.ediv [] or f := Expr.const ``Nat.div [].

Equations

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

def Blaster.Smt.translateIntEDiv.toEDivAlias (f : Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

Equations

• Blaster.Smt.translateIntEDiv.toEDivAlias (Lean.Expr.const `Int.ediv us) = Blaster.Optimize.mkNatDivOp
• Blaster.Smt.translateIntEDiv.toEDivAlias (Lean.Expr.const `Nat.div us) = Blaster.Optimize.mkIntEDivOp
• Blaster.Smt.translateIntEDiv.toEDivAlias (Lean.Expr.const n us) = Blaster.Optimize.throwEnvError (Lean.toMessageData "toEDivAlias: unexpected div operator " ++ Lean.toMessageData n)
• Blaster.Smt.translateIntEDiv.toEDivAlias f = Blaster.Optimize.throwEnvError (Lean.toMessageData "toEDivAlias: name expression expected but got " ++ Lean.toMessageData (reprStr f))

def Blaster.Smt.translateIntEMod (f : Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Perform the following actions:

• Return SimpleIdent "@Int.emod" when entry f := SimpleIdent "@Int.emod" exists in funInstCache
• Otherwise:
  • define @Int.emod Smt function (i.e., see defineIntEMod)
  • add entry f := SimpleIdent "@Int.emod" to funInstCache
  • add entry f' := SimpleIdent "@Int.emod" to funInstCache with: - f' := Expr.const Nat.mod _ if f := Expr.const ``Int.emod _- f' := Expr.const@Int.emod _ otherwise
  • return SimpleIdent "@Int.emod" Assume that f := Expr.const ``Int.emod [] or f := Expr.const ``Nat.mod []

Equations

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

def Blaster.Smt.translateIntEMod.toEModAlias (f : Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

Equations

• Blaster.Smt.translateIntEMod.toEModAlias (Lean.Expr.const `Int.emod us) = Blaster.Optimize.mkNatModOp
• Blaster.Smt.translateIntEMod.toEModAlias (Lean.Expr.const `Nat.mod us) = Blaster.Optimize.mkIntEModOp
• Blaster.Smt.translateIntEMod.toEModAlias (Lean.Expr.const n us) = Blaster.Optimize.throwEnvError (Lean.toMessageData "toEModAlias: unexpected mod operator " ++ Lean.toMessageData n)
• Blaster.Smt.translateIntEMod.toEModAlias f = Blaster.Optimize.throwEnvError (Lean.toMessageData "toEModAlias: name expression expected but got " ++ Lean.toMessageData (reprStr f))

def Blaster.Smt.translateIntTDiv (n : Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Perform the following actions:

• Return SimpleIdent "@Int.tdiv" when entry n := SimpleIdent "@Int.tdiv" exists in funInstCache
• Otherwise:
  • define @Int.tdiv Smt function (i.e., see defineIntTDiv)
  • add entry n := SimpleIdent "@Int.tdiv" to funInstCache
  • return SimpleIdent "@Int.tdiv" Assume that n := Expr.const ``Int.tdiv [].

Equations

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

def Blaster.Smt.translateIntTMod (n : Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Perform the following actions:

• Return SimpleIdent "@Int.tmod" when entry n := SimpleIdent "@Int.tmod" exists in funInstCache
• Otherwise:
  • define @Int.tmod Smt function (i.e., see defineIntTMod)
  • add entry n := SimpleIdent "@Int.tmod" to funInstCache
  • return SimpleIdent "@Int.tmod" Assume that n := Expr.const ``Int.tmod [].

Equations

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

def Blaster.Smt.translateIntFDiv (n : Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Perform the following actions:

• Return SimpleIdent "@Int.fdiv" when entry n := SimpleIdent "@Int.fdiv" exists in funInstCache
• Otherwise:
  • define @Int.fdiv Smt function (i.e., see defineIntFDiv)
  • add entry n := SimpleIdent "@Int.fdiv" to funInstCache
  • return SimpleIdent "@Int.fdiv" Assume that n := Expr.const ``Int.fdiv [].

Equations

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

def Blaster.Smt.translateIntFMod (n : Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Perform the following actions:

• Return SimpleIdent "@Int.fmod" when entry n := SimpleIdent "@Int.fmod" exists in funInstCache
• Otherwise:
  • define @Int.fmod Smt function (i.e., see defineIntFMod)
  • add entry n := SimpleIdent "@Int.fmod" to funInstCache
  • return SimpleIdent "@Int.fmod" Assume that n := Expr.const ``Int.fmod [].

Equations

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

def Blaster.Smt.translateIntPow (f : Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Perform the following actions:

• Return SimpleIdent "@Int.pow" when entry f := SimpleIdent "@Int.pow" exists in funInstCache
• Otherwise:
  • define Nat.sub function (if necessary)
  • define @Int.pow Smt function (i.e., see defineIntPow)
  • add entry f := SimpleIdent "@Int.pow" to funInstCache
  • return SimpleIdent "@Int.pow" Assume that f := Expr.const ``Int.pow []

Equations

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

def Blaster.Smt.translateNatPow (f : Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Perform the following actions:

• Return SimpleIdent "@Nat.pow" when entry f := SimpleIdent "@Nat.pow" exists in funInstCache
• Otherwise:
  • define Nat.sub function (if necessary)
  • define @Nat.pow Smt function (i.e., see defineNatPow)
  • add entry f := SimpleIdent "@Nat.pow" to funInstCache
  • return SimpleIdent "@Nat.pow" Assume that f := Expr.const ``Nat.pow []`

Equations

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

def Blaster.Smt.translateInttoNat (n : Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Perform the following actions:

• Return SimpleIdent "@Int.toNat" when entry n := SimpleIdent "@Int.toNat" exists in funInstCache
• Otherwise:
  • define Nat sort (if necessary)
  • define @Int.toNat Smt function (i.e., see defineInttoNat)
  • add entry n := SimpleIdent "@Int.toNat" to funInstCache
  • return SimpleIdent "@Int.toNat" Assume that n := Expr.const ``Int.toNat [].

Equations

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

def Blaster.Smt.getOpaqueSmtEquivFun (f : Lean.Expr) (s : SmtSymbol) : Optimize.TranslateEnvT SmtQualifiedIdent

Return stₙ when entry f := stₙ exists in funInstCache. Otherwise:

• add entry f := SimpleIdent s to funInstCache
• return SimpleIdent s

Equations

• Blaster.Smt.getOpaqueSmtEquivFun f s = do let __do_lift ← get match __do_lift.smtEnv.funInstCache.get? f with | none => Blaster.Smt.updateFunInstCache f s | some smtId => pure smtId

def Blaster.Smt.translateOpaqueFun (f : Lean.Expr) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT SmtQualifiedIdent

Given f a name expression for which a corresponding smt operator exists and n its corresponding name, and args the effective parameters for f, perform the following actions:

• When f := stₙ exists in funInstCache
  • return stₙ
• When no entry for f exists in funInstCache
  • add entry f := SimpleIdent (smtSymbolFor f) to funInstCache
  • define corresponding smt function only when hasSmtDefinedOperator f
  • return SimpleIdent (smtSymbolFor f)

An error is triggered

• when n corresponds to one of the opaque functions:
  • Exists
  • Blaster.decide'
  • Iff
  • Int.le
  • Nat.beq
  • Nat.ble
  • Nat.pred
  • Nat.le
• when args.size == 0 for Lt.lt

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateOpaqueFun f `Eq args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.eqSymbol
• Blaster.Smt.translateOpaqueFun f `BEq.beq args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.eqSymbol
• Blaster.Smt.translateOpaqueFun f `And args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.andSymbol
• Blaster.Smt.translateOpaqueFun f `Bool.and args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.andSymbol
• Blaster.Smt.translateOpaqueFun f `Or args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.orSymbol
• Blaster.Smt.translateOpaqueFun f `Bool.or args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.orSymbol
• Blaster.Smt.translateOpaqueFun f `Not args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.notSymbol
• Blaster.Smt.translateOpaqueFun f `Bool.not args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.notSymbol
• Blaster.Smt.translateOpaqueFun f `Blaster.dite' args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.iteSymbol
• Blaster.Smt.translateOpaqueFun f `Int.add args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.addSymbol
• Blaster.Smt.translateOpaqueFun f `Nat.add args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.addSymbol
• Blaster.Smt.translateOpaqueFun f `Int.neg args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.subSymbol
• Blaster.Smt.translateOpaqueFun f `Int.mul args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.mulSymbol
• Blaster.Smt.translateOpaqueFun f `Nat.mul args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.mulSymbol
• Blaster.Smt.translateOpaqueFun f `Int.toNat args = Blaster.Smt.translateInttoNat f
• Blaster.Smt.translateOpaqueFun f `Int.tdiv args = Blaster.Smt.translateIntTDiv f
• Blaster.Smt.translateOpaqueFun f `Int.tmod args = Blaster.Smt.translateIntTMod f
• Blaster.Smt.translateOpaqueFun f `Int.fdiv args = Blaster.Smt.translateIntFDiv f
• Blaster.Smt.translateOpaqueFun f `Int.fmod args = Blaster.Smt.translateIntFMod f
• Blaster.Smt.translateOpaqueFun f `Int.ediv args = Blaster.Smt.translateIntEDiv f
• Blaster.Smt.translateOpaqueFun f `Nat.div args = Blaster.Smt.translateIntEDiv f
• Blaster.Smt.translateOpaqueFun f `Int.emod args = Blaster.Smt.translateIntEMod f
• Blaster.Smt.translateOpaqueFun f `Nat.mod args = Blaster.Smt.translateIntEMod f
• Blaster.Smt.translateOpaqueFun f `Int.pow args = Blaster.Smt.translateIntPow f
• Blaster.Smt.translateOpaqueFun f `Nat.pow args = Blaster.Smt.translateNatPow f
• Blaster.Smt.translateOpaqueFun f `LE.le args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.leqSymbol
• Blaster.Smt.translateOpaqueFun f `Nat.ble args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.leqSymbol
• Blaster.Smt.translateOpaqueFun f `Nat.sub args = Blaster.Smt.translateNatSub f
• Blaster.Smt.translateOpaqueFun f `String.append args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.strAppendSymbol
• Blaster.Smt.translateOpaqueFun f `String.length args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.strLengthSymbol
• Blaster.Smt.translateOpaqueFun f `String.replace args = Blaster.Smt.getOpaqueSmtEquivFun f Blaster.Smt.strReplaceAllSymbol
• Blaster.Smt.translateOpaqueFun f n args = Blaster.Optimize.throwEnvError (Lean.toMessageData "translateOpaqueFun: unexpected opaque operator " ++ Lean.toMessageData n)

def Blaster.Smt.createAppNAux (pInfo : Optimize.FunEnvInfo) (s : SmtQualifiedIdent ⊕ SmtTerm) (args : Array Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (isHOF : Bool := false) : Optimize.TranslateEnvT SmtTerm

Helper function for createAppN

Equations

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

def Blaster.Smt.createAppNAux.genUnapplied (isHOF : Bool) (id : SmtQualifiedIdent ⊕ SmtTerm) : Optimize.TranslateEnvT SmtTerm

Equations

• Blaster.Smt.createAppNAux.genUnapplied isHOF (Sum.inl qi) = if isHOF = true then pure (Blaster.Smt.SmtTerm.SmtIdent qi) else pure (Blaster.Smt.SmtTerm.SmtIdent qi)
• Blaster.Smt.createAppNAux.genUnapplied isHOF (Sum.inr st) = if isHOF = true then pure st else Blaster.Optimize.throwEnvError (Lean.toMessageData "genUnapplied: SmtQualifiedIdent expected !!!")

def Blaster.Smt.createAppNAux.genApplied (pInfo : Optimize.FunEnvInfo) (isHOF : Bool) (id : SmtQualifiedIdent ⊕ SmtTerm) (sargs : Array SmtTerm) : Optimize.TranslateEnvT SmtTerm

Equations

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

@[inline]

def Blaster.Smt.createAppN (f : Lean.Expr) (s : SmtQualifiedIdent ⊕ SmtTerm) (args : Array Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (isHOF : Bool := false) : Optimize.TranslateEnvT SmtTerm

Given a function application f x₀ ... xₙ and s the corresponding generated smt identifier/term for f, perform the following:

• When n = 0 ∨ ∀ i ∈ [0..n], ¬ isExplicit xᵢ (i.e., instantiated polymorphic function passed as argument):
  • When isHOF:
    • When isSmtQualifiedIdent s
      • return .SmtIdent s
    • Otherwise (i.e., s is an Smt term, case when f corresponds to a function in a ctor argument)
      • return s
  • Otherwise:
    • When isSmtQualifiedIdent s
      • return asArraySmt s
    • Otherwise (i.e., only a defined function expected)
      • return ⊥
• When ∃ i ∈ [0..n], isExplicit xᵢ, let A := [x₀,..., xₙ] let B := [termTranslator A[i] | i ∈ [0..n] ∧ isExplicit A[i]]
  • When isHOF:
    • When isSmtQualifiedIdent s
      • return selectSmt (.SmtIdent s) B
    • Otherwise (i;e., case when f corresponds to a function in a ctor argument)
      • return selectSmt s B
  • Otherwise:
    • When isSmtQualifiedIdent s
      • return mkSmtAppN s B
    • Otherwise (i.e., only a defined function expected)
      • return ⊥

Equations

• Blaster.Smt.createAppN f s args termTranslator isHOF = do let pInfo ← Blaster.Optimize.getFunEnvInfo f Blaster.Smt.createAppNAux pInfo s args termTranslator isHOF

def Blaster.Smt.translateFunLambdaParamType (t : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) : Optimize.TranslateEnvT SortExpr

Given t corresponding the type of a function/lambda parameter:

• return translateType termTranslator t optionsForFunLambdaParam An error is triggered if t corresponds to the type of an implicit argument.

Equations

• Blaster.Smt.translateFunLambdaParamType t termTranslator = Blaster.Smt.translateType termTranslator t Blaster.Smt.optionsForFunLambdaParam

structure Blaster.Smt.FunctionDefinitions : Type

• funDecls : Array SmtFunDecl
• funBodies : Array SmtTerm
• isRec : Bool

def Blaster.Smt.instInhabitedFunctionDefinitions.default : FunctionDefinitions

Equations

• Blaster.Smt.instInhabitedFunctionDefinitions.default = { funDecls := default, funBodies := default, isRec := default }

instance Blaster.Smt.instInhabitedFunctionDefinitions : Inhabited FunctionDefinitions

Equations

• Blaster.Smt.instInhabitedFunctionDefinitions = { default := Blaster.Smt.instInhabitedFunctionDefinitions.default }

@[reducible, inline]

abbrev Blaster.Smt.FunctionGenEnv (α : Type) : Type

Equations

• Blaster.Smt.FunctionGenEnv = StateRefT' IO.RealWorld Blaster.Smt.FunctionDefinitions Blaster.Optimize.TranslateEnvT

def Blaster.Smt.defineFunctions (defs : FunctionDefinitions) : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.Smt.generateFunInst (f : Lean.Expr) (params : Optimize.ImplicitParameters) : Optimize.TranslateEnvT SmtQualifiedIdent

Given f := Expr.const n _ corresponding to a function name and params its implicit parameter infos, perform the following actions: let instanceArgs := Array.filter (λ p => p.isInstance) params

• When instanceArgs.isEmpty:
  • instName := funNameToSmtSymbol n
  • add entry f := SimpleIdent instName to funInstCache
  • return SimpleIdent instName
• When ¬ instanceArgs.isEmpty:
  • instName := funNameToSmtSymbol (n ++ (← mkFreshId))
  • instApp ← getInstApp f params
  • add entry instApp := SimpleIdent instName to funInstCache
  • return SimpleIdent instName An error is triggered when f is not a named expression.

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.generateFunInst f params = Blaster.Optimize.throwEnvError (Lean.toMessageData "generateFunInst: name expression expected but got " ++ Lean.toMessageData (reprStr f))

def Blaster.Smt.translateRecFun (f : Lean.Expr) (args : Array Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) : Optimize.TranslateEnvT SmtTerm

Given a recursive function application f x₁ ... xₙ, perform the following: let insApp := getInstApp f (← getImplicitParameters f x₁ ... xₙ)

• When ∃ instApp := smtId ∈ funInstCache
  • return createApp f smtId #[x₁ ... xₙ] termTranslator
• Otherwise,
  • generate function definition for f at the Smt level
  • smtId ← generateFunInst f (← getImplicitParameters f x₁ ... xₙ)
  • return createApp f smtId #[x₁ ... xₙ] termTranslator

Assume that f is a recursive function not tagged as opaque.

An error is triggered when

• f is not a name expression.
• No entry in recFunInstCache exists for f

Equations

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

def Blaster.Smt.translateRecFun.updateFunDefinitions (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (id : SmtQualifiedIdent) (fbody : Lean.Expr) (defs : FunctionDefinitions) : Optimize.TranslateEnvT FunctionDefinitions

Equations

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

def Blaster.Smt.translateRecFun.replaceGenericRecFun (f : Lean.Expr) (params : Optimize.ImplicitParameters) (e : Lean.Expr) : Option Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateRecFun.replaceGenericRecFun f params e = none

def Blaster.Smt.translateRecFun.generateRecFunDefinitions (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (funs : List Lean.Name) (us : List Lean.Level) (params : Optimize.ImplicitParameters) : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.Smt.isForbiddenConst (n : Lean.Name) : Bool

Return true only when n corresponds to a function/constructor name expected to be eliminated during optimization phase.

Equations

• Blaster.Smt.isForbiddenConst `Decidable.decide = true
• Blaster.Smt.isForbiddenConst `ite = true
• Blaster.Smt.isForbiddenConst `dite = true
• Blaster.Smt.isForbiddenConst `Iff = true
• Blaster.Smt.isForbiddenConst `Int.negSucc = true
• Blaster.Smt.isForbiddenConst `Int.le = true
• Blaster.Smt.isForbiddenConst `Nat.zero = true
• Blaster.Smt.isForbiddenConst `Nat.succ = true
• Blaster.Smt.isForbiddenConst `Nat.pred = true
• Blaster.Smt.isForbiddenConst `Nat.beq = true
• Blaster.Smt.isForbiddenConst `Nat.ble = true
• Blaster.Smt.isForbiddenConst `Nat.le = true
• Blaster.Smt.isForbiddenConst n = false

def Blaster.Smt.isForbiddenConstExpr (e : Lean.Expr) : Bool

Same as isForbiddenConst but expects a const expression as argument.

Equations

• Blaster.Smt.isForbiddenConstExpr (Lean.Expr.const n us) = Blaster.Smt.isForbiddenConst n
• Blaster.Smt.isForbiddenConstExpr e = false

@[inline]

def Blaster.Smt.updateAxiomMap (n : Lean.Name) : Optimize.TranslateEnvT SmtSymbol

Equations

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

def Blaster.Smt.inferUndeclFunType (t : Lean.Expr) (params : Optimize.ImplicitParameters) : Lean.Expr

Given t := ∀ α₀ → ∀ α₁ ... → αₙ, infer the instanitated type w.r.t. params such that:

• let S := [ αᵢ | i ∈ [0..n] ∧ ¬ params[i].isInstance ]
• let R := [ params[i].effectiveArg | i ∈ [0..n] ∧ ¬ params[i].isInstance ]
• let k := S.size-1
• let [α'₀, ..., α'ₚ] := [ αᵢ [S[0]/R[0]] ... [S[k]/R[k]] | i ∈ [0..n] ∧ params[i].isInstance ]
• return ∀ α'₀ → ∀ α'₁ ... → α'ₚ TODO: change function to pure tail rec call using stack-based approach

Equations

• Blaster.Smt.inferUndeclFunType t params = Blaster.Smt.inferUndeclFunType.visit params 0 t

partial def Blaster.Smt.inferUndeclFunType.visit (params : Optimize.ImplicitParameters) (idx : Nat) (t : Lean.Expr) : Lean.Expr

def Blaster.Smt.generateUndeclaredFun (f : Lean.Expr) (s : SmtSymbol) (params : Optimize.ImplicitParameters) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) : Optimize.TranslateEnvT Unit

Given f corresponding to either an undeclared class function, an axiom function or an opaque function params its corresponding implicit/explicit parameters and s its corresponding smt symbol, perform the following:

• Let ∀ α₀ → ∀ α₁ ... → αₙ := inferUndecFunType (← getFunEnvInfo f).type params
• declare smt function declare-fun s ((st₀) .. (stₙ₋₁)) stₙ)
• assert the following proposition to constraint the codomain value:
  • (assert (forall ((@x₀ st₀) ... (@xₙ₋₁ stₙ₋₁)) (! (@isTypeₙ (s @x₁ ... @xₙ₋₁)) :pattern ((s @x₁ ... @xₙ₋₁))) :qid s_cstr)

where ∀ i ∈ [0..n], αᵢ translates to Smt type stᵢ

Equations

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

def Blaster.Smt.translateConst (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) : Optimize.TranslateEnvT SmtTerm

Given e := Expr.const n l,

• When n := false
  • return BoolTerm false
• When n := False
  • return BoolTerm false
• When n := true
  • return BoolTerm true
• When n := True
  • return BoolTerm true
• When n := Int.ofNat
  • return termTranslator (← etaExpand e)
• When isInductiveTypeExpr e
  • return ⊥
• When isForbiddenUnappliedConst n
  • return ⊥
• When isMatchExpr e
  • return ⊥
• When n is a constructor with implicit arguments
  • return ⊥
• When n is a nullary constructor
  • return SmtIdent (.QualifiedIdent n (translateType termTranslator Type(n)))
• When n is a parameterized constructor
  • return termTranslator (← etaExpand e)
• When hasImplicitArgs e
  • return ⊥
• When n ∈ opaqueFuns ∨ isRecursiveFun n
  • return termTranslator (← etaExpand e)
• When isTheorem n ∧ ¬ hasSorryTheorem e ∧ ¬ Type(e).isForAll
  • return termTranslator (← optimizeExpr' Type(e))
• When isAxiom n ∨ some ConstantInfo.opaqueInfo _ ← getConstEnvInfo n
  • When n := s ∈ axiomMap:
    • return smtSimpleVarId s
  • Otherwise:
    • When isFunType Type(e)
      • return termTranslator (← etaExpand e)
    • Otherwise:
      • Let s = nameToSmtSymbol n
      • add n := s to axiomMap
      • Let t' ← removeTypeAbbrev Type(e)
      • Let st ← translateTypeAux termTranslator t'
      • declare smt symbol (declare-const s st)
      • Let pterm ← createPredQualifierApp s t'
      • assert term (assert pterm)
      • return smtSimpleVarId s
• Otherwise
  • return ⊥ An error is triggered when e is not a name expression.

NOTE: This function cannot be called on fun name expression (i.e., f x₁ ... xₙ, where e := f and f is a partially or totally applied function). It can only be applied on functions passed as arguments.

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateConst (Lean.Expr.const `Bool.false us) termTranslator = pure Blaster.Smt.falseSmt
• Blaster.Smt.translateConst (Lean.Expr.const `False us) termTranslator = pure Blaster.Smt.falseSmt
• Blaster.Smt.translateConst (Lean.Expr.const `Bool.true us) termTranslator = pure Blaster.Smt.trueSmt
• Blaster.Smt.translateConst (Lean.Expr.const `True us) termTranslator = pure Blaster.Smt.trueSmt
• Blaster.Smt.translateConst e termTranslator = Blaster.Optimize.throwEnvError (Lean.toMessageData "translateConst: name expression expected but got " ++ Lean.toMessageData (reprStr e))

def Blaster.Smt.translateConst.translateCtor (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (c : Lean.Name) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

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

def Blaster.Smt.translateConst.translateDefineFun? (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (n : Lean.Name) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

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

def Blaster.Smt.translateConst.translateTheorem? (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (n : Lean.Name) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

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

def Blaster.Smt.translateConst.getAxiomOpaqueType (n : Lean.Name) : Optimize.TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Smt.translateConst.translateAxiomOrOpaque? (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (n : Lean.Name) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

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

def Blaster.Smt.translateConst.isForbiddenUnappliedConst (n : Lean.Name) : Bool

Equations

• Blaster.Smt.translateConst.isForbiddenUnappliedConst `Exists = Blaster.Smt.isForbiddenConst `Exists
• Blaster.Smt.translateConst.isForbiddenUnappliedConst `Blaster.decide' = Blaster.Smt.isForbiddenConst `Blaster.decide'
• Blaster.Smt.translateConst.isForbiddenUnappliedConst `Blaster.dite' = Blaster.Smt.isForbiddenConst `Blaster.dite'
• Blaster.Smt.translateConst.isForbiddenUnappliedConst n = Blaster.Smt.isForbiddenConst n

def Blaster.Smt.translateApp (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) : Optimize.TranslateEnvT SmtTerm

Translate Application TODO: UPDATE

Equations

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

def Blaster.Smt.translateApp.translateEq? (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (f : Lean.Expr) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateApp.translateEq? e termTranslator f n args = pure none

def Blaster.Smt.translateApp.translateDITE? (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (f : Lean.Expr) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateApp.translateDITE? termTranslator f n args = pure none

def Blaster.Smt.translateApp.translateOfNat? (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateApp.translateOfNat? termTranslator n args = pure none

def Blaster.Smt.translateApp.translateDecide? (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateApp.translateDecide? termTranslator n args = pure none

def Blaster.Smt.translateApp.translateRelational? (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (f : Lean.Expr) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateApp.translateRelational? e termTranslator f n args = pure none

def Blaster.Smt.translateApp.genExistsTerm (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (lambdaE : Lean.Expr) : QuantifierEnvT SmtTerm

Equations

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

def Blaster.Smt.translateApp.translateExists? (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateApp.translateExists? termTranslator n args = pure none

def Blaster.Smt.translateApp.translateRecFun? (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (f : Lean.Expr) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

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

def Blaster.Smt.translateApp.translateAppliedCtor? (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (f : Lean.Expr) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

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

def Blaster.Smt.translateApp.getUndeclFunAppInst (f : Lean.Expr) (params : Optimize.ImplicitParameters) : Optimize.TranslateEnvT Lean.Expr

Equations

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

def Blaster.Smt.translateApp.isOpaqueAxiomOrUndeclFun (f : Lean.Expr) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT Bool

Equations

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

def Blaster.Smt.translateApp.translateAxiomOrUndeclFun? (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (f : Lean.Expr) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

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

def Blaster.Smt.translateApp.translateFullyApplied? (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (f : Lean.Expr) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

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

def Blaster.Smt.translateApp.translateInductivePredicate? (f : Lean.Expr) (n : Lean.Name) (_args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

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

def Blaster.Smt.translateApp.translateTheorem (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (n : Lean.Name) (args : Array Lean.Expr) : Optimize.TranslateEnvT (Option SmtTerm)

Equations

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

def Blaster.Smt.translateLambda (e : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) : Optimize.TranslateEnvT SmtTerm

Given e := λ (x₁ : t₁) → λ (xₙ : tₙ) => b, perform the following:

• let V := [ v | v ∈ getFVarsInExpr b ∧ ¬ isType v.type ∧ ¬ isClassConstraintExpr v.type ∧ ¬ isTopLevelFVar v ]
• let A := [x₁, ..., xₙ]
• let (x₁, st₁) ... (xₘ, stₘ) := [(A[i], translateFunLambdaParamType tᵢ termTranslator) | i ∈ [0..n] ∧ isExplicit A[i]]
• let rt ← translateFunLambdaParamType (← inferTypEnv b) termTranslator
• let n ← mkFreshId
• let FunArrowType := ArrowTN st₁ ... stₘ rt
• let decl ← generateFunInstDeclAux (← inferTypeEnv e) FunArrowType
• let some @apply{k} := decl.applyInstName
• let sb := termTranslator b
• When V = ∅
  • declare smt function (declare-const @lambda{n} FunArrowType)
  • assert the following proposition to properly constrain @lambda{n}: (assert (forall ((x₁ st₁) ... (xₘ stₘ)) (! (= (@apply{k} @lambda{n} x₁ ... xₘ) sb) :pattern ((@apply{k} @lambda{n} x₁ ... xₘ)) :qid @lambda{n]_def_cstr)))
  • return smtSimpleVarId @lambda{n}
• When V ≠ ∅
  • let (y₁, yt₁) ... (yₖ, ytₖ) := [(V[i], translateFunLambdaParamType V[i].type termTranslator) | i ∈ [0..V.size-1]]
  • let GlobalArrowType := ArrowTN yt₁ ... ytₖ FunArrowType
  • let [v₁, ..., vₖ] = V
  • let globalType ← ∀ v₁ → ... ∀ vₖ → outParam (← inferTypeEnv e)
  • let globalDecl ← generateFunInstDeclAux globalType GlobalArrowType
  • let some @apply{n} := globalDecl.applyInstName
  • declare smt function (declare-const @global_lambda{n} GlobalArrowType)
  • assert the following proposition to properly constrain @global_lambda{n}!
    • (assert (forall ((y₁, yt₁) ... (yₖ, ytₖ) (x₁, st₁) ... (xₘ, stₘ)) (! (= (@apply{k} (@apply{n} @global_lambda{n} y₁ ... yₖ) x₁ ... xₘ) sb) :pattern ((@apply{k} (@apply{n} @global_lambda{n} y₁ ... yₖ) x₁ ... xₘ)) :qid @global_lambda{n}_def_cstr)))
  • return (@apply{n} @global_lambda{n} y₁ ... yₖ)

Equations

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

def Blaster.Smt.translateLambda.retrieveLocalFVars (b : Lean.Expr) : Optimize.TranslateEnvT (Array Lean.Expr)

Equations

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

def Blaster.Smt.translateProj (n : Lean.Name) (idx : Nat) (p : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) : Optimize.TranslateEnvT SmtTerm

Given n a projection name, idx a projection and p the projection application term, perform the following:

• When n is not an inductive datatype (i.e., structure definition)
  • return ⊥
• When n has more than one ctor c (i.e., structure only has one defined ctor with each field as arguments)
  • return ⊥
• Otherwise:
  • return smt term application (c.idx+1 p)

Equations

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