mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix generation of basic sign lemmas

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-10-02 13:55:47 -07:00 • committed by Lev Nachmanson
parent 17ed9c39be
commit 8c59557099
1 changed files with 29 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -258,6 +258,7 @@ struct solver::imp {
return out; return out;
} }
// the monomials should be equal by modulo sign, but they are not equal in the model by modulo sign // the monomials should be equal by modulo sign, but they are not equal in the model by modulo sign
void fill_explanation_and_lemma_sign(const mon_eq& a, const mon_eq & b, int sign) { void fill_explanation_and_lemma_sign(const mon_eq& a, const mon_eq & b, int sign) {
expl_set expl; expl_set expl;
@ -271,12 +272,13 @@ struct solver::imp {
for (auto &p : *m_expl) for (auto &p : *m_expl)
m_lar_solver.print_constraint(p.second, tout); tout << "\n"; m_lar_solver.print_constraint(p.second, tout); tout << "\n";
); );
SASSERT(m_lemma->size() == 0);
lp::lar_term t; lp::lar_term t;
t.add_coeff_var(rational(1), a.var()); t.add_coeff_var(rational(1), a.var());
t.add_coeff_var(rational(- sign), b.var()); t.add_coeff_var(rational(- sign), b.var());
TRACE("nla_solver", print_explanation_and_lemma(tout);); ineq in(lp::lconstraint_kind::EQ, t, rational::zero());
ineq in(lp::lconstraint_kind::NE, t, rational::zero());
m_lemma->push_back(in); m_lemma->push_back(in);
TRACE("nla_solver", print_explanation_and_lemma(tout););
} }
// Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus. // Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus.
@ -293,18 +295,32 @@ struct solver::imp {
return ret; return ret;
} }
bool list_contains_one_to_refine(const std::unordered_set<unsigned> & to_refine_set,
const vector<mono_index_with_sign>& list_of_mon_indices) {
for (const auto& p : list_of_mon_indices) {
if (to_refine_set.find(p.m_i) != to_refine_set.end())
return true;
}
return false;
}
/** /**
* \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 generate_basic_lemma_for_mon_sign(unsigned i_mon) { bool generate_basic_sign_lemma(const unsigned_vector& to_refine) {
if (m_vars_equivalence.empty()) { if (m_vars_equivalence.empty()) {
return false; return false;
} }
std::unordered_set<unsigned> to_refine_set;
for (unsigned i : to_refine)
to_refine_set.insert(i);
for (auto it : m_rooted_monomials) { for (auto it : m_rooted_monomials) {
const auto & list = it.second; const auto & list = it.second;
if (!list_contains_one_to_refine(to_refine_set, list))
continue;
const auto & m0 = list[0]; const auto & m0 = list[0];
rational val = vvr(m_monomials[m0.m_i].var()) * m0.m_sign; rational val = vvr(m_monomials[m0.m_i].var()) * m0.m_sign;
// every other monomial in the list has to have the same value up to the sign // every other monomial in the list has to have the same value up to the sign
for (unsigned i = 1; i < list.size(); i++) { for (unsigned i = 1; i < list.size(); i++) {
@ -1241,14 +1257,19 @@ struct solver::imp {
// use basic multiplication properties to create a lemma // use basic multiplication properties to create a lemma
// for the given monomial // for the given monomial
bool generate_basic_lemma_for_mon(unsigned i_mon) { bool generate_basic_lemma_for_mon(unsigned i_mon) {
return generate_basic_lemma_for_mon_sign(i_mon) return
|| generate_basic_lemma_for_mon_zero(i_mon) generate_basic_lemma_for_mon_zero(i_mon)
|| generate_basic_lemma_for_mon_neutral(i_mon) ||
|| generate_basic_lemma_for_mon_proportionality(i_mon); generate_basic_lemma_for_mon_neutral(i_mon)
||
generate_basic_lemma_for_mon_proportionality(i_mon);
} }
// use basic multiplication properties to create a lemma // use basic multiplication properties to create a lemma
bool generate_basic_lemma(unsigned_vector & to_refine) { bool generate_basic_lemma(unsigned_vector & to_refine) {
if (generate_basic_sign_lemma(to_refine))
return true;
for (unsigned i : to_refine) { for (unsigned i : to_refine) {
if (generate_basic_lemma_for_mon(i)) { if (generate_basic_lemma_for_mon(i)) {
return true; return true;