Generated Seq constructors, sort-erased

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

seqConcat over two or more terms.

Equations

• Cvc.Untyped.Term.seqConcatN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_CONCAT terms

def Cvc.Untyped.Term.seqReplaceAll [Ω] (s pat repl : Term) : Env Term

Replaces every occurrence of a sub-sequence.

Equations

• s.seqReplaceAll pat repl = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_REPLACE_ALL #[s, pat, repl]

def Cvc.Untyped.Term.seqReplace [Ω] (s pat repl : Term) : Env Term

Replaces the first occurrence of a sub-sequence.

Equations

• s.seqReplace pat repl = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_REPLACE #[s, pat, repl]

def Cvc.Untyped.Term.seqAt [Ω] (s idx : Term) : Env Term

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

Equations

• s.seqAt idx = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_AT #[s, idx]

def Cvc.Untyped.Term.seqIndexof [Ω] (s sub start : Term) : Env Term

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

Equations

• s.seqIndexof sub start = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_INDEXOF #[s, sub, start]

def Cvc.Untyped.Term.mkEmptySeq [Ω] (α : Srt) : Env Term

The empty sequence of elements of sort α.

Equations

• Cvc.Untyped.Term.mkEmptySeq α = do let builtSrt ← pure α Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkEmptySequence builtSrt

def Cvc.Untyped.Term.seqExtract [Ω] (s idx len : Term) : Env Term

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

Equations

• s.seqExtract idx len = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_EXTRACT #[s, idx, len]

def Cvc.Untyped.Term.smtOp.binary.seqConcat : Lean.TrailingParserDescr

Equations

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

def Cvc.Untyped.Term.smtOp.nary.seqConcat : Lean.ParserDescr

Equations

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

def Cvc.Untyped.Term.seqNth [Ω] (s idx : Term) : Env Term

The element at idx; unspecified out of bounds.

Equations

• s.seqNth idx = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_NTH #[s, idx]

def Cvc.Untyped.Term.seqSuffix [Ω] (suf s : Term) : Env Term

Whether suf is a suffix of s.

Equations

• suf.seqSuffix s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_SUFFIX #[suf, s]

def Cvc.Untyped.Term.seqRev [Ω] (s : Term) : Env Term

Reversal.

Equations

• s.seqRev = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_REV #[s]

def Cvc.Untyped.Term.seqLength [Ω] (s : Term) : Env Term

Length.

Equations

• s.seqLength = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_LENGTH #[s]

def Cvc.Untyped.Term.seqUpdate [Ω] (s idx repl : Term) : Env Term

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

Equations

• s.seqUpdate idx repl = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_UPDATE #[s, idx, repl]

def Cvc.Untyped.Term.seqConcat [Ω] (lft rgt : Term) : Env Term

Concatenation.

Equations

• lft.seqConcat rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_CONCAT #[lft, rgt]

def Cvc.Untyped.Term.seqPrefix [Ω] (pre s : Term) : Env Term

Whether pre is a prefix of s.

Equations

• pre.seqPrefix s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_PREFIX #[pre, s]

def Cvc.Untyped.Term.seqContains [Ω] (s sub : Term) : Env Term

Whether s contains sub.

Equations

• s.seqContains sub = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_CONTAINS #[s, sub]

def Cvc.Untyped.Term.seqUnit [Ω] (elm : Term) : Env Term

The one-element sequence.

Equations

• elm.seqUnit = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEQ_UNIT #[elm]

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

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

• seqUnit [Ω] (elm : Term) : View.Seq

  The one-element sequence.

• seqConcat [Ω] (kids : Kids) : View.Seq

  Concatenation.

  kids holds every operand, two or more.

• seqLength [Ω] (s : Term) : View.Seq

  Length.

• seqAt [Ω] (s idx : Term) : View.Seq

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

• seqNth [Ω] (s idx : Term) : View.Seq

  The element at idx; unspecified out of bounds.

• seqExtract [Ω] (s idx len : Term) : View.Seq

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

• seqUpdate [Ω] (s idx repl : Term) : View.Seq

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

• seqIndexof [Ω] (s sub start : Term) : View.Seq

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

• seqReplace [Ω] (s pat repl : Term) : View.Seq

  Replaces the first occurrence of a sub-sequence.

• seqReplaceAll [Ω] (s pat repl : Term) : View.Seq

  Replaces every occurrence of a sub-sequence.

• seqRev [Ω] (s : Term) : View.Seq

  Reversal.

• seqContains [Ω] (s sub : Term) : View.Seq

  Whether s contains sub.

• seqPrefix [Ω] (pre s : Term) : View.Seq

  Whether pre is a prefix of s.

• seqSuffix [Ω] (suf s : Term) : View.Seq

  Whether suf is a suffix of s.

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

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

Equations

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

Values

A Lean Array denotes an SMT sequence: the empty sequence, then one unit sequence per element, concatenated.

def Cvc.Untyped.Term.isSeqValue [Ω] (term : Term) : 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.toUnsafe✝ term).isSequenceValue

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

The elements a constant sequence term denotes.

Equations

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

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

The elements a constant sequence term denotes.

Equations

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

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

The sequence term denoting an array of values.

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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