diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 18be79e50..d19aeb60b 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -269,63 +269,6 @@ struct solver::imp { return static_cast(-1) != j; } - - // Return 0 if the var has to to have a zero value, - // -1 if the monomial has to be negative - // 1 if positive. - // If strict is true on the entrance then it can be set to false, - // otherwise it remains false - // Returns 2 if the sign is not defined. - int get_mon_sign_zero_var(unsigned j, bool & strict) { - if (m_monomials_containing_var.find(j) == m_monomials_containing_var.end()) - return 2; - lpci lci = -1; - lpci uci = -1; - rational lb, ub; - bool lower_is_strict; - bool upper_is_strict; - m_lar_solver.has_lower_bound(j, lci, lb, lower_is_strict); - m_lar_solver.has_upper_bound(j, uci, ub, upper_is_strict); - - if (is_set(uci) && is_set(lci) && ub == lb) { - if (ub.is_zero()){ - m_expl->clear(); - m_expl->push_justification(uci); - m_expl->push_justification(lci); - return 0; - } - m_expl->push_justification(uci); - m_expl->push_justification(lci); - return ub.is_pos() ? 1 : -1; - } - - if (is_set(uci)) { - if (ub.is_neg()) { - m_expl->push_justification(uci); - return -1; - } - if (ub.is_zero()) { - strict = false; - m_expl->push_justification(uci); - return -1; - } - } - - if (is_set(lci)) { - if (lb.is_pos()) { - m_expl->push_justification(lci); - return 1; - } - if (lb.is_zero()) { - strict = false; - m_expl->push_justification(lci); - return 1; - } - } - - return 2; // the sign of the variable is not defined - } - bool var_is_fixed_to_zero(lpvar j) const { return m_lar_solver.column_has_upper_bound(j) && @@ -381,78 +324,7 @@ struct solver::imp { out << "\n"; return out; } - /** - * \brief - */ - bool get_one_of_var(lpvar j, rational & sign) { - lpci lci; - lpci uci; - rational lb, ub; - bool is_strict; - if (!m_lar_solver.has_lower_bound(j, lci, lb, is_strict)) - return false; - SASSERT(!is_strict); - if (!m_lar_solver.has_upper_bound(j, uci, ub, is_strict)) - return false; - SASSERT(!is_strict); - - if (ub == lb) { - if (ub == rational(1)) { - sign = rational(1); - } - else if (ub == -rational(1)) { - sign = rational(-1); - } - else - return false; - return true; - } - return false; - } - - vector get_ones_of_monomimal(const svector & vars) { - TRACE("nla_solver", tout << "get_ones_of_monomimal";); - vector ret; - for (unsigned i = 0; i < vars.size(); i++) { - mono_index_with_sign mi; - if (get_one_of_var(vars[i], mi.m_sign)) { - mi.m_i = i; - ret.push_back(mi); - } - } - return ret; - } - - void get_large_and_small_indices_of_monomimal(const monomial& m, - unsigned_vector & large, - unsigned_vector & _small) { - - for (unsigned i = 0; i < m.size(); ++i) { - unsigned j = m.vars()[i]; - lp::constraint_index lci = -1, uci = -1; - rational lb, ub; - bool is_strict; - if (m_lar_solver.has_lower_bound(j, lci, lb, is_strict)) { - SASSERT(!is_strict); - if (lb >= rational(1)) { - large.push_back(i); - } - } - if (m_lar_solver.has_upper_bound(j, uci, ub, is_strict)) { - SASSERT(!is_strict); - if (ub <= -rational(1)) { - large.push_back(i); - } - } - - if (is_set(lci) && is_set(uci) && -rational(1) <= lb && ub <= rational(1)) { - _small.push_back(i); - } - } - } - - // returns true if found bool find_monomial_of_vars(const svector& vars, monomial& m, rational & sign) const { auto it = m_rooted_monomials.find(vars); @@ -466,225 +338,6 @@ struct solver::imp { return true; } - bool find_complimenting_monomial(const svector & vars, lpvar & j) { - monomial m; - rational other_sign; - if (!find_monomial_of_vars(vars, m, other_sign)) { - return false; - } - j = m.var(); - return true; - } - - bool find_lpvar_and_sign_with_wrong_val( - const monomial& m, - svector & vars, - const rational& v, - rational sign, - lpvar& j) { - rational other_sign; - monomial mn; - if (!find_monomial_of_vars(vars, mn, other_sign)) { - return false; - } - sign *= other_sign; - j = mn.var(); - rational other_val = m_lar_solver.get_column_value_rational(j); - return sign * other_val != v; - } - - void add_explanation_of_large_value(lpvar j, expl_set & expl) { - lpci ci; - rational b; - bool strict; - if (m_lar_solver.has_lower_bound(j, ci, b, strict) && rational(1) <= b) { - expl.insert(ci); - } else if (m_lar_solver.has_upper_bound(j, ci, b, strict)) { - SASSERT(b <= rational(-1)); - expl.insert(ci); - } else { - UNREACHABLE(); - } - } - - void add_explanation_of_small_value(lpvar j, expl_set & expl) { - lpci ci; - rational b; - bool strict; - m_lar_solver.has_lower_bound(j, ci, b, strict); - SASSERT(b >= -rational(1)); - expl.insert(ci); - m_lar_solver.has_upper_bound(j, ci, b, strict); - SASSERT(b <= rational(1)); - expl.insert(ci); - } - - void large_lemma_for_proportion_case_on_known_signs(const monomial& m, - unsigned j, - int mon_sign, - int j_sign) { - // Imagine that the signs are all positive and flip them afterwards. - // For this case we would have x[j] < 0 || x[m.var()] < 0 || x[m.var] >= x[j] - // But for the general case we have - // j_sign * x[j] < 0 || mon_sign * x[m.var()] < 0 || mon_sign * x[m.var()] >= j_sign * x[j] - // the first literal - mk_ineq(rational(j_sign), j, lp::lconstraint_kind::LT); - mk_ineq(rational(mon_sign), m.var(), lp::lconstraint_kind::LT); - // the third literal - mk_ineq(rational(mon_sign), m.var(), - rational(j_sign), j, lp::lconstraint_kind::GE); - } - - bool large_lemma_for_proportion_case(const monomial& m, const svector & mask, - const unsigned_vector & large, unsigned j) { - TRACE("nla_solver", ); - const rational j_val = m_lar_solver.get_column_value_rational(j); - const rational m_val = m_lar_solver.get_column_value_rational(m.var()); - const rational m_abs_val = lp::abs(m_lar_solver.get_column_value_rational(m.var())); - // since the abs of masked factor is greater than or equal to one - // j_val has to be less than or equal to m_abs_val - int j_sign = j_val < - m_abs_val? -1: (j_val > m_abs_val)? 1: 0; - if (j_sign == 0) // abs(j_val) <= abs(m_val) which is not a conflict - return false; - expl_set expl; - add_explanation_of_reducing_to_rooted_monomial(m, expl); - for (unsigned k = 0; k < mask.size(); k++) { - if (mask[k] == 1) - add_explanation_of_large_value(m.vars()[large[k]], expl); - } - m_expl->clear(); - m_expl->add(expl); - int mon_sign = m_val < rational(0) ? -1 : 1; - large_lemma_for_proportion_case_on_known_signs(m, j, mon_sign, j_sign); - return true; - } - - bool small_lemma_for_proportion_case(const monomial& m, const svector & mask, - const unsigned_vector & _small, unsigned j) { - TRACE("nla_solver", ); - const rational j_val = m_lar_solver.get_column_value_rational(j); - const rational m_val = m_lar_solver.get_column_value_rational(m.var()); - const rational m_abs_val = lp::abs(m_lar_solver.get_column_value_rational(m.var())); - // since the abs of the masked factor is less than or equal to one - // j_val has to be greater than or equal to m_abs_val - if (j_val <= - m_abs_val || j_val > m_abs_val) - return false; - - expl_set expl; - add_explanation_of_reducing_to_rooted_monomial(m, expl); - for (unsigned k = 0; k < mask.size(); k++) { - if (mask[k] == 1) - add_explanation_of_small_value(m.vars()[_small[k]], expl); - } - m_expl->clear(); - m_expl->add(expl); - int mon_sign = m_val < rational(0) ? -1 : 1; - int j_sign = j_val >= rational(0)? 1: -1; - small_lemma_for_proportion_case_on_known_signs(m, j, mon_sign, j_sign); - return true; - } - - // It is the case where |x[j]| >= |x[m.var()]| should hold in the model, but it does not. - void small_lemma_for_proportion_case_on_known_signs(const monomial& m, unsigned j, int mon_sign, int j_sign) { - // Imagine that the signs are all positive. - // For this case we would have x[j] < 0 || x[m.var()] < 0 || x[j] >= x[m.var()] - // But for the general case we have - // j_sign * x[j] < 0 || mon_sign * x[m.var()] < 0 || j_sign * x[j] >= mon_sign * x[m.var] - - mk_ineq(rational(j_sign), j, lp::lconstraint_kind::LT); - mk_ineq(rational(mon_sign), m.var(), lp::lconstraint_kind::LT); - mk_ineq(rational(j_sign), j, -rational(mon_sign), m.var(), lp::lconstraint_kind::GE); - } - - bool large_basic_lemma_for_mon_proportionality(unsigned i_mon, const unsigned_vector& large) { - svector mask(large.size(), false); // init mask by false - const auto & m = m_monomials[i_mon]; - rational sign; - auto vars = reduce_monomial_to_rooted(m.vars(), sign); - auto vars_copy = vars; - auto v = lp::abs(m_lar_solver.get_column_value_rational(m.var())); - // We cross out from vars the "large" variables represented by the mask - for (unsigned k = 0; k < mask.size(); k++) { - if (mask[k]) { - mask[k] = true; - TRACE("nla_solver", tout << "large[" << k << "] = " << large[k];); - SASSERT(std::find(vars.begin(), vars.end(), vars_copy[large[k]]) != vars.end()); - vars.erase(vars_copy[large[k]]); - std::sort(vars.begin(), vars.end()); - // now the value of vars has to be v*sign - lpvar j; - if (find_complimenting_monomial(vars, j) && - large_lemma_for_proportion_case(m, mask, large, j)) { - TRACE("nla_solver", print_explanation_and_lemma(tout);); - return true; - } - } else { - SASSERT(mask[k]); - mask[k] = false; - vars.push_back(vars_copy[large[k]]); // vars might become unsorted - } - } - return false; // we exhausted the mask and did not find the compliment monomial - } - - bool small_basic_lemma_for_mon_proportionality(unsigned i_mon, const unsigned_vector& _small) { - svector mask(_small.size(), false); // init mask by false - const auto & m = m_monomials[i_mon]; - rational sign; - auto vars = reduce_monomial_to_rooted(m.vars(), sign); - auto vars_copy = vars; - auto v = lp::abs(m_lar_solver.get_column_value_rational(m.var())); - // We cross out from vars the "large" variables represented by the mask - for (unsigned k = 0; k < mask.size(); k++) { - if (!mask[k]) { - mask[k] = true; - TRACE("nla_solver", tout << "_small[" << k << "] = " << _small[k];); - SASSERT(std::find(vars.begin(), vars.end(), vars_copy[_small[k]]) != vars.end()); - vars.erase(vars_copy[_small[k]]); - std::sort(vars.begin(), vars.end()); - // now the value of vars has to be v*sign - lpvar j; - if (find_complimenting_monomial(vars, j) && - small_lemma_for_proportion_case(m, mask, _small, j)) { - TRACE("nla_solver", print_explanation_and_lemma(tout);); - return true; - } - } else { - SASSERT(mask[k]); - mask[k] = false; - vars.push_back(vars_copy[_small[k]]); // vars might become unsorted - } - } - - return false; // we exhausted the mask and did not find the compliment monomial - } - - // we derive a lemma from |x| >= 1 => |xy| >= |y| or |x| <= 1 => |xy| <= |y| - bool basic_lemma_for_mon_proportionality_from_factors_to_product(unsigned i_mon) { - const monomial & m = m_monomials[i_mon]; - unsigned_vector large; - unsigned_vector _small; - get_large_and_small_indices_of_monomimal(m, large, _small); - TRACE("nla_solver", tout << "large size = " << large.size() << ", _small size = " << _small.size();); - if (large.empty() && _small.empty()) - return false; - - return - large_basic_lemma_for_mon_proportionality(i_mon, large) - || - small_basic_lemma_for_mon_proportionality(i_mon, _small); - } - - // Using the following theorems - // |ab| >= |b| iff |a| >= 1 or b = 0 - // |ab| <= |b| iff |a| <= 1 or b = 0 - // and their commutative variants - bool basic_lemma_for_mon_proportionality(unsigned i_mon) { - TRACE("nla_solver", tout << "basic_lemma_for_mon_proportionality";); - return - basic_lemma_for_mon_proportionality_from_factors_to_product(i_mon) || - basic_lemma_for_mon_proportionality_from_product_to_factors(i_mon); - } - std::ostream & print_factorization(const factorization& f, std::ostream& out) const { for (unsigned k = 0; k < f.size(); k++ ) { print_var(f[k], out); @@ -694,130 +347,6 @@ struct solver::imp { return out << ", sign = " << f.sign(); } - - void restrict_signs_of_xy_and_y_on_lemma(lpvar y, lpvar xy, const rational& _y, const rational& _xy, int& y_sign, int &xy_sign) { - if (_y.is_pos()) { - mk_ineq(y, lp::lconstraint_kind::LE); - y_sign = 1; - } else { - mk_ineq(y, lp::lconstraint_kind::GT); - y_sign = -1; - } - - if (_y.is_pos()) { - mk_ineq(xy, lp::lconstraint_kind::LE); - xy_sign = 1; - } else { - mk_ineq(xy, lp::lconstraint_kind::GT); - xy_sign = -1; - } - } - - // We derive a lemma from |x| >= 1 || y = 0 => |xy| >= |y| - // Here f is a factorization of monomial xy ( it can have more factors than 2) - // f[k] plays the role of y, the rest of the factors play the role of x - bool lemma_for_proportional_factors_on_vars_ge(lpvar xy, unsigned k, const factorization& f) { - TRACE("nla_solver", - print_factorization(f, tout << "f="); - print_var(f[k], tout << "y=");); - NOT_IMPLEMENTED_YET(); - /* - const rational & _x = vvr(x); - const rational & _y = vvr(y); - - if (!(abs(_x) >= rational(1) || _y.is_zero())) - return false; - // the precondition holds - const rational & _xy = vvr(xy); - if (abs(_xy) >= abs(_y)) - return false; - // Here we just create the lemma. - lp::lar_term t; - if (abs(_x) >= rational(1)) { - // add to lemma x < -1 || x > 1 - t.add_coeff_var(rational(1), x); - if (_x >= rational(1)) - m_lemma->push_back(ineq(lp::lconstraint_kind::LT, t, rational(1))); - else { - lp_assert(_x <= -rational(1)); - m_lemma->push_back(ineq(lp::lconstraint_kind::GT, t, -rational(1))); - } - } else { - lp_assert(_y.is_zero() && t.is_empty()); - // add to lemma y != 0 - t.add_coeff_var(rational(1), y); - m_lemma->push_back(ineq(lp::lconstraint_kind::NE, t, rational::zero())); - } - - int xy_sign, y_sign; - restrict_signs_of_xy_and_y_on_lemma(y, xy, _y, _xy, y_sign, xy_sign); - - t.clear(); // abs(xy) - abs(y) <= 0 - t.add_coeff_var(rational(xy_sign), xy); - t.add_coeff_var(rational(-y_sign), y); - m_lemma->push_back(ineq(lp::lconstraint_kind::GE, t, rational::zero())); - TRACE("nla_solver", tout<< "lemma: ";print_lemma(*m_lemma, tout);); - return true; - */ - return false; - } - - // we derive a lemma from |x| <= 1 || y = 0 => |xy| <= |y| - bool lemma_for_proportional_factors_on_vars_le(lpvar xy, unsigned k, const factorization & f) { - NOT_IMPLEMENTED_YET(); - /* - TRACE("nla_solver", - print_var(xy, tout << "xy="); - print_var(x, tout << "x="); - print_var(y, tout << "y=");); - const rational & _x = vvr(x); - const rational & _y = vvr(y); - - if (!(abs(_x) <= rational(1) || _y.is_zero())) - return false; - // the precondition holds - const rational & _xy = vvr(xy); - if (abs(_xy) <= abs(_y)) - return false; - // Here we just create the lemma. - lp::lar_term t; - if (abs(_x) <= rational(1)) { - // add to lemma x < -1 || x > 1 - t.add_coeff_var(rational(1), x); - m_lemma->push_back(ineq(lp::lconstraint_kind::LT, t, -rational(1))); - m_lemma->push_back(ineq(lp::lconstraint_kind::GT, t, rational(1))); - } else { - lp_assert(_y.is_zero() && t.is_empty()); - // add to lemma y != 0 - t.add_coeff_var(rational(1), y); - m_lemma->push_back(ineq(lp::lconstraint_kind::NE, t, rational::zero())); - } - - int y_sign, xy_sign; - restrict_signs_of_xy_and_y_on_lemma(y, xy, _y, _xy, y_sign, xy_sign); - - t.clear(); // abs(xy) - abs(y) <= 0 - t.add_coeff_var(rational(xy_sign), xy); - t.add_coeff_var(rational(-y_sign), y); - m_lemma->push_back(ineq(lp::lconstraint_kind::LE, t, rational::zero())); - TRACE("nla_solver", tout<< "lemma: ";print_lemma(*m_lemma, tout);); - return true; - */ - return false; - } - - // we derive a lemma from |x| >= 1 || |y| = 0 => |xy| >= |y|, or the similar of <= - bool lemma_for_proportional_factors(unsigned i_mon, const factorization& f) { - lpvar var_of_mon = m_monomials[i_mon].var(); - TRACE("nla_solver", print_var(var_of_mon, tout); tout << " is factorized as "; print_factorization(f, tout);); - for (unsigned k = 0; k < f.size(); k++) { - if (lemma_for_proportional_factors_on_vars_ge(var_of_mon, k, f) || - lemma_for_proportional_factors_on_vars_le(var_of_mon, k, f)) - return true; - } - return false; - } - struct factorization_factory_imp: factorization_factory { const imp& m_imp; @@ -843,27 +372,6 @@ struct solver::imp { }; - - // we derive a lemma from |xy| >= |y| => |x| >= 1 || |y| = 0 - bool basic_lemma_for_mon_proportionality_from_product_to_factors(unsigned i_mon) { - for (auto factorization : factorization_factory_imp(i_mon, *this)) { - if (factorization.is_empty()) { - TRACE("nla_solver", tout << "empty factorization";); - continue; - } - if (lemma_for_proportional_factors(i_mon, factorization)) { - expl_set exp; - add_explanation_of_reducing_to_rooted_monomial(m_monomials[i_mon], exp); - for (lpvar j : factorization) - add_explanation_of_reducing_to_rooted_monomial(j, exp); - m_expl->clear(); - m_expl->add(exp); - return true; - } - } - return false; - } - void explain(const factorization& f, expl_set exp) { for (lpvar k : f) { unsigned mon_index = 0; @@ -1032,60 +540,6 @@ struct solver::imp { mk_ineq(m_monomials[i_mon].var(), -rational(sign), not_one_j,lp::lconstraint_kind::EQ); return true; } - - // // |xy| >= |y| -> |x| >= 1 or y = 0 - // bool basic_lemma_for_mon_proportionality_from_monomial_to_factors_ge_j(unsigned i_mon, const factorization& f, lpvar j) { - // if (vvr(j).is_zero()){ - // return false; - // } - - - // for (lpvar k : f) { - // if (k == j) { - // continue; - // } - - // if (vvr(k).is_zero()) { - // mk_ - // } - // } - // } - // // |xy| >= |y| -> |x| >= 1 or y = 0 - // // or - // // |xy| <= |y| -> |x| <= 1 or y = 0 - // bool basic_lemma_for_mon_proportionality_from_monomial_to_factors(unsigned i_mon, const factorization& f) { - // lpvar mon_var = m_monomials[i_mon].var(); - // for (lpvar j : f) { - // if (abs(vvr(mon_var)) >= abs(vvr(j))) { - // if (basic_lemma_for_mon_proportionality_from_monomial_to_factors_ge_j(i_mon, f, j)) - // return true; - - // } - // if (abs(vvr(mon_var)) <= abs(vvr(j)) ) { - // if (basic_lemma_for_mon_proportionality_from_monomial_to_factors_le_j(i_mon, f, j)) - // return true; - - // } - // } - // return false; - // } - - // |x| >= 1 or y = 0 -> |xy| >= |y| - // or - // |x| <= 1 or y = 0 -> |xy| <= |y| - bool basic_lemma_for_mon_proportionality_from_factors_to_monomial(unsigned i_mon, const factorization& f) { - return false; - } - - - bool basic_lemma_for_mon_proportionality(unsigned i_mon, const factorization& f) { - return false; - // return basic_lemma_for_mon_proportionality_from_monomial_to_factors(i_mon, f) - // || - // basic_lemma_for_mon_proportionality_from_factors_to_monomial(i_mon, f) - // ; - } - bool basic_lemma_for_mon_neutral(unsigned i_mon, const factorization& factorization) { return @@ -1100,8 +554,7 @@ struct solver::imp { bool basic_lemma_for_mon(unsigned i_mon) { for (auto factorization : factorization_factory_imp(i_mon, *this)) { if (basic_lemma_for_mon_zero(i_mon, factorization) || - basic_lemma_for_mon_neutral(i_mon, factorization) || - basic_lemma_for_mon_proportionality(i_mon, factorization)) + basic_lemma_for_mon_neutral(i_mon, factorization)) return true; } @@ -1739,5 +1192,4 @@ void solver::test_basic_sign_lemma_with_constraints() { nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); } - }