mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 13:07:53 +00:00
Code Activity

separate bounds introduction

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-10-29 14:16:34 -07:00
parent cf54e985e8
commit 6ba4ba142f
3 changed files with 50 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

54
src/math/lp/nla_bounds.cpp
View file

@ -25,18 +25,50 @@ namespace nla {
for (lpvar i : c().to_refine()) {
auto const &m = c().emons()[i];
for (lpvar j : m.vars()) {
if (!c().var_is_free(j))
continue;
if (m.is_bound_propagated())
continue;
c().emons().set_bound_propagated(m);
// split the free variable (j <= 0, or j > 0), and return
auto i(ineq(j, lp::lconstraint_kind::LE, rational::zero()));
c().add_literal(i);
TRACE(nla_solver, c().print_ineq(i, tout) << "\n");
++c().lp_settings().stats().m_nla_add_bounds;
return;
if (add_bounds_to_free_variable(m, j) ||
add_bounds_to_variable_at_value(j, 0) ||
add_bounds_to_variable_at_value(j, 1) ||
add_bounds_to_variable_at_value(j, -1)) {
++c().lp_settings().stats().m_nla_add_bounds;
return;
}
}
}
}
bool bounds::add_bounds_to_free_variable(monic const& m, lp::lpvar j) {
if (!c().var_is_free(j))
return false;
if (m.is_bound_propagated())
return false;
c().emons().set_bound_propagated(m);
// split the free variable (j <= 0, or j > 0), and return
auto i(ineq(j, lp::lconstraint_kind::LE, rational::zero()));
c().add_literal(i);
TRACE(nla_solver, c().print_ineq(i, tout) << "\n");
return true;
}
bool bounds::add_bounds_to_variable_at_value(lp::lpvar j, int value) {
// disable new functionality
return false;
auto v = c().val(j);
if (v != value)
return false;
if (c().var_is_fixed(j))
return false;
// fix a bound that hasn't already been fixed.
if (c().has_lower_bound(j) && c().get_lower_bound(j) == value) {
auto i(ineq(j, lp::lconstraint_kind::LE, rational(value)));
TRACE(nla_solver, c().print_ineq(i, tout) << "\n");
c().add_literal(i);
}
else {
auto i(ineq(j, lp::lconstraint_kind::GE, rational(value)));
TRACE(nla_solver, c().print_ineq(i, tout) << "\n");
c().add_literal(i);
}
return true;
}
} // namespace nla

11
src/math/lp/nla_bounds.h
View file

@ -18,19 +18,16 @@
--*/
#pragma once
#include "math/lp/nla_common.h"
#include "math/lp/nla_intervals.h"
#include "math/lp/nex.h"
#include "math/lp/cross_nested.h"
#include "util/uint_set.h"
#include "math/grobner/pdd_solver.h"
namespace nla {
class core;
class bounds : common {
bool add_bounds_to_free_variable(monic const& m, lp::lpvar j);
bool add_bounds_to_variable_at_value(lp::lpvar j, int i);
public:
bounds(core *core);
void operator()();

3
src/math/lp/nla_stellensatz.cpp
View file

@ -58,6 +58,7 @@ namespace nla {
saturate_basic_linearize();
TRACE(arith, display(tout << "stellensatz after saturation\n"));
lbool r = m_solver.solve();
// IF_VERBOSE(0, verbose_stream() << "stellensatz " << r << "\n");
if (r == l_false)
add_lemma();
return r;
@ -1507,9 +1508,11 @@ namespace nla {
lbool stellensatz::solver::solve() {
while (true) {
lbool r = solve_lra();
// IF_VERBOSE(0, verbose_stream() << "solve lra " << r << "\n");
if (r != l_true)
return r;
r = solve_lia();
// IF_VERBOSE(0, verbose_stream() << "solve lia " << r << "\n");
if (r != l_true)
return r;
unsigned sz = lra_solver->number_of_vars();