3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Commit graph

651 commits

Author SHA1 Message Date
Dan Liew 8840e5a00f Move `mk_pat_db_internal() from mk_util.py` to
``mk_genfile_common.py`` and adapt ``mk_util.py`` and
``mk_pat_db.py`` to use the code at its new location.

Whilst I'm here reindent ``mk_mem_initializer_cpp.py``.

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-09 11:22:48 +00:00
Dan Liew 114e165fad Move `mk_mem_initializer_cpp_internal() from mk_util.py` to
``mk_genfile_common.py`` and adapt ``mk_util.py`` and
``mk_mem_initializer_cpp.py`` to use the code at its new location. The interface
has been changed slightly so that ``mk_mem_initializer_cpp_internal()`` now
returns the path the generated file. The motivation behind this is so that
clients of the function know the path of the generated file.

Whilst I'm here reindent ``mk_mem_initializer_cpp.py`` and the relevant
code in ``mk_util.py``.

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-09 11:22:48 +00:00
Dan Liew f4e98a4fe5 Move `mk_install_tactic_cpp_internal() from mk_util.py` to
``mk_genfile_common.py`` and adapt ``mk_util.py`` and
``mk_install_tactic_cpp.py`` to use the code at its new location. The interface
has been changed slightly so that ``mk_install_tactic_cpp_internal()`` now
returns the path the generated file. The motivation behind this is so that
clients of the function know the path of the generated file.

Whilst I'm here reindent ``mk_install_tactic_cpp.py`` and the relevant
code in ``mk_util.py``.

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-09 11:22:48 +00:00
Dan Liew 404aa2a5a0 Move `mk_gparams_register_modules_internal() from mk_util.py`
to ``mk_genfile_common.py`` and adapt ``mk_util.py`` and
``mk_gparams_register_modules_cpp.py`` to use the code at its new
location. The interface has been changed slightly so that
``mk_gparams_register_modules_internal()`` now returns the path
to the generated file. The motivation behind this so that clients
of the function know the path to the generated file.

Whilst I'm here reindent ``mk_gparams_register_modules_cpp.py``
and the relevant code in ``mk_util.py``.

Also remove duplicated code that is now available in
``mk_genfile_common.py``.

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-09 11:22:48 +00:00
Dan Liew 8a35f744c7 Move `mk_def_file_internal() out of mk_util.py` into
``mk_genfile_common.py`` and adapt ``mk_util.py`` and
``mk_def_file.py`` to use the code at its new location.

Whilst I'm here also reindent ``mk_def_file.py`` and make it
use some of the code in ``mk_genfile_common.py`` to avoid code
duplication.

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-09 11:22:48 +00:00
Dan Liew 2b64729b21 Move `mk_z3consts_py_internal() out of mk_util.py` into
``mk_genfile_common.py`` and adapt ``mk_util.py`` and
``mk_consts_files.py`` to use the code at its new location. The
interface has been changed slightly so that
``mk_z3consts_py_internal()`` now returns the path to the generated
file. The motivation behind this is so that clients of the function
know the path to the generated file.

Whilst I'm here also reindent ``mk_consts_files.py`` and move some of
its code into ``mk_genfile_common.py`` so it can be shared.

Also update Z3_GENERATED_FILE_EXTRA_DEPENDENCIES in the CMake build
so it knows about ``mk_genfile_common.py``.

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-09 11:22:48 +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 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 cf5910e041 typos 2016-03-04 15:08:03 +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
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
Dan Liew e9ea687bb9 Disable the Python bindings by default which partially fixes issue #404.
To enable the Python bindings use the newly added ``--python`` option.
2016-01-08 21:21:54 +00:00
Mikolas Janota 743a59254e Merge remote-tracking branch 'upstream/master' into lackr 2016-01-07 16:39:43 +00:00
Christoph M. Wintersteiger 3e000d7525 build fix for libz3.vcxproj 2016-01-05 14:40:31 +00:00
Christoph M. Wintersteiger 8b47a84598 Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 11:34:35 +00:00
Christoph M. Wintersteiger 4915f2da04 Added facilities for generating a libz3.vcxproj next to z3.vcxproj for simplified DLL build in VS. 2016-01-04 21:53:24 +00:00
Christoph M. Wintersteiger 25af97fb8b tabs 2016-01-04 21:04:07 +00:00