3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Commit graph

1759 commits

Author SHA1 Message Date
jofleish 88f4664c65 Standardize ubutu-latest vmImage 2022-08-15 07:55:45 -07:00
Nikolaj Bjorner 78eaefe5a8 move solver-params to params 2022-08-08 11:34:41 +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 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
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 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
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 cd7ef11593 add decide callbacks to propagator API
this is an intermediary state. The decide_eh is only partially implemented.
2022-07-27 04:28:41 +02:00
Nikolaj Bjorner 3a8eb1e7ec increase version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-22 12:43:19 -07:00
Nikolaj Bjorner 845e852dba increment to include python fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-22 11:44:32 -07:00
Nikolaj Bjorner c6dad4a9ea Update release.yml for Azure Pipelines
Enable pypi publishing for 4.10 wheels
2022-07-22 10:01:49 -07:00
Nikolaj Bjorner 9cd3b9cad7 Merge branch 'master' of https://github.com/z3prover/z3 2022-07-21 20:28:02 -07:00
Nikolaj Bjorner adcb3e8f86 set version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-21 20:27:50 -07:00
Nikolaj Bjorner 59d47e3055 don't publish pypi yet
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-21 14:43:49 -07:00
Nikolaj Bjorner 7ded856bb1 script to test jsdoc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-18 09:51:34 -07: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 faf6c02cf8 remove --js from nightly and release doc builds as the npm run 'check-engine' fails
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-12 07:46:06 -07:00
Nikolaj Bjorner 4dc88f0993 add --js to nightly and release scripts, nb @ritave
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-11 20:37:50 -07:00
Stefan Muenzel 99212a2726
Use int64 for ocaml api functions that require it (#6150)
* Use int64 for ocaml api functions that require it

Signed-off-by: Stefan Muenzel <source@s.muenzel.net>

* Use elif

Signed-off-by: Stefan Muenzel <source@s.muenzel.net>
2022-07-11 09:25:05 -07:00
Nikolaj Bjorner 9d9414c111 inc version number 2022-07-06 14:00:40 -07:00
Nikolaj Bjorner cc841caf08 increment minor version for dev branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-06 10:15:34 -07:00
Nikolaj Bjorner 2ae84f88df Update release.yml for Azure Pipelines 2022-07-06 09:10:16 -07:00
Nikolaj Bjorner 15391fc9b9 remove musll from release.yml
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-06 07:37:51 -07:00
Nikolaj Bjorner f1b7ab3d3f x64
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-06 01:53:26 -07:00
Nikolaj Bjorner 7f2ebf84a2 Remove package sub-directory from release script 2022-07-06 01:09:11 -07:00
Nikolaj Bjorner bda86726af macarm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-05 20:02:27 -07:00
Nikolaj Bjorner 4f62336fa8 download arm64
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-05 18:23:32 -07:00
Nikolaj Bjorner 593d5be202 bind variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-05 17:21:59 -07:00
Nikolaj Bjorner 8b35b7becc bind variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-05 17:20:21 -07:00
Nikolaj Bjorner 594b5daa9d remove download of mullinux
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-05 17:18:04 -07:00
Nikolaj Bjorner 3ce6663536 update release script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-05 17:17:07 -07:00
Nikolaj Bjorner 73f35e067c Update release.yml for Azure Pipelines
pre-release
2022-07-05 17:13:55 -07:00
Nikolaj Bjorner 282c786f1c setting version to release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-05 11:51:12 -07:00
Nikolaj Bjorner e6e0c74324
Update update_api.py
fix typo
2022-07-02 13:17:14 -07:00
Nikolaj Bjorner c35d0d1e49
Update update_api.py
add automation!
2022-07-02 13:05:35 -07:00
Nikolaj Bjorner 5ba8231d07 make it work with old pythons
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-21 09:10:38 -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
Clemens Eisenhofer 2fa60aa43c
Added function to select the next variable to split on (User-Propagator) (#6096)
* Added function to select the next variable to split on

* Fixed typo

* Small fixes

* uint -> int
2022-06-19 10:49:25 -07:00
Nuno Lopes 73a24ca0a9 remove '#include <iostream>' from headers and from unneeded places
It's harmful to have iostream everywhere as it injects functions in the compiled files
2022-06-17 14:10:19 +01: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
Nikolaj Bjorner 93a0322cac update distribution scripts 2022-06-02 11:48:12 -07:00
Nikolaj Bjorner 366860be46 change to osx-11.0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-02 07:21:48 -07:00
Nikolaj Bjorner c7560e1394 change to osx-11.0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-02 07:20:28 -07:00
Nikolaj Bjorner 4191d84e58 change to 11.0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-02 07:12:45 -07:00
Nikolaj Bjorner 0b17a568ee fixes to script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-02 06:59:59 -07:00
Nikolaj Bjorner 9190f22eb4 os
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-01 21:23:44 -07:00
Nikolaj Bjorner 6396cfd6e7 os
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-01 21:20:19 -07:00
Nikolaj Bjorner 9ed7fd9454 Update nightly.yaml for Azure Pipelines 2022-06-01 19:17:27 -07:00
Nikolaj Bjorner aa8e89c5f3 try macos12 for arm64
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-01 19:11:17 -07:00
Nikolaj Bjorner bffa7ff2f6 add hint verification, combine bounds/farkas into one rule
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-29 10:12:05 -07:00
Nikolaj Bjorner 36ad377a7d na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-29 09:21:43 -07:00
Nikolaj Bjorner 9ec34d96ce comment out muslinux build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 18:14:42 -07:00
Nikolaj Bjorner 6abea2de2c fix nightly, fix regression identified by Nuno
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 18:03:15 -07:00
Nikolaj Bjorner ddc3445707 try to add back musllinux
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 14:47:39 -07:00
Nikolaj Bjorner 35db0ae58b workaround manylinux build failure (it is advertized as a compiler bug)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 14:34:58 -07:00
Nikolaj Bjorner d09d37cb10 wt$
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 14:27:22 -07:00
Nikolaj Bjorner 6b4bc5bd38 remove broken matrix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 14:26:00 -07:00
Nikolaj Bjorner e9660016bc remove hardwired image name
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 14:21:23 -07:00
Nikolaj Bjorner 6ce03cd6f0 Update nightly.yaml for Azure Pipelines 2022-05-28 14:18:50 -07:00
Nikolaj Bjorner 0038817656 Update nightly.yaml for Azure Pipelines 2022-05-28 14:13:50 -07:00
Nikolaj Bjorner 48701826f1 indent
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 13:57:03 -07:00
Nikolaj Bjorner 363b69f588 fix #6034 2022-05-16 16:44:13 -07:00
Nikolaj Bjorner f6b2874d7c update to take effect of def_API for callback functions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-16 10:30:54 -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
John Jones 361888f299
Generate bdist wheels for musllinux_1_1 (#6025) 2022-05-09 14:13:08 -07:00
Nikolaj Bjorner 8218f25222 add decide callback
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-08 15:30:03 -07:00
Nikolaj Bjorner 3b441137c0 ocaml build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-08 11:01:23 -07:00
Nikolaj Bjorner d58de2f8e4 java build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-08 10:20:32 -07:00
Nikolaj Bjorner a71ce54c34 freeze functions with callbacks for ocaml
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-08 10:04:50 -07:00
Nikolaj Bjorner cf4149d53e freeze functions with callbacks for ocaml
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-08 10:02:41 -07:00
Nikolaj Bjorner 1ab7be67d0 java build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-08 09:58:43 -07:00
Nikolaj Bjorner a3b066f0b4 ml: VOIDP -> ptr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-07 12:49:05 -07:00
Nikolaj Bjorner b633947762 don't log function pointers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-07 12:41:51 -07:00
Nikolaj Bjorner 6d40e6f401 java
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-07 11:24:46 -07:00
Nikolaj Bjorner 14214c5a07 exposing user propagators over .Net
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-07 11:08:40 -07:00
Nikolaj Bjorner 3ae781039b inc version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-05 07:09:54 -07:00
Nikolaj Bjorner d420706eae enable pypi release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-04 17:16:30 -07:00
Nikolaj Bjorner 47459ca795 pre-release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-04 12:04:51 -07:00
Nikolaj Bjorner 0b453a4af5 set release version 2022-04-25 08:57:32 +01:00
Nikolaj Bjorner 33ffd464cf inc version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-24 12:17:07 +01:00
Nikolaj Bjorner 0529e88589 enable pypi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-23 19:51:25 +01:00
Nikolaj Bjorner 8e509d34b5 remove test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-23 19:05:42 +01:00
Nikolaj Bjorner 8778f4d43f updated release script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-23 17:59:23 +01:00
Nikolaj Bjorner e6e00d894f update nightly/release scripts to produce arm64 for what is tested
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-21 10:18:40 +01:00
Nikolaj Bjorner c996a66da0 separate pre-processing, add callback parameter to push/pop in python API 2022-04-11 17:05:59 +02:00
Nikolaj Bjorner fe834b9e4e update regex 2022-04-09 07:40:48 +02:00
Nikolaj Bjorner c98eda03f7 nightly osx arm64 wheel 2022-04-09 06:55:31 +02:00
Nikolaj Bjorner fbd35fb58d skip unit tests for arm 2022-04-08 16:55:39 +02:00
Nikolaj Bjorner 91ca02864c arm64
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-04-08 14:59:22 +02: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 babac78c99 syntax error? 2022-04-08 06:59:07 +02:00
Nikolaj Bjorner 83d2aa85ec add arm64 build path 2022-04-08 06:35:25 +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
fleisherdev a863a91b13
Allow nightly builds to complete even if package signing fails - NOT published to nuget.org (#5951)
Co-authored-by: jofleish <jofleish@microsoft.com>
2022-04-07 08:19:21 +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
Nikolaj Bjorner b0605a9d36 Update nightly.yaml 2022-03-27 18:29:55 -10:00
Nikolaj Bjorner cb1e16fd76 Update nightly.yaml for Azure Pipelines 2022-03-27 17:42:16 -10:00
Nikolaj Bjorner da00deead8 disable arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-27 17:40:03 -10:00
Nikolaj Bjorner ae07a53764 Update nightly.yaml for Azure Pipelines 2022-03-26 17:14:31 -10:00
Nikolaj Bjorner a9a843294e try add ARM path for MacOS
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-26 17:10:23 -10:00
jofleish 42da9760f9 Continue on error in GitHub tagging 2022-03-24 12:35:10 -04:00
jofleish a4af26e2f0 Shorten public feed to Z3Nightly 2022-03-23 16:25:34 -04:00
jofleish bb4a2b97b6 remove project from public/org level feed 2022-03-23 14:28:43 -04:00
jofleish b8c61ca278 continue on error in deploy 2022-03-23 12:31:35 -04:00
jofleish 3ffc3c2f97 continue on github tagging error 2022-03-23 12:30:52 -04:00
jofleish 1ee3de5409 temporary workaround for build 2022-03-23 12:25:31 -04:00
jofleish d9e93d5f7c revert to buildid in version number 2022-03-23 09:53:15 -04:00
jofleish 13a33a3966 fix authentication input 2022-03-23 08:51:20 -04:00
jofleish 16f47954c0 Use camel case service name 2022-03-23 08:50:14 -04:00
jofleish 7bf2df1b7a Update nightly nuget service connection 2022-03-23 08:44:42 -04:00
jofleish 8273a20498 test publish to public project feed 2022-03-22 17:26:12 -04:00
John Fleisher ce04c16a6f
Jfleisher/nightlynuget (#5916)
* WiP: Test nightly version number change

* Fix debug assert

* WiP: test nuget publish to AzDo feed for nightly build

* WiP: Make Nuget deploy separate stage

* WiP: fix nightly stage name

* change nuget push to vstsfeed

* Try case sensitive name for artifacts

* WiP: use artifact folder names

* add Rev version to package

* WiP: build def variation on nightly build version

* WiP: use Build_BuildNumber and Build_DefinitionName

* WiP: using hyphen in nightly version

* Tag nightly packages with datetime

* fix commit

* Build.BuildId and Build.DefinitionName

* WiP: change suffix format to lead with alpha

* test z3public feed publish

* revert public publish test

* WiP: test build# versioning scheme

* WiP: another variant on version number for nightly

Co-authored-by: jfleisher <jofleish@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-22 12:19:58 -07:00
Nikolaj Bjorner a418678cd4 increment version number 2022-03-20 14:34:34 -07:00
Nikolaj Bjorner 1e8bae01e9 enable pypi in release pipeline
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 13:12:29 -07:00
Nikolaj Bjorner 9061ca58f1 call it macOSBuild 2022-03-19 15:25:50 -07:00
Nikolaj Bjorner b5b9c85c40 call it UbuntuBuild 2022-03-19 15:24:53 -07:00
Nikolaj Bjorner dfa65443e9 fix name for artifact
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-19 13:51:58 -07:00
Nikolaj Bjorner fd1f5cdd0f fix callback type declarations for propagators 2022-03-19 12:24:46 -07:00
Nikolaj Bjorner eaa2fb76ca update release pipeline with x86 Nuget
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-19 11:46:27 -07:00
Nikolaj Bjorner 81a5e56c89 publish to github
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 18:58:27 -07:00
Nikolaj Bjorner 39df8ee372 update win build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 17:39:58 -07:00
Nikolaj Bjorner 29e288367e pre-release pipeline
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 16:22:48 -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
Nikolaj Bjorner e7ded9cdbd update to 2022 2022-03-08 08:36:19 -08:00
Nuno Lopes 689e2d41de remove a bunch of unneeded memory allocations 2022-02-25 16:08:23 +00: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 456b8ee682 nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-21 04:18:05 -08:00
Nikolaj Bjorner c47e5aff60 multi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-20 14:03:13 -08:00
Nikolaj Bjorner cfe9846f0c multi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-20 13:59:42 -08:00
Nikolaj Bjorner b38b6daba3 add option to disable FPMATH 2022-02-20 15:33:13 +02:00
Nikolaj Bjorner 14ee02183c nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-20 13:43:11 +02:00
Nikolaj Bjorner e800269cee na 2022-02-20 13:05:53 +02:00
Nikolaj Bjorner c25d710958 try out arch arm64 on the mac 2022-02-20 10:31:29 +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 b259f46f85 dependencies 2022-01-13 12:34:58 -08:00
Nikolaj Bjorner 08294d62e5 separate dependencies for qe_lite 2022-01-12 03:26:22 -08:00
Nikolaj Bjorner 9ac57fc510 update version number for next release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-09 17:11:08 -08:00
Nikolaj Bjorner 174889ad5e id 2022-01-08 16:28:12 -08:00
Nikolaj Bjorner afbfea8ce6 name the package
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-08 15:52:50 -08:00
Nikolaj Bjorner 36ed1ffac2 update name of artifact
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-08 15:13:46 -08:00
Nikolaj Bjorner 40761ebb0d bug in script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-08 12:10:16 -08:00
Nikolaj Bjorner c2aff52dd7 os-info back to common 2022-01-08 11:33:43 -08:00
Nikolaj Bjorner d391043ffd only one arch at a time 2022-01-08 11:32:08 -08:00
Nikolaj Bjorner 2c44454a17 self -> env 2022-01-08 10:58:36 -08:00
Nikolaj Bjorner d6ce05009b try separate x86
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-08 10:14:28 -08:00
Nikolaj Bjorner 5ec7a66a45 change class name, add comment 2022-01-04 22:02:14 -08:00
Nikolaj Bjorner 964a5cd761 lump java together
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-04 20:48:05 -08:00
Nikolaj Bjorner ef3dd32364 some cleanup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-04 20:21:53 -08:00
Nikolaj Bjorner 7d311ac2ef use netstandard 2.0 per recommendations
seems that now the recommended starting point is 2.0 and not lower.
2021-12-25 13:44:49 -08:00
Nikolaj Bjorner ecf41972b1 increase minor version
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-23 14:41:52 -08:00
Nikolaj Bjorner dc09d3c5ea fix typo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-23 14:41:52 -08:00
Nikolaj Bjorner df8f9d7dcb Update release.yml for Azure Pipelines 2021-12-23 12:43:00 -08:00
Nikolaj Bjorner bd2a53c475 Update release.yml for Azure Pipelines 2021-12-23 11:48:08 -08:00
Nikolaj Bjorner 5d4420a763 Update release.yml for Azure Pipelines 2021-12-23 11:46:47 -08:00
Nikolaj Bjorner a00d68fe5a update release scripts and notes in master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-23 11:43:38 -08:00
Anton Kochkov f11fcec082
Migrate from deprecated distutils.sysconfig in scripts (#5729) 2021-12-22 07:59:13 -08:00
Nikolaj Bjorner db62038845 Update nightly.yaml
see if this gets us past the upload to GitHub issue
2021-12-16 14:20:40 -08:00
Nikolaj Bjorner 4641a20f4f #5700 - Add download x86 as part of release NuGet
x86 is part of nightly NuGet but was not added to the release pipeline.
2021-12-16 13:50:31 -08:00
Nikolaj Bjorner 4587575649 if you read this commit message you probably are a programmer who has no life
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-18 20:25:47 -08:00
Nikolaj Bjorner 43a827c931 Update release.yml for Azure Pipelines 2021-11-18 16:05:22 -08:00
Nikolaj Bjorner 71d5d2486c Update release.yml for Azure Pipelines 2021-11-18 15:01:43 -08:00
Nikolaj Bjorner 72f28f06e4 Update release.yml for Azure Pipelines 2021-11-18 14:05:13 -08:00
Nikolaj Bjorner b95ba89dbe update release pipeline
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-18 13:09:13 -08:00
Nikolaj Bjorner feadfbfba4 enable publish
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-18 12:00:44 -08:00
Nikolaj Bjorner 5194aa186a nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-17 09:36:50 -08:00
Nikolaj Bjorner 1752055aa6 update nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-16 09:49:16 -08:00
Nikolaj Bjorner c826b64e35 prepare release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-16 09:41:51 -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
Nuno Lopes 9b5ec6d004 logging cleanup
move everything out-of-line as common path doesn't log
fix some race conditions on file ptr vs enable_logging vars
2021-08-29 12:24:19 +01:00
Nuno Lopes 1f4a7c5101 logging: don't call the returned function twice (one for log, one for return)
Z3_simplify() does RETURN_Z3(simplify(...)), hence the function was being called twice
it turns out simplify is not idempotent, so calling it twice can result in different results
thus breaking the log.
2021-08-29 11:06:19 +01:00
Nikolaj Bjorner 9c7d9f06ed #5497 2021-08-22 17:22:37 -07:00
Karlheinz Friedberger 764e033bf4
Specify and document value for environment variable for loading native library in Java bindings (#5477)
* limit range of environment variable for loading the native library in Java to "true".

This change specifies the range of values that are allowed to set the environment
variable "z3.skipLibraryLoad".
Only the value "true" (in upper-, lower-, and mixed-case is accepted as valid value.
Other values, such as "false", "0", "1", "foo", an empty or a missing value are
evaluated to "false" and cause the default loading of the native library.

* adding documentation about environment variable for (not) loading the native library in Java.

This is a follow-up commit for #4667 to provide a publicly visible documentation.
2021-08-13 14:54:02 -07:00
Nikolaj Bjorner 6dfaaa43cd jobs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-30 22:38:56 -07:00
Nikolaj Bjorner 3f6a7748fa jobs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-30 22:38:16 -07:00
Nikolaj Bjorner ce23798cd0 coverage.yml
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-30 22:36:14 -07:00
Nikolaj Bjorner 211a6c8752 rename
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-29 11:32:20 -07:00
Nikolaj Bjorner d0686671c5 Merge branch 'master' of https://github.com/z3prover/z3 2021-07-29 11:31:45 -07:00
Nikolaj Bjorner db5252a81b add dummy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-29 11:31:39 -07:00
0152la 72d3074a44
Add Ubuntu CMake Coverage CI step (#5442)
Adds an extra step to CI jobs which executes the Z3 test suite with
coverage enabled, and additionally executed coverage-enhancing tests
added to z3test.
2021-07-29 11:29:49 -07:00
Nikolaj Bjorner a3010c8875 version inc, bvsort->bitvecsort 2021-07-13 17:14:47 +02:00
Nikolaj Bjorner 3a402ca2c1 Update release.yml for Azure Pipelines 2021-07-13 15:25:23 +02:00
Nikolaj Bjorner 75a5de99ca Update release.yml for Azure Pipelines 2021-07-13 15:24:19 +02:00
Nikolaj Bjorner 4c53655be7 add z3doc build to release script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-11 23:26:48 +02:00
Nikolaj Bjorner 10ad5bae21 increment version
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-11 06:17:58 +02:00
Nikolaj Bjorner bc2e6ce037 Update release.yml for Azure Pipelines 2021-07-10 22:42:02 +02:00
Nikolaj Bjorner 34885562e0 try without #!/bin/env python #5397 2021-07-10 15:20:56 +02:00
Iain Scott d61d5081a2
Delete unused NuGet release script. (#5351) 2021-06-16 10:48:51 -05:00
Nikolaj Bjorner 39af2a188d centos -> glibc 2021-06-04 15:54:19 -07:00
Nikolaj Bjorner 84b86ac8d2 updated ref to esrp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-06-04 15:13:34 -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 654e53e762 auxiliary build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-06-04 11:15:13 -07:00
Nikolaj Bjorner 7ce88ec032 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-06-04 11:02:00 -07:00
Nikolaj Bjorner dea7c92730 updated nightly 2021-06-04 10:54:32 -07:00
Iain Scott 48beb814f5
Use more generic linux-x64 for NuGet rid instead of specific ubuntu, debian, etc. (#5310) 2021-05-28 13:53:52 -07:00
Nikolaj Bjorner 8ba0fb5b58 rounding mode sort removed for incompatibility
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-21 16:18:43 -07:00
Iain Scott c18f012c83
Remove x64 suffix from NuGet package names. (#5292) 2021-05-21 13:51:02 -07:00
Matt Thornton ce1a48486e
Fix NuGet package name and glibc rid. (#5290) 2021-05-21 08:41:29 -07:00
Nikolaj Bjorner a59dcfdeab update python tag
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-20 15:23:39 -07:00
Matt Thornton 9cc1549dbe
Use osx-x64 for mac rid rather than macos. (#5288) 2021-05-20 15:19:31 -07:00
Nikolaj Bjorner a166aca48e na 2021-04-08 15:48:07 -07:00
Nikolaj Bjorner 9ef7cf1e81 test old connection 2021-04-08 12:14:29 -07:00
Nikolaj Bjorner 887b62efe6 another patch 2021-04-07 18:20:45 -07:00
Nikolaj Bjorner 6e1ac19c44 new name 2021-04-07 17:43:32 -07:00
Nikolaj Bjorner 90995b63c3 fix nightly 2021-04-07 15:43:39 -07:00
Nikolaj Bjorner eb13ad14e5 python build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-17 16:26:44 -07:00
Nikolaj Bjorner ab0735fde2 separate component for asserted_formulas to break dependency cycles
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-17 15:51:38 -07:00
Nikolaj Bjorner 25343232ca add dependency 2021-03-17 15:36:02 -07:00
Nikolaj Bjorner ddbcd08d46 move asserted_formulas to solver scope 2021-03-17 15:02:16 -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
Nikolaj Bjorner d03fdf5fed more descriptive naming convention 2021-03-15 15:48:33 -07:00
Nikolaj Bjorner 4b3fecc35e remove dependency on ast from params 2021-03-15 15:40:41 -07:00
Nikolaj Bjorner 1cb0dbae51 missing dependency for python build 2021-03-14 20:45:30 -07:00
Nikolaj Bjorner 8412ecbdbf fixes to new solver, add mode for using nlsat solver eagerly from nla_core 2021-03-14 13:57:04 -07:00
Nikolaj Bjorner bef6f1a729 fix build 2021-03-02 13:51:58 -08: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 85f0084e9c set options and change VS for nightly 2021-02-12 13:41:30 -08:00
Nikolaj Bjorner 80d297dca2 Try to move using windows latest instead of VS2017 2021-02-12 12:45:21 -08:00
Nikolaj Bjorner d0c96abe30 log classificaiton
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-02-11 14:44:05 -08:00
Nikolaj Bjorner 1d12b72bbc log classificaiton
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-02-11 14:43:05 -08:00
Nikolaj Bjorner 98eae28fca try to update setup.py to libc naming
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-02-11 11:52:05 -08:00
Nikolaj Bjorner b6294ab235 is glibc the new centos?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-02-11 11:17:33 -08:00
Nikolaj Bjorner c03bd5e1c8 is glibc the new centos?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-02-11 11:17:04 -08:00
Nikolaj Bjorner 5d46ac0aca is glibc the new centos?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-02-11 11:14:39 -08:00
Nikolaj Bjorner b7d1d03b08 try revert to u18 for centos zip 2021-02-11 10:36:48 -08:00
Nikolaj Bjorner 2301fce65e it helps to spell
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-02-11 09:44:03 -08:00
Nikolaj Bjorner 9883a0b983 downgrade to Ubuntu 18 for ocaml doc build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-02-11 09:43:22 -08:00
Nikolaj Bjorner 9cdb875ba2 remove use of deprecated linux_distribution 2021-02-11 09:40:23 -08:00
Don Syme 504b6559ab
[WIP] Suggestion: build .NET package for both x86 and x64 and rename (#5021)
* build package for x86

* build package for x86

* build package for x86

Co-authored-by: Don Syme <donsyme@fastmail.com>
2021-02-11 09:29:32 -08:00
Nikolaj Bjorner 16448104eb add new model event handler for incremental optimization 2021-02-05 17:11:04 -08:00
Nikolaj Bjorner c623e2db28 typo 2021-02-01 09:14:26 -08:00
Nikolaj Bjorner 60cc9d8182 set unicode by default 2021-01-31 11:32:33 -08:00
Nikolaj Bjorner 39bfdbd8c0 make the right diretory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-30 05:01:16 -08:00
Nikolaj Bjorner c99b805c14 mld
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-29 18:37:38 -08:00
Nikolaj Bjorner 87cd3487e5 missing pattern dependency
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-29 16:44:47 -08:00