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

Nikolaj's changes related to dependencies on infinite interval bounds

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-30 10:48:24 -07:00
parent 1915812f84
commit ccc9a77a1f
3 changed files with 10 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/math/interval/interval.h
View file

@ -43,6 +43,11 @@ public:
unsigned m_upper_open:1;
unsigned m_lower_inf:1;
unsigned m_upper_inf:1;
interval():
m_lower_open(false),
m_upper_open(false),
m_lower_inf(true),
m_upper_inf(true) {}
};
// Should be NOOPs for precise numeral types.

25
src/math/lp/nla_intervals.cpp
View file

@ -4,31 +4,6 @@
#include "util/mpq.h"
namespace nla {
void intervals::test_inf() {
interval a; // [1, inf)
m_config.set_lower(a, rational(1));
m_config.set_lower_is_open(a, false);
m_config.set_upper_is_inf(a, true);
a.m_lower_dep = mk_dep(1);
interval b; // [-1,-1]
m_config.set_lower(b, rational(-1));
m_config.set_lower_is_open(b, false);
m_config.set_upper(b, rational(-1));
m_config.set_upper_is_open(b, false);
b.m_lower_dep = mk_dep(2);
b.m_upper_dep = mk_dep(4);
interval_deps_combine_rule comb_rule;
interval c;
mul(a, b, c, comb_rule);
TRACE("nla_horner_test", tout << "c before combine_deps() "; display(tout, c););
combine_deps(a, b, comb_rule, c);
SASSERT(lower_is_inf(c));
SASSERT(!dep_in_upper1(comb_rule.m_lower_combine));
}
void intervals::set_var_interval_with_deps(lpvar v, interval& b) {
lp::constraint_index ci;
rational val;

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

@ -73,11 +73,10 @@ class intervals : common {
ci_dependency * m_upper_dep; // justification for the upper bound
};
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);
i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_combine);
i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine);
}
@ -159,10 +158,7 @@ public:
m_dep_manager(m_val_manager, m_alloc),
m_config(m_num_manager, m_dep_manager),
m_imanager(lim, im_config(m_num_manager, m_dep_manager))
{
test_inf();
}
void test_inf();
{}
interval mul(const svector<lpvar>&) const;
void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
@ -180,8 +176,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 = lower_is_inf(a)? nullptr : b.m_lower_dep;
a.m_upper_dep = upper_is_inf(a)?nullptr : b.m_upper_dep;
a.m_lower_dep = b.m_lower_dep;
a.m_upper_dep = 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 {