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

add a test for intervals

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

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

@ -4,6 +4,31 @@
#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;

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

@ -159,7 +159,10 @@ 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;