mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
move fixed variable propagation to nla_core/monomial_bounds
This commit is contained in:
parent
f3e7c8c9df
commit
c01336553e
|
@ -16,7 +16,15 @@ namespace nla {
|
|||
|
||||
monomial_bounds::monomial_bounds(core* c):
|
||||
common(c),
|
||||
dep(c->m_intervals.get_dep_intervals()) {}
|
||||
dep(c->m_intervals.get_dep_intervals()) {
|
||||
|
||||
std::function<void(lpvar v)> fixed_eh = [&](lpvar v) {
|
||||
c->trail().push(push_back_vector(m_fixed_var_trail));
|
||||
m_fixed_var_trail.push_back(v);
|
||||
};
|
||||
// uncomment to enable:
|
||||
// c->lra.m_fixed_var_eh = fixed_eh;
|
||||
}
|
||||
|
||||
void monomial_bounds::propagate() {
|
||||
for (lpvar v : c().m_to_refine) {
|
||||
|
@ -24,6 +32,46 @@ namespace nla {
|
|||
if (add_lemma())
|
||||
break;
|
||||
}
|
||||
propagate_fixed_vars();
|
||||
}
|
||||
|
||||
void monomial_bounds::propagate_fixed_vars() {
|
||||
if (m_fixed_var_qhead == m_fixed_var_trail.size())
|
||||
return;
|
||||
c().trail().push(value_trail(m_fixed_var_qhead));
|
||||
while (m_fixed_var_qhead < m_fixed_var_trail.size())
|
||||
propagate_fixed_var(m_fixed_var_trail[m_fixed_var_qhead++]);
|
||||
}
|
||||
|
||||
void monomial_bounds::propagate_fixed_var(lpvar v) {
|
||||
SASSERT(c().var_is_fixed(v));
|
||||
TRACE("nla_solver", tout << "propagate fixed var: " << c().var_str(v) << "\n";);
|
||||
for (auto const& m : c().emons().get_use_list(v))
|
||||
propagate_fixed_var(m, v);
|
||||
}
|
||||
|
||||
void monomial_bounds::propagate_fixed_var(monic const& m, lpvar v) {
|
||||
unsigned num_free = 0;
|
||||
lpvar free_var = null_lpvar;
|
||||
for (auto w : m)
|
||||
if (!c().var_is_fixed(w))
|
||||
++num_free, free_var = w;
|
||||
if (num_free != 1)
|
||||
return;
|
||||
u_dependency* d = nullptr;
|
||||
auto& lra = c().lra;
|
||||
lp::mpq coeff(1);
|
||||
for (auto w : m) {
|
||||
if (c().var_is_fixed(w)) {
|
||||
d = lra.join_deps(d, lra.join_deps(lra.get_column_lower_bound_witness(w), lra.get_column_upper_bound_witness(w)));
|
||||
coeff += lra.get_column_value(w).x;
|
||||
}
|
||||
}
|
||||
vector<std::pair<lp::mpq, lpvar>> coeffs;
|
||||
coeffs.push_back({coeff, free_var});
|
||||
coeffs.push_back({mpq(-1), v});
|
||||
lpvar j = lra.add_term(coeffs, UINT_MAX);
|
||||
lra.update_column_type_and_bound(j, llc::EQ, mpq(0), d);
|
||||
}
|
||||
|
||||
bool monomial_bounds::is_too_big(mpq const& q) const {
|
||||
|
|
|
@ -43,6 +43,13 @@ namespace nla {
|
|||
bool is_linear(monic const& m, lpvar& w, lpvar & fixed_to_zero);
|
||||
rational fixed_var_product(monic const& m, lpvar w);
|
||||
lpvar non_fixed_var(monic const& m);
|
||||
|
||||
// fixed variable propagation
|
||||
unsigned m_fixed_var_qhead = 0;
|
||||
unsigned_vector m_fixed_var_trail;
|
||||
void propagate_fixed_vars();
|
||||
void propagate_fixed_var(lpvar v);
|
||||
void propagate_fixed_var(monic const& m, lpvar v);
|
||||
public:
|
||||
monomial_bounds(core* core);
|
||||
void propagate();
|
||||
|
|
|
@ -100,11 +100,15 @@ class core {
|
|||
nra::solver m_nra;
|
||||
bool m_cautious_patching = true;
|
||||
lpvar m_patched_var = 0;
|
||||
monic const* m_patched_monic = nullptr;
|
||||
monic const* m_patched_monic = nullptr;
|
||||
|
||||
|
||||
|
||||
void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
|
||||
void add_bounds();
|
||||
|
||||
|
||||
|
||||
public:
|
||||
// constructor
|
||||
core(lp::lar_solver& s, params_ref const& p, reslimit&);
|
||||
|
|
|
@ -254,45 +254,6 @@ class theory_lra::imp {
|
|||
return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int);
|
||||
}
|
||||
|
||||
svector<theory_var> m_fixed_vars;
|
||||
unsigned m_fixed_vars_head = 0;
|
||||
|
||||
bool propagate_fixed_vars() {
|
||||
if (m_fixed_vars_head == m_fixed_vars.size())
|
||||
return false;
|
||||
ctx().push_trail(value_trail(m_fixed_vars_head));
|
||||
bool propagated = false;
|
||||
while (m_fixed_vars_head < m_fixed_vars.size()) {
|
||||
theory_var v = m_fixed_vars[m_fixed_vars_head++];
|
||||
enode* n = th.get_enode(v);
|
||||
for (enode* p : n->get_parents()) {
|
||||
expr* e = p->get_expr();
|
||||
expr* x, * y;
|
||||
if (!a.is_mul(e, x, y))
|
||||
continue;
|
||||
if (a.is_numeral(x) || a.is_numeral(y))
|
||||
continue;
|
||||
if (x == n->get_expr())
|
||||
std::swap(x, y);
|
||||
if (y != n->get_expr())
|
||||
continue;
|
||||
|
||||
// comment out to enable propagation:
|
||||
continue;
|
||||
|
||||
expr_ref k(a.mk_numeral(get_value(v), a.is_int(y)), m);
|
||||
literal eq1 = th.mk_eq(y, k, false);
|
||||
literal eq2 = th.mk_eq(e, a.mk_mul(x, k), false);
|
||||
ctx().mk_th_axiom(get_id(), ~eq1, eq2);
|
||||
|
||||
// v2 could perform propagation directly
|
||||
// v3 could consider multiplication of more than two variables.
|
||||
// such as e := x * y * z. If both x, y become fixed we have e = z * value(x) * value(y)
|
||||
// verbose_stream() << mk_bounded_pp(e, m) << " - " << mk_bounded_pp(n->get_expr(), m) << "\n";
|
||||
}
|
||||
}
|
||||
return propagated;
|
||||
}
|
||||
void ensure_nla() {
|
||||
if (!m_nla) {
|
||||
m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit());
|
||||
|
@ -913,18 +874,6 @@ public:
|
|||
lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test;
|
||||
lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
|
||||
m_lia = alloc(lp::int_solver, *m_solver.get());
|
||||
|
||||
std::function<void(lpvar)> new_fixed = [&](lpvar v) {
|
||||
theory_var u = lp().local_to_external(v);
|
||||
if (u == null_theory_var)
|
||||
return;
|
||||
expr* var = th.get_expr(u);
|
||||
if (a.is_numeral(var))
|
||||
return;
|
||||
m_fixed_vars.push_back(u);
|
||||
ctx().push_trail(push_back_vector(m_fixed_vars));
|
||||
};
|
||||
lp().m_fixed_var_eh = new_fixed;
|
||||
}
|
||||
|
||||
void internalize_is_int(app * n) {
|
||||
|
@ -2135,7 +2084,7 @@ public:
|
|||
}
|
||||
|
||||
bool propagate() {
|
||||
return process_atoms() && propagate_core() && propagate_fixed_vars();
|
||||
return process_atoms() && propagate_core();
|
||||
}
|
||||
|
||||
bool propagate_core() {
|
||||
|
|
Loading…
Reference in a new issue