mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

remove nex grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-31 14:47:26 -08:00
parent 2334ed5b66
commit 496a8c17aa
7 changed files with 3 additions and 996 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/CMakeLists.txt
View file

@ -30,7 +30,6 @@ z3_add_component(lp
nla_basics_lemmas.cpp
nla_common.cpp
nla_core.cpp
nla_grobner.cpp
nla_intervals.cpp
nla_monotone_lemmas.cpp
nla_order_lemmas.cpp

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

@ -34,7 +34,6 @@ core::core(lp::lar_solver& s, reslimit & lim) :
m_monotone(this),
m_intervals(this, lim),
m_horner(this, &m_intervals),
m_nex_grobner(this, &m_intervals),
m_pdd_manager(s.number_of_vars()),
m_pdd_grobner(lim, m_pdd_manager),
m_emons(m_evars),
@ -1626,14 +1625,6 @@ void core::display_matrix_of_m_rows(std::ostream & out) const {
}
}
void core::init_nex_grobner(nex_creator & nc) {
m_nex_grobner.init();
set_active_vars_weights(nc);
for (unsigned i : m_rows) {
m_nex_grobner.add_row(m_lar_solver.A_r().m_rows[i]);
}
}
void core::set_active_vars_weights(nex_creator& nc) {
nc.set_number_of_vars(m_lar_solver.column_count());
for (lpvar j : active_var_set()) {

3
src/math/lp/nla_core.h
View file

@ -29,7 +29,6 @@
#include "math/lp/nla_settings.h"
#include "math/lp/nex.h"
#include "math/lp/horner.h"
#include "math/lp/nla_grobner.h"
#include "math/lp/nla_intervals.h"
#include "math/grobner/pdd_grobner.h"
@ -95,7 +94,6 @@ public:
intervals m_intervals;
horner m_horner;
nla_settings m_nla_settings;
grobner m_nex_grobner;
dd::pdd_manager m_pdd_manager;
dd::grobner m_pdd_grobner;
@ -405,7 +403,6 @@ public:
void find_nl_cluster();
void prepare_rows_and_active_vars();
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar>& q);
void init_nex_grobner(nex_creator&);
std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
void display_matrix_of_m_rows(std::ostream & out) const;
void set_active_vars_weights(nex_creator&);

746
src/math/lp/nla_grobner.cpp
View file

@ -1,746 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
Revision History:
--*/
#include "math/lp/nla_grobner.h"
#include "math/lp/nla_core.h"
#include "math/lp/factorization_factory_imp.h"
using namespace nla;
grobner::grobner(core *c, intervals *s)
: common(c, s),
m_gc(m_nex_creator, c->m_reslim) {
std::function<void (lp::explanation const& e, std::ostream & out)> de;
de = [this](lp::explanation const& e, std::ostream& out) { m_core->print_explanation(e, out); };
grobner_core::params p;
p.m_expr_size_limit = c->m_nla_settings.grobner_expr_size_limit();
p.m_grobner_eqs_threshold = c->m_nla_settings.grobner_eqs_threshold();
m_gc = de;
m_gc = p;
}
void grobner::grobner_lemmas() {
c().lp_settings().stats().m_grobner_calls++;
m_reported = 0;
TRACE("grobner", tout << "before:\n"; display(tout););
m_gc.compute_basis_loop();
for (grobner_core::equation* e : m_gc.equations()) {
check_eq(e);
}
TRACE("grobner", tout << "after:\n"; display(tout););
}
void grobner::check_eq(grobner_core::equation* target) {
if (m_intervals->check_nex(target->expr(), target->dep())) {
TRACE("grobner", tout << "created a lemma for "; m_gc.display_equation(tout, *target) << "\n";
tout << "vars = \n";
for (lpvar j : get_vars_of_expr(target->expr())) {
c().print_var(j, tout);
}
tout << "\ntarget->expr() val = " << get_nex_val(target->expr(), [this](unsigned j) { return c().val(j); }) << "\n";);
c().lp_settings().stats().m_grobner_conflicts++;
}
}
void grobner::add_row(const vector<lp::row_cell<rational>> & row) {
TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n';
for (auto p : row) c().print_var(p.var(), tout) << "\n"; );
nex_creator::sum_factory sf(m_nex_creator);
u_dependency* dep = create_sum_from_row(row, m_nex_creator, sf, &m_gc.dep());
nex* e = m_nex_creator.simplify(sf.mk());
TRACE("grobner", tout << "e = " << *e << "\n";);
m_gc.assert_eq_0(e, dep);
}
/// -------------------------------
/// grobner_core
/***
The main algorithm maintains two sets (S, A),
where S is m_to_superpose, and A is m_to_simplify.
Initially S is empty and A contains the initial equations.
Each step proceeds as follows:
- pick a in A, and remove a from A
- simplify a using S
- simplify S using a
- for s in S:
b = superpose(a, s)
add b to A
- add a to S
- simplify A using a
*/
void grobner::init() {
m_gc.reset();
}
bool grobner_core::compute_basis_loop() {
while (!done()) {
if (compute_basis_step()) {
TRACE("grobner", tout << "progress in compute_basis_step\n";);
return true;
}
TRACE("grobner", tout << "continue compute_basis_loop\n";);
}
TRACE("grobner", tout << "return false from compute_basis_loop\n";);
TRACE("grobner_stats", print_stats(tout););
return false;
}
// return true iff cannot pick_next()
bool grobner_core::compute_basis_step() {
equation* eq = pick_next();
if (!eq) {
TRACE("grobner", tout << "cannot pick an equation\n";);
return true;
}
m_stats.m_compute_steps++;
simplify_eq_by_using_to_superpose(*eq);
if (equation_is_too_complex(eq)) {
return false;
}
if (!simplify_to_superpose_with_eq(eq)) {
return false;
}
TRACE("grobner", tout << "eq = "; display_equation(tout, *eq););
superpose(eq);
if (equation_is_too_complex(eq)) {
TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";);
del_equation(eq);
return false;
}
insert_to_superpose(eq);
simplify_m_to_simplify(eq);
TRACE("grobner", tout << "end of iteration:\n"; display(tout););
return false;
}
grobner_core::equation* grobner_core::pick_next() {
equation* r = nullptr;
ptr_buffer<equation> to_delete;
for (equation* curr : m_to_simplify) {
if (is_trivial(curr))
to_delete.push_back(curr);
else if (is_simpler(curr, r)) {
TRACE("grobner", tout << "preferring " << *(curr->expr()) << "\n";);;
r = curr;
}
}
for (equation* e : to_delete)
del_equation(e);
if (r)
m_to_simplify.erase(r);
TRACE("grobner", tout << "selected equation: "; if (!r) tout << "<null>\n"; else tout << *r->expr() << "\n";);
return r;
}
void grobner_core::simplify_eq_by_using_to_superpose(equation& eq) {
bool simplified;
TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
do {
simplified = false;
for (equation* p : m_to_superpose) {
if (simplify_source_target(*p, eq)) {
simplified = true;
}
if (canceled() || eq.expr()->is_scalar()) {
break;
}
}
} while (simplified && !eq.expr()->is_scalar());
TRACE("grobner",
if (simplified) { tout << "simplification result: "; display_equation(tout, eq); }
else { tout << "no simplification\n"; });
}
concat<grobner_core::equation_set, grobner_core::equation_set, grobner_core::equation*> grobner_core::equations() {
return concat<grobner_core::equation_set, grobner_core::equation_set, grobner_core::equation*>(m_to_superpose, m_to_simplify);
}
void grobner_core::reset() {
del_equations(0);
m_nex_creator.pop(0);
SASSERT(m_equations_to_delete.empty());
m_to_superpose.reset();
m_to_simplify.reset();
m_stats.reset();
}
// Return true if the equation is of the form 0 = 0.
bool grobner_core::is_trivial(equation* eq) const {
return eq->expr()->is_scalar() && eq->expr()->to_scalar().value().is_zero();
}
// returns true if eq1 is simpler than eq2
bool grobner_core::is_simpler(equation * eq1, equation * eq2) {
if (!eq2)
return true;
if (is_trivial(eq1))
return true;
if (is_trivial(eq2))
return false;
return m_nex_creator.gt(eq2->expr(), eq1->expr());
}
void grobner_core::del_equation(equation * eq) {
m_to_superpose.erase(eq);
m_to_simplify.erase(eq);
SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
m_equations_to_delete[eq->m_bidx] = nullptr;
dealloc(eq);
}
const nex* grobner_core::get_highest_monomial(const nex* e) const {
switch (e->type()) {
case expr_type::MUL:
return e;
case expr_type::SUM:
return e->to_sum()[0];
case expr_type::VAR:
return e;
default:
TRACE("grobner", tout << *e << "\n";);
return nullptr;
}
}
// source 3f + k + l = 0, so f = (-k - l)/3
// target 2fg + 3fp + e = 0
// target is replaced by 2(-k/3 - l/3)g + 3(-k/3 - l/3)p + e = -2/3kg -2/3lg - kp -lp + e
bool grobner_core::simplify_target_monomials(equation const& source, equation& target) {
nex const* high_mon = get_highest_monomial(source.expr());
if (high_mon == nullptr)
return false;
SASSERT(high_mon->all_factors_are_elementary());
TRACE("grobner_d", tout << "source = "; display_equation(tout, source) << "target = "; display_equation(tout, target) << "high_mon = " << *high_mon << "\n";);
nex * te = target.m_expr;
nex_sum * targ_sum;
if (te->is_sum()) {
targ_sum = to_sum(te);
} else if (te->is_mul()) {
targ_sum = m_nex_creator.mk_sum(te);
} else {
TRACE("grobner_d", tout << "return false\n";);
return false;
}
return simplify_target_monomials_sum(source, target, *targ_sum, *high_mon);
}
unsigned grobner_core::find_divisible(nex_sum const& targ_sum, const nex& high_mon) const {
unsigned j = 0;
for (auto t : targ_sum) {
if (divide_ignore_coeffs_check_only(*t, high_mon)) {
TRACE("grobner_d", tout << "yes div: " << *t << " / " << high_mon << "\n";);
return j;
}
++j;
}
TRACE("grobner_d", tout << "no div: " << targ_sum << " / " << high_mon << "\n";);
return -1;
}
bool grobner_core::simplify_target_monomials_sum(equation const& source,
equation& target, nex_sum& targ_sum,
const nex& high_mon) {
unsigned j = find_divisible(targ_sum, high_mon);
if (j + 1 == 0)
return false;
m_changed_leading_term = (j == 0);
unsigned targ_orig_size = targ_sum.size();
simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j, false); // false to avoid divisibility test
for (j++; j < targ_orig_size; j++) {
simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j, true);
}
TRACE("grobner_d", tout << "targ_sum = " << targ_sum << "\n";);
target.m_expr = m_nex_creator.simplify(&targ_sum);
target.m_dep = m_dep_manager.mk_join(source.dep(), target.dep());
TRACE("grobner_d", tout << "target = "; display_equation(tout, target););
return true;
}
bool grobner_core::divide_ignore_coeffs_check_only_nex_mul(nex_mul const& t, const nex& h) const {
TRACE("grobner_d", tout << "t = " << t << ", h=" << h << "\n";);
SASSERT(m_nex_creator.is_simplified(t) && m_nex_creator.is_simplified(h));
unsigned j = 0; // points to t
for(unsigned k = 0; k < h.number_of_child_powers(); k++) {
lpvar h_var = h.get_child_exp(k)->to_var().var();
bool p_swallowed = false;
for (; j < t.size() && !p_swallowed; j++) {
const nex_pow& tp = t[j];
if (tp.e()->to_var().var() == h_var) {
if (tp.pow() >= h.get_child_pow(k)) {
p_swallowed = true;
}
}
}
if (!p_swallowed) {
TRACE("grobner_d", tout << "no div " << t << " / " << h << "\n";);
return false;
}
}
TRACE("grobner_d", tout << "division " << t << " / " << h << "\n";);
return true;
}
// return true if h divides n
bool grobner_core::divide_ignore_coeffs_check_only(nex const& n , const nex& h) const {
if (n.is_mul())
return divide_ignore_coeffs_check_only_nex_mul(n.to_mul(), h);
if (!n.is_var())
return false;
const nex_var& v = n.to_var();
if (h.is_var()) {
return v.var() == h.to_var().var();
}
if (h.is_mul()) {
if (h.number_of_child_powers() > 1)
return false;
if (h.get_child_pow(0) != 1)
return false;
const nex* e = h.get_child_exp(0);
return e->is_var() && e->to_var().var() == v.var();
}
return false;
}
nex_mul * grobner_core::divide_ignore_coeffs_perform_nex_mul(nex_mul const& t, const nex& h) {
m_nex_creator.m_mk_mul.reset();
unsigned j = 0; // j points to t and k runs over h
for(unsigned k = 0; k < h.number_of_child_powers(); k++) {
lpvar h_var = to_var(h.get_child_exp(k))->var();
for (; j < t.size(); j++) {
auto const &tp = t[j];
if (tp.e()->to_var().var() == h_var) {
unsigned h_pow = h.get_child_pow(k);
SASSERT(tp.pow() >= h_pow);
j++;
if (tp.pow() > h_pow) {
m_nex_creator.m_mk_mul *= nex_pow(tp.e(), tp.pow() - h_pow);
}
break;
} else {
m_nex_creator.m_mk_mul *= tp;
}
}
}
for (; j < t.size(); j++) {
m_nex_creator.m_mk_mul *= t[j];
}
nex_mul* r = m_nex_creator.m_mk_mul.mk();
TRACE("grobner", tout << "r = " << *r << " = " << t << " / " << h << "\n";);
TRACE("grobner_d", tout << "r = " << *r << " = " << t << " / " << h << "\n";);
return r;
}
// perform the division t / h, but ignores the coefficients
// h does not change
nex_mul * grobner_core::divide_ignore_coeffs_perform(nex* e, const nex& h) {
if (e->is_mul())
return divide_ignore_coeffs_perform_nex_mul(e->to_mul(), h);
SASSERT(e->is_var());
return m_nex_creator.mk_mul(); // return the empty nex_mul
}
// if targ_sum->children()[j] = c*high_mon*p,
// and b*high_mon + e = 0, so high_mon = -e/b
// then targ_sum->children()[j] = - (c/b) * e*p
void grobner_core::simplify_target_monomials_sum_j(equation const& source, equation& target, nex_sum& targ_sum, const nex& high_mon, unsigned j, bool test_divisibility) {
nex * ej = targ_sum[j];
TRACE("grobner_d", tout << "high_mon = " << high_mon << ", ej = " << *ej << "\n";);
if (test_divisibility && !divide_ignore_coeffs_check_only(*ej, high_mon)) {
TRACE("grobner_d", tout << "no div\n";);
return;
}
nex_mul * ej_over_high_mon = divide_ignore_coeffs_perform(ej, high_mon);
TRACE("grobner_d", tout << "ej_over_high_mon = " << *ej_over_high_mon << "\n";);
rational c = ej->is_mul() ? to_mul(ej)->coeff() : rational(1);
TRACE("grobner_d", tout << "c = " << c << "\n";);
nex_creator::sum_factory sf(m_nex_creator);
add_mul_skip_first(sf ,-c/high_mon.coeff(), source.expr(), ej_over_high_mon);
targ_sum[j] = sf.mk();
TRACE("grobner_d", tout << "targ_sum = " << targ_sum << "\n";);
}
// return true iff simplified
bool grobner_core::simplify_source_target(equation const& source, equation& target) {
TRACE("grobner", tout << "simplifying: "; display_equation(tout, target); tout << "\nusing: "; display_equation(tout, source););
TRACE("grobner_d", tout << "simplifying: " << *(target.expr()) << " using " << *(source.expr()) << "\n";);
SASSERT(m_nex_creator.is_simplified(*source.expr()) && !equation_is_too_complex(&source));
if (equation_is_too_complex(&target))
return false;
SASSERT(m_nex_creator.is_simplified(*target.expr()));
if (target.expr()->is_scalar()) {
TRACE("grobner_d", tout << "no simplification\n";);
return false;
}
if (source.get_num_monomials() == 0) {
TRACE("grobner_d", tout << "no simplification\n";);
return false;
}
m_stats.m_simplified++;
bool result = false;
while (!canceled() && simplify_target_monomials(source, target)) {
TRACE("grobner", tout << "simplified target = "; display_equation(tout, target) << "\n";);
result = true;
}
if (result) {
target.m_dep = m_dep_manager.mk_join(target.dep(), source.dep());
update_stats_max_degree_and_size(&target);
TRACE("grobner", tout << "simplified "; display_equation(tout, target) << "\n";);
TRACE("grobner_d", tout << "simplified to " << *(target.expr()) << "\n";);
return true;
}
TRACE("grobner_d", tout << "no simplification\n";);
return false;
}
void grobner_core::process_simplified_target(equation* target, ptr_buffer<equation>& to_remove) {
if (is_trivial(target) || equation_is_too_complex(target)) {
to_remove.push_back(target);
} else if (m_changed_leading_term) {
insert_to_simplify(target);
to_remove.push_back(target);
}
}
bool grobner_core::simplify_to_superpose_with_eq(equation* eq) {
TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";);
SASSERT(!equation_is_too_complex(eq));
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
for (equation * target : m_to_superpose) {
if (canceled() || done())
break;
m_changed_leading_term = false;
// if the leading term is simplified, then the equation has to be moved to m_to_simplify
if (simplify_source_target(*eq, *target)) {
process_simplified_target(target, to_remove);
}
if (is_trivial(target)||equation_is_too_complex(target)) {
to_delete.push_back(target);
}
else {
SASSERT(m_nex_creator.is_simplified(*target->expr()));
}
}
for (equation* eq : to_remove)
m_to_superpose.erase(eq);
for (equation* eq : to_delete)
del_equation(eq);
return !canceled();
}
/*
Use the given equation to simplify m_to_simplify equations
*/
void grobner_core::simplify_m_to_simplify(equation* eq) {
TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";);
ptr_buffer<equation> to_delete;
for (equation* target : m_to_simplify) {
if (simplify_source_target(*eq, *target) && (is_trivial(target) || equation_is_too_complex(target)))
to_delete.push_back(target);
}
for (equation* eq : to_delete)
del_equation(eq);
}
// if e is the sum then add to r all children of e multiplied by beta, except the first one
// which corresponds to the highest monomial,
// otherwise do nothing
void grobner_core::add_mul_skip_first(nex_creator::sum_factory& sf, const rational& beta, nex const*e, nex_mul* c) {
if (e->is_sum()) {
nex_sum const & es = e->to_sum();
for (unsigned j = 1; j < es.size(); j++) {
sf += m_nex_creator.mk_mul(beta, es[j], c);
}
} else {
TRACE("grobner_d", tout << "e = " << *e << "\n";);
}
}
// let e1: alpha*ab+q=0, and e2: beta*ac+e=0, then beta*qc - alpha*eb = 0
nex * grobner_core::expr_superpose(nex const* e1, nex const* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c) {
TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\n";);
nex_creator::sum_factory sf(m_nex_creator);
rational alpha = - ab->coeff();
TRACE("grobner", tout << "e2 *= " << alpha << "*(" << *b << ")\n";);
add_mul_skip_first(sf, alpha, e2, b);
rational beta = ac->coeff();
TRACE("grobner", tout << "e1 *= " << beta << "*(" << *c << ")\n";);
add_mul_skip_first(sf, beta, e1, c);
nex * ret = m_nex_creator.simplify(sf.mk());
TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\nsuperpose = " << *ret << "\n";);
CTRACE("grobner", ret->is_scalar(), tout << "\n";);
return ret;
}
// let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
void grobner_core::superpose(equation * eq1, equation * eq2) {
TRACE("grobner_d", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2););
const nex * ab = get_highest_monomial(eq1->expr());
const nex * ac = get_highest_monomial(eq2->expr());
nex_mul *b = nullptr, *c = nullptr;
TRACE("grobner_d", tout << "ab="; if(ab) { tout << *ab; } else { tout << "null"; };
tout << " , " << " ac="; if(ac) { tout << *ac; } else { tout << "null"; }; tout << "\n";);
if (!find_b_c(ab, ac, b, c)) {
TRACE("grobner_d", tout << "there is no non-trivial common divider, no superposing\n";);
return;
}
equation* eq = alloc(equation);
TRACE("grobner_d", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2););
init_equation(eq, expr_superpose(eq1->expr(), eq2->expr(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep()));
if (m_nex_creator.gt(eq->expr(), eq1->expr()) || m_nex_creator.gt(eq->expr(), eq2->expr()) ||
equation_is_too_complex(eq)) {
TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";);
del_equation(eq);
} else {
m_stats.m_superposed++;
update_stats_max_degree_and_size(eq);
insert_to_simplify(eq);
}
}
// Let a be the greatest common divider of ab and bc,
// then ab/a is stored in b, and ac/a is stored in c
bool grobner_core::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) {
if (!find_b_c_check_only(ab, ac))
return false;
nex_creator::mul_factory fb(m_nex_creator), fc(m_nex_creator);
unsigned ab_size = ab->number_of_child_powers();
unsigned ac_size = ac->number_of_child_powers();
unsigned i = 0, j = 0;
for (;;) {
const nex* m = ab->get_child_exp(i);
const nex* n = ac->get_child_exp(j);
if (m_nex_creator.gt(m, n)) {
fb *= nex_pow(const_cast<nex*>(m), ab->get_child_pow(i));
if (++i == ab_size)
break;
} else if (m_nex_creator.gt(n, m)) {
fc *= nex_pow(const_cast<nex*>(n), ac->get_child_pow(j));
if (++j == ac_size)
break;
} else {
unsigned b_pow = ab->get_child_pow(i);
unsigned c_pow = ac->get_child_pow(j);
if (b_pow > c_pow) {
fb *= nex_pow(const_cast<nex*>(m), b_pow - c_pow);
} else if (c_pow > b_pow) {
fc *= nex_pow(const_cast<nex*>(n), c_pow - b_pow);
} // otherwise the power are equal and no child added to either b or c
i++; j++;
if (i == ab_size || j == ac_size) {
break;
}
}
}
while (i != ab_size) {
fb *= nex_pow(const_cast<nex*>(ab->get_child_exp(i)), ab->get_child_pow(i));
i++;
}
while (j != ac_size) {
fc *= nex_pow(const_cast<nex*>(ac->get_child_exp(j)), ac->get_child_pow(j));
j++;
}
b = fb.mk();
c = fc.mk();
TRACE("nla_grobner", tout << "b=" << *b << ", c=" <<*c << "\n";);
SASSERT(test_find_b_c(ab, ac, b, c));
return true;
}
// Finds out if ab and bc have a non-trivial common divider
bool grobner_core::find_b_c_check_only(const nex* ab, const nex* ac) const {
if (ab == nullptr || ac == nullptr)
return false;
SASSERT(m_nex_creator.is_simplified(*ab) && m_nex_creator.is_simplified(*ac));
unsigned i = 0, j = 0; // i points to ab, j points to ac
for (;;) {
const nex* m = ab->get_child_exp(i);
const nex* n = ac->get_child_exp(j);
if (m_nex_creator.gt(m , n)) {
i++;
if (i == ab->number_of_child_powers())
return false;
} else if (m_nex_creator.gt(n, m)) {
j++;
if (j == ac->number_of_child_powers())
return false;
} else {
TRACE("grobner", tout << "found common " << *m << "\n";);
return true;
}
}
TRACE("grobner", tout << "not found common " << " in " << *ab << " and " << *ac << "\n";);
return false;
}
void grobner_core::superpose(equation * eq) {
for (equation * target : m_to_superpose) {
superpose(eq, target);
}
}
bool grobner_core::canceled() {
return m_limit.get_cancel_flag();
}
bool grobner_core::done() {
return num_of_equations() >= m_params.m_grobner_eqs_threshold || canceled();
}
void grobner_core::del_equations(unsigned old_size) {
TRACE("grobner", );
SASSERT(m_equations_to_delete.size() >= old_size);
for (unsigned i = m_equations_to_delete.size(); i-- > old_size; ) {
equation* eq = m_equations_to_delete[i];
if (eq)
del_equation(eq);
}
m_equations_to_delete.shrink(old_size);
}
std::ostream& grobner_core::print_stats(std::ostream & out) const {
return out << "stats:\nsteps = " << m_stats.m_compute_steps << "\nsimplified: " <<
m_stats.m_simplified << "\nsuperposed: " <<
m_stats.m_superposed << "\nexpr degree: " << m_stats.m_max_expr_degree <<
"\nexpr size: " << m_stats.m_max_expr_size << "\n";
}
void grobner_core::update_stats_max_degree_and_size(const equation *e) {
if (m_stats.m_max_expr_size < e->expr()->size()) {
TRACE("grobner_stats_d", tout << "expr size = " << e->expr()->size() << "\n";);
TRACE("grobner_stats_d", display_equation(tout, *e););
m_stats.m_max_expr_size = e->expr()->size();
}
auto deg = e->expr()->get_degree();
if (m_stats.m_max_expr_degree < deg) {
TRACE("grobner_stats_d", tout << "expr degree = " << deg << "\n";);
m_stats.m_max_expr_degree = deg;
}
}
void grobner_core::display_equations(std::ostream & out, equation_set const & v, char const * header) const {
out << header << "\n";
for (const equation* e : v)
display_equation(out, *e);
}
void grobner_core::display_equations_no_deps(std::ostream & out, equation_set const & v, char const * header) const {
out << header << "\n";
for (const equation* e : v)
out << *(e->expr()) << "\n";
}
std::ostream& grobner_core::display_equation(std::ostream & out, const equation & eq) const {
out << "expr = " << *eq.expr() << "\n";
return display_dependency(out, eq.dep());
}
std::ostream& grobner_core::display(std::ostream& out) const {
display_equations_no_deps(out, m_to_superpose, "m_to_superpose:");
display_equations_no_deps(out, m_to_simplify, "m_to_simplify:");
return out;
}
void grobner_core::assert_eq_0(nex* e, u_dependency * dep) {
if (e == nullptr || is_zero_scalar(e))
return;
equation * eq = alloc(equation);
init_equation(eq, e, dep);
TRACE("grobner",
display_equation(tout, *eq);
/*tout << "\nvars\n";
for (unsigned j : get_vars_of_expr_with_opening_terms(e)) {
c().print_var(j, tout << "(") << ")\n";
} */);
insert_to_simplify(eq);
update_stats_max_degree_and_size(eq);
}
void grobner_core::init_equation(equation* eq, nex*e, u_dependency * dep) {
eq->m_bidx = m_equations_to_delete.size();
eq->m_dep = dep;
eq->m_expr = e;
m_equations_to_delete.push_back(eq);
SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
}
grobner_core::~grobner_core() {
del_equations(0);
}
std::ostream& grobner_core::display_dependency(std::ostream& out, u_dependency* dep) const {
svector<lp::constraint_index> expl;
m_dep_manager.linearize(dep, expl);
lp::explanation e(expl);
if (!expl.empty()) {
out << "constraints\n";
m_print_explanation(e, out);
out << "\n";
} else {
out << "no deps\n";
}
return out;
}
#ifdef Z3DEBUG
bool grobner_core::test_find_b(const nex* ab, const nex_mul* b) {
if (ab->is_var()) {
return b->size() == 0 || (b->get_degree() == 1 && b->get_child_exp(0)->to_var().var() ==
ab->to_var().var());
}
nex_mul& ab_clone = m_nex_creator.clone(ab)->to_mul();
nex_mul * a= divide_ignore_coeffs_perform(&ab_clone, *b);
ab_clone.m_coeff = rational(1);
SASSERT(b->coeff().is_one());
nex * m = m_nex_creator.mk_mul(a, m_nex_creator.clone(b));
m = m_nex_creator.simplify(m);
return m_nex_creator.equal(m, &ab_clone);
}
bool grobner_core::test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c) {
return test_find_b(ab, b) && test_find_b(ac, c);
}
#endif

224
src/math/lp/nla_grobner.h
View file

@ -1,224 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
Revision History:
--*/
#pragma once
#include "math/lp/nla_common.h"
#include "math/lp/nex.h"
#include "math/lp/nex_creator.h"
namespace nla {
class core;
struct grobner_stats {
long m_simplified;
long m_superposed;
long m_compute_steps;
unsigned m_max_expr_size;
unsigned m_max_expr_degree;
void reset() { memset(this, 0, sizeof(grobner_stats)); }
grobner_stats() { reset(); }
};
template <typename A, typename B, typename C>
class concat {
const A& m_a; // the first container
const B& m_b; // the second container
public:
class iterator {
const concat& m_c;
typename A::iterator m_a_it;
typename B::iterator m_b_it;
public:
iterator(const concat& c, bool begin):
m_c(c), m_a_it(begin? m_c.m_a.begin() : m_c.m_a.end()), m_b_it(begin? m_c.m_b.begin() : m_c.m_b.end()) {}
const C operator*() { return m_a_it != m_c.m_a.end() ? *m_a_it : *m_b_it; }
iterator& operator++() {
if (m_a_it != m_c.m_a.end())
m_a_it++;
else
m_b_it++;
return *this;
}
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& other) const { return m_a_it == other.m_a_it && m_b_it == other.m_b_it; }
bool operator!=(iterator const& other) const { return m_a_it != other.m_a_it || m_b_it != other.m_b_it; }
};
concat(const A& a, const B& b) : m_a(a), m_b(b) {}
iterator begin() { return iterator(*this, true); }
iterator end() { return iterator(*this, false); }
};
class grobner_core {
public:
struct params {
unsigned m_grobner_eqs_threshold;
unsigned m_expr_size_limit;
};
class equation {
unsigned m_bidx; //!< position at m_equations_to_delete
nex * m_expr; // simplified expressionted monomials
u_dependency * m_dep; //!< justification for the equality
public:
unsigned get_num_monomials() const {
switch(m_expr->type()) {
case expr_type::VAR: return 1;
case expr_type::SCALAR: return 0;
case expr_type::MUL: return 1;
case expr_type::SUM: return m_expr->size();
default: return 0;
}
}
// not guaranteed to return a nex_mul
nex const* get_monomial(unsigned idx) const {
switch(m_expr->type()) {
case expr_type::VAR:
case expr_type::SCALAR: UNREACHABLE();;
case expr_type::MUL:
SASSERT(idx == 0);
return m_expr;
case expr_type::SUM:
return m_expr->to_sum()[idx];
default: return nullptr;
}
}
const nex* expr() const { return m_expr; }
u_dependency * dep() const { return m_dep; }
unsigned hash() const { return m_bidx; }
friend class grobner_core;
};
private:
typedef obj_hashtable<equation> equation_set;
typedef ptr_vector<equation> equation_vector;
typedef std::function<void (lp::explanation const& e, std::ostream& out)> print_expl_t;
// fields
nex_creator& m_nex_creator;
reslimit& m_limit;
print_expl_t m_print_explanation;
equation_vector m_equations_to_delete;
grobner_stats m_stats;
equation_set m_to_superpose;
equation_set m_to_simplify;
region m_alloc;
mutable u_dependency_manager m_dep_manager;
nex_lt m_lt;
bool m_changed_leading_term;
params m_params;
public:
grobner_core(nex_creator& nc, reslimit& lim) :
m_nex_creator(nc),
m_limit(lim),
m_dep_manager(),
m_changed_leading_term(false)
{}
~grobner_core();
void reset();
bool compute_basis_loop();
void assert_eq_0(nex*, u_dependency * dep);
concat<equation_set, equation_set, equation*> equations();
u_dependency_manager& dep() const { return m_dep_manager; }
void display_equations_no_deps(std::ostream& out, equation_set const& v, char const* header) const;
void display_equations(std::ostream& out, equation_set const& v, char const* header) const;
std::ostream& display_equation(std::ostream& out, const equation& eq) const;
std::ostream& display(std::ostream& out) const;
void operator=(print_expl_t& pe) { m_print_explanation = pe; }
void operator=(params const& p) { m_params = p; }
private:
bool compute_basis_step();
bool simplify_source_target(equation const& source, equation& target);
void simplify_eq_by_using_to_superpose(equation &);
bool simplify_target_monomials(equation const& source, equation& target);
void process_simplified_target(equation* target, ptr_buffer<equation>& to_remove);
bool simplify_to_superpose_with_eq(equation*);
void simplify_m_to_simplify(equation*);
equation* pick_next();
bool canceled();
void superpose(equation * eq1, equation * eq2);
void superpose(equation * eq);
bool find_b_c(const nex *ab, const nex* ac, nex_mul*& b, nex_mul*& c);
bool find_b_c_check_only(const nex* ab, const nex* ac) const;
bool is_trivial(equation* ) const;
bool is_simpler(equation * eq1, equation * eq2);
void del_equations(unsigned old_size);
void del_equation(equation * eq);
void init_equation(equation* eq, nex*, u_dependency* d);
void insert_to_simplify(equation *eq) {
TRACE("grobner", display_equation(tout, *eq););
m_to_simplify.insert(eq);
}
void insert_to_superpose(equation *eq) {
SASSERT(m_nex_creator.is_simplified(*eq->expr()));
TRACE("grobner", display_equation(tout, *eq););
m_to_superpose.insert(eq);
}
const nex * get_highest_monomial(const nex * e) const;
bool simplify_target_monomials_sum(equation const&, equation&, nex_sum&, const nex&);
unsigned find_divisible(nex_sum const&, const nex&) const;
void simplify_target_monomials_sum_j(equation const&, equation&, nex_sum&, const nex&, unsigned, bool);
bool divide_ignore_coeffs_check_only(nex const& , const nex&) const;
bool divide_ignore_coeffs_check_only_nex_mul(nex_mul const&, nex const&) const;
nex_mul * divide_ignore_coeffs_perform(nex* , const nex&);
nex_mul * divide_ignore_coeffs_perform_nex_mul(nex_mul const& , const nex&);
nex * expr_superpose(nex const* e1, nex const* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c);
void add_mul_skip_first(nex_creator::sum_factory& sf, const rational& beta, nex const*e, nex_mul* c);
bool done();
unsigned num_of_equations() const { return m_to_simplify.size() + m_to_superpose.size(); }
void update_stats_max_degree_and_size(const equation*);
std::ostream& print_stats(std::ostream&) const;
std::ostream& display_dependency(std::ostream& out, u_dependency*) const;
bool equation_is_too_complex(const equation* eq) const {
return eq->expr()->size() > m_params.m_expr_size_limit;
}
#ifdef Z3DEBUG
bool test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c);
bool test_find_b(const nex* ab, const nex_mul* b);
#endif
};
class grobner : common {
grobner_core m_gc;
unsigned m_reported;
public:
grobner(core *, intervals *);
void grobner_lemmas();
~grobner() {}
private:
void prepare_rows_and_active_vars();
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar>& q);
std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
void display_matrix(std::ostream & out) const;
std::ostream& display(std::ostream& out) const { return m_gc.display(out); }
public:
void add_row(const vector<lp::row_cell<rational>> & row);
void check_eq(grobner_core::equation*);
void init();
nex_creator& get_nex_creator() { return m_nex_creator; }
}; // end of grobner
}

15
src/math/lp/nla_settings.h
View file

@ -29,10 +29,7 @@ class nla_settings {
unsigned m_horner_row_length_limit;
// grobner fields
bool m_run_grobner;
unsigned m_grobner_frequency;
unsigned m_grobner_eqs_threshold;
unsigned m_grobner_row_length_limit;
unsigned m_grobner_expr_size_limit;
public:
nla_settings() : m_run_order(true),
@ -41,15 +38,9 @@ public:
m_horner_frequency(4),
m_horner_row_length_limit(10),
m_run_grobner(true),
m_grobner_frequency(5),
m_grobner_eqs_threshold(512),
m_grobner_row_length_limit(10),
m_grobner_expr_size_limit(50)
m_grobner_row_length_limit(50)
{}
unsigned grobner_eqs_threshold() const { return m_grobner_eqs_threshold; }
unsigned& grobner_eqs_threshold() { return m_grobner_eqs_threshold; }
bool run_order() const { return m_run_order; }
bool& run_order() { return m_run_order; }
@ -65,9 +56,9 @@ public:
unsigned& horner_row_length_limit() { return m_horner_row_length_limit; }
bool run_grobner() const { return m_run_grobner; }
bool& run_grobner() { return m_run_grobner; }
bool& run_grobner() { return m_run_grobner; }
unsigned grobner_row_length_limit() const { return m_grobner_row_length_limit; }
unsigned grobner_expr_size_limit() const { return m_grobner_expr_size_limit; }
unsigned& grobner_row_length_limit() { return m_grobner_row_length_limit; }
};
}

1
src/smt/theory_lra.cpp
View file

@ -453,7 +453,6 @@ class theory_lra::imp {
m_nla->get_core()->m_nla_settings.horner_frequency() = nla.horner_frequency();
m_nla->get_core()->m_nla_settings.horner_row_length_limit() = nla.horner_row_length_limit();
m_nla->get_core()->m_nla_settings.run_grobner() = nla.grobner();
m_nla->get_core()->m_nla_settings.grobner_eqs_threshold() = nla.grobner_eqs_threshold();
}
}