diff --git a/specbot/SPECBOT_REPORT.md b/specbot/SPECBOT_REPORT.md deleted file mode 100644 index 8c65f9b14..000000000 --- a/specbot/SPECBOT_REPORT.md +++ /dev/null @@ -1,317 +0,0 @@ -# SpecBot Report: Z3 c3 Branch — Sequence Solver (`src/smt/seq/`) - -> **Target module:** `z3-c3/src/smt/seq/` -> **Repository:** [Z3Prover/z3](https://github.com/Z3Prover/z3) branch `c3` commit `6e8c201` -> **Files analyzed:** `seq_nielsen.h/cpp`, `seq_state.h/cpp`, `seq_regex.h/cpp`, `seq_parikh.h/cpp` -> **Date:** 2026-04-02 -> **Methodology:** Runtime-validated — 34 assertions (4 inv + 12 pre + 18 post) instrumented -> into `seq_nielsen.cpp`, rebuilt, and exercised via three test suites: -> 1. **Z3's own tests** (`test-z3.exe`): `nseq_basic` ✅, `seq_regex` ✅, `seq_parikh` ✅, `nseq_zipt` ❌ stack overflow, `seq_nielsen` ❌ assertion violation -> 2. **Specbot co-generated** (`test_specbot_seq.c`): 16 tests (13 pass, 3 crash) -> 3. **DeepTest-generated** (`test_deeptest_seq.c`): 49 tests (36 pass, 13 crash) -> -> **Results:** 34 assertions, ~5,000 checks, **1 suspect** (`post_solve_sat_path_nonempty` 33% pass rate from Z3's own tests), 16 crash-triggering tests, 2 Z3-internal test failures. - ---- - -## 1. Module Overview - -The `src/smt/seq/` directory implements a **Nielsen-transformation–based string constraint solver** for Z3, ported from the [ZIPT](https://github.com/CEisenhofer/ZIPT) system. The solver builds a search graph of constraint states connected by substitutions and decides satisfiability of conjunctions of string equalities (`str_eq`) and regex membership constraints (`str_mem`) using depth-bounded DFS with iterative deepening. - -### 1.1 Core Classes and Structs - -| Class/Struct | File | Description | -|---|---|---| -| `str_eq` | `seq_nielsen.h:368` | String equality constraint `lhs = rhs`. Both sides are `euf::snode*` trees (DAGs of string tokens). Carries a `dep_tracker` for conflict explanation. | -| `str_mem` | `seq_nielsen.h:394` | Regex membership constraint `str ∈ regex`. Carries derivation history (`m_history`) for cycle detection, a unique `m_id`, and `dep_tracker`. | -| `nielsen_subst` | `seq_nielsen.h:423` | Variable substitution `var → replacement`. `m_var` may be `s_var`, `s_power`, or `s_unit`. Carries `dep_tracker`. | -| `char_subst` | `seq_nielsen.h:347` | Character-level substitution mapping a symbolic `s_unit` to a concrete `s_char` or another `s_unit`. | -| `constraint` | `seq_nielsen.h:455` | Integer arithmetic constraint (equality, inequality, or disequality) stored per node. Wraps an `expr_ref` formula and `dep_tracker`. | -| `length_constraint` | `seq_nielsen.h:475` | Arithmetic length constraint derived from string equalities (e.g., `len(lhs) = len(rhs)`). Has a `length_kind` tag. | -| `nielsen_edge` | `seq_nielsen.h:491` | Edge in the Nielsen graph connecting two `nielsen_node`s. Carries substitutions, side constraints, and a progress flag. | -| `nielsen_node` | `seq_nielsen.h:526` | Node in the Nielsen graph. Holds the current constraint set (`str_eq`, `str_mem`, `constraint`), outgoing edges, backtrack state (reason, conflict flags), character constraints, and regex occurrence tracking. | -| `nielsen_graph` | `seq_nielsen.h:749` | The top-level Nielsen transformation graph. Owns all nodes and edges. Manages the search (iterative-deepening DFS), the arithmetic subsolver interface, Parikh filter, regex module, and modification counters. | -| `simple_solver` | `seq_nielsen.h:274` | Abstract interface for an incremental arithmetic subsolver. Provides `check()`, `assert_expr()`, `push()`/`pop()`, and optional bound queries. | -| `nielsen_stats` | `seq_nielsen.h:716` | Accumulated search statistics (solve calls, DFS nodes, modifier counts, etc.). | -| `tracked_str_eq` | `seq_state.h:30` | Extends `str_eq` with SMT-layer `enode*` pair for conflict reporting. | -| `tracked_str_mem` | `seq_state.h:36` | Extends `str_mem` with a `sat::literal` for conflict reporting. | -| `seq_regex` | `seq_regex.h:40` | Regex membership processing: stabilizer store, Brzozowski derivatives, emptiness checks, cycle detection, self-stabilizing propagation. Wraps `euf::sgraph`. | -| `seq_parikh` | `seq_parikh.h:62` | Parikh image filter: computes length stride of regex languages and generates modular arithmetic constraints (`len(str) = min_len + stride·k`). | - -### 1.2 Key Relationships - -``` -nielsen_graph - ├── owns: ptr_vector (all nodes) - ├── owns: ptr_vector (all edges) - ├── owns: seq_parikh* (Parikh filter) - ├── owns: seq_regex* (regex module) - ├── refs: simple_solver& m_solver (arithmetic subsolver, not owned) - ├── refs: simple_solver& m_core_solver - ├── refs: euf::sgraph& m_sg (string graph, not owned) - └── refs: seq_util& m_seq - -nielsen_node - ├── refs: nielsen_graph& m_graph (back-pointer to owning graph) - ├── has: vector (string equalities) - ├── has: vector (regex memberships) - ├── has: vector (integer constraints) - ├── has: ptr_vector (outgoing edges, not owned) - └── refs: nielsen_node* m_backedge (optional back-edge for cycle) - -nielsen_edge - ├── refs: nielsen_node* m_src (source node, not owned) - ├── refs: nielsen_node* m_tgt (target node, not owned) - ├── has: vector (substitutions) - └── has: vector (side constraints) - -seq_regex - ├── refs: euf::sgraph& m_sg - ├── has: u_map> m_stabilizers - └── has: uint_set m_self_stabilizing - -seq_parikh - ├── refs: ast_manager& m - ├── has: seq_util, arith_util - └── has: unsigned m_fresh_cnt -``` - -### 1.3 Enum Types - -| Enum | Values | Description | -|---|---|---| -| `simplify_result` | `proceed`, `conflict`, `satisfied`, `restart`, `restart_and_satisfied` | Outcome of constraint simplification at a node. | -| `backtrack_reason` | `unevaluated`, `extended`, `symbol_clash`, `parikh_image`, `subsumption`, `arithmetic`, `regex`, `regex_widening`, `character_range`, `smt`, `external`, `children_failed` | Why a node was backtracked from. | -| `search_result` | `sat`, `unsat`, `unknown` | Outcome of solve()/search_dfs(). | -| `length_kind` | `nonneg`, `eq`, `bound` | Type of arithmetic length constraint. | - ---- - -## 2. Specification Catalog - -All specifications are runtime-validated. Checks column shows Z3 tests / Specbot / DeepTest / Total. - -### Suspect - -| ID | Kind | Scope | Expression | Z3 | Specbot | DeepTest | Total | Pass Rate | -|---|---|---|---|---|---|---|---|---| -| `post_solve_sat_path_nonempty` | post | `nielsen_graph::solve()` → SAT | `!m_sat_path.empty()` | **1/3** | 5 | 15 | 21/23 | **91%** | - -Z3's `nseq_basic` test triggers SAT results where `m_sat_path` is empty — the solver returns SAT but doesn't populate the solution path. This may indicate a code path where `solve()` returns SAT via simplification (root satisfied without search) rather than DFS, skipping path construction. - -### 2.1 `str_eq` - -| ID | Kind | Scope | Expression | Z3 | Specbot | DeepTest | Total | -|---|---|---|---|---|---|---|---| -| `inv_eq_nonnull` | inv | `str_eq` (all public methods) | `[&]{ for (auto const& eq : m_str_eq) if (!eq.m_lhs \|\| !eq.m_rhs) return false; return true; }()` | 8 | 16 | 114 | 138 | -| `inv_no_trivial_eq` | inv | `str_eq` (after simplify) | `[&]{ for (auto const& eq : m_str_eq) if (eq.m_lhs == eq.m_rhs && eq.m_lhs != nullptr) return false; return true; }()` | 5 | 16 | 106 | 127 | -| `post_sort_ordered` | post | `str_eq::sort()` | `m_lhs->id() <= m_rhs->id()` | 7 | 34 | 303 | 344 | - -### 2.2 `str_mem` - -| ID | Kind | Scope | Expression | Z3 | Specbot | DeepTest | Total | -|---|---|---|---|---|---|---|---| -| `pre_add_mem_str_nonnull` | pre | `nielsen_node::add_str_mem()` | `mem.m_str != nullptr` | 2 | 7 | 63 | 72 | -| `pre_add_mem_regex_nonnull` | pre | `nielsen_node::add_str_mem()` | `mem.m_regex != nullptr` | 2 | 7 | 63 | 72 | - -### 2.3 `nielsen_subst` - -| ID | Kind | Scope | Expression | Z3 | Specbot | DeepTest | Total | -|---|---|---|---|---|---|---|---| -| `pre_apply_subst_var_nonnull` | pre | `nielsen_node::apply_subst()` | `s.m_var != nullptr` | 1 | 23 | 148 | 172 | -| `pre_apply_subst_repl_nonnull` | pre | `nielsen_node::apply_subst()` | `s.m_replacement != nullptr` | 1 | 23 | 148 | 172 | - -### 2.4 `nielsen_edge` - -| ID | Kind | Scope | Expression | Z3 | Specbot | DeepTest | Total | -|---|---|---|---|---|---|---|---| -| `pre_mk_edge_src_nonnull` | pre | `nielsen_graph::mk_edge()` | `src != nullptr` | 1 | 20 | 146 | 167 | -| `pre_mk_edge_tgt_nonnull` | pre | `nielsen_graph::mk_edge()` | `tgt != nullptr` | 1 | 20 | 146 | 167 | - -### 2.5 `nielsen_node` - -| ID | Kind | Scope | Expression | Z3 | Specbot | DeepTest | Total | -|---|---|---|---|---|---|---|---| -| `pre_add_eq_lhs_nonnull` | pre | `nielsen_node::add_str_eq()` | `eq.m_lhs != nullptr` | 7 | 12 | 117 | 136 | -| `pre_add_eq_rhs_nonnull` | pre | `nielsen_node::add_str_eq()` | `eq.m_rhs != nullptr` | 7 | 12 | 117 | 136 | -| `pre_clone_from_valid` | pre | `nielsen_node::clone_from()` | `parent.m_id != UINT_MAX` | 1 | 20 | 146 | 167 | -| `post_clone_str_eq_count` | post | `nielsen_node::clone_from()` | `m_str_eq.size() == parent.m_str_eq.size()` | 1 | 20 | 146 | 167 | -| `post_clone_str_mem_count` | post | `nielsen_node::clone_from()` | `m_str_mem.size() == parent.m_str_mem.size()` | 1 | 20 | 146 | 167 | -| `post_clone_constraint_count` | post | `nielsen_node::clone_from()` | `m_constraints.size() == parent.m_constraints.size()` | 1 | 20 | 146 | 167 | -| `pre_gen_ext_node_nonnull` | pre | `nielsen_graph::generate_extensions()` | `node != nullptr` | 1 | 11 | 89 | 101 | -| `pre_gen_ext_node_not_conflict` | pre | `nielsen_graph::generate_extensions()` | `!node->is_currently_conflict()` | 1 | 11 | 89 | 101 | -| `post_simplify_sat_no_eq` | post | `nielsen_node::simplify_and_init()` | `m_str_eq.empty()` (on satisfied) | 4 | 5 | 15 | 24 | -| `post_simplify_sat_no_mem` | post | `nielsen_node::simplify_and_init()` | `m_str_mem.empty()` (on satisfied) | 4 | 5 | 15 | 24 | -| `post_simplify_conflict_flagged` | post | `nielsen_node::simplify_and_init()` | `is_currently_conflict()` (on conflict) | 3 | 0 | 7 | 10 | - -### 2.6 `nielsen_graph` - -| ID | Kind | Scope | Expression | Z3 | Specbot | DeepTest | Total | -|---|---|---|---|---|---|---|---| -| `inv_root_consistent` | inv | `nielsen_graph` (all public methods) | `m_root == nullptr \|\| std::find(m_nodes.begin(), m_nodes.end(), m_root) != m_nodes.end()` | 6 | 8 | 29 | 43 | -| `inv_node_id_sequential` | inv | `nielsen_graph` (all public methods) | `[&]{ for (unsigned i = 0; i < m_nodes.size(); ++i) if (m_nodes[i]->id() != i) return false; return true; }()` | 6 | 8 | 29 | 43 | -| `pre_solve_root_exists` | pre | `nielsen_graph::solve()` | `m_root != nullptr` | 6 | 8 | 29 | 43 | -| `post_solve_sat_has_node` | post | `nielsen_graph::solve()` → SAT | `m_sat_node != nullptr` | 3 | 5 | 15 | 23 | -| `post_solve_unsat_has_conflict` | post | `nielsen_graph::solve()` → UNSAT | `!m_conflict_sources.empty()` | 3 | 0 | 0 | 3 | -| `post_create_root_set` | post | `nielsen_graph::create_root()` | `m_root != nullptr` | 9 | 40 | 152 | 201 | -| `post_create_root_id_zero` | post | `nielsen_graph::create_root()` | `m_root->id() == 0` | 9 | 40 | 152 | 201 | -| `post_create_root_in_nodes` | post | `nielsen_graph::create_root()` | `m_nodes[0] == m_root` | 9 | 40 | 152 | 201 | -| `post_mk_node_id_matches` | post | `nielsen_graph::mk_node()` | `n->id() == m_nodes.size() - 1` | 11 | 60 | 298 | 369 | -| `post_mk_node_in_nodes` | post | `nielsen_graph::mk_node()` | `m_nodes.back() == n` | 11 | 60 | 298 | 369 | -| `post_reset_nodes_empty` | post | `nielsen_graph::reset()` | `m_nodes.empty()` | 12 | 49 | 168 | 229 | -| `post_reset_edges_empty` | post | `nielsen_graph::reset()` | `m_edges.empty()` | 12 | 49 | 168 | 229 | -| `post_reset_root_null` | post | `nielsen_graph::reset()` | `m_root == nullptr` | 12 | 49 | 168 | 229 | -| `post_reset_sat_null` | post | `nielsen_graph::reset()` | `m_sat_node == nullptr` | 12 | 49 | 168 | 229 | - - -## 3. Confirmed Crashes and Failures - -### Z3's own test failures (2) - -**`nseq_zipt`** — Stack overflow (exit code `0xC00000FD`) after 88 seconds on equation `aaX = Xa` -``` -test_zipt_str_equations: -Checking equation: aaX = Xa ← hangs here, then stack overflow -``` - -**`seq_nielsen`** — Assertion violation: `root->outgoing().size() == 3` at `seq_nielsen.cpp:514` -``` -test_eq_split_basic -ASSERTION VIOLATION -File: C:\Users\Shuvendu\z3-c3\src\test\seq_nielsen.cpp -Line: 514 -root->outgoing().size() == 3 -``` - -### Specbot + DeepTest crash-triggering tests (16) - -16 additional tests crash Z3 on pre-existing hard SASSERTs (3 specbot, 13 DeepTest). - -All tests use the Z3 C API with `smt.string_solver=nseq`. - -- Specbot tests: `C:\Users\Shuvendu\z3-c3\build_nokiad\test_specbot_seq.c` -- DeepTest tests: `C:\Users\Shuvendu\z3-c3\build_nokiad\test_deeptest_seq.c` - -### Crash sites - -| Crash site | Root cause | -|-----------|-----------| -| `seq_nielsen.cpp:~3604` | Hard SASSERT `n->is_currently_conflict()` — node conflict state inconsistency | -| `seq_nielsen.h:649` | Backtrack reason state bug | -| `seq_nielsen.h:434` | Variable classification bug (`seq_extract`) | -| `seq_nielsen.cpp:3933` | Unexpected SAT on sub-check (`contains`) | - -### Specbot co-generated tests (3 crashes) - -**`test_regex_combined`** — `x ∈ [0-9]+` combined with `x ++ "-" ++ y = "123-abc"` *(specbot)* -```c -Z3_solver_assert(ctx, s, Z3_mk_seq_in_re(ctx, x, Z3_mk_re_plus(ctx, Z3_mk_re_range(ctx, "0", "9")))); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_concat(ctx, x, mk_concat(ctx, "-", y)), "123-abc")); -``` - -**`test_quadratic_eq`** — `x ++ x = y ++ y` *(specbot)* -```c -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_concat(ctx, x, x), mk_concat(ctx, y, y))); -``` - -**`test_long_string_eq`** — `x ++ y = "aaa...a"` (100 chars) with `|x| = 50` *(specbot)* -```c -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_concat(ctx, x, y), "aaa...a" /* 100 'a's */)); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_seq_length(ctx, x), 50)); -``` - -### DeepTest-generated tests — quadratic/power equations (5 crashes) - -**`test_commutative_eq`** — `x ++ y = y ++ x` with `|x|=2, |y|=3` *(DeepTest)* -```c -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_cat(ctx, x, y), mk_cat(ctx, y, x))); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_len(ctx, x), mk_int(ctx, 2))); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_len(ctx, y), mk_int(ctx, 3))); -``` - -**`test_triple_double`** — `x ++ x ++ x = y ++ y` with `|x|=2` *(DeepTest)* -```c -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_cat3(ctx, x, x, x), mk_cat(ctx, y, y))); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_len(ctx, x), mk_int(ctx, 2))); -``` - -**`test_power_eq`** — `x ++ x = "abab"` *(DeepTest)* -```c -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_cat(ctx, x, x), mk_str(ctx, "abab"))); -``` - -**`test_power_four_repeat`** — `x⁴ = "abcdabcdabcdabcd"` *(DeepTest)* -```c -Z3_ast x4 = mk_cat(ctx, mk_cat(ctx, x, x), mk_cat(ctx, x, x)); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x4, mk_str(ctx, "abcdabcdabcdabcd"))); -``` - -**`test_quadratic_interleaved`** — `x ++ "a" ++ y = y ++ "a" ++ x` with `|x|=1, |y|=1` *(DeepTest)* -```c -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_cat3(ctx, x, a, y), mk_cat3(ctx, y, a, x))); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_len(ctx, x), mk_int(ctx, 1))); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_len(ctx, y), mk_int(ctx, 1))); -``` - -### DeepTest-generated tests — deep variable chains (3 crashes) - -**`test_deep_chain_10`** — 10-variable cascade with length constraint *(DeepTest)* -```c -// v0++v1=v2, v2++v3=v4, v4++v5=v6, v6++v7=v8, v8++v9=v10 -// v10 = "abcdefghij", |v0| = 1 -``` - -**`test_diamond_subst`** — diamond: `x++y=z, x++w=z, z="abcdef", |x|=2` *(DeepTest)* -```c -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_cat(ctx, x, y), z)); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_cat(ctx, x, w), z)); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, z, mk_str(ctx, "abcdef"))); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_len(ctx, x), mk_int(ctx, 2))); -``` - -**`test_wide_fan`** — `x = a0++a1++a2++a3++a4` with all `|ai|=2`, `x="aabbccddee"` *(DeepTest)* - -### DeepTest-generated tests — regex + equations (1 crash) - -**`test_regex_plus_eq`** — `x ∈ [a-z]{3}` combined with `x++y = "abcdef"` *(DeepTest)* -```c -Z3_solver_assert(ctx, s, Z3_mk_seq_in_re(ctx, x, Z3_mk_re_loop(ctx, mk_range(ctx, "a", "z"), 3, 3))); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_cat(ctx, x, y), mk_str(ctx, "abcdef"))); -``` - -### DeepTest-generated tests — incremental solving (2 crashes) - -**`test_incremental_concat_varying`** — 30 push/pop rounds with varying concat targets *(DeepTest)* - -**`test_incremental_nested`** — 10×5 nested push/pop with length constraints *(DeepTest)* - -### DeepTest-generated tests — string operations (2 crashes) - -**`test_substr_extract`** — `substr(x,1,3) = "ell"` with prefix "h" and `|x|=5` *(DeepTest)* -```c -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_seq_extract(ctx, x, 1, 3), mk_str(ctx, "ell"))); -Z3_solver_assert(ctx, s, Z3_mk_seq_prefix(ctx, mk_str(ctx, "h"), x)); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_len(ctx, x), mk_int(ctx, 5))); -``` - -**`test_indexof_constraint`** — `indexof(x, "bc", 0) = 1` with `|x|=5` *(DeepTest)* -```c -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_seq_index(ctx, x, mk_str(ctx,"bc"), 0), mk_int(ctx, 1))); -Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, mk_len(ctx, x), mk_int(ctx, 5))); -``` - ---- - -## 4. Configuration - -``` -spec_mode: all -use_spec_db: false -use_deeptest_tests: true (49 DeepTest tests generated) -run_mutation: false -refinements: 3 -``` - ---- - -*End of SpecBot Report* diff --git a/specbot/test_deeptest_seq.c b/specbot/test_deeptest_seq.c deleted file mode 100644 index 2a6dff6ed..000000000 --- a/specbot/test_deeptest_seq.c +++ /dev/null @@ -1,987 +0,0 @@ -/* - * DeepTest: High-coverage tests for Z3-c3 seq solver (Nielsen graph) - * Targets under-exercised SPECBOT invariants/pre/postconditions in seq_nielsen.cpp - * - * Groups: - * A: Prefix/suffix cancellation (simplify pass 2) - * B: Symbol clash / conflict paths - * C: Deep variable chains (clone_from + apply_subst depth) - * D: Quadratic / VarNielsen modifier tests - * E: Regex derivatives + membership - * F: Power/repeat tests (simplify passes 3a-3e) - * G: Incremental solving stress (push/pop cycles) - * H: UNSAT / conflict collection - * I: Contains/replace/substr operation expansion - * J: Mixed theory (string + integer + boolean) - */ - -#include "z3.h" -#include -#include -#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) { - in_test = 0; - signal(SIGABRT, abort_handler); - longjmp(jmp_env, 1); - } -} - -void suppress_dialogs() { - SetErrorMode(SEM_FAILCRITICALERRORS | SEM_NOGPFAULTERRORBOX); - _CrtSetReportMode(_CRT_ASSERT, _CRTDBG_MODE_FILE); - _CrtSetReportFile(_CRT_ASSERT, _CRTDBG_FILE_STDERR); - _CrtSetReportMode(_CRT_ERROR, _CRTDBG_MODE_FILE); - _CrtSetReportFile(_CRT_ERROR, _CRTDBG_FILE_STDERR); - _set_invalid_parameter_handler( - (void (*)(const wchar_t*,const wchar_t*,const wchar_t*,unsigned int,uintptr_t))0 - ); - _set_abort_behavior(0, _WRITE_ABORT_MSG | _CALL_REPORTFAULT); - 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) { \ - __try { \ - name(); \ - in_test = 0; \ - tests_passed++; \ - fprintf(stderr, "[TEST] PASS %s\n", #name); \ - } __except(EXCEPTION_EXECUTE_HANDLER) { \ - in_test = 0; \ - tests_crashed++; \ - fprintf(stderr, "[TEST] CRASH %s (exception 0x%08lx)\n", #name, GetExceptionCode()); \ - } \ - } else { \ - tests_crashed++; \ - fprintf(stderr, "[TEST] ABORT %s (caught SIGABRT)\n", #name); \ - } \ -} 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); } -static Z3_ast mk_svar(Z3_context ctx, const char* name) { - return Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, name), Z3_mk_string_sort(ctx)); -} -static Z3_ast mk_cat(Z3_context ctx, Z3_ast a, Z3_ast b) { - Z3_ast args[2] = {a, b}; - return Z3_mk_seq_concat(ctx, 2, args); -} -static Z3_ast mk_cat3(Z3_context ctx, Z3_ast a, Z3_ast b, Z3_ast c) { - Z3_ast args[3] = {a, b, c}; - return Z3_mk_seq_concat(ctx, 3, args); -} -static Z3_ast mk_len(Z3_context ctx, Z3_ast s) { return Z3_mk_seq_length(ctx, s); } -static Z3_ast mk_int(Z3_context ctx, int v) { return Z3_mk_int(ctx, v, Z3_mk_int_sort(ctx)); } - -/* Create nseq solver with timeout */ -static Z3_solver mk_nseq(Z3_context ctx, unsigned timeout_ms) { - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - Z3_params p = Z3_mk_params(ctx); - Z3_params_inc_ref(ctx, p); - Z3_params_set_symbol(ctx, p, - Z3_mk_string_symbol(ctx, "smt.string_solver"), - Z3_mk_string_symbol(ctx, "nseq")); - Z3_params_set_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), timeout_ms); - Z3_solver_set_params(ctx, s, p); - Z3_params_dec_ref(ctx, p); - return s; -} - -/* Create context + solver, return both */ -typedef struct { Z3_config cfg; Z3_context ctx; Z3_solver sol; } TestEnv; - -static TestEnv mk_env(unsigned timeout_ms) { - TestEnv e; - e.cfg = Z3_mk_config(); - e.ctx = Z3_mk_context(e.cfg); - e.sol = mk_nseq(e.ctx, timeout_ms); - return e; -} -static void free_env(TestEnv* e) { - Z3_solver_dec_ref(e->ctx, e->sol); - Z3_del_config(e->cfg); - Z3_del_context(e->ctx); -} - -/* Helper: char range regex [lo-hi] */ -static Z3_ast mk_range(Z3_context ctx, const char* lo, const char* hi) { - return Z3_mk_re_range(ctx, mk_str(ctx, lo), mk_str(ctx, hi)); -} - -/* Helper: regex from literal string */ -static Z3_ast mk_re_lit(Z3_context ctx, const char* s) { - return Z3_mk_seq_to_re(ctx, mk_str(ctx, s)); -} - -/* ===================================================================== - * GROUP A: Prefix/suffix cancellation (simplify_and_init pass 2) - * ===================================================================== */ - -/* "abc" ++ x = "abc" ++ y => prefix cancellation */ -void test_prefix_cancel() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast lhs = mk_cat(e.ctx, mk_str(e.ctx, "abc"), x); - Z3_ast rhs = mk_cat(e.ctx, mk_str(e.ctx, "abc"), y); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs)); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x ++ "xyz" = y ++ "xyz" => suffix cancellation */ -void test_suffix_cancel() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast lhs = mk_cat(e.ctx, x, mk_str(e.ctx, "xyz")); - Z3_ast rhs = mk_cat(e.ctx, y, mk_str(e.ctx, "xyz")); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs)); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* "ab" ++ x ++ "cd" = "ab" ++ y ++ "cd" => both prefix and suffix cancelled */ -void test_prefix_suffix_cancel() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast lhs = mk_cat3(e.ctx, mk_str(e.ctx, "ab"), x, mk_str(e.ctx, "cd")); - Z3_ast rhs = mk_cat3(e.ctx, mk_str(e.ctx, "ab"), y, mk_str(e.ctx, "cd")); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs)); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Long shared prefix: "hello_world_" ++ x = "hello_world_" ++ y with length constraints */ -void test_long_prefix_cancel() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast lhs = mk_cat(e.ctx, mk_str(e.ctx, "hello_world_"), x); - Z3_ast rhs = mk_cat(e.ctx, mk_str(e.ctx, "hello_world_"), y); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 5))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, y), mk_int(e.ctx, 5))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Partial prefix overlap: "abc" ++ x = "abd" ++ y => 'ab' cancels, then 'c' vs 'd' clash */ -void test_partial_prefix_clash() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast lhs = mk_cat(e.ctx, mk_str(e.ctx, "abc"), x); - Z3_ast rhs = mk_cat(e.ctx, mk_str(e.ctx, "abd"), y); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs)); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* ===================================================================== - * GROUP B: Symbol clash / conflict detection - * ===================================================================== */ - -/* "a" ++ x = "b" ++ y => first char clash */ -void test_symbol_clash_ab() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_cat(e.ctx, mk_str(e.ctx, "a"), x), - mk_cat(e.ctx, mk_str(e.ctx, "b"), y))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* "x" ++ a = "y" ++ a => prefix clash, same suffix */ -void test_symbol_clash_same_suffix() { - TestEnv e = mk_env(10000); - Z3_ast a = mk_svar(e.ctx, "a"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_cat(e.ctx, mk_str(e.ctx, "x"), a), - mk_cat(e.ctx, mk_str(e.ctx, "y"), a))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* "abc" = "abd" => direct constant clash (UNSAT) */ -void test_const_clash() { - TestEnv e = mk_env(10000); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_str(e.ctx, "abc"), mk_str(e.ctx, "abd"))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Multiple clash patterns in conjunction */ -void test_multi_clash() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast z = mk_svar(e.ctx, "z"); - /* "a"++x = "b"++y AND "c"++y = "d"++z */ - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_cat(e.ctx, mk_str(e.ctx, "a"), x), - mk_cat(e.ctx, mk_str(e.ctx, "b"), y))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_cat(e.ctx, mk_str(e.ctx, "c"), y), - mk_cat(e.ctx, mk_str(e.ctx, "d"), z))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Clash with length constraint making it clearly UNSAT */ -void test_clash_with_length() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_cat(e.ctx, mk_str(e.ctx, "aa"), x), - mk_cat(e.ctx, mk_str(e.ctx, "bb"), x))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* ===================================================================== - * GROUP C: Deep variable chains (many clone_from + apply_subst) - * ===================================================================== */ - -/* Chain of 10 equations: x1++x2=x3, x3++x4=x5, ..., x9++x10=result="abcdefghij" */ -void test_deep_chain_10() { - TestEnv e = mk_env(15000); - char name[16]; - Z3_ast vars[11]; - for (int i = 0; i < 11; i++) { - sprintf(name, "v%d", i); - vars[i] = mk_svar(e.ctx, name); - } - /* v0++v1=v2, v2++v3=v4, v4++v5=v6, v6++v7=v8, v8++v9=v10 */ - for (int i = 0; i < 10; i += 2) { - Z3_ast cat = mk_cat(e.ctx, vars[i], vars[i+1]); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, cat, vars[i+2 < 11 ? i+2 : 10])); - } - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, vars[10], mk_str(e.ctx, "abcdefghij"))); - /* Constrain first var to single char to force cascading resolution */ - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, vars[0]), mk_int(e.ctx, 1))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Linear chain: x1=a++x2, x2=b++x3, ..., x7=h++x8, x8="" => forces all substitutions */ -void test_linear_subst_chain() { - TestEnv e = mk_env(15000); - char name[16]; - Z3_ast vars[9]; - const char* letters[] = {"a","b","c","d","e","f","g","h"}; - for (int i = 0; i < 9; i++) { - sprintf(name, "w%d", i); - vars[i] = mk_svar(e.ctx, name); - } - for (int i = 0; i < 8; i++) { - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - vars[i], mk_cat(e.ctx, mk_str(e.ctx, letters[i]), vars[i+1]))); - } - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, vars[8], mk_str(e.ctx, ""))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Diamond pattern: x++y=z, x++w=z, y=w => forces clone + merge */ -void test_diamond_subst() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast z = mk_svar(e.ctx, "z"); - Z3_ast w = mk_svar(e.ctx, "w"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), z)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, w), z)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, z, mk_str(e.ctx, "abcdef"))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 2))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Wide fan: x=a1++a2++a3++a4++a5 with all ai having length constraints */ -void test_wide_fan() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - char nm[8]; - Z3_ast parts[5]; - for (int i = 0; i < 5; i++) { - sprintf(nm, "a%d", i); - parts[i] = mk_svar(e.ctx, nm); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, parts[i]), mk_int(e.ctx, 2))); - } - /* x = a0 ++ a1 ++ a2 ++ a3 ++ a4 */ - Z3_ast cat01 = mk_cat(e.ctx, parts[0], parts[1]); - Z3_ast cat012 = mk_cat(e.ctx, cat01, parts[2]); - Z3_ast cat0123 = mk_cat(e.ctx, cat012, parts[3]); - Z3_ast cat01234 = mk_cat(e.ctx, cat0123, parts[4]); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, cat01234)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "aabbccddee"))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* ===================================================================== - * GROUP D: Quadratic / VarNielsen modifier - * ===================================================================== */ - -/* x ++ y = y ++ x (commutativity — classic quadratic) */ -void test_commutative_eq() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), mk_cat(e.ctx, y, x))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 2))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, y), mk_int(e.ctx, 3))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x ++ x ++ x = y ++ y (repeated variable, power reasoning) */ -void test_triple_double() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast xxx = mk_cat3(e.ctx, x, x, x); - Z3_ast yy = mk_cat(e.ctx, y, y); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, xxx, yy)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 2))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x ++ "a" ++ y = y ++ "a" ++ x (interleaved constant in quadratic) */ -void test_quadratic_interleaved() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast a = mk_str(e.ctx, "a"); - Z3_ast lhs = mk_cat3(e.ctx, x, a, y); - Z3_ast rhs = mk_cat3(e.ctx, y, a, x); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 1))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, y), mk_int(e.ctx, 1))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x ++ y ++ x = "abcab" (variable appears on both sides) */ -void test_var_both_sides() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast lhs = mk_cat3(e.ctx, x, y, x); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, mk_str(e.ctx, "abcab"))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x ++ x = "abab" (power / repeat equation) */ -void test_power_eq() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast xx = mk_cat(e.ctx, x, x); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, xx, mk_str(e.ctx, "abab"))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* ===================================================================== - * GROUP E: Regex derivatives + membership - * ===================================================================== */ - -/* x in (a|b)* with |x| = 5 */ -void test_regex_star_len() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast re_a = mk_re_lit(e.ctx, "a"); - Z3_ast re_b = mk_re_lit(e.ctx, "b"); - Z3_ast re_ab[2] = {re_a, re_b}; - Z3_ast re_union = Z3_mk_re_union(e.ctx, 2, re_ab); - Z3_ast re_star = Z3_mk_re_star(e.ctx, re_union); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, re_star)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 5))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x in [0-9]{3}-[0-9]{4} (phone pattern) */ -void test_regex_phone() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast digit = mk_range(e.ctx, "0", "9"); - Z3_ast d3 = Z3_mk_re_loop(e.ctx, digit, 3, 3); - Z3_ast dash = mk_re_lit(e.ctx, "-"); - Z3_ast d4 = Z3_mk_re_loop(e.ctx, digit, 4, 4); - Z3_ast parts[3] = {d3, dash, d4}; - Z3_ast phone_re = Z3_mk_re_concat(e.ctx, 3, parts); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, phone_re)); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x in (ab)* intersect (a|b){6} (intersection + bounded loop) */ -void test_regex_intersect() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast re_ab_star = Z3_mk_re_star(e.ctx, mk_re_lit(e.ctx, "ab")); - Z3_ast re_a = mk_re_lit(e.ctx, "a"); - Z3_ast re_b = mk_re_lit(e.ctx, "b"); - Z3_ast ab_union[2] = {re_a, re_b}; - Z3_ast re_ab_single = Z3_mk_re_union(e.ctx, 2, ab_union); - Z3_ast re_6 = Z3_mk_re_loop(e.ctx, re_ab_single, 6, 6); - Z3_ast inter[2] = {re_ab_star, re_6}; - Z3_ast re_isect = Z3_mk_re_intersect(e.ctx, 2, inter); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, re_isect)); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Multiple regex memberships: x in [a-z]+ AND x in .*"abc".* */ -void test_regex_multi_member() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - /* x in [a-z]+ */ - Z3_ast lower = Z3_mk_re_plus(e.ctx, mk_range(e.ctx, "a", "z")); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, lower)); - /* x in .*abc.* (contains "abc" via regex) */ - Z3_ast any = Z3_mk_re_star(e.ctx, Z3_mk_re_full(e.ctx, - Z3_mk_re_sort(e.ctx, Z3_mk_string_sort(e.ctx)))); - Z3_ast abc_lit = mk_re_lit(e.ctx, "abc"); - Z3_ast contain_parts[3] = {any, abc_lit, any}; - Z3_ast contain_re = Z3_mk_re_concat(e.ctx, 3, contain_parts); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, contain_re)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 6))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Regex with complement: x in [a-z]+ AND x NOT in .*"bad".* */ -void test_regex_complement() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast lower_plus = Z3_mk_re_plus(e.ctx, mk_range(e.ctx, "a", "z")); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, lower_plus)); - /* NOT contain "bad" */ - Z3_ast any = Z3_mk_re_star(e.ctx, Z3_mk_re_full(e.ctx, - Z3_mk_re_sort(e.ctx, Z3_mk_string_sort(e.ctx)))); - Z3_ast bad_re_parts[3] = {any, mk_re_lit(e.ctx, "bad"), any}; - Z3_ast bad_re = Z3_mk_re_concat(e.ctx, 3, bad_re_parts); - Z3_ast no_bad = Z3_mk_re_complement(e.ctx, bad_re); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, no_bad)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 4))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Regex + equation: x in [a-z]{3} AND x ++ y = "abcdef" */ -void test_regex_plus_eq() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast lower3 = Z3_mk_re_loop(e.ctx, mk_range(e.ctx, "a", "z"), 3, 3); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, lower3)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), mk_str(e.ctx, "abcdef"))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* ===================================================================== - * GROUP F: Power/repeat (simplify passes 3a-3e) - * ===================================================================== */ - -/* x in a{3,5} with |x| = 4 */ -void test_power_bounded_loop() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast re_a = mk_re_lit(e.ctx, "a"); - Z3_ast re_loop = Z3_mk_re_loop(e.ctx, re_a, 3, 5); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, re_loop)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 4))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x ++ x = y with |y| = 10 => forces power reasoning */ -void test_power_double_eq() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, x), y)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, y), mk_int(e.ctx, 10))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x in (ab){2,4} (multi-char repeat) */ -void test_power_multichar_loop() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast re_ab = mk_re_lit(e.ctx, "ab"); - Z3_ast re_loop = Z3_mk_re_loop(e.ctx, re_ab, 2, 4); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, re_loop)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 6))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x ++ x ++ x ++ x = "abcdabcdabcdabcd" (x repeated 4 times) */ -void test_power_four_repeat() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast x4_inner = mk_cat(e.ctx, x, x); - Z3_ast x4 = mk_cat(e.ctx, x4_inner, x4_inner); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x4, mk_str(e.ctx, "abcdabcdabcdabcd"))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* x in [a-z]{1,3} AND y in [0-9]{2,4} AND x++y has fixed length 5 */ -void test_power_mixed_ranges() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast alpha_re = Z3_mk_re_loop(e.ctx, mk_range(e.ctx, "a", "z"), 1, 3); - Z3_ast digit_re = Z3_mk_re_loop(e.ctx, mk_range(e.ctx, "0", "9"), 2, 4); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, alpha_re)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, y, digit_re)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_len(e.ctx, mk_cat(e.ctx, x, y)), mk_int(e.ctx, 5))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* ===================================================================== - * GROUP G: Incremental solving stress (push/pop cycles) - * ===================================================================== */ - -/* 50 rounds of push/assert/check/pop with simple equations */ -void test_incremental_simple_50() { - TestEnv e = mk_env(30000); - Z3_ast x = mk_svar(e.ctx, "x"); - for (int i = 0; i < 50; i++) { - char val[32]; - sprintf(val, "round_%d", i); - Z3_solver_push(e.ctx, e.sol); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, val))); - Z3_solver_check(e.ctx, e.sol); - Z3_solver_pop(e.ctx, e.sol, 1); - } - free_env(&e); -} - -/* Incremental with concat equations of increasing complexity */ -void test_incremental_concat_varying() { - TestEnv e = mk_env(30000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - for (int i = 0; i < 30; i++) { - Z3_solver_push(e.ctx, e.sol); - char s1[16], s2[16]; - sprintf(s1, "a%d", i); - sprintf(s2, "b%d", i); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_cat(e.ctx, x, y), mk_str(e.ctx, s1))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_len(e.ctx, x), mk_int(e.ctx, 1))); - Z3_solver_check(e.ctx, e.sol); - Z3_solver_pop(e.ctx, e.sol, 1); - } - free_env(&e); -} - -/* Incremental with regex memberships */ -void test_incremental_regex() { - TestEnv e = mk_env(30000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast lower_plus = Z3_mk_re_plus(e.ctx, mk_range(e.ctx, "a", "z")); - /* Keep regex membership across all pushes */ - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, lower_plus)); - for (int i = 1; i <= 20; i++) { - Z3_solver_push(e.ctx, e.sol); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, i))); - Z3_solver_check(e.ctx, e.sol); - Z3_solver_pop(e.ctx, e.sol, 1); - } - free_env(&e); -} - -/* Nested push/pop: 2 levels deep with string constraints */ -void test_incremental_nested() { - TestEnv e = mk_env(15000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - for (int i = 0; i < 10; i++) { - Z3_solver_push(e.ctx, e.sol); - char v1[16]; - sprintf(v1, "outer_%d", i); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_cat(e.ctx, x, y), mk_str(e.ctx, v1))); - Z3_solver_check(e.ctx, e.sol); - for (int j = 0; j < 5; j++) { - Z3_solver_push(e.ctx, e.sol); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, - mk_len(e.ctx, x), mk_int(e.ctx, j))); - Z3_solver_check(e.ctx, e.sol); - Z3_solver_pop(e.ctx, e.sol, 1); - } - Z3_solver_pop(e.ctx, e.sol, 1); - } - free_env(&e); -} - -/* ===================================================================== - * GROUP H: UNSAT / conflict collection paths - * ===================================================================== */ - -/* x = "abc" AND x = "def" (direct contradiction) */ -void test_unsat_direct() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "abc"))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "def"))); - Z3_lbool r = Z3_solver_check(e.ctx, e.sol); - fprintf(stderr, " [unsat_direct] result=%d\n", r); - free_env(&e); -} - -/* |x| = 3 AND x in [a-z]{5} (length conflict) */ -void test_unsat_length_regex() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 3))); - Z3_ast re = Z3_mk_re_loop(e.ctx, mk_range(e.ctx, "a", "z"), 5, 5); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, re)); - Z3_lbool r = Z3_solver_check(e.ctx, e.sol); - fprintf(stderr, " [unsat_length_regex] result=%d\n", r); - free_env(&e); -} - -/* x ++ y = "ab" AND |x| = 3 (length impossible: |x|+|y|=2, |x|=3) */ -void test_unsat_length_impossible() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), mk_str(e.ctx, "ab"))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 3))); - Z3_lbool r = Z3_solver_check(e.ctx, e.sol); - fprintf(stderr, " [unsat_length_impossible] result=%d\n", r); - free_env(&e); -} - -/* x in empty regex */ -void test_unsat_empty_regex() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_sort re_sort = Z3_mk_re_sort(e.ctx, Z3_mk_string_sort(e.ctx)); - Z3_ast empty_re = Z3_mk_re_empty(e.ctx, re_sort); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, empty_re)); - Z3_lbool r = Z3_solver_check(e.ctx, e.sol); - fprintf(stderr, " [unsat_empty_regex] result=%d\n", r); - free_env(&e); -} - -/* x = "abc" AND NOT(x = "abc") (tautological unsat) */ -void test_unsat_negation() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast abc = mk_str(e.ctx, "abc"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, abc)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_not(e.ctx, Z3_mk_eq(e.ctx, x, abc))); - Z3_lbool r = Z3_solver_check(e.ctx, e.sol); - fprintf(stderr, " [unsat_negation] result=%d\n", r); - free_env(&e); -} - -/* x ++ y = "abc" AND x = "ab" AND y = "cd" (suffix mismatch) */ -void test_unsat_concat_mismatch() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), mk_str(e.ctx, "abc"))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "ab"))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, y, mk_str(e.ctx, "cd"))); - Z3_lbool r = Z3_solver_check(e.ctx, e.sol); - fprintf(stderr, " [unsat_concat_mismatch] result=%d\n", r); - free_env(&e); -} - -/* ===================================================================== - * GROUP I: Contains/replace/substr operation expansion - * ===================================================================== */ - -/* contains(x, "needle") AND |x| = 6 (exact fit) */ -void test_contains_exact() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_contains(e.ctx, x, mk_str(e.ctx, "needle"))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 6))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* replace(x, "old", "new") = y AND x = "hold" */ -void test_replace_known() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast replaced = Z3_mk_seq_replace(e.ctx, x, mk_str(e.ctx, "old"), mk_str(e.ctx, "new")); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, replaced, y)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "hold"))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* substr(x, 1, 3) = "ell" AND prefix(x, "h") => x starts with "hell" */ -void test_substr_extract() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast sub = Z3_mk_seq_extract(e.ctx, x, mk_int(e.ctx, 1), mk_int(e.ctx, 3)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, sub, mk_str(e.ctx, "ell"))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_prefix(e.ctx, mk_str(e.ctx, "h"), x)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 5))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* indexof(x, "bc", 0) = 1 AND |x| = 5 */ -void test_indexof_constraint() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast idx = Z3_mk_seq_index(e.ctx, x, mk_str(e.ctx, "bc"), mk_int(e.ctx, 0)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, idx, mk_int(e.ctx, 1))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 5))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* contains(x, "ab") AND contains(x, "cd") AND |x| = 4 => x must be "abcd" or similar */ -void test_multi_contains() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_contains(e.ctx, x, mk_str(e.ctx, "ab"))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_contains(e.ctx, x, mk_str(e.ctx, "cd"))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 4))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* prefix and suffix constraints together */ -void test_prefix_suffix_ops() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_prefix(e.ctx, mk_str(e.ctx, "hel"), x)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_suffix(e.ctx, mk_str(e.ctx, "llo"), x)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 5))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* ===================================================================== - * GROUP J: Mixed theory (string + integer + boolean) - * ===================================================================== */ - -/* |x| + |y| = 10 AND x ++ y = z AND |x| > |y| */ -void test_mixed_len_arith() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_ast z = mk_svar(e.ctx, "z"); - Z3_ast int_sort_args[2] = {mk_len(e.ctx, x), mk_len(e.ctx, y)}; - Z3_ast len_sum = Z3_mk_add(e.ctx, 2, int_sort_args); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, len_sum, mk_int(e.ctx, 10))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), z)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_gt(e.ctx, mk_len(e.ctx, x), mk_len(e.ctx, y))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* ite(contains(x, "a"), x = "abc", x = "def") */ -void test_mixed_ite_contains() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast cond = Z3_mk_seq_contains(e.ctx, x, mk_str(e.ctx, "a")); - Z3_ast then_eq = Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "abc")); - Z3_ast else_eq = Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "def")); - Z3_ast ite = Z3_mk_ite(e.ctx, cond, then_eq, else_eq); - Z3_solver_assert(e.ctx, e.sol, ite); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* str.to_int(x) = 42 AND x in [0-9]+ */ -void test_mixed_str_to_int() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast to_int = Z3_mk_str_to_int(e.ctx, x); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, to_int, mk_int(e.ctx, 42))); - Z3_ast digit_plus = Z3_mk_re_plus(e.ctx, mk_range(e.ctx, "0", "9")); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, digit_plus)); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* int.to_str(n) = x AND n >= 100 AND n <= 999 */ -void test_mixed_int_to_str() { - TestEnv e = mk_env(10000); - Z3_ast n = Z3_mk_const(e.ctx, Z3_mk_string_symbol(e.ctx, "n"), Z3_mk_int_sort(e.ctx)); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, Z3_mk_int_to_str(e.ctx, n), x)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_ge(e.ctx, n, mk_int(e.ctx, 100))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_le(e.ctx, n, mk_int(e.ctx, 999))); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 3))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* Multiple string ops combined: contains + replace + length */ -void test_mixed_ops_combined() { - TestEnv e = mk_env(10000); - Z3_ast x = mk_svar(e.ctx, "x"); - Z3_ast y = mk_svar(e.ctx, "y"); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_contains(e.ctx, x, mk_str(e.ctx, "hello"))); - Z3_ast replaced = Z3_mk_seq_replace(e.ctx, x, mk_str(e.ctx, "hello"), mk_str(e.ctx, "world")); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, replaced, y)); - Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 8))); - Z3_solver_check(e.ctx, e.sol); - free_env(&e); -} - -/* ===================================================================== - * MAIN - * ===================================================================== */ -int main() { - suppress_dialogs(); - fprintf(stderr, "[SPECBOT] Starting DeepTest Z3-c3 seq solver tests\n"); - - Z3_global_param_set("smt.string_solver", "nseq"); - - /* Group A: Prefix/suffix cancellation */ - RUN_TEST(test_prefix_cancel); - RUN_TEST(test_suffix_cancel); - RUN_TEST(test_prefix_suffix_cancel); - RUN_TEST(test_long_prefix_cancel); - RUN_TEST(test_partial_prefix_clash); - - /* Group B: Symbol clash */ - RUN_TEST(test_symbol_clash_ab); - RUN_TEST(test_symbol_clash_same_suffix); - RUN_TEST(test_const_clash); - RUN_TEST(test_multi_clash); - RUN_TEST(test_clash_with_length); - - /* Group C: Deep variable chains */ - RUN_TEST(test_deep_chain_10); - RUN_TEST(test_linear_subst_chain); - RUN_TEST(test_diamond_subst); - RUN_TEST(test_wide_fan); - - /* Group D: Quadratic / VarNielsen */ - RUN_TEST(test_commutative_eq); - RUN_TEST(test_triple_double); - RUN_TEST(test_quadratic_interleaved); - RUN_TEST(test_var_both_sides); - RUN_TEST(test_power_eq); - - /* Group E: Regex derivatives */ - RUN_TEST(test_regex_star_len); - RUN_TEST(test_regex_phone); - RUN_TEST(test_regex_intersect); - RUN_TEST(test_regex_multi_member); - RUN_TEST(test_regex_complement); - RUN_TEST(test_regex_plus_eq); - - /* Group F: Power/repeat */ - RUN_TEST(test_power_bounded_loop); - RUN_TEST(test_power_double_eq); - RUN_TEST(test_power_multichar_loop); - RUN_TEST(test_power_four_repeat); - RUN_TEST(test_power_mixed_ranges); - - /* Group G: Incremental stress */ - RUN_TEST(test_incremental_simple_50); - RUN_TEST(test_incremental_concat_varying); - RUN_TEST(test_incremental_regex); - RUN_TEST(test_incremental_nested); - - /* Group H: UNSAT / conflict */ - RUN_TEST(test_unsat_direct); - RUN_TEST(test_unsat_length_regex); - RUN_TEST(test_unsat_length_impossible); - RUN_TEST(test_unsat_empty_regex); - RUN_TEST(test_unsat_negation); - RUN_TEST(test_unsat_concat_mismatch); - - /* Group I: Contains/replace/substr */ - RUN_TEST(test_contains_exact); - RUN_TEST(test_replace_known); - RUN_TEST(test_substr_extract); - RUN_TEST(test_indexof_constraint); - RUN_TEST(test_multi_contains); - RUN_TEST(test_prefix_suffix_ops); - - /* Group J: Mixed theory */ - RUN_TEST(test_mixed_len_arith); - RUN_TEST(test_mixed_ite_contains); - RUN_TEST(test_mixed_str_to_int); - RUN_TEST(test_mixed_int_to_str); - RUN_TEST(test_mixed_ops_combined); - - printf("=== DeepTest Z3-c3 Seq: %d/%d passed, %d crashed ===\n", - tests_passed, tests_run, tests_crashed); - return tests_run - tests_passed; -} diff --git a/specbot/test_specbot_seq.c b/specbot/test_specbot_seq.c deleted file mode 100644 index 17a725371..000000000 --- a/specbot/test_specbot_seq.c +++ /dev/null @@ -1,498 +0,0 @@ -#include "z3.h" -#include -#include -#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) { - in_test = 0; - signal(SIGABRT, abort_handler); - longjmp(jmp_env, 1); - } -} - -void suppress_dialogs() { - SetErrorMode(SEM_FAILCRITICALERRORS | SEM_NOGPFAULTERRORBOX); - _CrtSetReportMode(_CRT_ASSERT, _CRTDBG_MODE_FILE); - _CrtSetReportFile(_CRT_ASSERT, _CRTDBG_FILE_STDERR); - _CrtSetReportMode(_CRT_ERROR, _CRTDBG_MODE_FILE); - _CrtSetReportFile(_CRT_ERROR, _CRTDBG_FILE_STDERR); - _set_invalid_parameter_handler( - (void (*)(const wchar_t*,const wchar_t*,const wchar_t*,unsigned int,uintptr_t))0 - ); - _set_abort_behavior(0, _WRITE_ABORT_MSG | _CALL_REPORTFAULT); - 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) { \ - __try { \ - name(); \ - in_test = 0; \ - tests_passed++; \ - fprintf(stderr, "[TEST] PASS %s\n", #name); \ - } __except(EXCEPTION_EXECUTE_HANDLER) { \ - in_test = 0; \ - fprintf(stderr, "[TEST] CRASH %s (exception 0x%08lx)\n", #name, GetExceptionCode()); \ - } \ - } else { \ - fprintf(stderr, "[TEST] ABORT %s (caught SIGABRT)\n", #name); \ - } \ -} 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) { - return Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, name), Z3_mk_string_sort(ctx)); -} -Z3_ast mk_string_val(Z3_context ctx, const char* s) { - return Z3_mk_string(ctx, s); -} -Z3_ast mk_concat(Z3_context ctx, Z3_ast a, Z3_ast b) { - Z3_ast args[2] = {a, b}; - return Z3_mk_seq_concat(ctx, 2, args); -} - -/* Create a solver configured to use the nseq (Nielsen) string solver */ -Z3_solver mk_nseq_solver(Z3_context ctx) { - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - Z3_params p = Z3_mk_params(ctx); - Z3_params_inc_ref(ctx, p); - Z3_params_set_symbol(ctx, p, Z3_mk_string_symbol(ctx, "smt.string_solver"), - Z3_mk_string_symbol(ctx, "nseq")); - Z3_solver_set_params(ctx, s, p); - Z3_params_dec_ref(ctx, p); - return s; -} - -/* === TEST GROUPS === */ - -/* Group A: Basic equations - exercises clone_from, simplify, solve */ -void test_simple_eq() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast hello = mk_string_val(ctx, "hello"); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, hello)); - - Z3_lbool r = Z3_solver_check(ctx, s); - (void)r; - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_concat_eq() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast y = mk_string_var(ctx, "y"); - Z3_ast xy = mk_concat(ctx, x, y); - Z3_ast abc = mk_string_val(ctx, "abc"); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xy, abc)); - - Z3_lbool r = Z3_solver_check(ctx, s); - (void)r; - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_unsat_eq() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, mk_string_val(ctx, "a"))); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, mk_string_val(ctx, "b"))); - - Z3_lbool r = Z3_solver_check(ctx, s); - (void)r; - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_multi_var_eq() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast y = mk_string_var(ctx, "y"); - Z3_ast z = mk_string_var(ctx, "z"); - Z3_ast xy = mk_concat(ctx, x, y); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xy, z)); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, z, mk_string_val(ctx, "test"))); - - Z3_solver_check(ctx, s); - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_empty_string() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast empty = mk_string_val(ctx, ""); - Z3_ast xe = mk_concat(ctx, x, empty); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xe, x)); - - Z3_solver_check(ctx, s); - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -/* Group B: Regex membership - exercises add_str_mem, regex processing */ -void test_regex_basic() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast re = Z3_mk_re_plus(ctx, Z3_mk_re_range(ctx, mk_string_val(ctx, "a"), mk_string_val(ctx, "z"))); - Z3_solver_assert(ctx, s, Z3_mk_seq_in_re(ctx, x, re)); - - Z3_solver_check(ctx, s); - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_regex_combined() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast y = mk_string_var(ctx, "y"); - Z3_ast re = Z3_mk_re_plus(ctx, Z3_mk_re_range(ctx, mk_string_val(ctx, "0"), mk_string_val(ctx, "9"))); - Z3_solver_assert(ctx, s, Z3_mk_seq_in_re(ctx, x, re)); - - Z3_ast xy = mk_concat(ctx, x, mk_concat(ctx, mk_string_val(ctx, "-"), y)); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xy, mk_string_val(ctx, "123-abc"))); - - Z3_solver_check(ctx, s); - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -/* Group C: Length constraints */ -void test_length_eq() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast len_x = Z3_mk_seq_length(ctx, x); - Z3_ast five = Z3_mk_int(ctx, 5, Z3_mk_int_sort(ctx)); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, len_x, five)); - Z3_ast re = Z3_mk_re_plus(ctx, Z3_mk_re_range(ctx, mk_string_val(ctx, "a"), mk_string_val(ctx, "z"))); - Z3_solver_assert(ctx, s, Z3_mk_seq_in_re(ctx, x, re)); - - Z3_solver_check(ctx, s); - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_length_sum() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast y = mk_string_var(ctx, "y"); - Z3_ast z = mk_string_var(ctx, "z"); - Z3_ast xy = mk_concat(ctx, x, y); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xy, z)); - - Z3_ast ten = Z3_mk_int(ctx, 10, Z3_mk_int_sort(ctx)); - Z3_ast len_z = Z3_mk_seq_length(ctx, z); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, len_z, ten)); - - Z3_solver_check(ctx, s); - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -/* Group D: Nielsen-specific stress */ -void test_quadratic_eq() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - Z3_params p = Z3_mk_params(ctx); - Z3_params_inc_ref(ctx, p); - Z3_params_set_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), 5000); - Z3_solver_set_params(ctx, s, p); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast y = mk_string_var(ctx, "y"); - Z3_ast xx = mk_concat(ctx, x, x); - Z3_ast yy = mk_concat(ctx, y, y); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xx, yy)); - - Z3_solver_check(ctx, s); - - Z3_params_dec_ref(ctx, p); - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_many_vars() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - Z3_params p = Z3_mk_params(ctx); - Z3_params_inc_ref(ctx, p); - Z3_params_set_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), 5000); - Z3_solver_set_params(ctx, s, p); - - char name[16]; - Z3_ast vars[10]; - for (int i = 0; i < 10; i++) { - sprintf(name, "x%d", i); - vars[i] = mk_string_var(ctx, name); - } - for (int i = 0; i < 8; i += 2) { - Z3_ast cat = mk_concat(ctx, vars[i], vars[i+1]); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, cat, vars[i+2 < 10 ? i+2 : 0])); - } - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, vars[0], mk_string_val(ctx, "ab"))); - - Z3_solver_check(ctx, s); - - Z3_params_dec_ref(ctx, p); - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_push_pop() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, mk_string_val(ctx, "hello"))); - Z3_solver_check(ctx, s); - - Z3_solver_push(ctx, s); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, mk_string_val(ctx, "world"))); - Z3_solver_check(ctx, s); - Z3_solver_pop(ctx, s, 1); - - Z3_solver_check(ctx, s); - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_incremental_many() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - Z3_params p = Z3_mk_params(ctx); - Z3_params_inc_ref(ctx, p); - Z3_params_set_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), 5000); - Z3_solver_set_params(ctx, s, p); - - Z3_ast x = mk_string_var(ctx, "x"); - for (int i = 0; i < 20; i++) { - Z3_solver_push(ctx, s); - char val[32]; - sprintf(val, "test_%d", i); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, mk_string_val(ctx, val))); - Z3_solver_check(ctx, s); - Z3_solver_pop(ctx, s, 1); - } - - Z3_params_dec_ref(ctx, p); - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -/* Group E: Edge cases */ -void test_contains() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_solver_assert(ctx, s, Z3_mk_seq_contains(ctx, x, mk_string_val(ctx, "needle"))); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_seq_length(ctx, x), Z3_mk_int(ctx, 10, Z3_mk_int_sort(ctx)))); - - Z3_solver_check(ctx, s); - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_replace() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast y = mk_string_var(ctx, "y"); - Z3_ast replaced = Z3_mk_seq_replace(ctx, x, mk_string_val(ctx, "old"), mk_string_val(ctx, "new")); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, replaced, y)); - Z3_solver_assert(ctx, s, Z3_mk_seq_contains(ctx, x, mk_string_val(ctx, "old"))); - - Z3_solver_check(ctx, s); - - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -void test_long_string_eq() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); - Z3_params p = Z3_mk_params(ctx); - Z3_params_inc_ref(ctx, p); - Z3_params_set_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), 10000); - Z3_solver_set_params(ctx, s, p); - - char long_str[101]; - memset(long_str, 'a', 100); - long_str[100] = 0; - - Z3_ast x = mk_string_var(ctx, "x"); - Z3_ast y = mk_string_var(ctx, "y"); - Z3_ast xy = mk_concat(ctx, x, y); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xy, mk_string_val(ctx, long_str))); - Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_seq_length(ctx, x), Z3_mk_int(ctx, 50, Z3_mk_int_sort(ctx)))); - - Z3_solver_check(ctx, s); - - Z3_params_dec_ref(ctx, p); - Z3_solver_dec_ref(ctx, s); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - -int main() { - suppress_dialogs(); - fprintf(stderr, "[SPECBOT] Starting Z3 c3 seq solver invariant tests\n"); - - /* Force the Nielsen seq solver globally */ - Z3_global_param_set("smt.string_solver", "nseq"); - - /* Group A: Basic equations */ - RUN_TEST(test_simple_eq); - RUN_TEST(test_concat_eq); - RUN_TEST(test_unsat_eq); - RUN_TEST(test_multi_var_eq); - RUN_TEST(test_empty_string); - - /* Group B: Regex */ - RUN_TEST(test_regex_basic); - RUN_TEST(test_regex_combined); - - /* Group C: Length */ - RUN_TEST(test_length_eq); - RUN_TEST(test_length_sum); - - /* Group D: Nielsen stress */ - RUN_TEST(test_quadratic_eq); - RUN_TEST(test_many_vars); - RUN_TEST(test_push_pop); - RUN_TEST(test_incremental_many); - - /* Group E: Edge cases */ - RUN_TEST(test_contains); - RUN_TEST(test_replace); - RUN_TEST(test_long_string_eq); - - printf("=== SpecBot Z3-c3 Seq Tests: %d/%d passed ===\n", tests_passed, tests_run); - return tests_run - tests_passed; -} diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 030e9a871..4adecaa54 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -851,7 +851,6 @@ namespace seq { // (e.g., explain_conflict) can call mk_join / linearize. mutable dep_manager m_dep_mgr; - std::ostream &display(std::ostream &out, nielsen_node const* n) const; public: // Construct with a caller-supplied solver. Ownership is NOT transferred; @@ -936,6 +935,8 @@ namespace seq { // display for debugging std::ostream& display(std::ostream& out) const; + std::ostream &display(std::ostream &out, nielsen_node const *n) const; + // output the graph in graphviz DOT format. // nodes on the sat_path are highlighted green; conflict nodes red/darkred. // mirrors ZIPT's NielsenGraph.ToDot() diff --git a/src/smt/seq_model.cpp.draft b/src/smt/seq_model.cpp.draft index b5e38b93f..64b28b8bc 100644 --- a/src/smt/seq_model.cpp.draft +++ b/src/smt/seq_model.cpp.draft @@ -91,7 +91,6 @@ namespace smt { m_var_replacement.reset(); m_var_regex.reset(); m_trail.reset(); - m_mg = &mg; m_factory = alloc(seq_factory, m, m_seq.get_family_id(), mg.get_model()); mg.register_factory(m_factory); @@ -101,13 +100,17 @@ namespace smt { SASSERT(sat_node); // in case we report sat, this has to point to a satisfied Nielsen node! collect_var_regex_constraints(sat_node); + // solve integer constraints from the sat_path FIRST so that // m_int_model is available when snode_to_value evaluates power exponents // VERIFY(nielsen.solve_sat_path_raw(m_int_model)); // extract variable assignments from the satisfying leaf's substitution path extract_assignments(nielsen.sat_path()); + + // TODO: we may need to register nodes in the egraph that are created inside the + // inner solvers. } model_value_proc* seq_model::mk_value(enode* n, model_generator& mg) { @@ -123,6 +126,7 @@ namespace smt { } // For nth_u (underspecified nth), return a fresh value of the element sort. + // NSB review: this looks plain wrong. if (m_seq.str.is_nth_u(e)) { sort* srt = e->get_sort(); expr* val = m_factory->get_fresh_value(srt); @@ -160,7 +164,6 @@ namespace smt { m_var_regex.reset(); m_var_replacement.reset(); m_trail.reset(); - m_mg = nullptr; m_factory = nullptr; } @@ -205,60 +208,67 @@ namespace smt { sort* srt = n->get_sort(); if (!srt) srt = m_seq.str.mk_string_sort(); - return expr_ref(m_seq.str.mk_empty(srt), m); + return expr_ref(m_seq.str.mk_empty(srt), m); } + arith_util arith(m); + + if (m.is_value(n->get_expr())) + return expr_ref(n->get_expr(), m); if (n->is_char_or_unit()) { - expr *e = n->get_expr(); - SASSERT(m_seq.str.is_unit(e)); - SASSERT(values.size() == 1); - e = to_app(e)->get_arg(0); - unsigned c; - - expr *dval = values.get(0); - if (m_seq.is_const_char(dval, c)) - return expr_ref(m_seq.str.mk_string(zstring(c)), m); - return expr_ref(m_seq.str.mk_unit(dval), m); + expr *e = nullptr; + VERIFY(m_seq.str.is_unit(n->get_expr(), e)); + if (values.size() == 1) { + unsigned c; + expr *dval = values.get(0); + if (m_seq.is_const_char(dval, c)) + return expr_ref(m_seq.str.mk_string(zstring(c)), m); + return expr_ref(m_seq.str.mk_unit(dval), m); + } + else if (m_seq.str.is_nth_u(e)) { + auto arg = n->arg(0); + auto var_val = get_var_value(arg->arg(0)); + auto index_val = int_value(arg->arg(1)->get_expr()); + expr_ref val(m_seq.str.mk_nth(var_val, arith.mk_int(index_val)), m); + return expr_ref(m_seq.str.mk_unit(val), m); + } + else + NOT_IMPLEMENTED_YET(); } if (n->is_var()) { euf::snode *replacement = nullptr; if (!m_var_replacement.find(n->id(), replacement)) - return get_var_value(n); + return expr_ref(get_var_value(n), m); return mk_value_with_dependencies(n, replacement, values); } if (n->is_concat()) { - return expr_ref(m_seq.str.mk_concat(values, n->get_sort()), m); + expr_ref_vector es(m), vals(m); + unsigned idx = 0; + m_seq.str.get_concat(n->get_expr(), es); + for (auto e : es) { + if (m.is_value(e)) + vals.push_back(e); + else + vals.push_back(values[idx++]); + } + return expr_ref(m_seq.str.mk_concat(vals, n->get_sort()), m); } if (n->is_power()) { SASSERT(n->num_args() == 2); - SASSERT(values.size() == 2); + SASSERT(values.size() == 0); // Evaluate the base and exponent to produce a concrete string. // The base is a string snode; the exponent is an integer expression // whose value comes from the sat_path integer model. - expr* base_val = values.get(0); - expr *exp_expr = values.get(1); - - rational exp_val(0); - arith_util arith(m); - - - // Try to evaluate exponent: first check if it's a numeral, - // then try the int model from sat_path constraints, - // finally fall back to the proto_model from model_generator. - - bool has_val = arith.is_numeral(exp_expr, exp_val); - - SASSERT(has_val); - if (!has_val) { - arith_value avalue(m); - avalue.init(&m_ctx); - avalue.get_value(exp_expr, exp_val); - } + expr *base_val = n->arg(0)->get_expr(); + expr *exp_expr = n->arg(1)->get_expr(); + rational exp_val = int_value(exp_expr); + + if (exp_val.is_neg()) exp_val = rational(0); @@ -266,7 +276,7 @@ namespace smt { if (exp_val == 0) return expr_ref(m_seq.str.mk_empty(n->get_sort()), m); - + TRACE(seq, tout << mk_pp(n->get_expr(), m) << '\n'); // For small exponents, concatenate directly; for large ones, // return mk_power to avoid enormous AST chains. constexpr unsigned POWER_EXPAND_LIMIT = 10; @@ -282,17 +292,26 @@ namespace smt { // fallback: use the underlying expression return expr_ref(n->get_expr(), m); } - + void seq_model::collect_dependencies(euf::snode *n, ptr_vector &deps) const { - if (n->is_char() || n->is_unit()) - deps.push_back(m_ctx.get_enode(n->arg(0)->get_expr())); + if (m.is_value(n->get_expr())) + return; + if (n->is_char_or_unit()) { + expr *e = n->arg(0)->get_expr(); + if (m_ctx.e_internalized(e)) + deps.push_back(m_ctx.get_enode(e)); + } else if (n->is_concat()) { - for (unsigned i = 0; i < n->num_args(); ++i) - deps.push_back(m_ctx.get_enode(n->arg(i)->get_expr())); + expr_ref_vector es(m); + m_seq.str.get_concat(n->get_expr(), es); + for (auto e : es) { + if (!m.is_value(e)) + deps.push_back(m_ctx.get_enode(e)); + } } else if (n->is_power()) { - deps.push_back(m_ctx.get_enode(n->arg(0)->get_expr())); - deps.push_back(m_ctx.get_enode(n->arg(1)->get_expr())); + // pretend there are no dependencies + // TODO - may not be sufficient if the exponent is a variable with a binding that contains dependencies } else if (n->is_var()) { // we could have a binding n |-> replacement @@ -317,8 +336,12 @@ namespace smt { if (seen.contains(curr->id())) continue; seen.insert(curr->id()); - if (curr->is_char_or_unit()) { - deps.push_back(m_ctx.get_enode(curr->arg(0)->get_expr())); + if (m.is_value(curr->get_expr())) + ; + else if (curr->is_char_or_unit()) { + expr *e = curr->arg(0)->get_expr(); + if (m_ctx.e_internalized(e)) + deps.push_back(m_ctx.get_enode(e)); } else if (curr->is_concat()) { for (unsigned i = 0; i < curr->num_args(); ++i) @@ -326,14 +349,19 @@ namespace smt { } else if (curr->is_power()) { SASSERT(curr->num_args() == 2); - deps.push_back(m_ctx.get_enode(curr->arg(0)->get_expr())); - deps.push_back(m_ctx.get_enode(curr->arg(1)->get_expr())); } else if (curr->is_var()) { ; } - else + else { + IF_VERBOSE(0, { + verbose_stream() << "nseq collect_dependencies_rec: unhandled snode kind " << (int)curr->kind() << "\n"; + verbose_stream() << " curr: snode[" << curr->id() << "]"; + if (curr->get_expr()) verbose_stream() << " expr=" << mk_bounded_pp(curr->get_expr(), m, 2); + verbose_stream() << "\n"; + }); UNREACHABLE(); + } } } @@ -344,6 +372,8 @@ namespace smt { u_map var2value; ptr_buffer todo; unsigned idx = 0; + arith_util a(m); + expr_ref_vector args(m), pinned(m); todo.push_back(replacement); while (!todo.empty()) { SASSERT(idx <= values.size()); @@ -352,8 +382,26 @@ namespace smt { if (seen.contains(curr->id())) continue; seen.insert(curr->id()); - if (curr->is_char_or_unit()) { - var2value.insert(curr->id(), values[idx++]); + if (m.is_value(curr->get_expr())) + var2value.insert(curr->id(), curr->get_expr()); + else if (curr->is_char_or_unit()) { + auto arg = curr->arg(0); + expr *e = arg->get_expr(); + expr *val = nullptr; + if (m_ctx.e_internalized(e)) { + val = values[idx++]; + } + else if (m_seq.str.is_nth_u(e)) { + expr* var_value = get_var_value(arg->arg(0)); + auto index = int_value(arg->arg(1)->get_expr()); + val = m_seq.str.mk_nth(var_value, a.mk_int(index)); + } + else { + NOT_IMPLEMENTED_YET(); + } + val = m_seq.str.mk_unit(val); + var2value.insert(curr->id(), val); + pinned.push_back(val); } else if (curr->is_concat()) { for (unsigned i = 0; i < curr->num_args(); ++i) @@ -361,8 +409,6 @@ namespace smt { } else if (curr->is_power()) { SASSERT(curr->num_args() == 2); - var2value.insert(curr->arg(0)->id(), values[idx++]); - var2value.insert(curr->arg(1)->id(), values[idx++]); } else if (curr->is_var()) { ; @@ -373,8 +419,8 @@ namespace smt { // then reconstruct the value for replacement based on the collected sub-term values. SASSERT(values.size() == idx); todo.push_back(replacement); - expr_ref_vector args(m), pinned(m); - expr_ref val(m); + + expr *val = nullptr; while (!todo.empty()) { euf::snode *curr = todo.back(); if (var2value.contains(curr->id())) { @@ -383,7 +429,8 @@ namespace smt { } if (curr->is_power()) { - val = m_seq.str.mk_power(var2value.find(curr->arg(0)->id()), var2value.find(curr->arg(1)->id())); + auto ival = int_value(curr->arg(1)->get_expr()); + val = m_seq.str.mk_power(curr->arg(0)->get_expr(), a.mk_int(ival)); } else if (curr->is_concat()) { args.reset(); @@ -415,12 +462,7 @@ namespace smt { seq::nielsen_node const* root = nielsen.root(); if (!root) return; - for (auto const& eq : root->str_eqs()) { - if (eq.m_lhs && eq.m_lhs->get_expr()) - m_factory->register_value(eq.m_lhs->get_expr()); - if (eq.m_rhs && eq.m_rhs->get_expr()) - m_factory->register_value(eq.m_rhs->get_expr()); - } + // TODO - need to traverse sub-expressions for values. } expr* seq_model::get_var_value(euf::snode* var) { @@ -439,6 +481,21 @@ namespace smt { return val; } + rational seq_model::int_value(expr *_e) { + expr_ref e(_e, m); + m_ctx.get_rewriter()(e); + rational val; + arith_util a(m); + if (a.is_numeral(e, val)) + return val; + + arith_value avalue(m); + avalue.init(&m_ctx); + bool has_val = avalue.get_value(e, val); + CTRACE(seq, !has_val, tout << "no value associated with " << mk_pp(e, m) << "\n";); + return val; + } + expr* seq_model::mk_fresh_value(euf::snode* var) { SASSERT(var->get_expr()); if (!m_seq.is_seq(var->get_expr())) @@ -519,7 +576,7 @@ namespace smt { void seq_model::collect_var_regex_constraints(seq::nielsen_node const* sat_node) { SASSERT(sat_node); for (auto const& mem : sat_node->str_mems()) { - SASSERT(mem.m_str && mem.m_regex); + SASSERT(mem.well_formed()); if (mem.is_trivial(sat_node)) continue; // empty string in nullable regex: already satisfied, no variable to constrain VERIFY(mem.is_primitive()); // everything else should have been eliminated already diff --git a/src/smt/seq_model.h.draft b/src/smt/seq_model.h.draft index 1c78c0636..3ae371d7a 100644 --- a/src/smt/seq_model.h.draft +++ b/src/smt/seq_model.h.draft @@ -66,10 +66,6 @@ namespace smt { // trail for GC protection of generated expressions expr_ref_vector m_trail; - // integer variable model from sat_path constraints - model_ref m_int_model; - model_generator* m_mg = nullptr; - // per-variable regex constraints: maps snode id -> intersected regex snode. // collected during init() from the state's str_mem list. u_map m_var_regex; @@ -138,6 +134,9 @@ namespace smt { // with existing) into m_var_regex keyed by the string snode id. void collect_var_regex_constraints(seq::nielsen_node const* sat_node); + // extract integer value for an expression. + rational int_value(expr *e); + }; } diff --git a/tests/QF_S.tar.zst b/tests/QF_S.tar.zst deleted file mode 100644 index 0c2784382..000000000 Binary files a/tests/QF_S.tar.zst and /dev/null differ diff --git a/tests/QF_SLIA.tar.zst b/tests/QF_SLIA.tar.zst deleted file mode 100644 index 0ecec6684..000000000 Binary files a/tests/QF_SLIA.tar.zst and /dev/null differ