mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fixes in assigning constraints to intervals

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-29 18:07:38 -07:00
parent b9483d0aff
commit e2702f3ae8
5 changed files with 55 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -24,9 +24,18 @@ namespace nla {
class cross_nested {
typedef nla_expr<rational> nex;
nex& m_e;
std::function<void (const nex&)> m_call_on_result;
std::function<bool (const nex&)> m_call_on_result;
std::function<bool (unsigned)> m_var_is_fixed;
bool m_done;
public:
cross_nested(nex &e, std::function<void (const nex&)> call_on_result): m_e(e), m_call_on_result(call_on_result) {}
cross_nested(nex &e,
std::function<bool (const nex&)> call_on_result,
std::function<bool (unsigned)> var_is_fixed):
m_e(e),
m_call_on_result(call_on_result),
m_var_is_fixed(var_is_fixed),
m_done(false)
{}
void run() {
vector<nex*> front;
@ -123,7 +132,15 @@ public:
for(auto& p : occurences) {
SASSERT(p.second.m_occs > 1);
lpvar j = p.first;
if (m_var_is_fixed(j)) {
// it does not make sense to explore fixed multupliers
// because the interval products do not become smaller
// after factoring those out
continue;
}
explore_of_expr_on_sum_and_var(c, j, front);
if (m_done)
return;
*c = copy_of_c;
TRACE("nla_cn", tout << "restore c=" << *c << ", m_e=" << m_e << "\n";);
restore_front(copy_of_front, front);
@ -151,7 +168,7 @@ public:
if (occurences.empty()) {
if(front.empty()) {
TRACE("nla_cn", tout << "got the cn form: =" << m_e << "\n";);
m_call_on_result(m_e);
m_done = m_call_on_result(m_e);
} else {
nex* c = pop_back(front);
explore_expr_on_front_elem(c, front);

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

@ -52,23 +52,29 @@ bool horner::row_is_interesting(const T& row) const {
return false;
}
void horner::lemmas_on_expr(nex& e) {
TRACE("nla_horner", tout << "e = " << e << "\n";);
cross_nested cn(e, [this](const nex& n) {
bool horner::lemmas_on_expr(nex& e) {
TRACE("nla_horner", tout << "e = " << e << "\n";);
bool conflict = false;
cross_nested cn(e, [this, & conflict](const nex& n) {
auto i = interval_of_expr(n);
TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";);
m_intervals.check_interval_for_conflict_on_zero(i);} );
conflict = m_intervals.check_interval_for_conflict_on_zero(i);
return conflict;
},
[this](unsigned j) { return c().var_is_fixed(j); }
);
cn.run();
return conflict;
}
template <typename T>
void horner::lemmas_on_row(const T& row) {
bool horner::lemmas_on_row(const T& row) {
if (!row_is_interesting(row))
return;
return false;
nex e = create_sum_from_row(row);
lemmas_on_expr(e);
return lemmas_on_expr(e);
}
void horner::horner_lemmas() {
@ -84,8 +90,16 @@ void horner::horner_lemmas() {
for (auto & s : matrix.m_columns[j])
rows_to_check.insert(s.var());
}
for (unsigned i : rows_to_check) {
lemmas_on_row(matrix.m_rows[i]);
svector<unsigned> rows;
for (unsigned i : rows_to_check) {
rows.push_back(i);
}
unsigned r = c().random();
unsigned sz = rows.size();
for (unsigned i = 0; i < sz; i++) {
if (lemmas_on_row(matrix.m_rows[(i + r) % sz]))
break;
}
}
@ -145,7 +159,6 @@ interv horner::interval_of_expr(const nex& e) {
interv horner::interval_of_mul(const nex& e) {
SASSERT(e.is_mul());
auto & es = e.children();
interval_deps_combine_rule comb_rule;
interv a = interval_of_expr(es[0]);
if (m_intervals.is_zero(a)) {
m_intervals.set_zero_interval_deps_for_mult(a);
@ -161,9 +174,11 @@ interv horner::interval_of_mul(const nex& e) {
TRACE("nla_horner_details", tout << "got zero\n"; );
return b;
}
TRACE("nla_horner_details", tout << "es[k]= "<< es[k] << ", "; m_intervals.display(tout, b); );
TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); );
interv c;
interval_deps_combine_rule comb_rule;
m_intervals.mul(a, b, c, comb_rule);
TRACE("nla_horner_details", tout << "c before combine_deps() "; m_intervals.display(tout, c););
m_intervals.combine_deps(a, b, comb_rule, c);
TRACE("nla_horner_details", tout << "a "; m_intervals.display(tout, a););
TRACE("nla_horner_details", tout << "c "; m_intervals.display(tout, c););

4
src/math/lp/horner.h
View file

@ -35,7 +35,7 @@ public:
horner(core *core);
void horner_lemmas();
template <typename T> // T has an iterator of (coeff(), var())
void lemmas_on_row(const T&);
bool lemmas_on_row(const T&);
template <typename T> bool row_is_interesting(const T&) const;
template <typename T> nex create_sum_from_row(const T&);
intervals::interval interval_of_expr(const nex& e);
@ -46,6 +46,6 @@ public:
void set_interval_for_scalar(intervals::interval&, const rational&);
void set_var_interval(lpvar j, intervals::interval&);
std::set<lpvar> get_vars_of_expr(const nex &) const;
void lemmas_on_expr(nex &);
bool lemmas_on_expr(nex &);
}; // end of horner
}

7
src/math/lp/nla_intervals.h
View file

@ -74,7 +74,8 @@ class intervals : common {
};
void add_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
void add_deps(interval const& a, interval const& b,
interval_deps_combine_rule const& deps, interval& i) const {
i.m_lower_dep = mk_dependency(a, b, deps.m_lower_combine);
i.m_upper_dep = mk_dependency(a, b, deps.m_upper_combine);
}
@ -176,8 +177,8 @@ public:
void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); }
void set(interval& a, const interval& b) {
m_imanager.set(a, b);
a.m_lower_dep = b.m_lower_dep;
a.m_upper_dep = b.m_upper_dep;
a.m_lower_dep = lower_is_inf(a)? nullptr : b.m_lower_dep;
a.m_upper_dep = upper_is_inf(a)?nullptr : b.m_upper_dep;
}
void mul(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); }
void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {

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

@ -72,7 +72,9 @@ 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_test", tout << n << "\n";);
} );
return false;
} ,
[](unsigned) { return false; });
cn.run();
}