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

Simplify no effect checks in nla_core.cpp

Browse source 
Move up linear nlsat call to replace bounded nlsat.
This commit is contained in:
Nikolaj Bjorner 2025-09-12 13:56:13 -07:00 • committed by GitHub
parent 4fec287107
commit cf53f2c866
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1532,8 +1532,13 @@ lbool core::check() {
return l_false;
}
if (no_effect() && should_run_bounded_nlsat())
if (no_effect()) {
scoped_limits sl(m_reslim);
sl.push_child(&m_nra_lim);
ret = m_nra.check_assignment();
IF_VERBOSE(1, verbose_stream() << "nra check_assignment returned " << ret << "\n";);
}
else if (no_effect() && should_run_bounded_nlsat())
ret = bounded_nlsat();
if (no_effect())
@ -1545,14 +1550,9 @@ lbool core::check() {
if (no_effect())
m_divisions.check();
bool use_nra_linearization = true;
if (no_effect() && use_nra_linearization) {
scoped_limits sl(m_reslim);
sl.push_child(&m_nra_lim);
ret = m_nra.check_assignment();
IF_VERBOSE(1, verbose_stream() << "nra check_assignment returned " << ret << "\n";);
}
if (no_effect()) {
std::function<void(void)> check1 = [&]() { m_order.order_lemma();