def Blaster.Optimize.opaqueFuns : Lean.NameHashSet

list of operators that must not be unfolded, i.e., they will directly be translated to their corresponding SMT counterpart.

Equations

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

def Blaster.Optimize.relationalCompatibleTypes : Lean.NameHashSet

list of types for which: - LT instance is guaranteed to be irrelexive, anti-symmetric and transitive. - LE instance is guaranteed to be reflexive, symmetric and transitive. TODO: add other basic lean types (e.g., Char, etc)

Equations

• Blaster.Optimize.relationalCompatibleTypes = List.foldr (fun (c : Lean.Name) (s : Lean.NameHashSet) => s.insert c) Std.HashSet.emptyWithCapacity [`Nat, `Int, `Bool, `String]

def Blaster.Optimize.isCompatibleRelationalType (e : Lean.Expr) : Bool

Return true is e corresponds to a sort in relationalCompatibletypes.

Equations

• Blaster.Optimize.isCompatibleRelationalType (Lean.Expr.const n us) = Blaster.Optimize.relationalCompatibleTypes.contains n
• Blaster.Optimize.isCompatibleRelationalType e = false