Strings over nullables, sort-erased

One lifted constructor per liftable operator, <id>?, each answering none unless every argument is some.

The indexed operators do not lift, for the reason bit-vectors' do not: an Op cannot be handed to mkNullableLift.

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

strIsDigit lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strCharAt lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strToRegex lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strLength lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strConcat lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strPrefix lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strLt lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strReplaceRe lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strUpdate lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strToLower lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strSuffix lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strFromCode lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strToCode lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strToInt lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strToUpper lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strInRegex lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strLe lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strSubstr lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strFromInt lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strReplaceReAll lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strReplaceAll lifted over nullables, strictly: none unless every argument is some.

Equations

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

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.mkNullableLift cvc5.Kind.STRING_CONCAT terms

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

strContains lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strRev lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strIndexof lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strReplace lifted over nullables, strictly: none unless every argument is some.

Equations

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

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

strIndexofRe lifted over nullables, strictly: none unless every argument is some.

Equations

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