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

check the lar_solver status more often

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-06 16:12:52 -08:00 committed by Lev Nachmanson
parent c95f2a5bc6
commit efeeabe127
2 changed files with 39 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_lra.cpp
View file

@ -2974,9 +2974,11 @@ public:
else {
ci = m_solver->add_var_bound(vi, k, b.get_value());
}
if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
return;
}
TRACE("arith", tout << "v" << b.get_var() << "\n";);
add_ineq_constraint(ci, literal(bv, !is_true));
propagate_eqs(vi, ci, k, b);
}

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

@ -839,12 +839,26 @@ struct solver::imp {
m_expl->clear();
m_lemma->clear();
}
bool order_lemma(const unsigned_vector& to_refine) {
return false;
}
bool monotonicity_lemma(const unsigned_vector& to_refine) {
return false;
}
bool tangent_lemma(const unsigned_vector& to_refine) {
return false;
}
lbool check(lp::explanation & exp, lemma& l) {
TRACE("nla_solver", tout << "check of nla";);
m_expl = &exp;
m_lemma = &l;
lp_assert(m_lar_solver.get_status() == lp::lp_status::OPTIMAL);
if (m_lar_solver.get_status() != lp::lp_status::OPTIMAL)
return l_undef;
unsigned_vector to_refine;
for (unsigned i = 0; i < m_monomials.size(); i++) {
if (!check_monomial(m_monomials[i]))
@ -857,14 +871,29 @@ struct solver::imp {
TRACE("nla_solver", tout << "to_refine.size() = " << to_refine.size() << std::endl;);
init_search();
if (basic_lemma(to_refine)) {
return l_false;
}
return l_undef;
for (int search_level = 0; search_level < 3; search_level++) {
if (search_level == 0) {
if (basic_lemma(to_refine)) {
return l_false;
}
} else if (search_level == 1) {
if (order_lemma(to_refine)) {
return l_false;
}
} else { // search_level == 3
if (monotonicity_lemma(to_refine)) {
return l_false;
}
if (tangent_lemma(to_refine)) {
return l_false;
}
}
}
return l_undef;
}
void test_factorization(unsigned mon_index, unsigned number_of_factorizations) {
vector<ineq> lemma;
m_lemma = & lemma;