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

19030 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
17131983fe use loop instead of goto 2024-04-02 16:31:51 +02:00
Jakob Rath
88be5e6611 check hole_len 2024-04-02 16:28:45 +02:00
Jakob Rath
47f28c6857 find_overlap should stay on lower bit-width to find conflicts 2024-04-02 16:27:29 +02:00
Jakob Rath
f127d12e4c remove redundant intervals (disabled for now) 2024-04-02 15:10:12 +02:00
Nikolaj Bjorner
b07cb3dc54 use C++23 conventions in buffer.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-30 16:26:19 -07:00
Jakob Rath
287d772ff6 WIP: add missing conditions on size of "holes" 
when combining intervals of different bit widths
 2024-03-28 16:48:35 +01:00
Jakob Rath
0d3e88fd31 display_explain 2024-03-28 16:38:41 +01:00
Jakob Rath
a7c84da44d Fix monomials::parity 2024-03-27 10:49:02 +01:00
Jakob Rath
e22c86acb6 fixed_slice display 2024-03-25 14:34:06 +01:00
Jakob Rath
8a23523f20 fix crash on EBxzQox7raUO.smt2 2024-03-25 13:20:24 +01:00
Nikolaj Bjorner
ac6554eb92 set C++ version to 20 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-21 10:59:31 -07:00
Nikolaj Bjorner
182979771f disable verbose 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-21 10:41:31 -07:00
Jakob Rath
934b2ad5ef update target selection to what was intended 2024-03-21 13:53:26 +01:00
Jakob Rath
342db52558 fix 2024-03-21 12:03:52 +01:00
Jakob Rath
acd05686e4 relevant level should be based on what's to appear in the lemma 2024-03-21 11:05:55 +01:00
Jakob Rath
7d1a57b6e9 remove commented code 2024-03-20 15:38:42 +01:00
Jakob Rath
7922ee3e82 debug output 2024-03-20 15:37:34 +01:00
Jakob Rath
fd9c931168 skip entry for origin variable 2024-03-20 15:37:03 +01:00
Jakob Rath
23ca9d9fc5 select targets, try generic/specific version of projection 2024-03-20 15:26:33 +01:00
Jakob Rath
de809932eb refactor, minor fixes 2024-03-20 14:33:30 +01:00
Jakob Rath
ef6b5f82d1 relax level constraint 2024-03-20 13:39:16 +01:00
Jakob Rath
91a9feb5a8 warnings 2024-03-20 12:16:24 +01:00
Jakob Rath
f47fbdd714 Move interval projection out of viable 2024-03-20 12:11:14 +01:00
Jakob Rath
5339a2f70f Don't access solver_interface directly 2024-03-20 10:16:40 +01:00
Jakob Rath
a34bb99db3 Use variable from violated interval as origin 2024-03-20 10:15:25 +01:00
Jakob Rath
3a11350142 Move helper functions 2024-03-20 10:10:27 +01:00
Nikolaj Bjorner
6eeb022048 fix encoding for sdiv exposed by zQkAOXjEDwgm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-19 16:00:09 -07:00
Nikolaj Bjorner
ffe7b46e74 unsigned cast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-19 15:02:42 -07:00
Jakob Rath
f5eb457bee fix propagate_from_containing_slice dependency 2024-03-19 16:13:28 +01:00
Jakob Rath
489a1495d2 dep 2024-03-19 14:23:44 +01:00
Jakob Rath
adc5313916 remove debug output 2024-03-19 10:11:06 +01:00
Jakob Rath
148eafaaf0 Merge remote-tracking branch 'origin/master' into poly 2024-03-19 09:50:24 +01:00
dependabot[bot]
1a7437144c
Bump docker/build-push-action from 5.2.0 to 5.3.0 (#7170) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 5.2.0 to 5.3.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v5.2.0...v5.3.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-03-18 15:25:58 -07:00
cctv130
18365907a2
Update util.h (#7169) 2024-03-17 20:29:27 -07:00
Nikolaj Bjorner
b8a69987c3 fix #7165 2024-03-17 16:33:40 -07:00
Nikolaj Bjorner
fb824bee54 inline unfolding if it is linear or constant. 2024-03-16 13:02:26 -07:00
Nikolaj Bjorner
3555b25317 Merge branch 'poly' of https://github.com/z3prover/z3 into poly 2024-03-15 08:55:16 -07:00
Nikolaj Bjorner
e4cc6e29ca fix case when interval is full 2024-03-15 08:55:07 -07:00
Jakob Rath
aa1285288e Fix integration of propagate_from_containing_slice 2024-03-15 15:08:12 +01:00
Jakob Rath
dfb200a3c9 propagation from containing slice depends on concrete values 2024-03-15 12:31:31 +01:00
dependabot[bot]
6450a7a0b8
Bump docker/build-push-action from 5.1.0 to 5.2.0 (#7159) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 5.1.0 to 5.2.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v5.1.0...v5.2.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-03-14 16:54:01 -07:00
Jakob Rath
5704e8d154
fix intblast is_bounded (#7163) 2024-03-14 08:48:38 -07:00
Jakob Rath
2102db2df8 Fix viable entry reduction (case new_lo == new_hi) 2024-03-14 15:09:21 +01:00
Jakob Rath
f6c99585f3 fix warning 2024-03-14 15:08:00 +01:00
Nikolaj Bjorner
82dc254d0e Merge branch 'poly' of https://github.com/z3prover/z3 into poly 2024-03-13 16:20:54 -07:00
Nikolaj Bjorner
c2f8dd9a02 use -> types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-13 16:20:51 -07:00
Nikolaj Bjorner
1f0a6c051a update slice/offset claim structures to allow for equal variable. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-13 11:49:11 -07:00
Nikolaj Bjorner
1e9381c2f6 update slice/offset claim structures to allow for equal variable. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-13 11:48:09 -07:00
Jakob Rath
5d1602b6c7 print validation failures 2024-03-13 14:12:10 +01:00
Jakob Rath
7da7e99ca2 try_umul_blast 2024-03-13 14:01:07 +01:00