From e17fba7e393fe2dbff4f328f7afdef28e493ce0f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Jul 2026 12:20:00 -0700 Subject: [PATCH] Document known shady parts in seq_monadic (witness extraction, epsilon/N handling) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 34aa9af0-4977-411d-aaa7-7cb81cc4e9f8 --- src/ast/rewriter/seq_monadic.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 4af73793eb..49144bcb56 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -22,6 +22,20 @@ Author: Nikolaj Bjorner / Margus Veanes 2026 +Shady parts: + +- witness extraction is buggy. It should generally rely on a choice function that takes a + Boolean expression F[(:var 0)] with a single free variable and synthesize a value for the free + variable such that the expression is true. + For character predicates we can assume that the Boolean expressions are range predicates and we can + use utilities for range predicates. For other types use some best effort, say F is of the form (= (:var 0) value). + Expose the witness function in a self-contained module outside of this file. + +- checking intersections with continuation regexes is shady. The nullability check is now really about + whether there is an epsilon transition to the accepting state N. The copilot-generated code ignores this. + Generally, dealing with epsilon state is shady. There are many equivalent ways a state can be epsilon, such + as epsilon*, or comp(.+), etc. + --*/ #include "ast/rewriter/seq_monadic.h"