mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

fixes in nla_expr operators and delete m_reported

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-18 11:05:12 -07:00
parent 5cc3812aa9
commit cef9726f00
3 changed files with 20 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -25,7 +25,6 @@ class cross_nested {
typedef nla_expr<rational> nex;
nex& m_e;
std::function<void (const nex&)> m_call_on_result;
std::set<nex> m_reported;
public:
cross_nested(nex &e, std::function<void (const nex&)> call_on_result): m_e(e), m_call_on_result(call_on_result) {}
@ -105,12 +104,7 @@ public:
auto e_to_report = m_e;
e_to_report.simplify();
e_to_report.sort();
if (m_reported.find(e_to_report) == m_reported.end()) {
m_reported.insert(e_to_report);
m_call_on_result(e_to_report);
} else {
TRACE("nla_cn", tout << "do not report " << e_to_report << "\n";);
}
m_call_on_result(e_to_report);
} else {
nex* c = pop_back(front);
cross_nested_of_expr_on_front_elem(c, front);

15
src/math/lp/nla_expr.h
View file

@ -396,6 +396,11 @@ public:
nla_expr& operator/=(const nla_expr& b) {
TRACE("nla_cn_details", tout << *this <<", " << b << "\n";);
if (b.is_var()) {
*this = (*this) / b.var();
return *this;
}
SASSERT(b.is_mul());
if (is_sum()) {
for (auto & e : children()) {
@ -403,6 +408,10 @@ public:
}
return *this;
}
if (is_var()) {
*this = scalar(T(1));
return *this;
}
SASSERT(is_mul());
auto powers = b.get_powers_from_mul();
unsigned i = 0, k = 0;
@ -496,6 +505,7 @@ nla_expr<T> operator*(const nla_expr<T>& a, const nla_expr<T>& b) {
template <typename T>
nla_expr<T> operator/(const nla_expr<T>& a, lpvar j) {
TRACE("nla_cn_details", tout << "a=" << a << ", v" << j << "\n";);
SASSERT((a.is_mul() && a.contains(j)) || (a.is_var() && a.var() == j));
if (a.is_var())
return nla_expr<T>::scalar(T(1));
@ -514,8 +524,11 @@ nla_expr<T> operator/(const nla_expr<T>& a, lpvar j) {
}
if (b.children().size() > 1) {
b.type() = expr_type::MUL;
} else if (b.children().size() == 1) {
auto t = b.children()[0];
b = t;
} else {
b = b.children()[0];
b = nla_expr<T>::scalar(T(1));
}
return b;
}

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

@ -71,11 +71,6 @@ void test_cn_on_expr(horner::nex t) {
TRACE("nla_cn", tout << "t=" << t << '\n';);
cross_nested cn(t, [](const horner::nex& n) {
TRACE("nla_cn", tout << n << "\n";);
auto nn = n;
nn.simplify();
nn.sort();
TRACE("nla_cn", tout << "ordered version\n" << nn << "\n______________________\n";);
} );
cn.run();
}
@ -87,9 +82,12 @@ void test_cn() {
enable_trace("nla_cn_cn");
nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4);
test_cn_on_expr(a*b*d + a*b*c + c*b*d + a*c*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";);
test_cn_on_expr(a*b*d + a*b*c + c*b*d);
// nex t = a*a*d + a*b*c*d + a*a*c*c*d + a*d*d + e*a*e + e*a*c + e*d;
// test_cn_on_expr(t);
nex t = a*a*d + a*b*c*d + a*a*c*c*d + a*d*d + e*a*e + e*a*c + e*d;
test_cn_on_expr(t);
}
} // end of namespace nla