Matching SMT-LIB regular expressions

Regular expressions with their SMT-LIB meaning, and a matcher for literal strings. Matching takes the derivative of the expression by each character in turn (Brzozowski's method) and checks whether the rest accepts the empty string. For example, the derivative of "ab" ++ c* by a and then b is c*, which accepts the empty string, so "ab" matches.

inductive Strata.SMT.Regex.Re : Type

A regular expression over the SMT-LIB string alphabet.

• none : Re

  re.none: no string.

• all : Re

  re.all: every string.

• allChar : Re

  re.allchar: every string of one character.

• str (s : List Char) : Re

  str.to_re s: the string s.

• range (lo hi : Char) : Re

  re.range with single-character bounds.

• cat (a b : Re) : Re

  re.++

• union (a b : Re) : Re

  re.union

• inter (a b : Re) : Re

  re.inter

• star (a : Re) : Re

  re.*

• comp (a : Re) : Re

  re.comp: the complement of a.

• loop (a : Re) (lo hi : Nat) : Re

  re.loop: lo to hi repetitions of a; no string when lo > hi.

@[instance_reducible]

instance Strata.SMT.Regex.instDecidableEqRe : DecidableEq Re

Equations

• Strata.SMT.Regex.instDecidableEqRe = Strata.SMT.Regex.instDecidableEqRe.decEq

def Strata.SMT.Regex.instDecidableEqRe.decEq (x✝ x✝¹ : Re) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Strata.SMT.Regex.instOrdRe : Ord Re

Equations

• Strata.SMT.Regex.instOrdRe = { compare := Strata.SMT.Regex.instOrdRe.ord }

partial def Strata.SMT.Regex.instOrdRe.ord : Re → Re → Ordering

@[instance_reducible]

instance Strata.SMT.Regex.instInhabitedRe : Inhabited Re

Equations

• Strata.SMT.Regex.instInhabitedRe = { default := Strata.SMT.Regex.instInhabitedRe.default }

@[instance_reducible]

instance Strata.SMT.Regex.instReprRe : Repr Re

Equations

• Strata.SMT.Regex.instReprRe = { reprPrec := Strata.SMT.Regex.instReprRe.repr }

def Strata.SMT.Regex.instReprRe.repr : Re → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Strata.SMT.Regex.instReprRe.repr Strata.SMT.Regex.Re.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.SMT.Regex.Re.none")).group prec✝
• Strata.SMT.Regex.instReprRe.repr Strata.SMT.Regex.Re.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Strata.SMT.Regex.Re.all")).group prec✝

def Strata.SMT.Regex.maxSize : Nat

The node count above which matches? gives no answer.

Equations

• Strata.SMT.Regex.maxSize = 10000

def Strata.SMT.Regex.Re.ofRange (lo hi : String) : Re

re.range of two strings: the characters between them when both have one character, and no string otherwise.

Equations

• Strata.SMT.Regex.Re.ofRange lo hi = match lo.toList, hi.toList with | [l], [h] => Strata.SMT.Regex.Re.range l h | x, x_1 => Strata.SMT.Regex.Re.none

def Strata.SMT.Regex.Re.plus (a : Re) : Re

re.+: one or more repetitions.

Equations

• a.plus = a.cat a.star

def Strata.SMT.Regex.Re.sizeLe (n : Nat) (r : Re) : Bool

Whether r has at most n nodes. Counting stops once it passes n, so the check is cheap even on a tree with shared subterms, such as nested plus.

Equations

• Strata.SMT.Regex.Re.sizeLe n r = (Strata.SMT.Regex.Re.sizeLe.go✝ n r).isSome

def Strata.SMT.Regex.Re.mkCat : Re → Re → Re

Concatenation, simplified when a side is none or the empty string.

Equations

• Strata.SMT.Regex.Re.none.mkCat x✝ = Strata.SMT.Regex.Re.none
• x✝.mkCat Strata.SMT.Regex.Re.none = Strata.SMT.Regex.Re.none
• (Strata.SMT.Regex.Re.str []).mkCat x✝ = x✝
• x✝.mkCat (Strata.SMT.Regex.Re.str []) = x✝
• x✝¹.mkCat x✝ = x✝¹.cat x✝

def Strata.SMT.Regex.Re.alts : Re → List Re

The alternatives of r, with nested unions flattened.

Equations

• (a.union b).alts = a.alts ++ b.alts
• x✝.alts = [x✝]

@[irreducible]

def Strata.SMT.Regex.Re.dedupAdjacent : List Re → List Re

rs with each element equal to the one before it removed.

Equations

• Strata.SMT.Regex.Re.dedupAdjacent (a :: b :: tail) = if a = b then Strata.SMT.Regex.Re.dedupAdjacent (b :: tail) else a :: Strata.SMT.Regex.Re.dedupAdjacent (b :: tail)
• Strata.SMT.Regex.Re.dedupAdjacent x✝ = x✝

def Strata.SMT.Regex.Re.ofAlts : List Re → Re

The union of rs, nested to the right, or none when rs is empty.

Equations

• Strata.SMT.Regex.Re.ofAlts [] = Strata.SMT.Regex.Re.none
• Strata.SMT.Regex.Re.ofAlts [a] = a
• Strata.SMT.Regex.Re.ofAlts (a :: rs) = a.union (Strata.SMT.Regex.Re.ofAlts rs)

def Strata.SMT.Regex.Re.mkUnion (a b : Re) : Re

Union, normalized: the alternatives of both sides are sorted, with repeats and none removed, and the union is all when one of them is. This keeps derivatives small: those of re.all ++ "a" ++ re.all by each character would otherwise grow with the length of the string. A union of more than maxSize nodes is left as is, so the sort never runs on a large term; matches? gives up on a derivative that contains it.

Equations

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

def Strata.SMT.Regex.Re.mkInter : Re → Re → Re

Intersection, which is none when either side is.

Equations

• Strata.SMT.Regex.Re.none.mkInter x✝ = Strata.SMT.Regex.Re.none
• x✝.mkInter Strata.SMT.Regex.Re.none = Strata.SMT.Regex.Re.none
• x✝¹.mkInter x✝ = x✝¹.inter x✝

def Strata.SMT.Regex.Re.nullable : Re → Bool

Whether r matches the empty string.

Equations

• Strata.SMT.Regex.Re.none.nullable = false
• Strata.SMT.Regex.Re.allChar.nullable = false
• (Strata.SMT.Regex.Re.range lo hi).nullable = false
• Strata.SMT.Regex.Re.all.nullable = true
• a.star.nullable = true
• (Strata.SMT.Regex.Re.str s).nullable = s.isEmpty
• (a.cat b).nullable = (a.nullable && b.nullable)
• (a.union b).nullable = (a.nullable || b.nullable)
• (a.inter b).nullable = (a.nullable && b.nullable)
• a.comp.nullable = !a.nullable
• (a.loop lo hi).nullable = (decide (lo ≤ hi) && (lo == 0 || a.nullable))

def Strata.SMT.Regex.Re.derivNullable (c : Char) : Re → Re × Bool

The derivative of r by c, the strings s such that r matches c :: s, and whether r is nullable. Computing both in one pass avoids recomputing nullable at every cat.

Equations

• One or more equations did not get rendered due to their size.
• Strata.SMT.Regex.Re.derivNullable c Strata.SMT.Regex.Re.none = (Strata.SMT.Regex.Re.none, false)
• Strata.SMT.Regex.Re.derivNullable c Strata.SMT.Regex.Re.all = (Strata.SMT.Regex.Re.all, true)
• Strata.SMT.Regex.Re.derivNullable c Strata.SMT.Regex.Re.allChar = (Strata.SMT.Regex.Re.str [], false)
• Strata.SMT.Regex.Re.derivNullable c (Strata.SMT.Regex.Re.str []) = (Strata.SMT.Regex.Re.none, true)
• Strata.SMT.Regex.Re.derivNullable c (Strata.SMT.Regex.Re.str (d :: s)) = (if (c == d) = true then Strata.SMT.Regex.Re.str s else Strata.SMT.Regex.Re.none, false)
• Strata.SMT.Regex.Re.derivNullable c (Strata.SMT.Regex.Re.range lo hi) = (if (decide (lo ≤ c) && decide (c ≤ hi)) = true then Strata.SMT.Regex.Re.str [] else Strata.SMT.Regex.Re.none, false)
• Strata.SMT.Regex.Re.derivNullable c a.star = ((Strata.SMT.Regex.Re.derivNullable c a).fst.mkCat a.star, true)
• Strata.SMT.Regex.Re.derivNullable c a.comp = match Strata.SMT.Regex.Re.derivNullable c a with | (da, na) => (da.comp, !na)

def Strata.SMT.Regex.matches? (r : Re) (s : String) : Option Bool

Whether r matches s, or none when r or a derivative has more than maxSize nodes or s has a character outside the SMT-LIB alphabet.

Equations

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