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

18245 commits

This branch
This branch
All branches
Author SHA1 Message Date
Bruce Mitchener 9d1ceab1f2
cmake: Use FindPython3. (#7019) 
`FindPythonInterp` has been deprecated for a long time and is more
verbal about that deprecation now.

The build system no longer uses `PYTHON_EXECUTABLE` but instead uses
`Python3_EXECUTABLE`.
 2023-11-27 11:20:21 +01:00
Bruce Mitchener b5e8f59eae
mbp: term: Fix reorder ctor warning. (#7016) 
Initialize members in same order they are defined.
 2023-11-26 16:34:08 +01:00
Bruce Mitchener 9d3fef3e2b
cmake: Require cmake 3.16 or later. (#7015) 
Support for requiring cmake < 3.4 may go away soon (according to
a deprecation notice when building).

Ubuntu 20.04 provides cmake 3.16 and current is 3.27, so that seems
like a reasonable version to require.
 2023-11-26 16:30:22 +01:00
Bruce Mitchener 2354998cd2
z3.h: Don't include stdio.h (#7014) 
This doesn't seem to actually be used or needed here.
 2023-11-24 16:46:32 +01:00
dependabot[bot] a10c93e203
Bump docker/build-push-action from 5.0.0 to 5.1.0 (#7008) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 5.0.0 to 5.1.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v5.0.0...v5.1.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>
 2023-11-23 17:54:45 +01:00
Christoph M. Wintersteiger 16753e43f1
Add accessors for RCF numeral internals (#7013) 2023-11-23 17:54:23 +01:00
Nikolaj Bjorner 9382b96a32 add API to access symbols associated with quantifiers 2023-11-19 16:30:09 -08:00
Nikolaj Bjorner d272acc3ac fix crash when api_solver sets reset_tracked_assertions 2023-11-19 12:48:33 -08:00
Nikolaj Bjorner ac105b7d8c remove unused code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-19 11:47:00 -08:00
Nikolaj Bjorner 4350bd77ac check cancel flag to avoid unsound conflicts 2023-11-19 11:43:52 -08:00
Nikolaj Bjorner 32f8705ac3 #7001 - align is_numeral without to behavior if is_numeral with return numeral. 2023-11-19 10:43:14 -08:00
Nikolaj Bjorner 35bc522dae #7003 
minor tweaks to gomory and reset n3 within loop (but the entire function is dead code).
 2023-11-19 09:59:44 -08:00
Nikolaj Bjorner 924c296704 add logging 2023-11-18 12:30:40 -08:00
Nikolaj Bjorner 5bec982cc5 chores in theory_lra 2023-11-18 10:05:26 -08:00
Nikolaj Bjorner e40b8a2d13 household chores in legacy arithmetic solver 2023-11-18 09:56:06 -08:00
Nikolaj Bjorner 5ab1afe5c2 expose enode pp convenciences 2023-11-18 09:53:20 -08:00
Nikolaj Bjorner 1710fe4927 use iterator shortcut 2023-11-18 09:52:58 -08:00
Nikolaj Bjorner a9f9d3ddf4 build fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-17 10:15:01 -08:00
Nikolaj Bjorner b9455c3692 #6999 deal with implicit assumptions, more robust pattern matching 
The code is making some assumptions that arrays are 1-dimensional. This is not generally true.
Introducing pattern matching to ensure the assumption is met.
Avoid get_arg(..) especially when there is an approach based on pattern matching recognizers.
 2023-11-17 10:06:20 -08:00
Nikolaj Bjorner 6d6d6b8ed0 build issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-17 09:20:17 -08:00
Hari Govind V K f94a475da3
Qel fixes (#6999) 
* dont use qel for sequences. fix #6950

* handle negation of read-write. fix #6991

* handle neg-peq terms produced by distinct. fix #6889

* dbg print
 2023-11-17 09:18:04 -08:00
Nikolaj Bjorner 1b6c7d6541 fix #6996 2023-11-16 18:58:24 -08:00
Christoph M. Wintersteiger 36382ccb57
Fix memory and concurrency issues in OCaml API (#6992) 
* Fix memory and concurrency issues in OCaml API

* Undo locking changes
 2023-11-16 18:28:12 -08:00
Nikolaj Bjorner 5b9fdcf462 fix #6997 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-15 18:08:48 -08:00
Nikolaj Bjorner f1a39b8884 add comment regarding usage model for flush_objects() to relate with pr #6992 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-15 11:54:59 -08:00
Christoph M. Wintersteiger 3baaba5edd
Revert unsound NaN constraints in theory_fpa (#6993) 2023-11-14 14:28:30 -08:00
Nikolaj Bjorner c0ee4e9613 pip install importlib resources 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-14 10:02:24 -08:00
Nikolaj Bjorner 1ce95d3859 pip install importlib resources 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-14 10:01:13 -08:00
Nikolaj Bjorner 37b283fab9 use python3 in nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-14 08:54:10 -08:00
Nikolaj Bjorner 7ed27a1f41 prepare release script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-14 08:48:19 -08:00
Nikolaj Bjorner ad2107f079 fix #6978 2023-11-14 08:45:22 -08:00
Nikolaj Bjorner 4406011881 fix #6984 2023-11-14 07:40:32 -08:00
Nikolaj Bjorner 3c2e97ddb6 fix #6988 2023-11-14 07:30:32 -08:00
Nikolaj Bjorner c2610cb37c #6523 
malformed models on giveup status
 2023-11-13 14:32:53 -08:00
Nikolaj Bjorner 8a4e857294 #6523 
regressions from changes inside math/lp/int_solver
 2023-11-13 14:28:03 -08:00
Nikolaj Bjorner 3de5af3cb0 fix bug in bound simplification in Gomory for mixed integer linear cuts, enable fixed variable redution after bugfix, add notes that rewriting bounds does not work 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-10 16:39:04 +01:00
EyalBrilling aa9c7912dc
fixed possible undefined variable assigment (#6985) 2023-11-10 11:36:24 +01:00
Nikolaj Bjorner 0556059bdf change to expr_ref to allow trying simplification 2023-11-08 13:50:48 +01:00
Nikolaj Bjorner bd4d580b17 fix #6986 2023-11-08 13:49:30 +01:00
Nikolaj Bjorner e6385f8c85 disable bound validation in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-07 20:49:26 +01:00
Nikolaj Bjorner 3d99ed9dd4 Gomory cut / branch and bound improvements 
Improve fairness of cut generation by switching to find_infeasible_int_var with cascading priorities, allow stronger cuts by inlining terms.
 2023-11-07 19:59:02 +01:00
Nikolaj Bjorner 9f0b3cdc25 Add utility to expand sub-terms 2023-11-07 19:58:32 +01:00
Nikolaj Bjorner fb95760137 remove template 2023-11-07 19:57:50 +01:00
Nikolaj Bjorner 77dab53e9e track number of Gomory cuts 2023-11-07 19:57:49 +01:00
Nikolaj Bjorner 2d1f4d5d93 remove verbose logging 2023-11-07 19:57:49 +01:00
Nikolaj Bjorner e86eae27e6 #6523 and other heap-use-after-free error 2023-11-07 19:57:49 +01:00
Nikolaj Bjorner eed02b6d86 improved logging, use C++11 for loops instead of iterators 2023-11-07 19:57:49 +01:00
Lev Nachmanson 14312ef8a3 remove some warnings with clang 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-11-02 15:34:41 -07:00
Lev Nachmanson 08d3a82ce0 simplify the jump on entering 2023-11-02 11:09:01 -07:00
Lev Nachmanson bdf1fcf5c1 remove an assert 2023-11-02 09:59:03 -07:00