Skip to content

Commit

Permalink
Nlsat simplify (#7227)
Browse files Browse the repository at this point in the history 
* dev branch for simplification

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* bug fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* bugfixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix factorization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* separate out simplification functionality

* reorder initialization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* reorder initialization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Update README.md

* initial warppers for seq-map/seq-fold

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* expose fold as well

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add C++ bindings for sequence operations

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add abs function to API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add parameter validation to ternary and 4-ary functions for API #7219

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add pre-processing and reorder

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add pre-processing and reorder

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed May 15, 2024
1 parent e036a5b commit 8fe357f
Show file tree
Hide file tree
Showing 13 changed files with 1,274 additions and 843 deletions.
8 changes: 6 additions & 2 deletions src/math/lp/lp_settings.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,8 +128,12 @@ struct statistics {
unsigned m_grobner_conflicts;
unsigned m_offset_eqs;
unsigned m_fixed_eqs;
::statistics m_st;
statistics() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
void reset() {
memset(this, 0, sizeof(*this));
m_st.reset();
}
void collect_statistics(::statistics& st) const {
st.update("arith-factorizations", m_num_factorizations);
st.update("arith-make-feasible", m_make_feasible);
Expand Down Expand Up @@ -157,7 +161,7 @@ struct statistics {
st.update("arith-nla-lemmas", m_nla_lemmas);
st.update("arith-nra-calls", m_nra_calls);
st.update("arith-bounds-improvements", m_nla_bounds_improvements);

st.copy(m_st);
}
};

Expand Down
11 changes: 9 additions & 2 deletions src/math/lp/nra_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ struct solver::imp {
scoped_ptr<scoped_anum_vector> m_values; // values provided by LRA solver
scoped_ptr<scoped_anum> m_tmp1, m_tmp2;
nla::core& m_nla_core;

imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core):
lra(s),
m_limit(lim),
Expand Down Expand Up @@ -180,6 +180,7 @@ struct solver::imp {
}

lbool r = l_undef;
statistics& st = m_nla_core.lp_settings().stats().m_st;
try {
r = m_nlsat->check();
}
Expand All @@ -188,9 +189,11 @@ struct solver::imp {
r = l_undef;
}
else {
m_nlsat->collect_statistics(st);
throw;
}
}
m_nlsat->collect_statistics(st);
TRACE("nra",
m_nlsat->display(tout << r << "\n");
display(tout);
Expand Down Expand Up @@ -234,6 +237,7 @@ struct solver::imp {
return r;
}


void add_monic_eq_bound(mon_eq const& m) {
if (!lra.column_has_lower_bound(m.var()) &&
!lra.column_has_upper_bound(m.var()))
Expand Down Expand Up @@ -374,6 +378,7 @@ struct solver::imp {
}

lbool r = l_undef;
statistics& st = m_nla_core.lp_settings().stats().m_st;
try {
r = m_nlsat->check();
}
Expand All @@ -382,9 +387,11 @@ struct solver::imp {
r = l_undef;
}
else {
m_nlsat->collect_statistics(st);
throw;
}
}
m_nlsat->collect_statistics(st);

switch (r) {
case l_true:
Expand Down Expand Up @@ -665,7 +672,7 @@ nlsat::anum_manager& solver::am() {
scoped_anum& solver::tmp1() { return m_imp->tmp1(); }

scoped_anum& solver::tmp2() { return m_imp->tmp2(); }


void solver::updt_params(params_ref& p) {
m_imp->updt_params(p);
Expand Down
15 changes: 8 additions & 7 deletions src/math/polynomial/algebraic_numbers.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2594,27 +2594,28 @@ namespace algebraic_numbers {

void int_lt(numeral const & a, numeral & b) {
scoped_mpz v(qm());
if (!a.is_basic())
refine_until_prec(const_cast<numeral&>(a), 1);
if (a.is_basic()) {
qm().floor(basic_value(a), v);
qm().dec(v);
}
else {
refine_until_prec(const_cast<numeral&>(a), 1);
bqm().floor(qm(), lower(a.to_algebraic()), v);
}
else
bqm().floor(qm(), lower(a.to_algebraic()), v);
m_wrapper.set(b, v);
}

void int_gt(numeral const & a, numeral & b) {
scoped_mpz v(qm());
if (!a.is_basic())
refine_until_prec(const_cast<numeral&>(a), 1);
if (a.is_basic()) {
qm().ceil(basic_value(a), v);
qm().inc(v);
}
else {
refine_until_prec(const_cast<numeral&>(a), 1);
else
bqm().ceil(qm(), upper(a.to_algebraic()), v);
}

m_wrapper.set(b, v);
}

Expand Down
135 changes: 123 additions & 12 deletions src/math/polynomial/polynomial.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2504,30 +2504,139 @@ namespace polynomial {
return p;
}

void gcd_simplify(polynomial * p) {
if (m_manager.finite()) return;
void gcd_simplify(polynomial_ref& p, manager::ineq_type t) {
auto& m = m_manager.m();
unsigned sz = p->size();
if (sz == 0)
return;
unsigned g = 0;
for (unsigned i = 0; i < sz; i++) {
for (unsigned i = 0; i < sz; i++) {
if (!m.is_int(p->a(i))) {
gcd_simplify_slow(p, t);
return;
}
if (t != EQ && is_unit(p->m(i)))
continue;
int j = m.get_int(p->a(i));
if (j == INT_MIN || j == 1 || j == -1)
if (j == INT_MIN) {
gcd_simplify_slow(p, t);
return;
}
if (j == 1 || j == -1)
return;
g = u_gcd(abs(j), g);
if (g == 1)
return;
}
scoped_mpz r(m), gg(m);
scoped_mpz gg(m);
m.set(gg, g);
apply_gcd_simplify(gg, p, t);
}

void apply_gcd_simplify(mpz & g, polynomial_ref& p, manager::ineq_type t) {

auto& m = m_manager.m();

#if 0
m.display(verbose_stream() << "gcd ", g);
p->display(verbose_stream() << "\n", m_manager, false);
char const* tt = "";
switch (t) {
case ineq_type::GT: tt = ">"; break;
case ineq_type::LT: tt = "<"; break;
case ineq_type::EQ: tt = "="; break;
}
verbose_stream() << " " << tt << " 0\n ->\n";
#endif
scoped_mpz r(m);
unsigned sz = p->size();
m_som_buffer.reset();
for (unsigned i = 0; i < sz; ++i) {
m.div_gcd(p->a(i), gg, r);
m.set(p->a(i), r);
if (t != EQ && is_unit(p->m(i))) {
scoped_mpz one(m);
m.set(one, 1);
if (t == GT) {
// p - 2 - 1 >= 0
// p div 2 + floor((-2 - 1 ) / 2) >= 0
// p div 2 + floor(-3 / 2) >= 0
// p div 2 - 2 >= 0
// p div 2 - 1 > 0
//
// p + k > 0
// p + k - 1 >= 0
// p div g + (k - 1) div g >= 0
// p div g + (k - 1) div g + 1 > 0
m.sub(p->a(i), one, r);
bool is_neg = m.is_neg(r);
if (is_neg) {
m.neg(r);
m.add(r, g, r);
m.sub(r, one, r);
m.div_gcd(r, g, r);
m.neg(r);
}
else {
m.div_gcd(r, g, r);
}
m.add(r, one, r);
}
else {
// p + k < 0
// p + k + 1 <= 0
// p div g + (k + 1 + g - 1) div g <= 0
// p div g + (k + 1 + g - 1) div g - 1 < 0

m.add(p->a(i), one, r);
bool is_neg = m.is_neg(r);

if (is_neg) {
// p - k <= 0
// p <= k
// p div g <= k div g
// p div g - k div g <= 0
// p div g - k div g - 1 < 0
m.neg(r);
m.div_gcd(r, g, r);
m.neg(r);
m.sub(r, one, r);
}
else {
m.div_gcd(p->a(i), g, r);
m.add(p->a(i), g, r);
m.div_gcd(r, g, r);
m.sub(r, one, r);
}

}
}
else {
m.div_gcd(p->a(i), g, r);
}
if (!m.is_zero(r))
m_som_buffer.add(r, p->m(i));
}
p = m_som_buffer.mk();

// p->display(verbose_stream(), m_manager, false);
// verbose_stream() << " " << tt << " 0\n";
}

void gcd_simplify_slow(polynomial_ref& p, manager::ineq_type t) {
auto& m = m_manager.m();
unsigned sz = p->size();
scoped_mpz g(m);
m.set(g, 0);
for (unsigned i = 0; i < sz; i++) {
auto const& a = p->a(i);
if (m.is_one(a) || m.is_minus_one(a))
return;
if (t != EQ && is_unit(p->m(i)))
continue;
m.gcd(a, g, g);
if (m.is_one(g))
return;
}
apply_gcd_simplify(g, p, t);
}

polynomial * mk_zero() {
Expand Down Expand Up @@ -6087,9 +6196,11 @@ namespace polynomial {
}
return false;
}
if (!m_manager.ge(a1, a2))
return false;
++i, ++j;
if (m_manager.eq(a1, a2) || (m1->is_square() && m_manager.ge(a1, a2))) {
++i, ++j;
continue;
}
return false;
}
return i == sz1 && j == sz2;
}
Expand Down Expand Up @@ -6971,8 +7082,8 @@ namespace polynomial {
return m_imp->hash(p);
}

void manager::gcd_simplify(polynomial * p) {
m_imp->gcd_simplify(p);
void manager::gcd_simplify(polynomial_ref& p, ineq_type t) {
m_imp->gcd_simplify(p, t);
}

polynomial * manager::coeff(polynomial const * p, var x, unsigned k) {
Expand Down
3 changes: 2 additions & 1 deletion src/math/polynomial/polynomial.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -285,7 +285,8 @@ namespace polynomial {
/**
\brief Normalize coefficients by dividing by their gcd
*/
void gcd_simplify(polynomial* p);
enum ineq_type { EQ, LT, GT };
void gcd_simplify(polynomial_ref& p, ineq_type t);

/**
\brief Return true if \c m is the unit monomial.
Expand Down
15 changes: 4 additions & 11 deletions src/math/polynomial/polynomial_cache.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,20 +117,14 @@ namespace polynomial {
}

void reset_psc_chain_cache() {
psc_chain_cache::iterator it = m_psc_chain_cache.begin();
psc_chain_cache::iterator end = m_psc_chain_cache.end();
for (; it != end; ++it) {
del_psc_chain_entry(*it);
}
for (auto & k : m_psc_chain_cache)
del_psc_chain_entry(k);
m_psc_chain_cache.reset();
}

void reset_factor_cache() {
factor_cache::iterator it = m_factor_cache.begin();
factor_cache::iterator end = m_factor_cache.end();
for (; it != end; ++it) {
del_factor_entry(*it);
}
for (auto & e : m_factor_cache)
del_factor_entry(e);
m_factor_cache.reset();
}

Expand All @@ -139,7 +133,6 @@ namespace polynomial {
polynomial * mk_unique(polynomial * p) {
if (m_in_cache.get(pid(p), false))
return p;
// m.gcd_simplify(p);
polynomial * p_prime = m_poly_table.insert_if_not_there(p);
if (p == p_prime) {
m_cached_polys.push_back(p_prime);
Expand Down
1 change: 1 addition & 0 deletions src/nlsat/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ z3_add_component(nlsat
nlsat_evaluator.cpp
nlsat_explain.cpp
nlsat_interval_set.cpp
nlsat_simplify.cpp
nlsat_solver.cpp
nlsat_types.cpp
COMPONENT_DEPENDENCIES
Expand Down

0 comments on commit 8fe357f

Please sign in to comment.