Strings, typed

def Cvc.Typed.Term.strSubstr [Ω] (s : Term String) (idx len : Term Int) : Env (Term String)

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

Equations

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

def Cvc.Typed.Term.strUpdate [Ω] (s : Term String) (idx : Term Int) (repl : Term String) : Env (Term String)

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

Equations

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

def Cvc.Typed.Term.strCharAt [Ω] (s : Term String) (idx : Term Int) : Env (Term String)

The one-character string at an index, or the empty string if out of bounds.

Equations

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

def Cvc.Typed.Term.strToRegex [Ω] (s : Term String) : Env (Term Regex)

The regular expression matching exactly the given string.

Equations

• s.strToRegex = Cvc.Untyped.Term.strToRegex s

def Cvc.Typed.Term.strToInt [Ω] (s : Term String) : Env (Term Int)

Value of a string of digits, or -1 if it is not one.

Equations

• s.strToInt = Cvc.Untyped.Term.strToInt s

def Cvc.Typed.Term.strReplaceAll [Ω] (s pat repl : Term String) : Env (Term String)

Replaces every occurrence of a sub-string.

Equations

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

def Cvc.Typed.Term.strToCode [Ω] (s : Term String) : Env (Term Int)

Code point of a one-character string, or -1 otherwise.

Equations

• s.strToCode = Cvc.Untyped.Term.strToCode s

def Cvc.Typed.Term.strInRegex [Ω] (s : Term String) (re : Term Regex) : Env (Term Bool)

Whether s matches re.

Equations

• s.strInRegex re = Cvc.Untyped.Term.strInRegex s re

def Cvc.Typed.Term.strIsDigit [Ω] (s : Term String) : Env (Term Bool)

Whether the string is a single digit, "0" through "9".

Equations

• s.strIsDigit = Cvc.Untyped.Term.strIsDigit s

def Cvc.Typed.Term.strSuffix [Ω] (suf s : Term String) : Env (Term Bool)

Whether suf is a suffix of s.

Equations

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

def Cvc.Typed.Term.strPrefix [Ω] (pre s : Term String) : Env (Term Bool)

Whether pre is a prefix of s.

Equations

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

def Cvc.Typed.Term.strIndexofRe [Ω] (s : Term String) (re : Term Regex) (start : Term Int) : Env (Term Int)

Index of the first match of re in s at or after start, or -1.

Equations

• s.strIndexofRe re start = Cvc.Untyped.Term.strIndexofRe s re start

def Cvc.Typed.Term.strReplaceRe [Ω] (s : Term String) (re : Term Regex) (repl : Term String) : Env (Term String)

Replaces the first match of a regular expression.

Equations

• s.strReplaceRe re repl = Cvc.Untyped.Term.strReplaceRe s re repl

def Cvc.Typed.Term.strFromInt [Ω] (arg : Term Int) : Env (Term String)

Decimal representation of a non-negative integer, or the empty string otherwise.

Equations

• arg.strFromInt = Cvc.Untyped.Term.strFromInt arg

def Cvc.Typed.Term.strLe [Ω] (lft rgt : Term String) : Env (Term Bool)

Whether lft comes before rgt or equals it, lexicographically over code points.

Equations

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

def Cvc.Typed.Term.strRev [Ω] (s : Term String) : Env (Term String)

Reversal.

Equations

• s.strRev = Cvc.Untyped.Term.strRev s

def Cvc.Typed.Term.strReplaceReAll [Ω] (s : Term String) (re : Term Regex) (repl : Term String) : Env (Term String)

Replaces every match of a regular expression.

Equations

• s.strReplaceReAll re repl = Cvc.Untyped.Term.strReplaceReAll s re repl

def Cvc.Typed.Term.strContains [Ω] (s sub : Term String) : Env (Term Bool)

Whether s contains sub.

Equations

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

def Cvc.Typed.Term.strConcat [Ω] (lft rgt : Term String) : Env (Term String)

Concatenation.

Equations

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

def Cvc.Typed.Term.strToUpper [Ω] (s : Term String) : Env (Term String)

Conversion to upper case.

Equations

• s.strToUpper = Cvc.Untyped.Term.strToUpper s

def Cvc.Typed.Term.strToLower [Ω] (s : Term String) : Env (Term String)

Conversion to lower case.

Equations

• s.strToLower = Cvc.Untyped.Term.strToLower s

def Cvc.Typed.Term.mkString [Ω] (s : String) (useEscapes : Bool) : Env (Term String)

A string literal; with useEscapes, SMT-LIB escapes such as \u{48} in s are decoded.

Equations

• Cvc.Typed.Term.mkString s useEscapes = Cvc.Untyped.Term.mkString s useEscapes

def Cvc.Typed.Term.strFromCode [Ω] (code : Term Int) : Env (Term String)

The one-character string with the given code point, or the empty string if out of range.

Equations

• code.strFromCode = Cvc.Untyped.Term.strFromCode code

def Cvc.Typed.Term.strLt [Ω] (lft rgt : Term String) : Env (Term Bool)

Whether lft comes strictly before rgt, lexicographically over code points.

Equations

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

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

strConcat over two or more terms.

Equations

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

def Cvc.Typed.Term.strLength [Ω] (s : Term String) : Env (Term Int)

Length.

Equations

• s.strLength = Cvc.Untyped.Term.strLength s

def Cvc.Typed.Term.strReplace [Ω] (s pat repl : Term String) : Env (Term String)

Replaces the first occurrence of a sub-string.

Equations

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

def Cvc.Typed.Term.strIndexof [Ω] (s sub : Term String) (start : Term Int) : Env (Term Int)

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

Equations

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

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

Takes a term apart one level, at its sort, if String 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.String.OnRegex [Ω] : Type

String's operators with a result of sort Regex.

• strToRegex [Ω] (s : Term String) : OnRegex

  The regular expression matching exactly the given string.

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

String's operators with a result of sort Bool.

• strContains [Ω] (s sub : Term String) : OnBool

  Whether s contains sub.

• strPrefix [Ω] (pre s : Term String) : OnBool

  Whether pre is a prefix of s.

• strSuffix [Ω] (suf s : Term String) : OnBool

  Whether suf is a suffix of s.

• strIsDigit [Ω] (s : Term String) : OnBool

  Whether the string is a single digit, "0" through "9".

• strLt [Ω] (lft rgt : Term String) : OnBool

  Whether lft comes strictly before rgt, lexicographically over code points.

• strLe [Ω] (lft rgt : Term String) : OnBool

  Whether lft comes before rgt or equals it, lexicographically over code points.

• strInRegex [Ω] (s : Term String) (re : Term Regex) : OnBool

  Whether s matches re.

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

String's operators with a result of sort Int.

• strLength [Ω] (s : Term String) : OnInt

  Length.

• strIndexof [Ω] (s sub : Term String) (start : Term Int) : OnInt

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

• strIndexofRe [Ω] (s : Term String) (re : Term Regex) (start : Term Int) : OnInt

  Index of the first match of re in s at or after start, or -1.

• strToCode [Ω] (s : Term String) : OnInt

  Code point of a one-character string, or -1 otherwise.

• strToInt [Ω] (s : Term String) : OnInt

  Value of a string of digits, or -1 if it is not one.

inductive Cvc.Typed.View.String.OnString [Ω] : Type

String's operators with a result of sort String.

• strConcat [Ω] (kids : Kids String) : OnString

  Concatenation.

  kids holds every operand, two or more.

• strSubstr [Ω] (s : Term String) (idx len : Term Int) : OnString

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

• strCharAt [Ω] (s : Term String) (idx : Term Int) : OnString

  The one-character string at an index, or the empty string if out of bounds.

• strReplace [Ω] (s pat repl : Term String) : OnString

  Replaces the first occurrence of a sub-string.

• strReplaceAll [Ω] (s pat repl : Term String) : OnString

  Replaces every occurrence of a sub-string.

• strReplaceRe [Ω] (s : Term String) (re : Term Regex) (repl : Term String) : OnString

  Replaces the first match of a regular expression.

• strReplaceReAll [Ω] (s : Term String) (re : Term Regex) (repl : Term String) : OnString

  Replaces every match of a regular expression.

• strRev [Ω] (s : Term String) : OnString

  Reversal.

• strUpdate [Ω] (s : Term String) (idx : Term Int) (repl : Term String) : OnString

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

• strToLower [Ω] (s : Term String) : OnString

  Conversion to lower case.

• strToUpper [Ω] (s : Term String) : OnString

  Conversion to upper case.

• strFromCode [Ω] (code : Term Int) : OnString

  The one-character string with the given code point, or the empty string if out of range.

• strFromInt [Ω] (arg : Term Int) : OnString

  Decimal representation of a non-negative integer, or the empty string otherwise.

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

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

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

  An operator with a result of sort Bool.

• string [Ω] : OnString → View.String Typ.string

  An operator with a result of sort String.

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

  An operator with a result of sort Int.

• regex [Ω] : OnRegex → View.String Typ.regex

  An operator with a result of sort Regex.

Values

def Cvc.Typed.Term.isStringValue [Ω] (term : Term String) : Bool

Whether a term is a string value.

Equations

• term.isStringValue = Cvc.Untyped.Term.isStringValue term

def Cvc.Typed.Term.getStringValue [Ω] (term : Term String) : Res String

The string a term denotes, failing if it denotes none.

Equations

• term.getStringValue = Cvc.Untyped.Term.getStringValue term

def Cvc.Typed.Term.getStringValue? [Ω] (term : Term String) : Option String

The string a term denotes, failing if it denotes none.

Equations

• term.getStringValue? = Cvc.Untyped.Term.getStringValue? term

def Cvc.Typed.Term.mkStringValue [Ω] (s : String) : Env (Term String)

The string term denoting s, whatever characters it holds.

Fails on a character beyond cvc5's alphabet, whose code points stop at 0x2FFFF.

Equations

• Cvc.Typed.Term.mkStringValue s = Cvc.Untyped.Term.mkStringValue s

@[instance_reducible]

instance Cvc.Typed.Term.instSrtLikeString : SrtLike String

Equations

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

smt! literals of this theory

A string literal, written as in Lean, is a Term String.