From fbc33b20c869ece56ee6b7a985e846b61a02a14b Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 30 Nov 2018 19:52:57 +0700 Subject: [PATCH 01/13] cmake: Allow saving clang's optimization records. This gives some insight into what the compiler has decided to do or not do. --- CMakeLists.txt | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index bc5eecdef..34d2c689d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -425,6 +425,15 @@ list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT}) ################################################################################ include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake) +################################################################################ +# Save Clang optimization records +################################################################################ +option(SAVE_CLANG_OPTIMIZATION_RECORDS "Enable saving Clang optimization records." OFF) + +if (SAVE_CLANG_OPTIMIZATION_RECORDS) + z3_add_cxx_flag("-fsave-optimization-record" REQUIRED) +endif() + ################################################################################ # If using Ninja, force color output for Clang (and gcc, disabled to check build). ################################################################################ From 3149d7f7a4962dc9865999b28d829972786fce2e Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 30 Nov 2018 22:19:30 +0700 Subject: [PATCH 02/13] Fix typos. --- src/ast/datatype_decl_plugin.cpp | 2 +- src/math/realclosure/realclosure.cpp | 10 +++++----- src/sat/tactic/sat_tactic.cpp | 2 +- src/smt/smt_setup.cpp | 2 +- src/smt/theory_str.cpp | 26 +++++++++++++------------- src/tactic/sls/sls_engine.cpp | 2 +- src/test/lp/smt_reader.h | 4 ++-- 7 files changed, 24 insertions(+), 24 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 9cb685ccc..0271d8311 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -682,7 +682,7 @@ namespace datatype { /** \brief Return true if the inductive datatype is well-founded. - Pre-condition: The given argument constains the parameters of an inductive datatype. + Pre-condition: The given argument constrains the parameters of an inductive datatype. */ bool util::is_well_founded(unsigned num_types, sort* const* sorts) { buffer well_founded(num_types, false); diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 0bc3b43d3..3e05be734 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -154,7 +154,7 @@ namespace realclosure { struct value { unsigned m_ref_count; //!< Reference counter - bool m_rational; //!< True if the value is represented as an abitrary precision rational value. + bool m_rational; //!< True if the value is represented as an arbitrary precision rational value. mpbqi m_interval; //!< approximation as an interval with binary rational end-points // When performing an operation OP, we may have to make the width (upper - lower) of m_interval very small. // The precision (i.e., a small interval) needed for executing OP is usually unnecessary for subsequent operations, @@ -283,7 +283,7 @@ namespace realclosure { struct algebraic : public extension { polynomial m_p; mpbqi m_iso_interval; - sign_det * m_sign_det; //!< != 0 if m_iso_interval constains more than one root of m_p. + sign_det * m_sign_det; //!< != 0 if m_iso_interval constrains more than one root of m_p. unsigned m_sc_idx; //!< != UINT_MAX if m_sign_det != 0, in this case m_sc_idx < m_sign_det->m_sign_conditions.size() bool m_depends_on_infinitesimals; //!< True if the polynomial p depends on infinitesimal extensions. @@ -1741,7 +1741,7 @@ namespace realclosure { \brief In the sign determination algorithm main loop, we keep processing polynomials q, and checking whether they discriminate the roots of the target polynomial. - The vectors sc_cardinalities contains the cardinalites of the new realizable sign conditions. + The vectors sc_cardinalities contains the cardinalities of the new realizable sign conditions. That is, we started we a sequence of sign conditions sc_1, ..., sc_n, If q2_used is true, then we expanded this sequence as @@ -1750,7 +1750,7 @@ namespace realclosure { Thus, q is useful (i.e., it is a discriminator for the roots of p) IF If !q2_used, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0 - If q2_used, then There is an i s.t. AtLeatTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) + If q2_used, then There is an i s.t. AtLeastTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) */ bool keep_new_sc_assignment(unsigned sz, int const * sc_cardinalities, bool q2_used) { SASSERT(q2_used || sz % 2 == 0); @@ -2038,7 +2038,7 @@ namespace realclosure { // We should keep q only if it discriminated something. // That is, // If !use_q2, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0 - // If use_q2, then There is an i s.t. AtLeatTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) + // If use_q2, then There is an i s.t. AtLeastTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) if (!keep_new_sc_assignment(sc_cardinalities.size(), sc_cardinalities.c_ptr(), use_q2)) { // skip q since it did not reduced the cardinality of the existing sign conditions. continue; diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index ef8a9e77e..e6369a918 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -105,7 +105,7 @@ class sat_tactic : public tactic { else { // get simplified problem. #if 0 - IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constains interpreted atoms, recovering formula from sat solver...\"\n";); + IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constrains interpreted atoms, recovering formula from sat solver...\"\n";); #endif m_solver.pop_to_base_level(); ref mc; diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 2cf0e2651..a6b27784f 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -209,7 +209,7 @@ namespace smt { static void check_no_arithmetic(static_features const & st, char const * logic) { if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0) - throw default_exception("Benchmark constains arithmetic, but specified logic does not support it."); + throw default_exception("Benchmark constrains arithmetic, but specified logic does not support it."); } void setup::setup_QF_UF() { diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0e5393ac7..2ae445561 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -9424,15 +9424,15 @@ namespace smt { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { - int lrConstainted = 0; + int lrConstrained = 0; std::map::iterator lrit = freeVarMap.begin(); for (; lrit != freeVarMap.end(); lrit++) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { - lrConstainted = 1; + lrConstrained = 1; break; } } - if (lrConstainted == 0) { + if (lrConstrained == 0) { freeVarMap[var] = 1; } } @@ -9451,15 +9451,15 @@ namespace smt { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { - int lrConstainted = 0; + int lrConstrained = 0; std::map::iterator lrit = freeVarMap.begin(); for (; lrit != freeVarMap.end(); lrit++) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { - lrConstainted = 1; + lrConstrained = 1; break; } } - if (lrConstainted == 0) { + if (lrConstrained == 0) { freeVarMap[var] = 1; } } @@ -9471,15 +9471,15 @@ namespace smt { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { - int lrConstainted = 0; + int lrConstrained = 0; std::map::iterator lrit = freeVarMap.begin(); for (; lrit != freeVarMap.end(); lrit++) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { - lrConstainted = 1; + lrConstrained = 1; break; } } - if (lrConstainted == 0) { + if (lrConstrained == 0) { freeVarMap[var] = 1; } } @@ -9500,15 +9500,15 @@ namespace smt { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { - int lrConstainted = 0; + int lrConstrained = 0; std::map::iterator lrit = freeVarMap.begin(); for (; lrit != freeVarMap.end(); lrit++) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { - lrConstainted = 1; + lrConstrained = 1; break; } } - if (lrConstainted == 0) { + if (lrConstrained == 0) { freeVarMap[var] = 1; } } @@ -9762,7 +9762,7 @@ namespace smt { expr_ref concatlenExpr (mk_strlen(concat), m) ; bool allLeafResolved = true; if (! get_arith_value(concatlenExpr, lenValue)) { - // the length fo concat is unresolved yet + // the length of concat is unresolved yet if (get_len_value(concat, lenValue)) { // but all leaf nodes have length information TRACE("str", tout << "* length pop-up: " << mk_ismt2_pp(concat, m) << "| = " << lenValue << std::endl;); diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index 2aeb355ed..f55aa41aa 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -492,7 +492,7 @@ lbool sls_engine::search() { score = m_tracker.get_top_sum(); - // update assertion weights if a weigthing is enabled (sp < 1024) + // update assertion weights if a weighting is enabled (sp < 1024) if (m_paws) { for (unsigned i = 0; i < sz; i++) diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h index 5d386862c..4bce99765 100644 --- a/src/test/lp/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -193,14 +193,14 @@ namespace lp { } } - void adjust_rigth_side(formula_constraint & /* c*/, lisp_elem & /*el*/) { + void adjust_right_side(formula_constraint & /* c*/, lisp_elem & /*el*/) { // lp_assert(el.m_head == "0"); // do nothing for the time being } void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) { lp_assert(el.m_elems.size() == 2); set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]); - adjust_rigth_side(c, el.m_elems[1]); + adjust_right_side(c, el.m_elems[1]); } From bcfa8045fabbdf0bab640a3b8082db11f7603604 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 30 Nov 2018 23:12:21 +0700 Subject: [PATCH 03/13] Sink some values into loops. This removes some dead stores that happen prior to the loop and ensure that no one is looking at the values outside of the loop. --- src/math/polynomial/upolynomial.cpp | 6 ++---- src/smt/theory_lra.cpp | 10 ++++------ 2 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index 5a7ed0dc1..0290a5924 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -1339,12 +1339,10 @@ namespace upolynomial { // Return the number of sign changes in the coefficients of p unsigned manager::sign_changes(unsigned sz, numeral const * p) { unsigned r = 0; - int sign, prev_sign; - sign = 0; - prev_sign = 0; + int prev_sign = 0; unsigned i = 0; for (; i < sz; i++) { - sign = sign_of(p[i]); + int sign = sign_of(p[i]); if (sign == 0) continue; if (sign != prev_sign && prev_sign != 0) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ddf3e6fd2..c9db3f6b0 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2283,16 +2283,14 @@ public: iterator lo_inf = begin1, lo_sup = begin1; iterator hi_inf = begin2, hi_sup = begin2; - iterator lo_inf1 = begin1, lo_sup1 = begin1; - iterator hi_inf1 = begin2, hi_sup1 = begin2; bool flo_inf, fhi_inf, flo_sup, fhi_sup; ptr_addr_hashtable visited; for (unsigned i = 0; i < atoms.size(); ++i) { lp_api::bound* a1 = atoms[i]; - lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf); - hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf); - lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup); - hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup); + iterator lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf); + iterator hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf); + iterator lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup); + iterator hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup); if (lo_inf1 != end) lo_inf = lo_inf1; if (lo_sup1 != end) lo_sup = lo_sup1; if (hi_inf1 != end) hi_inf = hi_inf1; From c51caad5ad606747b050fa5e2bf247184397f4cf Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 30 Nov 2018 23:12:55 +0700 Subject: [PATCH 04/13] Remove duplicate initialization of a sort variable. --- src/smt/theory_bv.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 33207d15a..0f4a6480b 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1083,7 +1083,6 @@ namespace smt { for (unsigned i = 0; i <= num_args; i++) { expr* arg = (i == num_args)?n:n->get_arg(i); sort* s = get_manager().get_sort(arg); - s = get_manager().get_sort(arg); if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > m_params.m_bv_blast_max_size) { if (!m_approximates_large_bvs) { TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, get_manager()) << "\n";); From 2faf5ef995ad69dc7faa8ee168b89d2b25345681 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 30 Nov 2018 23:13:22 +0700 Subject: [PATCH 05/13] Remove unused iPos. This was incremented, but never actually used, so remove it. --- src/smt/theory_str.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 2ae445561..bd0885fa4 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7501,15 +7501,12 @@ namespace smt { expr_ref newConcat(m); if (arg1 != a1 || arg2 != a2) { TRACE("str", tout << "resolved concat argument(s) to eqc string constants" << std::endl;); - int iPos = 0; expr_ref_vector item1(m); if (a1 != arg1) { item1.push_back(ctx.mk_eq_atom(a1, arg1)); - iPos += 1; } if (a2 != arg2) { item1.push_back(ctx.mk_eq_atom(a2, arg2)); - iPos += 1; } expr_ref implyL1(mk_and(item1), m); newConcat = mk_concat(arg1, arg2); From a3ece29628501b405cb065f535ab0a003672fec0 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 1 Dec 2018 20:39:03 +0700 Subject: [PATCH 06/13] Remove include of immintrin.h. This file doesn't appear to be used and isn't available on all platforms. --- src/util/mpz.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 32a074eb3..47c88560c 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -30,7 +30,6 @@ Revision History: #else #error No multi-precision library selected. #endif -#include // Available GCD algorithms // #define EUCLID_GCD From 150fe881ce968427fbf7b13c1b2a794ea350fa5d Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 1 Dec 2018 21:06:16 +0700 Subject: [PATCH 07/13] Fix typo. --- src/util/hwf.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 32b1343e3..e6393adbd 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -303,7 +303,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o // CMW: modf is not the right function here. // modf(x.value, &o.value); - // According to the Intel Architecture manual, the x87-instrunction FRNDINT is the + // According to the Intel Architecture manual, the x87-instruction FRNDINT is the // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions. #ifdef _WINDOWS #if defined(USE_INTRINSICS) && \ From dad58073d33c1459ce1abc9a784b7d53e548e651 Mon Sep 17 00:00:00 2001 From: Travis Nielsen Date: Sat, 1 Dec 2018 16:47:19 -0600 Subject: [PATCH 08/13] Fix typo --- scripts/mk_genfile_common.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index c42eaf86d..a65b41026 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -719,7 +719,7 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path): fullname, line)) raise e except Exception as e: - _loggeer.error("Failed to read file {}\n".format(h_file)) + _logger.error("Failed to read file {}\n".format(h_file)) raise e # First pass will just generate the tactic factories fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, CODE) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, [](ast_manager &m, const params_ref &p) { return CODE; }))\n') From a0a940f9388196667e3c7b7d67714498e989217b Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sun, 2 Dec 2018 13:58:31 +0700 Subject: [PATCH 09/13] Remove unused THREAD_LOCAL macro. --- src/util/util.h | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/util/util.h b/src/util/util.h index b9f3bdc28..0ca02bc84 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -63,14 +63,6 @@ static_assert(sizeof(int64_t) == 8, "64 bits"); #define VEC2PTR(_x_) ((_x_).size() ? &(_x_)[0] : 0) -#ifdef _WINDOWS -// Disable thread local declspec as it seems to not work downlevel. -// #define THREAD_LOCAL __declspec(thread) -#define THREAD_LOCAL -#else -#define THREAD_LOCAL -#endif - #ifdef _MSC_VER # define STD_CALL __cdecl #else From a332eb10bc938909f75ace5780541e2ac83e0aff Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sun, 2 Dec 2018 22:10:37 +0700 Subject: [PATCH 10/13] Use C++11 thread_local for portability. This should work on all supported compilers rather than using __declspec(thread) and __thread. --- src/util/memory_manager.cpp | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 148306fbd..5d494834e 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -241,15 +241,8 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) { // when the local counter > SYNCH_THRESHOLD #define SYNCH_THRESHOLD 100000 -#ifdef _WINDOWS -// Actually this is VS specific instead of Windows specific. -__declspec(thread) long long g_memory_thread_alloc_size = 0; -__declspec(thread) long long g_memory_thread_alloc_count = 0; -#else -// GCC style -__thread long long g_memory_thread_alloc_size = 0; -__thread long long g_memory_thread_alloc_count = 0; -#endif +thread_local long long g_memory_thread_alloc_size = 0; +thread_local long long g_memory_thread_alloc_count = 0; static void synchronize_counters(bool allocating) { #ifdef PROFILE_MEMORY From f40eed99f7115654b0672f6bd8983ef139896c05 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sun, 2 Dec 2018 23:48:46 +0700 Subject: [PATCH 11/13] Remove unused nl_purify_tactic.cpp This file wasn't built and won't compile as the header for it is missing. Most of the related code was removed in df6b1a707ebc406bf47bc9ed1bdbeb98248ca39c. --- src/tactic/nlsat_smt/nl_purify_tactic.cpp | 799 ---------------------- src/tactic/tactic.h | 1 - 2 files changed, 800 deletions(-) delete mode 100644 src/tactic/nlsat_smt/nl_purify_tactic.cpp diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp deleted file mode 100644 index a02c2d327..000000000 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ /dev/null @@ -1,799 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - - nl_purify_tactic.cpp - -Abstract: - - Tactic for purifying quantifier-free formulas that mix QF_NRA and other theories. - It is designed to allow cooperation between the nlsat solver and other theories - in a decoupled way. - - Let goal be formula F. - Let NL goal be formula G. - Assume F is in NNF. - Assume F does not contain mix of real/integers. - Assume F is quantifier-free (please, otherwise we need to reprocess from instantiated satisfiable formula) - - For each atomic nl formula f, - - introduce a propositional variable p - - replace f by p - - add clauses p => f to G - - For each interface term t, - - introduce interface variable v (or use t if it is already a variable) - - replace t by v - - Check satisfiability of G. - If satisfiable, then check assignment to p and interface equalities on F - If unsat: - Retrieve core and add core to G. - else: - For interface equalities from model of F that are not equal in G, add - For interface variables that are equal under one model, but not the other model, - create interface predicate p_vw => v = w, add to both F, G. - Add interface equations to assumptions, recheck F. - If unsat retrieve core add to G. - -Author: - - Nikolaj Bjorner (nbjorner) 2015-5-5. - -Revision History: - ---*/ -#include "tactic/tactical.h" -#include "tactic/nlsat_smt/nl_purify_tactic.h" -#include "smt/tactic/smt_tactic.h" -#include "ast/rewriter/rewriter.h" -#include "nlsat/tactic/nlsat_tactic.h" -#include "tactic/filter_model_converter.h" -#include "util/obj_pair_hashtable.h" -#include "ast/rewriter/rewriter_def.h" -#include "ast/ast_pp.h" -#include "util/trace.h" -#include "smt/smt_solver.h" -#include "solver/solver.h" -#include "model/model_smt2_pp.h" -#include "ast/rewriter/expr_safe_replace.h" -#include "ast/ast_util.h" -#include "solver/solver2tactic.h" - -class nl_purify_tactic : public tactic { - - enum polarity_t { - pol_pos, - pol_neg, - pol_dual - }; - - ast_manager & m; - arith_util m_util; - params_ref m_params; - bool m_produce_proofs; - ref m_fmc; - tactic_ref m_nl_tac; // nlsat tactic - goal_ref m_nl_g; // nlsat goal - ref m_solver; // SMT solver - expr_ref_vector m_eq_preds; // predicates for equality between pairs of interface variables - svector m_eq_values; // truth value of the equality predicates in nlsat - app_ref_vector m_new_reals; // interface real variables - app_ref_vector m_new_preds; // abstraction predicates for smt_solver (hide real constraints) - expr_ref_vector m_asms; // assumptions to pass to SMT solver - ptr_vector m_ctx_asms; // assumptions passed by context - obj_hashtable m_ctx_asms_set; // assumptions passed by context - obj_hashtable m_used_asms; - obj_map m_bool2dep; - obj_pair_map m_eq_pairs; // map pairs of interface variables to auxiliary predicates - obj_map m_interface_cache; // map of compound real expression to interface variable. - obj_map m_polarities; // polarities of sub-expressions - -public: - struct rw_cfg : public default_rewriter_cfg { - enum mode_t { - mode_interface_var, - mode_bool_preds - }; - ast_manager& m; - nl_purify_tactic & m_owner; - app_ref_vector& m_new_reals; - app_ref_vector& m_new_preds; - obj_map& m_polarities; - obj_map& m_interface_cache; - expr_ref_vector m_args; - proof_ref_vector m_proofs; - mode_t m_mode; - - rw_cfg(nl_purify_tactic & o): - m(o.m), - m_owner(o), - m_new_reals(o.m_new_reals), - m_new_preds(o.m_new_preds), - m_polarities(o.m_polarities), - m_interface_cache(o.m_interface_cache), - m_args(m), - m_proofs(m), - m_mode(mode_interface_var) { - } - - virtual ~rw_cfg() {} - - arith_util & u() { return m_owner.m_util; } - - expr * mk_interface_var(expr* arg, proof_ref& arg_pr) { - expr* r; - if (m_interface_cache.find(arg, r)) { - return r; - } - if (is_uninterp_const(arg)) { - m_interface_cache.insert(arg, arg); - return arg; - } - r = m.mk_fresh_const(nullptr, u().mk_real()); - m_new_reals.push_back(to_app(r)); - m_owner.m_fmc->insert(to_app(r)->get_decl()); - m_interface_cache.insert(arg, r); - expr_ref eq(m); - eq = m.mk_eq(r, arg); - if (is_real_expression(arg)) { - m_owner.m_nl_g->assert_expr(eq); // m.mk_oeq(r, arg) - } - else { - m_owner.m_solver->assert_expr(eq); - } - if (m_owner.m_produce_proofs) { - arg_pr = m.mk_oeq(arg, r); - } - return r; - } - - bool is_real_expression(expr* e) { - return is_app(e) && (to_app(e)->get_family_id() == u().get_family_id()); - } - - void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref& pr) { - expr_ref old_pred(m.mk_app(f, num, args), m); - polarity_t pol = m_polarities.find(old_pred); - result = m.mk_fresh_const(nullptr, m.mk_bool_sort()); - m_polarities.insert(result, pol); - m_new_preds.push_back(to_app(result)); - m_owner.m_fmc->insert(to_app(result)->get_decl()); - if (pol != pol_neg) { - m_owner.m_nl_g->assert_expr(m.mk_or(m.mk_not(result), old_pred)); - } - if (pol != pol_pos) { - m_owner.m_nl_g->assert_expr(m.mk_or(result, m.mk_not(old_pred))); - } - if (m_owner.m_produce_proofs) { - pr = m.mk_oeq(old_pred, result); - } - TRACE("nlsat_smt", tout << old_pred << " : " << result << "\n";); - } - - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, - expr * const * new_no_patterns, - expr_ref & result, - proof_ref & result_pr) { - throw tactic_exception("quantifiers are not supported in mixed-mode nlsat engine"); - } - - br_status reduce_app(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { - if (m_mode == mode_bool_preds) { - return reduce_app_bool(f, num, args, result, pr); - } - else { - return reduce_app_real(f, num, args, result, pr); - } - } - - br_status reduce_app_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { - if (f->get_family_id() == m.get_basic_family_id()) { - if (f->get_decl_kind() == OP_EQ && u().is_real(args[0])) { - mk_interface_bool(f, num, args, result, pr); - return BR_DONE; - } - else { - return BR_FAILED; - } - } - if (f->get_family_id() == u().get_family_id()) { - switch (f->get_decl_kind()) { - case OP_LE: case OP_GE: case OP_LT: case OP_GT: - // these are the only real cases of non-linear atomic formulas besides equality. - mk_interface_bool(f, num, args, result, pr); - return BR_DONE; - default: - return BR_FAILED; - } - } - return BR_FAILED; - } - - // (+ (f x) y) - // (f (+ x y)) - // - bool is_arith_op(expr* e) { - return is_app(e) && to_app(e)->get_family_id() == u().get_family_id(); - } - - br_status reduce_app_real(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { - bool has_interface = false; - bool is_arith = false; - if (f->get_family_id() == u().get_family_id()) { - switch (f->get_decl_kind()) { - case OP_NUM: - case OP_IRRATIONAL_ALGEBRAIC_NUM: - return BR_FAILED; - default: - is_arith = true; - break; - } - } - m_args.reset(); - m_proofs.reset(); - for (unsigned i = 0; i < num; ++i) { - expr* arg = args[i]; - proof_ref arg_pr(m); - if (is_arith && !is_arith_op(arg)) { - has_interface = true; - m_args.push_back(mk_interface_var(arg, arg_pr)); - } - else if (!is_arith && u().is_real(arg)) { - has_interface = true; - m_args.push_back(mk_interface_var(arg, arg_pr)); - } - else { - m_args.push_back(arg); - } - if (arg_pr) { - m_proofs.push_back(arg_pr); - } - } - if (has_interface) { - result = m.mk_app(f, num, m_args.c_ptr()); - if (m_owner.m_produce_proofs) { - pr = m.mk_oeq_congruence(m.mk_app(f, num, args), to_app(result), m_proofs.size(), m_proofs.c_ptr()); - } - TRACE("nlsat_smt", tout << result << "\n";); - return BR_DONE; - } - else { - return BR_FAILED; - } - } - }; - -private: - - class rw : public rewriter_tpl { - rw_cfg m_cfg; - public: - rw(nl_purify_tactic & o): - rewriter_tpl(o.m, o.m_produce_proofs, m_cfg), - m_cfg(o) { - } - void set_bool_mode() { - m_cfg.m_mode = rw_cfg::mode_bool_preds; - } - void set_interface_var_mode() { - m_cfg.m_mode = rw_cfg::mode_interface_var; - } - }; - - - arith_util & u() { return m_util; } - - void check_point() { - if (m.canceled()) { - throw tactic_exception(Z3_CANCELED_MSG); - } - } - - void display_result(std::ostream& out, goal_ref_buffer const& result) { - for (unsigned i = 0; i < result.size(); ++i) { - result[i]->display_with_dependencies(out << "goal\n"); - } - } - - void update_eq_values(model_ref& mdl) { - expr_ref tmp(m); - for (unsigned i = 0; i < m_eq_preds.size(); ++i) { - expr* pred = m_eq_preds[i].get(); - m_eq_values[i] = l_undef; - if (mdl->eval(pred, tmp)) { - if (m.is_true(tmp)) { - m_eq_values[i] = l_true; - } - else if (m.is_false(tmp)) { - m_eq_values[i] = l_false; - } - } - } - } - - void solve( - goal_ref const& g, - goal_ref_buffer& result, - expr_dependency_ref& core, - model_converter_ref& mc) { - - while (true) { - check_point(); - TRACE("nlsat_smt", m_solver->display(tout << "SMT:\n"); m_nl_g->display(tout << "\nNL:\n"); ); - goal_ref tmp_nl = alloc(goal, m, true, false); - model_converter_ref nl_mc; - proof_converter_ref nl_pc; - expr_dependency_ref nl_core(m); - result.reset(); - tmp_nl->copy_from(*m_nl_g.get()); - (*m_nl_tac)(tmp_nl, result, nl_mc, nl_pc, nl_core); - - if (is_decided_unsat(result)) { - core2result(core, g, result); - TRACE("nlsat_smt", tout << "unsat\n";); - break; - } - if (!is_decided_sat(result)) { - TRACE("nlsat_smt", tout << "not a unit\n";); - break; - } - // extract evaluation on interface variables. - // assert booleans that evaluate to true. - // assert equalities between equal interface real variables. - - model_ref mdl_nl, mdl_smt; - if (nl_mc.get()) { - model_converter2model(m, nl_mc.get(), mdl_nl); - update_eq_values(mdl_nl); - enforce_equalities(mdl_nl, m_nl_g); - - setup_assumptions(mdl_nl); - - TRACE("nlsat_smt", - model_smt2_pp(tout << "nl model\n", m, *mdl_nl.get(), 0); - m_solver->display(tout << "smt goal:\n"); tout << "\n";); - } - result.reset(); - lbool r = m_solver->check_sat(m_asms.size(), m_asms.c_ptr()); - if (r == l_false) { - // extract the core from the result - ptr_vector ecore, asms; - expr_ref_vector clause(m); - expr_ref fml(m); - get_unsat_core(ecore, asms); - - // - // assumptions should also be used for the nlsat tactic, - // but since it does not support assumptions at this time - // we overapproximate the necessary core and accumulate - // all assumptions that are ever used. - // - for (unsigned i = 0; i < asms.size(); ++i) { - m_used_asms.insert(asms[i]); - } - if (ecore.empty()) { - core2result(core, g, result); - break; - } - for (unsigned i = 0; i < ecore.size(); ++i) { - clause.push_back(mk_not(m, ecore[i])); - } - fml = mk_or(m, clause.size(), clause.c_ptr()); - m_nl_g->assert_expr(fml); - continue; - } - else if (r == l_true) { - m_solver->get_model(mdl_smt); - if (enforce_equalities(mdl_smt, m_nl_g)) { - // SMT enforced a new equality that wasn't true for nlsat. - continue; - } - TRACE("nlsat_smt", - m_fmc->display(tout << "joint state is sat\n"); - nl_mc->display(tout << "nl\n");); - if (mdl_nl.get()) { - merge_models(*mdl_nl.get(), mdl_smt); - } - mc = m_fmc.get(); - apply(mc, mdl_smt, 0); - mc = model2model_converter(mdl_smt.get()); - result.push_back(alloc(goal, m)); - } - else { - TRACE("nlsat_smt", tout << "unknown\n";); - } - break; - } - TRACE("nlsat_smt", display_result(tout, result);); - } - - void get_unsat_core(ptr_vector& core, ptr_vector& asms) { - m_solver->get_unsat_core(core); - for (unsigned i = 0; i < core.size(); ++i) { - if (m_ctx_asms_set.contains(core[i])) { - asms.push_back(core[i]); - core[i] = core.back(); - core.pop_back(); - --i; - } - } - } - - void core2result(expr_dependency_ref & lcore, goal_ref const& g, goal_ref_buffer& result) { - result.reset(); - proof * pr = nullptr; - lcore = nullptr; - g->reset(); - obj_hashtable::iterator it = m_used_asms.begin(), end = m_used_asms.end(); - for (; it != end; ++it) { - lcore = m.mk_join(lcore, m.mk_leaf(m_bool2dep.find(*it))); - } - g->assert_expr(m.mk_false(), pr, lcore); - TRACE("nlsat_smt", g->display_with_dependencies(tout);); - result.push_back(g.get()); - } - - void setup_assumptions(model_ref& mdl) { - m_asms.reset(); - m_asms.append(m_ctx_asms.size(), m_ctx_asms.c_ptr()); - app_ref_vector const& fresh_preds = m_new_preds; - expr_ref tmp(m); - for (unsigned i = 0; i < fresh_preds.size(); ++i) { - expr* pred = fresh_preds[i]; - if (mdl->eval(pred, tmp)) { - polarity_t pol = m_polarities.find(pred); - // if assumption literals are used to satisfy NL state, - // we have to assume them when satisfying SMT state - if (pol != pol_neg && m.is_false(tmp)) { - m_asms.push_back(m.mk_not(pred)); - } - else if (pol != pol_pos && m.is_true(tmp)) { - m_asms.push_back(pred); - } - } - } - for (unsigned i = 0; i < m_eq_preds.size(); ++i) { - expr* pred = m_eq_preds[i].get(); - switch (m_eq_values[i]) { - case l_true: - m_asms.push_back(pred); - break; - case l_false: - m_asms.push_back(m.mk_not(pred)); - break; - default: - break; - } - } - TRACE("nlsat_smt", - tout << "assumptions:\n" << m_asms << "\n";); - } - - bool enforce_equalities(model_ref& mdl, goal_ref const& nl_g) { - TRACE("nlsat_smt", tout << "Enforce equalities " << m_interface_cache.size() << "\n";); - bool new_equality = false; - expr_ref_vector nums(m); - obj_map num2var; - obj_map::iterator it = m_interface_cache.begin(), end = m_interface_cache.end(); - for (; it != end; ++it) { - expr_ref r(m); - expr* v, *w, *pred; - w = it->m_value; - VERIFY(mdl->eval(w, r)); - TRACE("nlsat_smt", tout << mk_pp(w, m) << " |-> " << r << "\n";); - nums.push_back(r); - if (num2var.find(r, v)) { - if (!m_eq_pairs.find(v, w, pred)) { - pred = m.mk_fresh_const(nullptr, m.mk_bool_sort()); - m_eq_preds.push_back(pred); - m_eq_values.push_back(l_true); - m_fmc->insert(to_app(pred)->get_decl()); - nl_g->assert_expr(m.mk_or(m.mk_not(pred), m.mk_eq(w, v))); - nl_g->assert_expr(m.mk_or(pred, m.mk_not(m.mk_eq(w, v)))); - m_solver->assert_expr(m.mk_iff(pred, m.mk_eq(w, v))); - new_equality = true; - m_eq_pairs.insert(v, w, pred); - } - else { - // interface equality is already enforced. - } - } - else { - num2var.insert(r, w); - } - } - return new_equality; - } - - void merge_models(model const& mdl_nl, model_ref& mdl_smt) { - expr_safe_replace num2num(m); - expr_ref result(m), val2(m); - expr_ref_vector args(m); - unsigned sz = mdl_nl.get_num_constants(); - for (unsigned i = 0; i < sz; ++i) { - func_decl* v = mdl_nl.get_constant(i); - if (u().is_real(v->get_range())) { - expr* val = mdl_nl.get_const_interp(v); - if (mdl_smt->eval(v, val2)) { - if (val != val2) { - num2num.insert(val2, val); - } - } - } - } - sz = mdl_smt->get_num_functions(); - for (unsigned i = 0; i < sz; ++i) { - func_decl* f = mdl_smt->get_function(i); - if (has_real(f)) { - unsigned arity = f->get_arity(); - func_interp* f1 = mdl_smt->get_func_interp(f); - func_interp* f2 = alloc(func_interp, m, f->get_arity()); - for (unsigned j = 0; j < f1->num_entries(); ++j) { - args.reset(); - func_entry const* entry = f1->get_entry(j); - for (unsigned k = 0; k < arity; ++k) { - translate(num2num, entry->get_arg(k), result); - args.push_back(result); - } - translate(num2num, entry->get_result(), result); - f2->insert_entry(args.c_ptr(), result); - } - translate(num2num, f1->get_else(), result); - f2->set_else(result); - mdl_smt->register_decl(f, f2); - } - } - mdl_smt->copy_const_interps(mdl_nl); - } - - bool has_real(func_decl* f) { - for (unsigned i = 0; i < f->get_arity(); ++i) { - if (u().is_real(f->get_domain(i))) return true; - } - return u().is_real(f->get_range()); - } - - void translate(expr_safe_replace& num2num, expr* e, expr_ref& result) { - result = nullptr; - if (e) { - num2num(e, result); - } - } - - void get_polarities(goal const& g) { - ptr_vector forms; - svector pols; - unsigned sz = g.size(); - for (unsigned i = 0; i < sz; ++i) { - forms.push_back(g.form(i)); - pols.push_back(pol_pos); - } - polarity_t p, q; - while (!forms.empty()) { - expr* e = forms.back(); - p = pols.back(); - forms.pop_back(); - pols.pop_back(); - if (m_polarities.find(e, q)) { - if (p == q || q == pol_dual) continue; - p = pol_dual; - } - TRACE("nlsat_smt_verbose", tout << mk_pp(e, m) << "\n";); - m_polarities.insert(e, p); - if (is_quantifier(e) || is_var(e)) { - throw tactic_exception("nl-purify tactic does not support quantifiers"); - } - SASSERT(is_app(e)); - app* a = to_app(e); - func_decl* f = a->get_decl(); - if (f->get_family_id() == m.get_basic_family_id() && p != pol_dual) { - switch(f->get_decl_kind()) { - case OP_NOT: - p = neg(p); - break; - case OP_AND: - case OP_OR: - break; - default: - p = pol_dual; - break; - } - } - else { - p = pol_dual; - } - for (unsigned i = 0; i < a->get_num_args(); ++i) { - forms.push_back(a->get_arg(i)); - pols.push_back(p); - } - } - } - - polarity_t neg(polarity_t p) { - switch (p) { - case pol_pos: return pol_neg; - case pol_neg: return pol_pos; - case pol_dual: return pol_dual; - } - return pol_dual; - } - - polarity_t join(polarity_t p, polarity_t q) { - if (p == q) return p; - return pol_dual; - } - - void rewrite_goal(rw& r, goal_ref const& g) { - r.reset(); - expr_ref new_curr(m); - proof_ref new_pr(m); - unsigned sz = g->size(); - for (unsigned i = 0; i < sz; i++) { - expr * curr = g->form(i); - r(curr, new_curr, new_pr); - if (m_produce_proofs) { - proof * pr = g->pr(i); - new_pr = m.mk_modus_ponens(pr, new_pr); - } - g->update(i, new_curr, new_pr, g->dep(i)); - } - } - - void remove_pure_arith(goal_ref const& g) { - obj_map is_pure; - unsigned sz = g->size(); - for (unsigned i = 0; i < sz; i++) { - expr * curr = g->form(i); - if (is_pure_arithmetic(is_pure, curr)) { - m_nl_g->assert_expr(curr, g->pr(i), g->dep(i)); - g->update(i, m.mk_true(), g->pr(i), g->dep(i)); - } - } - } - - bool is_pure_arithmetic(obj_map& is_pure, expr* e0) { - ptr_vector todo; - todo.push_back(e0); - while (!todo.empty()) { - expr* e = todo.back(); - if (is_pure.contains(e)) { - todo.pop_back(); - continue; - } - if (!is_app(e)) { - todo.pop_back(); - is_pure.insert(e, false); - continue; - } - app* a = to_app(e); - bool pure = false, all_found = true, p; - pure |= (a->get_family_id() == u().get_family_id()) && u().is_real(a); - pure |= (m.is_eq(e) && u().is_real(a->get_arg(0))); - pure |= (a->get_family_id() == u().get_family_id()) && m.is_bool(a) && u().is_real(a->get_arg(0)); - pure |= (a->get_family_id() == m.get_basic_family_id()); - pure |= is_uninterp_const(a) && u().is_real(a); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - if (!is_pure.find(a->get_arg(i), p)) { - todo.push_back(a->get_arg(i)); - all_found = false; - } - else { - pure &= p; - } - } - if (all_found) { - is_pure.insert(e, pure); - todo.pop_back(); - } - } - return is_pure.find(e0); - } - -public: - - nl_purify_tactic(ast_manager & m, params_ref const& p): - m(m), - m_util(m), - m_params(p), - m_fmc(nullptr), - m_nl_tac(mk_nlsat_tactic(m, p)), - m_nl_g(nullptr), - m_solver(mk_smt_solver(m, p, symbol::null)), - m_eq_preds(m), - m_new_reals(m), - m_new_preds(m), - m_asms(m) - {} - - ~nl_purify_tactic() override {} - - void updt_params(params_ref const & p) override { - m_params = p; - } - - tactic * translate(ast_manager& m) override { - return alloc(nl_purify_tactic, m, m_params); - } - - void collect_statistics(statistics & st) const override { - m_nl_tac->collect_statistics(st); - m_solver->collect_statistics(st); - } - - void reset_statistics() override { - m_nl_tac->reset_statistics(); - } - - - void cleanup() override { - m_solver = mk_smt_solver(m, m_params, symbol::null); - m_nl_tac->cleanup(); - m_eq_preds.reset(); - m_eq_values.reset(); - m_new_reals.reset(); - m_new_preds.reset(); - m_eq_pairs.reset(); - m_polarities.reset(); - m_ctx_asms.reset(); - m_ctx_asms_set.reset(); - m_used_asms.reset(); - m_bool2dep.reset(); - } - - void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) override { - - tactic_report report("qfufnl-purify", *g); - TRACE("nlsat_smt", g->display(tout);); - - m_produce_proofs = g->proofs_enabled(); - mc = nullptr; pc = nullptr; core = nullptr; - - fail_if_proof_generation("qfufnra-purify", g); - // fail_if_unsat_core_generation("qfufnra-purify", g); - rw r(*this); - expr_ref_vector clauses(m); - m_nl_g = alloc(goal, m, true, false); - m_fmc = alloc(filter_model_converter, m); - - // first hoist interface variables, - // then annotate subformulas by polarities, - // finally extract polynomial inequalities by - // creating a place-holder predicate inside the - // original goal and extracting pure nlsat clauses. - r.set_interface_var_mode(); - rewrite_goal(r, g); - if (!g->unsat_core_enabled()) { - remove_pure_arith(g); - } - get_polarities(*g.get()); - r.set_bool_mode(); - rewrite_goal(r, g); - - extract_clauses_and_dependencies(g, clauses, m_ctx_asms, m_bool2dep, m_fmc); - - TRACE("nlsat_smt", tout << clauses << "\n";); - - for (unsigned i = 0; i < m_ctx_asms.size(); ++i) { - m_ctx_asms_set.insert(m_ctx_asms[i]); - } - - for (unsigned i = 0; i < clauses.size(); ++i) { - m_solver->assert_expr(clauses[i].get()); - } - g->inc_depth(); - solve(g, result, core, mc); - } -}; - - -tactic * mk_nl_purify_tactic(ast_manager& m, params_ref const& p) { - return alloc(nl_purify_tactic, m, p); -} diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 92cc7315f..dd6557dcc 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -78,7 +78,6 @@ protected: friend class nary_tactical; friend class binary_tactical; friend class unary_tactical; - friend class nl_purify_tactic; }; From 742efd5104c67c045172d880154c29b04c133ee7 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 3 Dec 2018 12:32:45 +0700 Subject: [PATCH 12/13] Remove undef max/min on macOS. This is no longer needed. --- src/util/trace.h | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/util/trace.h b/src/util/trace.h index 1a245036f..77c66afd4 100644 --- a/src/util/trace.h +++ b/src/util/trace.h @@ -24,10 +24,6 @@ Revision History: #undef max #undef min #endif -#ifdef __APPLE__ -#undef max -#undef min -#endif #include #ifdef _TRACE From a0264c08a872ddb83230be49fc501ae14429797b Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 3 Dec 2018 22:15:14 +0700 Subject: [PATCH 13/13] Windows builds need immintrin.h Fixes issue #2006. --- src/util/mpz.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 47c88560c..af95e1a2a 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -45,6 +45,11 @@ Revision History: #define LEHMER_GCD #endif +#ifdef _WINDOWS +// This is needed for _tzcnt_u32 and friends. +#include +#endif + #if defined(__GNUC__) #define _trailing_zeros32(X) __builtin_ctz(X) #else