mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58: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 14:28:28 -07:00
parent 0c6336c85d
commit 13434a2589
2 changed files with 30 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -196,7 +196,7 @@ bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const {
case expr_type::MUL: case expr_type::MUL:
{ {
if (b->get_degree() > 1) if (b->get_degree() > 1)
return false; return true;
auto it = to_mul(b)->children().begin(); auto it = to_mul(b)->children().begin();
const nex_pow & c = *it; const nex_pow & c = *it;
const nex * f = c.e(); const nex * f = c.e();
@ -319,10 +319,11 @@ nex * nex_creator::simplify_mul(nex_mul *e) {
} }
nex* nex_creator::simplify_sum(nex_sum *e) { nex* nex_creator::simplify_sum(nex_sum *e) {
TRACE("nla_cn_details", tout << "was e = " << *e << "\n";);
simplify_children_of_sum(e->children()); simplify_children_of_sum(e->children());
if (e->size() == 1) nex *r = e->size() == 1? e->children()[0]: e;
return e->children()[0]; TRACE("nla_cn_details", tout << "became r = " << *r << "\n";);
return e; return r;
} }
bool nex_creator::sum_is_simplified(const nex_sum* e) const { bool nex_creator::sum_is_simplified(const nex_sum* e) const {

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

@ -85,6 +85,9 @@ void test_simplify() {
); );
enable_trace("nla_cn"); enable_trace("nla_cn");
enable_trace("nla_cn_details"); enable_trace("nla_cn_details");
enable_trace("nla_cn_details_");
enable_trace("nla_test");
nex_creator & r = cn.get_nex_creator(); nex_creator & r = cn.get_nex_creator();
r.active_vars_weights().resize(3); r.active_vars_weights().resize(3);
for (unsigned j = 0; j < r.active_vars_weights().size(); j++) for (unsigned j = 0; j < r.active_vars_weights().size(); j++)
@ -92,45 +95,52 @@ void test_simplify() {
nex_var* a = r.mk_var(0); nex_var* a = r.mk_var(0);
nex_var* b = r.mk_var(1); nex_var* b = r.mk_var(1);
nex_var* c = r.mk_var(2); nex_var* c = r.mk_var(2);
auto bc = r.mk_mul(b, c);
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);
return;
auto m = r.mk_mul(); m->add_child_in_power(c, 2); auto m = r.mk_mul(); m->add_child_in_power(c, 2);
TRACE("nla_cn", tout << "m = " << *m << "\n";); TRACE("nla_test_", tout << "m = " << *m << "\n";);
auto n = r.mk_mul(a); auto n = r.mk_mul(a);
n->add_child_in_power(b, 7); n->add_child_in_power(b, 7);
n->add_child(r.mk_scalar(rational(3))); n->add_child(r.mk_scalar(rational(3)));
n->add_child_in_power(r.mk_scalar(rational(4)), 2); n->add_child_in_power(r.mk_scalar(rational(4)), 2);
n->add_child(r.mk_scalar(rational(1))); n->add_child(r.mk_scalar(rational(1)));
TRACE("nla_cn", tout << "n = " << *n << "\n";); TRACE("nla_test_", tout << "n = " << *n << "\n";);
m->add_child_in_power(n, 3); m->add_child_in_power(n, 3);
n->add_child_in_power(r.mk_scalar(rational(1, 3)), 2); n->add_child_in_power(r.mk_scalar(rational(1, 3)), 2);
TRACE("nla_cn", tout << "m = " << *m << "\n";); TRACE("nla_test_", tout << "m = " << *m << "\n";);
nex_sum * e = r.mk_sum(a, r.mk_sum(b, m)); nex_sum * e = r.mk_sum(a, r.mk_sum(b, m));
TRACE("nla_cn", tout << "e = " << *e << "\n";); TRACE("nla_test", tout << "before simplify e = " << *e << "\n";);
e = to_sum(r.simplify(e)); e = to_sum(r.simplify(e));
TRACE("nla_cn", tout << "simplified e = " << *e << "\n";); TRACE("nla_test", tout << "simplified e = " << *e << "\n";);
SASSERT(e->children().size() > 2);
nex_sum * e_m = r.mk_sum(); nex_sum * e_m = r.mk_sum();
for (const nex* ex: to_sum(e)->children()) { for (const nex* ex: to_sum(e)->children()) {
nex* ce = r.mk_mul(r.clone(ex), r.mk_scalar(rational(3))); nex* ce = r.mk_mul(r.clone(ex), r.mk_scalar(rational(3)));
TRACE("nla_test", tout << "before simpl ce = " << *ce << "\n";);
ce = r.simplify(ce); ce = r.simplify(ce);
TRACE("nla_cn", tout << "simplified ce = " << *ce << "\n";); TRACE("nla_test", tout << "simplified ce = " << *ce << "\n";);
e_m->add_child(ce); e_m->add_child(ce);
} }
e->add_child(e_m); e->add_child(e_m);
TRACE("nla_cn", tout << "before simplify sum e = " << *e << "\n";); TRACE("nla_test", tout << "before simplify sum e = " << *e << "\n";);
e = to_sum(r.simplify(e)); e = to_sum(r.simplify(e));
TRACE("nla_cn", tout << "simplified sum e = " << *e << "\n";); TRACE("nla_test", tout << "simplified sum e = " << *e << "\n";);
} }
void test_cn() { void test_cn() {
cross_nested cn( cross_nested cn(
[](const nex* n) { [](const nex* n) {
TRACE("nla_cn_test", tout << *n << "\n";); TRACE("nla_test", tout << *n << "\n";);
return false; return false;
} , } ,
[](unsigned) { return false; }, [](unsigned) { return false; },
[]{ return 1; }); []{ return 1; });
enable_trace("nla_cn"); enable_trace("nla_test");
enable_trace("nla_cn_details"); enable_trace("nla_test_details");
auto & cr = cn.get_nex_creator(); auto & cr = cn.get_nex_creator();
cr.active_vars_weights().resize(20); cr.active_vars_weights().resize(20);
for (unsigned j = 0; j < cr.active_vars_weights().size(); j++) for (unsigned j = 0; j < cr.active_vars_weights().size(); j++)
@ -161,15 +171,15 @@ void test_cn() {
nex * clone = cr.clone(cr.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed)); nex * clone = cr.clone(cr.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed));
clone = cr.simplify(clone); clone = cr.simplify(clone);
SASSERT(cr.is_simplified(clone)); SASSERT(cr.is_simplified(clone));
TRACE("nla_cn", tout << "clone = " << *clone << "\n";); TRACE("nla_test", tout << "clone = " << *clone << "\n";);
#endif #endif
// test_cn_on_expr(cr.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn); // test_cn_on_expr(cr.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn);
test_cn_on_expr(to_sum(clone), cn); test_cn_on_expr(to_sum(clone), cn);
// TRACE("nla_cn", tout << "done\n";); // TRACE("nla_test", tout << "done\n";);
// test_cn_on_expr(a*b*d + a*b*c + c*b*d + a*c*d); // test_cn_on_expr(a*b*d + a*b*c + c*b*d + a*c*d);
// TRACE("nla_cn", tout << "done\n";); // TRACE("nla_test", tout << "done\n";);
// test_cn_on_expr(a*b*b*d*d + a*b*b*c*d + c*b*b*d); // test_cn_on_expr(a*b*b*d*d + a*b*b*c*d + c*b*b*d);
// TRACE("nla_cn", tout << "done\n";); // TRACE("nla_test", tout << "done\n";);
// test_cn_on_expr(a*b*d + a*b*c + c*b*d); // test_cn_on_expr(a*b*d + a*b*c + c*b*d);
} }