From 3e0cf4b96d7c5b9725cf8354d497584465380df8 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 1 Nov 2019 14:15:54 -0700
Subject: [PATCH] port Grobner: fixes in nex simplifications
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/nex.h | 54 ++++++++--------
src/math/lp/nex_creator.cpp | 122 +++++++++++++++++++-----------------
src/math/lp/nla_grobner.cpp | 28 ++++++---
src/smt/smt_context_pp.cpp | 3 +-
4 files changed, 117 insertions(+), 90 deletions(-)
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index 0959f1d28..265c83ead 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -473,32 +473,36 @@ inline rational get_nex_val(const nex* e, std::function<rational (unsigned)> var
}
inline std::unordered_set<lpvar> get_vars_of_expr(const nex *e ) {
- std::unordered_set<lpvar> r;
- switch (e->type()) {
- case expr_type::SCALAR:
- return r;
- case expr_type::SUM:
- {
- for (auto c: *to_sum(e))
- for ( lpvar j : get_vars_of_expr(c))
- r.insert(j);
- }
- return r;
- case expr_type::MUL:
- {
- for (auto &c: *to_mul(e))
- for ( lpvar j : get_vars_of_expr(c.e()))
- r.insert(j);
- }
- return r;
- case expr_type::VAR:
- r.insert(to_var(e)->var());
- return r;
- default:
- TRACE("nla_cn_details", tout << e->type() << "\n";);
- SASSERT(false);
- return r;
+ std::unordered_set<lpvar> r;
+ switch (e->type()) {
+ case expr_type::SCALAR:
+ return r;
+ case expr_type::SUM:
+ {
+ for (auto c: *to_sum(e))
+ for ( lpvar j : get_vars_of_expr(c))
+ r.insert(j);
}
+ return r;
+ case expr_type::MUL:
+ {
+ for (auto &c: *to_mul(e))
+ for ( lpvar j : get_vars_of_expr(c.e()))
+ r.insert(j);
+ }
+ return r;
+ case expr_type::VAR:
+ r.insert(to_var(e)->var());
+ return r;
+ default:
+ TRACE("nla_cn_details", tout << e->type() << "\n";);
+ SASSERT(false);
+ return r;
}
}
+
+inline bool is_zero_scalar(nex *e) {
+ return e->is_scalar() && to_scalar(e)->value().is_zero();
+}
+}
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 78c341434..6c35fe475 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -87,7 +87,7 @@ bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) {
void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational& coeff) {
- TRACE("nla_cn_details", print_vector(children, tout););
+ TRACE("grobner_d", print_vector(children, tout););
vector<nex_pow> to_promote;
int skipped = 0;
for(unsigned j = 0; j < children.size(); j++) {
@@ -111,10 +111,10 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
children.shrink(children.size() - to_promote.size() - skipped);
for (nex_pow & p : to_promote) {
- TRACE("nla_cn_details", tout << p << "\n";);
+ TRACE("grobner_d", tout << p << "\n";);
nex_mul *pm = to_mul(p.e());
for (nex_pow& pp : *pm) {
- TRACE("nla_cn_details", tout << pp << "\n";);
+ TRACE("grobner_d", tout << pp << "\n";);
if (!eat_scalar_pow(coeff, pp, p.pow()))
children.push_back(nex_pow(pp.e(), pp.pow() * p.pow()));
}
@@ -123,7 +123,7 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
mul_to_powers(children);
- TRACE("nla_cn_details", print_vector(children, tout););
+ TRACE("grobner_d", print_vector(children, tout););
}
bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a, const nex_mul* b) const {
bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
@@ -183,7 +183,7 @@ bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a,
} while (true);
if (ret == -1)
ret = true;
- TRACE("nla_cn_details", tout << "a = "; print_vector(a, tout) << (ret == 1?" < ":" >= ") << *b << "\n";);
+ TRACE("nex_less", tout << "a = "; print_vector(a, tout) << (ret == 1?" < ":" >= ") << *b << "\n";);
return ret;
}
@@ -250,7 +250,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_m
} while (true);
if (ret == -1)
ret = true;
- TRACE("nla_cn_details", tout << "a = " << *a << (ret == 1?" < ":" >= ") << *b << "\n";);
+ TRACE("grobner_d", tout << "a = " << *a << (ret == 1?" < ":" >= ") << *b << "\n";);
return ret;
}
@@ -261,7 +261,7 @@ bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const
return true;
}
bool nex_creator::less_than_on_powers_mul(const vector<nex_pow>& children, const nex_mul* b) const {
- TRACE("nla_cn_details", tout << "children = "; print_vector(children, tout) << " , b = " << *b << "\n";);
+ TRACE("nex_less", tout << "children = "; print_vector(children, tout) << " , b = " << *b << "\n";);
SASSERT(children_are_simplified(children) && is_simplified(b));
unsigned a_deg = get_degree_children(children);
unsigned b_deg = b->get_degree();
@@ -279,7 +279,7 @@ bool nex_creator::less_than_on_powers_mul(const vector<nex_pow>& children, const
bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const {
- TRACE("nla_cn_details", tout << "a = " << *a << " , b = " << *b << "\n";);
+ TRACE("grobner_d", tout << "a = " << *a << " , b = " << *b << "\n";);
SASSERT(is_simplified(a) && is_simplified(b));
unsigned a_deg = a->get_degree();
unsigned b_deg = b->get_degree();
@@ -383,7 +383,7 @@ bool nex_creator::less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const
// the only difference with lt() that it disregards the coefficient in nex_mul
bool nex_creator::lt_for_sort_join_sum(const nex* a, const nex* b) const {
- TRACE("nla_cn_details_", tout << *a << " ? " << *b << "\n";);
+ TRACE("grobner_d_", tout << *a << " ? " << *b << "\n";);
if (a == b)
return false;
bool ret;
@@ -411,12 +411,12 @@ bool nex_creator::lt_for_sort_join_sum(const nex* a, const nex* b) const {
UNREACHABLE();
return false;
}
- TRACE("nla_cn_details_", tout << *a << (ret?" < ":" >= ") << *b << "\n";);
+ TRACE("grobner_d_", tout << *a << (ret?" < ":" >= ") << *b << "\n";);
return ret;
}
bool nex_creator::lt(const nex* a, const nex* b) const {
- TRACE("nla_cn_details_", tout << *a << " ? " << *b << "\n";);
+ TRACE("grobner_d_", tout << *a << " ? " << *b << "\n";);
if (a == b)
return false;
bool ret;
@@ -444,14 +444,14 @@ bool nex_creator::lt(const nex* a, const nex* b) const {
UNREACHABLE();
return false;
}
- TRACE("nla_cn_details_", tout << *a << (ret?" < ":" >= ") << *b << "\n";);
+ TRACE("grobner_d_", tout << *a << (ret?" < ":" >= ") << *b << "\n";);
return ret;
}
bool nex_creator::is_sorted(const nex_mul* e) const {
for (unsigned j = 0; j < e->size() - 1; j++) {
if (!(less_than_on_nex_pow((*e)[j], (*e)[j+1]))) {
- TRACE("nla_cn_details", tout << "not sorted e " << * e << "\norder is incorrect " <<
+ TRACE("grobner_d", tout << "not sorted e " << * e << "\norder is incorrect " <<
(*e)[j] << " >= " << (*e)[j + 1]<< "\n";);
return false;
@@ -464,24 +464,28 @@ bool nex_creator::is_sorted(const nex_mul* e) const {
bool nex_creator::mul_is_simplified(const nex_mul* e) const {
- if (e->size() == 0)
+ TRACE("nla_cn_", tout << "e = " << *e << "\n";);
+ if (e->size() == 0) {
+ TRACE("nla_cn", );
return false; // it has to be a scalar
- TRACE("nla_cn_details_", tout << "e = " << *e << "\n";);
- if (e->size() == 1 && e->begin()->pow() == 1 && e->coeff().is_one())
+ }
+ if (e->size() == 1 && e->begin()->pow() == 1 && e->coeff().is_one()) {
+ TRACE("nla_cn", );
return false;
+ }
std::set<const nex*, nex_lt> s([this](const nex* a, const nex* b) {return lt(a, b); });
for (const auto &p : *e) {
const nex* ee = p.e();
if (p.pow() == 0) {
- TRACE("nla_cn_details", tout << "not simplified " << *ee << "\n";);
+ TRACE("nla_cn", tout << "not simplified " << *ee << "\n";);
return false;
}
if (ee->is_mul()) {
- TRACE("nla_cn_details", tout << "not simplified " << *ee << "\n";);
+ TRACE("nla_cn", tout << "not simplified " << *ee << "\n";);
return false;
}
if (ee->is_scalar() && to_scalar(ee)->value().is_one()) {
- TRACE("nla_cn_details", tout << "not simplified " << *ee << "\n";);
+ TRACE("nla_cn", tout << "not simplified " << *ee << "\n";);
return false;
}
@@ -489,7 +493,7 @@ bool nex_creator::mul_is_simplified(const nex_mul* e) const {
if (it == s.end()) {
s.insert(ee);
} else {
- TRACE("nla_cn_details", tout << "not simplified " << *ee << "\n";);
+ TRACE("nla_cn", tout << "not simplified " << *ee << "\n";);
return false;
}
}
@@ -497,7 +501,7 @@ bool nex_creator::mul_is_simplified(const nex_mul* e) const {
}
nex * nex_creator::simplify_mul(nex_mul *e) {
- TRACE("nla_cn_details", tout << *e << "\n";);
+ TRACE("grobner_d", tout << *e << "\n";);
rational& coeff = e->coeff();
simplify_children_of_mul(e->children(), coeff);
if (e->size() == 1 && (*e)[0].pow() == 1 && coeff.is_one())
@@ -505,13 +509,13 @@ nex * nex_creator::simplify_mul(nex_mul *e) {
if (e->size() == 0 || e->coeff().is_zero())
return mk_scalar(e->coeff());
- TRACE("nla_cn_details", tout << *e << "\n";);
+ TRACE("grobner_d", tout << *e << "\n";);
SASSERT(is_simplified(e));
return e;
}
nex* nex_creator::simplify_sum(nex_sum *e) {
- TRACE("nla_cn_details", tout << "was e = " << *e << "\n";);
+ TRACE("grobner_d", tout << "was e = " << *e << "\n";);
simplify_children_of_sum(e->children());
nex *r;
if (e->size() == 1) {
@@ -521,7 +525,7 @@ nex* nex_creator::simplify_sum(nex_sum *e) {
} else {
r = e;
}
- TRACE("nla_cn_details", tout << "became r = " << *r << "\n";);
+ TRACE("grobner_d", tout << "became r = " << *r << "\n";);
return r;
}
@@ -529,6 +533,7 @@ bool nex_creator::sum_is_simplified(const nex_sum* e) const {
if (e->size() < 2) return false;
bool scalar = false;
for (nex * ee : *e) {
+ TRACE("nla_cn", tout << "ee = " << *ee << "\n";);
if (ee->is_sum()) {
TRACE("nla_cn", tout << "not simplified e = " << *e << "\n"
<< " has a child which is a sum " << *ee << "\n";);
@@ -579,7 +584,7 @@ void nex_creator::mul_to_powers(vector<nex_pow>& children) {
nex* nex_creator::create_child_from_nex_and_coeff(nex *e,
const rational& coeff) {
- TRACE("nla_cn_details", tout << *e << ", coeff = " << coeff << "\n";);
+ TRACE("grobner_d", tout << *e << ", coeff = " << coeff << "\n";);
if (coeff.is_one())
return e;
SASSERT(is_simplified(e));
@@ -616,15 +621,15 @@ nex* nex_creator::create_child_from_nex_and_coeff(nex *e,
}
// returns true if the key exists already
bool nex_creator::register_in_join_map(std::map<nex*, rational, nex_lt>& map, nex* e, const rational& r) const{
- TRACE("nla_cn_details", tout << *e << ", r = " << r << std::endl;);
+ TRACE("grobner_d", tout << *e << ", r = " << r << std::endl;);
auto map_it = map.find(e);
if (map_it == map.end()) {
map[e] = r;
- TRACE("nla_cn_details", tout << "inserting " << std::endl;);
+ TRACE("grobner_d", tout << "inserting " << std::endl;);
return false;
} else {
map_it->second += r;
- TRACE("nla_cn_details", tout << "adding " << r << " , got " << map_it->second << std::endl;);
+ TRACE("grobner_d", tout << "adding " << r << " , got " << map_it->second << std::endl;);
return true;
}
}
@@ -659,14 +664,14 @@ bool nex_creator::fill_join_map_for_sum(ptr_vector<nex> & children,
}
// a + 3bc + 2bc => a + 5bc
void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
- TRACE("nla_cn_details", print_vector_of_ptrs(children, tout););
+ TRACE("grobner_d", print_vector_of_ptrs(children, tout););
std::map<nex*, rational, nex_lt> map([this](const nex *a , const nex *b)
{ return lt_for_sort_join_sum(a, b); });
std::unordered_set<nex*> allocated_nexs; // handling (nex*) as numbers
nex_scalar * common_scalar;
fill_join_map_for_sum(children, map, allocated_nexs, common_scalar);
- TRACE("nla_cn_details", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});
+ TRACE("grobner_d", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});
children.clear();
for (auto& p : map) {
process_map_pair(p.first, p.second, children, allocated_nexs);
@@ -674,15 +679,15 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
if (common_scalar && !common_scalar->value().is_zero()) {
children.push_back(common_scalar);
}
- TRACE("nla_cn_details", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});
-}
-
-bool is_zero_scalar(nex *e) {
- return e->is_scalar() && to_scalar(e)->value().is_zero();
+ TRACE("grobner_d",
+ tout << "map=";
+ for (auto & p : map )
+ { tout << "(" << *p.first << ", " << p.second << ") "; }
+ tout << "\nchildren="; print_vector_of_ptrs(children, tout) << "\n";);
}
void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
- TRACE("nla_cn_details", print_vector_of_ptrs(children, tout););
+ TRACE("grobner_d", print_vector_of_ptrs(children, tout););
ptr_vector<nex> to_promote;
int skipped = 0;
for(unsigned j = 0; j < children.size(); j++) {
@@ -703,7 +708,7 @@ void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
}
}
- TRACE("nla_cn_details", print_vector_of_ptrs(children, tout););
+ TRACE("grobner_d", print_vector_of_ptrs(children, tout););
children.shrink(children.size() - to_promote.size() - skipped);
for (nex *e : to_promote) {
@@ -738,7 +743,7 @@ nex * nex_creator::mk_div_sum_by_mul(const nex_sum* m, const nex_mul* b) {
for (auto e : *m) {
r->add_child(mk_div_by_mul(e, b));
}
- TRACE("nla_cn_details", tout << *r << "\n";);
+ TRACE("grobner_d", tout << *r << "\n";);
return r;
}
@@ -747,11 +752,11 @@ nex * nex_creator::mk_div_mul_by_mul(const nex_mul *a, const nex_mul* b) {
b->get_powers_from_mul(m_powers);
nex_mul* ret = new nex_mul();
for (auto& p_from_a : *a) {
- TRACE("nla_cn_details", tout << "p_from_a = " << p_from_a << "\n";);
+ TRACE("grobner_d", tout << "p_from_a = " << p_from_a << "\n";);
const nex* e = p_from_a.e();
if (e->is_scalar()) {
ret->add_child_in_power(clone(e), p_from_a.pow());
- TRACE("nla_cn_details", tout << "processed scalar\n";);
+ TRACE("grobner_d", tout << "processed scalar\n";);
continue;
}
SASSERT(e->is_var());
@@ -775,17 +780,17 @@ nex * nex_creator::mk_div_mul_by_mul(const nex_mul *a, const nex_mul* b) {
pb -= pa;
}
}
- TRACE("nla_cn_details", tout << *ret << "\n";);
+ TRACE("grobner_d", tout << *ret << "\n";);
}
SASSERT(m_powers.size() == 0);
if (ret->size() == 0) {
delete ret;
- TRACE("nla_cn_details", tout << "return scalar\n";);
+ TRACE("grobner_d", tout << "return scalar\n";);
return mk_scalar(a->coeff() / b->coeff());
}
ret->coeff() = a->coeff() / b->coeff();
add_to_allocated(ret);
- TRACE("nla_cn_details", tout << *ret << "\n";);
+ TRACE("grobner_d", tout << *ret << "\n";);
return ret;
}
@@ -803,7 +808,7 @@ nex * nex_creator::mk_div_by_mul(const nex* a, const nex_mul* b) {
}
nex * nex_creator::mk_div(const nex* a, const nex* b) {
- TRACE("nla_cn_details", tout << *a <<" / " << *b << "\n";);
+ TRACE("grobner_d", tout << *a <<" / " << *b << "\n";);
if (b->is_var()) {
return mk_div(a, to_var(b)->var());
}
@@ -812,27 +817,31 @@ nex * nex_creator::mk_div(const nex* a, const nex* b) {
nex* nex_creator::simplify(nex* e) {
nex* es;
- TRACE("nla_cn_details", tout << *e << std::endl;);
+ TRACE("grobner_d", tout << *e << std::endl;);
if (e->is_mul())
es = simplify_mul(to_mul(e));
else if (e->is_sum())
es = simplify_sum(to_sum(e));
else
es = e;
- TRACE("nla_cn_details", tout << "simplified = " << *es << std::endl;);
+ TRACE("grobner_d", tout << "simplified = " << *es << std::endl;);
SASSERT(is_simplified(es));
return es;
}
-
+// adds to children the corrected expression and also adds to allocated the new expressions
void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex> & children, std::unordered_set<nex*>& allocated_nexs) {
- if (coeff.is_zero())
+ TRACE("grobner_d", tout << "e=" << *e << " , coeff= " << coeff << "\n";);
+ if (coeff.is_zero()) {
+ TRACE("grobner_d", tout << "did nothing\n";);
return;
+ }
bool e_is_old = allocated_nexs.find(e) != allocated_nexs.end();
if (!e_is_old) {
m_allocated.push_back(e);
}
if (e->is_mul()) {
- to_mul(e)->coeff() = coeff;
+ to_mul(e)->coeff() = coeff;
+ children.push_back(simplify(e));
} else {
SASSERT(e->is_var());
if (coeff.is_one()) {
@@ -844,7 +853,8 @@ void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex
}
bool nex_creator::is_simplified(const nex *e) const
-{
+{
+ TRACE("nla_cn", tout << "e = " << *e << "\n";);
if (e->is_mul())
return mul_is_simplified(to_mul(e));
if (e->is_sum())
@@ -861,7 +871,7 @@ unsigned nex_creator::find_sum_in_mul(const nex_mul* a) const {
return -1;
}
nex* nex_creator::canonize_mul(nex_mul *a) {
- TRACE("nla_cn_details", tout << "a = " << *a << "\n";);
+ TRACE("grobner_d", tout << "a = " << *a << "\n";);
unsigned j = find_sum_in_mul(a);
if (j + 1 == 0)
return a;
@@ -883,7 +893,7 @@ nex* nex_creator::canonize_mul(nex_mul *a) {
}
r->add_child(m);
}
- TRACE("nla_cn_details", tout << "canonized a = " << *r << "\n";);
+ TRACE("grobner_d", tout << "canonized a = " << *r << "\n";);
return canonize(r);
}
@@ -899,14 +909,14 @@ nex* nex_creator::canonize(const nex *a) {
(*s)[j] = canonize((*s)[j]);
}
t = simplify(s);
- TRACE("nla_cn_details", tout << *t << "\n";);
+ TRACE("grobner_d", tout << *t << "\n";);
return t;
}
return canonize_mul(to_mul(t));
}
bool nex_creator::equal(const nex* a, const nex* b) {
- TRACE("nla_cn_details", tout << *a << " against " << *b << "\n";);
+ TRACE("grobner_d", tout << *a << " against " << *b << "\n";);
nex_creator cn;
unsigned n = 0;
for (lpvar j : get_vars_of_expr(a)) {
@@ -921,8 +931,8 @@ bool nex_creator::equal(const nex* a, const nex* b) {
}
nex * ca = cn.canonize(a);
nex * cb = cn.canonize(b);
- TRACE("nla_cn_details", tout << "a = " << *a << ", canonized a = " << *ca << "\n";);
- TRACE("nla_cn_details", tout << "b = " << *b << ", canonized b = " << *cb << "\n";);
+ TRACE("grobner_d", tout << "a = " << *a << ", canonized a = " << *ca << "\n";);
+ TRACE("grobner_d", tout << "b = " << *b << ", canonized b = " << *cb << "\n";);
return !(cn.lt(ca, cb) || cn.lt(cb, ca));
}
#endif
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index d49a4a239..05a70ac7e 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -309,9 +309,10 @@ bool nla_grobner::simplify_target_monomials_sum(equation * source,
for (; j < targ_orig_size; j++) {
simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j);
}
+ TRACE("grobner_d", tout << "targ_sum = " << *targ_sum << "\n";);
target->exp() = m_nex_creator.simplify(targ_sum);
target->dep() = m_dep_manager.mk_join(source->dep(), target->dep());
- TRACE("grobner", tout << "target = "; display_equation(tout, *target););
+ TRACE("grobner_d", tout << "target = "; display_equation(tout, *target););
return true;
}
@@ -409,30 +410,36 @@ nex_mul * nla_grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) {
void nla_grobner::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex* high_mon, unsigned j) {
nex * ej = (*targ_sum)[j];
- TRACE("grobner", tout << "high_mon = " << *high_mon << ", ej = " << *ej << "\n";);
+ TRACE("grobner_d", tout << "high_mon = " << *high_mon << ", ej = " << *ej << "\n";);
nex_mul * ej_over_high_mon = divide_ignore_coeffs(ej, high_mon);
if (ej_over_high_mon == nullptr) {
- TRACE("grobner", tout << "no div\n";);
+ TRACE("grobner_d", tout << "no div\n";);
return;
}
- TRACE("grobner", tout << "ej_over_high_mon = " << *ej_over_high_mon << "\n";);
+ 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_sum * ej_sum = m_nex_creator.mk_sum();
(*targ_sum)[j] = ej_sum;
add_mul_skip_first(ej_sum ,-c/high_mon->coeff(), source->exp(), ej_over_high_mon);
- TRACE("grobner", tout << "targ_sum = " << *targ_sum << "\n";);
+ TRACE("grobner_d", tout << "targ_sum = " << *targ_sum << "\n";);
}
nla_grobner::equation * nla_grobner::simplify_source_target(equation * source, equation * target) {
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
+ TRACE("grobner_d", tout << "simplifying: " << *(target->exp()) << " using " << *(source->exp()) << "\n";);
SASSERT(m_nex_creator.is_simplified(source->exp()));
SASSERT(m_nex_creator.is_simplified(target->exp()));
if (target->exp()->is_scalar()) {
+ TRACE("grobner_d", tout << "no simplification\n";);
return nullptr;
}
- if (source->get_num_monomials() == 0)
+ if (source->get_num_monomials() == 0) {
+ TRACE("grobner_d", tout << "no simplification\n";);
return nullptr;
+ }
m_stats.m_simplify++;
bool result = false;
do {
@@ -446,8 +453,10 @@ nla_grobner::equation * nla_grobner::simplify_source_target(equation * source, e
TRACE("grobner", tout << "result: " << result << "\n"; if (result) display_equation(tout, *target););
if (result) {
target->dep() = m_dep_manager.mk_join(target->dep(), source->dep());
+ TRACE("grobner_d", tout << "simplied to " << *(target->exp()) << "\n";);
return target;
}
+ TRACE("grobner_d", tout << "no simplification\n";);
return nullptr;
}
@@ -482,6 +491,8 @@ void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equ
}
bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
+ TRACE("grobner_d", tout << "eq->exp " << *(eq->exp()) << "\n";);
+
ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
@@ -510,6 +521,7 @@ bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
}
void nla_grobner::simplify_to_superpose(equation* eq) {
+ TRACE("grobner_d", tout << "eq->exp " << *(eq->exp()) << "\n";);
ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
@@ -805,8 +817,8 @@ std::ostream& nla_grobner::display_equation(std::ostream & out, const equation &
}
void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
- TRACE("grobner", tout << "e = " << *e << "\n";);
- if (e == nullptr)
+ TRACE("grobner_e", tout << "e = " << *e << "\n";);
+ if (e == nullptr || is_zero_scalar(e))
return;
equation * eq = alloc(equation);
init_equation(eq, e, dep);
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 05f4fc51d..18ed6c021 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -496,7 +496,8 @@ namespace smt {
);
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
out.close();
-
+ if (m_lemma_id==2559)
+ exit(1);
return m_lemma_id;
}