mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity
15993 commits 23 branches 48 tags 157 MiB
Commit graph

602 commits

Author SHA1 Message Date
Louis Gesbert 8d5466e781 OCaml / static: fix linking options 2019-05-21 16:09:18 +02:00
Kate 7d43a4bca5 Fix Makefile generation for the OCaml api 2019-04-10 15:18:03 +01:00
Nikolaj Bjorner 869cb66736 step 1 in aligning version tweaks for #2184 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-16 11:52:55 -07:00
Nikolaj Bjorner 038f992ff4 remove platformtarget for dotnetcore spec 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-14 12:48:27 -07:00
Nuno Lopes deb2deb4ad fix linking of .so on old build system 2019-03-07 10:04:06 +00:00
Nuno Lopes c0f7afacc4 bump cmake minimum version to 3.4 as it was released 3+ years ago 
some misc compiler flags cleanup
 2019-03-07 09:58:36 +00:00
Nuno Lopes 7ad4ced12f librt no longer needed(?) 2019-03-06 12:16:48 +00:00
Nikolaj Bjorner 9dd41ba554 remove offending assert, disable assembly-info for dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:13:03 -08:00
Carsten Varming e1a9154555 Specify UTF-8 encoding in python build scripts 2019-01-05 13:48:15 -05:00
Nikolaj Bjorner c5ada288c2 updated script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-12 12:46:28 -08:00
Nikolaj Bjorner 8d23ad2f7e fix generation of assembly-sign-input to take escape sequences and absolute paths 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-12 10:14:38 -08:00
Nikolaj Bjorner db3e5ce070
Merge pull request #1997 from waywardmonkeys/change-64-bit-configuration-strategy 
Change how 64 bit builds are detected.
 2018-12-12 09:55:13 -08:00
Nikolaj Bjorner 02f01fcef1 adding esrp feature 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 17:31:09 -08:00
Nikolaj Bjorner 93c59ffbd9 update script to sign assembly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 15:48:33 -08:00
Bruce Mitchener 51a947b73d Change how 64 bit builds are detected. 
Instead of doing this at configure time, we look at the actual
compile time status. This also avoids hardcoding checks based on
what CPU architecture is present, which doesn't work when Z3 is
being built on non-x86_64 platforms.
 2018-12-09 16:16:20 +07:00
Nikolaj Bjorner ee7781e602 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-17 15:05:02 -08:00
Nikolaj Bjorner 9ec59fdb93 fix #1934 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-17 15:04:25 -08:00
Nikolaj Bjorner 5ebe342da1 add support for keyfiles 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-16 13:27:58 -08:00
Nikolaj Bjorner f4ced3c164 use netstandard1.4 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-15 16:40:35 -08:00
Nikolaj Bjorner 60d7444c96 build generated files outside of src 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-15 16:16:38 -08:00
Nikolaj Bjorner bb5837791a clean up dotnet core component 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-15 11:02:49 -08:00
Nikolaj Bjorner 8bfeca063d update example build for dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-15 10:36:27 -08:00
Nikolaj Bjorner 6a9c8a8999 remove spurious string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-14 19:40:56 -08:00
Nikolaj Bjorner 4f4463b2b7 update for nuget/core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-14 15:06:24 -08:00
Nikolaj Bjorner 13d1ccfeaf update for nuget/core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-14 14:59:53 -08:00
Nikolaj Bjorner c372500018 update for nuget/core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-14 14:51:58 -08:00
Nikolaj Bjorner 84baddf87c Merge branch 'master' of https://github.com/z3prover/z3 2018-11-14 14:07:16 -08:00
Nikolaj Bjorner 1cc2cc0143 add TBD marker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-14 14:07:14 -08:00
Nikolaj Bjorner 74db2f2509
Merge pull request #1939 from msoeken/dotnetcore-fix 
Choose runtime for .NET core DLL.
 2018-11-14 14:06:43 -08:00
Mathias Soeken 690bd8502a Choose runtime for .NET core DLL. 2018-11-14 13:47:46 -08:00
Nikolaj Bjorner 2501a875ef update script to generate file directly instead of from makefile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-14 13:44:40 -08:00
Nikolaj Bjorner c49d71ba66 Merge branch 'master' of https://github.com/z3prover/z3 2018-11-14 11:43:44 -08:00
Nikolaj Bjorner 139d8b85f0 core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-14 11:43:41 -08:00
Mathias Soeken 33363aeb58 Fix problem in mk_echo. 2018-11-14 11:27:55 -08:00
Mathias Soeken e39907c481 Fix some problems in mk_echo. 2018-11-14 11:25:18 -08:00
Mathias Soeken d4567a1255 Fix echo command for Windows. 2018-11-14 11:11:25 -08:00
Mathias Soeken 2fbaad15d7 Build example for dotnetcore. 2018-11-14 09:57:47 -08:00
Nikolaj Bjorner ccf6ca310e more dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-13 19:59:46 -08:00
Nikolaj Bjorner 37ec933c66 more dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-13 19:58:42 -08:00
Nikolaj Bjorner dbd5ef4526 more dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-13 19:58:09 -08:00
Nikolaj Bjorner bd78558826 adding dotnetcore handling 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-13 19:51:57 -08:00
Nikolaj Bjorner 225fb82d96 add TBD for dotnet example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-13 15:54:37 -08:00
Nikolaj Bjorner b02c698284 align variable names with dimacs input 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-08 16:52:10 -08:00
Nikolaj Bjorner 52801db3fd more dotnet core prepration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-22 16:28:01 -07:00
Nikolaj Bjorner 540922766d more dotnetcore preparation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-22 12:15:54 -07:00
Nikolaj Bjorner 4616ddf103 more prep for dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-22 11:50:07 -07:00
Nikolaj Bjorner 7c043dee7d more prep for dotnetcore 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-22 11:07:17 -07:00
Nikolaj Bjorner 8a93f34b4a Merge branch 'master' of https://github.com/z3prover/z3 2018-10-22 11:00:07 -07:00
Nikolaj Bjorner 81a92edb61 prepare to retool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-22 10:59:51 -07:00
Florian Pigorsch 326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
nabice 13183b7c7c Ignore current dir when searching for jni 2018-10-10 17:12:16 +08:00
Andrew Helwer 7941074fd1 Added packaging directions, removed linkresource flag 2018-10-06 18:22:55 -07:00
Nikolaj Bjorner 0c4754d94b rename version.h to z3_version.h to differentiate name in install include directory. Add support for z3_version.h in python build system. #1833 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-21 20:13:58 -07:00
Nikolaj Bjorner c247abfc65 prepare js output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-03 22:13:25 -07:00
Nikolaj Bjorner 753b9dd734 fix #1650 fix #1648 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-25 08:56:13 -07:00
Philipp Wendler 3e0506a71b Set the SONAME field of libz3.so to libz3.so. 
This fixes a problem when loading libz3java from Java,
where the dependency on libz3 is not detected as fulfilled
if the latter does not have SONAME set.
 2018-05-25 15:01:07 +02:00
Nikolaj Bjorner 50c93d1ad4 merge with 4.7.1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-22 17:10:36 -07:00
Sapan Bhatia c198b12743 Big_int is no longer a part of OCaml's standard library and must be 
included via the num package: https://github.com/ocaml/num
 2018-05-15 04:55:57 +05:30
Nikolaj Bjorner 888699548d
Revert "Specify encoding of source files in mk_util.py" 2018-05-03 11:59:49 -07:00
Carsten Varming c279fd9f2e Specify encoding of source files in mk_util.py 2018-05-02 23:27:33 -04:00
Nikolaj Bjorner c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Pierre Pronchery 5f7bd993de Add support for NetBSD 
Originally from David Holland <dholland@NetBSD.org>.
 2018-03-13 21:59:35 +01:00
Nikolaj Bjorner 0ce2001449 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-10 11:39:22 -08:00
Christoph M. Wintersteiger 0ef33a98c4
Revert "Fix encoding error" 2018-02-13 14:08:55 +00:00
Virgile ROBLES fddc4e311f
Fix encoding error 
The encode/decode is not needed and fails if any non-ASCII character is returned by g++ or clang++
 2018-01-26 00:30:59 +01:00
Ivan Gotovchits 49678065bd fixes compilation flags for OCaml plugins 
The `-linkall` option is needed for a plugin to be standalone,
otherwise it will miss those dependencies that are not used.
 2017-12-13 14:45:06 -05:00
Christoph M. Wintersteiger 7c63a5cc1d Fixed MSYS/MinGW build. Fixes #1335. 2017-11-11 16:38:53 +00:00
Christoph M. Wintersteiger 45975bec65 Improved support for MSYS/MINGW. Fixes #969. 2017-11-11 15:11:54 +00:00
Christoph M. Wintersteiger 19f43713c9 Fixed Windows build of C example. 2017-11-08 21:16:03 +00:00
Christoph M. Wintersteiger bec6c3f9e2 Fixed C example build. 2017-11-08 18:22:17 +00:00
Christoph M. Wintersteiger a8b52419f5 Fixed C example build. 2017-11-08 18:14:42 +00:00
Nikolaj Bjorner fd49a0c89c added facility to persist model transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 00:05:52 -05:00
Paul Ehrlich 2a459c5ff6 MSYS offers a MINGW shell as well. (uses different os.uname()) 2017-11-01 12:02:48 +01:00
Christoph M. Wintersteiger e50470f2c4 Added support for MSYS2 2017-10-30 18:24:38 +00:00
Nikolaj Bjorner c1b243a8e3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 19:24:30 +01:00
Nikolaj Bjorner a625301a41 expose incremental cubing over API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-28 15:05:10 -07:00
Christoph M. Wintersteiger 9a464dded4 Removed -std=c++11 from OCaml stubs build command. Fixes #1263. 2017-09-27 14:22:59 +01:00
Nikolaj Bjorner e1d08e9526 remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 20:41:29 -07:00
Nuno Lopes 4b00bc636b revert the patch to remove no-strict-aliasing 
VS 2012 doesnt support C++11 unions..
 2017-08-14 23:00:59 +01:00
Nuno Lopes 2473c69679 Drop no-strict-aliasing and fix 2 places where it was violated 2017-08-14 20:09:49 +01:00
Christoph M. Wintersteiger 6bc5209e26 Fixed build problems with .vcxproj 2017-08-01 15:53:55 +01:00
Daniel Perelman d57494395c Add --guardcf flag to mk_make.py to optionally enable Control Flow Guard. 2017-07-06 16:59:20 -07:00
Dan Liew d00892c9a6 [CMake] Fix dependencies for generating mem_initializer.cpp. 
Previously CMake was not aware of which headers files the generation
of `mem_initializer.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declare memory initializers/finalizers change.
* New headers are added that declare memory initializers/finalizer.

Now the `z3_add_component()` CMake function has been modifed so that
it now takes an optional `MEMORY_INIT_FINALIZER_HEADERS` argument
which allows the headers that declare memory initializers/finalizers
to be explicitly listed.

With this information CMake will now regenerate `mem_initializer.cpp`
correctly.

This required the `mk_mem_initializer_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
 2017-06-21 23:56:53 +01:00
Dan Liew 6f48a145aa [CMake] Fix dependencies for generating gparams_register_modules.cpp. 
Previously CMake was not aware of which headers files the generation
of `gparams_register_modules.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared module description/parameters change.
* New headers are added that declare module description/parameters.
* `.pyg` files that generate header files that declare module
  description/parameters change

Now the `z3_add_component()` CMake function has been modifed so that

* All header files that are generated from `.pyg` files are added as
dependencies and are scanned from module description/parameter
declarations. This implicit dependency of `gparams_register_modules.cpp`
depending on other generated header files seems unnecessary complex. We
should revisit this design decision once the Python/Makefile build
system is deprecated.

* The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS`
argument which allows the headers that declare module
description/paramters to be explicitly listed.

With this information CMake will now regenerate `gparams_register_modules.cpp`
correctly.

This required the `mk_gparams_register_modules_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
 2017-06-21 23:56:46 +01:00
Dan Liew 229fd3dc3e [CMake] Fix dependencies for generating install_tactic.cpp. 
Previously CMake was not aware of which headers files the generation
of `install_tactic.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared tactics/probes changed.
* New tactics/probes were added to new header files.

Now the `z3_add_component()` CMake function has been modifed to take an
optional `TACTIC_HEADERS` argument which allows the headers that declare
tactics/probes to be explicitly listed. The necessary component
declarations have been modified to declare their tactic/probe header
files.

With this information CMake will now regenerate `install_tactic.cpp`
correctly.

This required the `mk_install_tactic_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
 2017-06-21 23:03:48 +01:00
Nikolaj Bjorner 691788f449 remove stale references to foci 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-19 20:21:08 -07:00
Christoph M. Wintersteiger a258236229 Disabled debug output 2017-05-19 18:51:52 +01:00
Christoph M. Wintersteiger 46791047fa Fixed VS 2017 platform toolset version in .vcxproj 2017-05-12 14:28:55 +01:00
Nikolaj Bjorner a64a73255e make source directory relative to build directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 15:46:24 -07:00
Nikolaj Bjorner 7731163d11 use forward slash on src include 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 14:42:43 -07:00
Nikolaj Bjorner 911b24784a merge LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 10:46:11 -07:00
Christoph M. Wintersteiger 79dcf03a42 Enabled C++11 in GCC and Clang 2017-05-05 15:01:10 +01:00
Christoph M. Wintersteiger 0ebce66c57 Fixed bug with .NET keyfile path containing spaces. Fixes #1003. 2017-05-05 14:22:40 +01:00
Christoph M. Wintersteiger 3bbe5eceeb fix for --get-describe 2017-03-24 15:53:46 +00:00
Michael Lowell Roberts 3415672f31 fixed bug where mk_make.py --build=... would fail to handle absolute paths correctly. 2017-02-28 08:24:35 -08:00
Christoph M. Wintersteiger 59db0bc9c4 Merge pull request #829 from legendtang/fix_utf8_conf 
Fixed utf-8 version string handling for python2. Resolved #787
 2017-02-04 20:38:51 +00:00
Christoph M. Wintersteiger b9bfd4ddf5 Merge pull request #854 from angr/fix/fpic-arm 
Add -fpic to armv7/armv8 build
 2017-01-18 21:55:52 +00:00
Andrew Dutcher 1eec0799ca Add -fpic to armv7/armv8 build 2016-12-22 14:26:41 -08:00
Dan Liew 2e74a2c54e Refactor update_api.mk_ml() so that the source and output directories 
can be different. This feature will be needed by the CMake build system
to build the OCaml bindings.
 2016-12-19 21:05:17 +00:00
Dan Liew 76bbecf4fe Refactor mk_z3consts_ml() code into mk_z3consts_ml_internal() 
and move that into `mk_genfile_common.py`. Then adapt `mk_util.py` and
`mk_consts_files.py` to call into the code at its new location.

The purpose of this change is to have Python code common to the Python
and CMake build systems separate from Python code that is only used for
the Python build system.
 2016-12-19 21:05:17 +00:00