mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
6282 commits 49 branches 53 tags 182 MiB
Commit graph

6282 commits

This branch
This branch
All branches
Author SHA1 Message Date
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 #535 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 08:16:54 -07:00
Nikolaj Bjorner
05a784fa9e fix issue #535 
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 #531 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 #528 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 #527 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 #526 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 #522 
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 #523 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 #521 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
Nikolaj Bjorner
f951372f03 fix regression in internalizing bit-vectors, reported by Mikolas Janota 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-18 13:54:42 -07:00
Nikolaj Bjorner
b0f65335ab update copyright year 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-17 13:07:40 -07:00
Nikolaj Bjorner
ab82fee398 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-17 13:06:21 -07:00
Christoph M. Wintersteiger
94054593a4 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-17 17:52:32 +00:00
Christoph M. Wintersteiger
cc04fdbd70 Added eager ackermannization to QF_FP, so that small numbers of unspecified operators are eliminated upfront. 2016-03-17 17:52:26 +00:00
Nuno Lopes
f5c4800eec reduce-args: last fix for may_be_unique to support quantified variables in arbitrary exprs 2016-03-17 15:29:48 +00:00
Nuno Lopes
facb421398 reduce-args: fix unsoundness 2: f(v + 2), where b is quantified 2016-03-17 13:27:07 +00:00
Nuno Lopes
aed4619066 reduce-args: fixed unsoundness introduced in my previous commit 
skip an UF arg if it's quantified
e.g. forall a . f(a, b) -> f(b) (but not f)
 2016-03-17 13:14:43 +00:00
Christoph M. Wintersteiger
c8af48d7ef Bugfix for bvurem0 model evaluation (+1 rewriting step) 2016-03-17 13:09:52 +00:00