mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-28 19:38:51 +00:00
Code Activity
22356 commits 74 branches 58 tags 268 MiB
Commit graph

6 commits

Author SHA1 Message Date
Lev Nachmanson
7564ccc3f1
capture row by pointer (#9973) 
Capture row as a pointer as lambda strips the reference and the vector was copied by value in lar_solver!

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-06-27 17:43:08 -07:00
Copilot
39ea5ce8c0
Fix SINGLE_THREAD build: add mk_parallel_tactic stub to parallel_tactical.cpp (#9977) 
The `#ifdef SINGLE_THREAD` block in `parallel_tactical.cpp` only defined
`mk_parallel_tactic2`, leaving `mk_parallel_tactic` (called by
`smt_tactic_core.cpp`, `fd_solver.cpp`, and `inc_sat_solver.cpp`)
undefined — causing linker failures in the ST CI job.

## Changes

- **`src/solver/parallel_tactical.cpp`**: Add `mk_parallel_tactic` stub
inside `#ifdef SINGLE_THREAD` that falls back to `mk_solver2tactic(s)`,
consistent with how other parallel tactics degrade in single-threaded
mode (`par()` → `or_else_tactical`, `par_and_then()` →
`and_then_tactical`):

```cpp
#ifdef SINGLE_THREAD

tactic* mk_parallel_tactic2(solver* s, params_ref const& p) {
    return alloc(non_parallel_tactic2, s, p);
}

tactic* mk_parallel_tactic(solver* s, params_ref const& /* p */) {
    return mk_solver2tactic(s);
}

#else
// ... full parallel implementation
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
 2026-06-27 10:20:11 -06:00
Nikolaj Bjorner
612fab1c9a
Parallel tactic (#9824) (#9825) 
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>
 2026-06-26 10:36:15 -06:00
Nikolaj Bjorner
92065462b4 use std::exception as base class to z3_exception 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-04 11:08:15 -08:00
Nikolaj Bjorner
b700dbffce fix #6528 2023-01-10 14:42:23 -08:00
Nikolaj Bjorner
fcea32344e add missing tactic descriptions, add rewrite for tamagochi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-08 13:32:26 -08:00
Renamed from src/solver/parallel_tactic.cpp (Browse further)