3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 10:51:50 +00:00
Commit graph

5123 commits

Author SHA1 Message Date
Nuno Lopes 0b1b5a4328 fix VS x64 warning 2016-03-10 09:03:24 +00:00
Nikolaj Bjorner 2354e747bf Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-09 21:33:16 -08:00
Nikolaj Bjorner 3d7eb12117 tracking use of assumptions in tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-09 21:33:08 -08:00
Nikolaj Bjorner 843e95cddc updating CMakeLists file, hope it works :-)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-09 15:56:23 -08:00
Nikolaj Bjorner 6ad6998c57 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-09 15:53:16 -08:00
Nikolaj Bjorner 03a0a6f6a1 refactor occurrence utility for common use (to be used in ctx_simplifier) per Nuno's suggestion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-09 15:53:02 -08:00
Nuno Lopes 8b53628d67 remove a few unused decls 2016-03-09 17:01:06 +00:00
Dan Liew 04ca873abb [CMake] Provide a way to customise the install directories used for
executables, include files and libraries. We use
``GNUInstallDirs.cmake`` which ships with CMake to do the difficult work
of setting a sensible default and setting up CMake cache variables.
These can be overriden when running CMake by setting the
``CMAKE_INSTALL_BINDIR``, ``CMAKE_INSTALL_INCLUDEDIR`` and
``CMAKE_INSTALL_LIBDIR`` cache variables.
2016-03-09 14:22:27 +00:00
Christoph M. Wintersteiger 402e132ce5 Merge pull request #499 from delcypher/minor_cmake_fixes
Minor cmake fixes
2016-03-09 13:29:35 +00:00
Christoph M. Wintersteiger 7413b3278f Merge pull request #503 from martin-neuhaeusser/ufbv_and_ack
Fix bug in ufbv tactic that enabled ackermannization even if unsat co…
2016-03-09 13:29:13 +00:00
Dan Liew ad4ddff99a [CMake] If OpenMP support is not found make sure we set `USE_OPENMP`
to ``OFF`` to make it clear in ccmake/cmake-gui that the support is
disabled. Previously it would be left as ``ON`` even if support wasn't
actually enabled.
2016-03-09 13:07:14 +00:00
martin-neuhaeusser c7a7cc74fa Fix bug in ufbv tactic that enabled ackermannization even if unsat core or proof generation are requested 2016-03-09 14:06:39 +01:00
Dan Liew e12875ddb5 [CMake] Mirror the additional NDEBUG define for non debug builds recently added
by 03a8ef2795 . This relates to #463

Also leave a note regarding ``compiler_flags_override.cmake`` its
value is a bit dubious now that the compiler flags are almost the CMake
defaults.
2016-03-09 11:46:46 +00:00
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
Dan Liew 236875c3ab [CMake] Fix incorrect variable name. 2016-03-09 09:39:08 +00:00
Nikolaj Bjorner 71fff8ffa2 fix boundary case according to analysis #477, e.g., size = 252, PTR_ALIGNMENT=2, slot_id = 64 = NUM_SLOTS
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-09 00:42:50 -08:00
Nikolaj Bjorner 5db84575f6 fix regression in o7.smt2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-08 22:27:47 -08: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