mirror of
https://github.com/Z3Prover/z3
synced 2025-06-20 04:43:39 +00:00
more cleanup in nla_solver
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev
Lev Nachmanson
parent
492abc1e57
commit
94448f36bb
1 changed files with 1 additions and 549 deletions
|
|
@ -269,63 +269,6 @@ struct solver::imp {
|
||||||
return static_cast<unsigned>(-1) != j;
|
return static_cast<unsigned>(-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 {
|
bool var_is_fixed_to_zero(lpvar j) const {
|
||||||
return
|
return
|
||||||
m_lar_solver.column_has_upper_bound(j) &&
|
m_lar_solver.column_has_upper_bound(j) &&
|
||||||
|
|
@ -381,78 +324,7 @@ struct solver::imp {
|
||||||
out << "\n";
|
out << "\n";
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
/**
|
|
||||||
* \brief <return true if j is fixed to 1 or -1, and put the value into "sign">
|
|
||||||
*/
|
|
||||||
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<mono_index_with_sign> get_ones_of_monomimal(const svector<lpvar> & vars) {
|
|
||||||
TRACE("nla_solver", tout << "get_ones_of_monomimal";);
|
|
||||||
vector<mono_index_with_sign> 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
|
// returns true if found
|
||||||
bool find_monomial_of_vars(const svector<lpvar>& vars, monomial& m, rational & sign) const {
|
bool find_monomial_of_vars(const svector<lpvar>& vars, monomial& m, rational & sign) const {
|
||||||
auto it = m_rooted_monomials.find(vars);
|
auto it = m_rooted_monomials.find(vars);
|
||||||
|
|
@ -466,225 +338,6 @@ struct solver::imp {
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool find_complimenting_monomial(const svector<lpvar> & 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<lpvar> & 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<bool> & 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<bool> & 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<bool> 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<bool> 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 {
|
std::ostream & print_factorization(const factorization& f, std::ostream& out) const {
|
||||||
for (unsigned k = 0; k < f.size(); k++ ) {
|
for (unsigned k = 0; k < f.size(); k++ ) {
|
||||||
print_var(f[k], out);
|
print_var(f[k], out);
|
||||||
|
|
@ -694,130 +347,6 @@ struct solver::imp {
|
||||||
return out << ", sign = " << f.sign();
|
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 {
|
struct factorization_factory_imp: factorization_factory {
|
||||||
const imp& m_imp;
|
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) {
|
void explain(const factorization& f, expl_set exp) {
|
||||||
for (lpvar k : f) {
|
for (lpvar k : f) {
|
||||||
unsigned mon_index = 0;
|
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);
|
mk_ineq(m_monomials[i_mon].var(), -rational(sign), not_one_j,lp::lconstraint_kind::EQ);
|
||||||
return true;
|
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) {
|
bool basic_lemma_for_mon_neutral(unsigned i_mon, const factorization& factorization) {
|
||||||
return
|
return
|
||||||
|
|
@ -1100,8 +554,7 @@ struct solver::imp {
|
||||||
bool basic_lemma_for_mon(unsigned i_mon) {
|
bool basic_lemma_for_mon(unsigned i_mon) {
|
||||||
for (auto factorization : factorization_factory_imp(i_mon, *this)) {
|
for (auto factorization : factorization_factory_imp(i_mon, *this)) {
|
||||||
if (basic_lemma_for_mon_zero(i_mon, factorization) ||
|
if (basic_lemma_for_mon_zero(i_mon, factorization) ||
|
||||||
basic_lemma_for_mon_neutral(i_mon, factorization) ||
|
basic_lemma_for_mon_neutral(i_mon, factorization))
|
||||||
basic_lemma_for_mon_proportionality(i_mon, factorization))
|
|
||||||
return true;
|
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: ");
|
nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue