diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 207ac4c8c..ac9122335 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1746,7 +1746,6 @@ def mk_config(): 'OBJ_EXT=.obj\n' 'LIB_EXT=.lib\n' 'AR=lib\n' - 'AR_FLAGS=/nologo /LTCG\n' 'AR_OUTFLAG=/OUT:\n' 'EXE_EXT=.exe\n' 'LINK=cl\n' @@ -1765,23 +1764,25 @@ def mk_config(): extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) if DEBUG_MODE: config.write( + 'AR_FLAGS=/nologo\n' 'LINK_FLAGS=/nologo /MDd\n' 'SLINK_FLAGS=/nologo /LDd\n') if not VS_X64: config.write( - 'CXXFLAGS=/c /GL /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) + 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) config.write( - 'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') + 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' + 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: config.write( - 'CXXFLAGS=/c /GL /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) + 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) config.write( - 'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') + 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' + 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: # Windows Release mode config.write( + 'AR_FLAGS=/nologo /LTCG\n' 'LINK_FLAGS=/nologo /MD\n' 'SLINK_FLAGS=/nologo /LD\n') if TRACE: diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp index 7d5a23d99..0b2977a22 100644 --- a/src/math/polynomial/upolynomial_factorization.cpp +++ b/src/math/polynomial/upolynomial_factorization.cpp @@ -719,12 +719,11 @@ void hensel_lift_quadratic(z_manager& upm, numeral_vector const & C, // we create a new Z_p manager, since we'll be changing the input one zp_manager zp_upm(nm); zp_upm.set_zp(zpe_upm.m().p()); - zp_numeral_manager & zp_nm = zp_upm.m(); // get the U, V, such that A*U + B*V = 1 (mod p) scoped_mpz_vector U(nm), V(nm), D(nm); zp_upm.ext_gcd(A.size(), A.c_ptr(), B.size(), B.c_ptr(), U, V, D); - SASSERT(D.size() == 1 && zp_nm.is_one(D[0])); + SASSERT(D.size() == 1 && zp_upm.m().is_one(D[0])); // we start lifting from (a = p, b = p, r = p) scoped_mpz_vector A_lifted(nm), B_lifted(nm); diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 1567dff4f..58bc79e7a 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -89,8 +89,8 @@ public: :m_eof(false), m_eof_behind_buffer(false), m_next_index(0), - m_data_size(0), - m_ok(true) { + m_ok(true), + m_data_size(0) { m_data.resize(2*s_expansion_step); resize_data(0); #if _WINDOWS diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 30509d6bf..134c0746d 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -150,9 +150,9 @@ namespace pdr { } datalog::rule const& pred_transformer::find_rule(model_core const& model) const { - datalog::rule_manager& rm = ctx.get_context().get_rule_manager(); obj_map::iterator it = m_tag2rule.begin(), end = m_tag2rule.end(); TRACE("pdr_verbose", + datalog::rule_manager& rm = ctx.get_context().get_rule_manager(); for (; it != end; ++it) { expr* pred = it->m_key; tout << mk_pp(pred, m) << ":\n"; @@ -1137,9 +1137,6 @@ namespace pdr { if (n->get_model_ptr()) { models.insert(n->state(), n->get_model_ptr()); rules.insert(n->state(), n->get_rule()); - //pred_transformer& pt = n->pt(); - //context& ctx = pt.get_context(); - //datalog::context& dctx = ctx.get_context(); } todo.pop_back(); todo.append(n->children().size(), n->children().c_ptr()); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 3cae51bc2..857b57296 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1343,7 +1343,6 @@ namespace opt { break; } case O_MAXSMT: { - maxsmt& ms = *m_maxsmts.find(obj.m_id); rational value(0); for (unsigned i = 0; i < obj.m_terms.size(); ++i) { VERIFY(m_model->eval(obj.m_terms[i], val)); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 4f268268d..d505a9ffb 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -41,9 +41,9 @@ namespace opt { m_params(p), m_context(mgr, m_params), m(mgr), - m_dump_benchmarks(false), m_fm(fm), m_objective_sorts(m), + m_dump_benchmarks(false), m_first(true) { m_params.updt_params(p); m_params.m_relevancy_lvl = 0; diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index 971c7af57..9b84654b9 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -631,7 +631,6 @@ public: m(m), m_util(m), m_params(p), - m_produce_proofs(false), m_fmc(0), m_cancel(false), m_nl_tac(mk_nlsat_tactic(m, p)), diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h index 2da99cca5..e1060a7b0 100644 --- a/src/util/inf_rational.h +++ b/src/util/inf_rational.h @@ -63,10 +63,7 @@ class inf_rational { return s; } - inf_rational(): - m_first(rational()), - m_second(rational()) - {} + inf_rational() {} inf_rational(const inf_rational & r): m_first(r.m_first), diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 122db7217..743038972 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -24,9 +24,9 @@ Revision History: #endif synch_mpq_manager * rational::g_mpq_manager = 0; -rational rational::m_zero(0); -rational rational::m_one(1); -rational rational::m_minus_one(-1); +rational rational::m_zero; +rational rational::m_one; +rational rational::m_minus_one; vector rational::m_powers_of_two; void mk_power_up_to(vector & pws, unsigned n) { @@ -56,11 +56,17 @@ rational rational::power_of_two(unsigned k) { void rational::initialize() { if (!g_mpq_manager) { g_mpq_manager = alloc(synch_mpq_manager); + m().set(m_zero.m_val, 0); + m().set(m_one.m_val, 1); + m().set(m_minus_one.m_val, -1); } } void rational::finalize() { m_powers_of_two.finalize(); + m_zero.~rational(); + m_one.~rational(); + m_minus_one.~rational(); dealloc(g_mpq_manager); g_mpq_manager = 0; }