3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Commit graph

5007 commits

Author SHA1 Message Date
Dan Liew 98244ac9a9 [CMake] Remove global "generated file" dependency on `mk_util.py`.
Most file generation scripts don't depend on it anymore.

The exceptions are uses of ``update_api.py``. An explicit dependency
has been added here and a ``FIXME`` has been left to indicate that this
should be removed once ``update_api.py`` is completly independent of
``mk_util.py``.
2016-03-09 11:22:49 +00:00
Dan Liew b3f6a3c4af Remove use of global data structures in
``mk_install_tactic_cpp_internal()``
2016-03-09 11:22:49 +00:00
Dan Liew 87e99cd734 Move the code for generating `*.hpp files from *.pyg from mk_util.py` to
``mk_genfile_common.py``. A new function ``mk_hpp_from_pyg()`` has been added
which provides a more sensible interface (hides the nasty ``exec()`` stuff)
to create the ``*.hpp`` files from ``*.pyg`` files.

Both ``mk_util.py`` and ``pyg2hpp.py`` have been modified to use the new
interface.

Whilst I'm here reindent ``pyg2hpp.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.

I've tested this change by making sure that the all the ``*.hpp``
files generated from ``*.pyg`` files match the files generated
before this change.
2016-03-09 11:22:49 +00:00
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 a2e3788a20 [CMake] Refactor the dependency on `scripts/mk_util.py` into
a list ``Z3_GENERATED_FILE_EXTRA_DEPENDENCIES`` that is used by
the ``add_custom_command()`` declarations. This will let
us easily change the common dependencies for generating build files in
the future.
2016-03-09 11:22:48 +00:00
Nikolaj Bjorner 9743c188da add exception handling for making solver-1 discontinuation transparent, thanks to Martin, #497
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-08 17:00:12 -08:00
Nikolaj Bjorner 335a1dba6e guarding bb_rewriter now that it gets reset
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-08 16:50:06 -08:00
Nuno Lopes d0de8fff62 ensure ast_manager::are_equal returns true if expr ptrs are equal
found by Nikolaj
2016-03-08 16:53:09 +00:00
Nikolaj Bjorner 809fc86ac7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-07 16:42:39 -08:00
Nikolaj Bjorner 5994c5a948 fix partial model tracking over cancellation/exceptions, reported by August Shi. Fix regression test for fp-to-real, reset the pre-processor in inc_sat_solver on exceptions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-07 16:42:29 -08:00
Christoph M. Wintersteiger cef8c67cc0 Merge pull request #490 from delcypher/cmake_generate_files_comments
Try to improve some of the comments in ``scripts/update_api.py``
2016-03-07 18:51:44 +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
Nikolaj Bjorner 49d0e28621 allow parameters to overwrite logic, fixes bug report by Nuno
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-07 10:44:06 -08:00
Nikolaj Bjorner 8c4d791f01 use std::vector per Nuno's analysis to fix #420
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-07 08:08:17 -08:00
Christoph M. Wintersteiger 26f27867bf Merge pull request #487 from delcypher/cmake_missing_fpa2bv_rewriter
Add missing source file declarations to CMake build that were
2016-03-07 15:30:35 +00:00
Dan Liew 114f09cf4c Add missing source file declarations to CMake build that were
added by 70f13ced33
2016-03-07 15:00:22 +00:00
Christoph M. Wintersteiger 3a9b4985e4 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-07 13:35:54 +00:00
Nuno Lopes 9c620376c2 simplify ast::are_equal(), since pointer equality is sufficient 2016-03-07 13:15:12 +00:00
Christoph M. Wintersteiger 3560be86ac Merge branch 'delcypher-cmake_build_system4' 2016-03-07 13:12:16 +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 4423447029 Merge pull request #486 from 4tXJ7f/patch-1
[Z3py] Add examples for fpToFP
2016-03-07 11:31:12 +00:00
Christoph M. Wintersteiger eccf03aaac build fix for non-windows platforms 2016-03-07 11:21:06 +00:00
Andres Nötzli d6ece7e8a5 [Z3py] Add examples for fpToFP 2016-03-07 00:21:26 -08:00
Nikolaj Bjorner 4cd1efc50e address unused variable warnings from OSX build log
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-05 15:33:33 -08:00
Nikolaj Bjorner aa1ddd169a fix bug in offset for shift amount for free bindings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-05 15:25:14 -08:00
Nikolaj Bjorner 5c276d8bf1 Merge pull request #484 from NikolajBjorner/master
Replacing legacy evaluator from proto_model, fix scope-related bugs in rewriter
2016-03-05 10:36:52 -08:00
Nikolaj Bjorner 640308b546 make proto-model evaluation use model_evaluator instead of legacy evaluator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-05 10:27:19 -08:00
Nikolaj Bjorner 70f13ced33 make proto-model evaluation use model_evaluator instead of legacy evaluator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-05 10:14:15 -08:00
Christoph M. Wintersteiger a2ecb19d03 Added hash-consing remarks to mk_context and mk_context_rc.
Fixes #452
2016-03-05 17:58:32 +00:00
Christoph M. Wintersteiger 8abedbf389 whitespace 2016-03-05 17:55:27 +00:00
Christoph M. Wintersteiger 03a8ef2795 Fixed non-Windows preprocessor options.
Fixes #463
2016-03-05 17:14:19 +00:00
Dan Liew 7fd5042ff3 Minor tweaks to `README-CMake.md`. 2016-03-05 16:53:29 +00:00
Christoph M. Wintersteiger f34e15f289 whitespace 2016-03-05 16:47:39 +00:00
Christoph M. Wintersteiger 9dfc2bc61e Fixed memory leaks in fpa2bv converter.
Fixes #480
2016-03-05 16:47:08 +00:00
Christoph M. Wintersteiger 09832ca807 Fixed static Windows binary build. 2016-03-05 13:58:28 +00:00
Christoph M. Wintersteiger fedc6d4754 Fixed memory leak in fpa2bv tactic. 2016-03-05 12:54:36 +00:00
Nikolaj Bjorner f54c430756 Merge pull request #483 from zv/fix_arith_div
Bugfix for arith_rewriter single operand division
2016-03-04 18:51:14 -08:00
Zephyr Pellerin b13db1e82e Bugfix for arith_rewriter single operand division 2016-03-04 18:26:00 -08: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 a52d81ef3e Document `z3_add_component()`. 2016-03-04 15:26:09 +00:00
Dan Liew 29901e79e1 Fix how the list of linker flags `Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS`
is applied to targets. The ``LINK_FLAGS`` property of a target is
a string and not a list and so if ``Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS``
contained more than one flag the linker line would end up being
``-flag1;flag2;flag3;...`` which would not work. Now we use a new
function ``z3_append_linker_flag_list_to_target()`` to iterate through
the list and update the ``LINK_FLAGS`` property of the specified target
correctly.
2016-03-04 15:26:09 +00:00
Dan Liew a2cc6d256a Emit an error message if building the Python bindings is enabled
but libz3 is built statically. This build combination doesn't
work because the Python bindings need a dynamic libz3.
2016-03-04 15:26:09 +00:00
Dan Liew 7033ebe6b5 Fix running the CMake bootstrap script under Python 2.7 2016-03-04 15:26:09 +00:00
Dan Liew d12b558bea Fix typo spotted by @arrowd 2016-03-04 15:26:09 +00:00