3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 19:01:50 +00:00
Commit graph

719 commits

Author SHA1 Message Date
Christoph M. Wintersteiger d57a2a6dce Bumped version to 4.5.0 2016-11-07 22:02:30 +00:00
Christoph M. Wintersteiger 7f923c6a33 Include Python API files in distributions. 2016-11-07 22:00:28 +00:00
Christoph M. Wintersteiger 7bbdb7714f Added signed .NET assemblies in unix builds 2016-11-03 17:20:39 +00:00
Christoph M. Wintersteiger 6e0369036e fixed log output typo 2016-11-03 17:13:02 +00:00
Christoph M. Wintersteiger 6fb358a432 Build fix for libz3.vcxproj. 2016-10-28 13:45:10 +01:00
Christoph M. Wintersteiger 86285e1641 disabled unnecessary assertion 2016-10-26 12:59:26 +01:00
Christoph M. Wintersteiger 6ea45b4d65 fix for Python API installation 2016-10-25 14:23:55 +01:00
Christoph M. Wintersteiger 009af4455d Refactored and fixed model conversion for fpa2bv conversion of unspecified values via theory_fpa. 2016-10-15 18:35:39 +02: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
Nikolaj Bjorner 092c52e5b7 fix for package directory. issue #744
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-09-22 18:29:26 -07:00
Andrew Dutcher 4801a27c2d Fix up z3test to a) exist and b) work 2016-09-21 17:18:10 -07:00
Nikolaj Bjorner ef0dd74c53 try copy instead of cp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-09-21 16:14:27 -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 02783d0bfb Minor tweaks to make things more reliable/less obnoxious 2016-09-14 01:49:37 -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
Christoph M. Wintersteiger 7fd931d480 build fix 2016-07-29 00:55:05 +01:00
Christoph M. Wintersteiger d5954e829b Enabled donet key file in dist scripts 2016-07-28 18:49:57 +01:00
Christoph M. Wintersteiger 7fefe40f21 Added/improved facilities for strong name signing of the .NET assembly. 2016-07-28 18:07:34 +01:00
Christoph M. Wintersteiger 3587baaf24 Added full version strings and associated API functions. 2016-07-28 18:06:02 +01:00
Nikolaj Bjorner 9cab896632 adding sign option if keyfile is present
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-26 14:31:29 -07:00
Philipp Wendler c3b8c15f35 Java API: Make enum lookup more efficient.
The existing code causes an allocation of an array with all enum values
on every method call (inside the values() method),
and loops over all enum entries.
2016-07-22 17:32:57 +02:00
Philipp Wendler f325b51213 Java API: In fromInt() methods of enums fail on invalid value.
The existing code just returns one of the enum values if an unknown int
value is passed, silently hiding bugs.
2016-07-22 17:32:57 +02:00
Nikolaj Bjorner b303fd59c0 add some version information (and date) to log file to make it easier to trap version mismatch on log files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-28 18:11:30 -07:00
Christoph M. Wintersteiger 1fb672121c build fix for cygwin/mingw 2016-06-24 13:57:53 +01:00
Christoph M. Wintersteiger e3a41d0d98 Merge pull request #645 from martin-neuhaeusser/cross-mingw64
Extend build scripts to support MinGW64 cross-compilation on Windows.
2016-06-24 13:42:10 +01:00
Christoph M. Wintersteiger d90a575981 Merge pull request #646 from martin-neuhaeusser/ocaml-c89
Make C-layer of OCaml bindings C89 compatible.
2016-06-24 13:40:50 +01:00
Christoph M. Wintersteiger fad1dffbf0 Added PATH info to successful build message 2016-06-22 19:03:42 +01: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. Neuhäußer 22097efd4a Extend build scripts to support MinGW64 cross-compilation on Windows. 2016-06-10 16:43:57 +02:00
Teodor Vlasov 886759a58c add DOTNET_ENABLED in parser_options of mk_*_dist 2016-05-15 22:36:12 +03:00
Christoph M. Wintersteiger 86126e2c01 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-05-03 11:52:21 +01: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
Dan Liew 3042f0f964 Fix inconsistent emission of Java enumeration files. The ordering of emitted
enum values is not consistent between python 2 or 3. The root cause
of the problem was a dictionary's keys being iterated over which has
no defined order.

This has been fixed by iterating over the dictionary's items and
ordering by values.  We could order by key rather than the values but
seeing as these represent an enum, ordering by value makes more sense.
2016-04-17 19:03:17 +01:00
Dan Liew b3713e7496 Refactor `mk_z3consts_java() code into mk_z3consts_java_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-04-17 19:03:17 +01: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
Christoph M. Wintersteiger b178420797 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-31 18:11:30 +01: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 2eced4676f Merge pull request #539 from delcypher/cmake_dotnet_bindings
[CMake] Teach CMake to build .NET bindings
2016-03-29 13:56:35 +01:00
martin-neuhaeusser 28f9c61d76 Include *.cmx files during installation of OCaml bindings.
The *.cmx files are now installed using ocamlfind. They contain information from the
compiler that can be used during optimization (the upcoming OCaml 4.03.0 issues
warning 58 if those files are missing from a package).
2016-03-28 17:08:22 +02:00
Dan Liew 23ac66ef42 Fix inconsistent emission of `Enumerations.cs`. The ordering of emitted
enum values is not consistent between python 2 or 3. The root cause
of the problem was a dictionary's keys being iterated over which has
no defined order.

This has been fixed by iterating over the dictionary's items and
ordering by values.  We could order by key rather than the values but
seeing as these represent an enum, ordering by value makes more sense.
2016-03-26 17:59:11 +00:00
Dan Liew d3f87e44a2 Refactor `mk_z3consts_dotnet() code into mk_z3consts_dotnet_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-03-26 17:59:11 +00:00
Bobby Powers 7bb085a565 build: allow overriding of 'ar' in mk_config
This will still use 'ar' if AR isn't set in the environment, but lets
us override the default archive tool at configure time.

Just like CC and CXX, this doesn't apply to a ./configure for Windows.
2016-03-22 10:47:51 -04:00