instance Auto.SMT.instInhabitedLamAtomic : Inhabited Auto.SMT.LamAtomic✝

Equations

• Auto.SMT.instInhabitedLamAtomic = { default := Auto.SMT.LamAtomic.sort✝ default }

instance Auto.SMT.instHashableLamAtomic : Hashable Auto.SMT.LamAtomic✝

Equations

• Auto.SMT.instHashableLamAtomic = { hash := Auto.SMT.hashLamAtomic✝ }

instance Auto.SMT.instBEqLamAtomic : BEq Auto.SMT.LamAtomic✝

Equations

• Auto.SMT.instBEqLamAtomic = { beq := Auto.SMT.beqLamAtomic✝ }

instance Auto.SMT.instToStringLamAtomic : ToString Auto.SMT.LamAtomic✝

Equations

• Auto.SMT.instToStringLamAtomic = { toString := Auto.SMT.LamAtomic.toString✝ }

instance Auto.SMT.instOrdLamAtomic : Ord Auto.SMT.LamAtomic✝

Equations

• Auto.SMT.instOrdLamAtomic = { compare := fun (x y : Auto.SMT.LamAtomic✝) => compare (toString "" ++ toString x ++ toString "") (toString "" ++ toString y ++ toString "") }

@[reducible, inline]

abbrev Auto.SMT.SelectorInfo : Type

selectorInfo contains:

• The name of the selector
• Whether the selector is a projection
• The constructor that the selector is for
• The index of the argument that it is selecting
• The name of the SMT datatype that the selector is for (i.e. the name of the input type)
• The LamSort of the SMT datatype that the selector is for (i.e. the input type)
• The output type of the selector (full type is an arrow type that takes in a datatype and returns the output type)

Equations

• Auto.SMT.SelectorInfo = (String × Bool × Auto.SMT.LamAtomic✝ × Nat × String × Auto.Embedding.Lam.LamSort × Auto.Embedding.Lam.LamSort)

def Auto.SMT.LamAtomic.toLeanExpr (tyValMap varValMap etomValMap : Std.HashMap Nat Lean.Expr) (atomic : Auto.SMT.LamAtomic✝) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Auto.SMT.LamAtomic.toLeanExpr tyValMap varValMap etomValMap (Auto.SMT.LamAtomic.bvOfNat✝ a) = pure ((Lean.Expr.const `BitVec.ofNat []).app (Lean.Expr.lit (Lean.Literal.natVal a)))
• Auto.SMT.LamAtomic.toLeanExpr tyValMap varValMap etomValMap (Auto.SMT.LamAtomic.bvToNat✝ a) = pure ((Lean.Expr.const `BitVec.toNat []).app (Lean.Expr.lit (Lean.Literal.natVal a)))
• Auto.SMT.LamAtomic.toLeanExpr tyValMap varValMap etomValMap (Auto.SMT.LamAtomic.compCtor✝ a) = do let e ← Auto.Lam2D.interpLamTermAsUnlifted tyValMap varValMap etomValMap 0 a pure e
• Auto.SMT.LamAtomic.toLeanExpr tyValMap varValMap etomValMap (Auto.SMT.LamAtomic.compProj✝ a) = do let e ← Auto.Lam2D.interpLamTermAsUnlifted tyValMap varValMap etomValMap 0 a pure e

structure Auto.SMT.SMTNamingInfo : Type

• tyVal : Array (Lean.Expr × Lean.Level)
• varVal : Array (Lean.Expr × Embedding.Lam.LamSort)
• lamEVarTy : Array Embedding.Lam.LamSort

def Auto.SMT.SMTNamingInfo.exprToSuggestion (e : Lean.Expr) : Lean.MetaM String

Equations

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

def Auto.SMT.SMTNamingInfo.suggestNameForSort (sni : SMTNamingInfo) (s : Embedding.Lam.LamSort) : Lean.MetaM String

Equations

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

def Auto.SMT.SMTNamingInfo.suggestNameForSort.go (sni : SMTNamingInfo) : Embedding.Lam.LamSort → Lean.MetaM String

Equations

• One or more equations did not get rendered due to their size.
• Auto.SMT.SMTNamingInfo.suggestNameForSort.go sni (Auto.Embedding.Lam.LamSort.base b) = pure b.toString
• Auto.SMT.SMTNamingInfo.suggestNameForSort.go sni (a.func argTy) = Auto.SMT.SMTNamingInfo.suggestNameForSort.go sni argTy

def Auto.SMT.SMTNamingInfo.suggestNameForAtomic (sni : SMTNamingInfo) (a : Auto.SMT.LamAtomic✝) : Lean.MetaM String

Equations

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

def Auto.SMT.SMTNamingInfo.suggestNameForAtomic.go (sni : SMTNamingInfo) : Auto.SMT.LamAtomic✝ → Lean.MetaM String

Equations

• One or more equations did not get rendered due to their size.
• Auto.SMT.SMTNamingInfo.suggestNameForAtomic.go sni (Auto.SMT.LamAtomic.etom✝ a) = pure (toString "sk" ++ toString a ++ toString "")
• Auto.SMT.SMTNamingInfo.suggestNameForAtomic.go sni (Auto.SMT.LamAtomic.compCtor✝ a) = pure "cC"
• Auto.SMT.SMTNamingInfo.suggestNameForAtomic.go sni (Auto.SMT.LamAtomic.compProj✝ a) = pure "cP"

def Auto.SMT.lamTermAtom2String (sni : SMTNamingInfo) (lamVarTy : Array Embedding.Lam.LamSort) (n : Nat) : IR.SMT.TransM Auto.SMT.LamAtomic✝ Embedding.Lam.LamSort (Embedding.Lam.LamSort × String)

Equations

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

def Auto.SMT.lamTermEtom2String (sni : SMTNamingInfo) (lamEVarTy : Array Embedding.Lam.LamSort) (n : Nat) : IR.SMT.TransM Auto.SMT.LamAtomic✝ Embedding.Lam.LamSort (Embedding.Lam.LamSort × String)

Equations

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

def Auto.SMT.lamQuantified2STerm (sni : SMTNamingInfo) (forall? : Bool) (s : Embedding.Lam.LamSort) (body : IR.SMT.TransM Auto.SMT.LamAtomic✝ Embedding.Lam.LamSort IR.SMT.STerm) : IR.SMT.TransM Auto.SMT.LamAtomic✝ Embedding.Lam.LamSort IR.SMT.STerm

Equations

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

def Auto.SMT.sortAuxDecls : Array IR.SMT.Command

Equations

• Auto.SMT.sortAuxDecls = #[Auto.IR.SMT.Command.declSort "Empty" 0]

def Auto.SMT.termAuxDecls : Array IR.SMT.Command

Equations

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

def Auto.SMT.withExprValuation {α : Type} [Inhabited α] (sni : SMTNamingInfo) (h2lMap : Std.HashMap Auto.SMT.LamAtomic✝ String) (printFn : Std.HashMap Nat Lean.Expr → Std.HashMap Nat Lean.Expr → Std.HashMap Nat Lean.Expr → Lean.MetaM α) : Lean.MetaM α

printFn : (tyValMap : _) → (varValMap : _) → (etomValMap : _) → MetaM α

Equations

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

def Auto.lamFOL2SMT (sni : SMT.SMTNamingInfo) (lamVarTy lamEVarTy : Array Embedding.Lam.LamSort) (facts : Array Embedding.Lam.LamTerm) (minds : Array Embedding.Lam.MutualIndInfo) : IR.SMT.TransM Auto.SMT.LamAtomic✝ Embedding.Lam.LamSort (Array IR.SMT.Command × Array IR.SMT.STerm)

facts should not contain import versions of eq, ∀ or ∃ valid_fact_{i} corresponds to the i-th entry in facts

Equations

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

def Auto.lamFOL2SMTWithExtraInfo (sni : SMT.SMTNamingInfo) (lamVarTy lamEVarTy : Array Embedding.Lam.LamSort) (facts : Array Embedding.Lam.LamTerm) (minds : Array Embedding.Lam.MutualIndInfo) : IR.SMT.TransM Auto.SMT.LamAtomic✝ Embedding.Lam.LamSort (Array IR.SMT.Command × Array IR.SMT.STerm × Std.HashMap String Auto.SMT.LamAtomic✝ × Std.HashMap String Embedding.Lam.LamSort × Array SMT.SelectorInfo)

Identical to lamFOL2SMT but it also outputs Auto.IR.SMT.State.l2hMap, Auto.IR.SMT.getWfPredicatesInvMap, and selector information

Equations

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