From b0a4a15c9818ceefefb7ed1c8bae728c5f848c0a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2026 10:03:29 -0700 Subject: [PATCH] updated tests Signed-off-by: Nikolaj Bjorner --- specbot/test_deeptest_seq.c | 49 ++++++++++++++----- specbot/test_specbot_seq.c | 46 ++++++++++++++---- src/smt/seq/seq_nielsen.cpp | 97 ++++++++++++------------------------- 3 files changed, 106 insertions(+), 86 deletions(-) diff --git a/specbot/test_deeptest_seq.c b/specbot/test_deeptest_seq.c index e310b9068..2a6dff6ed 100644 --- a/specbot/test_deeptest_seq.c +++ b/specbot/test_deeptest_seq.c @@ -20,15 +20,15 @@ #include #include #include - -#ifdef _WIN32 -#include -#include #include static jmp_buf jmp_env; static volatile int in_test = 0; +#ifdef _WIN32 +#include +#include + void abort_handler(int sig) { (void)sig; if (in_test) { @@ -50,13 +50,6 @@ void suppress_dialogs() { _set_abort_behavior(0, _WRITE_ABORT_MSG | _CALL_REPORTFAULT); signal(SIGABRT, abort_handler); } -#else -void suppress_dialogs() {} -#endif - -static int tests_run = 0; -static int tests_passed = 0; -static int tests_crashed = 0; #define RUN_TEST(name) do { \ fprintf(stderr, "[TEST] Running %s\n", #name); \ @@ -79,6 +72,40 @@ static int tests_crashed = 0; } \ } while(0) +#else + +void abort_handler(int sig) { + (void)sig; + if (in_test) { + in_test = 0; + signal(SIGABRT, abort_handler); + longjmp(jmp_env, 1); + } +} + +void suppress_dialogs() { signal(SIGABRT, abort_handler); } + +#define RUN_TEST(name) do { \ + fprintf(stderr, "[TEST] Running %s\n", #name); \ + tests_run++; \ + in_test = 1; \ + if (setjmp(jmp_env) == 0) { \ + name(); \ + in_test = 0; \ + tests_passed++; \ + fprintf(stderr, "[TEST] PASS %s\n", #name); \ + } else { \ + tests_crashed++; \ + fprintf(stderr, "[TEST] ABORT %s (caught SIGABRT)\n", #name); \ + } \ +} while(0) + +#endif + +static int tests_run = 0; +static int tests_passed = 0; +static int tests_crashed = 0; + /* ===== Helpers ===== */ static Z3_sort mk_string_sort(Z3_context ctx) { return Z3_mk_string_sort(ctx); } static Z3_ast mk_str(Z3_context ctx, const char* s) { return Z3_mk_string(ctx, s); } diff --git a/specbot/test_specbot_seq.c b/specbot/test_specbot_seq.c index 9b8a4c735..17a725371 100644 --- a/specbot/test_specbot_seq.c +++ b/specbot/test_specbot_seq.c @@ -4,15 +4,15 @@ #include #include - -#ifdef _WIN32 -#include -#include #include static jmp_buf jmp_env; static volatile int in_test = 0; +#ifdef _WIN32 +#include +#include + void abort_handler(int sig) { (void)sig; if (in_test) { @@ -34,12 +34,6 @@ void suppress_dialogs() { _set_abort_behavior(0, _WRITE_ABORT_MSG | _CALL_REPORTFAULT); signal(SIGABRT, abort_handler); } -#else -void suppress_dialogs() {} -#endif - -static int tests_run = 0; -static int tests_passed = 0; #define RUN_TEST(name) do { \ fprintf(stderr, "[TEST] Running %s\n", #name); \ @@ -60,6 +54,38 @@ static int tests_passed = 0; } \ } while(0) +#else + +void abort_handler(int sig) { + (void)sig; + if (in_test) { + in_test = 0; + signal(SIGABRT, abort_handler); + longjmp(jmp_env, 1); + } +} + +void suppress_dialogs() { signal(SIGABRT, abort_handler); } + +#define RUN_TEST(name) do { \ + fprintf(stderr, "[TEST] Running %s\n", #name); \ + tests_run++; \ + in_test = 1; \ + if (setjmp(jmp_env) == 0) { \ + name(); \ + in_test = 0; \ + tests_passed++; \ + fprintf(stderr, "[TEST] PASS %s\n", #name); \ + } else { \ + fprintf(stderr, "[TEST] ABORT %s (caught SIGABRT)\n", #name); \ + } \ +} while(0) + +#endif + +static int tests_run = 0; +static int tests_passed = 0; + /* Helper to create string sort, variables, constants */ Z3_sort mk_string_sort(Z3_context ctx) { return Z3_mk_string_sort(ctx); } Z3_ast mk_string_var(Z3_context ctx, const char* name) { diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index b86f110fc..218c3789f 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1125,80 +1125,41 @@ namespace seq { } } - // consume symbolic characters (s_unit tokens) via uniform derivative - // check. When all minterms of the regex produce the same Brzozowski - // derivative, the derivative is independent of the character value - // and we can deterministically consume the token. Forward direction - // only (matches ZIPT history tracking convention). - // - // Extended: when uniform derivative fails but the token has a char_range - // constraint (from apply_regex_var_split), check if the char_range is a - // subset of a single minterm's character class. If so, the derivative - // is deterministic for that token. - // Mirrors ZIPT StrMem.SimplifyCharRegex lines 96-117. + // consume symbolic characters via uniform derivatives for (str_mem& mem : m_str_mem) { SASSERT(mem.m_str && mem.m_regex); if (mem.is_primitive()) continue; while (mem.m_str && !mem.m_str->is_empty()) { - euf::snode* tok = mem.m_str->first(); - if (!tok || !tok->is_unit()) + + // TODO: generalize this to work for reverse derivative as well. + euf::snode *tok = mem.m_str->first(); + if (!tok || !tok->is_char_or_unit()) break; - // - // TODO -rewrite to use symbolic derivative and add back resulting derived regex. - // + seq_rewriter rw(m); + expr_ref d(rw.mk_derivative(mem.m_regex->get_expr()), m); - // compute minterms and check for uniform derivative - euf::snode_vector minterms; - sg.compute_minterms(mem.m_regex, minterms); - VERIFY(!minterms.empty()); - // try char_range subset approach. - // If the symbolic char has a char_range constraint and that - // range is a subset of exactly one minterm's character class, - // we can deterministically take that minterm's derivative. - SASSERT(m_graph.m_parikh); - auto full = char_set::full(zstring::max_char()); - char_set* cs; - dep_tracker dep; - if (m_char_ranges.contains(tok->id())) { - auto& ranges = m_char_ranges[tok->id()]; - cs = &ranges.first; - dep = ranges.second; - } - else { - cs = &full; - dep = graph().dep_mgr().mk_empty(); + // Extract the inner char expression from seq.unit(?inner) + expr *unit_expr = tok->arg(0)->get_expr(), *inner_char; + + // substitute the inner char for the derivative variable in d + var_subst vs(m); + d = vs(d, inner_char); + + th_rewriter thrw(m); + thrw(d); + + auto next = sg.mk(d); + if (next->is_fail()) { + m_is_general_conflict = true; + set_conflict(backtrack_reason::regex, mem.m_dep); + return simplify_result::conflict; } - if (!cs->is_empty()) { - euf::snode* matching_deriv = nullptr; - bool found = false; - for (euf::snode* mt : minterms) { - SASSERT(mt && mt->get_expr()); - SASSERT(!mt->is_fail()); - char_set mt_cs = m_graph.m_seq_regex->minterm_to_char_set(mt->get_expr()); - if (cs->is_subset(mt_cs)) { - euf::snode* deriv = sg.brzozowski_deriv(mem.m_regex, mt); - if (!deriv) { found = false; break; } - if (deriv->is_fail()) { - m_is_general_conflict = true; - set_conflict(backtrack_reason::regex, graph().dep_mgr().mk_join(mem.m_dep, dep)); - return simplify_result::conflict; - } - matching_deriv = deriv; - found = true; - break; - } - } - if (found && matching_deriv) { - mem.m_str = sg.drop_left(mem.m_str, 1); - mem.m_regex = matching_deriv; - mem.m_history = sg.mk_concat(mem.m_history, tok); - continue; - } - } - break; + mem.m_str = sg.drop_left(mem.m_str, 1); + mem.m_regex = next; + mem.m_history = sg.mk_concat(mem.m_history, tok); } } @@ -3140,12 +3101,13 @@ namespace seq { } return false; } - + bool nielsen_graph::apply_regex_unit_split(nielsen_node *node) { for (str_mem const &mem : node->str_mems()) { SASSERT(mem.m_str && mem.m_regex); if (mem.is_primitive()) continue; + euf::snode *first = mem.m_str->first(); if (!first || !first->is_char_or_unit()) continue; @@ -3272,6 +3234,11 @@ namespace seq { created = true; } + // TODO: replace this with a version that just uses symbolic derivatives + // and not min-terms. + // It solves x -> unit(nth(x, 0)) ++ x + // Then the split_regex_unit can solve process the node further. + // Branch 2+: for each minterm m_i, x → ?c · x // where ?c is a symbolic char constrained by the minterm for (euf::snode* mt : minterms) {