Christoph M. Wintersteiger
649d474686
Build fix for C++ example
2016-12-09 19:09:47 +00:00
Nuno Lopes
1d417f6527
fix warnings in configure script
2016-11-23 09:32:20 +00:00
Christoph M. Wintersteiger
dee7c29b19
Added optional synchronization for multi-thread API logs. Relates to #798 .
2016-11-22 11:32:25 +00:00
Christoph M. Wintersteiger
014815a640
Fixed Windows distribution script.
2016-11-15 08:59:18 -08:00
Christoph M. Wintersteiger
889e5e9388
Bumped version number.
2016-11-07 23:19:59 +00:00
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
