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

515 commits

Author SHA1 Message Date
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