mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

fix in sign lemma for the zero case

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-12-29 11:37:46 +05:30
parent abbf8c587b
commit bc9edac913
1 changed files with 26 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

56
src/util/lp/nla_solver.cpp
View file

@ -561,6 +561,31 @@ struct solver::imp {
} }
return sign; return sign;
} }
void generate_zero_lemma(const monomial& m) {
unsigned zero_j = -1;
for (unsigned j : m.vars()){
if (vvr(j).is_zero()){
zero_j = j;
break;
}
}
SASSERT(zero_j + 1);
mk_ineq(zero_j, llc::NE);
mk_ineq(m.var(), llc::EQ);
}
// we know here that the value one of the vars of each monomial is zero
// so the value of each monomial has to be zero
bool sign_lemma_for_zero_on_list(const unsigned_vector& mon_list) {
for (unsigned i : mon_list) {
if (!vvr(m_monomials[i]).is_zero()) {
generate_zero_lemma(m_monomials[i]);
return true;
}
}
return false;
}
bool basic_sign_lemma_on_a_bucket_of_abs_vals(const vector<rational>& abs_vals, const unsigned_vector& list){ bool basic_sign_lemma_on_a_bucket_of_abs_vals(const vector<rational>& abs_vals, const unsigned_vector& list){
TRACE("nla_solver", TRACE("nla_solver",
@ -572,7 +597,7 @@ struct solver::imp {
rational val = vvr(m_monomials[list[0]].var()); rational val = vvr(m_monomials[list[0]].var());
int sign = vars_sign(m_monomials[list[0]].vars()); int sign = vars_sign(m_monomials[list[0]].vars());
if (sign == 0) { if (sign == 0) {
return false; return sign_lemma_for_zero_on_list(list);
} }
for (unsigned i = 1; i < list.size(); i++) { for (unsigned i = 1; i < list.size(); i++) {
@ -598,40 +623,11 @@ struct solver::imp {
return m_rm_table.vec()[rm_i]; return m_rm_table.vec()[rm_i];
} }
bool basic_sign_lemma_on_a_var_bucket_of_abs_vals(const rational& v, const unsigned_vector& vars ) {
for(unsigned j : vars) {
auto it = m_var_to_its_monomial.find(j);
if (it == m_var_to_its_monomial.end()) continue;
const monomial& m = m_monomials[it->second];
const rooted_mon& rm = mon_to_rooted_mon(m);
unsigned rm_j = var(rm);
if (rm_j == j) continue;
if (abs(vvr(rm_j)) != v) {
explain(m);
explain(rm);
generate_bsm(j, rm_j);
return true;
}
}
return false;
}
void generate_bsm(unsigned j, unsigned k) {
auto jv = vvr(j);
auto kv = vvr(k);
auto js = rational(rat_sign(jv));
auto ks = rational(rat_sign(kv));
mk_ineq(js, j, -ks, k, llc::EQ);
}
/** /**
* \brief <generate lemma by using the fact that -ab = (-a)b) and * \brief <generate lemma by using the fact that -ab = (-a)b) and
-ab = a(-b) -ab = a(-b)
*/ */
bool basic_sign_lemma() { bool basic_sign_lemma() {
for (const auto & p : m_vars_equivalence.m_vars_by_abs_values){
if (basic_sign_lemma_on_a_var_bucket_of_abs_vals(p.first, p.second))
return true;
}
for (const auto & p : m_vars_equivalence.monomials_by_abs_values()){ for (const auto & p : m_vars_equivalence.monomials_by_abs_values()){
if (basic_sign_lemma_on_a_bucket_of_abs_vals(p.first, p.second)) if (basic_sign_lemma_on_a_bucket_of_abs_vals(p.first, p.second))
return true; return true;