theorem
Regex.Backtracker.captureNext_soundness
{s : String}
{e : Data.Expr}
{bufferSize : ℕ}
{pos : s.ValidPos}
{matchedB : (BufferStrategy s bufferSize).Update}
(disj : e.Disjoint)
(hresB : captureNext (BufferStrategy s bufferSize) (NFA.compile e) ⋯ pos = some matchedB)
:
∃ (pos' : s.ValidPos) (pos'' : s.ValidPos) (groups : Data.CaptureGroups s),
pos ≤ pos' ∧ Data.Expr.Captures pos' pos'' groups e ∧ Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups groups) matchedB
theorem
Regex.Backtracker.captureNext_completeness'
{s : String}
{e : Data.Expr}
{bufferSize : ℕ}
{pos : s.ValidPos}
(hresB : captureNext (BufferStrategy s bufferSize) (NFA.compile e) ⋯ pos = none)
(pos' pos'' : s.ValidPos)
(groups : Data.CaptureGroups s)
(le : pos ≤ pos')
(c : Data.Expr.Captures pos' pos'' groups e)
:
theorem
Regex.Backtracker.captureNext_completeness
{s : String}
{e : Data.Expr}
{bufferSize : ℕ}
{pos : s.ValidPos}
(hresB : captureNext (BufferStrategy s bufferSize) (NFA.compile e) ⋯ pos = none)
:
¬∃ (pos' : s.ValidPos) (pos'' : s.ValidPos) (groups : Data.CaptureGroups s),
pos ≤ pos' ∧ Data.Expr.Captures pos' pos'' groups e
def
Regex.Backtracker.decideSearchProblem
{s : String}
(e : Data.Expr)
(pos : s.ValidPos)
(disj : e.Disjoint)
:
Equations
- One or more equations did not get rendered due to their size.