Sequences, typed

def Cvc.Typed.Term.seqConcat [Ω] {α : Type} (lft rgt : Term (Array α)) : Env (Term (Array α))

Concatenation.

Equations

• lft.seqConcat rgt = Cvc.Untyped.Term.seqConcat lft rgt

def Cvc.Typed.Term.seqRev [Ω] {α : Type} (s : Term (Array α)) : Env (Term (Array α))

Reversal.

Equations

• s.seqRev = Cvc.Untyped.Term.seqRev s

def Cvc.Typed.Term.seqReplace [Ω] {α : Type} (s pat repl : Term (Array α)) : Env (Term (Array α))

Replaces the first occurrence of a sub-sequence.

Equations

• s.seqReplace pat repl = Cvc.Untyped.Term.seqReplace s pat repl

def Cvc.Typed.Term.seqSuffix [Ω] {α : Type} (suf s : Term (Array α)) : Env (Term Bool)

Whether suf is a suffix of s.

Equations

• suf.seqSuffix s = Cvc.Untyped.Term.seqSuffix suf s

def Cvc.Typed.Term.mkEmptySeq [Ω] {α : Type} [ToTyp α] : Env (Term (Array α))

The empty sequence of elements of sort α.

Equations

• Cvc.Typed.Term.mkEmptySeq = do let srtOfα ← Cvc.Srt.of α Cvc.Untyped.Term.mkEmptySeq srtOfα

def Cvc.Typed.Term.seqContains [Ω] {α : Type} (s sub : Term (Array α)) : Env (Term Bool)

Whether s contains sub.

Equations

• s.seqContains sub = Cvc.Untyped.Term.seqContains s sub

def Cvc.Typed.Term.seqUpdate [Ω] {α : Type} (s : Term (Array α)) (idx : Term Int) (repl : Term (Array α)) : Env (Term (Array α))

Overwrites s from idx with repl, keeping its length; s if idx is out of range.

Equations

• s.seqUpdate idx repl = Cvc.Untyped.Term.seqUpdate s idx repl

def Cvc.Typed.Term.seqAt [Ω] {α : Type} (s : Term (Array α)) (idx : Term Int) : Env (Term (Array α))

The one-element sequence at an index, or the empty sequence if out of bounds.

Equations

• s.seqAt idx = Cvc.Untyped.Term.seqAt s idx

def Cvc.Typed.Term.seqExtract [Ω] {α : Type} (s : Term (Array α)) (idx len : Term Int) : Env (Term (Array α))

The sub-sequence of length len starting at idx; empty when out of range.

Equations

• s.seqExtract idx len = Cvc.Untyped.Term.seqExtract s idx len

def Cvc.Typed.Term.seqIndexof [Ω] {α : Type} (s sub : Term (Array α)) (start : Term Int) : Env (Term Int)

Index of the first occurrence of sub in s at or after start, or -1.

Equations

• s.seqIndexof sub start = Cvc.Untyped.Term.seqIndexof s sub start

def Cvc.Typed.Term.seqReplaceAll [Ω] {α : Type} (s pat repl : Term (Array α)) : Env (Term (Array α))

Replaces every occurrence of a sub-sequence.

Equations

• s.seqReplaceAll pat repl = Cvc.Untyped.Term.seqReplaceAll s pat repl

def Cvc.Typed.Term.seqUnit [Ω] {α : Type} (elm : Term α) : Env (Term (Array α))

The one-element sequence.

Equations

• elm.seqUnit = Cvc.Untyped.Term.seqUnit elm

def Cvc.Typed.Term.seqPrefix [Ω] {α : Type} (pre s : Term (Array α)) : Env (Term Bool)

Whether pre is a prefix of s.

Equations

• pre.seqPrefix s = Cvc.Untyped.Term.seqPrefix pre s

def Cvc.Typed.Term.seqConcatN [Ω] {α : Type} (terms : Terms (Array α)) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (Array α))

seqConcat over two or more terms.

Equations

• Cvc.Typed.Term.seqConcatN terms atLeastTwoElements = Cvc.Untyped.Term.seqConcatN terms atLeastTwoElements

def Cvc.Typed.Term.seqNth [Ω] {α : Type} (s : Term (Array α)) (idx : Term Int) : Env (Term α)

The element at idx; unspecified out of bounds.

Equations

• s.seqNth idx = Cvc.Untyped.Term.seqNth s idx

def Cvc.Typed.Term.seqLength [Ω] {α : Type} (s : Term (Array α)) : Env (Term Int)

Length.

Equations

• s.seqLength = Cvc.Untyped.Term.seqLength s

inductive Cvc.Typed.View.Seq.OnInt [Ω] : Type

Seq's operators with a result of sort Int.

• seqLength [Ω] (α : Typ) (s : Term (Typ.seq (Typ?.typ α)).Denote) : OnInt

  Length.

• seqIndexof [Ω] (α : Typ) (s sub : Term (Typ.seq (Typ?.typ α)).Denote) (start : Term Int) : OnInt

  Index of the first occurrence of sub in s at or after start, or -1.

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

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

• seqNth [Ω] {β : Type} [ToTyp β] (s : Term (Array β)) (idx : Term Int) : OnAny β

  The element at idx; unspecified out of bounds.

inductive Cvc.Typed.View.Seq.OnSeq [Ω] (γ : Type) [ToTyp γ] : Type

Seq's operators with a result of sort Seq.

• seqUnit [Ω] {γ : Type} [ToTyp γ] (elm : Term γ) : OnSeq γ

  The one-element sequence.

• seqConcat [Ω] {γ : Type} [ToTyp γ] (kids : Kids (Array γ)) : OnSeq γ

  Concatenation.

  kids holds every operand, two or more.

• seqAt [Ω] {γ : Type} [ToTyp γ] (s : Term (Array γ)) (idx : Term Int) : OnSeq γ

  The one-element sequence at an index, or the empty sequence if out of bounds.

• seqExtract [Ω] {γ : Type} [ToTyp γ] (s : Term (Array γ)) (idx len : Term Int) : OnSeq γ

  The sub-sequence of length len starting at idx; empty when out of range.

• seqUpdate [Ω] {γ : Type} [ToTyp γ] (s : Term (Array γ)) (idx : Term Int) (repl : Term (Array γ)) : OnSeq γ

  Overwrites s from idx with repl, keeping its length; s if idx is out of range.

• seqReplace [Ω] {γ : Type} [ToTyp γ] (s pat repl : Term (Array γ)) : OnSeq γ

  Replaces the first occurrence of a sub-sequence.

• seqReplaceAll [Ω] {γ : Type} [ToTyp γ] (s pat repl : Term (Array γ)) : OnSeq γ

  Replaces every occurrence of a sub-sequence.

• seqRev [Ω] {γ : Type} [ToTyp γ] (s : Term (Array γ)) : OnSeq γ

  Reversal.

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

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

Equations

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

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

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

• seq [Ω] (γ : Typ) : OnSeq γ.Denote → View.Seq (Typ.seq (Typ?.typ γ))

  An operator with a result of sort Seq.

• int [Ω] : OnInt → View.Seq Typ.int

  An operator with a result of sort Int.

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

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

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

  An operator with a result of sort Bool.

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

Seq's operators with a result of sort Bool.

• seqContains [Ω] (α : Typ) (s sub : Term (Typ.seq (Typ?.typ α)).Denote) : OnBool

  Whether s contains sub.

• seqPrefix [Ω] (α : Typ) (pre s : Term (Typ.seq (Typ?.typ α)).Denote) : OnBool

  Whether pre is a prefix of s.

• seqSuffix [Ω] (α : Typ) (suf s : Term (Typ.seq (Typ?.typ α)).Denote) : OnBool

  Whether suf is a suffix of s.

Values

def Cvc.Typed.Term.isSeqValue [Ω] {α : Type} (term : Term (Array α)) : Bool

Whether a term is a sequence value, of kind CONST_SEQUENCE.

Such values are what a model answers; a sequence built from constructors, such as seqConcat (seqUnit 0) (seqUnit 1), is not one even when its elements are values.

Equations

• term.isSeqValue = Cvc.Untyped.Term.isSeqValue term

def Cvc.Typed.Term.getSeqValue [Ω] {α : Type} [TermToValue α] (term : Term (Array α)) : Env (Array α)

The elements a constant sequence term denotes.

Only a sequence value in cvc5's normal form, such as a model's answer, is accepted: a term built by mkSeqValue is not one.

Equations

• term.getSeqValue = Cvc.Untyped.Term.getSeqValue term

def Cvc.Typed.Term.getSeqValueOf [Ω] (α : Type) [TermToValue α] (term : Term (Array α)) : Env (Array α)

The elements a constant sequence term denotes.

Only a sequence value in cvc5's normal form, such as a model's answer, is accepted: a term built by mkSeqValue is not one.

Equations

• Cvc.Typed.Term.getSeqValueOf α = Cvc.Typed.Term.getSeqValue

def Cvc.Typed.Term.mkSeqValue [Ω] {α : Type} [ToTyp α] [ValueToTerm α] (elems : Array α) : Env (Term (Array α))

The sequence term denoting an array of values.

Equations

• Cvc.Typed.Term.mkSeqValue = Cvc.Untyped.Term.mkSeqValue

@[instance_reducible]

instance Cvc.Typed.Term.instValueToTermArrayOfToTyp {α : Type} [ToTyp α] [ValueToTerm α] : ValueToTerm (Array α)

Equations

• Cvc.Typed.Term.instValueToTermArrayOfToTyp = { valueToTerm := fun [Cvc.Ω] => Cvc.Typed.Term.mkSeqValue }

@[instance_reducible]

instance Cvc.Typed.Term.instTermToValueArray {α : Type} [TermToValue α] : TermToValue (Array α)

Equations

• Cvc.Typed.Term.instTermToValueArray = { termToValue := fun [Cvc.Ω] => Cvc.Typed.Term.getSeqValue }