mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 09:04:07 +00:00
Code Activity
19510 commits 22 branches 48 tags 156 MiB
Commit graph

19510 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson 2ebb957cc8 enable cuts from proofs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 44fd0e48a8 fixes in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson a8e667c643 do not eliminate fresh variables when tightening 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 52b0b8d5d5 fixed dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 5ac428fcc9 comment out global_max_change 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 89e4f59df2 debug dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 798f0e2e8a test tightening with S 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 193116bf84 handle sat with tightening 2025-02-11 12:23:00 -10:00
Lev Nachmanson b1be8c0957 cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 5db46c1d81 use u_dependency in eprime_pair 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 1408fe60ab work on tighten_with_S 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson f0b5cd1066 remove a throw 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson be8f3e9c3e bug fix 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 0b1e923d2a small optimization 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 66c6bad01c optimize dio changes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 18c75e6333 less eager dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson bbeecc6f7c fix the build 2025-02-11 12:23:00 -10:00
Lev Nachmanson 3d5ee82bd1 handle zero rows correctly 2025-02-11 12:23:00 -10:00
Lev Nachmanson 78a58b06aa dio passes regression\smt2 tests with limited functionality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 245d448c66 fix term_o init 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson a796d48264 debug dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson df18885f97 debug dio 2025-02-11 12:23:00 -10:00
Lev Nachmanson cd13890650 fix in substitution of fresh variables, clean column.h 2025-02-11 12:23:00 -10:00
Lev Nachmanson f5e646cbcb bug fix in init and getting explanations 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 59e2dab69a create a conflict explanation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 52653e6e43 a version with less pointers: got a conflict 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson 5a36e02c58 in the middle 2025-02-11 12:23:00 -10:00
Lev Nachmanson 122e0135d2 use std::list 2025-02-11 12:23:00 -10:00
Lev Nachmanson 3b22d3b19d fix the crash 2025-02-11 12:23:00 -10:00
Lev Nachmanson abf29b57aa crash 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson a5dd59fdfb fix the build 2025-02-11 12:23:00 -10:00
Lev Nachmanson a1a01b9da6 move some functionality from int_solver to int_solver::imp 2025-02-11 12:23:00 -10:00
Lev Nachmanson 889292472e fix the build 2025-02-11 12:23:00 -10:00
Lev Nachmanson 3d6cc64e2e prepare for calling diophantine equations 2025-02-11 12:23:00 -10:00
Lev Nachmanson 097a25ebfe add parameter to control calling diophantine equations 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Clemens Eisenhofer acd48b6a30
Fixing #7465 (#7551) 
* Fixed bug in UP

* Put decrement at the right position

* Fixed replaying in UP

* Set UP persist clauses to false
 2025-02-11 09:20:25 -08:00
Nikolaj Bjorner c2b7b58c78 #7468 - add option (get-info :parameters) to display solver parameters that were updated globally and distinct from defaults 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-10 11:57:14 -08:00
Nikolaj Bjorner 62126fd6e2 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-10 11:51:21 -08:00
Can Cebeci af270da785
Fix complete_partial_func for finite domains (#7547) 2025-02-05 16:14:55 -08:00
Clemens Eisenhofer 091984419e
Fixed bug in UP (#7545) 
* Fixed bug in UP

* Put decrement at the right position
 2025-02-04 08:41:28 -08: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