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

22328 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ilana Shapiro
e45683de4b add the safe_run pattern from the tactic (which handles external cancel like Ctrl+C safely) to smt_parallel 2026-06-21 15:26:42 -07:00
Ilana Shapiro
293cb384c2 try to apply the lease cancel/reslimit race condition bugfix to smt_parallel from the tactic 2026-06-21 15:18:46 -07:00
Ilana Shapiro
e846b2a9e7 smt_parallel is back to using parallel_params only, removing smt_parallel_params.pyg, legacy params (e.g. inprocessing, sls, failed_literal_mode for bb) are hardcoded 2026-06-21 15:06:23 -07:00
Ilana Shapiro
85fa14774a rejection of invalid split atoms happens DURING selection of split atoms, not as a post-processing step, just like smt_parallel does. this requires changing the shape of the cube function so I've moved this to a second function, cube_vsids, for now and restored the original cube/lookahead functions to master branch. this should hopefully give a perf bump due to eliminating needless postprocessing 2026-06-21 14:58:03 -07:00
Ilana Shapiro
ac12384d00 reinstate legacy params for smt_parallel to use for the regression tests 2026-06-20 23:18:41 -07:00
Ilana Shapiro
6417930af5 clean up 2026-06-20 22:28:02 -07:00
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
e88cac2fe1 restore smt_parallel to old/original version so we have a consistent baseline (even though it still includes newer bugs we've identified) 2026-06-16 21:37:11 -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
dba826039d avoid spurious cancel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-14 23:31:37 -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
5b307545e6 change scheduling in old smt_parallel code to keep it updated 2026-06-14 22:02:00 -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
f2d5d6fecf add set_canceled to smt_parallel to avoid deadlock 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-13 16:13:47 -07:00
Nikolaj Bjorner
491d990ed1 use structured parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-13 08:38:58 -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
81af0cc230 remove atom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-12 10:58:11 -07:00
Nikolaj Bjorner
7f1e74c0da remove atom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-12 10:49:05 -07:00
copilot-swe-agent[bot]
502309f246
Sort cube candidates by activity with tie shuffling 2026-06-12 17:26:55 +00:00
copilot-swe-agent[bot]
af5bbb4566
Restore atom2bool_var.cpp to fix CI build break 2026-06-12 06:37:48 +00:00
copilot-swe-agent[bot]
4b7e4cf08a
Remove const_cast from smt_solver context access 2026-06-12 06:15:29 +00:00
Nikolaj Bjorner
a3f07ba9ab
Update atom2bool_var.cpp 2026-06-11 22:47:32 -07:00
Nikolaj Bjorner
96ac8bfd77 redo priority selection 2026-06-11 16:49:36 -07:00
Nikolaj Bjorner
9485e96416 signatrue update 2026-06-11 15:59:08 -07:00
Nikolaj Bjorner
6b91b5a1dd Merge branch 'solver_parallel' of https://github.com/z3prover/z3 into solver_parallel 2026-06-11 15:54:04 -07:00
Nikolaj Bjorner
deb9fe4240 use bool_var instead of unsigned 2026-06-11 15:53:44 -07:00
Nikolaj Bjorner
49d725f477 refactor 2026-06-11 15:40:38 -07:00
Nikolaj Bjorner
de028f33a2
Update inc_sat_solver.cpp 2026-06-11 15:40:11 -07:00
Nikolaj Bjorner
5aa06b6333 refactor phase update 2026-06-11 15:28:48 -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