mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix mk_div

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-01 10:41:45 -07:00
parent a8dd908fa0
commit 9f8f6dee9e
2 changed files with 16 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/cross_nested.h
View file

@ -370,7 +370,8 @@ public:
|| (ce->is_var() && to_var(ce)->var() == j);
}
// all factors of j go to a, the rest to b
void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) {
void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) {
TRACE("nla_cn_details", tout << "e = " << * e << ", j = " << m_nex_creator.ch(j) << std::endl;);
a = m_nex_creator.mk_sum();
m_b_split_vec.clear();
for (nex * ce: e->children()) {

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

@ -20,9 +20,9 @@
#include "math/lp/nex_creator.h"
#include <map>
namespace nla {
nex * nex_creator::mk_div(const nex* a, lpvar j) {
SASSERT(is_simplified(a));
TRACE("nla_cn_details", tout << "a=" << *a << ", " << ch(j) << "\n";);
SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j));
if (a->is_var())
return mk_scalar(rational(1));
@ -31,23 +31,21 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) {
for (auto& p : to_mul(a)->children()) {
const nex * c = p.e();
int pow = p.pow();
if (!seenj) {
if (c->contains(j)) {
if (!c->is_var()) {
bv.push_back(nex_pow(mk_div(c, j)));
if (pow != 1) {
bv.push_back(nex_pow(clone(c), pow));
}
} else {
SASSERT(to_var(c)->var() == j);
if (p.pow() != 1) {
bv.push_back(nex_pow(mk_var(j), pow - 1));
}
if (!seenj && c->contains(j)) {
if (!c->is_var()) {
bv.push_back(nex_pow(mk_div(c, j)));
if (pow != 1) {
bv.push_back(nex_pow(clone(c), pow - 1));
}
seenj = true;
}
} else {
SASSERT(to_var(c)->var() == j);
if (p.pow() != 1) {
bv.push_back(nex_pow(mk_var(j), pow - 1));
}
}
seenj = true;
} else {
bv.push_back(nex_pow(clone(c)));
bv.push_back(nex_pow(clone(c), pow));
}
}
if (bv.size() > 1) {