3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 06:15:37 +00:00
Commit graph

657 commits

Author SHA1 Message Date
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
Christoph M. Wintersteiger a9ffc258d0 Merge branch 'cmake_build_system4' of https://github.com/delcypher/z3-1 into delcypher-cmake_build_system4 2016-03-07 13:12:04 +00:00
Christoph M. Wintersteiger eccf03aaac build fix for non-windows platforms 2016-03-07 11:21:06 +00:00
Christoph M. Wintersteiger 03a8ef2795 Fixed non-Windows preprocessor options.
Fixes #463
2016-03-05 17:14:19 +00:00
Christoph M. Wintersteiger 09832ca807 Fixed static Windows binary build. 2016-03-05 13:58:28 +00:00
Christoph M. Wintersteiger 40c5152075 Added --staticbin option.
Relates to #456
2016-03-04 18:32:45 +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 d54d6b50f0 Teach the Python build system to use the `version.h.in` template file used
by the CMake build and use the existing ``configre_file()`` function
to generate the ``version.h`` file needed by the build.
2016-03-04 15:26:09 +00:00
Dan Liew 8bc7d319c7 Refactor `mk_z3consts_py()` to that is usable externally via a new
function ``mk_z3consts_py_internal()`` which called by a new
``mk_consts_files.py`` script. This will script will allow the const
declarations for the different Z3 language bindings to be generated.
Right now only support for python is implemented but more can be added
in the future.
2016-03-04 15:26:09 +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 46ac368f86 Refactor `mk_def_file()` so that it is usable externally via a new
function ``mk_def_file_internal()`` which is called by a
new ``mk_def_file.py`` script. This will allow other build systems to
generate the ``api_dll.def`` file.
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
Dan Liew 2b3fe3d02c Refactor `mk_gparams_register_modules()` so that it is usable externally via a new
function ``mk_gparams_register_modules_internal()`` which is called by a
new ``mk_gparams_register_modules_cpp.py`` script. This will allow other build systems to
generate the ``gparams_register_modules.cpp`` files.
2016-03-04 15:22:00 +00:00
Dan Liew 2f7f022605 Refactor `mk_mem_initializer_cpp()` so that it is usable externally via a new
function ``mk_mem_initializer_cpp_internal()`` which is called by a
new ``mk_mem_initializer_cpp.py`` script. This will allow other build systems to
generate the ``mem_initializer.cpp`` files.
2016-03-04 15:22:00 +00:00
Dan Liew a13438818f Refactor `mk_install_tactic_cpp()` so that it is usable externally via a new
function ``mk_install_tactic_cpp_internal()`` which is called by a
new ``mk_install_tactic_cpp.py`` script. This will allow other build systems to
generate the ``install_tactic.cpp`` files.
2016-03-04 15:22:00 +00:00
Dan Liew ef58179462 Refactor `mk_pat_db()` so that it is usable externally via a new function
``mk_pat_db_internal()`` which is called by a new ``mk_pat_db.py`` script. This
will allow other build systems to generate the ``database.h`` file.
2016-03-04 15:22:00 +00:00
Dan Liew 9558dc14fb Refactor `exec_pyg_scripts()` so that it is usable externally
via a new ``pyg2hpp.py`` script. This will allow other build systems to
take ``pyg`` files and generate the corresponding ``hpp`` files.
2016-03-04 15:22:00 +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 b27977ea90 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-02 15:14:12 +00:00
Christoph M. Wintersteiger 4fe4db6657 build fix for static libray on Windows 2016-03-01 17:34:45 +00:00
Nikolaj Bjorner 4cf72e23e6 fix python 3 compat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-02-27 09:58:45 -08:00
Nikolaj Bjorner ce8862d415 fix bug in conflict clause generation in seq-branch-variable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-02-26 18:15:45 -08:00
Christoph M. Wintersteiger 0930cfc53f ML API build fixes for cygwin 2016-02-15 15:44:46 +00:00
Christoph M. Wintersteiger 62cae4186b ML API bug fixes 2016-02-15 12:54:05 +00:00
Christoph M. Wintersteiger 18c0a3bfaf removed comments 2016-02-14 19:57:21 +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 e484fc365d add outline of bv bounds tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-02-12 22:57:47 +00:00
Christoph M. Wintersteiger c01f0323c3 Merge branch 'lackr' of https://github.com/MikolasJanota/z3 into MikolasJanota-lackr 2016-02-10 14:26:04 +00:00
Christoph M. Wintersteiger a16f524eae Install target fix for ocamlfind_install on Windows.
Relates to #409
2016-02-09 19:58:52 +00:00
Mikolas Janota b614e7732b Merge remote-tracking branch 'upstream/master' into lackr 2016-02-08 12:54:22 +00:00
Dan Liew 508d2e32c8 Fix a bug in Python build scripts where an extra ending slash in the
build directory would cause REV_BUILD_DIR to be set incorrectly and
would lead to a broken Makefile being generated.

What would happen before:

```
$ python scripts/mk_make.py --build FOO_1
...
REV_BUILD_DIR='..'
```

```
$ python scripts/mk_make.py --build FOO_1/
...
REV_BUILD_DIR='../..'
```
^^^^^ that's wrong. It should be REV_BUILD_DIR='..'

To fix this the ``reverse_path()`` function has been taught to ignore empty
components in ``p.split(os.sep)``.
2016-02-05 14:51:15 +00:00
Dan Liew 33f676ef6b Do not hardcode default build directory name. 2016-02-05 14:39:27 +00:00
Dan Liew 6112ea2ec7 Fix typo 2016-02-05 14:38:41 +00:00
mikolas faa620f673 Further refactoring ackermannization. 2016-02-03 17:31:19 +00:00
mikolas 2679b74543 refactoring 2016-02-03 13:53:52 +00:00
Mikolas Janota 2141a075ba Refactoring ackermannization functionality. 2016-01-28 18:24:54 +00:00
Mikolas Janota e7477e2f6a Moving things around. Adding tactic just for ackermannization. 2016-01-26 17:02:51 +00:00
Mikolas Janota 094d357b07 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-13 12:10:36 +00:00
Dan Liew 250c8d028d Fix bug when configuring when building OCaml bindings is enabled
when using Python2.

The output from ``check_output()`` has ``unicode`` type under
Python 2 but type ``str`` under Python 3. This type ended up being
used inside the ``MakeRuleCmd`` class which asserts that it receives
paths of type ``str``. To fix the problem under Python 2 the asserts
have been made weaker by also allowing the paths to be of type
``unicode``.
2016-01-12 19:38:43 +00:00
Dan Liew cb106d71cf Teach the OCaml bindings install rule to respect the DESTDIR makefile
variable. Previously it would try to install into the system (e.g.
``/usr/lib/ocaml``) regardless of the value of DESTDIR.

Unfortunately it looks like packagers who use DESTDIR to do staged
installs will need to have their packages patch their user's OCaml
``ld.conf`` file manually at package install time (not ``make install``
time) with the extra path to the Z3 Ocaml package directory. We could
use the ``touch`` command to create an empty ``ld.conf`` before running
``ocamlfind install`` but that adds the wrong path to ``ld.conf``
because it contains DESTDIR.
2016-01-11 21:13:25 +00:00
Dan Liew f038291293 Don't silently fail if ocamlfind cannot be found when building the Ocaml
bindings is enabled. That is really unhelpful behaviour. Instead emit a
warning. I would prefer an error message but apparently being able to
build but not install the OCaml bindings is desirable.

Whilst I'm here also print information about ocamlfind where it should
have been mentioned.
2016-01-11 19:36:02 +00:00
Mikolas Janota b26e4b1516 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-11 18:27:47 +00:00
Dan Liew 49a2ed01c8 Improve error message emitting during configure when the Python
bindings are enabled and the set python package directory does
not live under the install prefix. This is the other part required
to fix issue #404.
2016-01-08 21:21:54 +00:00