Lean Inductive types having an Smt counterpart

Create a reserve smt symbol for s

def Blaster.Smt.mkReservedSymbol (s : String) : SmtSymbol

Equations

• Blaster.Smt.mkReservedSymbol s = Blaster.Smt.SmtSymbol.ReservedSymbol s

Create a normal smt symbol for s

def Blaster.Smt.mkNormalSymbol (s : String) : SmtSymbol

Equations

• Blaster.Smt.mkNormalSymbol s = Blaster.Smt.SmtSymbol.NormalSymbol s

Builtin Smt sort names.

Smt Int symbol.

def Blaster.Smt.intSymbol : SmtSymbol

Equations

• Blaster.Smt.intSymbol = Blaster.Smt.mkReservedSymbol "Int"

Smt Bool symbol.

def Blaster.Smt.boolSymbol : SmtSymbol

Equations

• Blaster.Smt.boolSymbol = Blaster.Smt.mkReservedSymbol "Bool"

Smt Prop symbol.

def Blaster.Smt.propSymbol : SmtSymbol

Equations

• Blaster.Smt.propSymbol = Blaster.Smt.mkReservedSymbol "Prop"

Smt String symbol.

def Blaster.Smt.stringSymbol : SmtSymbol

Equations

• Blaster.Smt.stringSymbol = Blaster.Smt.mkReservedSymbol "String"

Smt Nat symbol.

def Blaster.Smt.natSymbol : SmtSymbol

Equations

• Blaster.Smt.natSymbol = Blaster.Smt.mkReservedSymbol "Nat"

Smt Empty symbol.

def Blaster.Smt.emptySymbol : SmtSymbol

Equations

• Blaster.Smt.emptySymbol = Blaster.Smt.mkReservedSymbol "Empty"

Smt PEmpty symbol.

def Blaster.Smt.pemptySymbol : SmtSymbol

Equations

• Blaster.Smt.pemptySymbol = Blaster.Smt.mkReservedSymbol "PEmpty"

Smt universal type symbol.

def Blaster.Smt.typeSymbol : SmtSymbol

Equations

• Blaster.Smt.typeSymbol = Blaster.Smt.mkReservedSymbol "@@Type"

Builtin Smt sorts.

Smt Int Sort.

def Blaster.Smt.intSort : SortExpr

Equations

• Blaster.Smt.intSort = Blaster.Smt.SortExpr.SymbolSort Blaster.Smt.intSymbol

Smt Bool Sort.

def Blaster.Smt.boolSort : SortExpr

Equations

• Blaster.Smt.boolSort = Blaster.Smt.SortExpr.SymbolSort Blaster.Smt.boolSymbol

Smt Prop Sort. NOTE: This sort is defined during translation whenever required. (see function definePropSort)

def Blaster.Smt.propSort : SortExpr

Equations

• Blaster.Smt.propSort = Blaster.Smt.SortExpr.SymbolSort Blaster.Smt.propSymbol

Smt String Sort.

def Blaster.Smt.stringSort : SortExpr

Equations

• Blaster.Smt.stringSort = Blaster.Smt.SortExpr.SymbolSort Blaster.Smt.stringSymbol

Smt Param Sort instance.

@[inline]

def Blaster.Smt.paramSort (s : SmtSymbol) (args : Array SortExpr) : SortExpr

Equations

• Blaster.Smt.paramSort s args = Blaster.Smt.SortExpr.ParamSort s args

Smt Array Sort

def Blaster.Smt.arraySort (args : Array SortExpr) : SortExpr

Equations

• Blaster.Smt.arraySort args = Blaster.Smt.paramSort (Blaster.Smt.mkReservedSymbol "Array") args

Smt Nat Sort. NOTE: This sort is defined during translation whenever required. (see function defineNatSort)

def Blaster.Smt.natSort : SortExpr

Equations

• Blaster.Smt.natSort = Blaster.Smt.SortExpr.SymbolSort Blaster.Smt.natSymbol

Smt Empty Sort. NOTE: This sort is declared during translation whenever required. (see function defineEmptySort)

def Blaster.Smt.emptySort : SortExpr

Equations

• Blaster.Smt.emptySort = Blaster.Smt.SortExpr.SymbolSort Blaster.Smt.emptySymbol

Smt PEmpty Sort. NOTE: This sort is declared during translation whenever required. (see function definePEmptySort)

def Blaster.Smt.pemptySort : SortExpr

Equations

• Blaster.Smt.pemptySort = Blaster.Smt.SortExpr.SymbolSort Blaster.Smt.pemptySymbol

Smt @@Type Sort used to denote universal sort NOTE: This sort is declared during translation whenever required. (see function defineTypeSort).

def Blaster.Smt.typeSort : SortExpr

Equations

• Blaster.Smt.typeSort = Blaster.Smt.SortExpr.SymbolSort Blaster.Smt.typeSymbol

Builtin Smt symbols.

equality Smt symbol.

def Blaster.Smt.eqSymbol : SmtSymbol

Equations

• Blaster.Smt.eqSymbol = Blaster.Smt.mkReservedSymbol "="

Boolean not Smt symbol

def Blaster.Smt.notSymbol : SmtSymbol

Equations

• Blaster.Smt.notSymbol = Blaster.Smt.mkReservedSymbol "not"

Boolean and Smt symbol.

def Blaster.Smt.andSymbol : SmtSymbol

Equations

• Blaster.Smt.andSymbol = Blaster.Smt.mkReservedSymbol "and"

Boolean or Smt symbol.

def Blaster.Smt.orSymbol : SmtSymbol

Equations

• Blaster.Smt.orSymbol = Blaster.Smt.mkReservedSymbol "or"

Implies Smt symbol.

def Blaster.Smt.impSymbol : SmtSymbol

Equations

• Blaster.Smt.impSymbol = Blaster.Smt.mkReservedSymbol "=>"

Integer addition Smt symbol.

def Blaster.Smt.addSymbol : SmtSymbol

Equations

• Blaster.Smt.addSymbol = Blaster.Smt.mkReservedSymbol "+"

Integer subtraction Smt symbol.

def Blaster.Smt.subSymbol : SmtSymbol

Equations

• Blaster.Smt.subSymbol = Blaster.Smt.mkReservedSymbol "-"

Integer multiplication Smt symbol.

def Blaster.Smt.mulSymbol : SmtSymbol

Equations

• Blaster.Smt.mulSymbol = Blaster.Smt.mkReservedSymbol "*"

Integer native Smt division symbol.

def Blaster.Smt.divSymbol : SmtSymbol

Equations

• Blaster.Smt.divSymbol = Blaster.Smt.mkReservedSymbol "div"

Integer native Smt modulo symbol.

def Blaster.Smt.modSymbol : SmtSymbol

Equations

• Blaster.Smt.modSymbol = Blaster.Smt.mkReservedSymbol "mod"

Integer Euclidean division Smt symbol. NOTE: This function is defined during translation whenever required.

def Blaster.Smt.edivSymbol : SmtSymbol

Equations

• Blaster.Smt.edivSymbol = Blaster.Smt.mkReservedSymbol "@Int.ediv"

Integer Euclidean modulo Smt symbol. NOTE: This function is defined during translation whenever required.

def Blaster.Smt.emodSymbol : SmtSymbol

Equations

• Blaster.Smt.emodSymbol = Blaster.Smt.mkReservedSymbol "@Int.emod"

Integer truncate division Smt symbol. NOTE: This function is defined during translation whenever required.

def Blaster.Smt.tdivSymbol : SmtSymbol

Equations

• Blaster.Smt.tdivSymbol = Blaster.Smt.mkReservedSymbol "@Int.tdiv"

Integer truncate modulo Smt symbol. NOTE: This function is defined during translation whenever required.

def Blaster.Smt.tmodSymbol : SmtSymbol

Equations

• Blaster.Smt.tmodSymbol = Blaster.Smt.mkReservedSymbol "@Int.tmod"

Integer floor division Smt symbol. NOTE: This function is defined during translation whenever required.

def Blaster.Smt.fdivSymbol : SmtSymbol

Equations

• Blaster.Smt.fdivSymbol = Blaster.Smt.mkReservedSymbol "@Int.fdiv"

Integer floor modulo Smt symbol. NOTE: This function is defined during translation whenever required.

def Blaster.Smt.fmodSymbol : SmtSymbol

Equations

• Blaster.Smt.fmodSymbol = Blaster.Smt.mkReservedSymbol "@Int.fmod"

Integer to Nat Smt symbol. NOTE: This function is defined during translation whenever required.

def Blaster.Smt.toNatSymbol : SmtSymbol

Equations

• Blaster.Smt.toNatSymbol = Blaster.Smt.mkReservedSymbol "@Int.toNat"

Integer cast Smt symbol. NOTE: Only available in z3. This cast function is mainly used as a wrapper around power to to only handle positive exponentiation. Indeed, negative exponentiation can lead to a Real representation, which cannot be the case for Lean4 pow for both Int and Nat.

def Blaster.Smt.toIntSymbol : SmtSymbol

Equations

• Blaster.Smt.toIntSymbol = Blaster.Smt.mkReservedSymbol "to_int"

Native integer power Smt symbol.

def Blaster.Smt.powSymbol : SmtSymbol

Equations

• Blaster.Smt.powSymbol = Blaster.Smt.mkReservedSymbol "^"

Integer power Smt symbol. NOTE: This function is defined during translation whenever required.

def Blaster.Smt.intPowSymbol : SmtSymbol

Equations

• Blaster.Smt.intPowSymbol = Blaster.Smt.mkReservedSymbol "@Int.pow"

Nat power Smt symbol. NOTE: This function is defined during translation whenever required.

def Blaster.Smt.natPowSymbol : SmtSymbol

Equations

• Blaster.Smt.natPowSymbol = Blaster.Smt.mkReservedSymbol "@Nat.pow"

Nat subtraction Smt symbol. NOTE: This function is defined during translation whenever required.

def Blaster.Smt.natSubSymbol : SmtSymbol

Equations

• Blaster.Smt.natSubSymbol = Blaster.Smt.mkReservedSymbol "@Nat.sub"

Integer absolute Smt symbol.

def Blaster.Smt.absSymbol : SmtSymbol

Equations

• Blaster.Smt.absSymbol = Blaster.Smt.mkReservedSymbol "abs"

less than Smt symbol.

def Blaster.Smt.ltSymbol : SmtSymbol

Equations

• Blaster.Smt.ltSymbol = Blaster.Smt.mkReservedSymbol "<"

less than or equal to Smt symbol.

def Blaster.Smt.leqSymbol : SmtSymbol

Equations

• Blaster.Smt.leqSymbol = Blaster.Smt.mkReservedSymbol "<="

if-then-else Smt symbol.

def Blaster.Smt.iteSymbol : SmtSymbol

Equations

• Blaster.Smt.iteSymbol = Blaster.Smt.mkReservedSymbol "ite"

underscore Smt symbol.

def Blaster.Smt.underSymbol : SmtSymbol

Equations

• Blaster.Smt.underSymbol = Blaster.Smt.mkReservedSymbol "_"

select Smt symbol.

def Blaster.Smt.selectSymbol : SmtSymbol

Equations

• Blaster.Smt.selectSymbol = Blaster.Smt.mkReservedSymbol "select"

as-array Smt symbol.

def Blaster.Smt.asArraySymbol : SmtSymbol

Equations

• Blaster.Smt.asArraySymbol = Blaster.Smt.mkReservedSymbol "as-array"

less than Smt symbol for String.

def Blaster.Smt.strLtSymbol : SmtSymbol

Equations

• Blaster.Smt.strLtSymbol = Blaster.Smt.mkReservedSymbol "str.<"

less than or equal to Smt symbol for String.

def Blaster.Smt.strLeqSymbol : SmtSymbol

Equations

• Blaster.Smt.strLeqSymbol = Blaster.Smt.mkReservedSymbol "str.<="

append Smt symbol for String.

def Blaster.Smt.strAppendSymbol : SmtSymbol

Equations

• Blaster.Smt.strAppendSymbol = Blaster.Smt.mkReservedSymbol "str.++"

replace Smt symbol for String. NOTE: Unlike the replace Lean4 function, this function only replaces the first occurrence of src by dst in s. The equivalent function for Lean4 is str.replace_all

def Blaster.Smt.strReplaceSymbol : SmtSymbol

Equations

• Blaster.Smt.strReplaceSymbol = Blaster.Smt.mkReservedSymbol "str.replace"

replace all Smt symbol for String.

def Blaster.Smt.strReplaceAllSymbol : SmtSymbol

Equations

• Blaster.Smt.strReplaceAllSymbol = Blaster.Smt.mkReservedSymbol "str.replace_all"

length Smt symbol for String.

def Blaster.Smt.strLengthSymbol : SmtSymbol

Equations

• Blaster.Smt.strLengthSymbol = Blaster.Smt.mkReservedSymbol "str.len"

Builtin Smt functions.

Create an Smt application term with function name nm and parameters args.

def Blaster.Smt.mkSmtAppN (nm : SmtQualifiedIdent) (args : Array SmtTerm) : SmtTerm

Equations

• Blaster.Smt.mkSmtAppN nm args = Blaster.Smt.SmtTerm.AppTerm nm args

Same as mkSmtAppN but accepts an Smt symbol as function name.

def Blaster.Smt.mkSimpleSmtAppN (nm : SmtSymbol) (args : Array SmtTerm) : SmtTerm

Equations

• Blaster.Smt.mkSimpleSmtAppN nm args = Blaster.Smt.mkSmtAppN (Blaster.Smt.SmtQualifiedIdent.SimpleIdent nm) args

Create an Equality Smt application

def Blaster.Smt.eqSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.eqSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.eqSymbol #[op1, op2]

Create an Boolean not Smt application

def Blaster.Smt.notSmt (op : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.notSmt op = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.notSymbol #[op]

Create an Boolean and Smt application

def Blaster.Smt.andSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.andSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.andSymbol #[op1, op2]

Create an Boolean or Smt application

def Blaster.Smt.orSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.orSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.orSymbol #[op1, op2]

Create an Implies Smt application

def Blaster.Smt.impliesSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.impliesSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.impSymbol #[op1, op2]

Create an Integer addtion Smt application

def Blaster.Smt.addSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.addSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.addSymbol #[op1, op2]

Create an Integer subtraction Smt application

def Blaster.Smt.subSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.subSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.subSymbol #[op1, op2]

Create an Integer multiplication Smt application

def Blaster.Smt.mulSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.mulSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.mulSymbol #[op1, op2]

Create an Integer native division Smt application

def Blaster.Smt.divSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.divSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.divSymbol #[op1, op2]

Create an Integer native modulo Smt application

def Blaster.Smt.modSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.modSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.modSymbol #[op1, op2]

Create an Integer negation Smt application

def Blaster.Smt.negSmt (op : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.negSmt op = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.subSymbol #[op]

Create an Integer Euclidean division Smt application.

def Blaster.Smt.edivSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.edivSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.edivSymbol #[op1, op2]

Create an Integer Euclidean modulo Smt application.

def Blaster.Smt.emodSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.emodSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.emodSymbol #[op1, op2]

Create an Integer truncate division Smt application.

def Blaster.Smt.tdivSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.tdivSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.tdivSymbol #[op1, op2]

Create an Integer truncate modulo Smt application.

def Blaster.Smt.tmodSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.tmodSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.tmodSymbol #[op1, op2]

Create an Integer floor division Smt application.

def Blaster.Smt.fdivSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.fdivSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.fdivSymbol #[op1, op2]

Create an Integer floor modulo Smt application.

def Blaster.Smt.fmodSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.fmodSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.fmodSymbol #[op1, op2]

Create an Integer to Nat Smt conversion.

def Blaster.Smt.toNatSmt (op : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.toNatSmt op = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.toNatSymbol #[op]

Create a native Integer power Smt application.

def Blaster.Smt.powSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.powSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.toIntSymbol #[Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.powSymbol #[op1, op2]]

Create an Integer power Smt application.

def Blaster.Smt.intPowSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.intPowSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.intPowSymbol #[op1, op2]

Create a Nat subtraction Smt application

def Blaster.Smt.natSubSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.natSubSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.natSubSymbol #[op1, op2]

Create a Nat division Smt application. NOTE: This is an alias to Int.ediv at Smt level.

def Blaster.Smt.natDivSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.natDivSmt op1 op2 = Blaster.Smt.edivSmt op1 op2

Create a Nat modulo Smt application. NOTE: This is an alias to Int.emod at Smt level.

def Blaster.Smt.natModSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.natModSmt op1 op2 = Blaster.Smt.emodSmt op2 op1

Create an Nat power Smt application.

def Blaster.Smt.natPowSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.natPowSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.natPowSymbol #[op1, op2]

Create an Integer absolute Smt application.

def Blaster.Smt.absSmt (op : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.absSmt op = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.absSymbol #[op]

Create a less than Smt application.

def Blaster.Smt.ltSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.ltSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.ltSymbol #[op1, op2]

Create a less than or equal to Smt application.

def Blaster.Smt.leqSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.leqSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.leqSymbol #[op1, op2]

Create an if-then-else Smt application.

def Blaster.Smt.iteSmt (c t e : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.iteSmt c t e = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.iteSymbol #[c, t, e]

Create a String less than Smt application.

def Blaster.Smt.strLtSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.strLtSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.strLtSymbol #[op1, op2]

Create a String less than or equal to Smt application.

def Blaster.Smt.strLeqSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.strLeqSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.strLeqSymbol #[op1, op2]

Create a String append Smt application.

def Blaster.Smt.strAppendSmt (op1 op2 : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.strAppendSmt op1 op2 = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.strAppendSymbol #[op1, op2]

Create a String replace Smt application.

def Blaster.Smt.strReplaceSmt (s src dst : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.strReplaceSmt s src dst = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.strReplaceSymbol #[s, src, dst]

Create a String replace all Smt application.

def Blaster.Smt.strReplaceAllSmt (s src dst : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.strReplaceAllSmt s src dst = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.strReplaceAllSymbol #[s, src, dst]

Create a String length Smt application.

def Blaster.Smt.strLengthSmt (s : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.strLengthSmt s = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.strLengthSymbol #[s]

Create an as-array Smt application (i.e., converting a function to an array representation).

def Blaster.Smt.asArraySmt (f : SmtQualifiedIdent) : SmtTerm

Equations

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

Create a select Smt application (i.e., applying an fun array representation to its arguments).

def Blaster.Smt.selectSmt (f : SmtTerm) (args : Array SmtTerm) : SmtTerm

Equations

• Blaster.Smt.selectSmt f args = Blaster.Smt.mkSimpleSmtAppN Blaster.Smt.selectSymbol (#[f] ++ args)

Return true Smt term.

def Blaster.Smt.trueSmt : SmtTerm

Equations

• Blaster.Smt.trueSmt = Blaster.Smt.SmtTerm.BoolTerm true

Return false Smt term.

def Blaster.Smt.falseSmt : SmtTerm

Equations

• Blaster.Smt.falseSmt = Blaster.Smt.SmtTerm.BoolTerm false

Convert an Integer literal to an Smt representation.

def Blaster.Smt.intLitSmt (n : Int) : SmtTerm

Equations

• Blaster.Smt.intLitSmt (Int.ofNat n_2) = Blaster.Smt.SmtTerm.NumTerm n_2
• Blaster.Smt.intLitSmt (Int.negSucc n_2) = Blaster.Smt.negSmt (Blaster.Smt.SmtTerm.NumTerm (n_2.add 1))

Convert an Nat literal to an Smt representation.

def Blaster.Smt.natLitSmt (n : Nat) : SmtTerm

Equations

• Blaster.Smt.natLitSmt n = Blaster.Smt.SmtTerm.NumTerm n

Convert an String literal to an Smt representation.

def Blaster.Smt.strLitSmt (s : String) : SmtTerm

Equations

• Blaster.Smt.strLitSmt s = Blaster.Smt.SmtTerm.StrTerm (toString "\"" ++ toString s ++ toString "\"")

Create an Smt variable identifier.

def Blaster.Smt.smtSimpleVarId (nm : SmtSymbol) : SmtTerm

Equations

• Blaster.Smt.smtSimpleVarId nm = Blaster.Smt.SmtTerm.SmtIdent (Blaster.Smt.SmtQualifiedIdent.SimpleIdent nm)

Create an Smt qualified variable identifier.

def Blaster.Smt.smtQualifiedVarId (nm : SmtSymbol) (t : SortExpr) : SmtTerm

Equations

• Blaster.Smt.smtQualifiedVarId nm t = Blaster.Smt.SmtTerm.SmtIdent (Blaster.Smt.SmtQualifiedIdent.QualifiedIdent nm t)

Create an e-matching pattern to be used for a forall or an exists Smt term.

def Blaster.Smt.mkPattern (patterns : Array SmtTerm) : SmtAttribute

Equations

• Blaster.Smt.mkPattern patterns = Blaster.Smt.SmtAttribute.Pattern patterns

Create a debug annotation name for a forall/exists Smt term.

def Blaster.Smt.mkQid (s : SmtSymbol) : SmtAttribute

Equations

• Blaster.Smt.mkQid s = Blaster.Smt.SmtAttribute.Qid s

Annotate an Smt term with an optional list of attributes.

def Blaster.Smt.annotateTerm (t : SmtTerm) (opt : Option (Array SmtAttribute)) : SmtTerm

Equations

• Blaster.Smt.annotateTerm t none = t
• Blaster.Smt.annotateTerm t (some atts) = t.AnnotatedTerm atts

Associate an optional name nm to an Smt term.

def Blaster.Smt.nameTerm (t : SmtTerm) (nm : Option String) : SmtTerm

Equations

• Blaster.Smt.nameTerm t none = t
• Blaster.Smt.nameTerm t (some nmThm) = t.AnnotatedTerm #[Blaster.Smt.SmtAttribute.Named (Blaster.Smt.mkNormalSymbol nmThm)]

Create a forall Smt Term, with quantifiers vars and body b. An optional theorem name nmThm can be provided as well as specific patterns to facilitate e-matching and debugging during solving.

def Blaster.Smt.mkForallTerm (nmThm : Option String) (vars : SortedVars) (b : SmtTerm) (att : Option (Array SmtAttribute)) : SmtTerm

Equations

• Blaster.Smt.mkForallTerm nmThm vars b att = Blaster.Smt.nameTerm (Blaster.Smt.SmtTerm.ForallTerm vars (Blaster.Smt.annotateTerm b att)) nmThm

Create an existential Smt Term, with quantifiers vars and body b. An optional theorem name nmThm can be provided as well as specific patterns to facilitate e-matching and debugging during solving.

def Blaster.Smt.mkExistsTerm (nmThm : Option String) (vars : SortedVars) (b : SmtTerm) (att : Option (Array SmtAttribute)) : SmtTerm

Equations

• Blaster.Smt.mkExistsTerm nmThm vars b att = Blaster.Smt.nameTerm (Blaster.Smt.SmtTerm.ExistsTerm vars (Blaster.Smt.annotateTerm b att)) nmThm

Create a lambda Smt term with parameters args and body b.

def Blaster.Smt.mkLambdaTerm (args : SortedVars) (b : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.mkLambdaTerm args b = Blaster.Smt.SmtTerm.LambdaTerm args b

Create a let Smt term with bindings binds and body b.

def Blaster.Smt.mkLetTerm (binds : Array (SmtSymbol × SmtTerm)) (b : SmtTerm) : SmtTerm

Equations

• Blaster.Smt.mkLetTerm binds b = Blaster.Smt.SmtTerm.LetTerm binds b

Helper functions.

Append smt symbol nm with "_{s}".

def Blaster.Smt.appendSymbol (nm : SmtSymbol) (s : String) : SmtSymbol

Equations

• Blaster.Smt.appendSymbol (Blaster.Smt.SmtSymbol.ReservedSymbol str) s = Blaster.Smt.mkReservedSymbol (toString str ++ toString "_" ++ toString s)
• Blaster.Smt.appendSymbol (Blaster.Smt.SmtSymbol.NormalSymbol str) s = Blaster.Smt.mkNormalSymbol (toString str ++ toString "_" ++ toString s)

Return true when t := BoolTerm true. Otherwise false.

def Blaster.Smt.isTrueSmt (t : SmtTerm) : Bool

Equations

• Blaster.Smt.isTrueSmt (Blaster.Smt.SmtTerm.BoolTerm b) = b
• Blaster.Smt.isTrueSmt t = false

Return true when t := AppTerm idt args. Otherwise false.

def Blaster.Smt.isAppTerm (t : SmtTerm) : Bool

Equations

• Blaster.Smt.isAppTerm (Blaster.Smt.SmtTerm.AppTerm nm args) = true
• Blaster.Smt.isAppTerm t = false

Determine if t is an equality Smt expression and return it's corresponding arguments. Otherwise return none.

def Blaster.Smt.eqSmt? (t : SmtTerm) : Option (SmtTerm × SmtTerm)

Equations

• Blaster.Smt.eqSmt? (Blaster.Smt.SmtTerm.AppTerm (Blaster.Smt.SmtQualifiedIdent.SimpleIdent sym) args) = if (sym == Blaster.Smt.eqSymbol) = true then some (args[0]!, args[1]!) else none
• Blaster.Smt.eqSmt? t = none

Determine if t is a not Smt expression and return its corresponding argument. Otherwise return none.

def Blaster.Smt.notSmt? (t : SmtTerm) : Option SmtTerm

Equations

• Blaster.Smt.notSmt? (Blaster.Smt.SmtTerm.AppTerm (Blaster.Smt.SmtQualifiedIdent.SimpleIdent sym) args) = if (sym == Blaster.Smt.notSymbol) = true then some args[0]! else none
• Blaster.Smt.notSmt? t = none

Return true when t corresponds to ParamSort with name nm. Otherwise false.

def Blaster.Smt.isParamSort (t : SortExpr) (sName : SmtSymbol) : Bool

Equations

• Blaster.Smt.isParamSort (Blaster.Smt.SortExpr.ParamSort nm ps) sName = (nm == sName)
• Blaster.Smt.isParamSort (Blaster.Smt.SortExpr.SymbolSort nm) sName = false

Return the smt symbol associated to the given Smt qualified identifier.

def Blaster.Smt.getSymbol : SmtQualifiedIdent → SmtSymbol

Equations

• Blaster.Smt.getSymbol (Blaster.Smt.SmtQualifiedIdent.SimpleIdent nm) = nm
• Blaster.Smt.getSymbol (Blaster.Smt.SmtQualifiedIdent.QualifiedIdent nm t) = nm