structure Blaster.Smt.MatchResult : Type

• discrTerms : Array SmtTerm

  Translated match discriminators

• iteTerm : Option SmtTerm

  Ite term generated when translating each match pattern

@[inline]

def Blaster.Smt.removeAndOptNamedPatternExpr (p : Lean.Expr) : Optimize.TranslateEnvT Lean.Expr

Equations

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

def Blaster.Smt.translateMatchAux? (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (idx : Nat) (discrs lhs : Array Lean.Expr) (alt _matchType : Lean.Expr) (acc : Option MatchResult) : Optimize.TranslateEnvT (Option MatchResult)

Is the accumulator rewriter function to be used with matchExprRewriter when translating a match expression to an smt if-then-else.

Equations

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

def Blaster.Smt.translateMatchAux?.insertFVars (h : Std.HashSet Lean.FVarId) (v : Lean.Expr) : Optimize.TranslateEnvT (Std.HashSet Lean.FVarId)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.translateMatchAux?.insertFVars h v = pure h

def Blaster.Smt.translateMatchAux?.mkRhs (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (discrTerms : Array SmtTerm) (lhs : Array Lean.Expr) (rhs : Lean.Expr) : Optimize.TranslateEnvT SmtTerm

Equations

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

def Blaster.Smt.translateMatchAux?.mkIte (termTranslator : Lean.Expr → Optimize.TranslateEnvT SmtTerm) (lhs : Array Lean.Expr) (rhs : Lean.Expr) (mres : MatchResult) : Optimize.TranslateEnvT (Option MatchResult)

Equations

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

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

Translate a match expression to an smt if-then-else term s.t.: match e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ ===> if (mkCond se₁ p₍₁₎₍₁₎) ∧ ... ∧ (mkCond seₙ p₍₁₎₍ₙ₎) then (mkRhs [se₁ ... seₙ] [p₍₁₎₍₁₎ ... p₍₁₎₍ₙ₎] t₁) else if (mkCond se₁ p₍₂₎₍₁₎) ∧ ... ∧ (mkCond seₙ p₍₂₎₍ₙ₎) then (mkRhs [se₁ ... seₙ] [p₍₂₎₍₁₎ ... p₍₂₎₍ₙ₎] t₂) ... else (mkRhs [se₁ ... seₙ] [p₍ₘ₎₍₁₎ ... p₍ₘ₎₍ₙ₎] tₘ)

with:

• ∀ i ∈ [1..n], seᵢ := termTranslator e

• mkCond se p : let p' ← removeAndOptNamedPatternExpr p; := ( = se sp ) if isIntNatStrCst(p') with sp := termTranslator p' := (<= N se ) if p' = N + n ∧ Type(N) = Nat := (<= 0 se ) if p' = Int.ofNat n := (<= N se ) if p' = Int.ofNat (N + n) := (<= se (- N)) if p' = Int.Neg (Int.ofNat (N + n)) := (is-C se) if p' = C (i.e., nullary constructor) := (and (is-C se) (and (mkCond (C.1 se) x₁) (... (and (mkCond (C.k-1 se) xₖ₋₁) (mkCond (C.k se) xₖ))))) if p' = C x₁ ... xₖ := True if p' = fv := ⊥ otherwise

• mkRhs [se₁ ... seₙ] [p₁ ... pₙ] t : let st := termTranslator t := (mkLet se₁ p₁ ( ... (mkLet seₙ₋₁ pₙ₋₁ (mkLet seₙ pₙ st))))

• mkLet se p t : := (let ((sfv se)) t) if p = fv with sfv = fvarIdToSmtSymbol fv := t if p = C (i.e., nullary constructor) := t if isIntNatStrCst(p)

  := (let ((sn se)) (mkLet sn' e t)) if p = namedPattern t n e h` with sn = fvarIdToSmtSymbol n ∧ sn' = smtSimpleVarId sn

  := (let ((sn (- se N))) t) if p = N + n ∧ Type(N) = Nat with sn = fvarIdToSmtSymbol n

  := (let ((sn (- se N))) (mkLet sn' e t)) if p = N + (namedPattern t n e h) ∧ Type(N) = Nat with sn = fvarIdToSmtSymbol n ∧ sn' = smtSimpleVarId sn := (let ((sn se)) t) if p = Int.ofNat n with sn = fvarIdToSmtSymbol n

  := (let ((sn se)) (mkLet sn' e t)) if p = Int.ofNat (namedPattern t n e t) with sn = fvarIdToSmtSymbol n ∧ sn' = smtSimpleVarId sn

  := (let ((sn (- se N))) t) if p = Int.ofNat (N + n) with sn = fvarIdToSmtSymbol n

  := (let ((sn (- se N))) (mkLet sn' e t)) if p = Int.ofNat (N + namedPattern t n e h) with sn = fvarIdToSmtSymbol n ∧ sn' = smtSimpleVarId sn

  := (let ((sn (- (+ se N)))) t) if p' = Int.Neg (Int.ofNat (N + n)) with sn = fvarIdToSmtSymbol n

  := (let ((sn (- (+ se N)))) (mkLet sn' e t)) if p' = Int.Neg (Int.ofNat (N + namedPattern t n e h)) with sn = fvarIdToSmtSymbol n ∧ sn' = smtSimpleVarId sn

  := (mkLet (C.1 se) x₁ (.. (mkLet (C.k-1 se) xₖ₋₁ (mkLet (C.k se) xₙ t)))) if p' = C x₁ ... xₖ

  := ⊥ otherwise

Note that we here expect the optimization phase must reach match expression whenever at least one eᵢ is a constant/ctor.

Equations

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