mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

#6523

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-16 09:27:22 -07:00
parent f678861aef
commit c9c5dbc347
2 changed files with 15 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/math/lp/nla_core.cpp
View file

@ -563,18 +563,15 @@ bool core::var_is_fixed(lpvar j) const {
bool core::var_is_free(lpvar j) const { bool core::var_is_free(lpvar j) const {
return lra.column_is_free(j); return lra.column_is_free(j);
} }
std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const { std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {
lra.print_term_as_indices(in.term(), out); lra.print_term_as_indices(in.term(), out);
out << " " << lconstraint_kind_string(in.cmp()) << " " << in.rs(); return out << " " << lconstraint_kind_string(in.cmp()) << " " << in.rs();
return out;
} }
std::ostream & core::print_var(lpvar j, std::ostream & out) const { std::ostream & core::print_var(lpvar j, std::ostream & out) const {
if (is_monic_var(j)) { if (is_monic_var(j))
print_monic(m_emons[j], out); print_monic(m_emons[j], out);
}
lra.print_column_info(j, out); lra.print_column_info(j, out);
signed_var jr = m_evars.find(j); signed_var jr = m_evars.find(j);
@ -1524,9 +1521,11 @@ void core::add_bounds() {
lpvar i = m_to_refine[(k + r) % sz]; lpvar i = m_to_refine[(k + r) % sz];
auto const& m = m_emons[i]; auto const& m = m_emons[i];
for (lpvar j : m.vars()) { for (lpvar j : m.vars()) {
if (!var_is_free(j)) continue; if (!var_is_free(j))
continue;
// split the free variable (j <= 0, or j > 0), and return // split the free variable (j <= 0, or j > 0), and return
m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero())); m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
TRACE("nla_solver", print_ineq(m_literals.back(), tout) << "\n");
++lp_settings().stats().m_nla_add_bounds; ++lp_settings().stats().m_nla_add_bounds;
return; return;
} }

10
src/sat/smt/arith_solver.cpp
View file

@ -1443,7 +1443,6 @@ namespace arith {
case lp::NE: is_eq = true; sign = true; break; case lp::NE: is_eq = true; sign = true; break;
default: UNREACHABLE(); default: UNREACHABLE();
} }
TRACE("arith", tout << "is_lower: " << is_lower << " sign " << sign << "\n";);
// TBD utility: lp::lar_term term = mk_term(ineq.m_poly); // TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
// then term is used instead of ineq.m_term // then term is used instead of ineq.m_term
sat::literal lit; sat::literal lit;
@ -1452,6 +1451,7 @@ namespace arith {
else else
lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower)); lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower));
TRACE("arith", tout << "is_lower: " << is_lower << " sign " << sign << " " << ctx.literal2expr(lit) << "\n";);
return sign ? ~lit : lit; return sign ? ~lit : lit;
} }
@ -1488,6 +1488,14 @@ namespace arith {
auto lit = mk_ineq_literal(ineq); auto lit = mk_ineq_literal(ineq);
ctx.mark_relevant(lit); ctx.mark_relevant(lit);
s().set_phase(lit); s().set_phase(lit);
// force trichotomy axiom for equality literals
if (ineq.cmp() == lp::EQ) {
nla::lemma l;
l.push_back(ineq);
l.push_back(nla::ineq(lp::LT, ineq.term(), ineq.rs()));
l.push_back(nla::ineq(lp::GT, ineq.term(), ineq.rs()));
false_case_of_check_nla(l);
}
} }
for (const nla::lemma& l : m_nla->lemmas()) for (const nla::lemma& l : m_nla->lemmas())
false_case_of_check_nla(l); false_case_of_check_nla(l);