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

19304 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
c30600c2ef fixes in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:41 -10:00
Lev Nachmanson
5f70eb0524 do not eliminate fresh variables when tightening 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:41 -10:00
Lev Nachmanson
1769c6059e fixed dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:41 -10:00
Lev Nachmanson
2ca7b31d13 comment out global_max_change 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
f05d1abccc debug dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
8d8ee99db3 test tightening with S 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
7d8212646d handle sat with tightening 2025-02-03 13:30:40 -10:00
Lev Nachmanson
9118abebc7 cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
e0185121c5 use u_dependency in eprime_pair 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
b20566a488 work on tighten_with_S 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
a1a9825e43 remove a throw 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
a75eff6525 bug fix 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
0c6dcfedb8 small optimization 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
9ec55de5c6 optimize dio changes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
7c9cb44c94 less eager dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:40 -10:00
Lev Nachmanson
4fea4259ec fix the build 2025-02-03 13:30:40 -10:00
Lev Nachmanson
1a99fa56cb handle zero rows correctly 2025-02-03 13:30:40 -10:00
Lev Nachmanson
178411ad0c dio passes regression\smt2 tests with limited functionality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:39 -10:00
Lev Nachmanson
dcd80ac95b fix term_o init 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:39 -10:00
Lev Nachmanson
c29d04dc3c debug dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:39 -10:00
Lev Nachmanson
1cb71b4648 debug dio 2025-02-03 13:30:39 -10:00
Lev Nachmanson
db899fd670 fix in substitution of fresh variables, clean column.h 2025-02-03 13:30:39 -10:00
Lev Nachmanson
5f71604198 bug fix in init and getting explanations 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:39 -10:00
Lev Nachmanson
0814fa40b0 create a conflict explanation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:39 -10:00
Lev Nachmanson
53605d4e0a a version with less pointers: got a conflict 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:30:00 -10:00
Lev Nachmanson
876cbc527d in the middle 2025-02-03 13:24:33 -10:00
Lev Nachmanson
778db5e763 use std::list 2025-02-03 13:24:33 -10:00
Lev Nachmanson
c1e577e932 fix the crash 2025-02-03 13:24:33 -10:00
Lev Nachmanson
484af98af6 crash 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:24:33 -10:00
Lev Nachmanson
0eeef3b806 fix the build 2025-02-03 13:24:33 -10:00
Lev Nachmanson
0b9b1c4472 move some functionality from int_solver to int_solver::imp 2025-02-03 13:24:33 -10:00
Lev Nachmanson
66b778cb25 fix the build 2025-02-03 13:24:33 -10:00
Lev Nachmanson
7050589adf prepare for calling diophantine equations 2025-02-03 13:24:33 -10:00
Lev Nachmanson
049520483f add parameter to control calling diophantine equations 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-03 13:24:33 -10:00
Nikolaj Bjorner
17d47ca8c7 fix #7493 2025-02-02 15:00:31 -08:00
Nikolaj Bjorner
99cbfa715c Add a sharp throttle to lia2card tactic to control overhead in default tactic mode 
lia2card was added to qfuflia tactic based on a user scenario, but it overshot: lia2card is by default harmful. It is here tamed to only convert binary variables and throttle on nested ite terms
 2025-02-02 13:58:51 -08:00
Nikolaj Bjorner
fd2a8a554d disable small clause generation for propagation 2025-02-01 20:04:29 -08:00
Nikolaj Bjorner
0ef26983fc release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-31 17:31:37 -08:00
Nikolaj Bjorner
aea4490fb2 throttle overhead with lia2card 2025-01-31 12:36:59 -08:00
Nikolaj Bjorner
d465bdbb87 include extensionality constraints for arrays 2025-01-31 11:06:40 -08:00
Nikolaj Bjorner
d6dcc515eb rehearse release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-31 09:49:42 -08:00
Nikolaj Bjorner
edc5679530 updated release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-31 09:49:16 -08:00
Nikolaj Bjorner
8ae24e2b38 update release version 2025-01-31 09:29:28 -08:00
dependabot[bot]
1d622a678e
Bump docker/build-push-action from 6.12.0 to 6.13.0 (#7535) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.12.0 to 6.13.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.12.0...v6.13.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>
 2025-01-31 09:26:49 -08:00
Clemens Eisenhofer
9557e7cacf
Minor (#7540) 2025-01-31 08:22:30 -08:00
Nikolaj Bjorner
1ce6e66ac9 generalize logic detection to use sub-string matching 2025-01-30 16:34:54 -08:00
Nikolaj Bjorner
eb825855fa increase the log level on callbacks with bit-indices that get set 2025-01-30 16:34:36 -08:00
Nikolaj Bjorner
c9ac4d6f75 pre-flatten use list before iterating over m_unsat 
select_max_same_sign accesses the use-list which may cause it to be flattened.
 2025-01-30 16:34:17 -08:00
Nikolaj Bjorner
e3566288a4 fixes based on benchmarking UFDTLIA/NIA/BV 2025-01-29 17:00:26 -08:00
Nikolaj Bjorner
f1e0950069 fix several crashes exposed by QF_UFDTNIA benchmark sets 2025-01-29 16:23:38 -08:00