Regular expressions over nullables, sort-erased

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

The regex term becomes nullable. Note the string-matching operators live in the string theory, so strInRe? is generated there.

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

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

Equations

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

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

reInter? over two or more terms.

Equations

• Cvc.Untyped.Term.reInterN? terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.REGEXP_INTER terms

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

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

Equations

• re.reComplement? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.REGEXP_COMPLEMENT #[re]

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

reUnion? over two or more terms.

Equations

• Cvc.Untyped.Term.reUnionN? terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.REGEXP_UNION terms

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

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

Equations

• re.reStar? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.REGEXP_STAR #[re]

def Cvc.Untyped.Term.reRange? [Ω] (lo hi : Term) : Env Term

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

Equations

• lo.reRange? hi = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.REGEXP_RANGE #[lo, hi]

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

reConcat? over two or more terms.

Equations

• Cvc.Untyped.Term.reConcatN? terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.REGEXP_CONCAT terms

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

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

Equations

• re.rePlus? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.REGEXP_PLUS #[re]

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

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

Equations

• re.reOpt? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.REGEXP_OPT #[re]

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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