Arrays

The Lean type denoting an SMT array: a default element plus the finitely many indices that differ from it. Indices are held in a Std.TreeMap, so the index type must be ordered.

Converting a total map to a term and back is done by Cvc.Untyped.Theory.Array and Cvc.Typed.Theory.Array.

structure Cvc.TotalMap (α β : Type) [Ord α] : Type

A total map from α (the indices) to β (the elements), used to encode SMT-LIB arrays.

• defaultElem : β

  Default element that all indices not captured by map are mapped to.

• map : Std.TreeMap α β compare

  Maps indices to elements.

def Cvc.TotalMap.mkConst {α : Type} [Ord α] {β : Type} (defaultElem : β) : TotalMap α β

Equations

• Cvc.TotalMap.mkConst defaultElem = { defaultElem := defaultElem }

def Cvc.TotalMap.default {α : Type} [Ord α] {β : Type} [Inhabited β] : TotalMap α β

Equations

• Cvc.TotalMap.default = Cvc.TotalMap.mkConst default

instance Cvc.TotalMap.instNonempty {α : Type} [Ord α] {β : Type} [B : Nonempty β] : Nonempty (TotalMap α β)

@[instance_reducible]

instance Cvc.TotalMap.instInhabited {α : Type} [Ord α] {β : Type} [Inhabited β] : Inhabited (TotalMap α β)

Equations

• Cvc.TotalMap.instInhabited = { default := Cvc.TotalMap.default }

@[instance_reducible]

instance Cvc.TotalMap.instToTyp {α : Type} [Ord α] {β : Type} [ToTyp α] [ToTyp β] : ToTyp (TotalMap α β)

Equations

• Cvc.TotalMap.instToTyp = { typ := Cvc.Typ.arrayTo (Cvc.Typ?.typ (Cvc.Typ.of α)) (Cvc.Typ?.typ (Cvc.Typ.of β)) }

Basic operations

def Cvc.TotalMap.insert {α β : Type} [Ord α] (map : TotalMap α β) (key : α) (val : β) : TotalMap α β

Equations

• map.insert key val = { defaultElem := map.defaultElem, map := map.map.insert key val }

def Cvc.TotalMap.get? {α β : Type} [Ord α] (map : TotalMap α β) (key : α) : Option β

Equations

• map.get? key = map.map.get? key

def Cvc.TotalMap.get {α β : Type} [Ord α] (map : TotalMap α β) (key : α) : β

Equations

• map.get key = (map.get? key).getD map.defaultElem

String representation

def Cvc.TotalMap.foldlStrings {α β : Type} [Ord α] [ToString α] [ToString β] (map : TotalMap α β) {γ : Type u_1} (f : γ → Bool → String → γ) (init : γ) : γ

Equations

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

def Cvc.TotalMap.lines {α β : Type} [Ord α] [ToString α] [ToString β] (map : TotalMap α β) : Array String

Equations

• map.lines = map.foldlStrings (fun (acc : Array String) (x : Bool) (s : String) => acc.push s) #[]

def Cvc.TotalMap.toString {α β : Type} [Ord α] [ToString α] [ToString β] (map : TotalMap α β) : String

String representation.

Equations

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

@[instance_reducible]

instance Cvc.TotalMap.instToString {α β : Type} [Ord α] [ToString α] [ToString β] : ToString (TotalMap α β)

Equations

• Cvc.TotalMap.instToString = { toString := Cvc.TotalMap.toString }