mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 22:53:24 +00:00
Code Activity

create a lemma for basic proportional case

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-27 15:43:09 +08:00
parent 633265cc6a
commit d935bdb6c4
1 changed files with 56 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

96
src/util/lp/niil_solver.cpp
View file

@ -282,7 +282,7 @@ struct solver::imp {
return out; return out;
} }
std::ostream& print_explanation(std::ostream& out) { std::ostream& print_explanation(std::ostream& out) const {
for (auto &p : *m_expl) { for (auto &p : *m_expl) {
m_lar_solver.print_constraint(p.second, out) << "\n"; m_lar_solver.print_constraint(p.second, out) << "\n";
} }
@ -305,14 +305,7 @@ struct solver::imp {
lp::lar_term t; lp::lar_term t;
t.add_monomial(rational(1), a.var()); t.add_monomial(rational(1), a.var());
t.add_monomial(rational(- sign), b.var()); t.add_monomial(rational(- sign), b.var());
TRACE("niil_solver", TRACE("niil_solver", print_explanation_and_lemma(tout););
m_lar_solver.print_term(t, tout);
tout << "\ncreated lemma: ";
print_monomial(a, tout);
tout << "\n";
print_monomial(b, tout);
);
ineq in(lp::lconstraint_kind::NE, t); ineq in(lp::lconstraint_kind::NE, t);
m_lemma->push_back(in); m_lemma->push_back(in);
} }
@ -482,23 +475,28 @@ struct solver::imp {
t.m_v = -rs; t.m_v = -rs;
ineq in(kind, t); ineq in(kind, t);
m_lemma->push_back(in); m_lemma->push_back(in);
TRACE("niil_solver", TRACE("niil_solver", print_explanation_and_lemma(tout););
tout << "used constraints:\n";
print_explanation(tout);
tout << "derived constraint ";
m_lar_solver.print_term(t, tout);
tout << " " << lp::lconstraint_kind_string(kind) << " 0\n";
tout << "the monomial is : ";
print_monomial(m_monomials[i_mon], tout) << "\n";
lpvar mon_var = m_monomials[i_mon].var();
tout << "the monomial value in the model is: " << m_lar_solver.get_column_name(mon_var) << " = " << m_lar_solver.get_column_value_rational(mon_var);
);
return true; return true;
} }
std::ostream & print_ineq(ineq & in, std::ostream & out) const {
m_lar_solver.print_term(in.m_term, out);
out << " " << lp::lconstraint_kind_string(in.m_cmp) << " 0";
return out;
}
std::ostream & print_lemma(lemma& l, std::ostream & out) const {
for (auto & in: l) {
out << "("; print_ineq(in, out) << ")";
}
return out;
}
std::ostream & print_explanation_and_lemma(std::ostream & out) const {
out << "explanation:\n"; print_explanation(out) << "\nlemma\n:" ; print_lemma(*m_lemma, out) << "\n";
return out;
}
/** /**
* \brief <return true if j is fixed to 1 or -1, and put the value into "sign"> * \brief <return true if j is fixed to 1 or -1, and put the value into "sign">
*/ */
@ -656,20 +654,12 @@ tout << "the monomial is : ";
for (unsigned k : mask) { for (unsigned k : mask) {
add_explanation_of_one(ones_of_monomial[k]); add_explanation_of_one(ones_of_monomial[k]);
} }
TRACE("niil_solver",
for (auto &p : *m_expl)
m_lar_solver.print_constraint(p.second, tout); tout << "\n";
);
lp::lar_term t; lp::lar_term t;
t.add_monomial(rational(1), m.var()); t.add_monomial(rational(1), m.var());
t.add_monomial(rational(- sign), j); t.add_monomial(rational(- sign), j);
TRACE("niil_solver",
m_lar_solver.print_term(t, tout);
tout << "\n";
);
ineq in(lp::lconstraint_kind::EQ, t); ineq in(lp::lconstraint_kind::EQ, t);
m_lemma->push_back(in); m_lemma->push_back(in);
TRACE("niil_solver", print_explanation_and_lemma(tout););
} }
// vars here are minimal vars for m.vs // vars here are minimal vars for m.vs
@ -720,11 +710,13 @@ tout << "the monomial is : ";
} }
bool large_lemma_for_proportion_case(const mon_eq& m, const svector<unsigned> & mask, bool large_lemma_for_proportion_case(const mon_eq& m, const svector<unsigned> & mask,
const svector<unsigned> & large, unsigned j) { const svector<unsigned> & large, unsigned j) {
const rational j_val = lp::abs(m_lar_solver.get_column_value_rational(j)); TRACE("niil_solver", );
const rational j_val = m_lar_solver.get_column_value_rational(j);
const rational m_val = lp::abs(m_lar_solver.get_column_value_rational(m.m_v)); const rational m_val = lp::abs(m_lar_solver.get_column_value_rational(m.m_v));
// since the masked factor is greater than or equal to one // since the masked factor is greater than or equal to one
// j_val has to be less than or equal to m_val // j_val has to be less than or equal to m_val
if (j_val <= m_val) int sign = j_val < - m_val? -1: (j_val > m_val)? 1: 0;
if (sign == 0) // abs(j_val) <= m_val which is not a conflict
return false; return false;
expl_set expl; expl_set expl;
add_explanation_of_reducing_to_mininal_monomial(m, expl); add_explanation_of_reducing_to_mininal_monomial(m, expl);
@ -735,16 +727,32 @@ tout << "the monomial is : ";
m_expl->clear(); m_expl->clear();
m_expl->add(expl); m_expl->add(expl);
return false; if (sign == -1) {
lp::lar_term t; // j >= -m_val or j + m.m_v >= 0
t.add_monomial(rational(1), j);
t.add_monomial(rational(1), m.m_v);
t.m_v = rational(0);
ineq in(lp::lconstraint_kind::GE, t);
m_lemma->push_back(in);
return true;
}
SASSERT(sign == 1);
lp::lar_term t; // j <= m_val or j - m.m_v <= 0
t.add_monomial(rational(1), j);
t.add_monomial(rational(-1), m.m_v);
t.m_v = rational(0);
ineq in(lp::lconstraint_kind::LE, t);
m_lemma->push_back(in);
return true;
} }
bool large_basic_lemma_for_mon_proportionality(unsigned i_mon, const svector<unsigned>& large) { bool large_basic_lemma_for_mon_proportionality(unsigned i_mon, const svector<unsigned>& large) {
svector<unsigned> mask(large.size(), (unsigned) 0); svector<unsigned> mask(large.size(), (unsigned) 0); // init mask by zeroes
const auto & m = m_monomials[i_mon]; const auto & m = m_monomials[i_mon];
int sign; int sign;
auto vars = reduce_monomial_to_minimal(m.m_vs, sign); auto vars = reduce_monomial_to_minimal(m.m_vs, sign);
auto v = lp::abs(m_lar_solver.get_column_value_rational(m.m_v)); auto v = lp::abs(m_lar_solver.get_column_value_rational(m.m_v));
// We crossing out the "large" variables representing the mask from vars // We cross out from vars the "large" variables represented by the mask
do { do {
for (unsigned k = 0; k < mask.size(); k++) { for (unsigned k = 0; k < mask.size(); k++) {
if (mask[k] == 0) { if (mask[k] == 0) {
@ -754,10 +762,11 @@ tout << "the monomial is : ";
std::sort(vars.begin(), vars.end()); std::sort(vars.begin(), vars.end());
// now the value of vars has to be v*sign // now the value of vars has to be v*sign
lpvar j; lpvar j;
if (!find_compimenting_monomial(vars, j)) if (find_compimenting_monomial(vars, j) &&
return false; large_lemma_for_proportion_case(m, mask, large, j)) {
if (large_lemma_for_proportion_case(m, mask, large, j)) TRACE("niil_solver", print_explanation_and_lemma(tout););
return true; return true;
}
} else { } else {
SASSERT(mask[k] == 1); SASSERT(mask[k] == 1);
mask[k] = 0; mask[k] = 0;
@ -765,6 +774,7 @@ tout << "the monomial is : ";
} }
} }
} while(true); } while(true);
TRACE("niil_solver", tout << "return false";);
return false; // we exhausted the mask and did not find the compliment monomial return false; // we exhausted the mask and did not find the compliment monomial
} }
@ -807,7 +817,9 @@ tout << "the monomial is : ";
bool generate_basic_lemma(svector<unsigned> & to_refine) { bool generate_basic_lemma(svector<unsigned> & to_refine) {
for (unsigned i : to_refine) for (unsigned i : to_refine)
if (generate_basic_lemma_for_mon(i)) { if (generate_basic_lemma_for_mon(i)) {
TRACE("niil_solver", tout << "a lemma generated for monomial " << i << std::endl;); TRACE("niil_solver", tout << "a lemma generated for monomial " << i << std::endl;
tout << "lemma.size() = " << m_lemma->size() << "\n";
print_explanation_and_lemma(tout); );
return true; return true;
} }
return false; return false;
@ -864,6 +876,8 @@ tout << "the monomial is : ";
void init_search() { void init_search() {
map_vars_to_monomials_and_constraints(); map_vars_to_monomials_and_constraints();
init_vars_equivalence(); init_vars_equivalence();
m_expl->clear();
m_lemma->clear();
} }
lbool check(lp::explanation & exp, lemma& l) { lbool check(lp::explanation & exp, lemma& l) {