mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

split between derived and model based lemma generation

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2019-02-05 12:23:47 -08:00 • committed by Lev Nachmanson
parent 53b6b65a16
commit d06182d199
1 changed files with 41 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -371,11 +371,11 @@ struct solver::imp {
} }
std::ostream& print_explanation(lp::explanation& exp, std::ostream& out) const { std::ostream& print_explanation(lp::explanation& exp, std::ostream& out) const {
out << "expl = "; out << "expl: ";
for (auto &p : exp) { for (auto &p : exp) {
m_lar_solver.print_constraint(p.second, out); m_lar_solver.print_constraint(p.second, out);
out << " ";
} }
out << "\n";
return out; return out;
} }
@ -950,12 +950,27 @@ struct solver::imp {
} }
// here we use the fact // here we use the fact
// xy = 0 -> x = 0 or y = 0, for derived case is handled by mk_ineq // xy = 0 -> x = 0 or y = 0
bool basic_lemma_for_mon_zero(const rooted_mon& rm, const factorization& f) { bool basic_lemma_for_mon_zero_derived(const rooted_mon& rm, const factorization& f) {
TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout););
add_empty_lemma_and_explanation();
explain_fixed_var(var(rm));
std::unordered_set<lpvar> processed;
for (auto j : f) {
if (try_insert(var(j), processed))
mk_ineq(var(j), llc::EQ, current_lemma());
}
explain(rm, current_expl());
TRACE("nla_solver", print_lemma(current_lemma(), tout););
return true;
}
// here we use the fact xy = 0 -> x = 0 or y = 0
bool basic_lemma_for_mon_zero_model_based(const rooted_mon& rm, const factorization& f) {
TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout););
SASSERT(vvr(rm).is_zero()); SASSERT(vvr(rm).is_zero());
add_empty_lemma_and_explanation(); add_empty_lemma_and_explanation();
explain_fixed_var(var(rm)); mk_ineq(var(rm), llc::NE, current_lemma());
for (auto j : f) { for (auto j : f) {
mk_ineq(var(j), llc::EQ, current_lemma()); mk_ineq(var(j), llc::EQ, current_lemma());
} }
@ -974,7 +989,15 @@ struct solver::imp {
print_factorization(f, out << "fact: ") << "\n"; print_factorization(f, out << "fact: ") << "\n";
} }
void explain_fixed_var(unsigned j) { void explain_var_separated_from_zero(lpvar j) {
SASSERT(var_is_separated_from_zero(j));
if (m_lar_solver.column_has_upper_bound(j) && (m_lar_solver.get_upper_bound(j)< lp::zero_of_type<lp::impq>()))
current_expl().add(m_lar_solver.get_column_upper_bound_witness(j));
else
current_expl().add(m_lar_solver.get_column_lower_bound_witness(j));
}
void explain_fixed_var(lpvar j) {
SASSERT(var_is_fixed(j)); SASSERT(var_is_fixed(j));
current_expl().add(m_lar_solver.get_column_upper_bound_witness(j)); current_expl().add(m_lar_solver.get_column_upper_bound_witness(j));
current_expl().add(m_lar_solver.get_column_lower_bound_witness(j)); current_expl().add(m_lar_solver.get_column_lower_bound_witness(j));
@ -1003,10 +1026,17 @@ struct solver::imp {
return true; return true;
} }
bool var_is_separated_from_zero(lpvar j) const {
return (m_lar_solver.column_has_upper_bound(j) && m_lar_solver.get_upper_bound(j) < lp::zero_of_type<lp::impq>())
||
(m_lar_solver.column_has_lower_bound(j) && m_lar_solver.get_lower_bound(j) > lp::zero_of_type<lp::impq>());
}
// x = 0 or y = 0 -> xy = 0 // x = 0 or y = 0 -> xy = 0
bool basic_lemma_for_mon_non_zero_derived(const rooted_mon& rm, const factorization& f) { bool basic_lemma_for_mon_non_zero_derived(const rooted_mon& rm, const factorization& f) {
TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout););
SASSERT (!vvr(rm).is_zero()); if (!var_is_separated_from_zero(var(rm)))
return false;
int zero_j = -1; int zero_j = -1;
for (auto j : f) { for (auto j : f) {
if (var_is_fixed_to_zero(var(j))) { if (var_is_fixed_to_zero(var(j))) {
@ -1020,8 +1050,7 @@ struct solver::imp {
} }
add_empty_lemma_and_explanation(); add_empty_lemma_and_explanation();
explain_fixed_var(zero_j); explain_fixed_var(zero_j);
mk_ineq(var(rm), llc::EQ, current_lemma()); explain_var_separated_from_zero(var(rm));
explain(rm, current_expl()); explain(rm, current_expl());
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma_and_expl(tout););
return true; return true;
@ -1339,7 +1368,7 @@ struct solver::imp {
for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) { for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) {
if (factorization.is_empty()) if (factorization.is_empty())
continue; continue;
if (basic_lemma_for_mon_zero(rm, factorization) || if (basic_lemma_for_mon_zero_model_based(rm, factorization) ||
basic_lemma_for_mon_neutral_model_based(rm, factorization)) { basic_lemma_for_mon_neutral_model_based(rm, factorization)) {
explain(factorization, current_expl()); explain(factorization, current_expl());
return true; return true;
@ -1365,7 +1394,7 @@ struct solver::imp {
for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) { for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) {
if (factorization.is_empty()) if (factorization.is_empty())
continue; continue;
if (basic_lemma_for_mon_zero(rm, factorization) || if (basic_lemma_for_mon_zero_derived(rm, factorization) ||
basic_lemma_for_mon_neutral_derived(rm, factorization)) { basic_lemma_for_mon_neutral_derived(rm, factorization)) {
explain(factorization, current_expl()); explain(factorization, current_expl());
return true; return true;
@ -2419,7 +2448,7 @@ struct solver::imp {
bool no_lemmas_hold() const { bool no_lemmas_hold() const {
for (auto & l : * m_lemma_vec) { for (auto & l : * m_lemma_vec) {
if (lemma_holds(l)) if ((!l.empty()) && lemma_holds(l))
return false; return false;
} }
return true; return true;