mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity
16849 commits 23 branches 48 tags 156 MiB
Commit graph

16849 commits

This branch
This branch
All branches
Author SHA1 Message Date
Bruce Mitchener 7eb1e6dd23 userPropagator: Compile as C++20. 
Using std::unordered_map::contains requires C++20.
 2022-08-05 07:41:14 +03:00
Bruce Mitchener 1d9345c3de Fix typos. 2022-08-05 07:40:50 +03:00
Bruce Mitchener 08165f5367 No need to return a const bool. 2022-08-05 07:40:19 +03:00
Nikolaj Bjorner 9da6895276 add option to select with folding 2022-08-04 16:59:26 +03:00
Nikolaj Bjorner a8ff976bcc max maximal unfolding configurable 2022-08-04 16:59:26 +03:00
Bruce Mitchener a3161bdc15 update_api.py: Remove usage of MKException. 
This wasn't working as it was being accessed from a function object
rather than the module.

Instead, let's just print the error and exit.
 2022-08-04 07:54:42 +03:00
Bruce Mitchener 8a3556e5ba cmake: Remove dep on mk_util.py for update_api.py calls. 
update_api.py doesn't depend on mk_util.py any longer, so these
dependencies can go away.
 2022-08-04 07:54:26 +03:00
Bruce Mitchener ad4c786ea4 mk_unix_dist.py: Fix --nopython 
Writing to the global PYTHON_ENABLED requires that it be flagged
as a global.
 2022-08-04 07:54:10 +03:00
Bruce Mitchener dc75031a36 Remove all per-OS defines apart from _WINDOWS. 
These are all unused and shouldn't be needed. Mostly we need
something for differentiating between POSIX and non-POSIX
(until we can reduce some of those differences as well).

We shouldn't need to modify the build system to build on a new
OS if it is basically a Unix and is supported by cmake.
 2022-08-03 19:03:04 +03:00
Bruce Mitchener 85b96dc877 cmake: Remove telling the Intel compiler to link OpenMP. 
This also removes a duplicated branch since the Intel compiler
is already handled at the same time as GCC and Clang, so it
doesn't need its own block as well.
 2022-08-03 19:02:12 +03:00
Saloed d908ebec4c fix memory_high_watermark parameter according to documentation 2022-08-03 18:50:54 +03:00
Bruce Mitchener d8c99480c6 test/lp: Replace if linux with if not windows. 
This is stuff that works on posix, so we can flip the check.
 2022-08-03 08:22:54 +03:00
Bruce Mitchener 55b70b4c7e Remove contrib/cmake. 
This mainly contained a bootstrap script that did nothing except
say that it would be deleted soon. It has been 5 years, so it
should be safe to go away now.
 2022-08-03 08:22:13 +03:00
Bruce Mitchener 112dba559f Remove unused private member from smaller_pattern. 2022-08-03 08:21:32 +03:00
Bruce Mitchener 3ab96281eb Remove Travis CI configs. 2022-08-03 08:20:57 +03:00
Nikolaj Bjorner 774ce3d7ab create special case for osx arm 
shortcut when store/select are distinct

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-03 07:56:02 +03:00
Bruce Mitchener 42f5047463 cmake: Cleanup remnants of workaround for USES_TERMINAL. 
In older versions, this was dependent upon the version of cmake,
but when it was updated for newer cmake, these remnants were
left.
 2022-08-02 17:39:10 +03:00
Bruce Mitchener 8313282cda Use char version of find_last_of when possible. 2022-08-02 17:38:11 +03:00
Bruce Mitchener b3612264a9 Use cmake properties for symbol visibility and PIC. 2022-08-02 09:32:03 +03:00
Bruce Mitchener 886c3abec1 Remove remnants of _MP_MSBIGNUM checks. 2022-08-02 09:28:57 +03:00
dependabot[bot] 053c3ec9e8 Bump docker/build-push-action from 3.0.0 to 3.1.0 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 3.0.0 to 3.1.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v3.0.0...v3.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>
 2022-08-02 09:27:27 +03:00
Bruce Mitchener fb1d0bc899 cmake: Remove ExternalProject BUILD_ALWAYS workaround. 
This was only needed for cmake < 3.1, but we require later
than that.
 2022-08-02 09:27:11 +03:00
Bruce Mitchener 9a99c78ffb Enable thread_local code more broadly. 
This was only being enabled on Windows, Linux, and FreeBSD. (FreeBSD
only had it enabled in the legacy build system, not in cmake.)

`thread_local` is part of C++11, so now that we require C++17
or later and more recent compilers, this should work everywhere
that threading does, so only disable it within a `SINGLE_THREAD`
build.
 2022-08-02 09:24:51 +03:00
Bruce Mitchener 82d853e5f8 Use = delete to delete special methods. 
This provides a better experience than just marking them as
private and leaving them as undefined symbols.
 2022-08-02 09:23:14 +03:00
Bruce Mitchener 059b795faa Fix warning about \ref when building website.dox 2022-08-01 18:51:20 +03:00
Jakob Rath 2c2ab0d57a Additional BV matchers 2022-08-01 18:37:11 +03:00
Jakob Rath 5d858da58a union_find::reserve 2022-08-01 18:37:11 +03:00
Jakob Rath e8e64d3098 dlist::insert_before/after 2022-08-01 18:37:11 +03:00
Jakob Rath de6a0ab1a7 PDD operations 2022-08-01 18:37:11 +03:00
Jakob Rath 42233ab5c8 Additional BDD operations; BDD vectors and finite domain abstraction 2022-08-01 18:37:11 +03:00
Jakob Rath 9275d1e57a sparse_matrix iterators 2022-08-01 18:37:11 +03:00
Jakob Rath 6eae27ffad numeral helper functions 2022-08-01 18:37:11 +03:00
Jakob Rath e31926d132 var_queue display 2022-08-01 18:37:11 +03:00
Jakob Rath 6a929f91c8 scoped_ptr_vector usability 2022-08-01 18:37:11 +03:00
Jakob Rath d2fe174320 Add SASSERT_EQ and VERIFY_EQ 2022-08-01 18:37:11 +03:00
Jakob Rath 79ee543d25 Move tbv to util 2022-08-01 18:37:11 +03:00
Bruce Mitchener a89be68050 Use false instead of 0. 2022-08-01 18:28:07 +03:00
Bruce Mitchener fe1e301735 Remove Z3_bool, Z3_TRUE, Z3_FALSE from the API. 
These have just been aliases for the standard type `bool` and
values `true` and `false` for a long time now.
 2022-08-01 14:25:00 +03:00
Bruce Mitchener 77e5d6ab19 Use nullptr consistently instead of 0 or NULL. 2022-08-01 14:24:32 +03:00
Nikolaj Bjorner bf282b05c8 fix #6213 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-31 18:40:59 +03:00
Nikolaj Bjorner 4a1baa7d2d fix #6165 2022-07-30 17:10:01 +02:00
Bruce Mitchener 5d0dea05aa
Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
Nikolaj Bjorner f7fbb78fc8 Merge branch 'master' of https://github.com/z3prover/z3 2022-07-30 06:32:41 +02:00
Nikolaj Bjorner a6fe260354 update minor versin number to ABI change to remove Z3_bool from z3_api.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-30 06:31:22 +02:00
Bruce Mitchener fc40e3c510 Remove usages of Z3_bool, just use bool. 2022-07-30 05:49:05 +02:00
Bruce Mitchener c682ec1135 Remove remaining references to Z3_bool_opt. 2022-07-30 05:48:27 +02:00
Nikolaj Bjorner 591d485358 update versions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-30 05:26:43 +02:00
Nikolaj Bjorner a2d44194a4 Update release.yml for Azure Pipelines 
set credential to key at nuget.org
 2022-07-30 05:20:33 +02:00
Nikolaj Bjorner 69b1337ca6 inc release number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-29 23:31:26 +02:00
Nikolaj Bjorner 2a8e73f34f Merge branch 'master' of https://github.com/z3prover/z3 2022-07-29 23:30:37 +02:00