mirror of
https://github.com/Z3Prover/z3
synced 2026-03-07 05:44:51 +00:00
add comparison report
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
69eab28550
commit
c7bf96325c
3 changed files with 324 additions and 0 deletions
189
comparison-report.md
Normal file
189
comparison-report.md
Normal file
|
|
@ -0,0 +1,189 @@
|
|||
# Comparison Report: Case Splits in `smt_parallel.cpp` vs. AriParti
|
||||
|
||||
## Overview
|
||||
|
||||
This report compares how **Z3's `src/smt/smt_parallel.cpp`** and **AriParti** (`src/partitioner/src/math/subpaving/subpaving_t_def.h` + orchestrated by `src/AriParti.py`) perform case splits in parallel arithmetic SMT solving.
|
||||
|
||||
---
|
||||
|
||||
## Architecture
|
||||
|
||||
| Aspect | Z3 `smt_parallel.cpp` | AriParti |
|
||||
|---|---|---|
|
||||
| Parallelism model | Shared-memory multi-threaded (C++ threads, one `smt::context` per worker) | Process-based distributed (partitioner process + N solver sub-processes, IPC via named pipes) |
|
||||
| Where splits happen | Inside each SMT worker thread, using the live SMT context state | In a standalone subpaving partitioner process, before handing off to external solvers |
|
||||
| Split representation | `expr_ref` atom (e.g., `x ≤ mid`) passed to `batch_manager`, which builds a search tree | Bound pair (`x ≤ mid` / `x > mid`) installed on two child nodes in the subpaving tree |
|
||||
| Sub-problem dispatch | Workers pull cubes from a shared `search_tree` via `batch_manager::get_cube()` | Child nodes are serialised to `.smt2` files and dispatched to external solver processes |
|
||||
|
||||
---
|
||||
|
||||
## Case Split Flow
|
||||
|
||||
### Z3 (`smt_parallel.cpp`)
|
||||
|
||||
```
|
||||
worker::run()
|
||||
→ check_cube() [run SMT check with current cube]
|
||||
→ l_undef result
|
||||
→ get_split_atom()
|
||||
1. get_arith_split_atom() ← AriParti-style arithmetic split
|
||||
2. VSIDS Boolean fallback ← if no arithmetic atom found
|
||||
→ batch_manager::split() ← insert atom into search tree (binary split)
|
||||
→ simplify() ← optional inprocessing
|
||||
```
|
||||
|
||||
### AriParti (`subpaving_t_def.h` / `AriParti.py`)
|
||||
|
||||
```
|
||||
context_t::operator()() ← main partitioner loop
|
||||
→ create_new_task() ← if a leaf is ready, emit it as an .smt2 task
|
||||
→ select_split_node() ← pick highest-priority leaf from heap
|
||||
→ split_node(n)
|
||||
→ select_best_var(n) ← multi-key heuristic
|
||||
→ compute midpoint
|
||||
→ mk_node(left), mk_node(right)
|
||||
→ propagate(left/right) ← BICP immediately
|
||||
→ emit "unsat-task" or "new-task" messages to master
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
## Variable Selection Heuristic
|
||||
|
||||
### Z3 `get_arith_split_atom()`
|
||||
|
||||
Iterates over all 0-arity arithmetic enodes visible in the current SMT context. For each variable it records:
|
||||
|
||||
- `occ`: count of arithmetic-comparison parent enodes (≤, ≥, <, >, =)
|
||||
- `has_lo`, `has_up`, `lo`, `up`: current theory bounds from `arith_value`
|
||||
|
||||
**Ranking (highest priority first):**
|
||||
1. **Higher occurrence count** – more active in constraint network
|
||||
2. **Fully bounded preferred over half-bounded or unbounded**
|
||||
3. **Wider interval** (for fully-bounded variables)
|
||||
4. **Interval contains zero** – as tiebreaker
|
||||
|
||||
Variables whose interval is already a point (`lo == up`) are skipped.
|
||||
|
||||
### AriParti `select_best_var()`
|
||||
|
||||
Uses a `var_info` struct with five keys and a *dynamic key ordering* (`key_rank`) that rotates per node to break ties diversely:
|
||||
|
||||
| Key index | Criterion | Better is… |
|
||||
|---|---|---|
|
||||
| 0 | `m_split_cnt` – global split count | Lower (less-split variables preferred) |
|
||||
| 1 | `m_cz` – interval contains zero | `true` preferred |
|
||||
| 2 | `m_deg` – max polynomial degree | Higher preferred (prioritises nonlinear vars) |
|
||||
| 3 | `m_occ` – occurrence in undecided clauses | Higher preferred |
|
||||
| 4 | `m_width` – interval width (with penalties for unbounded) | Wider preferred |
|
||||
|
||||
Key ordering for a child node is derived from its parent's `key_rank` by rotating one position whenever the parent's ranking had consecutive equal keys; this diversifies splits across the tree.
|
||||
|
||||
Variables that are fully determined (`lower == upper`), Boolean (`m_is_bool`), or defined (`m_defs[x] != nullptr`) are excluded.
|
||||
|
||||
**Unbounded width penalties (AriParti only):**
|
||||
- Fully unbounded: `width = 1024²`
|
||||
- Half-bounded (`(-∞, u]`): `width = 1024 + u` (if `u ≥ 0`), or `width = 1024 / max(1, -u)` (if `u < 0`)
|
||||
- Half-bounded (`[l, ∞)`): symmetric formula
|
||||
|
||||
---
|
||||
|
||||
## Midpoint Computation
|
||||
|
||||
Both implementations agree on the core zero-split heuristic (AriParti Section 4.2): **if the interval straddles zero, split at 0**.
|
||||
|
||||
| Case | Z3 `get_arith_split_atom()` | AriParti `split_node()` |
|
||||
|---|---|---|
|
||||
| Interval contains 0 | `mid = 0` | `mid = 0` |
|
||||
| Fully bounded `[lo, up]` | `mid = (lo + up) / 2`; `floor(mid)` for integers | `mid = (lo + up) / 2`; ceiling applied if `width > 10` |
|
||||
| Half-bounded `[lo, ∞)` | `mid = lo` (split at lower bound) | `mid = lo + delta` (`delta = 128`) |
|
||||
| Half-bounded `(-∞, up]` | `mid = up - 1` (int) or `up - 0.5` (real) | `mid = floor(up) - delta` |
|
||||
| Fully unbounded | `mid = 0` | `mid = 0` (via `m_cz = true`) |
|
||||
|
||||
The split produces two branches: `x ≤ mid` and `x > mid` in both cases.
|
||||
|
||||
---
|
||||
|
||||
## Node / Leaf Selection
|
||||
|
||||
### Z3
|
||||
|
||||
Workers call `batch_manager::get_cube()`, which calls `search_tree::activate_node()` and `find_active_node()`. The search tree uses a simple work-stealing model: each worker tries to continue the node it last worked on; if unavailable, it picks any open node. There is no explicit priority between open nodes.
|
||||
|
||||
### AriParti
|
||||
|
||||
Uses a **priority heap** (`m_leaf_heap`, ordered by `node_info::operator<`):
|
||||
|
||||
1. **Lowest depth first** – broader, shallower problems are split first
|
||||
2. **Most undecided clauses** – more constrained nodes processed first
|
||||
3. **Most undecided literals**
|
||||
4. **Lowest node ID** (earlier-created nodes preferred as tiebreaker)
|
||||
|
||||
This gives AriParti more control over the shape of the partitioning tree.
|
||||
|
||||
---
|
||||
|
||||
## Post-Split Processing
|
||||
|
||||
| Aspect | Z3 | AriParti |
|
||||
|---|---|---|
|
||||
| Bound propagation after split | None immediately; full SMT check on next `check_cube()` | Immediate BICP (`propagate()`) on both children; inconsistent children are pruned at once |
|
||||
| Inprocessing simplification | Optional `simplify()` after split (configurable, one-shot) | None; each sub-task is a fresh SMT instance |
|
||||
| Learned clause sharing | Yes: units and clauses shared via `batch_manager::collect_clause()` | None: each solver instance is independent |
|
||||
| Backtracking | `batch_manager::backtrack()` annotates nodes in search tree with unsat-cores | Master (`AriParti.py`) propagates `unsat` upward and downward via `push_up` / `push_down` |
|
||||
|
||||
---
|
||||
|
||||
## Boolean Variables
|
||||
|
||||
- **Z3**: When `get_arith_split_atom()` finds no arithmetic variable, it falls back to a VSIDS-style Boolean heuristic: selects the unassigned Boolean variable with the highest product of positive/negative literal activity scores (`m_lit_scores[0][v] * m_lit_scores[1][v]`), then halves both scores.
|
||||
- **AriParti**: `select_best_var()` explicitly skips Boolean variables (`if (m_is_bool[x]) continue`). Boolean case splits are not performed by the partitioner; they occur only inside each external solver instance.
|
||||
|
||||
---
|
||||
|
||||
## Shared Origins and Similarities
|
||||
|
||||
Both implementations are directly inspired by the AriParti paper (Section 4.2):
|
||||
|
||||
1. **Zero-split heuristic**: both preferentially split at 0 when the interval straddles zero.
|
||||
2. **Midpoint bisection**: both use `(lo + up) / 2` for fully-bounded intervals.
|
||||
3. **Occurrence count**: both use the number of arithmetic constraints that mention a variable as a key factor.
|
||||
4. **Interval width**: both prefer variables with wider intervals as a heuristic for "less constrained" variables.
|
||||
5. **Binary tree structure**: both build a binary case-split tree where each split adds exactly two child nodes.
|
||||
6. **Arithmetic-only primary heuristic**: both focus exclusively on arithmetic (Int/Real) variables for the primary split decision.
|
||||
|
||||
The Z3 implementation (`get_arith_split_atom()`) was explicitly added to `smt_parallel.cpp` as an "AriParti-style arithmetic interval split" (see comment at line 543–549), making it a direct re-implementation of the core idea from the AriParti paper within Z3's parallel SMT framework.
|
||||
|
||||
---
|
||||
|
||||
## Key Differences Summary
|
||||
|
||||
| Dimension | Z3 `smt_parallel.cpp` | AriParti |
|
||||
|---|---|---|
|
||||
| **Architecture** | Shared-memory threads inside Z3 | Distributed processes with IPC |
|
||||
| **Variable selection keys** | 3 (occ, width, cz) | 5 (split\_cnt, cz, deg, occ, width) with dynamic ordering |
|
||||
| **Split-count tracking** | Not tracked | Tracked globally; fewer-split vars preferred |
|
||||
| **Polynomial degree** | Not considered | Considered (key 2: higher degree preferred) |
|
||||
| **Boolean fallback** | VSIDS-style score-based | None (Boolean vars skipped entirely) |
|
||||
| **Unbounded width** | Sentinel `−1`; fully-bounded strictly preferred | Penalty values (1024, 1024²) enable ranking across all cases |
|
||||
| **Split delta (semi-unbounded)** | `1` (int) / `0.5` (real) | `128` (fixed `m_split_delta`) |
|
||||
| **Node priority** | Work-stealing, no explicit ordering | Priority heap (depth, undecided clauses, undecided literals) |
|
||||
| **Post-split propagation** | None until full SMT check | Immediate BICP; infeasible children pruned instantly |
|
||||
| **Clause learning across workers** | Yes (shared via batch\_manager) | No (each solver is isolated) |
|
||||
| **Inprocessing** | Optional (`m_inprocessing` flag) | None (whole new sub-task per child) |
|
||||
| **SLS portfolio** | Yes (optional parallel SLS worker) | No |
|
||||
|
||||
---
|
||||
|
||||
## Source Locations
|
||||
|
||||
| Component | File |
|
||||
|---|---|
|
||||
| Z3 arithmetic split | `src/smt/smt_parallel.cpp`, `worker::get_arith_split_atom()` (lines 414–534) |
|
||||
| Z3 Boolean split fallback | `src/smt/smt_parallel.cpp`, `worker::get_split_atom()` (lines 537–570) |
|
||||
| Z3 search tree split | `src/smt/smt_parallel.cpp`, `batch_manager::split()` (lines 342–358) |
|
||||
| AriParti variable selection | `src/partitioner/src/math/subpaving/subpaving_t_def.h`, `select_best_var()` (lines 2354–2421) |
|
||||
| AriParti var\_info ranking | `src/partitioner/src/math/subpaving/subpaving_t.h`, `struct var_info`, `operator<` (lines 453–519) |
|
||||
| AriParti split\_node | `src/partitioner/src/math/subpaving/subpaving_t_def.h`, `split_node()` (lines 2516–2610) |
|
||||
| AriParti node priority | `src/partitioner/src/math/subpaving/subpaving_t.h`, `struct node_info`, `operator<` (lines 430–451) |
|
||||
| AriParti master orchestration | `src/AriParti.py`, `ArithPartition::solve()` and `push_up()` / `push_down()` |
|
||||
|
|
@ -24,6 +24,7 @@ Author:
|
|||
#include "ast/simplifiers/then_simplifier.h"
|
||||
#include "smt/smt_parallel.h"
|
||||
#include "smt/smt_lookahead.h"
|
||||
#include "smt/smt_arith_value.h"
|
||||
#include "solver/solver_preprocess.h"
|
||||
#include "params/smt_parallel_params.hpp"
|
||||
|
||||
|
|
@ -410,11 +411,144 @@ namespace smt {
|
|||
return r;
|
||||
}
|
||||
|
||||
expr_ref parallel::worker::get_arith_split_atom() {
|
||||
arith_util a(m);
|
||||
arith_value av(m);
|
||||
av.init(ctx.get());
|
||||
|
||||
// For each arithmetic constant (arity-0 variable of Int/Real sort) collect:
|
||||
// - occurrence count: number of arithmetic-comparison parent enodes
|
||||
// - current theory bounds from arith_value (may be absent for unbounded vars)
|
||||
//
|
||||
// Variables without theory-propagated bounds are still valid split candidates:
|
||||
// they will be split at 0 (AriParti's zero-split heuristic, paper Section 4.2).
|
||||
struct VarInfo {
|
||||
unsigned occ = 0;
|
||||
bool has_lo = false, has_up = false;
|
||||
rational lo, up;
|
||||
bool lo_strict = false, up_strict = false;
|
||||
};
|
||||
obj_map<expr, VarInfo> vars;
|
||||
|
||||
for (enode *n : ctx->enodes()) {
|
||||
expr *e = n->get_expr();
|
||||
if (!is_app(e))
|
||||
continue;
|
||||
if (to_app(e)->get_num_args() != 0)
|
||||
continue; // only 0-arity constant declarations
|
||||
if (!a.is_int_real(e))
|
||||
continue;
|
||||
VarInfo &info = vars.insert_if_not_there(e, VarInfo{});
|
||||
for (enode *p : n->get_parents()) {
|
||||
expr *pe = p->get_expr();
|
||||
if (a.is_le(pe) || a.is_ge(pe) || a.is_lt(pe) || a.is_gt(pe) ||
|
||||
m.is_eq(pe))
|
||||
++info.occ;
|
||||
}
|
||||
if (info.occ == 0)
|
||||
info.occ = 1;
|
||||
info.has_lo = av.get_lo(e, info.lo, info.lo_strict);
|
||||
info.has_up = av.get_up(e, info.up, info.up_strict);
|
||||
}
|
||||
if (vars.empty())
|
||||
return expr_ref(m);
|
||||
|
||||
// Select the best variable using AriParti's heuristic (Section 4.2):
|
||||
// 1. More occurrences in arithmetic atoms is better.
|
||||
// 2. Among ties, wider interval is better.
|
||||
// 3. Among ties, interval containing zero is better.
|
||||
// Fully-bounded variables are preferred over half-bounded or unbounded
|
||||
// because the interval width is more meaningful.
|
||||
expr *best_term = nullptr;
|
||||
rational best_width = rational(-1);
|
||||
unsigned best_occ = 0;
|
||||
bool best_cz = false;
|
||||
bool best_bounded = false;
|
||||
|
||||
for (auto const &[term, info] : vars) {
|
||||
if (info.has_lo && info.has_up && info.lo >= info.up)
|
||||
continue; // already fixed — nothing useful to split
|
||||
|
||||
bool fully_bounded = info.has_lo && info.has_up;
|
||||
rational width = fully_bounded ? (info.up - info.lo) : rational(-1);
|
||||
bool cz;
|
||||
if (fully_bounded)
|
||||
cz = (info.lo <= rational::zero() && rational::zero() <= info.up);
|
||||
else if (info.has_lo)
|
||||
cz = (info.lo <= rational::zero());
|
||||
else if (info.has_up)
|
||||
cz = (rational::zero() <= info.up);
|
||||
else
|
||||
cz = true; // unbounded: split at 0 is always valid
|
||||
|
||||
bool prefer = !best_term;
|
||||
if (!prefer) {
|
||||
if (info.occ > best_occ)
|
||||
prefer = true;
|
||||
else if (info.occ == best_occ) {
|
||||
if (fully_bounded && !best_bounded)
|
||||
prefer = true;
|
||||
else if (fully_bounded == best_bounded) {
|
||||
if (width > best_width)
|
||||
prefer = true;
|
||||
else if (width == best_width && cz && !best_cz)
|
||||
prefer = true;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (prefer) {
|
||||
best_term = term;
|
||||
best_width = width;
|
||||
best_occ = info.occ;
|
||||
best_cz = cz;
|
||||
best_bounded = fully_bounded;
|
||||
}
|
||||
}
|
||||
if (!best_term)
|
||||
return expr_ref(m);
|
||||
|
||||
VarInfo bi;
|
||||
vars.find(best_term, bi);
|
||||
|
||||
// Compute split midpoint following AriParti Section 4.2.
|
||||
rational mid;
|
||||
if (best_cz) {
|
||||
mid = rational::zero();
|
||||
} else if (bi.has_lo && bi.has_up) {
|
||||
mid = (bi.lo + bi.up) / rational(2);
|
||||
if (a.is_int(best_term))
|
||||
mid = floor(mid);
|
||||
} else if (bi.has_lo) {
|
||||
mid = bi.lo; // split at known lower bound
|
||||
} else if (bi.has_up) {
|
||||
mid = bi.up - rational(1);
|
||||
if (!a.is_int(best_term))
|
||||
mid = bi.up - rational(1, 2);
|
||||
} else {
|
||||
mid = rational::zero();
|
||||
}
|
||||
|
||||
sort *srt = best_term->get_sort();
|
||||
LOG_WORKER(2, " arith split on " << mk_bounded_pp(best_term, m, 2)
|
||||
<< " at " << mid << "\n");
|
||||
return expr_ref(a.mk_le(best_term, a.mk_numeral(mid, srt)), m);
|
||||
}
|
||||
|
||||
expr_ref parallel::worker::get_split_atom() {
|
||||
expr_ref result(m);
|
||||
double score = 0;
|
||||
unsigned n = 0;
|
||||
ctx->pop_to_search_lvl();
|
||||
|
||||
// Try AriParti-style arithmetic interval split first.
|
||||
// This is particularly effective for arithmetic theories (QF_LRA, QF_LIA,
|
||||
// QF_NRA, QF_NIA) where splitting at the midpoint of a variable's current
|
||||
// interval is more informative than a Boolean variable split.
|
||||
expr_ref arith_atom = get_arith_split_atom();
|
||||
if (arith_atom)
|
||||
return arith_atom;
|
||||
|
||||
// Fall back to Boolean variable score-based splitting (VSIDS-style).
|
||||
for (bool_var v = 0; v < ctx->get_num_bool_vars(); ++v) {
|
||||
if (ctx->get_assignment(v) != l_undef)
|
||||
continue;
|
||||
|
|
|
|||
|
|
@ -147,6 +147,7 @@ namespace smt {
|
|||
unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share
|
||||
|
||||
expr_ref get_split_atom();
|
||||
expr_ref get_arith_split_atom();
|
||||
|
||||
lbool check_cube(expr_ref_vector const& cube);
|
||||
void share_units();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue