diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ac9122335..b51143ff2 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -85,6 +85,7 @@ VS_PAR=False VS_PAR_NUM=8 GPROF=False GIT_HASH=False +OPTIMIZE=False FPMATH="Default" FPMATH_FLAGS="-mfpmath=sse -msse -msse2" @@ -551,6 +552,8 @@ def display_help(exit_code): print(" -v, --vsproj generate Visual Studio Project Files.") if IS_WINDOWS: print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.") + if IS_WINDOWS: + print(" --optimize generate optimized code during linking.") print(" -j, --java generate Java bindings.") print(" --ml generate OCaml bindings.") print(" --staticlib build Z3 static library.") @@ -577,13 +580,13 @@ def display_help(exit_code): def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH - global LINUX_X64 + global LINUX_X64, OPTIMIZE try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof', - 'githash=', 'x86', 'ml']) + 'githash=', 'x86', 'ml', 'optimize']) except: print("ERROR: Invalid command line option") display_help(1) @@ -618,6 +621,8 @@ def parse_options(): DOTNET_ENABLED = False elif opt in ('--staticlib'): STATIC_LIB = True + elif opt in ('--optimize'): + OPTIMIZE = True elif not IS_WINDOWS and opt in ('-p', '--prefix'): PREFIX = arg PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages') @@ -1781,8 +1786,9 @@ def mk_config(): '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 + if OPTIMIZE: + config.write('AR_FLAGS=/nologo /LTCG\n') config.write( - 'AR_FLAGS=/nologo /LTCG\n' 'LINK_FLAGS=/nologo /MD\n' 'SLINK_FLAGS=/nologo /LD\n') if TRACE: diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 826d95ef0..660a11faa 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -882,10 +882,10 @@ namespace smt { template void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v); enum max_min_t { UNBOUNDED, AT_BOUND, OPTIMIZED, BEST_EFFORT}; - max_min_t max_min(theory_var v, bool max, bool& has_shared); + max_min_t max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared); bool max_min(svector const & vars); - max_min_t max_min(row& r, bool max, bool& has_shared); + max_min_t max_min(row& r, bool max, bool maintain_integrality, bool& has_shared); bool unbounded_gain(inf_numeral const & max_gain) const; bool safe_gain(inf_numeral const& min_gain, inf_numeral const & max_gain) const; void normalize_gain(numeral const& divisor, inf_numeral & max_gain) const; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 0e4eba822..91ee6def5 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1133,7 +1133,7 @@ namespace smt { inf_eps_rational theory_arith::maximize(theory_var v, expr_ref& blocker, bool& has_shared) { TRACE("bound_bug", display_var(tout, v); display(tout);); has_shared = false; - max_min_t r = max_min(v, true, has_shared); + max_min_t r = max_min(v, true, true, has_shared); if (r == UNBOUNDED) { has_shared = false; blocker = get_manager().mk_false(); @@ -1553,13 +1553,14 @@ namespace smt { typename theory_arith::max_min_t theory_arith::max_min( row & r, bool max, + bool maintain_integrality, bool& has_shared) { m_stats.m_max_min++; unsigned best_efforts = 0; bool inc = false; context& ctx = get_context(); - SASSERT(valid_assignment()); + SASSERT(!maintain_integrality || valid_assignment()); numeral a_ij, curr_a_ij, coeff, curr_coeff; inf_numeral min_gain, max_gain, curr_min_gain, curr_max_gain; @@ -1633,7 +1634,7 @@ namespace smt { if (x_j == null_theory_var) { TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";); - SASSERT(valid_assignment()); + SASSERT(!maintain_integrality || valid_assignment()); result = OPTIMIZED; break; } @@ -1648,7 +1649,7 @@ namespace smt { SASSERT(!unbounded_gain(max_gain)); update_value(x_j, max_gain); TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";); - SASSERT(valid_assignment()); + SASSERT(!maintain_integrality || valid_assignment()); continue; } if (!inc && lower(x_j)) { @@ -1656,7 +1657,7 @@ namespace smt { max_gain.neg(); update_value(x_j, max_gain); TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";); - SASSERT(valid_assignment()); + SASSERT(!maintain_integrality || valid_assignment()); continue; } if (ctx.is_shared(get_enode(x_j))) { @@ -1681,7 +1682,7 @@ namespace smt { TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";); } update_value(x_j, max_gain); - SASSERT(valid_assignment()); + SASSERT(!maintain_integrality || valid_assignment()); continue; } @@ -1709,7 +1710,7 @@ namespace smt { coeff.neg(); add_tmp_row(r, coeff, r2); SASSERT(r.get_idx_of(x_j) == -1); - SASSERT(valid_assignment()); + SASSERT(!maintain_integrality || valid_assignment()); } TRACE("opt", display(tout);); return (best_efforts>0)?BEST_EFFORT:result; @@ -1781,10 +1782,10 @@ namespace smt { \brief Maximize/Minimize the given variable. The bounds of v are update if procedure succeeds. */ template - typename theory_arith::max_min_t theory_arith::max_min(theory_var v, bool max, bool& has_shared) { + typename theory_arith::max_min_t theory_arith::max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared) { expr* e = get_enode(v)->get_owner(); - SASSERT(valid_assignment()); + SASSERT(!maintain_integrality || valid_assignment()); SASSERT(!is_quasi_base(v)); if ((max && at_upper(v)) || (!max && at_lower(v))) { TRACE("opt", tout << "At bound: " << mk_pp(e, get_manager()) << "...\n";); @@ -1803,7 +1804,7 @@ namespace smt { add_tmp_row_entry(m_tmp_row, it->m_coeff, it->m_var); } } - max_min_t r = max_min(m_tmp_row, max, has_shared); + max_min_t r = max_min(m_tmp_row, max, maintain_integrality, has_shared); if (r == OPTIMIZED) { TRACE("opt", tout << mk_pp(e, get_manager()) << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n"; display_row(tout, m_tmp_row, true); display_row_info(tout, m_tmp_row);); @@ -1830,9 +1831,9 @@ namespace smt { svector::const_iterator it = vars.begin(); svector::const_iterator end = vars.end(); for (; it != end; ++it) { - if (max_min(*it, true, has_shared) == OPTIMIZED && !has_shared) + if (max_min(*it, true, false, has_shared) == OPTIMIZED && !has_shared) succ = true; - if (max_min(*it, false, has_shared) == OPTIMIZED && !has_shared) + if (max_min(*it, false, false, has_shared) == OPTIMIZED && !has_shared) succ = true; } if (succ) { diff --git a/src/smt/theory_arith_inv.h b/src/smt/theory_arith_inv.h index 007c8025f..9c56ea367 100644 --- a/src/smt/theory_arith_inv.h +++ b/src/smt/theory_arith_inv.h @@ -214,10 +214,13 @@ namespace smt { template bool theory_arith::valid_assignment() const { - return - valid_row_assignment() && + if (valid_row_assignment() && satisfy_bounds() && - satisfy_integrality(); + satisfy_integrality()) { + return true; + } + TRACE("arith", display(tout);); + return false; } #endif diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 8ff122c1e..c2322fce2 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -2371,7 +2371,7 @@ namespace smt { return FC_CONTINUE; } - if (!max_min_nl_vars()) + if (!max_min_nl_vars()) return FC_CONTINUE; if (check_monomial_assignments()) { diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp index e276d1792..9c02b5f0f 100644 --- a/src/tactic/arith/probe_arith.cpp +++ b/src/tactic/arith/probe_arith.cpp @@ -549,9 +549,10 @@ struct is_non_qfufnra_functor { case OP_IRRATIONAL_ALGEBRAIC_NUM: return; case OP_MUL: - if (n->get_num_args() == 2 || - (!u.is_numeral(n->get_arg(0)) && - !u.is_numeral(n->get_arg(1)))) { + if (n->get_num_args() == 2 && + u.is_real(n->get_arg(0)) && + !u.is_numeral(n->get_arg(0)) && + !u.is_numeral(n->get_arg(1))) { m_has_nonlinear = true; } return; diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index 9b84654b9..ec150453d 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -311,16 +311,17 @@ private: // assert equalities between equal interface real variables. model_ref mdl_nl, mdl_smt; - 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";); - + if (mdl_nl.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) { @@ -352,7 +353,9 @@ private: TRACE("nlsat_smt", m_fmc->display(tout << "joint state is sat\n"); nl_mc->display(tout << "nl\n");); - merge_models(*mdl_nl.get(), mdl_smt); + 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());