mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-23 00:50:29 +00:00
Code Activity
22322 commits 76 branches 58 tags 263 MiB
Commit graph

28 commits

Author SHA1 Message Date
Ilana Shapiro
c798213d87 restore invalid atom case: Path atoms now get rejected in the retry loop and removed from the candidate pool, same as global backbone/negation rejections. 2026-06-20 22:08:58 -07:00
Ilana Shapiro
868b5eeaa7 some bugfixes: Avoid updating max_conflicts through params in the parallel tactic path. Expose direct conflict-limit setters on solver wrappers and use them for SMT and incremental SAT solvers. Also restore single-candidate non-lookahead cube selection to match the parallel split heuristic, specifically do the filtering for invalid atoms during split atom selection. this requires new params so we have a separate get_split_atoms function for now. 2026-06-20 22:06:00 -07:00
Ilana Shapiro
37f02a28f3 fix param copy bug when setting conflicts, fix exception handling in the tactic, and fix some bugs with how we're chooseing split atoms in the cube function 2026-06-20 18:28:12 -07:00
Ilana Shapiro
f86feab060 attempt to fix lease cancel/reslimit race condition in worker 2026-06-20 16:58:11 -07:00
Nikolaj Bjorner
41471bbc3e add comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-17 17:45:02 -06:00
Ilana Shapiro
b5a3d4fcb0 clean up but dangerous race condition is still present in the worker. an example: 
1. Manager decides worker’s lease is stale.
  2. It records/sends lease cancel.
  3. Worker finishes naturally before observing
  4. Worker releases/discards old lease.
  5. The lease-cancel counter is still sitting on the worker limit.
  6. Later, a naked m.inc() check sees that stale cancel and treats it as global cancellation.
 2026-06-16 21:50:52 -07:00
Ilana Shapiro
5c8cbaea3a Handle cancellation for parallel leases 2026-06-16 20:15:10 -07:00
Ilana Shapiro
c10e7c2a6f attempt at lease policy patch 2026-06-16 20:13:33 -07:00
Nikolaj Bjorner
fc5e4d7557 check for lease expiration before checking for m.inc() 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-15 16:00:26 -06:00
Nikolaj Bjorner
48ae786c4c catch exceptions from cube and backbone calls. They can throw 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-15 14:02:43 -06:00
Nikolaj Bjorner
2b9b9a9623 log exceptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-15 10:28:52 -07:00
Nikolaj Bjorner
4237f9d86b log exceptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-15 10:03:46 -07:00
Nikolaj Bjorner
4dbd592137 guard cancelation behind !m.inc() 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-14 23:56:48 -07:00
Ilana Shapiro
778760ec98 Merge branch 'solver_parallel' of github.com:Z3Prover/z3 into solver_parallel 2026-06-14 23:32:32 -07:00
Ilana Shapiro
be1b2f6e15 normalize parallel params 2026-06-14 23:31:47 -07:00
Nikolaj Bjorner
e95f9757c9 lipstick 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-14 22:38:40 -07:00
Nikolaj Bjorner
26f7ce23b6 lipstick 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-14 22:29:33 -07:00
Nikolaj Bjorner
38a8644ae3 avoid double cancel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-14 22:24:21 -07:00
Ilana Shapiro
fc3892486c fix cancel bugs and remove smt_parallel_params 2026-06-14 19:55:28 -07:00
Nikolaj Bjorner
84a3c8789f fix scoping for functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-14 14:06:48 -07:00
Nikolaj Bjorner
96092b196c add exception handling in case run method throws 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-14 13:46:29 -07:00
Nikolaj Bjorner
f2270d4654 make sure split atoms are not already used on the path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-13 17:01:09 -07:00
Nikolaj Bjorner
bcbfeec6c0 address deadlock in cancellation path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-13 08:32:34 -07:00
Nikolaj Bjorner
864c6a3f34 remove get/set max conflicts from solver, handle it using updt_params and get_params. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-12 18:34:08 -07:00
Nikolaj Bjorner
e06ca1489e remove parallal_stats 2026-06-11 14:51:28 -07:00
Nikolaj Bjorner
6ef8660adb
Parallel tactic (#9824) 
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
 2026-06-11 09:14:00 -07:00
Copilot
5fa7d6d63d
Simplify parallel_tactical2.cpp for naming consistency and minor expression cleanup (#9526) 
This updates `src/solver/parallel_tactical2.cpp` with targeted
simplifications to align style and reduce local verbosity without
changing solver behavior. The changes are limited to member naming
consistency, cast style consistency, and a small `expr_ref` construction
cleanup.

- **`batch_manager` member naming consistency**
- Renamed the two outlier private fields to follow the existing `m_`
convention:
    - `shared_clause_trail` → `m_shared_clause_trail`
    - `shared_clause_set` → `m_shared_clause_set`
- Updated all corresponding reads/writes in clause collection, reset,
and clause-return paths.

- **Cast style consistency**
- Replaced C-style cast in thread count calculation with
`static_cast<unsigned>(...)` for consistency with style already used in
the file.

- **Simplified `expr_ref` construction in cube assembly**
- Collapsed default-init + assignment into direct construction when
pushing cube literals.

```cpp
// Before
expr_ref lit(g2l.to());
lit = g2l(cur->get_literal().get());
cube.push_back(std::move(lit));

// After
cube.push_back(expr_ref(g2l(cur->get_literal().get()), g2l.to()));
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-05-13 16:57:52 -04:00
Copilot
85465dcc66
Add parallel_tactical2.cpp: portfolio parallel solver using the solver API (#9515) 
* add parallel_tactical2.cpp: portfolio parallel solver using solver API

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/8b3749c7-5957-41aa-85b5-2d76d4780d61

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* address code review: cap conflict growth, clarify cube/split comments, use mk_or for conflict clause

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/8b3749c7-5957-41aa-85b5-2d76d4780d61

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-05-12 21:19:27 -04:00