mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

disable local optimization in presence of non-linear constraints, addresses issue #758

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-23 21:45:35 -07:00
parent b476784f23
commit 4f3f21bff1
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_arith_aux.h
View file

@ -1056,6 +1056,11 @@ namespace smt {
inf_eps_rational<inf_rational> theory_arith<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shared) { inf_eps_rational<inf_rational> theory_arith<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
TRACE("bound_bug", display_var(tout, v); display(tout);); TRACE("bound_bug", display_var(tout, v); display(tout););
has_shared = false; has_shared = false;
if (!m_nl_monomials.empty()) {
has_shared = true;
blocker = mk_gt(v);
return inf_eps_rational<inf_rational>(get_value(v));
}
max_min_t r = max_min(v, true, true, has_shared); max_min_t r = max_min(v, true, true, has_shared);
if (r == UNBOUNDED) { if (r == UNBOUNDED) {
has_shared = false; has_shared = false;
@ -1300,6 +1305,7 @@ namespace smt {
*/ */
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::pick_var_to_leave( bool theory_arith<Ext>::pick_var_to_leave(
@ -1331,7 +1337,7 @@ namespace smt {
if (update_gains(inc, s, coeff_ij, min_gain, max_gain) || if (update_gains(inc, s, coeff_ij, min_gain, max_gain) ||
(x_i == null_theory_var && !unbounded_gain(max_gain))) { (x_i == null_theory_var && !unbounded_gain(max_gain))) {
x_i = s; x_i = s;
a_ij = coeff_ij; a_ij = coeff_ij;
} }
has_shared |= ctx.is_shared(get_enode(s)); has_shared |= ctx.is_shared(get_enode(s));
} }