Docs: regex tag matching

This feels cursed.

docs/examples/tags/alt.log

@@ -0,0 +1,42 @@
+./gen.sh -s alt -t unbounded_hAdX
+$ sby --dumptasks alt.sby
+$ sby --dumptags alt.sby
+known
+liveness
+unbounded
+$ sby --dumptags alt.sby unbounded_hAdX
+\w+_h[AB]d[XY]
+known
+unbounded
+unbounded_h.d.
+$ sby --dumpdefaults alt.sby
+$ sby --dumpcfg alt.sby
+[tasks]
+unbounded_h.d. : unbounded
+liveness_h.d. : liveness
+\w+_h[AB]d[XY] : known
+
+[options]
+
+[engines]
+abc pdr
+aiger suprove
+
+[script]
+
+[files]
+$ sby --dumpcfg alt.sby unbounded_hAdX
+[options]
+mode prove
+
+[engines]
+abc pdr
+
+[script]
+read -sv A.v X.v unbounded.v
+prep -top unbounded
+
+[files]
+unbounded.v
+hostA.v
+deviceX.v

docs/examples/tags/alt.sby

@@ -0,0 +1,38 @@
+[tasks]
+unbounded_h.d. : unbounded
+liveness_h.d. : liveness
+\w+_h[AB]d[XY] : known
+
+[options]
+unbounded: mode prove
+liveness: mode live
+
+[engines]
+~liveness: abc pdr
+~unbounded: aiger suprove
+
+[script]
+--pycode-begin--
+m = re.fullmatch(r'(unbounded|liveness)_h(.)d(.)', task or '')
+if m:
+    top, h, d = m.groups()
+    output(f'read -sv {h}.v {d}.v {top}.v')
+    output(f'prep -top {top}')
+else:
+    assert task is None, f'Invalid task {task!r}'
+--pycode-end--
+
+[files]
+--pycode-begin--
+m = re.fullmatch(r'(\w+)_h(\w)d(\w)', task or '')
+if m:
+    assert 'known' in tags, f'Unknown host/device {task!r}'
+    top, h, d = m.groups()
+    sources = [
+        f"{top}.v",
+        f"host{h}.v",
+        f"device{d}.v",
+    ]
+    for source in sources:
+        output(source)
+--pycode-end--

docs/source/advanced/tags.rst

@@ -107,3 +107,30 @@ generated config does not include any lines that are conditionally enabled
 .. literalinclude:: /../examples/tags/complex.log
    :language: console
    :start-at: dumpcfg
+
+A better way
+~~~~~~~~~~~~
+
+For this particular example, a better approach might be the following:
+
+.. literalinclude:: /../examples/tags/alt.sby
+   :language: sby
+
+This uses regex string matching on the task name, allowing any task to be
+provided in the ``sby`` call that matches at least one task.  This allows for
+all of the same calls, e.g. ``sby alt.sby unbounded_hAdX``, but there are no
+longer any default tasks, so calling ``sby alt.sby`` is no longer valid.
+
+.. warning::
+
+   So long as the provided task matches *any* regex task then SBY will recognize
+   it as valid, opening up the potential for downstream issues where a partially
+   recognized task name is not fully configured.  Extreme care should be taken
+   when using multiple regex tasks.
+
+We use the tag ``known`` here to validate that the host/device implementations
+are valid. This isn't strictly necessary, but it does mean that we can provide
+an error message if an unknown host/device is used, and demonstrates that care
+must be taken when using regex matching.  e.g. without the ``assert task is
+None`` line, a task of ``witness_hAdX`` would provide an error message about
+``mode`` being unset, which may not be immediately obvious as to why that is.