3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Commit graph

17 commits

Author SHA1 Message Date
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