Generated Array constructors, sort-erased

def Cvc.Untyped.Term.eqRange [Ω] (lft rgt lo hi : Term) : Env Term

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.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.EQ_RANGE #[lft, rgt, lo, hi]

def Cvc.Untyped.Term.store [Ω] (arr idx elm : Term) : Env Term

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

Equations

• arr.store idx elm = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.STORE #[arr, idx, elm]

def Cvc.Untyped.Term.select [Ω] (arr idx : Term) : Env Term

Reads the element stored at an index.

Equations

• arr.select idx = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SELECT #[arr, idx]

def Cvc.Untyped.Term.mkConstArray [Ω] (ι : Srt) (default : Term) : Env Term

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

Equations

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

inductive Cvc.Untyped.View.Array [Ω] : Type

Array's operators, taken apart one level, sort-erased.

• select [Ω] (arr idx : Term) : View.Array

  Reads the element stored at an index.

• store [Ω] (arr idx elm : Term) : View.Array

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

• eqRange [Ω] (lft rgt lo hi : Term) : View.Array

  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.

def Cvc.Untyped.View.Array.of? [Ω] (viewed : Term) : Option View.Array

Takes a term apart one level, if Array owns its operator.

Equations

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

Values

A TotalMap denotes an SMT array: a constant array holding the default element, with one store per binding. Reading one back peels that spine, keeping the outermost store for a repeated index since it is the one that wins.

def Cvc.Untyped.Term.isConstArray [Ω] (term : Term) : Bool

Determine if this term is a constant array.

Equations

• term.isConstArray = (Cvc.Untyped.Term.toUnsafe✝ term).isConstArray

def Cvc.Untyped.Term.getConstArrayBase? [Ω] (term : Term) : Option Term

The default element of a constant-array term, if it is one.

Equations

• term.getConstArrayBase? = (Cvc.Untyped.Term.toUnsafe✝ term).getConstArrayBase?

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

The array term denoting a total map.

Equations

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

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

The total map a constant array term denotes.

Equations

• term.getArrayValue = Cvc.Untyped.Term.getArrayValue.peel✝ Std.TreeMap.empty term

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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