mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity
5121 commits 23 branches 48 tags 156 MiB
Commit graph

5121 commits

Author SHA1 Message Date
Dan Liew 6a2a8e06d7 [CMake] Declare uninstall rule before the components so that they 
can add dependencies to the rule for their own custom uninstall
logic.
 2016-03-26 17:59:11 +00:00
Dan Liew 23ac66ef42 Fix inconsistent emission of `Enumerations.cs`. The ordering of emitted 
enum values is not consistent between python 2 or 3. The root cause
of the problem was a dictionary's keys being iterated over which has
no defined order.

This has been fixed by iterating over the dictionary's items and
ordering by values.  We could order by key rather than the values but
seeing as these represent an enum, ordering by value makes more sense.
 2016-03-26 17:59:11 +00:00
Dan Liew d3f87e44a2 Refactor `mk_z3consts_dotnet() code into mk_z3consts_dotnet_internal()` 
and move that into ``mk_genfile_common.py``. Then adapt ``mk_util.py`` and
``mk_consts_files.py`` to call into the code at its new location.

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-26 17:59:11 +00:00
Nikolaj Bjorner 0870b4a5a0 add length coherence check for length = 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-25 17:17:34 -07:00
Nikolaj Bjorner f34a54fea0 fix stats collection over exceptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 17:08:13 -07:00
Nikolaj Bjorner 808855ce6b add internalization for auxiliary division functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 16:20:42 -07:00
Nikolaj Bjorner 709a5d9524 fix bug: & -> && 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 16:09:12 -07:00
Nikolaj Bjorner b30b8008b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-24 08:48:52 -07:00
Nikolaj Bjorner 29845d037b fix build break on seq evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 08:48:42 -07:00
Nuno Lopes 83e34638e6 add support to build with MSVC /Gr (fastcall mode for x86) 
not enabled by default nor exposed at the moment
 2016-03-24 15:39:18 +00:00
Nikolaj Bjorner 89fad8913f fix issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 08:16:54 -07:00
Nikolaj Bjorner 05a784fa9e fix issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 08:16:19 -07:00
Nikolaj Bjorner fe4f3e7772 fix regressions exposed in QF_LIA: manager got initialized early and Euclidean solver is not safe even with some throttle 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-23 20:38:18 -07:00
Nikolaj Bjorner 87989dd93e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-23 17:25:23 -07:00
Nikolaj Bjorner 45fdb95f53 fix performance for model construction, recognize concats of values as a value for pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-23 17:23:57 -07:00
Nikolaj Bjorner 8a4624e21f Merge pull request from seahorn/qearrays 
extend model with the value of a fresh variable
 2016-03-23 16:54:16 -07:00
Arie Gurfinkel 4e7b6b6586 proposed fix to compare 2016-03-23 19:20:57 -04:00
Arie Gurfinkel ee125b4fe3 extend model with the value of a fresh variable 2016-03-23 19:07:50 -04:00
Nikolaj Bjorner 96f113afee Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-23 10:19:25 -07:00
Nikolaj Bjorner ec681d7565 some of Arie's fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-23 10:19:16 -07:00
Christoph M. Wintersteiger 7e02c8f82a Merge pull request from EinNarr/master 
Clean up README
 2016-03-23 16:50:51 +00:00
Bohao Zhang 749e1a1fb1 Clean up README 
mentioning C++ and Java.
 2016-03-23 16:14:38 +01:00
Christoph M. Wintersteiger 5af5549a56 Merge pull request from tabe/examples-typo 
Fix typo in examples/*/README
 2016-03-23 12:41:14 +00:00
Takeshi Abe 5c2969c0f0 Fix typo 2016-03-23 12:51:41 +09:00
Nikolaj Bjorner fd6fe87c5d enable qe-lite for UFNIA benchmarks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-22 15:41:21 -07:00
Christoph M. Wintersteiger 4badc52dc3 Merge pull request from bpowers/_build 
build: allow overriding of 'ar' in mk_config
 2016-03-22 15:05:55 +00:00
Christoph M. Wintersteiger 8bcac82658 Merge branch 'master' of https://github.com/Z3Prover/z3 
# Conflicts:
#	CMakeLists.txt
 2016-03-22 15:04:48 +00:00
Christoph M. Wintersteiger 38fc49a05d Merge branch 'delcypher-cmake_fix_enable_tracing_in_debug_mode' 2016-03-22 15:02:40 +00:00
Bobby Powers 7bb085a565 build: allow overriding of 'ar' in mk_config 
This will still use 'ar' if AR isn't set in the environment, but lets
us override the default archive tool at configure time.

Just like CC and CXX, this doesn't apply to a ./configure for Windows.
 2016-03-22 10:47:51 -04:00
Nikolaj Bjorner 72ec6dc8e1 remove debug code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-21 16:58:48 -07:00
Nikolaj Bjorner 5e737641b7 remove qe-lite pass in quant_tatics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-21 16:57:30 -07:00
Nikolaj Bjorner 701f32471e hardening model checker code against cancellations' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-21 15:04:20 -07:00
Dan Liew d3afdc957b [CMake] Fix issue 
Previously tracing could be disabled and was not enabled by default in a
debug build. This isn't desirable but I had avoided fixing it because
enabling tracing in debug mode would be confusing because
``ENABLE_TRACING`` could be set to off but tracing would be enabled
anyway.

I have resolved this by renaming the option from ``ENABLE_TRACING`` to
``ENABLE_TRACING_FOR_NON_DEBUG``. The semantics of the optiona are now
that it will enable tracing in non-debug builds. I have also added code
to ensure that tracing is always enabled in debug builds.

Whilst I was here I also fixed how ``option()`` was being used. The
default value and comment were in the wrong order.
 2016-03-21 19:37:33 +00:00
Nikolaj Bjorner 3dc2028925 adding min/max 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-21 09:20:57 -07:00
Nikolaj Bjorner 680c28d083 remove nnf conversion which breaks NRA property 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 16:34:04 -07:00
Nikolaj Bjorner 1a5449c3d4 enable new NRA solver for nra benchmarks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 12:35:29 -07:00
Nikolaj Bjorner 73e29c6ee6 fix regression warning on invalid case split strategy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 10:20:43 -07:00
Nikolaj Bjorner 92b5aac12a adjusting new tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 10:13:23 -07:00
Nikolaj Bjorner b66fc4e355 Merge pull request from delcypher/fix_no_kind_namespace 
Fix gcc build broken by f175f864ec.
 2016-03-20 10:12:14 -07:00
Dan Liew 971fd59fbb Fix gcc build broken by f175f864ec. 
C++ enums (unless they are class enums) don't define their own
namespace.
 2016-03-20 10:18:59 +00:00
Nikolaj Bjorner f0bdcbb3db expose qsat tactic to default tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 18:40:59 -07:00
Christoph M. Wintersteiger fe201013e0 Merge pull request from delcypher/cmake_python_custom_install_location 
[CMake] Add CMAKE_INSTALL_PYTHON_PKG_DIR option to control where python
 2016-03-20 00:57:31 +00:00
Nikolaj Bjorner 67dc5ce2b5 fix cmake issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 15:51:31 -07:00
Nikolaj Bjorner 20bbdfe31a moving remaining qsat functionality over 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 15:35:26 -07:00
Nikolaj Bjorner 296addf246 add new files to cmakelists 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:44:44 -07:00
Nikolaj Bjorner d614fedde2 more merges with qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:41:41 -07:00
Nikolaj Bjorner 76d637626a include more qsat features 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:30:24 -07:00
Nikolaj Bjorner c4472ce717 include more qsat features 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:29:23 -07:00
Nikolaj Bjorner f175f864ec merge useful utilities from qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:01:44 -07:00
Dan Liew 8746cc4a14 [CMake] Add CMAKE_INSTALL_PYTHON_PKG_DIR option to control where python 
bindings are installed.
 2016-03-18 22:18:51 +00:00