structure Cvc.AnyFloat (exp sig : UInt32) : Type

A float with generic exponent and significand, see also Cvc.Float.

@[reducible, inline]

abbrev Cvc.Float : Type

Equivalent of Float by enforcing the IEEE 754 standard, see also Cvc.AnyFloat.

Equations

• Cvc.Float = Cvc.AnyFloat 11 53

structure Cvc.Abstract (kind : Srt.Kind) : Type

structure Cvc.TMap (Idx Elm : Type) extends Ord Idx : Type

Total map from Idx to Elm, called array in SMT-LIB/cvc.

• compare : Idx → Idx → Ordering
• toRBMap : RBMap Idx Elm

  Red-black map representation containing indices with known value.

def Cvc.TMap.ofRBMap {Idx : Type} [Ord Idx] {Elm : Type} (toRBMap : RBMap Idx Elm) : Cvc.TMap Idx Elm

Constructor.

Equations

• Cvc.TMap.ofRBMap toRBMap = { toOrd := inferInstance, toRBMap := toRBMap }

@[reducible, inline]

abbrev Cvc.TMap.unspecified {Idx : Type} [Ord Idx] {Elm : Type} : Cvc.TMap Idx Elm

A total map with unknown values for all indices.

Equations

• Cvc.TMap.unspecified = Cvc.TMap.ofRBMap Cvc.RBMap.empty

def Cvc.TMap.get {Idx Elm : Type} (array : Cvc.TMap Idx Elm) (idx : Idx) : Option Elm

The known value of an index if any.

Equations

• array.get idx = Batteries.RBMap.find? array.toRBMap idx

def Cvc.TMap.getD {Idx Elm : Type} (array : Cvc.TMap Idx Elm) (idx : Idx) (defaultVal : Elm) : Elm

The known value of an index or a default value.

Equations

• array.getD idx defaultVal = (array.get idx).getD defaultVal

def Cvc.TMap.getI {Idx Elm : Type} (array : Cvc.TMap Idx Elm) [Inhabited Elm] (idx : Idx) : Elm

The known value of an index for Inhabited elements.

Equations

• array.getI idx = (array.get idx).getD default

instance Cvc.TMap.instGetElemOptionTrue {Idx Elm : Type} : GetElem (Cvc.TMap Idx Elm) Idx (Option Elm) fun (x : Cvc.TMap Idx Elm) (x : Idx) => True

Equations

• Cvc.TMap.instGetElemOptionTrue = { getElem := fun (array : Cvc.TMap Idx Elm) (idx : Idx) (x : True) => array.get idx }

structure Cvc.Bag (Elm : Type) extends Ord Elm : Type

Map between elements and their cardinality in the bag.

• compare : Elm → Elm → Ordering
• toRBMap : RBMap Elm Nat

  Black-tree map representation.

def Cvc.Bag.ofRBMap {Elm : Type} [Ord Elm] (toRBMap : RBMap Elm Nat) : Cvc.Bag Elm

Constructor.

Equations

• Cvc.Bag.ofRBMap toRBMap = { toOrd := inferInstance, toRBMap := toRBMap }

def Cvc.Bag.empty {Elm : Type} [Ord Elm] : Cvc.Bag Elm

Empty bag constructor.

Equations

• Cvc.Bag.empty = { toOrd := inferInstance, toRBMap := Cvc.RBMap.empty }

def Cvc.Bag.distinctSize {Elm : Type} (bag : Cvc.Bag Elm) : Nat

Number of distinct elements in the map.

Equations

• bag.distinctSize = Batteries.RBMap.size bag.toRBMap

def Cvc.Bag.size {Elm : Type} (bag : Cvc.Bag Elm) : Nat

Number of elements in the map, see also distinctSize.

Equations

• bag.size = Batteries.RBMap.foldl (fun (sum : Nat) (x : Elm) (n : Nat) => sum + n) 0 bag.toRBMap

def Cvc.Bag.card {Elm : Type} (bag : Cvc.Bag Elm) : Nat

Number of elements in the map, see also distinctSize.

Equations

• @Cvc.Bag.card = @Cvc.Bag.size

def Cvc.Bag.getMult {Elm : Type} (bag : Cvc.Bag Elm) (elm : Elm) : Nat

Retrieves the multiplicity of an element.

Equations

• bag.getMult elm = (Batteries.RBMap.find? bag.toRBMap elm).getD 0

def Cvc.Bag.contains {Elm : Type} (bag : Cvc.Bag Elm) (elm : Elm) : Bool

True on elements of multiplicity at least one.

Equations

• bag.contains elm = match Batteries.RBMap.find? bag.toRBMap elm with | none => false | some 0 => false | some n.succ => true

def Cvc.Bag.erase {Elm : Type} (bag : Cvc.Bag Elm) (elm : Elm) : Cvc.Bag Elm

Removes an element from the bag.

Equations

• bag.erase elm = { toOrd := bag.toOrd, toRBMap := bag.toRBMap.erase elm }

def Cvc.Bag.setCard {Elm : Type} (bag : Cvc.Bag Elm) (elm : Elm) (count : Nat) : Cvc.Bag Elm

Forces the multiplicity of an element.

Equations

• bag.setCard elm 0 = bag.erase elm
• bag.setCard elm x✝ = { toOrd := bag.toOrd, toRBMap := bag.toRBMap.insert elm x✝ }

def Cvc.Bag.countDo {Elm : Type} (bag : Cvc.Bag Elm) (elm : Elm) {α : Sort u_1} (f : Nat → α) : α

Passes the multiplicity of an element to a function.

Equations

• bag.countDo elm f = f (Batteries.RBMap.findD bag.toRBMap elm 0)

def Cvc.Bag.countMap {Elm : Type} (bag : Cvc.Bag Elm) (elm : Elm) (f : Nat → Nat) : Cvc.Bag Elm

Map over the multiplicity of an element.

Equations

• bag.countMap elm f = bag.setCard elm (bag.countDo elm f)

def Cvc.Bag.insert {Elm : Type} (bag : Cvc.Bag Elm) (elm : Elm) (count : Nat := 1) : Cvc.Bag Elm

Inserts an element count times.

Equations

• bag.insert elm count = bag.countMap elm fun (x : Nat) => x + count

def Cvc.Bag.remove {Elm : Type} (bag : Cvc.Bag Elm) (elm : Elm) (count : Nat := 1) : Cvc.Bag Elm

Removes an element count times.

Equations

• bag.remove elm count = bag.countMap elm fun (x : Nat) => x - count

structure Cvc.FiniteField (n : Nat) : Type

structure Cvc.RoundingMode : Type

structure Cvc.Regex : Type

Regular expression.

• toString : String

  String representation.

structure Cvc.Set (Elm : Type) extends Ord Elm : Type

A set of elements.

• compare : Elm → Elm → Ordering
• toRBSet : RBSet Elm

  Red-black set representation.

def Cvc.Set.ofRBSet {Elm : Type} [Ord Elm] (toRBSet : RBSet Elm) : Cvc.Set Elm

Constructor.

Equations

• Cvc.Set.ofRBSet toRBSet = { toOrd := inferInstance, toRBSet := toRBSet }

def Cvc.Set.empty {Elm : Type} [Ord Elm] : Cvc.Set Elm

Empty set.

Equations

• Cvc.Set.empty = Cvc.Set.ofRBSet Cvc.RBSet.empty

def Cvc.Set.size {Elm : Type} (set : Cvc.Set Elm) : Nat

Size of the set.

Equations

• set.size = Batteries.RBSet.size set.toRBSet

def Cvc.Set.card {Elm : Type} (set : Cvc.Set Elm) : Nat

Size of the set.

Equations

• @Cvc.Set.card = @Cvc.Set.size

def Cvc.Set.contains {Elm : Type} (set : Cvc.Set Elm) (elm : Elm) : Bool

True if the element is in the set.

Equations

• set.contains elm = Batteries.RBSet.contains set.toRBSet elm

def Cvc.Set.insert {Elm : Type} (set : Cvc.Set Elm) (elm : Elm) : Cvc.Set Elm

Inserts an element in the set.

Equations

• set.insert elm = { toOrd := set.toOrd, toRBSet := set.toRBSet.insert elm }

structure Cvc.Uninterpreted (name : String) : Type

@[reducible, inline]

abbrev Cvc.Srt.toType : Srt → Type

Type corresponding to an Srt.

Equations

• (Cvc.Srt.abstract kind).toType = Cvc.Abstract kind
• (idx.array elm).toType = Cvc.TMap idx.toType elm.toType
• elm.bag.toType = Cvc.Bag elm.toType
• Cvc.Srt.bool.toType = Bool
• (Cvc.Srt.bitVec n).toType = BitVec n
• (Cvc.Srt.finiteField n).toType = Cvc.FiniteField n
• (Cvc.Srt.float exp sig).toType = Cvc.AnyFloat exp sig
• (dom.function cod).toType = (dom.toType → cod.toType)
• Cvc.Srt.int.toType = Int
• (lft.prod rgt).toType = (lft.toType × rgt.toType)
• Cvc.Srt.real.toType = Rat
• Cvc.Srt.regex.toType = Cvc.Regex
• Cvc.Srt.roundingMode.toType = Cvc.RoundingMode
• elm.seq.toType = Array elm.toType
• elm.set.toType = Cvc.Set elm.toType
• Cvc.Srt.string.toType = String
• Cvc.Srt.unit.toType = Unit
• (Cvc.Srt.uninterpreted cons).toType = Cvc.Uninterpreted cons

instance Cvc.Srt.instCoeSortType : CoeSort Srt Type

Equations

• Cvc.Srt.instCoeSortType = { coe := Cvc.Srt.toType }