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

merge changes from Z3Prover repository

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-24 12:11:48 -08:00
parent f22d4b50cc
commit ee255ef8b3
6 changed files with 1064 additions and 165 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/math/dd/dd_pdd.cpp
View file

@ -723,6 +723,7 @@ namespace dd {
bool do_gc = m_free_nodes.empty();
if (do_gc && !m_disable_gc) {
gc();
SASSERT(n.m_hi == 0 || (!m_free_nodes.contains(n.m_hi) && !m_free_nodes.contains(n.m_lo)));
e = m_node_table.insert_if_not_there2(n);
e->get_data().m_refcount = 0;
}

313
src/math/grobner/grobner.cpp
View file

@ -56,8 +56,8 @@ void grobner::del_equations(unsigned old_size) {
}
void grobner::del_equation(equation * eq) {
m_to_superpose.erase(eq);
m_to_simplify.erase(eq);
m_processed.erase(eq);
m_to_process.erase(eq);
SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
m_equations_to_delete[eq->m_bidx] = 0;
del_monomials(eq->m_monomials);
@ -85,11 +85,36 @@ void grobner::unfreeze_equations(unsigned old_size) {
it += old_size;
for (; it != end; ++it) {
equation * eq = *it;
m_to_simplify.insert(eq);
m_to_process.insert(eq);
}
m_equations_to_unfreeze.shrink(old_size);
}
void grobner::push_scope() {
m_scopes.push_back(scope());
scope & s = m_scopes.back();
s.m_equations_to_unfreeze_lim = m_equations_to_unfreeze.size();
s.m_equations_to_delete_lim = m_equations_to_delete.size();
}
void grobner::pop_scope(unsigned num_scopes) {
SASSERT(num_scopes >= get_scope_level());
unsigned new_lvl = get_scope_level() - num_scopes;
scope & s = m_scopes[new_lvl];
unfreeze_equations(s.m_equations_to_unfreeze_lim);
del_equations(s.m_equations_to_delete_lim);
m_scopes.shrink(new_lvl);
}
void grobner::reset() {
flush();
m_processed.reset();
m_to_process.reset();
m_equations_to_unfreeze.reset();
m_equations_to_delete.reset();
m_unsat = nullptr;
}
void grobner::display_var(std::ostream & out, expr * var) const {
if (is_app(var) && to_app(var)->get_num_args() > 0)
out << mk_bounded_pp(var, m_manager);
@ -163,8 +188,8 @@ void grobner::display_equations(std::ostream & out, equation_set const & v, char
}
void grobner::display(std::ostream & out) const {
display_equations(out, m_to_superpose, "m_to_superpose:");
display_equations(out, m_to_simplify, "m_to_simplify:");
display_equations(out, m_processed, "processed:");
display_equations(out, m_to_process, "to process:");
}
void grobner::set_weight(expr * n, int weight) {
@ -196,7 +221,7 @@ void grobner::update_order(equation_set & s, bool processed) {
if (update_order(eq)) {
if (processed) {
to_remove.push_back(eq);
m_to_simplify.insert(eq);
m_to_process.insert(eq);
}
}
}
@ -205,8 +230,8 @@ void grobner::update_order(equation_set & s, bool processed) {
}
void grobner::update_order() {
update_order(m_to_simplify, false);
update_order(m_to_superpose, true);
update_order(m_to_process, false);
update_order(m_processed, true);
}
bool grobner::var_lt::operator()(expr * v1, expr * v2) const {
@ -287,6 +312,7 @@ grobner::monomial * grobner::mk_monomial(rational const & coeff, expr * m) {
}
void grobner::init_equation(equation * eq, v_dependency * d) {
eq->m_scope_lvl = get_scope_level();
unsigned bidx = m_equations_to_delete.size();
eq->m_bidx = bidx;
eq->m_dep = d;
@ -305,7 +331,7 @@ void grobner::assert_eq_0(unsigned num_monomials, monomial * const * monomials,
equation * eq = alloc(equation);
eq->m_monomials.swap(ms);
init_equation(eq, ex);
m_to_simplify.insert(eq);
m_to_process.insert(eq);
}
}
@ -321,7 +347,7 @@ void grobner::assert_eq_0(unsigned num_monomials, rational const * coeffs, expr
normalize_coeff(ms); \
eq->m_monomials.swap(ms); \
init_equation(eq, ex); \
m_to_simplify.insert(eq); \
m_to_process.insert(eq); \
}
MK_EQ(coeffs[i]);
@ -371,7 +397,7 @@ void grobner::assert_monomial_tautology(expr * m) {
eq->m_monomials.push_back(m1);
normalize_coeff(eq->m_monomials);
init_equation(eq, static_cast<v_dependency*>(nullptr)); \
m_to_simplify.insert(eq);
m_to_process.insert(eq);
}
/**
@ -450,7 +476,7 @@ void grobner::normalize_coeff(ptr_vector<monomial> & monomials) {
/**
\brief Simplify the given monomials
*/
void grobner::simplify_ptr_monomials(ptr_vector<monomial> & monomials) {
void grobner::simplify(ptr_vector<monomial> & monomials) {
std::stable_sort(monomials.begin(), monomials.end(), m_monomial_lt);
merge_monomials(monomials);
normalize_coeff(monomials);
@ -476,22 +502,19 @@ inline bool grobner::is_trivial(equation * eq) const {
/**
\brief Sort monomials, and merge monomials with the same body.
*/
void grobner::simplify_eq(equation * eq) {
simplify_ptr_monomials(eq->m_monomials);
void grobner::simplify(equation * eq) {
simplify(eq->m_monomials);
if (is_inconsistent(eq) && !m_unsat)
m_unsat = eq;
}
/**
\brief Return true if monomial m1 is (* c1 M) and m2 is (* c2 M M').
Store M' in m_tmp_vars1.
Store M' in rest.
\remark This method assumes the variables of m1 and m2 are sorted.
*/
bool grobner::divide_ignore_coeffs(monomial const * m2, monomial const * m1) {
SASSERT(m1 != m2);
ptr_vector<expr> & rest = m_tmp_vars1;
rest.reset();
bool grobner::is_subset(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest) const {
unsigned i1 = 0;
unsigned i2 = 0;
unsigned sz1 = m1->m_vars.size();
@ -532,11 +555,12 @@ bool grobner::divide_ignore_coeffs(monomial const * m2, monomial const * m1) {
}
/**
\brief Multiply the monomials of source starting at position start_idx by (coeff * vars), and store the resultant monomials in m_tmp_monomials
\brief Multiply the monomials of source starting at position start_idx by (coeff * vars), and store the resultant monomials
at result.
*/
void grobner::mul_append_skip_first(equation const * source, rational const & coeff, ptr_vector<expr> const & vars) {
void grobner::mul_append(unsigned start_idx, equation const * source, rational const & coeff, ptr_vector<expr> const & vars, ptr_vector<monomial> & result) {
unsigned sz = source->get_num_monomials();
for (unsigned i = 1; i < sz; i++) {
for (unsigned i = start_idx; i < sz; i++) {
monomial const * m = source->get_monomial(i);
monomial * new_m = alloc(monomial);
new_m->m_coeff = m->m_coeff;
@ -546,7 +570,7 @@ void grobner::mul_append_skip_first(equation const * source, rational const & co
for (expr* e : new_m->m_vars)
m_manager.inc_ref(e);
std::stable_sort(new_m->m_vars.begin(), new_m->m_vars.end(), m_var_lt);
m_tmp_monomials.push_back(new_m);
result.push_back(new_m);
}
}
@ -574,65 +598,67 @@ grobner::equation * grobner::copy_equation(equation const * eq) {
return r;
}
// source 3f + k = 0, so f = -k/3
// target 2fg + e = 0
// target is replaced by 2(-k/3)g + e = -2/3kg + e
bool grobner::simplify_target_monomials(equation const * source, equation * target) {
unsigned i = 0;
unsigned new_target_sz = 0;
unsigned target_sz = target->m_monomials.size();
monomial const * LT = source->get_monomial(0);
m_tmp_monomials.reset();
for (; i < target_sz; i++) {
monomial * targ_i = target->m_monomials[i];
if (divide_ignore_coeffs(targ_i, LT)) {
if (i == 0)
m_changed_leading_term = true;
if (!m_tmp_vars1.empty())
target->m_lc = false;
mul_append_skip_first(source, - targ_i->m_coeff / (LT->m_coeff), m_tmp_vars1);
del_monomial(targ_i);
}
else {
if (i != new_target_sz) {
target->m_monomials[new_target_sz] = targ_i;
}
new_target_sz++;
}
}
if (new_target_sz < target_sz) {
target->m_monomials.shrink(new_target_sz);
target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr());
simplify_eq(target);
TRACE("grobner", tout << "result: "; display_equation(tout, *target););
return true;
}
return false;
}
/**
\brief Simplify the target equation using the source as a rewrite rule.
Return 0 if target was not simplified.
Return target if target was simplified but source->m_scope_lvl <= target->m_scope_lvl.
Return new_equation if source->m_scope_lvl > target->m_scope_lvl, moreover target is freezed, and new_equation contains the result.
*/
grobner::equation * grobner::simplify_source_target(equation const * source, equation * target) {
grobner::equation * grobner::simplify(equation const * source, equation * target) {
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
if (source->get_num_monomials() == 0)
return nullptr;
m_stats.m_simplify++;
bool result = false;
bool simplified;
do {
if (simplify_target_monomials(source, target)) {
result = true;
} else {
break;
simplified = false;
unsigned i = 0;
unsigned j = 0;
unsigned sz = target->m_monomials.size();
monomial const * LT = source->get_monomial(0);
ptr_vector<monomial> & new_monomials = m_tmp_monomials;
new_monomials.reset();
ptr_vector<expr> & rest = m_tmp_vars1;
for (; i < sz; i++) {
monomial * curr = target->m_monomials[i];
rest.reset();
if (is_subset(LT, curr, rest)) {
if (i == 0)
m_changed_leading_term = true;
if (source->m_scope_lvl > target->m_scope_lvl) {
target = copy_equation(target);
SASSERT(target->m_scope_lvl >= source->m_scope_lvl);
}
if (!result) {
// first time that source is being applied.
target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
}
simplified = true;
result = true;
rational coeff = curr->m_coeff;
coeff /= LT->m_coeff;
coeff.neg();
if (!rest.empty())
target->m_lc = false;
mul_append(1, source, coeff, rest, new_monomials);
del_monomial(curr);
target->m_monomials[i] = 0;
}
else {
target->m_monomials[j] = curr;
j++;
}
}
if (simplified) {
target->m_monomials.shrink(j);
target->m_monomials.append(new_monomials.size(), new_monomials.c_ptr());
simplify(target);
}
} while (!m_manager.canceled());
TRACE("grobner", tout << "result: " << result << "\n"; if (result) display_equation(tout, *target););
if (result) {
target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
return target;
}
return nullptr;
while (simplified && !m_manager.canceled());
TRACE("grobner", tout << "result: "; display_equation(tout, *target););
return result ? target : nullptr;
}
/**
@ -644,11 +670,11 @@ grobner::equation * grobner::simplify_source_target(equation const * source, equ
grobner::equation * grobner::simplify_using_processed(equation * eq) {
bool result = false;
bool simplified;
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities of size " << m_to_superpose.size() << "\n";);
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities\n";);
do {
simplified = false;
for (equation const* p : m_to_superpose) {
equation * new_eq = simplify_source_target(p, eq);
for (equation const* p : m_processed) {
equation * new_eq = simplify(p, eq);
if (new_eq) {
result = true;
simplified = true;
@ -687,7 +713,7 @@ bool grobner::is_better_choice(equation * eq1, equation * eq2) {
grobner::equation * grobner::pick_next() {
equation * r = nullptr;
ptr_buffer<equation> to_delete;
for (equation * curr : m_to_simplify) {
for (equation * curr : m_to_process) {
if (is_trivial(curr))
to_delete.push_back(curr);
else if (is_better_choice(curr, r))
@ -696,82 +722,79 @@ grobner::equation * grobner::pick_next() {
for (equation * e : to_delete)
del_equation(e);
if (r)
m_to_simplify.erase(r);
m_to_process.erase(r);
TRACE("grobner", tout << "selected equation: "; if (!r) tout << "<null>\n"; else display_equation(tout, *r););
return r;
}
void grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove) {
if (new_target != target) {
m_equations_to_unfreeze.push_back(target);
to_remove.push_back(target);
if (m_changed_leading_term) {
m_to_simplify.insert(new_target);
to_remove.push_back(target);
}
else {
to_insert.push_back(new_target);
}
target = new_target;
}
else {
if (m_changed_leading_term) {
m_to_simplify.insert(target);
to_remove.push_back(target);
}
}
}
/**
\brief Use the given equation to simplify processed terms.
*/
bool grobner::simplify_processed_with_eq(equation * eq) {
bool grobner::simplify_processed(equation * eq) {
ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
equation_set::iterator it = m_to_superpose.begin();
equation_set::iterator end = m_to_superpose.end();
equation_set::iterator it = m_processed.begin();
equation_set::iterator end = m_processed.end();
for (; it != end && !m_manager.canceled(); ++it) {
equation * target = *it;
equation * curr = *it;
m_changed_leading_term = false;
// if the leading term is simplified, then the equation has to be moved to m_to_simplify
equation * new_target = simplify_source_target(eq, target);
if (new_target != nullptr) {
process_simplified_target(to_insert, new_target, target, to_remove);
// if the leading term is simplified, then the equation has to be moved to m_to_process
equation * new_curr = simplify(eq, curr);
if (new_curr != nullptr) {
if (new_curr != curr) {
m_equations_to_unfreeze.push_back(curr);
to_remove.push_back(curr);
if (m_changed_leading_term) {
m_to_process.insert(new_curr);
to_remove.push_back(curr);
}
else {
to_insert.push_back(new_curr);
}
curr = new_curr;
}
else {
if (m_changed_leading_term) {
m_to_process.insert(curr);
to_remove.push_back(curr);
}
}
}
if (is_trivial(target))
to_delete.push_back(target);
if (is_trivial(curr))
to_delete.push_back(curr);
}
for (equation* eq : to_insert)
m_to_superpose.insert(eq);
m_processed.insert(eq);
for (equation* eq : to_remove)
m_to_superpose.erase(eq);
m_processed.erase(eq);
for (equation* eq : to_delete)
del_equation(eq);
return !m_manager.canceled();
}
/**
\brief Use the given equation to simplify m_to_simplify equation.
\brief Use the given equation to simplify to-process terms.
*/
void grobner::simplify_m_to_simplify(equation * eq) {
void grobner::simplify_to_process(equation * eq) {
ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
for (equation* target : m_to_simplify) {
equation * new_target = simplify_source_target(eq, target);
if (new_target != nullptr && new_target != target) {
m_equations_to_unfreeze.push_back(target);
to_insert.push_back(new_target);
to_remove.push_back(target);
target = new_target;
for (equation* curr : m_to_process) {
equation * new_curr = simplify(eq, curr);
if (new_curr != nullptr && new_curr != curr) {
m_equations_to_unfreeze.push_back(curr);
to_insert.push_back(new_curr);
to_remove.push_back(curr);
curr = new_curr;
}
if (is_trivial(target))
to_delete.push_back(target);
if (is_trivial(curr))
to_delete.push_back(curr);
}
for (equation* eq : to_insert)
m_to_simplify.insert(eq);
m_to_process.insert(eq);
for (equation* eq : to_remove)
m_to_simplify.erase(eq);
m_to_process.erase(eq);
for (equation* eq : to_delete)
del_equation(eq);
}
@ -780,7 +803,7 @@ void grobner::simplify_m_to_simplify(equation * eq) {
\brief If m1 = (* c M M1) and m2 = (* d M M2) and M is non empty, then return true and store M1 in rest1 and M2 in rest2.
*/
bool grobner::unify(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest1, ptr_vector<expr> & rest2) {
TRACE("grobner", tout << "unifying: "; display_monomial(tout, *m1); tout << " and "; display_monomial(tout, *m2); tout << "\n";);
TRACE("grobner", tout << "unifying: "; display_monomial(tout, *m1); tout << " "; display_monomial(tout, *m2); tout << "\n";);
bool found_M = false;
unsigned i1 = 0;
unsigned i2 = 0;
@ -832,39 +855,35 @@ void grobner::superpose(equation * eq1, equation * eq2) {
rest1.reset();
ptr_vector<expr> & rest2 = m_tmp_vars2;
rest2.reset();
TRACE("grobner", tout << "trying to superpose:\n"; display_equation(tout, *eq1); display_equation(tout, *eq2););
if (unify(eq1->m_monomials[0], eq2->m_monomials[0], rest1, rest2)) {
TRACE("grobner", tout << "superposing:\n"; display_equation(tout, *eq1); display_equation(tout, *eq2);
tout << "rest1: "; display_vars(tout, rest1.size(), rest1.c_ptr()); tout << "\n";
tout << "rest2: "; display_vars(tout, rest2.size(), rest2.c_ptr()); tout << "\n";);
ptr_vector<monomial> & new_monomials = m_tmp_monomials;
new_monomials.reset();
mul_append_skip_first(eq1, eq2->m_monomials[0]->m_coeff, rest2);
mul_append(1, eq1, eq2->m_monomials[0]->m_coeff, rest2, new_monomials);
rational c = eq1->m_monomials[0]->m_coeff;
c.neg();
mul_append_skip_first(eq2, c, rest1);
simplify_ptr_monomials(new_monomials);
mul_append(1, eq2, c, rest1, new_monomials);
simplify(new_monomials);
TRACE("grobner", tout << "resulting monomials: "; display_monomials(tout, new_monomials.size(), new_monomials.c_ptr()); tout << "\n";);
if (new_monomials.empty())
return;
m_num_new_equations++;
TRACE("grobner", tout << "success superposing\n";);
equation * new_eq = alloc(equation);
new_eq->m_monomials.swap(new_monomials);
init_equation(new_eq, m_dep_manager.mk_join(eq1->m_dep, eq2->m_dep));
new_eq->m_lc = false;
m_to_simplify.insert(new_eq);
} else {
TRACE("grobner", tout << "unify did not work\n";);
m_to_process.insert(new_eq);
}
}
/**
\brief Superpose the given equations with the equations in m_to_superpose.
\brief Superpose the given equations with the equations in m_processed.
*/
void grobner::superpose(equation * eq) {
for (equation * target : m_to_superpose) {
superpose(eq, target);
for (equation * curr : m_processed) {
superpose(eq, curr);
}
}
@ -874,33 +893,26 @@ void grobner::compute_basis_init() {
}
bool grobner::compute_basis_step() {
TRACE("grobner", display(tout););
equation * eq = pick_next();
if (!eq)
if (!eq)
return true;
m_stats.m_num_processed++;
#ifdef PROFILE_GB
if (m_stats.m_num_to_superpose % 100 == 0) {
verbose_stream() << "[grobner] " << m_to_superpose.size() << " " << m_to_simplify.size() << "\n";
if (m_stats.m_num_processed % 100 == 0) {
verbose_stream() << "[grobner] " << m_processed.size() << " " << m_to_process.size() << "\n";
}
#endif
equation * new_eq = simplify_using_processed(eq);
if (new_eq == nullptr || new_eq->get_num_monomials() == 0) {
TRACE("grobner",);
}
if (new_eq != nullptr && eq != new_eq) {
// equation was updated using non destructive updates
m_equations_to_unfreeze.push_back(eq);
eq = new_eq;
}
if (m_manager.canceled()) return false;
if (!simplify_processed_with_eq(eq)) {
TRACE("grobner", tout << "end of iteration:\n"; display(tout););
return false;
}
if (!simplify_processed(eq)) return false;
superpose(eq);
m_to_superpose.insert(eq);
simplify_m_to_simplify(eq);
m_processed.insert(eq);
simplify_to_process(eq);
TRACE("grobner", tout << "end of iteration:\n"; display(tout););
return false;
}
@ -908,10 +920,7 @@ bool grobner::compute_basis_step() {
bool grobner::compute_basis(unsigned threshold) {
compute_basis_init();
while (m_num_new_equations < threshold && !m_manager.canceled()) {
if (compute_basis_step()) {
return true;
}
if (compute_basis_step()) return true;
}
return false;
}
@ -922,12 +931,12 @@ void grobner::copy_to(equation_set const & s, ptr_vector<equation> & result) con
}
/**
\brief Copy the equations in m_to_superpose and m_to_simplify to result.
\brief Copy the equations in m_processed and m_to_process to result.
\warning This equations can be deleted when compute_basis is invoked.
*/
void grobner::get_equations(ptr_vector<equation> & result) const {
copy_to(m_to_superpose, result);
copy_to(m_to_simplify, result);
copy_to(m_processed, result);
copy_to(m_to_process, result);
}

30
src/math/grobner/grobner.h
View file

@ -58,6 +58,7 @@ public:
};
class equation {
unsigned m_scope_lvl; //!< scope level when this equation was created.
unsigned m_bidx:31; //!< position at m_equations_to_delete
unsigned m_lc:1; //!< true if equation if a linear combination of the input equations.
ptr_vector<monomial> m_monomials; //!< sorted monomials
@ -97,8 +98,8 @@ protected:
obj_map<expr, int> m_var2weight;
var_lt m_var_lt;
monomial_lt m_monomial_lt;
equation_set m_to_superpose;
equation_set m_to_simplify;
equation_set m_processed;
equation_set m_to_process;
equation_vector m_equations_to_unfreeze;
equation_vector m_equations_to_delete;
bool m_changed_leading_term; // set to true, if the leading term was simplified.
@ -107,6 +108,7 @@ protected:
unsigned m_equations_to_unfreeze_lim;
unsigned m_equations_to_delete_lim;
};
svector<scope> m_scopes;
ptr_vector<monomial> m_tmp_monomials;
ptr_vector<monomial> m_del_monomials;
ptr_vector<expr> m_tmp_vars1;
@ -153,20 +155,19 @@ protected:
void normalize_coeff(ptr_vector<monomial> & monomials);
void simplify_ptr_monomials(ptr_vector<monomial> & monomials);
void simplify(ptr_vector<monomial> & monomials);
void simplify_eq(equation * eq);
void simplify(equation * eq);
bool divide_ignore_coeffs(monomial const * m1, monomial const * m2);
bool is_subset(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest) const;
void mul_append_skip_first(equation const * source, rational const & coeff, ptr_vector<expr> const & vars);
void mul_append(unsigned start_idx, equation const * source, rational const & coeff, ptr_vector<expr> const & vars, ptr_vector<monomial> & result);
monomial * copy_monomial(monomial const * m);
equation * copy_equation(equation const * eq);
equation * simplify_source_target(equation const * source, equation * target);
bool simplify_target_monomials(equation const * source, equation * target);
equation * simplify(equation const * source, equation * target);
equation * simplify_using_processed(equation * eq);
@ -174,9 +175,9 @@ protected:
equation * pick_next();
bool simplify_processed_with_eq(equation * eq);
bool simplify_processed(equation * eq);
void simplify_m_to_simplify(equation * eq);
void simplify_to_process(equation * eq);
bool unify(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest1, ptr_vector<expr> & rest2);
@ -191,6 +192,8 @@ public:
~grobner();
unsigned get_scope_level() const { return m_scopes.size(); }
/**
\brief Set the weight of a term that is viewed as a variable by this module.
The weight is used to order monomials. If the weight is not set for a term t, then the
@ -271,14 +274,19 @@ public:
/**
\brief Reset state. Remove all equalities asserted with assert_eq.
*/
void reset();
void get_equations(ptr_vector<equation> & result) const;
void push_scope();
void pop_scope(unsigned num_scopes);
void display_equation(std::ostream & out, equation const & eq) const;
void display_monomial(std::ostream & out, monomial const & m) const;
void display(std::ostream & out) const;
void process_simplified_target(ptr_buffer<equation>& to_delete, equation* new_curr, equation*& curr, ptr_buffer<equation>& to_remove);
};
#endif /* GROBNER_H_ */

882
src/math/grobner/pdd_grobner.cpp Normal file
View file

@ -0,0 +1,882 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Abstract:
Grobner core based on pdd representation of polynomials
Author:
Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
--*/
#include "math/grobner/pdd_grobner.h"
#include "util/uint_set.h"
namespace dd {
/***
A simple algorithm maintains two sets (S, A),
where S is m_processed, 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
Alternate:
- Fix a variable ordering x1 > x2 > x3 > ....
In each step:
- pick a in A with *highest* variable x_i in leading term of *lowest* degree.
- simplify a using S
- simplify S using a
- if a does not contains x_i, put it back into A and pick again (determine whether possible)
- for s in S:
b = superpose(a, s)
add b to A
- add a to S
- simplify A using a
Apply a watch list to filter out relevant elements of S
Index leading_term_watch: Var -> Equation*
Only need to simplify equations that contain eliminated variable.
The watch list can be used to index into equations that are useful to simplify.
A Bloom filter on leading term could further speed up test whether reduction applies.
For p in A:
populate watch list by maxvar(p) |-> p
For p in S:
do not occur in watch list
- the variable ordering should be chosen from a candidate model M,
in a way that is compatible with weights that draw on the number of occurrences
in polynomials with violated evaluations and with the maximal slack (degree of freedom).
weight(x) := < count { p in P | x in p, M(p) != 0 }, min_{p in P | x in p} slack(p,x) >
slack is computed from interval assignments to variables, and is an interval in which x can possibly move
(an over-approximation).
The alternative version maintains the following invariant:
- polynomials not in the watch list cannot be simplified using a
Justification:
- elements in S have no variables watched
- elements in A are always reduced modulo all variables above the current x_i.
TBD:
Linear Elimination:
- comprises of a simplification pass that puts linear equations in to_processed
- so before simplifying with respect to the variable ordering, eliminate linear equalities.
Extended Linear Simplification (as exploited in Bosphorus AAAI 2019):
- multiply each polynomial by one variable from their orbits.
- The orbit of a varible are the variables that occur in the same monomial as it in some polynomial.
- The extended set of polynomials is fed to a linear Gauss Jordan Eliminator that extracts
additional linear equalities.
- Bosphorus uses M4RI to perform efficient GJE to scale on large bit-matrices.
Long distance vanishing polynomials (used by PolyCleaner ICCAD 2019):
- identify polynomials p, q, such that p*q = 0
- main case is half-adders and full adders (p := x + y, q := x * y) over GF2
because (x+y)*x*y = 0 over GF2
To work beyond GF2 we would need to rely on simplification with respect to asserted equalities.
The method seems rather specific to hardware multipliers so not clear it is useful to
generalize.
- find monomials that contain pairs of vanishing polynomials, transitively
withtout actually inlining.
Then color polynomial variables w by p, resp, q if they occur in polynomial equalities
w - r = 0, such that all paths in r contain a node colored by p, resp q.
polynomial variables that get colored by both p and q can be set to 0.
When some variable gets colored, other variables can be colored.
- We can walk pdd nodes by level to perform coloring in a linear sweep.
PDD nodes that are equal to 0 using some equality are marked as definitions.
First walk definitions to search for vanishing polynomial pairs.
Given two definition polynomials d1, d2, it must be the case that
level(lo(d1)) = level(lo(d1)) for the polynomial lo(d1)*lo(d2) to be vanishing.
Then starting from the lowest level examine pdd nodes.
Let the current node be called p, check if the pdd node p is used in an equation
w - r = 0. In which case, w inherits the labels from r.
Otherwise, label the node by the intersection of vanishing polynomials from lo(p) and hi(p).
Eliminating multiplier variables, but not adders [Kaufmann et al FMCAD 2019 for GF2];
- Only apply GB saturation with respect to variables that are part of multipliers.
- Perhaps this amounts to figuring out whether a variable is used in an xor or more
*/
grobner::grobner(reslimit& lim, pdd_manager& m) :
m(m),
m_limit(lim),
m_conflict(nullptr)
{}
grobner::~grobner() {
reset();
}
void grobner::saturate() {
simplify();
if (is_tuned()) tuned_init();
TRACE("grobner", display(tout););
try {
while (!done() && step()) {
TRACE("grobner", display(tout););
DEBUG_CODE(invariant(););
}
DEBUG_CODE(invariant(););
}
catch (pdd_manager::mem_out) {
// don't reduce further
}
}
bool grobner::step() {
m_stats.m_compute_steps++;
return is_tuned() ? tuned_step() : basic_step();
}
bool grobner::basic_step() {
return basic_step(pick_next());
}
grobner::scoped_process::~scoped_process() {
if (e) {
pdd p = e->poly();
SASSERT(!p.is_val());
if (p.hi().is_val()) {
g.push_equation(solved, e);
}
else {
g.push_equation(processed, e);
}
}
}
bool grobner::basic_step(equation* e) {
if (!e) return false;
scoped_process sd(*this, e);
equation& eq = *e;
TRACE("grobner", display(tout << "eq = ", eq); display(tout););
SASSERT(eq.state() == to_simplify);
if (!simplify_using(eq, m_processed)) return false;
if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
if (check_conflict(eq)) { sd.e = nullptr; return false; }
if (!simplify_using(m_processed, eq)) return false;
superpose(eq);
return simplify_using(m_to_simplify, eq);
}
grobner::equation* grobner::pick_next() {
equation* eq = nullptr;
for (auto* curr : m_to_simplify) {
if (!eq || is_simpler(*curr, *eq)) {
eq = curr;
}
}
if (eq) pop_equation(eq);
return eq;
}
void grobner::simplify() {
try {
while (!done() &&
(simplify_linear_step(true) ||
simplify_elim_pure_step() ||
simplify_cc_step() ||
simplify_leaf_step() ||
simplify_linear_step(false) ||
/*simplify_elim_dual_step() ||*/
false)) {
DEBUG_CODE(invariant(););
TRACE("grobner", display(tout););
}
}
catch (pdd_manager::mem_out) {
// done reduce
}
}
struct grobner::compare_top_var {
bool operator()(equation* a, equation* b) const {
return a->poly().var() < b->poly().var();
}
};
bool grobner::simplify_linear_step(bool binary) {
TRACE("grobner", tout << "binary " << binary << "\n";);
equation_vector linear;
for (equation* e : m_to_simplify) {
pdd p = e->poly();
if (binary) {
if (p.is_binary()) linear.push_back(e);
}
else if (p.is_linear()) {
linear.push_back(e);
}
}
return simplify_linear_step(linear);
}
/**
\brief simplify linear equations by using top variable as solution.
The linear equation is moved to set of solved equations.
*/
bool grobner::simplify_linear_step(equation_vector& linear) {
if (linear.empty()) return false;
use_list_t use_list = get_use_list();
compare_top_var ctv;
std::stable_sort(linear.begin(), linear.end(), ctv);
equation_vector trivial;
unsigned j = 0;
for (equation* src : linear) {
unsigned v = src->poly().var();
equation_vector const& uses = use_list[v];
TRACE("grobner",
display(tout << "uses of: ", *src) << "\n";
for (equation* e : uses) {
display(tout, *e) << "\n";
});
bool changed_leading_term;
bool all_reduced = true;
for (equation* dst : uses) {
if (src == dst || is_trivial(*dst)) {
continue;
}
pdd q = dst->poly();
if (!src->poly().is_binary() && !q.is_linear()) {
all_reduced = false;
continue;
}
remove_from_use(dst, use_list, v);
simplify_using(*dst, *src, changed_leading_term);
if (is_trivial(*dst)) {
trivial.push_back(dst);
}
else if (is_conflict(dst)) {
pop_equation(dst);
set_conflict(dst);
return true;
}
else if (changed_leading_term) {
pop_equation(dst);
push_equation(to_simplify, dst);
}
// v has been eliminated.
SASSERT(!m.free_vars(dst->poly()).contains(v));
add_to_use(dst, use_list);
}
if (all_reduced) {
linear[j++] = src;
}
}
linear.shrink(j);
for (equation* src : linear) {
pop_equation(src);
push_equation(solved, src);
}
for (equation* e : trivial) {
del_equation(e);
}
DEBUG_CODE(invariant(););
return j > 0;
}
/**
\brief simplify using congruences
replace pair px + q and ry + q by
px + q, px - ry
since px = ry
*/
bool grobner::simplify_cc_step() {
TRACE("grobner", tout << "cc\n";);
u_map<equation*> los;
bool reduced = false;
unsigned j = 0;
for (equation* eq1 : m_to_simplify) {
SASSERT(eq1->state() == to_simplify);
pdd p = eq1->poly();
auto* e = los.insert_if_not_there2(p.lo().index(), eq1);
equation* eq2 = e->get_data().m_value;
pdd q = eq2->poly();
if (eq2 != eq1 && (p.hi().is_val() || q.hi().is_val()) && !p.lo().is_val()) {
*eq1 = p - eq2->poly();
*eq1 = m_dep_manager.mk_join(eq1->dep(), eq2->dep());
reduced = true;
if (is_trivial(*eq1)) {
retire(eq1);
continue;
}
else if (check_conflict(*eq1)) {
continue;
}
}
m_to_simplify[j] = eq1;
eq1->set_index(j++);
}
m_to_simplify.shrink(j);
return reduced;
}
/**
\brief remove ax+b from p if x occurs as a leaf in p and a is a constant.
*/
bool grobner::simplify_leaf_step() {
TRACE("grobner", tout << "leaf\n";);
use_list_t use_list = get_use_list();
equation_vector leaves;
for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
equation* e = m_to_simplify[i];
pdd p = e->poly();
if (!p.hi().is_val()) {
continue;
}
leaves.reset();
for (equation* e2 : use_list[p.var()]) {
if (e != e2 && e2->poly().var_is_leaf(p.var())) {
leaves.push_back(e2);
}
}
for (equation* e2 : leaves) {
bool changed_leading_term;
remove_from_use(e2, use_list);
simplify_using(*e2, *e, changed_leading_term);
add_to_use(e2, use_list);
if (is_trivial(*e2)) {
pop_equation(e2);
retire(e2);
}
else if (e2->poly().is_val()) {
pop_equation(e2);
set_conflict(*e2);
return true;
}
else if (changed_leading_term) {
pop_equation(e2);
push_equation(to_simplify, e2);
}
}
}
return false;
}
/**
\brief treat equations as processed if top variable occurs only once.
*/
bool grobner::simplify_elim_pure_step() {
TRACE("grobner", tout << "pure\n";);
use_list_t use_list = get_use_list();
unsigned j = 0;
for (equation* e : m_to_simplify) {
pdd p = e->poly();
if (!p.is_val() && p.hi().is_val() && use_list[p.var()].size() == 1) {
push_equation(solved, e);
}
else {
m_to_simplify[j] = e;
e->set_index(j++);
}
}
if (j != m_to_simplify.size()) {
m_to_simplify.shrink(j);
return true;
}
return false;
}
/**
\brief
reduce equations where top variable occurs only twice and linear in one of the occurrences.
*/
bool grobner::simplify_elim_dual_step() {
use_list_t use_list = get_use_list();
unsigned j = 0;
bool reduced = false;
for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
equation* e = m_to_simplify[i];
pdd p = e->poly();
// check that e is linear in top variable.
if (e->state() != to_simplify) {
reduced = true;
}
else if (!done() && !is_trivial(*e) && p.hi().is_val() && use_list[p.var()].size() == 2) {
for (equation* e2 : use_list[p.var()]) {
if (e2 == e) continue;
bool changed_leading_term;
remove_from_use(e2, use_list);
simplify_using(*e2, *e, changed_leading_term);
if (is_conflict(e2)) {
pop_equation(e2);
set_conflict(e2);
}
// when e2 is trivial, leading term is changed
SASSERT(!is_trivial(*e2) || changed_leading_term);
if (changed_leading_term) {
pop_equation(e2);
push_equation(to_simplify, e2);
}
add_to_use(e2, use_list);
break;
}
reduced = true;
push_equation(solved, e);
}
else {
m_to_simplify[j] = e;
e->set_index(j++);
}
}
if (reduced) {
// clean up elements in m_to_simplify
// they may have moved.
m_to_simplify.shrink(j);
j = 0;
for (equation* e : m_to_simplify) {
if (is_trivial(*e)) {
retire(e);
}
else if (e->state() == to_simplify) {
m_to_simplify[j] = e;
e->set_index(j++);
}
}
m_to_simplify.shrink(j);
return true;
}
else {
return false;
}
}
void grobner::add_to_use(equation* e, use_list_t& use_list) {
unsigned_vector const& fv = m.free_vars(e->poly());
for (unsigned v : fv) {
use_list.reserve(v + 1);
use_list[v].push_back(e);
}
}
void grobner::remove_from_use(equation* e, use_list_t& use_list) {
unsigned_vector const& fv = m.free_vars(e->poly());
for (unsigned v : fv) {
use_list.reserve(v + 1);
use_list[v].erase(e);
}
}
void grobner::remove_from_use(equation* e, use_list_t& use_list, unsigned except_v) {
unsigned_vector const& fv = m.free_vars(e->poly());
for (unsigned v : fv) {
if (v != except_v) {
use_list.reserve(v + 1);
use_list[v].erase(e);
}
}
}
grobner::use_list_t grobner::get_use_list() {
use_list_t use_list;
for (equation * e : m_to_simplify) {
add_to_use(e, use_list);
}
for (equation * e : m_processed) {
add_to_use(e, use_list);
}
return use_list;
}
void grobner::superpose(equation const & eq) {
for (equation* target : m_processed) {
superpose(eq, *target);
}
}
/*
Use a set of equations to simplify eq
*/
bool grobner::simplify_using(equation& eq, equation_vector const& eqs) {
bool simplified, changed_leading_term;
do {
simplified = false;
for (equation* p : eqs) {
if (try_simplify_using(eq, *p, changed_leading_term)) {
simplified = true;
}
if (canceled() || eq.poly().is_val()) {
break;
}
}
}
while (simplified && !eq.poly().is_val());
TRACE("grobner", display(tout << "simplification result: ", eq););
return !done();
}
/*
Use the given equation to simplify equations in set
*/
bool grobner::simplify_using(equation_vector& set, equation const& eq) {
unsigned j = 0, sz = set.size();
for (unsigned i = 0; i < sz; ++i) {
equation& target = *set[i];
bool changed_leading_term = false;
bool simplified = !done() && try_simplify_using(target, eq, changed_leading_term);
if (simplified && is_trivial(target)) {
retire(&target);
}
else if (simplified && check_conflict(target)) {
// pushed to solved
}
else if (simplified && changed_leading_term) {
SASSERT(target.state() == processed);
push_equation(to_simplify, target);
if (!m_watch.empty()) {
m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1);
add_to_watch(target);
}
}
else {
set[j] = set[i];
target.set_index(j++);
}
}
set.shrink(j);
return !done();
}
/*
simplify target using source.
return true if the target was simplified.
set changed_leading_term if the target is in the m_processed set and the leading term changed.
*/
bool grobner::try_simplify_using(equation& dst, equation const& src, bool& changed_leading_term) {
if (&src == &dst) {
return false;
}
m_stats.m_simplified++;
pdd t = src.poly();
pdd r = dst.poly().reduce(t);
if (r == dst.poly() || is_too_complex(r)) {
return false;
}
TRACE("grobner",
tout << "reduce: " << dst.poly() << "\n";
tout << "using: " << t << "\n";
tout << "to: " << r << "\n";);
changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly());
dst = r;
dst = m_dep_manager.mk_join(dst.dep(), src.dep());
update_stats_max_degree_and_size(dst);
return true;
}
void grobner::simplify_using(equation & dst, equation const& src, bool& changed_leading_term) {
if (&src == &dst) return;
m_stats.m_simplified++;
pdd t = src.poly();
pdd r = dst.poly().reduce(t);
changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly());
TRACE("grobner",
tout << "reduce: " << dst.poly() << "\n";
tout << "using: " << t << "\n";
tout << "to: " << r << "\n";);
if (r == dst.poly()) return;
dst = r;
dst = m_dep_manager.mk_join(dst.dep(), src.dep());
update_stats_max_degree_and_size(dst);
}
/*
let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
*/
void grobner::superpose(equation const& eq1, equation const& eq2) {
TRACE("grobner_d", display(tout << "eq1=", eq1); display(tout << "eq2=", eq2););
pdd r(m);
if (m.try_spoly(eq1.poly(), eq2.poly(), r) &&
!r.is_zero() && !is_too_complex(r)) {
m_stats.m_superposed++;
add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()));
}
}
bool grobner::tuned_step() {
equation* e = tuned_pick_next();
if (!e) return false;
scoped_process sd(*this, e);
equation& eq = *e;
SASSERT(!m_watch[eq.poly().var()].contains(e));
SASSERT(eq.state() == to_simplify);
if (!simplify_using(eq, m_processed)) return false;
if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
if (check_conflict(eq)) { sd.e = nullptr; return false; }
if (!simplify_using(m_processed, eq)) return false;
TRACE("grobner", display(tout << "eq = ", eq););
superpose(eq);
simplify_watch(eq);
return true;
}
void grobner::tuned_init() {
unsigned_vector const& l2v = m.get_level2var();
m_level2var.resize(l2v.size());
m_var2level.resize(l2v.size());
for (unsigned i = 0; i < l2v.size(); ++i) {
m_level2var[i] = l2v[i];
m_var2level[l2v[i]] = i;
}
m_watch.reset();
m_watch.reserve(m_level2var.size());
m_levelp1 = m_level2var.size();
for (equation* eq : m_to_simplify) add_to_watch(*eq);
}
void grobner::add_to_watch(equation& eq) {
SASSERT(eq.state() == to_simplify);
SASSERT(is_tuned());
pdd const& p = eq.poly();
if (!p.is_val()) {
m_watch[p.var()].push_back(&eq);
}
}
void grobner::simplify_watch(equation const& eq) {
unsigned v = eq.poly().var();
auto& watch = m_watch[v];
unsigned j = 0;
for (equation* _target : watch) {
equation& target = *_target;
SASSERT(target.state() == to_simplify);
SASSERT(target.poly().var() == v);
bool changed_leading_term = false;
if (!done()) {
try_simplify_using(target, eq, changed_leading_term);
}
if (is_trivial(target)) {
pop_equation(target);
retire(&target);
}
else if (is_conflict(target)) {
pop_equation(target);
set_conflict(target);
}
else if (target.poly().var() != v) {
// move to other watch list
m_watch[target.poly().var()].push_back(_target);
}
else {
// keep watching same variable
watch[j++] = _target;
}
}
watch.shrink(j);
}
grobner::equation* grobner::tuned_pick_next() {
while (m_levelp1 > 0) {
unsigned v = m_level2var[m_levelp1-1];
equation_vector const& watch = m_watch[v];
equation* eq = nullptr;
for (equation* curr : watch) {
pdd const& p = curr->poly();
if (curr->state() == to_simplify && p.var() == v) {
if (!eq || is_simpler(*curr, *eq))
eq = curr;
}
}
if (eq) {
pop_equation(eq);
m_watch[eq->poly().var()].erase(eq);
return eq;
}
--m_levelp1;
}
return nullptr;
}
grobner::equation_vector const& grobner::equations() {
m_all_eqs.reset();
for (equation* eq : m_solved) m_all_eqs.push_back(eq);
for (equation* eq : m_to_simplify) m_all_eqs.push_back(eq);
for (equation* eq : m_processed) m_all_eqs.push_back(eq);
return m_all_eqs;
}
void grobner::reset() {
for (equation* e : m_solved) dealloc(e);
for (equation* e : m_to_simplify) dealloc(e);
for (equation* e : m_processed) dealloc(e);
m_solved.reset();
m_processed.reset();
m_to_simplify.reset();
m_stats.reset();
m_watch.reset();
m_level2var.reset();
m_var2level.reset();
m_conflict = nullptr;
}
void grobner::add(pdd const& p, u_dependency * dep) {
if (p.is_zero()) return;
equation * eq = alloc(equation, p, dep);
if (check_conflict(*eq)) {
return;
}
push_equation(to_simplify, eq);
if (!m_watch.empty()) {
m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1);
add_to_watch(*eq);
}
update_stats_max_degree_and_size(*eq);
}
bool grobner::canceled() {
return m_limit.get_cancel_flag();
}
bool grobner::done() {
return
m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold ||
canceled() ||
m_conflict != nullptr;
}
grobner::equation_vector& grobner::get_queue(equation const& eq) {
switch (eq.state()) {
case processed: return m_processed;
case to_simplify: return m_to_simplify;
case solved: return m_solved;
}
UNREACHABLE();
return m_to_simplify;
}
void grobner::del_equation(equation* eq) {
pop_equation(eq);
retire(eq);
}
void grobner::pop_equation(equation& eq) {
equation_vector& v = get_queue(eq);
unsigned idx = eq.idx();
if (idx != v.size() - 1) {
equation* eq2 = v.back();
eq2->set_index(idx);
v[idx] = eq2;
}
v.pop_back();
}
void grobner::push_equation(eq_state st, equation& eq) {
eq.set_state(st);
equation_vector& v = get_queue(eq);
eq.set_index(v.size());
v.push_back(&eq);
}
void grobner::update_stats_max_degree_and_size(const equation& e) {
m_stats.m_max_expr_size = std::max(m_stats.m_max_expr_size, e.poly().tree_size());
m_stats.m_max_expr_degree = std::max(m_stats.m_max_expr_degree, e.poly().degree());
}
void grobner::collect_statistics(statistics& st) const {
st.update("steps", m_stats.m_compute_steps);
st.update("simplified", m_stats.m_simplified);
st.update("superposed", m_stats.m_superposed);
st.update("degree", m_stats.m_max_expr_degree);
st.update("size", m_stats.m_max_expr_size);
}
std::ostream& grobner::display(std::ostream & out, const equation & eq) const {
out << eq.poly() << "\n";
if (m_print_dep) m_print_dep(eq.dep(), out);
return out;
}
std::ostream& grobner::display(std::ostream& out) const {
out << "solved\n"; for (auto e : m_solved) display(out, *e);
out << "processed\n"; for (auto e : m_processed) display(out, *e);
out << "to_simplify\n"; for (auto e : m_to_simplify) display(out, *e);
statistics st;
collect_statistics(st);
st.display(out);
return out;
}
void grobner::invariant() const {
// equations in processed have correct indices
// they are labled as processed
unsigned i = 0;
for (auto* e : m_processed) {
VERIFY(e->state() == processed);
VERIFY(e->idx() == i);
VERIFY(!e->poly().is_val());
++i;
}
i = 0;
uint_set head_vars;
for (auto* e : m_solved) {
VERIFY(e->state() == solved);
VERIFY(e->idx() == i);
++i;
pdd p = e->poly();
if (!p.is_val() && p.hi().is_val()) {
unsigned v = p.var();
SASSERT(!head_vars.contains(v));
head_vars.insert(v);
}
}
if (!head_vars.empty()) {
for (auto * e : m_to_simplify) {
for (auto v : m.free_vars(e->poly())) VERIFY(!head_vars.contains(v));
}
for (auto * e : m_processed) {
for (auto v : m.free_vars(e->poly())) VERIFY(!head_vars.contains(v));
}
}
// equations in to_simplify have correct indices
// they are labeled as non-processed
// their top-most variable is watched
i = 0;
for (auto* e : m_to_simplify) {
VERIFY(e->idx() == i);
VERIFY(e->state() == to_simplify);
pdd const& p = e->poly();
VERIFY(!p.is_val());
CTRACE("grobner", !m_watch.empty() && !m_watch[p.var()].contains(e),
display(tout << "not watched: ", *e) << "\n";);
VERIFY(m_watch.empty() || m_watch[p.var()].contains(e));
++i;
}
// the watch list consists of equations in to_simplify
// they watch the top most variable in poly
i = 0;
for (auto const& w : m_watch) {
for (equation* e : w) {
VERIFY(!e->poly().is_val());
VERIFY(e->poly().var() == i);
VERIFY(e->state() == to_simplify);
VERIFY(m_to_simplify.contains(e));
}
++i;
}
}
}

2
src/math/lp/nla_intervals.cpp
View file

@ -486,7 +486,7 @@ interv intervals::interval_of_expr(const nex* e, unsigned p) {
return b;
}
case expr_type::MUL: {
interv b = interval_of_mul<with_deps>(e->to_mul());
interv b = interval_of_mul<wd>(e->to_mul());
if (p != 1)
return power<wd>(b, p);
return b;

1
src/math/lp/nla_intervals.h
View file

@ -135,7 +135,6 @@ class intervals {
};
region m_alloc;
common::ci_value_manager m_val_manager;
mutable unsynch_mpq_manager m_num_manager;
mutable u_dependency_manager m_dep_manager;
im_config m_config;