Mirror of upstream AutomataDotNet/Automata#6 ("SFAz3 models seem to have max length 21 characters"), tracking how this fork resolves it and what it builds on top. Four distinct items.
1. The ~21-char witness cap — root cause + fix (DONE)
Not a fundamental length limit. Witness generation died on a NullReferenceException in BDDAlgebra.Choose, from a cross-solver BDD-terminal identity mismatch: RexEngine(BitWidth) builds its own internal CharSetSolver, while the automaton is built by the caller with a separate CharSetSolver. The transition-label BDDs belong to the caller's algebra; the Choose descent compares against the engine solver's True/False terminals (distinct object identities), never reaches a terminal, follows a null child, dereferences null. "21 chars" was just where the divergent walk crashed (the Z3 4.5 → 4.8.1 upgrade shifted the path into the crashing region).
Fix: algebra-identity guard at the top of RexEngine.GenerateMember. Regression test GenerateMember_WitnessOver21Chars_CapIsLifted (witness ≥ 22 for [a-z]{22}). Commit 9e1fb28.
2. .NET 8 modernization (DONE)
- core Framework 4.5 → net8.0 (39f6462)
- tests → net8.0 + MSTest v2, 91/94 green baseline (d2d5e06)
RNGCryptoServiceProvider → RandomNumberGenerator, SYSLIB0023 (40d5b25)- Z3 updated.
3. SMT-LIB 2.6 string-theory bridge to modern Z3 (DONE)
Surface & (1edc3a7), ~ (a9e00c1), wired through automaton + SMT (59d2a3e), RegexToSMTConverter made public (4a7b7f0). RegexToSMTConverter now emits SMT-LIB 2.6 string theory (str.to_re / re.range / re.inter / re.comp / (_ re.loop m n)) consumed by Z3 via ParseSMTLIB2String + str.in_re — sidesteps the product-DFA blowup (#2). Cost moves into Z3's string solver; large conjunctions can return unknown (the real wall, not the cap).
4. End-to-end Sudoku demo (DONE, in CoursIA)
Full notebook: Sudoku as symbolic-regex intersection → Z3 generates the grid — jsboige/CoursIA#3136. Standalone SMT mechanism: jsboige/CoursIA#3130. Brzozowski-derivative finiteness (linear-time recognition) formalized in Lean: jsboige/CoursIA#3018.
Status
Cap-fix kept (genuine NRE fix; the scaling wall is the product-DFA path, bypassed by item 3). Full write-up: jsboige/CoursIA#2979. To be closed alongside the upstream AutomataDotNet#6 closing comment.
Mirror of upstream AutomataDotNet/Automata#6 ("SFAz3 models seem to have max length 21 characters"), tracking how this fork resolves it and what it builds on top. Four distinct items.
1. The ~21-char witness cap — root cause + fix (DONE)
Not a fundamental length limit. Witness generation died on a
NullReferenceExceptioninBDDAlgebra.Choose, from a cross-solver BDD-terminal identity mismatch:RexEngine(BitWidth)builds its own internalCharSetSolver, while the automaton is built by the caller with a separateCharSetSolver. The transition-label BDDs belong to the caller's algebra; theChoosedescent compares against the engine solver's True/False terminals (distinct object identities), never reaches a terminal, follows a null child, dereferences null. "21 chars" was just where the divergent walk crashed (the Z3 4.5 → 4.8.1 upgrade shifted the path into the crashing region).Fix: algebra-identity guard at the top of
RexEngine.GenerateMember. Regression testGenerateMember_WitnessOver21Chars_CapIsLifted(witness ≥ 22 for[a-z]{22}). Commit 9e1fb28.2. .NET 8 modernization (DONE)
RNGCryptoServiceProvider→RandomNumberGenerator, SYSLIB0023 (40d5b25)3. SMT-LIB 2.6 string-theory bridge to modern Z3 (DONE)
Surface
&(1edc3a7),~(a9e00c1), wired through automaton + SMT (59d2a3e),RegexToSMTConvertermade public (4a7b7f0).RegexToSMTConverternow emits SMT-LIB 2.6 string theory (str.to_re/re.range/re.inter/re.comp/(_ re.loop m n)) consumed by Z3 viaParseSMTLIB2String+str.in_re— sidesteps the product-DFA blowup (#2). Cost moves into Z3's string solver; large conjunctions can returnunknown(the real wall, not the cap).4. End-to-end Sudoku demo (DONE, in CoursIA)
Full notebook: Sudoku as symbolic-regex intersection → Z3 generates the grid — jsboige/CoursIA#3136. Standalone SMT mechanism: jsboige/CoursIA#3130. Brzozowski-derivative finiteness (linear-time recognition) formalized in Lean: jsboige/CoursIA#3018.
Status
Cap-fix kept (genuine NRE fix; the scaling wall is the product-DFA path, bypassed by item 3). Full write-up: jsboige/CoursIA#2979. To be closed alongside the upstream AutomataDotNet#6 closing comment.