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

5623 commits

Author SHA1 Message Date
hongjiawu
6a2f27476c Update README.md 2016-03-10 18:10:59 +01:00
Christoph M. Wintersteiger
9095d7db44 Merge pull request #504 from delcypher/cmake_custom_install_dirs
[CMake] Provide a way to customise the install directories
2016-03-10 12:39:11 +00:00
Nuno Lopes
d6c3260db7 reduce_args_tactic: make it aware that 'a + const' may be a unique value in bv theory
it allows us to remove UFs that are of the form f(a + 1), f(a + 2), etc..
2016-03-10 10:15:09 +00:00
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
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
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
fa0fc6b141 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-07 15:37:41 +00:00
Christoph M. Wintersteiger
3968423c26 build fix for ML API 2016-03-07 15:35:25 +00: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
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
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