Individual symbol representation

structure Cvc.Symbol (β α : Type) : Type

• name : String
• get : β

class Cvc.Symbol.Getter (α β : Type) : Type

• getInner : α → β

@[defaultInstance 1000]

instance Cvc.Symbol.instGetter {β α : Type} : Getter (Symbol β α) β

Equations

• Cvc.Symbol.instGetter = { getInner := Cvc.Symbol.get }

@[reducible, inline]

abbrev Cvc.Symbol.Ident (α : Type) : Type

Equations

• Cvc.Symbol.Ident α = Cvc.Symbol String α

instance Cvc.Symbol.instCoeSortIdentString {α : Type} : CoeSort (Symbol.Ident α) String

Equations

• Cvc.Symbol.instCoeSortIdentString = { coe := Cvc.Symbol.get }

@[reducible, inline]

abbrev Cvc.Symbol.Term (α : Type) : Type

Equations

• Cvc.Symbol.Term α = Cvc.Symbol (Cvc.Term α) α

instance Cvc.Symbol.instCoeTermTerm {α : Type} : Coe (Symbol.Term α) (Term α)

Equations

• Cvc.Symbol.instCoeTermTerm = { coe := Cvc.Symbol.get }

@[reducible, inline]

abbrev Cvc.Symbol.Value (α : Type) : Type

Equations

• Cvc.Symbol.Value α = Cvc.Symbol (Cvc.Value α) α

instance Cvc.Symbol.instCoeValueValue {α : Type} : Coe (Symbol.Value α) (Value α)

Equations

• Cvc.Symbol.instCoeValueValue = { coe := Cvc.Symbol.get }

@[reducible, inline]

abbrev Cvc.Symbol.Repr : Type 1

Equations

• Cvc.Symbol.Repr = ((α : Type) → [Cvc.IsSrt α] → Type)

@[reducible, inline]

abbrev Cvc.Symbol.Repr.Ident : Symbol.Repr

Equations

• Cvc.Symbol.Repr.Ident x✝¹ = String

@[reducible, inline]

abbrev Cvc.Symbol.Repr.Term : Symbol.Repr

Equations

• Cvc.Symbol.Repr.Term x✝ = Cvc.Term x✝

@[reducible, inline]

abbrev Cvc.Symbol.Repr.Value : Symbol.Repr

Equations

• Cvc.Symbol.Repr.Value x✝ = Cvc.Value x✝

def Cvc.Symbol.mapM {m : Type → Type u_1} {β α : Type} [Monad m] (sym : Symbol β α) {γ : Type} (f : β → m γ) : m (Symbol γ α)

Equations

• sym.mapM f = do let val ← f sym.get pure { name := sym.name, get := val }

def Cvc.Symbol.map {β α : Type} (sym : Symbol β α) {γ : Type} (f : β → γ) : Symbol γ α

Equations

• sym.map f = sym.mapM f

def Cvc.Symbol.mkIdent {α : Type} (name : String) : Symbol.Ident α

Equations

• Cvc.Symbol.mkIdent name = { name := name, get := name }

def Cvc.Symbol.mkIdent' (name : String) (α : Type) : Symbol.Ident α

Equations

• Cvc.Symbol.mkIdent' name α = { name := name, get := name }

def Cvc.Symbol.mkTerm {α : Type} : String → Term α → Symbol.Term α

Equations

• Cvc.Symbol.mkTerm = Cvc.Symbol.mk

def Cvc.Symbol.mkValue {α : Type} : String → Value α → Symbol.Value α

Equations

• Cvc.Symbol.mkValue = Cvc.Symbol.mk

def Cvc.Symbol.declare {α : Type} (ident : Symbol.Ident α) [IsSrt α] : Smt (Symbol.Term α)

Equations

• Cvc.Symbol.declare ident = do let term ← Cvc.Smt.declare' ident.name pure { name := ident.name, get := term }

@[reducible, inline]

abbrev Cvc.Symbol.Ident.mk {α : Type} (name : String) : Symbol.Ident α

Equations

• @Cvc.Symbol.Ident.mk = @Cvc.Symbol.mkIdent

@[reducible, inline]

abbrev Cvc.Symbol.Ident.mk' (name : String) (α : Type) : Symbol.Ident α

Equations

• Cvc.Symbol.Ident.mk' = Cvc.Symbol.mkIdent'

def Cvc.Symbol.Ident.toString {α : Type} (ident : Symbol.Ident α) : String

String representation.

Equations

• ident.toString = ident.name

instance Cvc.Symbol.Ident.instToString {α : Type} : ToString (Symbol.Ident α)

Equations

• Cvc.Symbol.Ident.instToString = { toString := Cvc.Symbol.Ident.toString }

def Cvc.Symbol.assert (sTerm : Symbol.Term Bool) : Smt Unit

Asserts a Boolean term-symbol.

TODO

• Is this function actually useful?

Equations

• Cvc.Symbol.assert sTerm = Cvc.Smt.assert sTerm.get

def Cvc.Symbol.getValue {α : Type} [IsSrt α] (term : Symbol.Term α) : Smt.Sat (Symbol.Value α)

Retrieves tho symbol-value of a symbol-term in a Sat context.

Equations

• Cvc.Symbol.getValue term = Cvc.Symbol.mkValue term.name <$> Cvc.Smt.getValue term.get

def Cvc.Symbol.Term.toString {α : Type} (term : Symbol.Term α) : String

String representation.

Equations

• term.toString = toString term.get

instance Cvc.Symbol.Term.instToString {α : Type} : ToString (Symbol.Term α)

Equations

• Cvc.Symbol.Term.instToString = { toString := Cvc.Symbol.Term.toString }

def Cvc.Symbol.Value.toString {α : Type} (value : Symbol.Value α) : String

String representation.

Equations

• value.toString = toString value.get

instance Cvc.Symbol.Value.instToString {α : Type} : ToString (Symbol.Value α)

Equations

• Cvc.Symbol.Value.instToString = { toString := Cvc.Symbol.Value.toString }