inductive Cvc.Srt.Kind :

A sort kind.

abstract : Kind
array : Kind
bag : Kind
bool : Kind
bitVec : Kind
finiteField : Kind
float : Kind
function : Kind
int : Kind
prod : Kind
real : Kind
regex : Kind
roundingMode : Kind
seq : Kind
set : Kind
string : Kind
unit : Kind
uninterpreted : Kind

Instances For

source

instance Cvc.Srt.instOrdKind :

Ord Kind

Equations

Cvc.Srt.instOrdKind = { compare := Cvc.Srt.ordKind✝ }

source

inductive Cvc.Srt :

Type

A cvc sort, Sort-coercion realized by Srt.toType.

abstract (kind : Kind) : Srt
An abstract sort.
array (idx elm : Srt) : Srt
Total map from an index sort to an element sort.
Called array in SMT-LIB/cvc.
bag (elm : Srt) : Srt
A multi-set/bag of elements.
bool : Srt
Boolean sort.
bitVec (size : Nat) : Srt
Sort of bit-vectors of length size.
finiteField (size : Nat) : Srt
Finite field sort.
float (exp sig : UInt32) : Srt
Floating-point sort.
function (dom cod : Srt) : Srt
Function sort.
Cvc5 actually takes an array of domains, and I think, does not allow the codomain to be a function sort. We're trying to adapt cvc5 sorts for a lean world by pretending they behave as lean function types.
int : Srt
Integer sort.
prod (lft rgt : Srt) : Srt
Product sort.
Cvc5 has a notion of tuple or arity [0, ∞[, but that maps terribly to lean types. The goal with this constructor is to limit Srt creation to only (binary) products.
real : Srt
Real sort.
regex : Srt
Regular expression sort.
roundingMode : Srt
Rounding mode sort.
seq (elm : Srt) : Srt
Array sort, called sequence in SMT-LIB/cvc.
set (elm : Srt) : Srt
Set sort.
string : Srt
String sort.
unit : Srt
Unit sort.
uninterpreted (name : String) : Srt
An uninterpreted sort.

Instances For

source

instance Cvc.Srt.instInhabitedKind :

Inhabited Kind

Equations

Cvc.Srt.instInhabitedKind = { default := Cvc.Srt.Kind.abstract }

source

instance Cvc.Srt.instDecidableEqKind :

DecidableEq Kind

Equations

Cvc.Srt.instDecidableEqKind x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

source

instance Cvc.instHashableSrt :

Hashable Srt

Equations

Cvc.instHashableSrt = { hash := Cvc.hashSrt✝ }

source

def Cvc.Srt.kind :

Srt → Kind

Turns a sort into a sort kind.

Equations

Instances For

source

instance Cvc.instInhabitedSrt :

Inhabited Srt

Equations

Cvc.instInhabitedSrt = { default := Cvc.Srt.abstract default }

source

instance Cvc.Srt.Kind.instToString :

ToString Kind

Equations

Cvc.Srt.Kind.instToString = { toString := Cvc.Srt.Kind.toString }

source

def Cvc.Srt.Kind.toString :

Kind → String

String representation.

Equations

Cvc.Srt.Kind.abstract.toString = "abstract"
Cvc.Srt.Kind.array.toString = "array"
Cvc.Srt.Kind.bag.toString = "bag"
Cvc.Srt.Kind.bool.toString = "bool"
Cvc.Srt.Kind.bitVec.toString = "bitVec"
Cvc.Srt.Kind.finiteField.toString = "finiteField"
Cvc.Srt.Kind.float.toString = "float"
Cvc.Srt.Kind.function.toString = "function"
Cvc.Srt.Kind.int.toString = "int"
Cvc.Srt.Kind.prod.toString = "prod"
Cvc.Srt.Kind.real.toString = "real"
Cvc.Srt.Kind.regex.toString = "regex"
Cvc.Srt.Kind.roundingMode.toString = "roundingMode"
Cvc.Srt.Kind.seq.toString = "seq"
Cvc.Srt.Kind.set.toString = "set"
Cvc.Srt.Kind.string.toString = "string"
Cvc.Srt.Kind.unit.toString = "unit"
Cvc.Srt.Kind.uninterpreted.toString = "uninterpreted"

Instances For

source

def Cvc.Srt.Kind.toSort :

Kind → cvc5.SortKind

Turns itself into an unsafe sort.

Equations

Instances For

source

def Cvc.Srt.Kind.ofSrt :

Srt → Kind

Turns a sort into a sort kind.

Equations

Cvc.Srt.Kind.ofSrt = Cvc.Srt.kind

Instances For

source

instance Cvc.Srt.instHashableKind :

Hashable Kind

Equations

Cvc.Srt.instHashableKind = { hash := Cvc.Srt.hashKind✝ }

source

instance Cvc.Srt.instDecidableEqListSrt :

DecidableEq (List Srt)

Equations

One or more equations did not get rendered due to their size.
Cvc.Srt.instDecidableEqListSrt [] (head :: tail) = isFalse ⋯
Cvc.Srt.instDecidableEqListSrt (head :: tail) [] = isFalse ⋯
Cvc.Srt.instDecidableEqListSrt [] [] = isTrue Cvc.Srt.instDecidableEqListSrt._proof_8

source

instance Cvc.Srt.instDecidableEqArraySrt :

DecidableEq (Array Srt)

Equations

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

source

instance Cvc.Srt.instDecidableEq :

DecidableEq Srt

Equations

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

source

def Cvc.Srt.beq :

Srt → Srt → Bool

Boolean equality.

TODO #

Probably should not use instDecidableEq for boolean equality; I'm not sure how efficient the code generated is.

Equations

x1✝.beq x2✝ = decide (x1✝ = x2✝)

Instances For

source

inductive Cvc.Srt.toString.Paren :

Type

Specifies how to paren the string representation of a sort.

This only impacts the sort's top-level, paren for sub-sorts are decided by their super-sorts.

none : Paren
Don't paren the sort at all.
ifFunction : Paren
Only paren if it's a function.
ifArgs : Paren
Only paren argument-having type constructors such as (Array Bool).
composite : Paren
Always paren composite sorts (Array Bool) but not leaf-sorts Bool.

Instances For

source

instance Cvc.Srt.toString.instInhabitedParen :

Inhabited Paren

Equations

Cvc.Srt.toString.instInhabitedParen = { default := Cvc.Srt.toString.Paren.none }

source

instance Cvc.Srt.toString.instHashableParen :

Hashable Paren

Equations

Cvc.Srt.toString.instHashableParen = { hash := Cvc.Srt.toString.hashParen✝ }

source

instance Cvc.Srt.toString.instDecidableEqParen :

DecidableEq Paren

Equations

Cvc.Srt.toString.instDecidableEqParen x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

source

instance Cvc.Srt.toString.instOrdParen :

Ord Paren

Equations

Cvc.Srt.toString.instOrdParen = { compare := Cvc.Srt.toString.ordParen✝ }

source

def Cvc.Srt.toString.Paren.max :

Paren

Maximum paren-ing.

NB: leaf-sorts such as Srt.bool are never paren-ed.

Equations

Cvc.Srt.toString.Paren.max = Cvc.Srt.toString.Paren.composite

Instances For

source

def Cvc.Srt.toString.Paren.fun? :

Paren → Bool

Equations

Instances For

source

def Cvc.Srt.toString.Paren.args? :

Paren → Bool

Equations

Instances For

source

def Cvc.Srt.toString.Paren.apply? (self : Paren) :

Paren → Bool

Equations

self.apply? Cvc.Srt.toString.Paren.none = false
self.apply? Cvc.Srt.toString.Paren.ifFunction = self.fun?
self.apply? Cvc.Srt.toString.Paren.ifArgs = self.args?
self.apply? Cvc.Srt.toString.Paren.composite = decide (self = Cvc.Srt.toString.Paren.composite)

Instances For

source

def Cvc.Srt.toString.Paren.apply (self that : Paren) (s : String) :

String

Equations

self.apply that s = if self.apply? that = true then toString "(" ++ toString s ++ toString ")" else s

Instances For

source

partial def Cvc.Srt.toString (srt : Srt) (paren : toString.Paren := toString.Paren.none) :

String

String representation.

source

instance Cvc.Srt.instToString :

ToString Srt

Equations

Cvc.Srt.instToString = { toString := fun (srt : Cvc.Srt) => srt.toString }

source

def Cvc.Srt.ofSort (sort : cvc5.Sort) (maxDepth : Nat := 100000) :

Res Srt

Constructor from unsafe sorts.

This function recurses on sub-sorts retrieved by FFI: there is no chance to prove it terminates. Hence the maxDepth optional parameter that sets an upper-bound on the recursion depth, causing this function to crash if maxDepth is reached.

Equations

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

Instances For

source

def Cvc.Srt.ofSort.failKind {α : Type} (k : cvc5.SortKind) :

Res α

Equations

Cvc.Srt.ofSort.failKind k = Cvc.Res.failInternal (toString "unexpected sort-kind `" ++ toString k ++ toString "`")

Instances For

source

def Cvc.Srt.ofSort.aux (maxDepth : Nat := 100000) (sort : cvc5.Sort) :

Nat → Res Srt

Equations

One or more equations did not get rendered due to their size.
Cvc.Srt.ofSort.aux maxDepth sort 0 = Cvc.Res.failUser (toString "maximum depth `" ++ toString maxDepth ++ toString "` reached")