3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Commit graph

644 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
0c03a87c82 merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-03 14:08:29 -08:00
Christoph M. Wintersteiger
758c9cd7a0 Build fix for install dependencies 2016-01-01 17:02:31 +00:00
Christoph M. Wintersteiger
d6330e157d Refactored Python API installation build. 2016-01-01 16:42:01 +00:00
Nikolaj Bjorner
f414869456 add symbolic automaton
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-23 19:46:10 -08:00
Nikolaj Bjorner
7a9bd72e2e merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-22 17:48:47 -08:00
Nikolaj Bjorner
ea876715e3 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-22 10:46:50 -08: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