Arrays, typed

def Cvc.Typed.Term.store [Ω] {ι κ : Type} [Ord ι] (arr : Term (TotalMap ι κ)) (idx : Term ι) (elm : Term κ) : Env (Term (TotalMap ι κ))

Writes an element at an index, yielding the updated array.

Equations

• arr.store idx elm = Cvc.Untyped.Term.store arr idx elm

def Cvc.Typed.Term.eqRange [Ω] {ι κ : Type} [Ord ι] (lft rgt : Term (TotalMap ι κ)) (lo hi : Term ι) : Env (Term Bool)

Equality of two arrays at every index from lo to hi, both included.

Needs cvc5's arrays-exp option, and an integer, real, bit-vector or floating-point index.

Equations

• lft.eqRange rgt lo hi = Cvc.Untyped.Term.eqRange lft rgt lo hi

def Cvc.Typed.Term.select [Ω] {ι κ : Type} [Ord ι] (arr : Term (TotalMap ι κ)) (idx : Term ι) : Env (Term κ)

Reads the element stored at an index.

Equations

• arr.select idx = Cvc.Untyped.Term.select arr idx

def Cvc.Typed.Term.mkConstArray [Ω] {ι κ : Type} [Ord ι] [ToTyp ι] [ToTyp κ] (default : Term κ) : Env (Term (TotalMap ι κ))

The array mapping every index, of sort ι, to default.

Equations

• default.mkConstArray = do let srtOfι ← Cvc.Srt.of ι Cvc.Untyped.Term.mkConstArray srtOfι default

inductive Cvc.Typed.View.Array [Ω] : Typ → Type

Array's operators, taken apart one level, indexed by the sort each produces.

• any [Ω] {τ : Typ} : OnAny τ.Denote → View.Array τ

  An operator whose result's sort is a type variable.

• array [Ω] (ξ ζ : Typ) [Ord ξ.Denote] : OnTotalMap ξ.Denote ζ.Denote → View.Array (Typ.arrayTo (Typ?.typ ξ) (Typ?.typ ζ))

  An operator with a result of sort TotalMap.

• bool [Ω] : OnBool → View.Array Typ.bool

  An operator with a result of sort Bool.

inductive Cvc.Typed.View.Array.OnTotalMap [Ω] (ξ : Type) [Ord ξ] [ToTyp ξ] (ζ : Type) [ToTyp ζ] : Type

Array's operators with a result of sort TotalMap.

• store [Ω] {ξ : Type} [Ord ξ] [ToTyp ξ] {ζ : Type} [ToTyp ζ] (arr : Term (TotalMap ξ ζ)) (idx : Term ξ) (elm : Term ζ) : OnTotalMap ξ ζ

  Writes an element at an index, yielding the updated array.

inductive Cvc.Typed.View.Array.OnBool [Ω] : Type

Array's operators with a result of sort Bool.

• eqRange [Ω] (ι κ : Typ) (lft rgt : Term (Typ.arrayTo (Typ?.typ ι) (Typ?.typ κ)).Denote) (lo hi : Term ι.Denote) : OnBool

  Equality of two arrays at every index from lo to hi, both included.

  Needs cvc5's arrays-exp option, and an integer, real, bit-vector or floating-point index.

inductive Cvc.Typed.View.Array.OnAny [Ω] (β : Type) [ToTyp β] : Type

Array's operators whose result's sort is a type variable.

• select [Ω] {β : Type} [ToTyp β] (ι : Typ) (arr : Term (Typ.arrayTo (Typ?.typ ι) (Typ?.typ (Typ.of β))).Denote) (idx : Term ι.Denote) : OnAny β

  Reads the element stored at an index.

def Cvc.Typed.View.Array.of [Ω] (τ : Typ) (t : Term τ.Denote) : Env (Option (View.Array τ))

Takes a term apart one level, at its sort, if Array owns its operator and the term's sort fits it.

Equations

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

Values

def Cvc.Typed.Term.isConstArray [Ω] {α β : Type} [Ord α] (term : Term (TotalMap α β)) : Bool

Determine if this term is a constant array.

Equations

• term.isConstArray = Cvc.Untyped.Term.isConstArray term

def Cvc.Typed.Term.mkArrayValue {α β : Type} [Ω] [Ord α] [ToTyp α] [ValueToTerm α] [ValueToTerm β] : TotalMap α β → Env (Term (TotalMap α β))

The array term denoting a total map.

Equations

• Cvc.Typed.Term.mkArrayValue = Cvc.Untyped.Term.mkArrayValue

def Cvc.Typed.Term.getArrayValue {α β : Type} [Ω] [Ord α] [TermToValue α] [TermToValue β] : Term (TotalMap α β) → Env (TotalMap α β)

The total map a constant array term denotes.

Equations

• Cvc.Typed.Term.getArrayValue = Cvc.Untyped.Term.getArrayValue

@[instance_reducible]

instance Cvc.Typed.Term.instValueToTermTotalMap {α β : Type} [Ord α] [ToTyp α] [ValueToTerm α] [ValueToTerm β] : ValueToTerm (TotalMap α β)

Equations

• Cvc.Typed.Term.instValueToTermTotalMap = { valueToTerm := fun [Cvc.Ω] => Cvc.Typed.Term.mkArrayValue }

@[instance_reducible]

instance Cvc.Typed.Term.instTermToValueTotalMap {α β : Type} [Ord α] [TermToValue α] [TermToValue β] : TermToValue (TotalMap α β)

Equations

• Cvc.Typed.Term.instTermToValueTotalMap = { termToValue := fun [Cvc.Ω] => Cvc.Typed.Term.getArrayValue }