3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00

add hook for in-processing simplification for NLA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-10-25 15:09:21 -07:00
parent 6ba151599e
commit e2db2b864b
4 changed files with 9 additions and 27 deletions

View file

@ -1556,9 +1556,6 @@ lbool core::check() {
if (no_effect())
m_monomial_bounds.propagate();
if (no_effect() && improve_bounds())
return l_false;
{
std::function<void(void)> check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); };
@ -1793,28 +1790,6 @@ void core::set_use_nra_model(bool m) {
void core::collect_statistics(::statistics & st) {
}
bool core::improve_bounds() {
return false;
uint_set seen;
bool bounds_improved = false;
auto insert = [&](lpvar v) {
if (seen.contains(v))
return;
seen.insert(v);
if (lra.improve_bound(v, false))
bounds_improved = true, lp_settings().stats().m_nla_bounds_improvements++;
if (lra.improve_bound(v, true))
bounds_improved = true, lp_settings().stats().m_nla_bounds_improvements++;
};
for (auto & m : m_emons) {
insert(m.var());
for (auto v : m.vars())
insert(v);
}
return bounds_improved;
}
void core::propagate() {
clear();
@ -1822,6 +1797,10 @@ void core::propagate() {
m_monics_with_changed_bounds.reset();
}
void core::simplify() {
// in-processing simplifiation can go here, such as bounds improvements.
}
} // end of nla

View file

@ -104,8 +104,6 @@ class core {
void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
void add_bounds();
// try to improve bounds for variables in monomials.
bool improve_bounds();
public:
// constructor
@ -386,6 +384,8 @@ public:
bool no_lemmas_hold() const;
void propagate();
void simplify();
lbool test_check();
lpvar map_to_root(lpvar) const;

View file

@ -38,6 +38,7 @@ namespace nla {
bool need_check();
lbool check();
void propagate();
void simplify() { m_core->simplify(); }
lbool check_power(lpvar r, lpvar x, lpvar y);
bool is_monic_var(lpvar) const;
bool influences_nl_var(lpvar) const;

View file

@ -1091,6 +1091,8 @@ public:
void restart_eh() {
m_arith_eq_adapter.restart_eh();
if (m_nla)
m_nla->simplify();
}
void relevant_eh(app* n) {