mirror of
https://github.com/Z3Prover/z3
synced 2026-04-18 01:50:17 +00:00
Add specbot test files from c3 branch
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/cd4905c3-da72-4e93-b0f4-b512453d2bf6 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
GitHub
parent
8d7ed66ebf
commit
8e165e14c0
3 changed files with 1749 additions and 0 deletions
317
specbot/SPECBOT_REPORT.md
Normal file
317
specbot/SPECBOT_REPORT.md
Normal file
|
|
@ -0,0 +1,317 @@
|
|||
# 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<nielsen_node> (all nodes)
|
||||
├── owns: ptr_vector<nielsen_edge> (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<str_eq> (string equalities)
|
||||
├── has: vector<str_mem> (regex memberships)
|
||||
├── has: vector<constraint> (integer constraints)
|
||||
├── has: ptr_vector<nielsen_edge> (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<nielsen_subst> (substitutions)
|
||||
└── has: vector<constraint> (side constraints)
|
||||
|
||||
seq_regex
|
||||
├── refs: euf::sgraph& m_sg
|
||||
├── has: u_map<ptr_vector<snode>> 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*
|
||||
960
specbot/test_deeptest_seq.c
Normal file
960
specbot/test_deeptest_seq.c
Normal file
|
|
@ -0,0 +1,960 @@
|
|||
/*
|
||||
* 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 <stdio.h>
|
||||
#include <string.h>
|
||||
#include <stdlib.h>
|
||||
#include <setjmp.h>
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
#include <crtdbg.h>
|
||||
#include <signal.h>
|
||||
|
||||
static jmp_buf jmp_env;
|
||||
static volatile int in_test = 0;
|
||||
|
||||
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);
|
||||
}
|
||||
#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); \
|
||||
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)
|
||||
|
||||
/* ===== 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;
|
||||
}
|
||||
472
specbot/test_specbot_seq.c
Normal file
472
specbot/test_specbot_seq.c
Normal file
|
|
@ -0,0 +1,472 @@
|
|||
#include "z3.h"
|
||||
#include <stdio.h>
|
||||
#include <string.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
#include <setjmp.h>
|
||||
|
||||
#ifdef _WIN32
|
||||
#include <windows.h>
|
||||
#include <crtdbg.h>
|
||||
#include <signal.h>
|
||||
|
||||
static jmp_buf jmp_env;
|
||||
static volatile int in_test = 0;
|
||||
|
||||
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);
|
||||
}
|
||||
#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); \
|
||||
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)
|
||||
|
||||
/* 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;
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue