mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity
16421 commits 23 branches 48 tags 156 MiB
Commit graph

1472 commits

Author SHA1 Message Date
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
Nikolaj Bjorner 34c34b68ee one more nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 16:40:59 -08:00
Nikolaj Bjorner 41a4d102f4 try ocamlfind in the loop 
Thanks to @c-cube
 2021-01-29 13:37:16 -08:00
Nikolaj Bjorner b11203e2d2 try local env 2021-01-29 08:41:14 -08:00
Nikolaj Bjorner 1d7cabaf9a typo 2021-01-29 08:15:40 -08:00
Nikolaj Bjorner a2d344c401 use build path 2021-01-29 07:32:04 -08:00
Nikolaj Bjorner 1f71aeded9 ocamldoc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 06:47:10 -08:00
Nikolaj Bjorner 5c9b205dfc run mk_api_doc in the same environment as make where opan config env is used 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 06:25:24 -08:00
Nikolaj Bjorner 8a229bf684 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 22:39:02 -08:00
Nikolaj Bjorner c271a42a2e change zip command 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 21:01:08 -08:00
Nikolaj Bjorner de9f215d12 generate Ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 20:58:43 -08:00
Nikolaj Bjorner a526eea123 doc/api not doc/html 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 20:01:46 -08:00
Nikolaj Bjorner 1800b48258 zip doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 19:38:51 -08:00
Nikolaj Bjorner c8aab1972a have nightly generate doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 16:05:41 -08:00
Nikolaj Bjorner 3d4a43f07b have nightly generate doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 16:04:08 -08:00
Nikolaj Bjorner 7068ccdebd have nightly generate doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 16:01:42 -08:00
Nikolaj Bjorner d08814a1fe have nightly generate doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 15:57:01 -08:00
Nikolaj Bjorner d2abc9ed0f remove comment #4956 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-21 22:18:24 -08:00
pcarbonn 0eb04df834
fix #4956 (#4958) 2021-01-21 22:16:49 -08:00
Nikolaj Bjorner 987efced76 upgrade compilers 2021-01-21 14:25:08 -08:00
Nikolaj Bjorner 6f09ecb229 set version 2021-01-21 14:24:58 -08:00
Nikolaj Bjorner fb48481860 update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 12:51:48 -08:00
Nikolaj Bjorner 517d907567 Update release.yml for Azure Pipelines 2021-01-20 12:06:47 -08:00
Nikolaj Bjorner af914f101e change to macos latest 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 10:19:00 -08:00
Nikolaj Bjorner 3f2349f0f7 update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 01:36:09 -08:00
Nikolaj Bjorner 80f429c3fb nuget 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 00:33:05 -08:00
Nikolaj Bjorner 3bc18ab0d1 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-19 23:54:10 -08:00
Nikolaj Bjorner ec5d08ac00 update release script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-19 23:24:17 -08:00
Nikolaj Bjorner 91c54f6c39 na 2021-01-12 14:03:55 -08:00
Nikolaj Bjorner 8abb644378 add xml file to the mix #4578 2021-01-12 00:23:02 -08:00
Nikita Leshenko d8eba2d72f
scripts/update_api: Replace Z3_LIBRARY_DIRS with Z3_LIB_DIRS (#4915) 
The error message that is printed when libz3.so can't be loaded contains
incorrect instruction to set `Z3_LIBRARY_DIRS` builtin. The correct variable
name is `Z3_LIB_DIRS`.

Signed-off-by: Nikita Leshenko <nikita@leshenko.net>
 2020-12-26 12:27:10 -08:00
Nikolaj Bjorner 6284f6fb03 Update nightly.yaml for Azure Pipelines 2020-12-22 14:45:15 -08:00
Nikolaj Bjorner 9d22cf4d4f add signing to nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-22 13:13:04 -08:00
Nikolaj Bjorner 1c3b768ed0 update ubuntu version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-22 12:38:05 -08:00
Nikolaj Bjorner 0ed33af279 Update nightly.yaml for Azure Pipelines 2020-12-22 11:52:09 -08:00
Nikolaj Bjorner 8692fcdf3b Update nightly.yaml for Azure Pipelines 2020-12-22 10:47:33 -08:00
Nikolaj Bjorner d72f6c80df Update nightly.yaml for Azure Pipelines 2020-12-22 09:58:03 -08:00
Nikolaj Bjorner 010d578e8f sym file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 18:08:23 -08:00
Nikolaj Bjorner 021bd8a994 sym file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 17:08:38 -08:00
Nikolaj Bjorner f26662d079 na 2020-12-21 16:18:07 -08:00
Nikolaj Bjorner 3576b66e32 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 15:46:42 -08:00
Nikolaj Bjorner 0c94d6dab6 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 13:43:50 -08:00
Nikolaj Bjorner d67f9fb3f1 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 13:07:00 -08:00
Nikolaj Bjorner 835dd9414f nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 13:06:26 -08:00
Nikolaj Bjorner 3121c39a14 nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 13:04:00 -08:00
Nikolaj Bjorner d0fbeb11c9 Update nightly.yaml for Azure Pipelines 2020-12-21 11:57:00 -08:00
Nikolaj Bjorner a72856111b add destination to custom command 2020-12-21 11:42:04 -08:00
Nikolaj Bjorner a164087384 remove cheap-eqs option as there is already propagate_eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 11:04:04 -08:00
Nikolaj Bjorner 5866d6ee3f custom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 09:40:08 -08:00
Nikolaj Bjorner 84a7f3fcd0 quote? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 08:54:46 -08:00
Nikolaj Bjorner 5a20413d04 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 18:03:06 -08:00
Nikolaj Bjorner 715b1fd393 try snupkg parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 17:54:11 -08:00
Nikolaj Bjorner 9e54cd63dc wrap remove/move 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 16:19:21 -08:00
Nikolaj Bjorner 2c313ddb7a wrap remove/move 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 15:46:26 -08:00
Nikolaj Bjorner d94244b236 shutil.remove -> os.remove 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 13:59:17 -08:00
Nikolaj Bjorner 726853de4e add stages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 13:57:54 -08:00
Nikolaj Bjorner b108f5163d add stages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 13:56:54 -08:00
Nikolaj Bjorner 6c42e8068c shutil.remove -> os.remove 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 13:47:19 -08:00
Nikolaj Bjorner 6b312a58a3 move/remove 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 12:06:46 -08:00
Nikolaj Bjorner 9e86c8761e move/remove 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 12:06:16 -08:00
Nikolaj Bjorner 8cb1dd29b5 mk-nuget-task where is the icon? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 11:16:47 -08:00
Nikolaj Bjorner dd05c683e0 update license to nuget 4.9 URL 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 10:34:24 -08:00
Nikolaj Bjorner 359d66b579 Update nightly.yaml for Azure Pipelines 2020-12-19 18:42:32 -08:00
Nikolaj Bjorner 76a4bf5fa0 Update nightly.yaml for Azure Pipelines 2020-12-19 18:42:10 -08:00
Nikolaj Bjorner 64a92f720b new nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-19 18:24:02 -08:00
Nikolaj Bjorner c100a18b37 use ReleaseVersion macro 2020-12-19 17:34:54 -08:00
Nikolaj Bjorner 3cd49d56c2 Update nightly.yaml for Azure Pipelines 2020-12-19 17:29:26 -08:00
Nikolaj Bjorner 5ce3c18fd0 Update nightly.yaml for Azure Pipelines 2020-12-19 16:59:07 -08:00
Nikolaj Bjorner e8b506a172 update for nuget 2020-12-19 16:56:25 -08:00
Nikolaj Bjorner 4039785bb6 initial steps for including symbols 
@ahelwer - seems several steps are involved for enableing snupkg. I will try to see if I can get there. The NugetCommand@2 specifies whether to include symbols, but I haven't found the portion where it allows the user to specify the name of the package (to snukpg instead of nupkg).
 2020-12-19 16:44:05 -08:00
Nikolaj Bjorner 72e57f550d update release similar to nightly 2020-11-11 17:38:07 -08:00
Nikolaj Bjorner fdd3e6c4c2 Update nightly.yaml for Azure Pipelines 2020-11-10 16:26:06 -08:00
Nikolaj Bjorner 8c60e7b8f4 Update nightly.yaml for Azure Pipelines 2020-11-10 16:24:56 -08:00
Nikolaj Bjorner 41cc037204 change manylinux to ubuntu-latest 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-10 16:17:35 -08:00
Nikolaj Bjorner 5ace60c812 enforce guard option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-10 09:22:32 -08: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
Nikolaj Bjorner 72d407a49f
mbp (#4741) 
* adding dt-solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* dt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* move mbp to self-contained module

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Create CMakeLists.txt

* dt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* rename to bool_var2expr to indicate type class

* mbp

* na

* add projection

* na

* na

* na

* na

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* deps

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* testing arith/q

* na

* newline for model printing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-21 15:48:40 -07:00
Nikolaj Bjorner 2f756da294
adding dt-solver (#4739) 
* adding dt-solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* dt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* move mbp to self-contained module

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Create CMakeLists.txt

* dt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* rename to bool_var2expr to indicate type class

* mbp

* na
 2020-10-18 15:28:21 -07:00
Nikolaj Bjorner 44679d8f5b
arith_solver (#4733) 
* porting arithmetic solver

* integrating arithmetic

* lp

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-16 10:49:46 -07:00
Nikolaj Bjorner fa58a36b9f
model refactor (#4723) 
* refactor model fixing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* missing cond macro

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add macros dependency

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* deps and debug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add dependency to normal forms

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* build issues

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* compile

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix leal regression

* complete model fixer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fold back private functionality to model_finder

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* avoid duplicate fixed callbacks

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-05 14:13:05 -07:00
Nikolaj Bjorner 79162b96f3 updated dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-01 08:11:55 -07:00
Nikolaj Bjorner cddb32a21d remove out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-29 13:43:50 -07:00
Nikolaj Bjorner 4562c07ceb redo egraph 2020-09-29 13:43:49 -07:00
Nikolaj Bjorner 43db7df2b5
user solver (#4709) 
* user solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-24 04:55:34 -07:00
Nikolaj Bjorner d56dd1db7b update version' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-11 04:37:35 -07:00
Sergey Vladimirov 6324d2fb55
Set target for java classes to 1.8 (#4685) 2020-09-11 04:05:45 -07:00
Nikolaj Bjorner c7ba86e227 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 21:49:43 -07:00
Nikolaj Bjorner f11e2d0eba try again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 20:00:25 -07:00
Nikolaj Bjorner 7dbf30b465 include nupkg 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 19:21:46 -07:00
Nikolaj Bjorner 3616688d6b update pipeline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 17:26:47 -07:00
Nikolaj Bjorner 9cb47188ea Update release.yml for Azure Pipelines 2020-09-10 15:41:12 -07:00
Nikolaj Bjorner 79734f26ae move to python3 for release.yml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 11:51:28 -07:00
Nikolaj Bjorner 6e7a80b68e change version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 10:59:06 -07:00
Nikolaj Bjorner c481570257 disable pip in trial release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 10:16:57 -07:00
Nikolaj Bjorner fe43f8df8f na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-03 08:11:43 -07:00
Nikolaj Bjorner 35e3d8425c move fpa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 11:16:21 -07:00
Nikolaj Bjorner b9cbb08858 shuffle dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 09:51:39 -07:00
Nikolaj Bjorner 86c11b9349 order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 13:05:25 -07:00
Nikolaj Bjorner b03d1c8053 deps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 13:01:49 -07:00
Nikolaj Bjorner 0440cfeea7 add smt params dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 12:59:22 -07:00
Nikolaj Bjorner 4244ce4aad adding ack/model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 12:55:47 -07:00
Sergey Vladimirov 7f0b5bc129
Allow to skip System.loadLibrary() calls from Java Native class (#4667) 2020-08-28 07:30:26 -07:00
Nikolaj Bjorner 4ab35a9bb5 euf model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-26 15:55:20 -07:00
Nikolaj Bjorner c21a2fcf9f sat solver setup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-26 09:40:42 -07:00
Nikolaj Bjorner ecd3315a74 add sat-euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-25 12:16:57 -07:00
Nikolaj Bjorner 3dedc13481 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-24 02:00:37 -07:00
Nikolaj Bjorner 65e6d942ac euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-24 01:55:13 -07:00
Nikolaj Bjorner 96f10b8c1c user propagator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-22 19:01:04 -07:00
Nikolaj Bjorner 2d5b749745 extend solver callbacks with methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-21 19:24:59 -07:00
Nikolaj Bjorner 080be7a2af merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-21 12:14:28 -07:00
Nikolaj Bjorner 4857d60c99 user propagator over the API 2020-08-18 21:53:02 -07:00
Nikolaj Bjorner e591b321bb set guard/cf and dynamic base in release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-17 08:21:44 -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
Nikolaj Bjorner 9bc5552ca2 add vcrunime pattern to distribution directive #4542 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-25 08:56:13 -07:00
Nikolaj Bjorner 274323b818 fix reset order for #4533 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-19 16:07:45 -07:00
Nuno Lopes 07e5b228a2 try to fix nightly build by moving to python3. python2 isn't supported anymore by setuptools 2020-05-31 11:40:13 +01:00
Ivan Gotovchits 24a9ca3226
fixes numerous issues in OCaml bindings building process (#4468) 
It now works both in dynamic and static mode and the compiled
libraries can be used by all linkers in the OCaml system, without
any specificy instructions other than specifying the dependency on
the z3 library.

Using the libraries
===================

Compiling binaries
------------------

The libraries can be linked statically with both ocamlc and ocamlopt
compilers, e.g.,

```
ocamlfind ocamlc -thread -package z3 -linkpkg run.ml -o run
```
or
```
ocamlfind ocamlopt -thread -package z3 -linkpkg run.ml -o run
```

When bindings compiled with the `--staticlib` the produced binary will
not have any dependencies on z3
```
$ ldd ./run
        linux-vdso.so.1 (0x00007fff9c9ed000)
        libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fb56f09c000)
        libgmp.so.10 => /usr/lib/x86_64-linux-gnu/libgmp.so.10 (0x00007fb56ee1b000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fb56ebfc000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb56e85e000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fb56e65a000)
        libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fb56e442000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb56e051000)
        /lib64/ld-linux-x86-64.so.2 (0x00007fb570de9000)
```

The bytecode version will have a depedency on z3 and other external
libraries (packed as dlls and usually installed in opam switch):
```
$ ocamlobjinfo run | grep 'Used DLL' -A5
Used DLLs:
        dllz3ml
        dllzarith
        dllthreads
        dllunix
```

But it is possible to compile a portable self-contained version of the
bytecode executable using the `-custom` switch:

```
ocamlfind ocamlc -custom -thread -package z3 -linkpkg run.ml -o run
```

The build binary is now quite large but doesn't have any external
dependencies (modulo the system dependencies):
```
$ du -h run
27M     run
$ ocamlobjinfo run | grep 'Used DLL' | wc -l
0
$ ldd run
        linux-vdso.so.1 (0x00007ffee42c2000)
        libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fdbdc415000)
        libgmp.so.10 => /usr/lib/x86_64-linux-gnu/libgmp.so.10 (0x00007fdbdc194000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fdbdbf75000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fdbdbbd7000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fdbdb9d3000)
        libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fdbdb7bb000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fdbdb3ca000)
        /lib64/ld-linux-x86-64.so.2 (0x00007fdbde026000)
```

Loading in toplevel
-------------------

It is also possible to use the built libraries in toplevel and use
them in ocaml scripts, e.g.,
```
$ ocaml
        OCaml version 4.09.0

 # #use "topfind";;
 - : unit = ()
 Findlib has been successfully loaded. Additional directives:
  #require "package";;      to load a package
  #list;;                   to list the available packages
  #camlp4o;;                to load camlp4 (standard syntax)
  #camlp4r;;                to load camlp4 (revised syntax)
  #predicates "p,q,...";;   to set these predicates
  Topfind.reset();;         to force that packages will be reloaded
  #thread;;                 to enable threads

- : unit = ()
 # #require "z3";;
 /home/ivg/.opam/4.09.0/lib/zarith: added to search path
 /home/ivg/.opam/4.09.0/lib/zarith/zarith.cma: loaded
 /home/ivg/.opam/4.09.0/lib/z3: added to search path
 /home/ivg/.opam/4.09.0/lib/z3/z3ml.cma: loaded
 #
```

To use z3 in a script mode add the following preamble to a file with
OCaml code:
```
  #!/usr/bin/env ocaml
  #use "topfind";;
  #require "z3";;

  (* your OCaml code *)
```

Then it is possible to run it as `./script` (provided that the code is
in a file named `script` and permissions are set with `chmod a+x
script`).

Of course, such scripts will depend on ocaml installation that shall
have z3 dependencies installed.

Using Dynlink
-------------

The built z3ml.cmxs file is a self-contained shared library that
doesn't have any depndencies on z3 (the z3 code is included in it) and
could be loaded with `Dynlink.loadfile` in runtime.

Installation
============

I did not touch the installation part in this PR, as I was using opam
and installed artifacts as simple as:
```
ocamlfind install z3 build/api/ml/* build/libz3-static.a
```

assuming that the following configuration and building process
```
python2.7 scripts/mk_make.py --ml --staticlib
make -C build
```

Though the default installation script in the make file shall work.

Dynamic Library mode
====================

The dynamic library mode is also supported provided that libz3.so is
installed in a search path of the dynamic loader (or the location is
added via the LD_LIBRARY_PATH) or stored in rpaths of the built
binary.

Build Artifacts
===============

In the static mode (--staticlib), the following files are built and
installed:

- `{z3,z3enums,z3native}.{cmi,cmo,cmx,o,mli}`: the three compilation
units (modules) that comprise Z3 bindings. The `*.mli` files are not
necessary but are installed for the user convenience and documentation
purposes. The *.cmi files enables access to the unit
definitions. Finally, `*.cmo` contain the bytecode and `*.cmx, *.o`
contain the native code. Files with the code are necessary for cross-module
optimization but are not strictly needed as the code is also
duplicated in the libraries.

- libz3-static.a (OR libz3.so if built not in the staticlib mode)
contains the machine code of the Z3 library;

- z3ml.{a,cma,cmxa,cmxs} - the OCaml code for the bindings. File
z3ml.a and z3ml.cmxa are static libraries with OCaml native code,
which will be included in the final binary when ocamlopt is used. The
z3 library code itself is not included in those three artifacts, but
the instructions where to find it are. The same is truce for `z3ml.a`
which includes the bytecode of the bindings as well as instructions
how to link the final product. Finally, `z3ml.cmxs` is a standalone
shared library that could be loaded in runtime use
`Dynlink.loadfile` (which used dlopen on posix machines underneath the
hood).

- libz3ml.a is the archived machine code for `z3native_stubs.c`, which
is made by ocamlmklib: `ar rcs api/ml/libz3ml.a
api/ml/z3native_stubs.o` it is needed to build statically linked
binaries and libraries that use z3 bindings.

- dllz3ml.so is the shared object that contains `z3native_stubs.o` as
well as correct ldd entries for C++ and Z3 libraries to enable proper
static and dynamic linking. The file is built with ocamlmklib on posix
systems as
```
gcc -shared -o api/ml/dllz3ml.so api/ml/z3native_stubs.o -L. -lz3-static -lstdc++
```

It is used by `ocaml`, `ocamlrun`, and `ocamlc` to link z3 and c++
code into the OCaml runtime and enables usage of z3 bindings in
non-custom runtimes (default runtimes).

The `dllz3ml.so` is usually installed in the stubs library in opam
installation (`$(opam config var lib)/stublibs`), it is done
automatically by `ocamlfind` so no special treatment is needed.

Technical Details
=================

The patch itself is rather small. First of all, we have to use
`-l<lib>` instead of `-cclib -l<lib>` in ocamlmklib since the latter
will pass the options only to the ocaml{c,opt} linker and will not
use the passed libraries when shared and non-shared versions of the
bindings are built (libz3ml.a and dllz3ml.so). They were both missing
either z3 code itself and ldd entries for stdc++ (and z3 if built not
in --staticlib mode).

Having stdc++ entry streamlines the compilation process and makes
dynamic loading more resistant to the inclusion order.

Finally, we had to add `-L.` to make sure that the built artifacts are
correctly found by gcc.

I specifically left the cygwin part of the code intact as I have no
idea what the original author meant by this, neither do I use or
tested this patch in the cygwin or mingw environemt. I think that this
code is rather outdated and shouldn't really work. E.g., in the
--staticlib mode adding z3linkdep (which is libz3-static.a) as an
argument to `ocamlmklib` will yield the following broken archive
```
ar rcs api/ml/libz3ml.a libz3-static.a api/ml/z3native_stubs.o
```
and it is not allowed (or supported) to have .a in archives (though it
doesn't really hurt as most of the systems will just ignore it).

But otherwise, cygwin, mingw shall behave as they did (the only change
that affects them is `-L.` which I believe should be benign).
 2020-05-27 09:21:14 -07:00
Nikolaj Bjorner b3366bae5a remove test-examples from MacOS build, re-add maxsat example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 13:52:44 -07:00
Nikolaj Bjorner 5fe0eeda63 disable regressions in ST mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 09:37:06 -07:00
Nikolaj Bjorner fcd2bc605c try to make template parsing work 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 19:17:36 -07:00
Nikolaj Bjorner 323a752bbf disable maxsat. for a mysterious reason it started failing on a single macos build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 19:16:32 -07:00
Lev Nachmanson d3c00ca2c3 change mode to executable to some py files 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-16 14:12:16 -07:00
Nuno Lopes 0313cf6d4c restore exec bit on configure & scripts/*.sh 2020-05-16 20:07:36 +01:00
Lev Nachmanson 08940cff8f comment out the call to nra_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 11:26:40 -07:00
Nikolaj Bjorner 17b8db95c1 inc version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-08 15:05:01 -07:00
Nikolaj Bjorner ee522e1668 update comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-08 15:03:52 -07:00
Nikolaj Bjorner ad55a1f1c6 Update release.yml for Azure Pipelines 
disable pypi republish for 4.8
 2020-05-08 14:12:38 -07:00
Nikolaj Bjorner 42e6cbce3d publish also ubuntu build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-08 14:10:23 -07:00
Nikolaj Bjorner 9a44ed854b enable pip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-08 12:34:07 -07:00
Nikolaj Bjorner 2804b40edb disable nuget publish for now 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-08 12:32:57 -07:00
Andrew Helwer b42ea38028
Automatically push release pipeline packages to nuget.org (#4249) 2020-05-07 17:31:27 -07:00
Nikolaj Bjorner 611c14844d fix #3194, remove euclidean solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-08 16:05:13 +01:00
Phillip Schanely a20d4fa362 Use the latin-1 codec instead of ascii in Python bindings. 
The latin-1 codec maps byte values 0-255 to unicode codepoints 0-255.
The ascii codec only maps the lower half of that range.
 2020-03-05 21:52:22 -08:00
Nikolaj Bjorner 5a357f9998 fixup build of example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 14:34:44 -08:00
Nikolaj Bjorner 80c98dfb1f avoid const in ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 10:40:10 -08:00
Nikolaj Bjorner a65efb682b avoid const in ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 10:40:10 -08:00
jeff 6330bf7d25 fix z3 library search order 2020-02-26 20:56:51 -08:00
Nikolaj Bjorner 833b54a12c fix dotnet build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 09:44:21 -08:00
Nikolaj Bjorner f0689546f3 return non-escaped string value for Python #3080 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 09:16:23 -08:00
Rose Kunkel aaf2c3bdcc Fix https://github.com/Z3Prover/z3/issues/2998 2020-02-14 18:03:59 -10:00
Lev Nachmanson 8388868c27 fix the make build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 3bc67d1804 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 6cd495979d fix the test build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Andrew Helwer ea3b149575
Script assembly signing & NuGet package creation in Azure Pipelines (#2862) 
Windows x86/x64 builds now parallelized
Windows assemblies now signed
NuGet package created
NuGet package signed
NuGet package published to NuGet.org
 2020-01-16 18:34:01 -08:00
Nikolaj Bjorner ab1f2f2e63 reduce use of symbols in gparams 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:54:26 -08:00
Nikolaj Bjorner f70696d8e7 reduce contention #2842 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 20:10:11 -08:00
Nikolaj Bjorner 40a4326ad4 add anf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-05 16:46:49 -08:00
Andrew Helwer a72f848fde Nightly pipeline now uses SNK file in repo 2020-01-03 13:15:51 -08:00
Andrew Helwer 7dbb69ff32 Now consume SNK file in repo instead as build secret 2020-01-02 17:41:12 -08:00
Nikolaj Bjorner 1d0572354b add bit-matrix, avoid flattening and/or after bit-blasting, split pdd_grobner into solver/simplifier, add xlin, add smtfd option for incremental mode logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-01 20:14:20 -08:00
Nikolaj Bjorner 4a94abe7d7 Update nightly.yaml 
update name
 2019-12-20 23:18:19 -08:00
Nikolaj Bjorner b13e7b9df3 Update nightly.yaml 
again
 2019-12-20 22:29:47 -08:00
Nikolaj Bjorner c8703cbc42 Update nightly.yaml 
try again
 2019-12-20 22:26:14 -08:00
Nikolaj Bjorner 8a75e9090b Update nightly.yaml 
mac -> osx
 2019-12-20 21:16:11 -08:00
Nikolaj Bjorner c5d31be613 Update nightly.yaml 
add Python top zip
 2019-12-20 21:12:13 -08:00
Nikolaj Bjorner 495658e07a try adding macos to nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-20 20:16:28 -08:00
Nikolaj Bjorner 469f618742 build dependencies, invariant annotation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 13:48:27 -08:00
Nikolaj Bjorner 1fdde9e056 move bdd to separate space 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 10:03:01 -08:00
Federico Poli 8ebbc094eb Link librt when compiling with --staticbin on Linux 
Fixes issue #2457. The workaround is described here: https://stackoverflow.com/questions/58848694/gcc-whole-archive-recipe-for-static-linking-to-pthread-stopped-working-in-rec
 2019-11-27 09:16:48 -08:00
Nikolaj Bjorner 07dcb0a98b
Merge pull request #2477 from evmaus/master 
MSAN Integration Build
 2019-11-26 09:31:23 -08:00
Nikolaj Bjorner e45bafe9bf increase version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-19 14:17:48 -08:00
Nikolaj Bjorner 30e7c225cd upgrade pip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-19 12:58:44 -08:00
Nikolaj Bjorner f170e655d5 add importlib_metatada 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-19 10:56:56 -08:00
Nikolaj Bjorner 429fc7c408 rename additional build options #2709 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-18 23:02:44 -08:00
Nikolaj Bjorner 3729458d14 enable pypi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-18 19:20:15 -08:00
Andrew Helwer 37382d22c4 Updated references to Z3 icon 2019-11-18 12:24:39 -08:00
Nikolaj Bjorner dd827cae1c remove IS_GNU 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-08 14:49:35 -08:00
Federico Poli 7eb6731ac2 Link pthread with --whole-archive option on Linux 
This fixes a SIGSEGV on Ubuntu 16.04 when running z3 compiled with `--staticbin` (issue #2457). It seems that without the --whole-archive option the linker does not statically link all pthread symbols.

The fix is described here: https://stackoverflow.com/a/45271521/2491528
 2019-11-06 11:18:32 +01:00
Samuel Thibault da061bbcc3 Add hurd support 
Signed-off-by: Samuel Thibault <samuel.thibault@ens-lyon.org>
 2019-11-03 01:22:44 -08:00
Nikolaj Bjorner 16d4ccd396 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-31 10:06:09 -07:00
philzook58 ed03c1d9e6 Removed incorrect include directories flag in ocaml META file 2019-10-25 18:05:13 -07:00
Nikolaj Bjorner a8049c7feb update nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-24 16:34:41 -07:00
Michał Janiszewski 9ae1a6f061 Add MSVC ARM64 job to Azure Pipelines 2019-10-24 15:19:53 -07:00
Nikolaj Bjorner 9847675095 fix #2647 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-22 08:26:40 -07:00
Nikolaj Bjorner 0acbdffacf update mk_nuget_task 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 15:34:05 -07:00
Nikolaj Bjorner bfc30440ac update nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 13:57:45 -07:00
Nikolaj Bjorner 9fae4a16e6 update nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 12:35:12 -07:00
Nikolaj Bjorner 4051fbd8b2 update nuget packaging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 11:19:28 -07:00
Nikolaj Bjorner f086f01ae0 update nuget script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 10:09:37 -07:00
Nikolaj Bjorner 928e08f28f update nightly runner 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 09:31:28 -07:00
Nikolaj Bjorner af442cf281 update nightly runner 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 09:29:43 -07:00
Nikolaj Bjorner 0756581a99 add nuget stage to nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 08:22:18 -07:00
Nikolaj Bjorner 5c78f855ad re-add deletion for nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 07:49:57 -07:00
Nikolaj Bjorner aef0c19d36 add pdb to distribution components 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 07:48:45 -07:00