Generated String constructors, sort-erased

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

Whether s matches re.

Equations

• s.strInRegex re = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.STRING_IN_REGEXP #[s, re]

def Cvc.Untyped.Term.strReplaceReAll [Ω] (s re repl : Term) : Env Term

Replaces every match of a regular expression.

Equations

• s.strReplaceReAll re repl = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.STRING_REPLACE_RE_ALL #[s, re, repl]

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

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

Equations

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

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

Reversal.

Equations

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

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

Whether s contains sub.

Equations

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

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

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

Equations

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

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

Replaces every occurrence of a sub-string.

Equations

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

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

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

Equations

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

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

Whether suf is a suffix of s.

Equations

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

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

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

Equations

• Cvc.Untyped.Term.mkString s useEscapes = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkString s useEscapes

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

Whether pre is a prefix of s.

Equations

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

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

Conversion to lower case.

Equations

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

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

Replaces the first occurrence of a sub-string.

Equations

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

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

Concatenation.

Equations

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

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

strConcat over two or more terms.

Equations

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

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

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

Equations

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

def Cvc.Untyped.Term.strReplaceRe [Ω] (s re repl : Term) : Env Term

Replaces the first match of a regular expression.

Equations

• s.strReplaceRe re repl = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.STRING_REPLACE_RE #[s, re, repl]

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

Length.

Equations

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

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

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

Equations

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

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

The regular expression matching exactly the given string.

Equations

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

def Cvc.Untyped.Term.strIndexofRe [Ω] (s re start : Term) : Env Term

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

Equations

• s.strIndexofRe re start = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.STRING_INDEXOF_RE #[s, re, start]

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

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

Equations

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

def Cvc.Untyped.Term.strFromInt [Ω] (arg : Term) : Env Term

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

Equations

• arg.strFromInt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.STRING_FROM_INT #[arg]

def Cvc.Untyped.Term.strFromCode [Ω] (code : Term) : Env Term

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

Equations

• code.strFromCode = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.STRING_FROM_CODE #[code]

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Conversion to upper case.

Equations

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

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

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

Equations

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

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

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

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

  Whether s contains sub.

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

  Whether pre is a prefix of s.

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

  Whether suf is a suffix of s.

• strIsDigit [Ω] (s : Term) : View.String

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

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

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

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

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

• strInRegex [Ω] (s re : Term) : View.String

  Whether s matches re.

• strConcat [Ω] (kids : Kids) : View.String

  Concatenation.

  kids holds every operand, two or more.

• strLength [Ω] (s : Term) : View.String

  Length.

• strSubstr [Ω] (s idx len : Term) : View.String

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

• strCharAt [Ω] (s idx : Term) : View.String

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

• strIndexof [Ω] (s sub start : Term) : View.String

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

• strIndexofRe [Ω] (s re start : Term) : View.String

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

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

  Replaces the first occurrence of a sub-string.

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

  Replaces every occurrence of a sub-string.

• strReplaceRe [Ω] (s re repl : Term) : View.String

  Replaces the first match of a regular expression.

• strReplaceReAll [Ω] (s re repl : Term) : View.String

  Replaces every match of a regular expression.

• strRev [Ω] (s : Term) : View.String

  Reversal.

• strUpdate [Ω] (s idx repl : Term) : View.String

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

• strToLower [Ω] (s : Term) : View.String

  Conversion to lower case.

• strToUpper [Ω] (s : Term) : View.String

  Conversion to upper case.

• strToCode [Ω] (s : Term) : View.String

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

• strFromCode [Ω] (code : Term) : View.String

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

• strToInt [Ω] (s : Term) : View.String

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

• strFromInt [Ω] (arg : Term) : View.String

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

• strToRegex [Ω] (s : Term) : View.String

  The regular expression matching exactly the given string.

Values

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

Whether a term is a string value.

Equations

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

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

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

Equations

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

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

The string term denoting s, whatever characters it holds.

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

Equations

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

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

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

Equations

• term.getStringValue? = Except.toOption term.getStringValue

@[instance_reducible]

instance Cvc.Untyped.Term.instSrtLikeString : SrtLike String

Equations

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

smt! literals

String literals in smt!. Without this module smt! accepts none.

def Cvc.Untyped.Term.smtStr : Lean.ParserDescr

String literal.

Equations

• Cvc.Untyped.Term.smtStr = Lean.ParserDescr.node `Cvc.Untyped.Term.smtStr 1024 (Lean.ParserDescr.const `str)