mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
5006 commits 49 branches 53 tags 182 MiB
Commit graph

5006 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
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
Dan Liew
017e9a2461 Try to fix the freebsd build by linking against the system's 
threading library.
 2016-03-04 15:26:09 +00:00