mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
19040 commits 23 branches 48 tags 157 MiB
Commit graph

19040 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
954dddbfb3 retain pip install build, remove audit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-28 09:44:28 -07:00
Nikolaj Bjorner
5360656440 fix expected 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-28 09:40:57 -07:00
dependabot[bot]
0bf3eeb807
Bump docker/build-push-action from 6.6.1 to 6.7.0 (#7350) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.6.1 to 6.7.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.6.1...v6.7.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-08-28 09:32:00 -07:00
Nikolaj Bjorner
f6dbaee6ce adding to nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 17:17:53 -07:00
Audrey Dutcher
e1f1d677ff
New python packaging and tests (#7356) 
* Simplify/modernize python packaging

* Modify azure CI to utilize new python packaging
 2024-08-27 17:12:31 -07:00
Nikolaj Bjorner
677b5b4196 fixes to handling signed operators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 14:00:26 -07:00
Nikolaj Bjorner
b1f7965697 fix mul inverse 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 13:40:09 -07:00
Nikolaj Bjorner
ed0ffc1b49 fixes to mul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 11:58:18 -07:00
Nikolaj Bjorner
4146e938e8 na 2024-08-27 11:45:27 -07:00
Nikolaj Bjorner
3bcd98b653 include bounds checks in set random 2024-08-27 10:59:27 -07:00
Nikolaj Bjorner
7699ce56db fixing repair 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 10:39:15 -07:00
Nikolaj Bjorner
6b0a10637c reserve for multiplication 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 10:06:10 -07:00
Nikolaj Bjorner
a0ae5c8d5e fixup repairs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 04:30:18 -07:00
Nikolaj Bjorner
6488e33915 fixes to fixed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 18:42:32 -07:00
Nikolaj Bjorner
9fcddc5774 fixes to bv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 17:51:14 -07:00
Nikolaj Bjorner
349ebd0a5b #7344 2024-08-26 14:22:28 -07:00
Nikolaj Bjorner
84da614de3 make gcc linting happy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 11:40:01 -07:00
Nikolaj Bjorner
b84b4e7f9a fix attribute order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 11:38:27 -07:00
Nikolaj Bjorner
49ba3bc12f address compiler warnings gcc-13 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 11:33:54 -07:00
Nikolaj Bjorner
eb555ee0a7 use std::pow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 10:32:42 -07:00
Nikolaj Bjorner
e3b92fec82 use exponential decay with breaks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 10:21:46 -07:00
Kirill A. Korinsky
cff1e9233f
Avoid broken stack at few places (#7353) 
* Avoid broken stack by degree_lit_num_lt

* Avoid broken stack by fix_dl_var_tactic

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 10:02:54 -07:00
Nikolaj Bjorner
6a68cc55bb #7353 - clear pointer when existing stack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 09:59:56 -07:00
Nikolaj Bjorner
62a8512401 use reward as proxy for score 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 09:49:53 -07:00
Nikolaj Bjorner
2549a2cf07 use reward as proxy for score 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 09:30:38 -07:00
Nikolaj Bjorner
cd92b38697 avoid negative reward 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 09:21:38 -07:00
Nikolaj Bjorner
ace3472a96 add smt params to path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-25 18:49:57 -07:00
Nikolaj Bjorner
8a49002f60 reorg monomials 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-25 18:33:01 -07:00
Nikolaj Bjorner
fa6091dc16 remove coefficient from multiplication definition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-25 15:23:59 -07:00
Nikolaj Bjorner
2bcb56fb13 disable non-tabu version of find_nl_moves 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-25 13:00:08 -07:00
Nikolaj Bjorner
df980acd67 use unit coefficients for muls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-25 12:59:22 -07:00
Nikolaj Bjorner
0df6fe65f7 enable multiplier expansion, enable linear move 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 18:31:59 -07:00
Nikolaj Bjorner
803fd2a10f remove linear opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 18:31:02 -07:00
Nikolaj Bjorner
7f02ee4263 separate linear update remove 20% threshold 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 18:14:31 -07:00
Nikolaj Bjorner
ab66239c11 separate linear update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 18:13:16 -07:00
Nikolaj Bjorner
ebbcfafd81 include 5% reset probability 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 17:58:49 -07:00
Nikolaj Bjorner
32c3a5af67 include linear moves 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 17:56:34 -07:00
Nikolaj Bjorner
d6b89ba2d5 make reset updates recursive 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 14:16:34 -07:00
Nikolaj Bjorner
47b793a5e0 disable nested mul, use non-lookahead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:55:43 -07:00
Nikolaj Bjorner
059ccd67bb disable nested mul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:27:09 -07:00
Nikolaj Bjorner
c643672e9f perform lookahead update + nested mul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:25:48 -07:00
Nikolaj Bjorner
29aca5b1d6 flatten products 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:00:50 -07:00
Nikolaj Bjorner
87d556d37d delay factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 10:57:35 -07:00
Nikolaj Bjorner
67d3f3b110 localize impact of factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 10:14:59 -07:00
Nikolaj Bjorner
3c92119b1a disable tabu in fallback modes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 09:55:43 -07:00
Nikolaj Bjorner
11ed99089b remove restart 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 09:32:04 -07:00
Nikolaj Bjorner
b2bc51e9ac fix bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 16:44:44 -07:00
Nikolaj Bjorner
0b8177c7d6 generalize factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 16:23:37 -07:00
Nikolaj Bjorner
69dd247cfc re-add tabu override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 09:25:34 -07:00
Nikolaj Bjorner
a2b8b724b2 fixes to semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 09:20:11 -07:00