mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix a bug in nla_expr

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-05 13:22:54 -07:00
parent 5d2ba2fce1
commit 1e625db84b
3 changed files with 15 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/gomory.cpp
View file

@ -259,6 +259,13 @@ class gomory::imp {
}
public:
void dump(std::ostream& out) {
out << "applying cut at:\n"; print_linear_combination_indices_only<row_strip<mpq>, mpq>(m_row, out); out << std::endl;
for (auto & p : m_row) {
m_int_solver.m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out);
}
out << "inf_col = " << m_inf_col << std::endl;
}
lia_move create_cut() {
TRACE("gomory_cut",

10
src/math/lp/horner.cpp
View file

@ -181,6 +181,7 @@ nex horner::split_with_var(const nex& e, lpvar j) {
r.add_child(cross_nested_of_sum(a));
return r;
}
TRACE("nla_cn", tout << "b = " << b << "\n";);
return nex::sum(nex::mul(cross_nested_of_sum(a), nex::var(j)), b);
}
@ -203,7 +204,7 @@ nex horner::cross_nested_of_sum(const nex& e) {
}
template <typename T> nex horner::create_expr_from_row(const T& row) {
TRACE("nla_cn", tout << "row="; m_core->m_lar_solver.print_term_as_indices(row, tout););
TRACE("nla_cn", tout << "row="; m_core->print_term(row, tout) << "\n";);
nex e;
if (row.size() > 1) {
e.type() = expr_type::SUM;
@ -216,6 +217,7 @@ template <typename T> nex horner::create_expr_from_row(const T& row) {
const auto &p = *row.begin();
return nex::mul(p.coeff(), nexvar(p.var()));
}
std::cout << "ops\n";
SASSERT(false);
return e;
}
@ -231,7 +233,8 @@ void horner::set_interval_for_scalar(interv& a, const T& v) {
}
interv horner::interval_of_expr(const nex& e) {
TRACE("nla_cn_details", tout << e.type() << " e=" << e << std::endl;);
TRACE("nla_cn", tout << e.type() << " e=" << e << std::endl;);
interv a;
switch (e.type()) {
case expr_type::SCALAR:
@ -252,7 +255,8 @@ interv horner::interval_of_expr(const nex& e) {
}
template <typename T>
interv horner::interval_of_mul(const vector<nla_expr<T>>& es) {
interv a = interval_of_expr(es[0]);
interv a = interval_of_expr(es[0]);
// std::cout << "a" << std::endl;
TRACE("nla_cn", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";);
for (unsigned k = 1; k < es.size(); k++) {
interv b = interval_of_expr(es[k]);

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

@ -151,11 +151,7 @@ public:
}
}
nla_expr(expr_type t): m_type(t) {}
nla_expr() {
#if Z3DEBUG
m_type = expr_type::UNDEF;
#endif
}
nla_expr(): m_type(expr_type::UNDEF) {}
void add_child(const nla_expr& e) {
m_children.push_back(e);