From d77e9d5c9547eea8238616c6a4f868bb4a71cb0c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Mar 2026 00:26:57 -0700 Subject: [PATCH] add code review comment Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_regex.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/smt/seq/seq_regex.cpp b/src/smt/seq/seq_regex.cpp index 537b38c6a..b867e731a 100644 --- a/src/smt/seq/seq_regex.cpp +++ b/src/smt/seq/seq_regex.cpp @@ -16,10 +16,18 @@ Author: --*/ #include "smt/seq/seq_regex.h" -#include namespace seq { + // NSB code review: change the stabilizers set to + // add the regexes in the domain of m_stabilizers to a trail (expr_ref_vector + // change the range to be a vector of expressions, not snodes + // add regexes in the range of m_stabilizers to the trail + // this is to ensure that the expressions are valid also after scope changes. + // maybe all regexes entered are created at base level for quantifier free formulas + // but we should not assume this. The sgraph also can change based on scope. + // the Stabilizer data-structure persists across search. + // Collect possible first characters of a syntactically known *string* // expression (the body of to_re). Regex operators (union, complement, // intersection, ...) are not expected here.