mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +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 12:00:14 -07:00
parent 10abd61c67
commit 0c6336c85d
1 changed files with 10 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -410,19 +410,20 @@ bool nex_creator::register_in_join_map(std::map<nex*, rational, nex_lt>& map, ne
void nex_creator::process_mul_in_simplify_sum(nex_mul* em, std::map<nex*, rational, nex_lt> &map, vector<nex_mul> & tmp) { void nex_creator::process_mul_in_simplify_sum(nex_mul* em, std::map<nex*, rational, nex_lt> &map, vector<nex_mul> & tmp) {
auto it = em->children().begin(); auto it = em->children().begin();
if (it->e()->is_scalar()) { if (it->e()->is_scalar()) {
SASSERT(it->pow() == 1);
rational r = to_scalar(it->e())->value(); rational r = to_scalar(it->e())->value();
auto end = em->children().end(); auto end = em->children().end();
if (em->children().size() == 2 && em->children()[1].pow() == 1) { if (em->children().size() == 2 && em->children()[1].pow() == 1) {
register_in_join_map(map, em->children()[1].e(), r); register_in_join_map(map, em->children()[1].e(), r);
} } else {
SASSERT(it->pow() == 1); tmp.push_back(nex_mul());
tmp.push_back(nex_mul()); nex_mul * m = &tmp[tmp.size()-1];
nex_mul * m = &tmp[tmp.size()-1]; for (it++; it != end; it++) {
for (it++; it != end; it++) { m->add_child_in_power(it->e(), it->pow());
m->add_child_in_power(it->e(), it->pow()); }
} if (!register_in_join_map(map, m, r))
if (!register_in_join_map(map, m, r)) tmp.pop_back();
tmp.pop_back(); }
} else { } else {
register_in_join_map(map, em, rational(1)); register_in_join_map(map, em, rational(1));
} }