inductive Blaster.Smt.SmtSymbol : Type

Smt-Lib V2 Smt symbol.

• ReservedSymbol (str : String) : SmtSymbol

  To be used for reserve word (e.g., operator symbol)

• NormalSymbol (str : String) : SmtSymbol

  To be used for representing user defined symbol

instance Blaster.Smt.instInhabitedSmtSymbol : Inhabited SmtSymbol

Equations

• Blaster.Smt.instInhabitedSmtSymbol = { default := Blaster.Smt.SmtSymbol.NormalSymbol "" }

instance Blaster.Smt.instBEqSmtSymbol : BEq SmtSymbol

Equations

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

instance Blaster.Smt.instHashableSmtSymbol : Hashable SmtSymbol

Equations

• Blaster.Smt.instHashableSmtSymbol = { hash := Blaster.Smt.SmtSymbol.hash✝ }

inductive Blaster.Smt.SortExpr : Type

Smt-Lib V2 sort expression.

• SymbolSort (nm : SmtSymbol) : SortExpr
• ParamSort (nm : SmtSymbol) (ps : Array SortExpr) : SortExpr

instance Blaster.Smt.instInhabitedSortExpr : Inhabited SortExpr

Equations

• Blaster.Smt.instInhabitedSortExpr = { default := Blaster.Smt.SortExpr.SymbolSort default }

@[reducible, inline]

abbrev Blaster.Smt.SortedVars : Type

Equations

• Blaster.Smt.SortedVars = Array (Blaster.Smt.SmtSymbol × Blaster.Smt.SortExpr)

inductive Blaster.Smt.SmtQualifiedIdent : Type

Smt-Lib V2 qualified identifier.

• SimpleIdent (nm : SmtSymbol) : SmtQualifiedIdent
• QualifiedIdent (nm : SmtSymbol) (t : SortExpr) : SmtQualifiedIdent

instance Blaster.Smt.instInhabitedSmtQualifiedIdent : Inhabited SmtQualifiedIdent

Equations

• Blaster.Smt.instInhabitedSmtQualifiedIdent = { default := Blaster.Smt.SmtQualifiedIdent.SimpleIdent default }

def Blaster.Smt.isIteApp (nm : SmtQualifiedIdent) : Bool

Return true if smt qualified ident correspond to smt ite symbol

Equations

• Blaster.Smt.isIteApp (Blaster.Smt.SmtQualifiedIdent.SimpleIdent (Blaster.Smt.SmtSymbol.ReservedSymbol "ite")) = true
• Blaster.Smt.isIteApp nm = false

inductive Blaster.Smt.SmtAttribute : Type

Smt term annotation attributes.

• Named (n : SmtSymbol) : SmtAttribute
• Pattern (p : Array SmtTerm) : SmtAttribute
• Qid (n : SmtSymbol) : SmtAttribute

inductive Blaster.Smt.SmtTerm : Type

Smt-Lib V2 term.

• NumTerm (v : Nat) : SmtTerm
• DecTerm (v : String) : SmtTerm
• BoolTerm (b : Bool) : SmtTerm
• BinTerm (v : String) : SmtTerm
• HexTerm (v : String) : SmtTerm
• StrTerm (v : String) : SmtTerm
• SmtIdent (nm : SmtQualifiedIdent) : SmtTerm
• AppTerm (nm : SmtQualifiedIdent) (args : Array SmtTerm) : SmtTerm
• LetTerm (bs : Array (SmtSymbol × SmtTerm)) (body : SmtTerm) : SmtTerm
• ForallTerm (bs : SortedVars) (body : SmtTerm) : SmtTerm
• ExistsTerm (bs : SortedVars) (body : SmtTerm) : SmtTerm
• LambdaTerm (bs : SortedVars) (body : SmtTerm) : SmtTerm
• AnnotatedTerm (t : SmtTerm) (annot : Array SmtAttribute) : SmtTerm

instance Blaster.Smt.instInhabitedSmtAttribute : Inhabited SmtAttribute

Equations

• Blaster.Smt.instInhabitedSmtAttribute = { default := Blaster.Smt.SmtAttribute.Qid default }

instance Blaster.Smt.instInhabitedSmtTerm : Inhabited SmtTerm

Equations

• Blaster.Smt.instInhabitedSmtTerm = { default := Blaster.Smt.SmtTerm.NumTerm 0 }

@[reducible, inline]

abbrev Blaster.Smt.SmtSelector : Type

Equations

• Blaster.Smt.SmtSelector = (Blaster.Smt.SmtSymbol × Blaster.Smt.SortExpr)

@[reducible, inline]

abbrev Blaster.Smt.SmtConstructorDecl : Type

Equations

• Blaster.Smt.SmtConstructorDecl = (Blaster.Smt.SmtSymbol × Option (Array Blaster.Smt.SmtSelector))

structure Blaster.Smt.SmtDatatypeDecl : Type

• params : Option (Array SmtSymbol)
• ctors : Array SmtConstructorDecl

instance Blaster.Smt.instInhabitedSmtDatatypeDecl : Inhabited SmtDatatypeDecl

Equations

• Blaster.Smt.instInhabitedSmtDatatypeDecl = { default := { params := none, ctors := #[] } }

structure Blaster.Smt.SmtSortDecl : Type

• name : SmtSymbol
• arity : Nat

instance Blaster.Smt.instInhabitedSmtSortDecl : Inhabited SmtSortDecl

Equations

• Blaster.Smt.instInhabitedSmtSortDecl = { default := { name := default, arity := 0 } }

structure Blaster.Smt.SmtFunDecl : Type

• name : SmtSymbol
• params : SortedVars
• ret : SortExpr

instance Blaster.Smt.instInhabitedSmtFunDecl : Inhabited SmtFunDecl

Equations

• Blaster.Smt.instInhabitedSmtFunDecl = { default := { name := default, params := #[], ret := default } }

inductive Blaster.Smt.SmtCommand : Type

Smt-Lib V2 command submitted to backend solver.

• assertTerm (t : SmtTerm) : SmtCommand
• checkSat : SmtCommand
• checkSatAssuming (args : Array SmtTerm) : SmtCommand
• declareConst (nm : SmtSymbol) (t : SortExpr) : SmtCommand
• declareDataType (nm : SmtSymbol) (decl : SmtDatatypeDecl) : SmtCommand
• declareMutualDataTypes (nms : Array SmtSortDecl) (decls : Array SmtDatatypeDecl) : SmtCommand
• declareFun (nm : SmtSymbol) (args : Array SortExpr) (rt : SortExpr) : SmtCommand
• defineFun (isRec : Bool) (nm : SmtSymbol) (args : SortedVars) (rt : SortExpr) (body : SmtTerm) : SmtCommand
• defineFunsRec (decls : Array SmtFunDecl) (bodies : Array SmtTerm) : SmtCommand
• declareSort (nm : SmtSymbol) (arity : Nat) : SmtCommand
• defineSort (nm : SmtSymbol) (args : Option (Array SmtSymbol)) (body : SortExpr) : SmtCommand
• exitSmt : SmtCommand
• getModel : SmtCommand
• getProof : SmtCommand
• evalTerm (t : SmtTerm) : SmtCommand
• setLogic (l : String) : SmtCommand
• setOption (opt value : String) : SmtCommand

instance Blaster.Smt.instInhabitedSmtCommand : Inhabited SmtCommand

Equations

• Blaster.Smt.instInhabitedSmtCommand = { default := Blaster.Smt.SmtCommand.setLogic "" }

Set of Smt-Lib V2 permitted characters in "simple" smt symbol.

opaque Blaster.Smt.validSimpleChars : String

ToString instances for Smt-Lib V2 syntax.

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.
• (Blaster.Smt.SmtSymbol.ReservedSymbol str).toString = str

instance Blaster.Smt.instToStringSmtSymbol : ToString SmtSymbol

Equations

• Blaster.Smt.instToStringSmtSymbol = { toString := Blaster.Smt.SmtSymbol.toString }

instance Blaster.Smt.instToStringSortExpr : ToString SortExpr

Equations

• Blaster.Smt.instToStringSortExpr = { toString := Blaster.Smt.SortExpr.toString✝ }

instance Blaster.Smt.instToStringSortedVars : ToString SortedVars

Equations

• Blaster.Smt.instToStringSortedVars = { toString := Blaster.Smt.SortedVars.toString✝ }

instance Blaster.Smt.instToStringSmtQualifiedIdent : ToString SmtQualifiedIdent

Equations

• Blaster.Smt.instToStringSmtQualifiedIdent = { toString := Blaster.Smt.SmtQualifiedIdent.toString✝ }

instance Blaster.Smt.instToStringSmtAttribute : ToString SmtAttribute

Equations

• Blaster.Smt.instToStringSmtAttribute = { toString := Blaster.Smt.SmtAttribute.toString✝ }

instance Blaster.Smt.instToStringSmtTerm : ToString SmtTerm

Equations

• Blaster.Smt.instToStringSmtTerm = { toString := Blaster.Smt.SmtTerm.toString✝ }

instance Blaster.Smt.instToStringSmtSelector : ToString SmtSelector

Equations

• Blaster.Smt.instToStringSmtSelector = { toString := Blaster.Smt.SmtSelector.toString✝ }

instance Blaster.Smt.instToStringSmtConstructorDecl : ToString SmtConstructorDecl

Equations

• Blaster.Smt.instToStringSmtConstructorDecl = { toString := Blaster.Smt.SmtConstructorDecl.toString✝ }

instance Blaster.Smt.instToStringSmtDatatypeDecl : ToString SmtDatatypeDecl

Equations

• Blaster.Smt.instToStringSmtDatatypeDecl = { toString := Blaster.Smt.SmtDatatypeDecl.toString✝ }

instance Blaster.Smt.instToStringSmtSortDecl : ToString SmtSortDecl

Equations

• Blaster.Smt.instToStringSmtSortDecl = { toString := Blaster.Smt.SmtSortDecl.toString✝ }

instance Blaster.Smt.instToStringSmtFunDecl : ToString SmtFunDecl

Equations

• Blaster.Smt.instToStringSmtFunDecl = { toString := Blaster.Smt.SmtFunDecl.toString✝ }

instance Blaster.Smt.instToStringSmtCommand : ToString SmtCommand

Equations

• Blaster.Smt.instToStringSmtCommand = { toString := Blaster.Smt.SmtCommand.toString✝ }