mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 11:43:36 +00:00
Code Activity
7058 commits 23 branches 48 tags 156 MiB
Commit graph

159 commits

Author SHA1 Message Date
Nikolaj Bjorner 2e3a5a2060 attempt at addressing #989 by referencing _lib directly instead of over lib() in function calls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 11:03:18 -07:00
George Karpenkov dbdb0307db Free allocated char arrays in JNI API 
Fixes #886
 2017-03-01 15:22:15 +01:00
martin-neuhaeusser 0e966f21ff Fix off-by-one bug in array indexing in the OCaml bindings 
This patch fixes an off-by-one bug that occurred in the construction of output arrays
in the OCaml bindings.
 2017-01-30 17:28:24 +01:00
Nikolaj Bjorner a0a81fc2d7 add format #879 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-26 08:37:37 -08:00
Daniel Perelman f7ebe16046 Omit '.dll' from library name for DllImport. 2017-01-11 16:56:28 -08:00
Christoph M. Wintersteiger d8d869822f Cleaned up #include<iostream> in api* objects. 2017-01-10 21:04:44 +00: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
Kevin Chung e16577ff61 Making z3 python look in its installation directory for the z3 lib 2016-12-18 17:27:55 -05:00
Christoph M. Wintersteiger 5dec919217 Remove unnecessary "unsafe" qualifier on internal .NET API class. 2016-10-06 16:36:19 +01:00
Andrew Dutcher 7816c53352 allow python to load libz3 using loader's default search 2016-09-28 21:05:55 -07:00
Andrew Dutcher 02217d048b replace all non-portable filepath slashes with os.path.join 2016-09-14 14:19:10 -07:00
Andrew Dutcher cb83c42100 Make python stuff live in a python directory in the build tree 2016-09-14 01:49:16 -07:00
Andrew Dutcher 704105306c FINISH IT 2016-09-14 01:40:01 -07:00
Andrew Dutcher 0bbd172af3 First steps to a sane python build 2016-09-14 01:37:04 -07:00
Andrew Dutcher fa6cc19184 Moved python bindings into package 2016-09-14 01:33:07 -07:00
martin-neuhaeusser f069b1c0e9 Make C-layer of OCaml bindings C89 compatible. 
This patch ensures that the C code generated for the OCaml stubs complies with C89. It is needed to compile Z3 with OCaml support with Visual Studio versions older than VS2013.
 2016-06-10 16:49:06 +02:00
Martin R. Neuhaeusser 436113896d Fix typo in OCaml bindings 2016-04-19 12:51:16 +02:00
Martin R. Neuhaeusser 6889767c9a Fix bug in OCaml API where double values have been wrapped incorrectly. 
This patch fixes a segmentation fault that occurs due to incorrect
wrapping of double values in the OCaml API.
 2016-04-19 10:10:28 +02:00
Martin R. Neuhaeusser 67ac1a003e Avoid conversion between mutable arrays and lists in OCaml API. 
This patch eliminates the conversion between OCaml arrays and lists
from Z3's OCaml API.
 2016-04-18 17:20:27 +02:00
martin-neuhaeusser b873c6b508 Simplify OCaml API 
This patch simplifies the implementation of the OCaml bindings. For example,
the applyX wrapper functions have become unnecessary in the new OCaml API.
It also removes the internal ML2C structure that was used as an intermediate
layer between the C and the OCaml layer.
 2016-04-06 12:10:59 +02:00
martin-neuhaeusser f133f478c8 Translate correctly between OCaml option values and NULL pointers 
This patch refactors the update_api script and the z3.ml implementation
to properly translate between OCaml options and NULL pointers. Some
unifications and simplifications (avoidance of unnecessary value allocation)
in the script that creates the native bindings.
 2016-04-04 17:16:15 +02:00
martin-neuhaeusser b85516c271 Fix reference counting in the C layer of the OCaml bindings 
The Z3 context and its reference counters are stored in a structure which is allocated
by the C layer outside the OCaml heap, whenever a Z3 context is created. The structure
and its Z3 context are disposed, once the last reference counter reaches zero. Reference
counters are decremented by C-level finalizers.

The OCaml representations for a Z3 context wrap only a pointer to the corresponding structure.
 2016-04-03 09:41:06 +02:00
Martin R. Neuhaeusser feae0e8277 Use a custom block for storing a Z3_config in the ML bindings. 2016-03-31 18:31:59 +02:00
Christoph M. Wintersteiger cfda8e9e03 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-08 14:32:30 +00:00
Dan Liew 589227235e Try to improve some of the comments in `scripts/update_api.py` 
based on discussion in #461.
 2016-03-07 18:45:34 +00:00
Christoph M. Wintersteiger 3968423c26 build fix for ML API 2016-03-07 15:35:25 +00:00
Christoph M. Wintersteiger 0ea2ac3f28 API script fix 2016-03-07 14:21:33 +00:00
Christoph M. Wintersteiger 027331aef2 resolved merge conflicts 2016-03-07 14:20:10 +00:00
Dan Liew 1d9a7dcf47 Add missing shebang in `scripts/update_api.py`. The script 
was already marked as executable but it wasn't possible to execute
from a shell due to the missing shebang.
 2016-03-04 15:31:56 +00:00
Dan Liew f6e946443e Made emission of the API module files `api_log_macros.h`, 
``api_log_macros.cpp`` and ``api_commands.cpp`` optional in
``update_api.py``. This is required to implement support for
building and installing Z3's API bindings with CMake.
 2016-03-04 15:26:09 +00:00
Dan Liew db34baa979 Partially refactor the code in `update_api.py` so that it can 
be used as a script for other build systems and is callable via
a new ``generate_files()`` function from ``mk_util.py``. This removes
the horrible ``_execfile()`` hack that was previously in ``mk_util.py``.

Unfortunately lots of bad code is still in ``update_api.py`` but
fixing all of its problems is too much work right now.
 2016-03-04 15:26:09 +00:00
Christoph M. Wintersteiger c9a5676346 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-04 15:15:16 +00:00
Christoph M. Wintersteiger cf5910e041 typos 2016-03-04 15:08:03 +00:00
Christoph M. Wintersteiger 62cae4186b ML API bug fixes 2016-02-15 12:54:05 +00:00
Christoph M. Wintersteiger b99fcb9c8a More new OCaml API 2016-02-14 19:56:22 +00:00
Christoph M. Wintersteiger 824169da0a New OCaml API 2016-02-13 22:09:45 +00:00
Nikolaj Bjorner 9c6271dded add debugging facilities for github issues #384 #367 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 10:43:18 -08:00
Christoph M. Wintersteiger d5f79c1f17 build fix for ML API 2015-12-12 19:30:25 +00:00
Nikolaj Bjorner 2122fdee45 fix build script for update to name of get_error_msg 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-19 08:33:27 -08:00
Nikolaj Bjorner 1d4b996765 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 16:39:51 -08:00
Christoph M. Wintersteiger 706a037bf4 Python 3.x string decoding fix 2015-11-16 15:16:50 +01:00
Nikolaj Bjorner bea68cd194 remove deprecated API functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 17:05:15 -08:00
Christoph M. Wintersteiger 05eb78ccac fix for string decoding in build scripts 2015-11-14 15:42:49 +00:00
Christoph M. Wintersteiger 639dfc4b30 fix for string decoding in build scripts 2015-11-14 15:06:55 +00:00
Christoph M. Wintersteiger 27dcd8c5b6 Fix for python decoding of command line output strings 
Fixes #302
 2015-11-13 17:15:04 +00:00
Christoph M. Wintersteiger b1fcdadd55 Merge branch 'buildsystem_cleanup' of https://github.com/daniel-j-h/z3 into daniel-j-h-buildsystem_cleanup 2015-10-19 15:18:13 +01:00
Christoph M. Wintersteiger d8d0b21e42 Bugfix for dll/so name resolution in Java. 
Fixes #111
 2015-05-29 12:55:17 +01:00
Nikolaj Bjorner 3ba2e712b2 merge with unstable branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-12 15:54:52 -07:00
Daniel J. Hofmann ce9036c300 Minor python-related style fixes 2015-04-09 21:24:15 +02:00
Christoph M. Wintersteiger 03020b9f96 Build system bugfixes. 
Partially fixes #27
 2015-04-08 12:09:14 +01:00