From 8ab428b6600e0d0263b2986aea02553dc3fc931d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Jun 2018 17:42:44 -0700 Subject: [PATCH 1/9] try new gcd Signed-off-by: Nikolaj Bjorner --- src/util/mpz.cpp | 120 ++++++++++++++++++++++++++++++++++------------- 1 file changed, 87 insertions(+), 33 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 39ea428a7..409ca325f 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -45,43 +45,97 @@ Revision History: #define LEHMER_GCD #endif -template -static T gcd_core(T u, T v) { - if (u == 0) - return v; - if (v == 0) - return u; - int k; - - for (k = 0; ((u | v) & 1) == 0; ++k) { - u >>= 1; - v >>= 1; - } - - while ((u & 1) == 0) - u >>= 1; - +#if 1 +#include + +#define _trailing_zeros32(x) _tzcnt_u32(x) + +#ifdef _AMD64_ +#define _trailing_zeros64(x) _tzcnt_u64(x) +#else +inline uint64 _trailing_zeros64(uint64 x) { + uint64 r = 0; + for (; 0 == (x & 1) && r < 64; ++r, x >>= 1); + return r; +} +#endif + +#else + +inline unsigned _trailing_zeros32(unsigned x) { + unsigned r = 0; + for (; 0 == (x & 1) && r < 32; ++r, x >>= 1); + return r; +} +#endif + +#define _bit_min(x, y) (y + ((x - y) & ((int)(x - y) >> 31))) +#define _bit_max(x, y) (x - ((x - y) & ((int)(x - y) >> 31))) + + + +unsigned u_gcd(unsigned u, unsigned v) { + if (u == 0) return v; + if (v == 0) return u; + unsigned shift = _trailing_zeros32(u | v); + u >>= _trailing_zeros32(u); + v >>= _trailing_zeros32(v); + if (u == 1 || v == 1) return 1 << shift; + if (u == v) return u << shift; do { - while ((v & 1) == 0) - v >>= 1; - - if (u < v) { - v -= u; - } - else { - T diff = u - v; - u = v; - v = diff; - } - v >>= 1; - } while (v != 0); - - return u << k; +#if 1 + unsigned diff = u - v; + unsigned mdiff = diff & (unsigned)((int)diff >> 31); + u = v + mdiff; // min + v = diff - 2 * mdiff; // if v <= u: u - v, if v > u: v - u = u - v - 2 * (u - v) +#endif +#if 0 + unsigned t = _bit_max(u, v); + u = _bit_min(u, v); + v = t; + v -= u; +#endif +#if 0 + unsigned t = std::max(u, v); + u = std::min(u,v); + v = t; + v -= u; +#endif +#if 0 + if (u > v) std::swap(u, v); + v -= u; +#endif +#if 0 + unsigned d1 = u - v; + unsigned d2 = v - u; + unsigned md21 = d2 & (unsigned)((int)d1 >> 31); + unsigned md12 = d1 & (unsigned)((int)d2 >> 31); + u = _bit_min(u, v); + v = md12 | md21; +#endif + + v >>= _trailing_zeros32(v); + } + while (v != 0); + return u << shift; +} + +uint64 u64_gcd(uint64 u, uint64 v) { + if (u == 0) return v; + if (v == 0) return u; + if (u == 1 || v == 1) return 1; + uint64 shift = _trailing_zeros64(u | v); + u >>= _trailing_zeros64(u); + do { + v >>= _trailing_zeros64(v); + if (u > v) std::swap(u, v); + v -= u; + } + while (v != 0); + return u << shift; } -unsigned u_gcd(unsigned u, unsigned v) { return gcd_core(u, v); } -uint64_t u64_gcd(uint64_t u, uint64_t v) { return gcd_core(u, v); } template mpz_manager::mpz_manager(): From 99bdb461583e34f16df6b7f6508eebeafaf9d893 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Jun 2018 17:48:30 -0700 Subject: [PATCH 2/9] int64_t Signed-off-by: Nikolaj Bjorner --- src/util/mpz.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 409ca325f..8f65a3602 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -74,7 +74,6 @@ inline unsigned _trailing_zeros32(unsigned x) { #define _bit_max(x, y) (x - ((x - y) & ((int)(x - y) >> 31))) - unsigned u_gcd(unsigned u, unsigned v) { if (u == 0) return v; if (v == 0) return u; @@ -121,11 +120,11 @@ unsigned u_gcd(unsigned u, unsigned v) { return u << shift; } -uint64 u64_gcd(uint64 u, uint64 v) { +uint64_t u64_gcd(uint64_t u, uint64_t v) { if (u == 0) return v; if (v == 0) return u; if (u == 1 || v == 1) return 1; - uint64 shift = _trailing_zeros64(u | v); + auto shift = _trailing_zeros64(u | v); u >>= _trailing_zeros64(u); do { v >>= _trailing_zeros64(v); From d7f51f2443edd5ee57255fc652a2da5e7f990aae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Jun 2018 18:20:23 -0700 Subject: [PATCH 3/9] try flags to fix gcc build Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a086afd71..f34e400f5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -381,7 +381,7 @@ endif() # FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard" if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" STREQUAL "i686")) if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")) - set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2") + set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2" "-mfsr") # FIXME: Remove "x.." when CMP0054 is set to NEW elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") set(SSE_FLAGS "/arch:SSE2") From ad67424987aeae720054b21f3196471dac08f474 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Jun 2018 18:23:04 -0700 Subject: [PATCH 4/9] deal with shift exponent error Signed-off-by: Nikolaj Bjorner --- src/util/mpz.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 8f65a3602..6387fccd9 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -79,10 +79,10 @@ unsigned u_gcd(unsigned u, unsigned v) { if (v == 0) return u; unsigned shift = _trailing_zeros32(u | v); u >>= _trailing_zeros32(u); - v >>= _trailing_zeros32(v); if (u == 1 || v == 1) return 1 << shift; if (u == v) return u << shift; do { + v >>= _trailing_zeros32(v); #if 1 unsigned diff = u - v; unsigned mdiff = diff & (unsigned)((int)diff >> 31); @@ -113,8 +113,6 @@ unsigned u_gcd(unsigned u, unsigned v) { u = _bit_min(u, v); v = md12 | md21; #endif - - v >>= _trailing_zeros32(v); } while (v != 0); return u << shift; From 8565de2c5b38cd355ea15f1da3f460f352162f86 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Jun 2018 19:17:37 -0700 Subject: [PATCH 5/9] deal with shift exponent error Signed-off-by: Nikolaj Bjorner --- src/util/mpz.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 6387fccd9..2a85320a5 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -49,9 +49,13 @@ Revision History: #if 1 #include -#define _trailing_zeros32(x) _tzcnt_u32(x) +#if defined(__GNUC__) +#define _trailing_zeros32(X) __builtin_ctz(X) +#else +#define _trailing_zeros32(X) _tzcnt_u32(X) +#endif -#ifdef _AMD64_ +#if defined(_AMD64_) && !defined(__GNUC__) #define _trailing_zeros64(x) _tzcnt_u64(x) #else inline uint64 _trailing_zeros64(uint64 x) { From bb5306031369dd22cfcc291ea7aeeb83b2c8fc63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Jun 2018 19:26:40 -0700 Subject: [PATCH 6/9] int64_t Signed-off-by: Nikolaj Bjorner --- src/util/mpz.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 2a85320a5..50f0d68e7 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -58,8 +58,8 @@ Revision History: #if defined(_AMD64_) && !defined(__GNUC__) #define _trailing_zeros64(x) _tzcnt_u64(x) #else -inline uint64 _trailing_zeros64(uint64 x) { - uint64 r = 0; +inline uint64_t _trailing_zeros64(uint64_t x) { + uint64_t r = 0; for (; 0 == (x & 1) && r < 64; ++r, x >>= 1); return r; } From 88ead235f0f8ab16e90efc52bc4b2b5df7269123 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Jun 2018 19:30:56 -0700 Subject: [PATCH 7/9] gcc mode Signed-off-by: Nikolaj Bjorner --- src/util/mpz.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 50f0d68e7..ddca84922 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -55,8 +55,12 @@ Revision History: #define _trailing_zeros32(X) _tzcnt_u32(X) #endif -#if defined(_AMD64_) && !defined(__GNUC__) -#define _trailing_zeros64(x) _tzcnt_u64(x) +#if defined(_AMD64_) + #if defined(__GNUC__) + #define _trailing_zeros64(X) __builtin_ctzll(X) + #else + #define _trailing_zeros64(X) _tzcnt_u64(X) + #endif #else inline uint64_t _trailing_zeros64(uint64_t x) { uint64_t r = 0; From 4547f2c001d894808987487a5e98c713debff411 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Jun 2018 22:03:03 -0700 Subject: [PATCH 8/9] enable non-expression bodies of quantifiers to fix #1667 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 10 +++++++--- src/util/mpz.cpp | 9 --------- 2 files changed, 7 insertions(+), 12 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 7657fb347..89615e11e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1898,13 +1898,17 @@ def is_quantifier(a): def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): if __debug__: - _z3_assert(is_bool(body), "Z3 expression expected") + _z3_assert(is_bool(body) or is_app(vs) or (len(vs) > 0 and is_app(vs[0])), "Z3 expression expected") _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)") _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected") - _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions") - ctx = body.ctx + _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions") if is_app(vs): + ctx = vs.ctx vs = [vs] + else: + ctx = vs[0].ctx + if not is_expr(body): + body = BoolVal(body, ctx) num_vars = len(vs) if num_vars == 0: return body diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index ddca84922..861a31cfb 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -46,7 +46,6 @@ Revision History: #endif -#if 1 #include #if defined(__GNUC__) @@ -69,14 +68,6 @@ inline uint64_t _trailing_zeros64(uint64_t x) { } #endif -#else - -inline unsigned _trailing_zeros32(unsigned x) { - unsigned r = 0; - for (; 0 == (x & 1) && r < 32; ++r, x >>= 1); - return r; -} -#endif #define _bit_min(x, y) (y + ((x - y) & ((int)(x - y) >> 31))) #define _bit_max(x, y) (x - ((x - y) & ((int)(x - y) >> 31))) From 0520d1a1f694339039a68796353c4ee040b94e46 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Jun 2018 07:38:30 -0700 Subject: [PATCH 9/9] remove trial with mfsr flag Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index f34e400f5..a086afd71 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -381,7 +381,7 @@ endif() # FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard" if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" STREQUAL "i686")) if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")) - set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2" "-mfsr") + set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2") # FIXME: Remove "x.." when CMP0054 is set to NEW elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") set(SSE_FLAGS "/arch:SSE2")