## Summary
Adds a global configuration parameter **`suppress_platform_verbose`**
(bool, default `false`).
When set to `true`, memory and time information is suppressed from
verbose output — the same behavior as the `-V` flag proposed in #10301,
but driven by a global parameter instead of a dedicated command-line
switch. This yields deterministic, platform-independent verbose output
that is useful for testing and diffing.
Usage:
```
z3 -v:2 suppress_platform_verbose=true problem.smt2
```
## Approach
Instead of introducing a `-V` command-line flag (#10301), this registers
`suppress_platform_verbose` as a global parameter via `env_params`,
wired to a lightweight `get_suppress_platform_verbose()` flag in `util`.
Verbose output sites guard only their **memory** (`mem_stat`) and
**time** (`m_watch` / `:time` / `:before-memory` / `:after-memory`)
fields on this flag. Platform-independent counters (e.g. `:cost`,
`:threshold`, `:elim-vars`) are always emitted.
Affected sites:
- SAT: asymm-branch, probing, scc, simplifier (subsumer /
blocked-clauses / resolution), solver stats (`sat.stats`, `:memory`,
`mk_stat`)
- SMT: context stats (`smt.stats`)
- Tactic report (`:time`, `:before-memory`, `:after-memory`)
## Validation
- Release build succeeds.
- `suppress_platform_verbose` appears in `z3 -pd` with the correct
type/default, and is accepted on the command line.
- All 93 `test-z3 /a` unit tests pass.
Closes the need for the `-V` switch in #10301.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
https://github.com/Z3Prover/z3/pull/10284 changed the UNREACHABLE macro
in debug.h to use __builtin_unreachable() to indicate to the compiler
that the
code leading it should be considered unreachable.
In https://github.com/Z3Prover/z3/pull/10295 Copilot figured out that
this was wrong: the unreachable macro makes calls, which shouldn't be
elided, and whose arguments should be evaluated. It partially fixed the
problem by declaring invoke_exit_action to be `[[noreturn]]`. This
eliminated warnings in non-debug builds, but when Z3_DEBUG is enabled,
`UNREACHABLE` ends with an invocation of `INVOKE_DEBUGER()`. This can
call `invoke_debugger()`, which *can* actually return (so it can't be
given the `[[noreturn]]` attribute. So we still get warnings in debug
builds.
This PR fixes those, creating a Z3_unreachable_case macro, which is just
a combination of `UNREACHABLE()` and `Z3_fallthrough`. It uses that in
the places that give warnings.
It seemed better to me to still have these cases have a single macro,
rather than `UNREACHABLE` followed by an explicit `Z3_fallthrough`; this
seemed to me like it would confuse people -- "how can you fall through
if this code is unreachable?" But I'm open to alternative suggestions!
Commit d46fbad3 added `__builtin_unreachable()` to the `UNREACHABLE()`
macro in Clang builds to suppress `-Wimplicit-fallthrough` warnings. In
Release+Clang mode, this causes UB: Clang can legally eliminate the
`invoke_exit_action` call (since reaching `__builtin_unreachable()` is
UB, the compiler assumes the entire branch is dead), so when
`UNREACHABLE()` is actually hit, the function continues with
uninitialized state — producing the segfault observed in the FPA C
example.
## Changes
- **`src/util/debug.h`** — Declare `invoke_exit_action` as
`[[noreturn]]`. This is semantically accurate: the function always
terminates via `exit()` or `throw`, never returning normally. The
`[[noreturn]]` annotation naturally suppresses `-Wimplicit-fallthrough`
after `UNREACHABLE()` without any UB.
- **`src/util/debug.h`** — Remove `__compiler_unreachable` macro and its
use in `UNREACHABLE()`. With `[[noreturn]]` on `invoke_exit_action`, it
is redundant.
- **`src/util/debug.cpp`** — Add `[[noreturn]]` to the
`invoke_exit_action` definition to match.
```cpp
// Before (broken in Release+Clang: UB allows optimizer to eliminate invoke_exit_action)
# define UNREACHABLE() { notify_assertion_violation(...); invoke_exit_action(ERR_UNREACHABLE); }; __builtin_unreachable()
// After (invoke_exit_action is [[noreturn]], no UB)
# define UNREACHABLE() { notify_assertion_violation(...); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0)
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This PR enable the "-Wimplicit-fallthrough" warning, then fix all the
warnings this gets
in the clang build, by:
* Augmenting UNREACHABLE to add __builtin_unreachable(), which
suppresses
warnings for fallthrough in that cse.
* Adding Z3_fallthrough in many cases, to make it clear that
fallthroughs are intentional.
* Adding [[noreturn]] to functions that throw, so the compiler knows
they don't fall through to the next case.
* In a couple of cases, there's a fall-through to a default case, which
does "break", or "return nullptr". In those cases, I duplicated the
action in the preceding case, to make it more self-contained, and robust
in the face of change.
In some cases, I am concerned about whether the warnings are identifying
real bugs. For example, the fall-throughs in these files seem at least a
little suspect:
nnf.cpp
seq_rewriter.cpp
lar_solver.cpp
while very probably correct, also seem at least a tiny bit suspect.
However, this PR does *not* attempt to change any behavior, only to
silence the warnings. It would be great if somebody with more knowledge
of the code could vet these cases. If vetted, the explicit presence of
the Z3_fallthrough would reassure future readers of the code that the
fall-through is intentional, not accidental.
`memory_max_size` OOMs were recoverable at `check_sat` time
(`Z3_L_UNDEF` + error handler), but `Z3_solver_reset` could still
terminate the process with an uncaught `out_of_memory_error`. This
change keeps reset on the C API error-reporting path instead of letting
teardown allocations trip the same hard limit.
- **Reset path hardening**
- `Z3_solver_reset` now performs solver teardown under a temporary
suspension of the global memory cap, then restores the previous cap
afterward.
- This avoids aborts when allocator accounting is still above
`memory_max_size` at reset time.
- **Memory manager support**
- Added `memory::get_max_size()` to snapshot/restore the active cap
precisely.
- **Regression coverage**
- Extended `src/test/memory.cpp` with a focused scenario that trips
`Z3_MEMOUT_FAIL` and then calls `Z3_solver_reset` under a non-throwing
error handler, covering the previously aborting recovery path.
```cpp
struct scoped_memory_limit_reset {
size_t m_prev_max;
scoped_memory_limit_reset(): m_prev_max(memory::get_max_size()) {
memory::set_max_size(0);
}
~scoped_memory_limit_reset() {
memory::set_max_size(m_prev_max);
}
} scoped_max_memory;
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10250
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Building Z3 on Windows with MinGW (`mingw-w64-ucrt-x86_64-gcc`) fails
with undefined references to `SymSetOptions`, `SymInitialize`,
`SymFromAddr`, and `SymGetLineFromAddr64` from the DbgHelp library used
in `src/util/debug.cpp` for stack backtraces.
The existing `#pragma comment(lib, "dbghelp.lib")` in `debug.cpp` is an
MSVC-only extension — MinGW silently ignores it, so `dbghelp` is never
passed to the linker.
## Changes
- **`CMakeLists.txt`**: Append `dbghelp` to `Z3_DEPENDENT_LIBS` in the
`WIN32` platform block. This feeds the library to both the `libz3` and
`shell` link steps regardless of compiler.
- **`src/util/debug.cpp`**: Guard the `#pragma comment` with `#ifdef
_MSC_VER` to make the MSVC-only intent explicit.
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10171
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
…icts
Add core::optimize_nl_bounds() (gated by arith.nl.optimize_bounds) which
runs LP max/min over monomial leaf variables inside core::propagate(),
analogous to solver=2's max_min_nl_vars, so nla (arith.solver=6) can
detect cross-nested conflicts previously missed. Collect improved bounds
first, then apply them and re-establish feasibility once; reconcile the
core solver via find_feasible_solution before the raw maximize solves to
preserve inf_heap_is_correct(). Skip null witnesses in
get_dependencies_of_maximum for implied/unconditional bounds.
On FStar-UInt128-divergence solver=6 this yields unsat in 2
final-checks, seed-insensitive (seeds 1-10).
Copilot-Session: ac36bb84-de91-4e6c-86df-6008c7396ceb
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: ac36bb84-de91-4e6c-86df-6008c7396ceb
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This PR completes the job started by
https://github.com/Z3Prover/z3/pull/10169. It adds `-Wextra-semi` to the
set of CLANG_ONLY_WARNINGS, and adds
```
START_DISABLE_EXTRA_SEMI_WARNING;
...macro invocations with trailing semis...
END_DISABLE_WARNING;
```
around all the blocks of macro invocations that provoked warnings.
(Additionally, in realclosure.h, there was one block of macro
invocations that did *not* follow the trailing-semi pattern; changed
that to look like all the others).
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
https://github.com/Z3Prover/z3/pull/10020 deleted a number of
unnecessary (and, by a strict interpretation, illegal) semicolons. These
were detected by adding -Wextra-semi to CLANG_ONLY_WARNINGS during
testing. The PR did not eliminate all such unnecessary/illegal
semi-colons; Nikolaj Bjorner argued that some IDEs would be confused by
doing so for macro invocations, which otherwise look like function
calls. So it left those, and did not include adding -Wextra-semi to
CLANG_ONLY_WARNINGS in the PR.
I'm worried that not having -Wextra-semi will allow instances of the
semis we'd like to eliminate to creep back in. This PR introduces a
mechanism to disable the warnings for regions with such macro
invocations, and uses that mechanism for one file. If accepted, a
subsequent PR would use this mechanism in all the remaining places, so
that there is a clean clang build with -Wextra-semi.
I verified that:
* It compiles cleanly for if the enable/disable macros have null
definitions, as they would for non-clang compilations.
* It compiles cleanly for a clang build without -Wextra-semis.
* It compiles successfully, albeit with *many* warnings, for a clang
build with-Wextra-semis -- but none of those errors are for the regions
in ast.h where the warning is disabled.
`string_hash`'s tail-byte handling reads bytes through plain `char`,
whose signedness is implementation-defined. On signed-char platforms
(x86_64 Linux, macOS) bytes ≥ `0x80` are sign-extended before entering
the hash state (e.g. `c+=((unsigned)data[10]<<24);` becomes `c +=
0xFF80xxxx` instead of `c += 0x0080xxxx`); on unsigned-char platforms
(Linux aarch64) they are not. Hashes of byte strings containing such
bytes therefore differ across platforms.
This is not just cosmetic: `mpz_manager::hash` feeds the digit arrays of
large numerals through `string_hash`, so AST hashes of bit-vector
constants like `(_ bv36028797018963968 64)` (= 2^55, whose digit bytes
include `0x80`) differ between architectures. AST hashes determine hash
table layouts throughout the solver, so preprocessing and search take
platform-dependent paths for byte-identical input.
Observed impact (Z3 4.15.3 release binaries as well as local gcc-13
builds, identical `.smt2` input generated by CBMC from the
[mldsa-native](https://github.com/pq-code-package/mldsa-native)
verification suite — quantifiers + arrays + bit-vectors, ~120k lines):
| instance | x86_64 | aarch64 |
|---|---|---|
| instance A | 643 s | 11.7 s |
| instance B | 22.8 s | 1578 s |
Tracing AST construction on both hosts showed the first divergence at
the registration of the numeral `2^55`, whose node hash was `2587296535`
on x86_64 vs `808470355` on aarch64, with identical mpz digit arrays;
from that point on, hash table iteration orders (and consequently
`ctx-simplify` steps, quantifier instantiation order, and case-split
order) diverge. With this patch, instance A solves in ~21 s on x86_64
(down from 643 s), matching the aarch64 behaviour class.
The fix casts the tail bytes to `unsigned char`, matching the
4-byte-chunk path (which is already signedness-independent via `memcpy`
into `unsigned`). Note that hash values on signed-char platforms change
for inputs containing bytes ≥ `0x80` (pure-ASCII symbol names are
unaffected).
(Found while investigating cross-platform proof-time instability
reported in diffblue/cbmc#8991.)
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Large Python bitvector workloads were hitting a sharp performance cliff
during `Solver.add(...)`, consistent with severe hash-table clustering
in expression-heavy assertion paths. The issue was sensitive to input
size/alignment, indicating weak low-bit dispersion in hash combination.
- **Hash mixing update (`src/util/hash.h`)**
- Replaced the old `combine_hash(h1, h2)` arithmetic/xor sequence with
stronger mixing:
- boost-style combine step
- `hash_u(...)` finalization
- Goal: improve low-bit entropy used by chained hash-table bucket
selection under aligned/high-volume AST patterns.
- **Regression guard and A/B comparison (`src/test/chashtable.cpp`)**
- Added `tst_combine_hash_low_bits()` and invoked it from
`tst_chashtable()`.
- The test stresses aligned first components (`i << 12`) combined with a
fixed seed.
- Added an in-test comparison between the **old** and **new** pairwise
hash combiners and validates:
- reduced collision counts for low-bit projections (8-bit and 16-bit
suffixes),
- improved low-bit uniformity for 8-bit and 16-bit suffixes,
- reported prefix/suffix uniformity metrics (high/low 8 and 16 bits) for
visibility in test output.
```cpp
static inline unsigned combine_hash(unsigned h1, unsigned h2) {
h1 ^= h2 + 0x9e3779b9 + (h1 << 6) + (h1 >> 2);
return hash_u(h1);
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Details in original PR: https://github.com/Z3Prover/z3/pull/10007
---------
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Can Cebeci <can.cebeci99@gmail.com>
Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This is a second version of https://github.com/Z3Prover/z3/pull/9957. I
address @NikolajBjorner 's comments about not changing the semicolons
after macro invocations, because some editors work better with them
present. It now, to the best of my ability, only deletes semis:
* after the closing brace of namespace decl.
* after the closing brace of an extern "C" decl.
* after a function definition.
This PR is very large, but it consists entirely of deletions of
semicolons in these situations.
(If there was a way to update the previous PR, which had been closed,
and that is preferable, please let me know. I couldn't figure it out.)
## Summary
Follow-up to #10001 addressing @NikolajBjorner's review comment:
> isn't this nearly identical AI generated code to the other file? There
has to be some modular approach to deal with sorting vectors?
#10001 introduced two nearly-identical copies of a bounds-safe,
mutation-aware index-permutation merge sort:
- `algebraic_numbers.cpp::merge_sort_roots_perm`
- `nlsat/levelwise.cpp::merge_sort_perm`
Both exist because the comparator (`anum_manager::compare`/`lt`) is
**not pure**: it mutates the algebraic numbers it compares (refining
isolating intervals) and may throw on the resource limit, which makes
`std::sort` undefined behavior (the original SIGSEGV).
## Change
Extract the algorithm into a single shared helper
`util/index_sort_with_mutations.h` (`stable_index_merge_sort`). The long
rationale for why `std::sort` is unsafe and merge sort is safe now lives
in exactly one place. Both call sites become thin wrappers that build
the scratch buffer and forward their local comparator.
No behavioral change: same stable O(n log n) merge sort over an index
permutation.
## Verification
CMake/Ninja Release build:
- `test-z3 /seq algebraic_numbers` — PASS
- `test-z3 /seq algebraic` — PASS
- NRA/NIA smoke solves with `nlsat.lws=true` return expected sat/unsat.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add new parallel algorithm as a tactic (parallel_tactical2.cpp)
Don't port over old experiments from smt_parallel that we aren't using
(sls, inprocessing, failed_literal_mode for bb detection)
Fix bugs: lease cancellation/reslimit race condition, involves changing
lease epoch to simple boolean flag
Also, now there is a single shared set of params for the tactic and
smt_parallel
**Test runs for the parallel_tactical2 vs old smt_parallel version:**
run-2747-Z3-threads-4-qflia-30s-stats.md
run-2746-Z3-threads-4-qflia-30s-parallel_tactic-stats.md
run-2745-Z3-threads-1-qfbv-30s-stats.md
run-3013-Z3-threads-4-qfbv-30s-parallel_tactic-stats.md --> note this is
indeed run-3013, I reran after a bugfix in inc_sat_solver
run-2743-Z3-threads-4-qfnia-30s-stats.md
run-2742-Z3-threads-4-qfnia-30s-parallel_tactic-stats.md
**Test runs for the new smt_parallel with bugfixes:**
run-2801-Z3-threads-4-qflia-30s-smtparallel-bugfixes-stats.md,
run-2800-Z3-threads-4-qflia-30s-smtparallel-bugfixes-stats.md
run-2797-Z3-threads-4-qfnia-30s-smtparallel-bugfixes-stats.md
compare to old smt_parallel:
run-2747-Z3-threads-4-qflia-30s-stats.md
run-2743-Z3-threads-4-qfnia-30s-stats.md
Note that there is a slight regression on lia in run-2800. The source of
this appears to be the new new LP largest-cube LIA heuristic param,
which is enabled by default. disabling this param in run-2801 restored
performance (I didn't change this in this PR though, just something to
note)
http://mtzguido.tplinkdns.com:8081/z3/compare_stats.html
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Implemented the largest cube heuristic from Bromberger and Weidenbach's
paper on cubes. Also fixes an overflow bug in mzp.
Use vswhere to find the visual studio version on windows in the build's ymls.
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Homebrew upgrade from Z3 4.15.4 to 4.16.0 failed on macOS 12 during
`src/ast/ast.cpp` compilation because `obj_map::key_data` was used with
`(key, value)` construction but only implicit constructors existed. This
surfaced at `m_poly_roots.insert(new_node, new_node)` and similar map
operations.
- **Root cause addressed**
- `obj_map<Key, Value>::key_data` relied on implicit constructors, which
are insufficient under stricter toolchains when `key_data(k, v)` /
`key_data(k)` are instantiated via `obj_map` helpers.
- **Code change (minimal, targeted)**
- Added explicit struct constructors in `src/util/obj_hashtable.h` for:
- default initialization
- key-only construction (`key_data(Key* k)`)
- key + lvalue value (`key_data(Key* k, Value const& v)`)
- key + rvalue value (`key_data(Key* k, Value&& v)`)
- No behavioral changes to map semantics; this only makes existing call
sites well-formed across compilers.
- **Example of the change**
```c++
struct key_data {
Key * m_key = nullptr;
Value m_value;
key_data() = default;
key_data(Key* k): m_key(k) {}
key_data(Key* k, Value const& v): m_key(k), m_value(v) {}
key_data(Key* k, Value&& v): m_key(k), m_value(std::move(v)) {}
// ...
};
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Z3's -T measures wall clock time, whereas `ulimit -t` measures CPU time.
Currently, an expired ulimit timeout crashes Z3 without printing
statistics; this patch makes it react cleanly (just as if it has
encountered a regular timeout) to SIGXCPU, the signal that ulimit sends
before sending SIGKILL.
Recent GCC builds report two warning classes in core codepaths: a
possible uninitialized read in `bound_propagator::relevant_bound`, and
repeated `-Warray-bounds` diagnostics in `mpz_manager::get_sign_cell`
when materializing small integers into a reserved `mpz_cell`.
- **Warning cleanup in bound propagation**
- Initialize `interval_size` at declaration in
`src/ast/simplifiers/bound_propagator.cpp` so the compiler can prove
safety across templated `LOWER/UPPER` instantiations using `std::clamp`.
- Preserves existing control flow and refinement heuristics (`bounded`
remains the gate for interval-based logic).
- **Warning cleanup in mpz small-value cell materialization**
- In `src/util/mpz.h`, replace direct writes through `cell->m_digits[0]`
with writes via a derived digits pointer
(`reinterpret_cast<digit_t*>(cell + 1)`), avoiding zero-length
trailing-array indexing diagnostics.
- Keeps memory layout and semantics unchanged for the stack-reserved
`sign_cell` buffer.
- **Representative change**
```cpp
cell = reserve;
cell->m_size = 1;
digit_t* cell_digits = reinterpret_cast<digit_t*>(cell + 1);
cell_digits[0] = a.value() < 0 ? -a.value() : a.value();
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Final version of parallel architecture for FMCAD26 submission (#9475)
* setting up new backbone experiment
* fix phase scores bug
* debug crash from negated atoms
* backbone thread/global backbones in progress, does NOT compile yet
* debug, still need to add backbones worker as a new thread
* setting up complicated condition variable thing for backbones worker thread
* debug
* debug lock contention
* it's a little messy, but change how i'm checking backbones by initiating with batch check
* don't split on global backbones, share global backbones once detected. still need to prune search tree with backbones
* close global backbone branches in search tree
* fix backbone ranking (take average of bb age over cubes and incorporate hits/num cubes the bb appears in
* add stats to backbone experiment
* gate the backbones experiment by local vs global
* update stats and fix bug about unsat core size=1 means global backbone
* phase negation ablation
* unforce phase ablation
* reset ablations
* add todo notes
* fix backbone aging
* first draft of Janota Alg 7
* process exactly 10 bb candidates in each batch
* fixing the Janota algorithm
* add backbone stats for Janota algorithm
* fix bug about global backbones not being checked unless local is also true
* hopefully fix bug about closing global backbones in search tree
* fix another bug in janota alg
* report random seed for debug
* print random seed for debug
* refactor janota alg code, still can't repro the crash
* fix some bugs in the janota algorithm
* try to fix weird memory leak thing with ramon/linux
* revert fix, it didn't work
* add second backbones thread
* increase chunk size when undef
* fix how the 2 backbone threads work on batches (they each race to finish the same batch). this was very complicated to code due to thread synchronization and while it runs there may be bugs
* update how we report stats for backbones
* first draft of doing the bb threads in neg and pos mode, needs revising
* fix some bugs in the positive version of the bb check, still need to review
* debug some more things in the positive bb worker
* keep bb candidates sorted, increase batch and chunk size
* try to resolve a couple of bugs
* fix very bad bug about backbones workers not doing anything
* ablate positive backbone thread
* fix how we record backbones in positive mode (shouldn't impact previous run)
* clarify code about adding found backbones
* add back the positive bb thread
* try to fix the random segfault bug + ablate the postiive bb thread again
* clean up logs
* share clauses with bb threads
* fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* resolve deadlock
* add comment about SAT bb case
* todo comments
* complete TODOs in code, still need to debug bb threads
* debug bb threads, add bb_positive thread back in
* ablate bb_positive thread
* style
* configure num bb threads as param
* enable sat and unsat mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove while true
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updates
* try to fix rewriter_exception bug
* possibly reduce code under lock when only 1 bb thread
* add some copilot-suggested optimizations
* add copilot suggestions to fix condition variable synchronization with bb threads
* revert changes that are too messy with the code
* ablate collect clauses
* ablate condition variable logic changes
* ablate reset batch
* revert ablation
* remove m_batch_in_progress that makes the bb threads wait until both have exited the batch after one signals cancel (can be long if one is stuck in ctx check)
* sharing theory lemmas
* finish setup for search tree thread modes, and fix local bb setup to pull from the global pool
* variable renames
* update bb hyperparams after copilot (hopefully??) ran tuning experiments
* fix possible AST manager bug
* ablate collect clauses
* remove bb collect shared clauses
* fix local bb experiment bug and reinstate collect clauses for global bb
* local bb cands are thread-local ablation
* remove thread-local local bb ablation
* fix bug in nonthread-local bb experiment
* fix more nonthreadlocal bb bugs
* try to fix local bb bug
* AST manager mismatch bugfix
* attempt to fix another canonicalization bug
* try another bugfix
* try another bugfix
* try yet another bugfix
* thread local bb ablation
* ablate force phase
* ablate set activity
* undo ablations since apparently it's not forcing phase or boosting activities
* remove old experiments
* try guarding m_birthdate size
* try to fix several bugs including with m_birthdate initialization and how we're storing original phases
* one more bugfix
* remove local bb experiment after negative signals on experiments, and change bb ranking to VSIDS scores as opposed to phase
* select bb polarity based on phase, not VSIDS
* first attempt with codex. Codex notes:
What changed:
- Each tree node now tracks:
- active worker count
- lease epoch
- cancel epoch
- get_cube() now hands each worker an explicit lease: (node, epoch, cancel_epoch).
- try_split() and backtrack() now operate on that lease, and the batch manager releases the worker’s lease under the tree lock before mutating the
node.
- If another worker closes the leased node or subtree, the batch manager cancels only the workers whose current leased nodes are now closed.
- Workers detect canceled leases after check(), reset their local cancel flag, abandon the stale lease, and continue instead of turning that into a
global exception.
- The “reopen immediately into the open queue” policy is preserved. I did not add a barrier waiting for all workers on a node to finish.
- Active-worker accounting is now separate from the open/active/closed scheduling status, so reopening a node no longer erases the fact that other
workers are still on it.
I also updated search_tree bookkeeping so:
- closure bumps node cancel/lease epochs
- active-node counting uses actual active-worker presence, not just status == active
* fix smts bugfix git merge issues with backtrack
* fix(parallel-smt): gate split/backtrack by lease epoch
What it changes:
- util/search_tree.h
- bumps node epoch on split
- threads epoch through should_split(...) and try_split(...)
- always records effort, but only split/reopen if the lease epoch still matches
- smt/smt_parallel.cpp
- requires is_lease_valid(..., lease.epoch) before backtrack(...)
- passes lease.epoch into m_search_tree.try_split(...)
* clean up code and add some comments
* fix bug about backtracking condition being too strict: The epoch guard should not block backtrack(...) the same way it blocks try_split(...). A stale worker that proves UNSAT for n should still be able to
close n, and that closure should then cancel the other workers on n and its subtree.
I changed smt/smt_parallel.cpp accordingly:
- try_split(...) still uses epoch to reject stale structural splits
- backtrack(...) no longer requires is_lease_valid(..., epoch); it only requires that the lease is not already canceled
So the intended asymmetry is now restored:
- stale split: reject
- stale unsat/backtrack: allow closure, then cancel affected workers
* ablate to no backtracking on stale leases
* fix merge
* revert codex change about exception handling
* fix linux bugs
* ablate backtrack gating
* attempt to fix linux crashes
* ablate backtracking on global bb
* the rare bb bug appears to be from creating the synthetic lease for a bb node and then backtracking on the synthetic lease. this is an attempt to fix it
* clean up code
* try to fix bug about active worker counts/lease accounting. current policy should hold: - stale leases: release/decrement
- canceled leases: do not release/decrement (just ignore since we have an invariant that canceled leases mean closed nodes that are never revisited
* delay premature root activation
* fix major semantic bug about threads continually choosing the root if their lease is reset
* fix cancellation to unknown status
* fix very bad bug about all threads needing to start at the root
* ablate active ranking: now nodes are only reopened if they are truly inactive (active worker count is 0)
* fix some bugs about leases
* ablate adding static effort only
* fix some bugs about leases
* don't explode effort for portfolio nodes
* fix: still accumulate per-node effort, but don't over-accumulate on portfolio solves
* restore dynamically scaled effort
* clean up merge from cherry pick
* tighten which nodes we detect for proven global bb closure (only detect nonclosed nodes)
* fix cancel to unknown exception on bb code
* lease cancellation doens't touch rlimit now, it just sets max conflicts to 0. also fix a VERY BAD BUG about effort never being updated until all leases are done on a node, which meant we never left the root
* cross-thread modification of max conflicts is unsafe, so create an atomic lease canceled variable that's ch
ecked in ctx where max conflicts is also checked
* move atomic lease check in the context to the more global get_cancel_flag function
* Fix new SIGSEV. issue: The root cause: get_cancel_flag() is called from within propagation loops (mid-BCP, mid-equality-propagation, mid-atom-propagation). When it returns true there, the solver exits early and leaves the context in an intermediate state —
propagation queues partially processed, theory state potentially inconsistent with boolean state.
For the global cancel (m.limit().cancel()), this is harmless: the worker exits entirely and the context is destroyed. Intermediate state doesn't matter.
For a lease cancel, the context is reused — the worker gets a new cube and calls ctx->check() again on the same context object. Re-entering check() on a context interrupted mid-propagation causes it to access that corrupted intermediate
state → SIGSEGV.
The m_max_conflicts check is the only checkpoint that's safe for re-entry: it only fires post-conflict-resolution, pre-decision, when propagation queues are empty and theory state is consistent.
Fix: Remove m_lease_canceled from get_cancel_flag(). Keep it only at safe, between-phase checkpoints where the context is in a known-consistent state. The result is two safe checkpoints for m_lease_canceled: after each conflict (post-resolution, queues empty) and before each theory final check (not yet entered the theory). Neither interrupts the solver mid-mutation. The SIGSEGV should be
gone, and NIA performance should improve because long theory final checks (where NIA burns most time) are now preemptable before they start.
* fix new inconsistent theory bug: The problem is returning FC_GIVEUP from inside final_check() after some theories have already run final_check_eh() and pushed propagations into the queue. Those pending propagations reference context state that gets invalidated on the next check() call → SIGSEGV. The fix: check m_lease_canceled before entering final_check() in bounded_search(), never from inside it. That way the context is always in a clean pre-final-check state when we bail out. This is safe: decide() returned false (all variables assigned, no pending propagations), theories haven't been touched yet, context is in a fully consistent state. For NIA, this is still a meaningful win — we avoid entering expensive arithmetic final checks entirely when the lease is already canceled.
* ablate lease cancel check in ctx final theory check due to crash (??)
* gate bb-specific code behind param
* try some possible bugfixes for the sigsev
* ablate some bugfixes
* remove second lease cancel check in smt_context, not sure it's safe. only check where we do the max conflicts check
* restore exception handling logic to master branch
* restore reslimit cancels since the bug appears to be latent
* add bookkeeping for race condition of multiple lease cancels on a single node (messes with reslimit)
* restore unrelated code to master
* restore local bb experiment
* ablate restore local bb phase/activity after search
* undo local bb ablation about resetting phase/activities, and reinstate the shared lemmas of length 2 and 3 experiment
* re-ablate restore local bb phase/activity after search, due to positive experimental signal on smt comp LIA
* change split policy from lightweight proof skeleton to VSIDS. NOTE: enabling local bb will mess with this since we aren't restoring activities right now
* backtrack more aggressively in search tree: close matching external targets (i.e. repeat literals on other branches)
* find_shallowest_timed_out_leaf_depth is now shallowest_unsolved_leaf_depth and is based on num activations > 0, not effort > 0
* fix soundness bug about closing external targets with nontrivial cores
* epoch is no longer needed, just cancel epoch. remove epoch
* core minimize draft, and fix bug in tree expansion policy about shallowest leaf depth needing to be timed out
* core minimization thread (remove search tree worker core min since it was blocking)
* collect shared clauses in core min thread
* bugfixes in core min algorithm
* fix more bugs in core min algorithm
* more core min bugfixes based on feedback and increase m_core_minimize_conflict_budget to 5000 (might need to increase it more for harder SMT COMP problems)
* fix bug in backtrack_unlocked
* fix compiler error
* more core min bugfix from nikolaj
* clean up
* failed literal probe collects shared clauses
* core min thread shares units
* failed literal thread now tests the top 500 global bb cands each round, instead of scanning everything. on QF_LIA/Sz128_2823.smt2 this got us from 51->75 discovered backbones
* remove core minimizer unit sharing (experimentally showed no effect)
* core minimization thread candidate cores are ranked first by depth (deepest->shallowest) then by size (largest->smallest). also, the core's node is set to the deepest node in the core which is not necessarily the search node (slightly semantically stronger). finally, clean up bb/failed literal params
* failed literal probe runs continuously
* fix a lot of things about the FL thread and how bb cands are being processed. also re-add the local bb experiment for ablations
* ablate continuous run on FL thread (up to the max BM examples
* ablate m_max_failed_literal_prioritized_size back to 100
* redesign FL probe again
* ablate FL continuous probe
* reinstate continuous FL probe after positive NIA signal, but also re-add the BM maintaining 1000 bb cands and these are used a
s backups instead of just looping over the top 100 all the time
* change FL thread scheduling to attempt to do less duplicate checks
* restore some old FL behavior
* batch manager dedups global bb cands by atoms, not literals. if we have 2 of the same atom, the polarity with higher rank is kept for the stored bb candidate literal.
* ablations
* reinstate FL check for new batch with epochs, before merge, this is a temp branch
* undo comment out cv call
* restore old changes
* bb batch mode is continuous, with checks for new candidates after the first round
* separate FL probe into 2 threads for pos and neg mode
* attempt to add unit-based bb detection in chunking mode
* add bb detection via workers' units. also rename some variables
* modify the fallback policies for bb detection in batch mode but also in FL mode
* ablate continuous checking for batch bb mode
* major refactor for bb code. we share units and collect them as pruning bb's in all threads now (including core min and bb threads). we always check for units in batch mode now. finally, the batch mode fallback is now FL probing
* bb candidates are atoms, not literals, since we currently test both polarities in parallel.
batch mode retry terminates if we made zero progress after a retry round to avoid resource stress
fix bug about bb ranking being backwards for how we process them
* fix polarity bug for FL mode dedup
* restore polarity-sensitive bb candidate ranking via lits
* ablate sharing non-worker units
* ablate share unit as bb
* ablate incomplete-theory give-up paths
* restore unit sharing as bb collection on workers
* restore incomplete-theory give-up paths
* clean up code
* clean up code
* clean up code
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.lan1>
* add ablate_backtracking experiment
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.lan1>
* setting up new backbone experiment
* fix phase scores bug
* debug crash from negated atoms
* backbone thread/global backbones in progress, does NOT compile yet
* debug, still need to add backbones worker as a new thread
* setting up complicated condition variable thing for backbones worker thread
* debug
* debug lock contention
* it's a little messy, but change how i'm checking backbones by initiating with batch check
* don't split on global backbones, share global backbones once detected. still need to prune search tree with backbones
* close global backbone branches in search tree
* fix backbone ranking (take average of bb age over cubes and incorporate hits/num cubes the bb appears in
* add stats to backbone experiment
* gate the backbones experiment by local vs global
* update stats and fix bug about unsat core size=1 means global backbone
* phase negation ablation
* unforce phase ablation
* reset ablations
* add todo notes
* fix backbone aging
* first draft of Janota Alg 7
* process exactly 10 bb candidates in each batch
* fixing the Janota algorithm
* add backbone stats for Janota algorithm
* fix bug about global backbones not being checked unless local is also true
* hopefully fix bug about closing global backbones in search tree
* fix another bug in janota alg
* report random seed for debug
* print random seed for debug
* refactor janota alg code, still can't repro the crash
* fix some bugs in the janota algorithm
* try to fix weird memory leak thing with ramon/linux
* revert fix, it didn't work
* add second backbones thread
* increase chunk size when undef
* fix how the 2 backbone threads work on batches (they each race to finish the same batch). this was very complicated to code due to thread synchronization and while it runs there may be bugs
* update how we report stats for backbones
* first draft of doing the bb threads in neg and pos mode, needs revising
* fix some bugs in the positive version of the bb check, still need to review
* debug some more things in the positive bb worker
* keep bb candidates sorted, increase batch and chunk size
* try to resolve a couple of bugs
* fix very bad bug about backbones workers not doing anything
* ablate positive backbone thread
* fix how we record backbones in positive mode (shouldn't impact previous run)
* clarify code about adding found backbones
* add back the positive bb thread
* try to fix the random segfault bug + ablate the postiive bb thread again
* clean up logs
* share clauses with bb threads
* fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* resolve deadlock
* add comment about SAT bb case
* todo comments
* complete TODOs in code, still need to debug bb threads
* debug bb threads, add bb_positive thread back in
* ablate bb_positive thread
* style
* configure num bb threads as param
* enable sat and unsat mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove while true
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updates
* try to fix rewriter_exception bug
* possibly reduce code under lock when only 1 bb thread
* add some copilot-suggested optimizations
* add copilot suggestions to fix condition variable synchronization with bb threads
* revert changes that are too messy with the code
* ablate collect clauses
* ablate condition variable logic changes
* ablate reset batch
* revert ablation
* remove m_batch_in_progress that makes the bb threads wait until both have exited the batch after one signals cancel (can be long if one is stuck in ctx check)
* sharing theory lemmas
* finish setup for search tree thread modes, and fix local bb setup to pull from the global pool
* variable renames
* update bb hyperparams after copilot (hopefully??) ran tuning experiments
* fix possible AST manager bug
* ablate collect clauses
* remove bb collect shared clauses
* fix local bb experiment bug and reinstate collect clauses for global bb
* local bb cands are thread-local ablation
* remove thread-local local bb ablation
* fix bug in nonthread-local bb experiment
* fix more nonthreadlocal bb bugs
* try to fix local bb bug
* AST manager mismatch bugfix
* attempt to fix another canonicalization bug
* try another bugfix
* try another bugfix
* try yet another bugfix
* thread local bb ablation
* ablate force phase
* ablate set activity
* undo ablations since apparently it's not forcing phase or boosting activities
* remove old experiments
* try guarding m_birthdate size
* try to fix several bugs including with m_birthdate initialization and how we're storing original phases
* one more bugfix
* remove local bb experiment after negative signals on experiments, and change bb ranking to VSIDS scores as opposed to phase
* select bb polarity based on phase, not VSIDS
* first attempt with codex. Codex notes:
What changed:
- Each tree node now tracks:
- active worker count
- lease epoch
- cancel epoch
- get_cube() now hands each worker an explicit lease: (node, epoch, cancel_epoch).
- try_split() and backtrack() now operate on that lease, and the batch manager releases the worker’s lease under the tree lock before mutating the
node.
- If another worker closes the leased node or subtree, the batch manager cancels only the workers whose current leased nodes are now closed.
- Workers detect canceled leases after check(), reset their local cancel flag, abandon the stale lease, and continue instead of turning that into a
global exception.
- The “reopen immediately into the open queue” policy is preserved. I did not add a barrier waiting for all workers on a node to finish.
- Active-worker accounting is now separate from the open/active/closed scheduling status, so reopening a node no longer erases the fact that other
workers are still on it.
I also updated search_tree bookkeeping so:
- closure bumps node cancel/lease epochs
- active-node counting uses actual active-worker presence, not just status == active
* fix smts bugfix git merge issues with backtrack
* fix(parallel-smt): gate split/backtrack by lease epoch
What it changes:
- util/search_tree.h
- bumps node epoch on split
- threads epoch through should_split(...) and try_split(...)
- always records effort, but only split/reopen if the lease epoch still matches
- smt/smt_parallel.cpp
- requires is_lease_valid(..., lease.epoch) before backtrack(...)
- passes lease.epoch into m_search_tree.try_split(...)
* clean up code and add some comments
* fix bug about backtracking condition being too strict: The epoch guard should not block backtrack(...) the same way it blocks try_split(...). A stale worker that proves UNSAT for n should still be able to
close n, and that closure should then cancel the other workers on n and its subtree.
I changed smt/smt_parallel.cpp accordingly:
- try_split(...) still uses epoch to reject stale structural splits
- backtrack(...) no longer requires is_lease_valid(..., epoch); it only requires that the lease is not already canceled
So the intended asymmetry is now restored:
- stale split: reject
- stale unsat/backtrack: allow closure, then cancel affected workers
* ablate to no backtracking on stale leases
* fix merge
* revert codex change about exception handling
* fix linux bugs
* ablate backtrack gating
* attempt to fix linux crashes
* ablate backtracking on global bb
* the rare bb bug appears to be from creating the synthetic lease for a bb node and then backtracking on the synthetic lease. this is an attempt to fix it
* clean up code
* try to fix bug about active worker counts/lease accounting. current policy should hold: - stale leases: release/decrement
- canceled leases: do not release/decrement (just ignore since we have an invariant that canceled leases mean closed nodes that are never revisited
* delay premature root activation
* fix major semantic bug about threads continually choosing the root if their lease is reset
* fix cancellation to unknown status
* fix very bad bug about all threads needing to start at the root
* ablate active ranking: now nodes are only reopened if they are truly inactive (active worker count is 0)
* fix some bugs about leases
* ablate adding static effort only
* fix some bugs about leases
* don't explode effort for portfolio nodes
* fix: still accumulate per-node effort, but don't over-accumulate on portfolio solves
* restore dynamically scaled effort
* clean up merge from cherry pick
* tighten which nodes we detect for proven global bb closure (only detect nonclosed nodes)
* fix cancel to unknown exception on bb code
* lease cancellation doens't touch rlimit now, it just sets max conflicts to 0. also fix a VERY BAD BUG about effort never being updated until all leases are done on a node, which meant we never left the root
* cross-thread modification of max conflicts is unsafe, so create an atomic lease canceled variable that's ch
ecked in ctx where max conflicts is also checked
* move atomic lease check in the context to the more global get_cancel_flag function
* Fix new SIGSEV. issue: The root cause: get_cancel_flag() is called from within propagation loops (mid-BCP, mid-equality-propagation, mid-atom-propagation). When it returns true there, the solver exits early and leaves the context in an intermediate state —
propagation queues partially processed, theory state potentially inconsistent with boolean state.
For the global cancel (m.limit().cancel()), this is harmless: the worker exits entirely and the context is destroyed. Intermediate state doesn't matter.
For a lease cancel, the context is reused — the worker gets a new cube and calls ctx->check() again on the same context object. Re-entering check() on a context interrupted mid-propagation causes it to access that corrupted intermediate
state → SIGSEGV.
The m_max_conflicts check is the only checkpoint that's safe for re-entry: it only fires post-conflict-resolution, pre-decision, when propagation queues are empty and theory state is consistent.
Fix: Remove m_lease_canceled from get_cancel_flag(). Keep it only at safe, between-phase checkpoints where the context is in a known-consistent state. The result is two safe checkpoints for m_lease_canceled: after each conflict (post-resolution, queues empty) and before each theory final check (not yet entered the theory). Neither interrupts the solver mid-mutation. The SIGSEGV should be
gone, and NIA performance should improve because long theory final checks (where NIA burns most time) are now preemptable before they start.
* fix new inconsistent theory bug: The problem is returning FC_GIVEUP from inside final_check() after some theories have already run final_check_eh() and pushed propagations into the queue. Those pending propagations reference context state that gets invalidated on the next check() call → SIGSEGV. The fix: check m_lease_canceled before entering final_check() in bounded_search(), never from inside it. That way the context is always in a clean pre-final-check state when we bail out. This is safe: decide() returned false (all variables assigned, no pending propagations), theories haven't been touched yet, context is in a fully consistent state. For NIA, this is still a meaningful win — we avoid entering expensive arithmetic final checks entirely when the lease is already canceled.
* ablate lease cancel check in ctx final theory check due to crash (??)
* gate bb-specific code behind param
* try some possible bugfixes for the sigsev
* ablate some bugfixes
* remove second lease cancel check in smt_context, not sure it's safe. only check where we do the max conflicts check
* restore exception handling logic to master branch
* restore reslimit cancels since the bug appears to be latent
* add bookkeeping for race condition of multiple lease cancels on a single node (messes with reslimit)
* restore unrelated code to master
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.lan1>
* first attempt with codex. Codex notes:
What changed:
- Each tree node now tracks:
- active worker count
- lease epoch
- cancel epoch
- get_cube() now hands each worker an explicit lease: (node, epoch, cancel_epoch).
- try_split() and backtrack() now operate on that lease, and the batch manager releases the worker’s lease under the tree lock before mutating the
node.
- If another worker closes the leased node or subtree, the batch manager cancels only the workers whose current leased nodes are now closed.
- Workers detect canceled leases after check(), reset their local cancel flag, abandon the stale lease, and continue instead of turning that into a
global exception.
- The “reopen immediately into the open queue” policy is preserved. I did not add a barrier waiting for all workers on a node to finish.
- Active-worker accounting is now separate from the open/active/closed scheduling status, so reopening a node no longer erases the fact that other
workers are still on it.
I also updated search_tree bookkeeping so:
- closure bumps node cancel/lease epochs
- active-node counting uses actual active-worker presence, not just status == active
* fix(parallel-smt): gate split/backtrack by lease epoch
What it changes:
- util/search_tree.h
- bumps node epoch on split
- threads epoch through should_split(...) and try_split(...)
- always records effort, but only split/reopen if the lease epoch still matches
- smt/smt_parallel.cpp
- requires is_lease_valid(..., lease.epoch) before backtrack(...)
- passes lease.epoch into m_search_tree.try_split(...)
* clean up code and add some comments
* fix bug about backtracking condition being too strict: The epoch guard should not block backtrack(...) the same way it blocks try_split(...). A stale worker that proves UNSAT for n should still be able to
close n, and that closure should then cancel the other workers on n and its subtree.
I changed smt/smt_parallel.cpp accordingly:
- try_split(...) still uses epoch to reject stale structural splits
- backtrack(...) no longer requires is_lease_valid(..., epoch); it only requires that the lease is not already canceled
So the intended asymmetry is now restored:
- stale split: reject
- stale unsat/backtrack: allow closure, then cancel affected workers
* ablate to no backtracking on stale leases
* revert codex change about exception handling
* remove old code
* ablate backtracking gate
* attempt to fix linux crashes
* try to fix bug about active worker counts/lease accounting. current policy should hold: - stale leases: release/decrement
- canceled leases: do not release/decrement (just ignore since we have an invariant that canceled leases mean closed nodes that are never revisited
* delay premature root activation
* fix major semantic bug about threads continually choosing the root if their lease is reset
* fix cancellation to unknown status
* fix very bad bug about all threads needing to start at the root
* ablate active ranking: now nodes are only reopened if they are truly inactive (active worker count is 0)
* fix some bugs about leases
* ablate adding static effort only
* fix some bugs about leases
* don't explode effort for portfolio nodes
* fix: still accumulate per-node effort, but don't over-accumulate on portfolio solves
* restore dynamically scaled effort
* lease cancellation doens't touch rlimit now, it just sets max conflicts to 0. also fix a VERY BAD BUG about effort never being updated until all leases are done on a node, which meant we never left the root
* cross-thread modification of max conflicts is unsafe, so create an atomic lease canceled variable that's ch
ecked in ctx where max conflicts is also checked
* move atomic lease check in the context to the more global get_cancel_flag function
* Fix new SIGSEV. issue: The root cause: get_cancel_flag() is called from within propagation loops (mid-BCP, mid-equality-propagation, mid-atom-propagation). When it returns true there, the solver exits early and leaves the context in an intermediate state —
propagation queues partially processed, theory state potentially inconsistent with boolean state.
For the global cancel (m.limit().cancel()), this is harmless: the worker exits entirely and the context is destroyed. Intermediate state doesn't matter.
For a lease cancel, the context is reused — the worker gets a new cube and calls ctx->check() again on the same context object. Re-entering check() on a context interrupted mid-propagation causes it to access that corrupted intermediate
state → SIGSEGV.
The m_max_conflicts check is the only checkpoint that's safe for re-entry: it only fires post-conflict-resolution, pre-decision, when propagation queues are empty and theory state is consistent.
Fix: Remove m_lease_canceled from get_cancel_flag(). Keep it only at safe, between-phase checkpoints where the context is in a known-consistent state. The result is two safe checkpoints for m_lease_canceled: after each conflict (post-resolution, queues empty) and before each theory final check (not yet entered the theory). Neither interrupts the solver mid-mutation. The SIGSEGV should be
gone, and NIA performance should improve because long theory final checks (where NIA burns most time) are now preemptable before they start.
* fix new inconsistent theory bug: The problem is returning FC_GIVEUP from inside final_check() after some theories have already run final_check_eh() and pushed propagations into the queue. Those pending propagations reference context state that gets invalidated on the next check() call → SIGSEGV. The fix: check m_lease_canceled before entering final_check() in bounded_search(), never from inside it. That way the context is always in a clean pre-final-check state when we bail out. This is safe: decide() returned false (all variables assigned, no pending propagations), theories haven't been touched yet, context is in a fully consistent state. For NIA, this is still a meaningful win — we avoid entering expensive arithmetic final checks entirely when the lease is already canceled.
* remove second lease cancel check in smt_context, not sure it's safe. only check where we do the max conflicts check
* check epoch match in release_lease_unlocked
* restore exception handling logic to master branch
* restore reslimit cancels since the bug appears to be latent
---------
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.lan1>
* Refactor parallel search tree to use global node selection (SMTS-style) instead of DFS traversal.
Introduce effort-based prioritization, allow activation of any open node, and add controlled/gated
expansion to prevent over-partitioning and improve load balancing.
* clean up code
* ablations
* ablations2: effort
* ablations2: activation
* ablations3: more activations
* ablations4: visit all nodes before splitting
* throttle tree size min is based on workers not activated nodes
* ablate random throttling
* ablate nonlinear effort
* clean up code
* ablate throttle
* ablate where add_effort is
* reset
* clean up a function and add comment
---------
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
Reset polynomial cache and assignments in nlsat::solver:👿:clear()
to prevent use-after-free when the solver is destroyed. The missing
resets caused heap corruption when check_assignment's
compute_linear_explanation created cached polynomials and root atoms
that outlived the solver's other data structures during destruction.
Also fix _scoped_numeral_vector copy constructor to read from other
instead of uninitialized self.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
**Root cause**: `vector::resize(SZ s, Args args...)` in `src/util/vector.h` took `args` by value and used `std::forward<Args>(args)` in a loop. The first iteration moved from `args`, leaving all subsequent elements with a moved-from state (`rational{0/0}` instead of
`rational{0/1}`). This corrupted the coefficient vector in the pretty printer, causing a division-by-zero assertion when multiplying.
**Fix**: Changed `resize` to take `Args const& args` and copy-construct each element instead of forwarding/moving.
- Relax restore_x() to handle backup/current size mismatches: when
backup is shorter (new columns added), call
move_non_basic_columns_to_bounds() to find a feasible solution.
- Fix 100x performance regression in nonlinear optimization: save LP
optimum before check_nla and return it as bound regardless of NLA
result, so opt_solver::check_bound() can validate via full re-solve
with accumulated NLA lemmas.
- Refactor theory_lra::maximize() into three helpers: max_with_lp(),
max_with_nl(), and max_result().
- Add mk_gt(theory_var, impq const&) overload for building blockers
from saved LP optimum values.
- Add BNH multi-objective optimization test (7/7 sat in <1s vs 1/7
in 30s before fix).
- Add restore_x test for backup size mismatch handling.
Fixes#8890
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
