mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix nex simplification

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-02 17:14:34 -07:00
parent 43294cea16
commit a888e79696
3 changed files with 18 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/math/lp/nex_creator.cpp
View file

@ -61,15 +61,15 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) {
return mk_mul(bv);
}
bool nex_creator::eat_scalar_pow(nex_scalar *& r, nex_pow& p) {
bool nex_creator::eat_scalar_pow(nex_scalar *& r, nex_pow& p, unsigned pow) {
if (!p.e()->is_scalar())
return false;
nex_scalar *pe = to_scalar(p.e());
if (r == nullptr) {
r = pe;
r->value() = r->value().expt(p.pow());
r->value() = r->value().expt(p.pow()*pow);
} else {
r->value() *= pe->value().expt(p.pow());
r->value() *= pe->value().expt(p.pow()*pow);
}
return true;
}
@ -82,7 +82,7 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children) {
int skipped = 0;
for(unsigned j = 0; j < children.size(); j++) {
nex_pow& p = children[j];
if (eat_scalar_pow(r, p)) {
if (eat_scalar_pow(r, p, 1)) {
skipped++;
continue;
}
@ -101,8 +101,10 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children) {
children.shrink(children.size() - to_promote.size() - skipped);
for (nex_pow & p : to_promote) {
TRACE("nla_cn_details", tout << p << "\n";);
for (nex_pow& pp : to_mul(p.e())->children()) {
if (!eat_scalar_pow(r, pp))
TRACE("nla_cn_details", tout << pp << "\n";);
if (!eat_scalar_pow(r, pp, p.pow()))
children.push_back(nex_pow(pp.e(), pp.pow() * p.pow()));
}
}

2
src/math/lp/nex_creator.h
View file

@ -224,7 +224,7 @@ public:
void simplify_children_of_sum(ptr_vector<nex> & children);
bool eat_scalar_pow(nex_scalar *& r, nex_pow& p);
bool eat_scalar_pow(nex_scalar *& r, nex_pow& p, unsigned);
void simplify_children_of_mul(vector<nex_pow> & children, lt_on_vars lt, std::function<nex_scalar*()> mk_scalar);
bool lt(const nex* a, const nex* b) const;

12
src/test/lp/lp.cpp
View file

@ -83,8 +83,8 @@ void test_simplify() {
[](unsigned) { return false; },
[]() { return 1; } // for random
);
// enable_trace("nla_cn");
// enable_trace("nla_cn_details");
enable_trace("nla_cn");
enable_trace("nla_cn_details");
// enable_trace("nla_cn_details_");
enable_trace("nla_test");
@ -99,6 +99,14 @@ void test_simplify() {
auto a_plus_bc = r.mk_sum(a, bc);
auto simp_a_plus_bc = r.simplify(a_plus_bc);
SASSERT(to_sum(simp_a_plus_bc)->size() > 1);
auto three_ab = r.mk_mul(r.mk_scalar(rational(3)), a, b);
auto three_ab_square = r.mk_mul();
three_ab_square->add_child_in_power(three_ab, 3);
TRACE("nla_test", tout << "before simplify " << *three_ab_square << "\n";);
three_ab_square = to_mul(r.simplify(three_ab_square));
TRACE("nla_test", tout << *three_ab_square << "\n";);
nex_scalar * s = to_scalar(three_ab_square->children()[0].e());
SASSERT(s->value() == rational(27));
auto m = r.mk_mul(); m->add_child_in_power(c, 2);
TRACE("nla_test_", tout << "m = " << *m << "\n";);
auto n = r.mk_mul(a);