mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 07:36:38 +00:00
Code Activity
19056 commits 23 branches 48 tags 157 MiB
Commit graph

19056 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 5fdf300557 adding dt plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-14 17:55:52 -07:00
Nikolaj Bjorner ef20237edd fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-14 11:31:34 -07:00
Nikolaj Bjorner 54cce7b10b restore use of value_hash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-14 10:46:31 -07:00
Nikolaj Bjorner f136d46fb4 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-13 19:23:05 -07:00
Nikolaj Bjorner 04824786be fix test for new signature of flip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-13 15:26:08 -07:00
Nikolaj Bjorner c1b9a3cc9e allow for alternating 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-13 13:32:56 -07:00
Nikolaj Bjorner 9b54254fa2 throttle save model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-12 19:09:25 -07:00
Nikolaj Bjorner 2bd335db81 alternate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-12 16:11:05 -07:00
Nikolaj Bjorner 609c46395f recover shift-weight loop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-12 15:29:48 -07:00
Nikolaj Bjorner 1765141261 fx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-12 12:19:55 -07:00
Nikolaj Bjorner 766b9df4e2 fixup handling of disequality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-12 10:25:19 -07:00
Nikolaj Bjorner d7b82366c6 avoid units 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 19:33:39 -07:00
Nikolaj Bjorner 2af713e4db fixing incremental 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 16:50:31 -07:00
Nikolaj Bjorner 46252b669c fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 16:17:54 -07:00
Nikolaj Bjorner 9eb6f97e6b fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 15:18:36 -07:00
Nikolaj Bjorner d2ce7b0ea2 break build again 2024-10-11 14:53:12 -07:00
Nikolaj Bjorner d278a1651d fix build 2024-10-11 14:28:36 -07:00
Nikolaj Bjorner 9b6c161ad2 break sls build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 14:02:42 -07:00
Nikolaj Bjorner 2ecb1c8b94 fix sls build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 14:02:06 -07:00
Nikolaj Bjorner 73f09fe94a updated package 2024-10-11 11:06:03 -07:00
Nikolaj Bjorner 5d9d134151 Merge branch 'master' into sls 2024-10-11 09:56:46 -07:00
Nikolaj Bjorner f8fa2de35b add incremental mode 2024-10-11 09:54:46 -07:00
Nikolaj Bjorner da614c65e5 remove m_level attribute, use s->get_scope_level directly 2024-10-08 19:56:57 -07:00
Nikolaj Bjorner 6bd46b0922 fix #7363. Replay relevancy on unit literals that are re-asserted during backtracking. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-08 19:40:37 -07:00
Nikolaj Bjorner cfd00ad672 add slice solver option to command context 2024-10-08 09:24:52 -07:00
Nikolaj Bjorner 8a95dd4d65 A slice solver option for interactive use case 
A slice solver prunes the set of active assertions based on symbol occurrences in a goal that is tracked as a @query.
Ground assertions that have symbols intersecting with the query are included in the solver state, and quantifiers that with patterns that intersect with the slice are included. The slice is the fixedpoint of including symbols from all included assertions.
Enable the functionality for command-line use by setting solver.slice=true
 2024-10-08 09:24:52 -07:00
Nikolaj Bjorner 0fec7efc7b micro-tuning 2024-10-08 09:24:52 -07:00
Nikolaj Bjorner c6cd25c822 mico-tuning 2024-10-08 09:24:52 -07:00
Peli de Halleux 24d7b05c0d
refactor and optimize git operations for commit messages and failure analysis (#7412) 2024-10-04 16:55:00 -07:00
Nikolaj Bjorner 2ae4ac8d0a fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-04 08:38:52 -07:00
Nikolaj Bjorner b60e1a2ed2 fixup variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-03 20:06:45 -07:00
Nikolaj Bjorner 969511ac00 fixup std-order / inv-order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-03 19:35:16 -07:00
Nikolaj Bjorner 66bb310966 reset before manager is deallocated 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-03 18:19:14 -07:00
Nikolaj Bjorner a98c925069 optimize var_subst 2024-10-03 18:14:47 -07:00
Nikolaj Bjorner f5db6bf92b install Julia for macos build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-03 12:48:15 -07:00
Nikolaj Bjorner e58eb9f302 fix indentation for mbp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-03 12:47:12 -07:00
Nuno Lopes 3586b613f7 remove default destructors 2024-10-02 22:20:12 +01:00
Nikolaj Bjorner b170f10148 reorder template definition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-02 13:41:02 -07:00
dependabot[bot] 6dec943b29
Bump docker/build-push-action from 6.7.0 to 6.9.0 (#7408) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.7.0 to 6.9.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.7.0...v6.9.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2024-10-02 13:23:39 -07:00
Nikolaj Bjorner d686e92bfa disambiguate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-02 10:45:16 -07:00
Nikolaj Bjorner 93ff89bf98 add == for const_ref and ref to disambiguate equality. 2024-10-02 10:45:16 -07:00
Nikolaj Bjorner c7af97364a fixes for #7402 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-01 15:15:47 -07:00
Nikolaj Bjorner 328616b8b2 fix build warnings 2024-09-30 17:25:19 -07:00
Nikolaj Bjorner 8c39863019 fix typo in arch for setup.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 16:17:40 -07:00
Nikolaj Bjorner 4cefc513eb add sequoia to os versions #7407 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 16:05:53 -07:00
Nikolaj Bjorner 19f63cd6e3 add sequoia to os versions #7407 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 15:57:49 -07:00
Nikolaj Bjorner 86b97186b0 fix build warnings 2024-09-30 15:51:48 -07:00
Nikolaj Bjorner 551cc53a2f fix un-intialized variable warnings 2024-09-30 15:08:33 -07:00
Nikolaj Bjorner 2c94a3a1b3 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 13:09:01 -07:00
Nikolaj Bjorner 7da58b9e84 fix build warnings 2024-09-30 10:34:26 -07:00