def Blaster.Smt.removeTypeAbbrev (te : Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

Removes an occurrence of type abbreviation in type expression t

Equations

• Blaster.Smt.removeTypeAbbrev te = Blaster.Smt.removeTypeAbbrev.visit te fun (e : Lean.Expr) => pure e

partial def Blaster.Smt.removeTypeAbbrev.visit (te : Lean.Expr) (k : Lean.Expr → Optimize.TranslateEnvT Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

def Blaster.Smt.nameToSmtSymbol (n : Lean.Name) : SmtSymbol

Generate an smt symbol from a given Name.

Equations

• Blaster.Smt.nameToSmtSymbol n = Blaster.Smt.mkNormalSymbol (toString n)

def Blaster.Smt.sortNameToSmtSymbol (v : Lean.FVarId) (unique : Bool := true) : Optimize.TranslateEnvT SmtSymbol

Generate a smt symbol for a free variable id corresponding to a sort name (e.g., α : Type) s.t.:

• return smt symbol "@" ++ v.getUserName ++ v.name when unique is set to true
• return smt symbol "@" ++ v.getUserName otherwise.

Equations

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

def Blaster.Smt.indNameToSmtSymbol (indName : Lean.Name) : SmtSymbol

Generate an smt symbol from a given inductive type name.

Equations

• Blaster.Smt.indNameToSmtSymbol indName = Blaster.Smt.mkNormalSymbol (toString "@" ++ toString indName.toString)

def Blaster.Smt.toTaggedCtorSelector? (e : Lean.Expr) : Option Lean.Expr

Return some b if e := mkAnnotation __solver.ctorSelector b'`.

Equations

• Blaster.Smt.toTaggedCtorSelector? (Lean.Expr.mdata d b) = if (Lean.KVMap.size d == 1 && Lean.KVMap.getBool d `_solver.ctorSelector) = true then some b else none
• Blaster.Smt.toTaggedCtorSelector? e = none

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

Return true if e := mkAnnotation _solver.ctorSelector b'`.

Equations

• Blaster.Smt.isTaggedCtorSelector (Lean.Expr.mdata d b) = (Lean.KVMap.size d == 1 && Lean.KVMap.getBool d `_solver.ctorSelector)
• Blaster.Smt.isTaggedCtorSelector e = false

def Blaster.Smt.mkCtorSelectorSymbol (ctor : Lean.Name) (idx : Nat) : SmtSymbol

Given ctor a constructor name and idx corresponding to the index for one of the ctor's effective parameters, create the ctor selector symbol ctor.idx

Equations

• Blaster.Smt.mkCtorSelectorSymbol ctor idx = Blaster.Smt.mkNormalSymbol (toString ctor ++ toString "." ++ toString idx)

def Blaster.Smt.mkCtorSelectorExpr (ctor : Lean.Name) (idx : Nat) (arg type : Lean.Expr) : Optimize.TranslateEnvT (Lean.Expr × SmtTerm)

Given ctor a constructor name and idx corresponding to the index for one of the ctor's arguments and arg the current ctor arg and t its corresponding type, perform the following:

• add {ctor}.idx := ← getFunEnvInfo arg to funCtorCache when isFunType t
• create expression ctor.idx x and tag it as a ctor selector.
• create the corresponding smt term
• return both as result The tag is used during translation.

Equations

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

def Blaster.Smt.mkCtorTestorTerm (ctor : Lean.Name) (s : SmtTerm) : SmtTerm

Given ctor a constructor name and an smt term s, create the smt term application is-ctor s.

Equations

• Blaster.Smt.mkCtorTestorTerm ctor s = Blaster.Smt.mkSimpleSmtAppN (Blaster.Smt.mkNormalSymbol (toString "is-" ++ toString ctor)) #[s]

def Blaster.Smt.mkGenericCtorTestorTerm (ctor : Lean.Name) : SmtTerm

Given ctor a constructor name, create the smt term is-ctor x.

Equations

• Blaster.Smt.mkGenericCtorTestorTerm ctor = Blaster.Smt.mkCtorTestorTerm ctor (Blaster.Smt.smtSimpleVarId (Blaster.Smt.mkReservedSymbol "@x"))

def Blaster.Smt.declareArrowTypeSort (nbArity : Nat) : Optimize.TranslateEnvT SmtSymbol

Return s when nbArity := s exists in arrowTypeArities. Otherwise, perform the following:

• let s := @@ArrowT{nbArity}
• Add entry nbArity := s in arrowTypeArities
• declare sort (declare-sort s nbArity)
• return s

Equations

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

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

Define smt universal sort @@Type and its corresponding predicate qualified whenever flag typeUniverse is not set. Do nothing otherwise. Assume isTypeSym := @isType

Equations

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

def Blaster.Smt.updateSortCache (v : Lean.FVarId) (s : SmtSymbol) : Optimize.TranslateEnvT Unit

Update sort cache with v.

Equations

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

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

Return vstrₙ when entry v := vstrₙ exists in sortCache, otherwise, perform the following:

• vstr := "@" ++ v.getUserName ++ v.name.
• add define-sort "vstr" () @@Type to the Smt context
• add entry v := vstr to sortCache
• return vstr

Equations

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

def Blaster.Smt.cacheIndName (indName : Lean.Name) : Optimize.TranslateEnvT Unit

Add an inductive datatype name to the visited inductive datatype cache.

Equations

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

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

Return true when indName is already in the visited inductive datatype cache (i.e., indTypeCache)

Equations

• Blaster.Smt.isVisitedIndName indName = do let __do_lift ← get pure (__do_lift.smtEnv.indTypeVisited.contains indName)

def Blaster.Smt.updateIndInstCacheAux (d : Lean.Expr) (n : SmtSymbol) (instSort : SortExpr) (isReservedSymbol : Bool := false) (applyInstName : Option SmtSymbol := none) : Optimize.TranslateEnvT Optimize.IndTypeDeclaration

Given d corresponding to a inductive datatype name expression, or an instantiated polymorphic inductive datatype, or a function instance declaration and n a unique smt identifier generated for d and instSort the instantiated Smt sort for d, perform the following:

• add entry d := {instName := "@is{n}", instSort, applyInstName} in indTypeInstCache
• return {instName := "@is{n}", instSort, applyInstName}

with applyInstName set to none for inductive datatype and set to some @apply{uniq_xxx}. See function generateFunInstDeclAux.

Equations

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

def Blaster.Smt.updateIndInstCache (d : Lean.Expr) (n : SmtSymbol) (instSort : SortExpr) : Optimize.TranslateEnvT Unit

Same as updateIndInstCacheAux but return value is discarded.

Equations

• Blaster.Smt.updateIndInstCache d n instSort = discard (Blaster.Smt.updateIndInstCacheAux d n instSort)

def Blaster.Smt.isTopLevelFVar (v : Lean.FVarId) : Optimize.TranslateEnvT Bool

Return true if v is tagged as a top level free variable.

Equations

• Blaster.Smt.isTopLevelFVar v = do let __do_lift ← get match __do_lift.smtEnv.quantifiedFVars.get? v with | none => pure false | some b => pure b

def Blaster.Smt.updateQuantifiedFVarsCache (v : Lean.FVarId) (topLevel : Bool) : Optimize.TranslateEnvT Unit

Perform the following:

• add v to quantifierFvars cache
• add v to topLevelVars only when topLevel is set to true and ¬ isType (← inferTypeEnv (mkFVar v)).

Equations

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

def Blaster.Smt.isInQuantifiedFVarsCache (v : Lean.FVarId) : Optimize.TranslateEnvT Bool

Return true if v is in the quantified fvars cache.

Equations

• Blaster.Smt.isInQuantifiedFVarsCache v = do let __do_lift ← get pure (__do_lift.smtEnv.quantifiedFVars.contains v)

def Blaster.Smt.isPatternMatchFVar (v : Lean.FVarId) : Optimize.TranslateEnvT Bool

Return true when an entry exists for v in inPatternMatching.

Equations

• Blaster.Smt.isPatternMatchFVar v = do let __do_lift ← get pure (__do_lift.smtEnv.options.inPatternMatching.contains v)

def Blaster.Smt.createSortExpr (args : Array SortExpr) : Optimize.TranslateEnvT SortExpr

Return an Smt Array sort when args.size > 1. Otherwise return args[0]!. An error is triggered when args.size < 1.

Equations

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

def Blaster.Smt.generateInstType (indName : Lean.Name) (args : Array Lean.Expr) (typeTranslator : Lean.Expr → Optimize.TranslateEnvT SortExpr) : Optimize.TranslateEnvT SortExpr

Given n corresponding to the name of an inductive datatype, and x₀ ... xₖ the parameters instantiating the inductive datatype, perform the following actions:

• When k > 0: let A := [x₀, ..., xₖ] let B := [typeTranslator A[i] | i ∈ [0..k] ∧ ¬ isClassConstraintExpr (← inferTypeEnv A[i])]
  • return ParamSort (indNameToSmtSymbol n) B
• When k = 0:
  • return SymbolSort indNameToSmtSymbol n)

Equations

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

def Blaster.Smt.retrieveGenericArgs (args : Array Lean.Expr) : Optimize.TranslateEnvT (Array Lean.Expr)

Given arguments x₀ ... xₙ perform the following: let A := [x₀, ..., xₙ] let V := {α | i ∈ [0..n] ∧ α ∈ getFVarsInExpr A[i] ∧ isGenericParam A[i]} return [α | α ∈ V]

Equations

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

def Blaster.Smt.getIndInst (t : Lean.Expr) (args : Array Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

Given an inductive datatype instance t x₀ ... xₙ, perform the following:

• When ∀ i ∈ [0..n], ¬ isGenericParam xᵢ,
  • return t x₀ ... xₙ
• When ∃ i ∈ [0..n], isGenericParam xᵢ, let A := [x₀, ..., xₙ] let V := [α | i ∈ [0..n] ∧ α ∈ getFVarsInExpr A[i] ∧ isGenericParam A[i] ] let [b₀ ... bₘ ] := V
  • return λ b₀ → .. → bₘ → t x₀ ... xₙ

Equations

• Blaster.Smt.getIndInst t args = do let genericArgs ← Blaster.Smt.retrieveGenericArgs args have auxApp : Lean.Expr := Lean.mkAppN t args liftM (Lean.Meta.mkLambdaFVars genericArgs auxApp true)

def Blaster.Smt.retrieveArrowTypes (t : Lean.Expr) : Array Lean.Expr

Given t := ∀ α₀ → ∀ α₁ ... → αₙ returns #[α₀, α₁ ..., αₙ]. Assumes that t no more contains any class constraints (see function removeClassConstraintsInFunType).

Equations

• Blaster.Smt.retrieveArrowTypes t = Blaster.Smt.retrieveArrowTypes.visit t #[]

def Blaster.Smt.retrieveArrowTypes.visit (e : Lean.Expr) (arrowTypes : Array Lean.Expr) : Array Lean.Expr

Equations

• Blaster.Smt.retrieveArrowTypes.visit (Lean.Expr.forallE binderName t b binderInfo) arrowTypes = Blaster.Smt.retrieveArrowTypes.visit b (arrowTypes.push t)
• Blaster.Smt.retrieveArrowTypes.visit e arrowTypes = arrowTypes.push e

def Blaster.Smt.removeClassConstraintsInFunType (t : Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

Given t := ∀ α₀ → ∀ α₁ ... → αₙ, perform the following:

• let A := [αᵢ | i ∈ [0..n-1], isClassConstraintExpr αᵢ]
• let [α'₀ ... α'ₚ] := A
• return ∀ α'₀ → α'₁ → ... → α'ₚ → αₙ`

Equations

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

def Blaster.Smt.generateIndInstDecl (t : Lean.Expr) (args : Array Lean.Expr) (assertFlag : Option Bool) (typeTranslator : Lean.Expr → Optimize.TranslateEnvT SortExpr) (declarePredicate : Bool := true) : Optimize.TranslateEnvT Optimize.IndTypeDeclaration

Given t := Expr.const n _ corresponding to an inductive datatype name and args the parameters instantiating the inductive datatype (if any), perform the following actions:

• When args.size > 0:
  • instName := nameToSmtSymbol (n ++ (← mkFreshId)) (i.e., generate a unique name for instance)
  • instSort ← generateInstType n args typeTranslator
  • instApp ← getIndInst t args
  • add entry instApp := {@is{instName}, instSort} to indTypeInstCache
  • When declarePredicate:
    • When assertFlag := some b:
      • define smt predicate (define-fun @is{instName} ((@x instSort)) Bool b)
    • Otherwise:
      • declare smt predicate (declare-fun @is{instName} ((instSort)) Bool)
  • return {instName, instSort}
• When args.size = 0:
  • instName := nameToSmtSymbol n
  • instSort ← generateInstType n args typeTranslator
  • add entry t := {@is{instName}, instSort} to indTypeInstCache
  • When declarePredicate:
    • When assertFlag := some b:
      • define smt predicate (define-fun @is{instName} ((@x instSort)) Bool b)
    • Otherwise:
      • declare smt predicate (declare-fun @is{instName} ((instSort)) Bool)
  • return {instName, instSort} Assumes that t corresponds to the name of an inductive datatype.

Equations

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

def Blaster.Smt.getFunInstDeclAux (t : Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

Given t := ∀ α₀ → ∀ α₁ ... → αₙ, perform the following: Let A := [αᵢ | i ∈ [0..n-1]]

• When ∀ i ∈ [0..n], ¬ isGenericParam A[i],
  • return t
• When ∃ i ∈ [0..n], isGenericParam A[i], let V := {v | i ∈ [0..n] ∧ v ∈ getFVarsInExpr A[i] ∧ isGenericParam A[i]} let B := [v | v ∈ V] ++ [A[i] | i ∈ [0..n] ∧ isGenericParam A[i]] let [b₀ ... bₘ ] := B let [α'₀ ... α'ₚ] := A
  • return λ b₀ → .. → bₘ → ∀ α'₀ → α'₁ → ... → α'ₚ → αₙ Assumes that t does not have any implicit types (i.e., removeClassConstraintsInFunType called)

Equations

• Blaster.Smt.getFunInstDeclAux t = do let genericArgs ← Blaster.Smt.retrieveGenericArgs (Blaster.Smt.retrieveArrowTypes t) liftM (Blaster.Optimize.mkLambdaFVars' genericArgs t)

def Blaster.Smt.getFunInstDecl (t : Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

Same as getFunInstDeclAux but calls removeClassConstraintsInFunType on t` first.

Equations

• Blaster.Smt.getFunInstDecl t = do let t' ← Blaster.Smt.removeClassConstraintsInFunType t Blaster.Smt.getFunInstDeclAux t'

def Blaster.Smt.withInstantiatedImplicitArgs {α : Type} (t : Lean.Expr) (k : Lean.Expr → Optimize.TranslateEnvT α) : Optimize.TranslateEnvT α

Given t := ∀ α₀ → ∀ α₁ ... → αₙ, execute k t', with t' obtained as follows:

• let [α'₀ ... α'ₚ] := [αᵢ | i ∈ [0..n-1], isExplicit αᵢ]
• t' := ∀ α'₀ → α'₁ → ... → α'ₚ → αₙ`
• with free variables created for implicit arguments.

Equations

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

def Blaster.Smt.getPredicateDeclaration (t : Lean.Expr) : Optimize.TranslateEnvT (Option Optimize.IndTypeDeclaration)

Return decl.instName when t := decl exists in indTypeInstCache. Otherwise none. TODO: UPDATE

Equations

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

def Blaster.Smt.getPredicateDeclaration.getInst (e : Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

Equations

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

def Blaster.Smt.getPredicateDeclaration.getType (e : Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

Equations

• Blaster.Smt.getPredicateDeclaration.getType (Lean.Expr.fvar fvarId) = Blaster.Optimize.inferTypeEnv (Lean.Expr.fvar fvarId)
• Blaster.Smt.getPredicateDeclaration.getType e = pure e

def Blaster.Smt.getApplyInstName (t : Lean.Expr) : Optimize.TranslateEnvT SmtSymbol

Return n only when entry t := decl exists in indTypeInstCache and decl.applyInstName := some n. An error is triggered when:

• no entry exist for t
• decl.applyInstName is set to none.

Equations

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

def Blaster.Smt.createPredQualifierAppAux (st : SmtTerm) (t : Lean.Expr) : Optimize.TranslateEnvT SmtTerm

Given st an smt term and t its corresponding type expression, perform the following:

• retrieve predicate qualifier name instName for t
• return smt application (instName v) An error is triggered if the predicate qualifier name for t does not exists. Assume that there is no type abbreviation in t, i.e., call to removeTypeAbbrev has been applied.

Equations

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

def Blaster.Smt.createPredQualifierApp (smtSym : SmtSymbol) (t : Lean.Expr) : Optimize.TranslateEnvT SmtTerm

Same as createPredQualifierAppAux but accepts an SmtSymbol as argument.

Equations

• Blaster.Smt.createPredQualifierApp smtSym t = Blaster.Smt.createPredQualifierAppAux (Blaster.Smt.smtSimpleVarId smtSym) t

def Blaster.Smt.generateFunInstDeclAux (t : Lean.Expr) (st : SortExpr) : Optimize.TranslateEnvT Optimize.IndTypeDeclaration

Given t := α₁ → α₂ ... → αₙ and st its corresponding smt representation (i.e., ArrowTN sα₁ sα₂ sαₙ), perform the following action:

• let funInst ← getFunInstDecl t
• When funInst := {@is{instName}, st, applyInstName} ∈ indTypeInstCache
  • return {@is{instName}, st, applyInstName}
• Otherwise:
  • let n ← mkFreshId
  • instName ← (Fun ++ n) (i.e., generate a unique name for function instance)
  • add entry t := {@is{instName}, st, applyInstName := some @apply{n}} to indTypeInstCache
  • declare smt predicate (declare-fun @is{instName} ((instSort)) Bool)
  • declare apply function (declare-fun @apply{n} (st sα₁ ... sαₙ₋₁) sαₙ)
  • assert the following propositions to specify congruence, extensionality and codomain values constraints:

    • (assert (forall ((@f (ArrowTN sα₁ sα₂ sαₙ))(@x₁ sα₁) ... (@xₙ₋₁ sαₙ₋₁) (@y₁ sα₁) ... (@yₙ₋₁ sαₙ₋₁)) (! (=> (= @x₁ @y₁) (=> (= @x₂ @y₂) ... (=> (= @xₙ₋₁ @yₙ₋₁) (= (@apply{n} @f @x₁ ... @xₙ₋₁) (@apply{n} @f @y₁ ... @yₙ₋₁))))) :pattern ((@apply{n} @f @x₁ ... @xₙ₋₁) (@apply{n} @f @y₁ ... @yₙ₋₁) (= @x₁ @y₁) ... (= @xₙ₋₁ @yₙ₋₁)) :qid @apply{n}_congr_args)))

    • (assert (forall ((@f (ArrowTN sα₁ sα₂ sαₙ)) (@g (ArrowTN sα₁ sα₂ sαₙ)) (@x₁ sα₁) ... (@xₙ₋₁ sαₙ₋₁)) (! (=> (= @f @g) (= (@apply{n} @f @x₁ ... @xₙ₋₁) (@apply{n} @g @x₁ ... @xₙ₋₁))) :pattern ((@apply{n} @f @x₁ ... @xₙ₋₁) (@apply{n} @g @x₁ ... @xₙ₋₁) (= @f @g)) :qid @apply{n}_congr_fun)))

    • (assert (forall ((@f (ArrowTN sα₁ sα₂ sαₙ)) (@g (ArrowTN sα₁ sα₂ sαₙ)) (@x₁ sα₁) ... (@xₙ₋₁ sαₙ₋₁)) (! (=> (= (@apply{n} @f @x₁ ... @xₙ₋₁) (@apply{n} @g @x₁ ... @xₙ₋₁)) (= @f @g)) :pattern (= (@apply{n} @f @x₁ ... @xₙ₋₁) (@apply{n} @g @x₁ ... @xₙ₋₁))) :qid @apply{n}_ext_fun)))

    • (assert (forall ((@f (ArrowTN sα₁ sα₂ ... αₙ))) (! (= (forall ((@x₁ sα₁) ... (@xₙ₋₁ sαₙ₋₁)) (@isTypeₙ (@apply{n} @f @x₁ ... @xₙ₋₁))) (@is{instName} @f) ) :pattern ( (@is{instName} @f)) :qid @isFun{v}_cstr)))

    • with ∀ i ∈ [1..n] = s

  • return {@is{instName}, st}

Equations

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

def Blaster.Smt.generateFunInstDeclAux.removeOutParam : Lean.Expr → Lean.Expr

Equations

• Blaster.Smt.generateFunInstDeclAux.removeOutParam ((Lean.Expr.const `outParam us).app e) = e
• Blaster.Smt.generateFunInstDeclAux.removeOutParam x✝ = x✝

def Blaster.Smt.generateFunInstDeclAux.generateApplyFunAndAssertions (st : SortExpr) (t : Lean.Expr) (instName applyName : SmtSymbol) : Optimize.TranslateEnvT Unit

Equations

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

@[inline]

def Blaster.Smt.generateFunInstDecl (t : Lean.Expr) (st : SortExpr) : Optimize.TranslateEnvT Unit

Same as generateFunInstDeclAux but return ().

Equations

• Blaster.Smt.generateFunInstDecl t st = discard (Blaster.Smt.generateFunInstDeclAux t st)

def Blaster.Smt.generateSortInstDecl (t : Lean.Expr) : Optimize.TranslateEnvT Unit

Given t := Expr.sort _ perform the following actions only when no entry for t exists in indTypeInstCache:

• When t := Expr.sort .zero

  • add entry t := {@isProp, propSort} to indTypeInstCache`
  • define smt sort (define-sort Prop () Bool)
  • declare smt function (declare-fun @isProp ((Prop)) Bool) with true assertion

• When isType t

  • add entry t := {@isType, typeSort} to indTypeInstCache`
  • Define smt univseral sort @@Type when flag typeUniverse is not set (see function declareTypeSort`)

An error is triggered when t is not the expected sort type.

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.generateSortInstDecl t = Blaster.Optimize.throwEnvError (Lean.toMessageData "generateSortInstDecl: sort type expected but got " ++ Lean.toMessageData (reprStr t))

def Blaster.Smt.getRecRuleFor (recVal : Lean.RecursorVal) (c : Lean.Name) : Optimize.TranslateEnvT Lean.RecursorRule

TODO: UPDATE SPEC

Equations

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

structure Blaster.Smt.TypeOptions : Type

Options for translateType.

• inTypeDefinition : Bool

  flag set to true only when translating an inductive datatype so as not to generate predicate qualifier for generic types used in ctor parameters.

• genericParamFun : Bool

  flag set to true only when translating type of function arguments so as to use universal sort @@Type when function are still polymorphic after instantiation.

def Blaster.Smt.instInhabitedTypeOptions.default : TypeOptions

Equations

• Blaster.Smt.instInhabitedTypeOptions.default = { inTypeDefinition := default, genericParamFun := default }

instance Blaster.Smt.instInhabitedTypeOptions : Inhabited TypeOptions

Equations

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

def Blaster.Smt.optionsForInductiveType : TypeOptions

type options to be used when translating inductive datatype.

Equations

• Blaster.Smt.optionsForInductiveType = { inTypeDefinition := true }

def Blaster.Smt.optionsForPredicateQualifier : TypeOptions

type options to be used when generating predicate qualifiers.

Equations

• Blaster.Smt.optionsForPredicateQualifier = { genericParamFun := true }

def Blaster.Smt.optionsForFunLambdaParam : TypeOptions

Same as optionsForPredicateQualifier.

Equations

• Blaster.Smt.optionsForFunLambdaParam = { genericParamFun := true }

def Blaster.Smt.translateInductiveType (indValStart : Lean.InductiveVal) (typeTranslator : Lean.Expr → Optimize.TranslateEnvT SortExpr) : Optimize.TranslateEnvT Unit

TODO: UPDATE SPEC

Given indValStart an inductive value info for an inductive datatype, update the inductive datatype declaration indTypeMap. Intuitively, for the non-mutual inductive List, inductive List (α : Type u) where | nil : List α | cons (head : α) (tail : List α) : List α

The following entry will be added. `List := [{ indName := List, numParams := 1, hasProp := false ctors := [ { ctorName := nil, nbFields := 0, hasProp := false, propIndices := [], rhs := λ α : Type u → nil }, { ctorName := cons, nbFields := 2, hasProp := false, propIndices := [], rhs := λ α : Type u → λ head : α → λ tail : List α → cons head tail } ]

As for the following mutual inductive declaration, mutual inductive Attribute (α : Type u) where | Named (n : String) | Pattern (p : List (Term α)) | Qid (n : String)

inductive Term (α : Type u) where
| Ident (s : String)
| App (nm : String) (args : List (Term α))
| Annotated (t : Term α) (annot : List (Attribute α))

end

The following entries will be added:

• Attribute := decls
• Term := decls with decls := [{ indName := Attribute, numParams := 1, hasProp := false, ctors := [ { ctorName := Named, nbFields := 1, hasProp := false, propIndices := [], rhs := λ α : Type u → λ n : String → Named n }, { ctorName := Pattern, nbFields := 1, hasProp := false, propIndices := [], rhs := λ α : Type u → λ p : List (Term α) → Pattern p } { ctorName := Qid, nbFields := 1, hasProp := false, propIndices := [], rhs := λ α : Type u → λ n : String → Qid n } ] }, { indName := Term, numParams := 1, hasProp := false, ctors := [ { ctorName := Named, nbFields := 1, hasProp := false, propIndices := [], rhs := λ α : Type u → λ s : String → Ident s }, { ctorName := App, nbFields := 2, hasProp := false, propIndices := [], rhs := λ α : Type u → λ nm : String → λ args : List (Term α) → App nm args }, { ctorName := Annotated, nbFields := 2, hasProp := false, propIndices := [], rhs := λ α : Type u → λ t : Term α → λ annot : List (Attribute α) → Annotated nm args } ] } ]

Note that optimizer is called on each constructor rhs to apply proper formalization when at least one of the arguments is a proposition.

An error is triggered when:

• ∀ n ∈ indValStart.all
  • no inductive info is found for n;
  • no recursive info is found for n;
  • no recursor rule is found for at least one constructor for n.

Equations

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

def Blaster.Smt.translateInductiveType.defineDataType (sortDecls : Array SmtSortDecl) (typeDecls : Array SmtDatatypeDecl) : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.Smt.translateInductiveType.genIndParams (indVal : Lean.InductiveVal) : Optimize.TranslateEnvT (Option (Array SmtSymbol))

Equations

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

def Blaster.Smt.translateInductiveType.createCtorDeclaration (typeTranslator : Lean.Expr → Optimize.TranslateEnvT SortExpr) (recVal : Lean.RecursorVal) (recRule : Lean.RecursorRule) : Optimize.TranslateEnvT SmtConstructorDecl

Equations

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

def Blaster.Smt.translateInductiveType.createCtorDecls (typeTranslator : Lean.Expr → Optimize.TranslateEnvT SortExpr) (recVal : Lean.RecursorVal) (ctors : List Lean.Name) : Optimize.TranslateEnvT (Array SmtConstructorDecl)

Equations

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

partial def Blaster.Smt.defineInstPredicateQualifier (typeTranslator : Lean.Expr → Optimize.TranslateEnvT SortExpr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (t : Lean.Expr) (args : Array Lean.Expr) : Optimize.TranslateEnvT Unit

Given an instantiated inductive data type t x₁ ... xₙ, generate it's corresponding predicate qualifier predicate and propositional assertions when instance is not already in indTypeInstCache. In particular,

• let instApp ← getIndInst t #[x₁, ..., xₙ]
• When instApp := {instName, instSort} ∈ indTypeInstCache
  • return ()
• Otherwise:
  • let {instName, instSort} ← generateIndInstDecl t args typeTranslator
  • When `∀ c ∈ Ctors(t), c = C (i.e., nullary constructors)
    • declare smt predicate (declare-fun @is{instName} ((instSort)) Bool)`
  • Otherwise:
    • declare smt predicate (declare-fun @is{instName} ((instSort)) Bool)`
    • For each c ∈ Ctors(t),
      • When c = C (i.e., nullary constructor) don't generate any assertion
      • When c = C p₁ ... pₙ, generate assertion (assert (forall ((@x instSort)) (! (=> (@is{instName} @x) (=> is-C @x (and predTermᵢ ... predTermₙ))) :pattern ((@is{instName} @x) (is-C @x))))) with ∀ i ∈ [1..n], (isProp pᵢ → predTermᵢ = (= (C.i @x) (← termTranslator (← optimizeExpr pᵢ)))) ∧ (¬ isProp pᵢ → predTermᵢ = (isTypeᵢ (C.i @x))) TODO: UPDATE SPEC

def Blaster.Smt.defineInstPredicateQualifier.isEnumeration (indVal : Lean.InductiveVal) : Optimize.TranslateEnvT Bool

Equations

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

partial def Blaster.Smt.defineInstPredicateQualifier.declareIndInst (typeTranslator : Lean.Expr → Optimize.TranslateEnvT SortExpr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (t : Lean.Expr) (args : Array Lean.Expr) : Optimize.TranslateEnvT Unit

partial def Blaster.Smt.defineInstPredicateQualifier.generatePredicates (typeTranslator : Lean.Expr → Optimize.TranslateEnvT SortExpr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (indName : Lean.Name) (us : List Lean.Level) (decl : Optimize.IndTypeDeclaration) (args : Array Lean.Expr) (mutualRec : Bool := false) : Optimize.TranslateEnvT Unit

def Blaster.Smt.defineInstPredicateQualifier.substitutePred (sub : Lean.Expr × Lean.Expr) (e : Lean.Expr) : Option Lean.Expr

Equations

• Blaster.Smt.defineInstPredicateQualifier.substitutePred sub e = if (sub.fst == e) = true then some sub.snd else none

def Blaster.Smt.defineInstPredicateQualifier.updatePredTerm (prevTerm newTerm : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.defineInstPredicateQualifier.updatePredTerm prevTerm newTerm = if Blaster.Smt.isTrueSmt prevTerm = true then newTerm else Blaster.Smt.andSmt prevTerm newTerm

def Blaster.Smt.defineInstPredicateQualifier.updateIteTerm (recRule : Lean.RecursorRule) (prevTerm predTerm : SmtTerm) : SmtTerm

Equations

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

partial def Blaster.Smt.defineInstPredicateQualifier.getPredicateQualifierName (typeTranslator : Lean.Expr → Optimize.TranslateEnvT SortExpr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (t : Lean.Expr) (currDecl : Optimize.IndTypeDeclaration) : Optimize.TranslateEnvT SmtSymbol

partial def Blaster.Smt.defineInstPredicateQualifier.generatePredicateAssertions (typeTranslator : Lean.Expr → Optimize.TranslateEnvT SortExpr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (indName : Lean.Name) (us : List Lean.Level) (declInd : Optimize.IndTypeDeclaration) (recVal : Lean.RecursorVal) (recRule : Lean.RecursorRule) (args : Array Lean.Expr) (funBody : SmtTerm) : Optimize.TranslateEnvT SmtTerm

def Blaster.Smt.translateNonOpaqueType (t : Lean.Expr) (args : Array Lean.Expr) (typeTranslator : Lean.Expr → TypeOptions → Optimize.TranslateEnvT SortExpr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (topts : TypeOptions) : Optimize.TranslateEnvT SortExpr

TODO: UPDATE SPEC.

Equations

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

def Blaster.Smt.translateNonOpaqueType.translateInstType (t : Lean.Expr) (args : Array Lean.Expr) (typeTranslator : Lean.Expr → TypeOptions → Optimize.TranslateEnvT SortExpr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (topts : TypeOptions) (indName : Lean.Name) : Optimize.TranslateEnvT SortExpr

Equations

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

def Blaster.Smt.translateSmtEquivType (n : Lean.Expr) (s : SmtSymbol) (t : SortExpr) : Optimize.TranslateEnvT SortExpr

Given n a name expression for which a corresponding smt sort exists (e.g., Bool, Int, String), s its corresponding Smt symbol and t its corresponding Smt sort, perform the following actions:

• When entry n := s exists in indTypeInstCache
  • return t
• Otherwise:
  • add entry n := s in indTypeInstCache
  • define smt predicate (define-fun @is{s} ((@x s)) Bool true)
  • return t

Equations

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

def Blaster.Smt.translateNatType (n : Lean.Expr) : Optimize.TranslateEnvT SortExpr

Perform the following actions:

• When entry n := "Nat" exists in indTypeInstCache return #[natSort]
• Otherwise:
  • add entry n := {@isNat, natSort} in indTypeInstCache
  • define smt sort (define-sort Nat () Int)
  • define smt predicate (define-fun @isNat ((@x Nat)) Bool (<= 0 @x))
  • return natSort Assume that n := Expr.const ``Nat [].

Equations

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

def Blaster.Smt.translateEmptyType (n : Lean.Expr) : Optimize.TranslateEnvT SortExpr

Perform the following actions:

• When entry n := "Empty" exists in indTypeInstCache
  • return emptySort
• Otherwise:
  • add entry n := "Empty" in indTypeInstCache
  • add entry n := {@isEmpty, emptySort} in indTypeInstCache`
  • declare smt sort (declare-sort Empty 0)
  • define smt predicate (define-fun @isEmpty (@x (Empty)) Bool false)
  • return emptySort Assume that n := Expr.const ``Empty [].

Equations

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

def Blaster.Smt.translatePEmptyType (n : Lean.Expr) : Optimize.TranslateEnvT SortExpr

Perform the following actions:

• When entry n := "PEmpty" exists in indTypeInstCache
  • return pemptySort
• Otherwise:
  • add entry n := {@isPEmpty, pemptySort} in indTypeInstCache
  • declare smt sort (declare-sort PEmpty 0)
  • define smt predicate (define-fun @isPEmpty ((PEmpty)) Bool false)
  • return pemptySort Assume that n := Expr.const ``PEmpty [..].

Equations

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

def Blaster.Smt.translateOpaqueType (e : Lean.Expr) : Optimize.TranslateEnvT (Option SortExpr)

Translate opaque sorts to their Smt counterpart. An error is triggered when e does not correspond to a name expression. TODO: update function when opacifying other Lean inductive types (e.g., BitVector, Char, etc).

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateOpaqueType (Lean.Expr.const `Bool us) = do let a ← Blaster.Smt.translateSmtEquivType (Lean.Expr.const `Bool us) Blaster.Smt.boolSymbol Blaster.Smt.boolSort pure (some a)
• Blaster.Smt.translateOpaqueType (Lean.Expr.const `Empty us) = do let a ← Blaster.Smt.translateEmptyType (Lean.Expr.const `Empty us) pure (some a)
• Blaster.Smt.translateOpaqueType (Lean.Expr.const `Int us) = do let a ← Blaster.Smt.translateSmtEquivType (Lean.Expr.const `Int us) Blaster.Smt.intSymbol Blaster.Smt.intSort pure (some a)
• Blaster.Smt.translateOpaqueType (Lean.Expr.const `Nat us) = do let a ← Blaster.Smt.translateNatType (Lean.Expr.const `Nat us) pure (some a)
• Blaster.Smt.translateOpaqueType (Lean.Expr.const `PEmpty us) = do let a ← Blaster.Smt.translatePEmptyType (Lean.Expr.const `PEmpty us) pure (some a)
• Blaster.Smt.translateOpaqueType (Lean.Expr.const n us) = pure none
• Blaster.Smt.translateOpaqueType e = Blaster.Optimize.throwEnvError (Lean.toMessageData "translateOpaqueType: name expression expected but got " ++ Lean.toMessageData (reprStr e))

partial def Blaster.Smt.translateTypeAux (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (t : Lean.Expr) (topts : TypeOptions := default) : Optimize.TranslateEnvT SortExpr

TODO: UPDATE SPEC

partial def Blaster.Smt.translateTypeAux.translateArrowType (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (e : Lean.Expr) (opts : TypeOptions) : Optimize.TranslateEnvT SortExpr

def Blaster.Smt.translateType (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (t : Lean.Expr) (topts : TypeOptions := default) : Optimize.TranslateEnvT SortExpr

TODO: UPDATE SPEC

Equations

• Blaster.Smt.translateType termTranslator t topts = do let __do_lift ← Blaster.Smt.removeTypeAbbrev t Blaster.Smt.translateTypeAux termTranslator __do_lift topts

structure Blaster.Smt.QuantifierEnv : Type

• quantifiers : SortedVars
• premises : Array SmtTerm
• topLevel : Bool

def Blaster.Smt.instInhabitedQuantifierEnv.default : QuantifierEnv

Equations

• Blaster.Smt.instInhabitedQuantifierEnv.default = { quantifiers := default, premises := default, topLevel := default }

instance Blaster.Smt.instInhabitedQuantifierEnv : Inhabited QuantifierEnv

Equations

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

@[reducible, inline]

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

Equations

• Blaster.Smt.QuantifierEnvT = StateRefT' IO.RealWorld Blaster.Smt.QuantifierEnv Blaster.Optimize.TranslateEnvT

def Blaster.Smt.initialQuantifierEnv (topLevel : Bool) : QuantifierEnv

Equations

• Blaster.Smt.initialQuantifierEnv topLevel = { quantifiers := #[], premises := #[], topLevel := topLevel }

def Blaster.Smt.translateQuantifier (n t : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) : QuantifierEnvT Unit

Translate a quantifier (n : t) by performing the following actions:

• Add n to the quantified fvars cache.
• When isType t, e.g., (α : Type or α : Sort u)
  • Call defineSortAndCache n to declare an Smt sort and return quantified array qts unchanged
• When ¬ isType t:
  • translate n to an Smt symbol s
  • translate t to a Smt type st
  • When toplevel flag is set:
    • Call declareConst s st to declare a free Smt scalar variable when st := α (i.e., scalar type).
    • Call declareFun s #[α₁ ... αₙ] β to declare an uninterpreted Smt function when st := α₁ → ... → αₙ → β.
  • When toplevel flag is not set:
    • Add (s : st) to quantifier array qts when st := α (i.e., scalar type)
    • Add (s : Array α₁ ... αₙ β) to quantifier array qts when st := α₁ → ... → αₙ → β.

Assume that t is not a proposition (i.e., !(← isPropEnv t)) nor a class constraint. An error is triggered if n is not an fvar expression.

TODO: UPDATE SPEC

Equations

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

def Blaster.Smt.translateQuantifier.updatePredicateQualifiers (t : Lean.Expr) (smtSym : SmtSymbol) : QuantifierEnvT Unit

Equations

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

def Blaster.Smt.translateQuantifier.updateQuantifiers (smtSym : SmtSymbol) (smtType : SortExpr) : QuantifierEnvT Unit

Equations

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

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

TODO: UPDATE SPEC

Equations

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

def Blaster.Smt.translateForAll.genForAllTerm (fbody : SmtTerm) : QuantifierEnvT SmtTerm

Equations

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

def Blaster.Smt.translateForAll.updatePremises (p : SmtTerm) : QuantifierEnvT Unit

Equations

• Blaster.Smt.translateForAll.updatePremises p = modify fun (env : Blaster.Smt.QuantifierEnv) => { quantifiers := env.quantifiers, premises := env.premises.push p, topLevel := env.topLevel }

def Blaster.Smt.translateFreeVar (f : Lean.Expr) (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) : Optimize.TranslateEnvT SmtTerm

Translate free variable expression f := Expr.fvar v to an Smt term such that:

• When v ∈ (← get).smtEnv.quantifiedFVars:
  • return `fvarIdToSmtTerm v
• When v ∉ (← get).smtEnv.quantifiedFVars:
  • add v to the quantified fvars cache
  • Let t' ← removeTypeAbbrev (← inferTypeEnv f)
  • smtType ← translateType optimize termTranslator t'
  • smtSym ← fvarIdToSmtSymbol v
  • declare smt symbol at top level, i.e., (declare-const smtSym smtType)
  • pTerm ← createPredQualifierApp smtSym t'
  • assert pTerm at smt level, i.e., (assert pTerm)
  • return smtSimpleVarId smtSym An error is triggered when
  • f is not an fvar expression; or
  • f has a sort type

Equations

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