mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

a bug fix for handling infeasibilities created in add_var_bound()

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-09 14:02:40 -08:00 committed by Lev Nachmanson
parent 2993453798
commit 23a7e5e302
2 changed files with 68 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_lra.cpp
View file

@ -2988,11 +2988,11 @@ public:
else {
ci = m_solver->add_var_bound(vi, k, b.get_value());
}
TRACE("arith", tout << "v" << b.get_var() << "\n";);
add_ineq_constraint(ci, literal(bv, !is_true));
if (is_infeasible()) {
return;
}
TRACE("arith", tout << "v" << b.get_var() << "\n";);
add_ineq_constraint(ci, literal(bv, !is_true));
propagate_eqs(vi, ci, k, b);
}
@ -3289,7 +3289,7 @@ public:
c.neg();
ctx().mark_as_relevant(c);
}
TRACE("arith", ctx().display_literals_verbose(tout, m_core););
TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";);
ctx().mk_th_axiom(get_id(), m_core.size(), m_core.c_ptr());
}
}
@ -3760,6 +3760,8 @@ public:
break;
}
case null_source:
out << idx << " null";
break;
default:
UNREACHABLE();
break;

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

@ -519,9 +519,9 @@ struct solver::imp {
}
void trace_print_monomial_and_factorization(unsigned i_mon, const factorization& f, std::ostream& out) const {
out << "mon = ";
print_monomial(i_mon, out);
out << "\nfact = "; print_factorization(f, out);
print_monomial(i_mon, out << "mon: ") << "\n";
out << "value: " << vvr(m_monomials[i_mon].var()) << "\n";
print_factorization(f, out << "fact: ") << "\n";
}
// x = 0 or y = 0 -> xy = 0
bool basic_lemma_for_mon_zero_from_factors_to_monomial(unsigned i_mon, const factorization& f) {
@ -840,11 +840,64 @@ struct solver::imp {
m_lemma->clear();
}
bool order_lemma(const unsigned_vector& to_refine) {
bool order_lemma_on_factor(const factorization& f, unsigned k, int sign) {
return false;
}
bool order_lemma_on_factorization(unsigned i_mon, const factorization& f) {
for (unsigned k = 0; k < f.size(); k++) {
const rational & v = vvr(f[k]);
if (v.is_zero())
continue;
int sign = ((v.is_pos() && f.sign().is_pos()) || (v.is_neg() && f.sign().is_neg()))? 1 : -1;
if (order_lemma_on_factor(f, k, sign)) {
return true;
}
}
return false;
}
bool order_lemma_on_monomial(unsigned i_mon) {
for (auto factorization : factorization_factory_imp(i_mon, *this)) {
if (factorization.is_empty())
continue;
if (order_lemma_on_factorization(i_mon, factorization))
return true;
}
return false;
}
bool order_lemma(const unsigned_vector& to_refine) {
for (unsigned i_mon : to_refine) {
if (order_lemma_on_monomial(i_mon)) {
return true;
}
}
return false;
}
bool monotonicity_lemma_on_factorization(unsigned i_mon, const factorization& factorization) {
return false;
}
bool monotonicity_lemma_on_monomial(unsigned i_mon) {
for (auto factorization : factorization_factory_imp(i_mon, *this)) {
if (factorization.is_empty())
continue;
if (monotonicity_lemma_on_factorization(i_mon, factorization))
return true;
}
return false;
}
bool monotonicity_lemma(const unsigned_vector& to_refine) {
for (unsigned i_mon : to_refine) {
if (monotonicity_lemma_on_monomial(i_mon)) {
return true;
}
}
return false;
}
@ -857,16 +910,20 @@ struct solver::imp {
m_expl = &exp;
m_lemma = &l;
if (m_lar_solver.get_status() != lp::lp_status::OPTIMAL)
if (m_lar_solver.get_status() != lp::lp_status::OPTIMAL) {
TRACE("nla_solver", tout << "unknown\n";);
return l_undef;
}
unsigned_vector to_refine;
for (unsigned i = 0; i < m_monomials.size(); i++) {
if (!check_monomial(m_monomials[i]))
to_refine.push_back(i);
}
if (to_refine.empty())
if (to_refine.empty()) {
return l_true;
}
TRACE("nla_solver", tout << "to_refine.size() = " << to_refine.size() << std::endl;);