mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-09 01:11:55 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-19 17:28:10 -07:00
parent 444a9b1c4f
commit 3c38ee2690
1 changed files with 21 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/math/lp/nra_solver.cpp
View file

@ -374,30 +374,28 @@ struct solver::imp {
process_polynomial_check_assignment(num_mon, p, bound, nl2lp, t); process_polynomial_check_assignment(num_mon, p, bound, nl2lp, t);
switch (a->get_kind()) { switch (a->get_kind()) {
case nlsat::atom::EQ: {
{ // Introduce a single ineq variable and assign it per case; common handling after switch.
nla::ineq inq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below
if (m_nla_core.ineq_holds(inq)) switch (a->get_kind()) {
return l_undef; case nlsat::atom::EQ:
lemma |= inq; inq = nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound);
break;
case nlsat::atom::LT:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound);
break;
case nlsat::atom::GT:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound);
break;
default:
UNREACHABLE();
return l_undef;
} }
break; if (m_nla_core.ineq_holds(inq))
case nlsat::atom::LT: return l_undef;
{ lemma |= inq;
nla::ineq inq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); }
if (m_nla_core.ineq_holds(inq)) break;
return l_undef;
lemma |= inq;
}
break;
case nlsat::atom::GT:
{
nla::ineq inq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound);
if (m_nla_core.ineq_holds(inq))
return l_undef;
lemma |= inq;
}
break;
default: default:
UNREACHABLE(); UNREACHABLE();
return l_undef; return l_undef;