3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Commit graph

633 commits

Author SHA1 Message Date
NikolajBjorner 260cb337de try to instrument nightly with aarch compiler for arm64
Signed-off-by: NikolajBjorner <nbjorner@microsoft.com>
2023-08-02 11:25:16 -07:00
NikolajBjorner ea95f8086f try to instrument nightly with aarch compiler for arm64
Signed-off-by: NikolajBjorner <nbjorner@microsoft.com>
2023-08-02 11:24:32 -07:00
Nikolaj Bjorner d33d8ac07a revert setting arm on linux
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-02 10:55:03 -07:00
Nikolaj Bjorner 9b5727adde enable arm for non-osx
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-02 10:51:52 -07:00
Jerry James f5c069f899
Fix regular expression strings with escapes (#6797) 2023-07-07 09:57:07 -07:00
Kevin Phoenix 1a9990a92f
Use sys.getdefaultencoding() instead of sys.stdout.encoding (#6612) 2023-02-28 11:46:10 -08:00
John Fleisher f72cdda5fb
Change to 4 digit assembly version (#6297)
* WiP: test build specific version number

* update mk_win_dist for assembly-version

* Add print statements for version

* remove stray semicolon

* undo quote change in projectstr

* nit fixes

* revert print formatting for Mac build

* fix spaces
2022-08-31 06:46:06 -07:00
John Fleisher b3f4d3fdc7
Publish Z3 symbols (#6280)
* WiP: publish symbols for package

* set debugtype to full

* fix internal nuget feed publishing

* Try pipeline github authorization

* Update github service connection

* WiP: try symbol publish in build

* try Z3Prover for GitHub connection

* WiP: collect symbols

* revert symbol type to pdbonly (only portable is not supported for publishing)

* Publish symbols in nightly and release

* Revert this: comment out publish to test release build pipe

* restore publishing

* Turn of index sources to eliminate warning that it is not supported for Github

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-17 07:30:55 -07: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
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 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
Nikolaj Bjorner b743e210f8 give java dynamic lib a chance for extra flags for #5848 2022-07-15 08:44:05 -07:00
Nikolaj Bjorner b254f4086b Separate out native static content for Java
Make it easier to add native methods for callbacks (for user propagator) #6097

The Java User propagator wrapper should define a base class with virtual methods that can be invoked from functions defined in NativeStatic.txt
2022-06-21 09:09:42 -07:00
Olaf Tomalka 7fdcbbaee9
Add high level bindings for js (#6048)
* [Draft] Added unfinished code for high level bindings for js

* * Rewrote structure of js api files
* Added more high level apis

* Minor fixes

* Fixed wasm github action

* Fix JS test

* Removed ContextOptions type

* * Added Ints to JS Api
* Added tests to JS Api

* Added run-time checks for contexts

* Removed default contexts

* Merged Context and createContext so that the api behaves the sames as in other constructors

* Added a test for Solver

* Added Reals

* Added classes for IntVals and RealVals

* Added abillity to specify logic for solver

* Try to make CI tests not fail

* Changed APIs after a round of review

* Fix test

* Added BitVectors

* Made sort into getter

* Added initial JS docs

* Added more coercible types

* Removed done TODOs
2022-06-14 09:55:58 -07:00
Gleb Popov 6f7be77e2b
Buildsystem fixes for FreeBSD. (#6029)
* Enable thread-local storage on FreeBSD.

* Pass -soname linker flag on FreeBSD.
2022-05-12 10:54:57 -07:00
Nikolaj Bjorner 3821eb4134 fpflags 2022-04-08 14:47:38 +02:00
Nikolaj Bjorner 67434a3096 again 2022-04-08 14:40:55 +02:00
Nikolaj Bjorner 9533dbaf5c missing arg specifier 2022-04-08 14:34:52 +02:00
Nikolaj Bjorner 746a4161af more passing of parameters 2022-04-08 14:24:21 +02:00
Nikolaj Bjorner cb6aba2315 more arm 2022-04-08 14:07:56 +02:00
Nikolaj Bjorner 79553261d1 no uname on nt 2022-04-08 07:02:32 +02:00
Nikolaj Bjorner 2e91d66888 Update mk_util.py
use more meaningful name
2022-04-08 06:28:36 +02:00
Nikolaj Bjorner c47bd1d01f add arm64 auto-detect
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-07 13:43:35 +02:00
Nikolaj Bjorner 8c2909f52b working on python make for arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-07 13:36:23 +02:00
Nikolaj Bjorner 05ec77cb56 revert 2022-04-03 12:20:10 -07:00
Nikolaj Bjorner 321745fdb1 #5941
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-03 11:07:54 -07:00
Matt Thornton 4e0a2f5968
Dispose of intermediate Z3Objects created in dotnet api. (#5901)
* Dispose of intermediate Z3Objects created in dotnet api.

* Set C# LangVersion to 8.0.

* Fix build errors.

* Fix warning about empty using statement.

* Fix Xor to only dispose of objects that it creates internally.
2022-03-17 08:08:05 -07:00
Emma Jane Bonestell dc110f10a4
Update mk_util.py (#5864)
Fix dynamic -lib opam builds on MSYS2
2022-02-23 03:36:46 -08:00
Nikolaj Bjorner b38b6daba3 add option to disable FPMATH 2022-02-20 15:33:13 +02:00
Nikolaj Bjorner 4f6fcf8ea7 fix #5814
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-08 10:20:19 +02:00
Nikolaj Bjorner ef3dd32364 some cleanup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-04 20:21:53 -08:00
Anton Kochkov f11fcec082
Migrate from deprecated distutils.sysconfig in scripts (#5729) 2021-12-22 07:59:13 -08:00
Weng Shiwei 723b755ca7
Fix the command of install_name_tool -id. (#5622)
* Fix the command of `install_name_tool -id`.

* Fix: don't call `ml_example.byte`.
2021-10-27 11:10:45 +02:00
Weng Shiwei 066076557f
Add post-install testing for ocaml binding. (#5617)
* Add path flags for cc loader (linux).

* Fix os linking and loading problem (maybe on #4840).

* Add post-install test of OCaml binding on ubuntu.

* Minor.

* Tentative CI for macos.
2021-10-25 11:21:02 +02:00
Weng Shiwei cd8d8bbb63
Fix runtime search path for shared-lib and add '-static' to the name of static-lib. (#5616)
* Fix runtime search path for shared-lib and add '-static' to static-lib.

* Revert the change on `META.in`.
2021-10-21 18:27:54 -04:00
Nikolaj Bjorner 9c7d9f06ed #5497 2021-08-22 17:22:37 -07:00
Nuno Lopes 2f9be23d90 attempt to fix MSVC build 2021-06-04 19:49:59 +01:00
Nikolaj Bjorner 88ec0f9fdd undo cxx hoist
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-06-04 11:39:46 -07:00
Nikolaj Bjorner 3655c399f5 hoist c++ flags
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-06-04 11:33:56 -07:00
Nikolaj Bjorner 887b62efe6 another patch 2021-04-07 18:20:45 -07:00
Nikolaj Bjorner 90995b63c3 fix nightly 2021-04-07 15:43:39 -07:00
Andrew V. Jones d0515dca50
Circular seq axioms node (#5104)
* Dealing with ambiguity when calling 'find_file' #5089

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

* Correcting ambiguity when calling 'find_file' if the file is in the current src dir #5089

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

* Ensuring consistency when obtaining the original include #5089

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
2021-03-16 06:58:54 -07:00
Nuno Lopes d396d46bd1 let's test if all the buildbots are happy with C++17
it's stil a bit too early for C++20
2021-02-18 18:13:10 +00:00
Nikolaj Bjorner 672e392386 guard
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-10 08:01:29 -08:00
Pierre Bouvier 24321e311b
Add support of the SunOS platform (Solaris, OpenSolaris, OpenIndiana) (#4757)
* Add support of the SunOS plateform (OpenSolaris, OpenIndiana) in scripts/mk_util.py

* Add missing casts for the SunOS plateform (OpenSolaris, OpenIndiana) for the pow function
2020-10-27 11:39:21 -07:00
Sergey Vladimirov 6324d2fb55
Set target for java classes to 1.8 (#4685) 2020-09-11 04:05:45 -07:00
Nikolaj Bjorner 4d586c2c13 remove stale references to gac/csc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-26 12:03:03 -07:00
Nikolaj Bjorner f17ead21f9 fix #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-21 10:11:39 -07:00
Nikolaj Bjorner e8b5abe63e revert - copy over xml in mk-dist mode #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 11:17:29 -07:00
Nikolaj Bjorner a7b71239ae copy over xml in mk-dist mode #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-20 10:22:57 -07:00