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

rename and add some interval methods

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-27 14:24:06 -07:00
parent 4ef7bf2bf6
commit 9fb66e9365
5 changed files with 170 additions and 160 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -80,14 +80,14 @@ public:
#define DEP_IN_LOWER2 4
#define DEP_IN_UPPER2 8
typedef short bound_deps;
inline bool dep_in_lower1(bound_deps d) { return (d & DEP_IN_LOWER1) != 0; }
inline bool dep_in_lower2(bound_deps d) { return (d & DEP_IN_LOWER2) != 0; }
inline bool dep_in_upper1(bound_deps d) { return (d & DEP_IN_UPPER1) != 0; }
inline bool dep_in_upper2(bound_deps d) { return (d & DEP_IN_UPPER2) != 0; }
inline bound_deps dep1_to_dep2(bound_deps d) {
typedef short deps_combine_rule;
inline bool dep_in_lower1(deps_combine_rule d) { return (d & DEP_IN_LOWER1) != 0; }
inline bool dep_in_lower2(deps_combine_rule d) { return (d & DEP_IN_LOWER2) != 0; }
inline bool dep_in_upper1(deps_combine_rule d) { return (d & DEP_IN_UPPER1) != 0; }
inline bool dep_in_upper2(deps_combine_rule d) { return (d & DEP_IN_UPPER2) != 0; }
inline deps_combine_rule dep1_to_dep2(deps_combine_rule d) {
SASSERT(!dep_in_lower2(d) && !dep_in_upper2(d));
bound_deps r = d << 2;
deps_combine_rule r = d << 2;
SASSERT(dep_in_lower1(d) == dep_in_lower2(r));
SASSERT(dep_in_upper1(d) == dep_in_upper2(r));
SASSERT(!dep_in_lower1(r) && !dep_in_upper1(r));
@ -99,9 +99,9 @@ inline bound_deps dep1_to_dep2(bound_deps d) {
It contains the dependencies for the output lower and upper bounds
for the resultant interval.
*/
struct interval_deps {
bound_deps m_lower_deps;
bound_deps m_upper_deps;
struct interval_deps_combine_rule {
deps_combine_rule m_lower_combine;
deps_combine_rule m_upper_combine;
};
template<typename C>
@ -239,30 +239,30 @@ public:
/**
\brief b <- -a
*/
void neg(interval const & a, interval & b, interval_deps & b_deps);
void neg(interval const & a, interval & b, interval_deps_combine_rule & b_deps);
void neg(interval const & a, interval & b);
void neg_jst(interval const & a, interval_deps & b_deps);
void neg_jst(interval const & a, interval_deps_combine_rule & b_deps);
/**
\brief c <- a + b
*/
void add(interval const & a, interval const & b, interval & c, interval_deps & c_deps);
void add(interval const & a, interval const & b, interval & c, interval_deps_combine_rule & c_deps);
void add(interval const & a, interval const & b, interval & c);
void add_jst(interval const & a, interval const & b, interval_deps & c_deps);
void add_jst(interval const & a, interval const & b, interval_deps_combine_rule & c_deps);
/**
\brief c <- a - b
*/
void sub(interval const & a, interval const & b, interval & c, interval_deps & c_deps);
void sub(interval const & a, interval const & b, interval & c, interval_deps_combine_rule & c_deps);
void sub(interval const & a, interval const & b, interval & c);
void sub_jst(interval const & a, interval const & b, interval_deps & c_deps);
void sub_jst(interval const & a, interval const & b, interval_deps_combine_rule & c_deps);
/**
\brief b <- k * a
*/
void mul(numeral const & k, interval const & a, interval & b, interval_deps & b_deps);
void mul(numeral const & k, interval const & a, interval & b, interval_deps_combine_rule & b_deps);
void mul(numeral const & k, interval const & a, interval & b) { div_mul(k, a, b, false); }
void mul_jst(numeral const & k, interval const & a, interval_deps & b_deps);
void mul_jst(numeral const & k, interval const & a, interval_deps_combine_rule & b_deps);
/**
\brief b <- (n/d) * a
*/
@ -278,58 +278,58 @@ public:
That is, we must invert k rounding towards +oo or -oo depending whether we
are computing a lower or upper bound.
*/
void div(interval const & a, numeral const & k, interval & b, interval_deps & b_deps);
void div(interval const & a, numeral const & k, interval & b, interval_deps_combine_rule & b_deps);
void div(interval const & a, numeral const & k, interval & b) { div_mul(k, a, b, true); }
void div_jst(interval const & a, numeral const & k, interval_deps & b_deps) { mul_jst(k, a, b_deps); }
void div_jst(interval const & a, numeral const & k, interval_deps_combine_rule & b_deps) { mul_jst(k, a, b_deps); }
/**
\brief c <- a * b
*/
void mul(interval const & a, interval const & b, interval & c, interval_deps & c_deps);
void mul(interval const & a, interval const & b, interval & c, interval_deps_combine_rule & c_deps);
void mul(interval const & a, interval const & b, interval & c);
void mul_jst(interval const & a, interval const & b, interval_deps & c_deps);
void mul_jst(interval const & a, interval const & b, interval_deps_combine_rule & c_deps);
/**
\brief b <- a^n
*/
void power(interval const & a, unsigned n, interval & b, interval_deps & b_deps);
void power(interval const & a, unsigned n, interval & b, interval_deps_combine_rule & b_deps);
void power(interval const & a, unsigned n, interval & b);
void power_jst(interval const & a, unsigned n, interval_deps & b_deps);
void power_jst(interval const & a, unsigned n, interval_deps_combine_rule & b_deps);
/**
\brief b <- a^(1/n) with precision p.
\pre if n is even, then a must not contain negative numbers.
*/
void nth_root(interval const & a, unsigned n, numeral const & p, interval & b, interval_deps & b_deps);
void nth_root(interval const & a, unsigned n, numeral const & p, interval & b, interval_deps_combine_rule & b_deps);
void nth_root(interval const & a, unsigned n, numeral const & p, interval & b);
void nth_root_jst(interval const & a, unsigned n, numeral const & p, interval_deps & b_deps);
void nth_root_jst(interval const & a, unsigned n, numeral const & p, interval_deps_combine_rule & b_deps);
/**
\brief Given an equation x^n = y and an interval for y, compute the solution set for x with precision p.
\pre if n is even, then !lower_is_neg(y)
*/
void xn_eq_y(interval const & y, unsigned n, numeral const & p, interval & x, interval_deps & x_deps);
void xn_eq_y(interval const & y, unsigned n, numeral const & p, interval & x, interval_deps_combine_rule & x_deps);
void xn_eq_y(interval const & y, unsigned n, numeral const & p, interval & x);
void xn_eq_y_jst(interval const & y, unsigned n, numeral const & p, interval_deps & x_deps);
void xn_eq_y_jst(interval const & y, unsigned n, numeral const & p, interval_deps_combine_rule & x_deps);
/**
\brief b <- 1/a
\pre !contains_zero(a)
*/
void inv(interval const & a, interval & b, interval_deps & b_deps);
void inv(interval const & a, interval & b, interval_deps_combine_rule & b_deps);
void inv(interval const & a, interval & b);
void inv_jst(interval const & a, interval_deps & b_deps);
void inv_jst(interval const & a, interval_deps_combine_rule & b_deps);
/**
\brief c <- a/b
\pre !contains_zero(b)
\pre &a == &c (that is, c should not be an alias for a)
*/
void div(interval const & a, interval const & b, interval & c, interval_deps & c_deps);
void div(interval const & a, interval const & b, interval & c, interval_deps_combine_rule & c_deps);
void div(interval const & a, interval const & b, interval & c);
void div_jst(interval const & a, interval const & b, interval_deps & c_deps);
void div_jst(interval const & a, interval const & b, interval_deps_combine_rule & c_deps);
/**
\brief Store in r an interval that contains the number pi.

204
src/math/interval/interval_def.h
View file

@ -713,31 +713,31 @@ bool interval_manager<C>::before(interval const & a, interval const & b) const {
}
template<typename C>
void interval_manager<C>::neg_jst(interval const & a, interval_deps & b_deps) {
void interval_manager<C>::neg_jst(interval const & a, interval_deps_combine_rule & b_deps) {
if (lower_is_inf(a)) {
if (upper_is_inf(a)) {
b_deps.m_lower_deps = 0;
b_deps.m_upper_deps = 0;
b_deps.m_lower_combine = 0;
b_deps.m_upper_combine = 0;
}
else {
b_deps.m_lower_deps = DEP_IN_UPPER1;
b_deps.m_upper_deps = 0;
b_deps.m_lower_combine = DEP_IN_UPPER1;
b_deps.m_upper_combine = 0;
}
}
else {
if (upper_is_inf(a)) {
b_deps.m_lower_deps = 0;
b_deps.m_upper_deps = DEP_IN_LOWER1;
b_deps.m_lower_combine = 0;
b_deps.m_upper_combine = DEP_IN_LOWER1;
}
else {
b_deps.m_lower_deps = DEP_IN_UPPER1;
b_deps.m_upper_deps = DEP_IN_LOWER1;
b_deps.m_lower_combine = DEP_IN_UPPER1;
b_deps.m_upper_combine = DEP_IN_LOWER1;
}
}
}
template<typename C>
void interval_manager<C>::neg(interval const & a, interval & b, interval_deps & b_deps) {
void interval_manager<C>::neg(interval const & a, interval & b, interval_deps_combine_rule & b_deps) {
neg_jst(a, b_deps);
neg(a, b);
}
@ -792,13 +792,13 @@ void interval_manager<C>::neg(interval const & a, interval & b) {
}
template<typename C>
void interval_manager<C>::add_jst(interval const & a, interval const & b, interval_deps & c_deps) {
c_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2;
c_deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2;
void interval_manager<C>::add_jst(interval const & a, interval const & b, interval_deps_combine_rule & c_deps) {
c_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_LOWER2;
c_deps.m_upper_combine = DEP_IN_UPPER1 | DEP_IN_UPPER2;
}
template<typename C>
void interval_manager<C>::add(interval const & a, interval const & b, interval & c, interval_deps & c_deps) {
void interval_manager<C>::add(interval const & a, interval const & b, interval & c, interval_deps_combine_rule & c_deps) {
add_jst(a, b, c_deps);
add(a, b, c);
}
@ -818,13 +818,13 @@ void interval_manager<C>::add(interval const & a, interval const & b, interval &
}
template<typename C>
void interval_manager<C>::sub_jst(interval const & a, interval const & b, interval_deps & c_deps) {
c_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2;
c_deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2;
void interval_manager<C>::sub_jst(interval const & a, interval const & b, interval_deps_combine_rule & c_deps) {
c_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_UPPER2;
c_deps.m_upper_combine = DEP_IN_UPPER1 | DEP_IN_LOWER2;
}
template<typename C>
void interval_manager<C>::sub(interval const & a, interval const & b, interval & c, interval_deps & c_deps) {
void interval_manager<C>::sub(interval const & a, interval const & b, interval & c, interval_deps_combine_rule & c_deps) {
sub_jst(a, b, c_deps);
sub(a, b, c);
}
@ -844,18 +844,18 @@ void interval_manager<C>::sub(interval const & a, interval const & b, interval &
}
template<typename C>
void interval_manager<C>::mul_jst(numeral const & k, interval const & a, interval_deps & b_deps) {
void interval_manager<C>::mul_jst(numeral const & k, interval const & a, interval_deps_combine_rule & b_deps) {
if (m().is_zero(k)) {
b_deps.m_lower_deps = 0;
b_deps.m_upper_deps = 0;
b_deps.m_lower_combine = 0;
b_deps.m_upper_combine = 0;
}
else if (m().is_neg(k)) {
b_deps.m_lower_deps = DEP_IN_UPPER1;
b_deps.m_upper_deps = DEP_IN_LOWER1;
b_deps.m_lower_combine = DEP_IN_UPPER1;
b_deps.m_upper_combine = DEP_IN_LOWER1;
}
else {
b_deps.m_lower_deps = DEP_IN_LOWER1;
b_deps.m_upper_deps = DEP_IN_UPPER1;
b_deps.m_lower_combine = DEP_IN_LOWER1;
b_deps.m_upper_combine = DEP_IN_UPPER1;
}
}
@ -918,7 +918,7 @@ void interval_manager<C>::div_mul(numeral const & k, interval const & a, interva
}
template<typename C>
void interval_manager<C>::mul(numeral const & k, interval const & a, interval & b, interval_deps & b_deps) {
void interval_manager<C>::mul(numeral const & k, interval const & a, interval & b, interval_deps_combine_rule & b_deps) {
mul_jst(k, a, b_deps);
mul(k, a, b);
}
@ -931,57 +931,57 @@ void interval_manager<C>::mul(int n, int d, interval const & a, interval & b) {
}
template<typename C>
void interval_manager<C>::div(interval const & a, numeral const & k, interval & b, interval_deps & b_deps) {
void interval_manager<C>::div(interval const & a, numeral const & k, interval & b, interval_deps_combine_rule & b_deps) {
div_jst(a, k, b_deps);
div(a, k, b);
}
template<typename C>
void interval_manager<C>::mul_jst(interval const & i1, interval const & i2, interval_deps & r_deps) {
void interval_manager<C>::mul_jst(interval const & i1, interval const & i2, interval_deps_combine_rule & r_deps) {
if (is_zero(i1)) {
r_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
r_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
r_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1;
r_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1;
}
else if (is_zero(i2)) {
r_deps.m_lower_deps = DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_upper_deps = DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_lower_combine = DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_upper_combine = DEP_IN_LOWER2 | DEP_IN_UPPER2;
}
else if (is_N(i1)) {
if (is_N(i2)) {
// x <= b <= 0, y <= d <= 0 --> b*d <= x*y
// a <= x <= b <= 0, c <= y <= d <= 0 --> x*y <= a*c (we can use the fact that x or y is always negative (i.e., b is neg or d is neg))
r_deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2;
r_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER1; // we can replace DEP_IN_UPPER1 with DEP_IN_UPPER2
r_deps.m_lower_combine = DEP_IN_UPPER1 | DEP_IN_UPPER2;
r_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER1; // we can replace DEP_IN_UPPER1 with DEP_IN_UPPER2
}
else if (is_M(i2)) {
// a <= x <= b <= 0, y <= d, d > 0 --> a*d <= x*y (uses the fact that b is not positive)
// a <= x <= b <= 0, c <= y, c < 0 --> x*y <= a*c (uses the fact that b is not positive)
r_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2 | DEP_IN_UPPER1;
r_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER1;
r_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_UPPER2 | DEP_IN_UPPER1;
r_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER1;
}
else {
// a <= x <= b <= 0, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that x is neg (b is not positive) or y is pos (c is not negative))
// x <= b <= 0, 0 <= c <= y --> x*y <= b*c
r_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2 | DEP_IN_UPPER1; // we can replace DEP_IN_UPPER1 with DEP_IN_UPPER2
r_deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2;
r_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_UPPER2 | DEP_IN_UPPER1; // we can replace DEP_IN_UPPER1 with DEP_IN_UPPER2
r_deps.m_upper_combine = DEP_IN_UPPER1 | DEP_IN_LOWER2;
}
}
else if (is_M(i1)) {
if (is_N(i2)) {
// b > 0, x <= b, c <= y <= d <= 0 --> b*c <= x*y (uses the fact that d is not positive)
// a < 0, a <= x, c <= y <= d <= 0 --> x*y <= a*c (uses the fact that d is not positive)
r_deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_lower_combine = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
}
else if (is_M(i2)) {
r_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
}
else {
// a < 0, a <= x, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that c is not negative)
// b > 0, x <= b, 0 <= c <= y <= d --> x*y <= b*d (uses the fact that c is not negative)
r_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2 | DEP_IN_LOWER2;
r_deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2 | DEP_IN_LOWER2;
r_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_UPPER2 | DEP_IN_LOWER2;
r_deps.m_upper_combine = DEP_IN_UPPER1 | DEP_IN_UPPER2 | DEP_IN_LOWER2;
}
}
else {
@ -989,27 +989,27 @@ void interval_manager<C>::mul_jst(interval const & i1, interval const & i2, inte
if (is_N(i2)) {
// 0 <= a <= x <= b, c <= y <= d <= 0 --> x*y <= b*c (uses the fact that x is pos (a is not neg) or y is neg (d is not pos))
// 0 <= a <= x, y <= d <= 0 --> a*d <= x*y
r_deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_LOWER1; // we can replace DEP_IN_LOWER1 with DEP_IN_UPPER2
r_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2;
r_deps.m_lower_combine = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_LOWER1; // we can replace DEP_IN_LOWER1 with DEP_IN_UPPER2
r_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER2;
}
else if (is_M(i2)) {
// 0 <= a <= x <= b, c <= y --> b*c <= x*y (uses the fact that a is not negative)
// 0 <= a <= x <= b, y <= d --> x*y <= b*d (uses the fact that a is not negative)
r_deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_LOWER1;
r_deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2 | DEP_IN_LOWER1;
r_deps.m_lower_combine = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_LOWER1;
r_deps.m_upper_combine = DEP_IN_UPPER1 | DEP_IN_UPPER2 | DEP_IN_LOWER1;
}
else {
SASSERT(is_P(i2));
// 0 <= a <= x, 0 <= c <= y --> a*c <= x*y
// x <= b, y <= d --> x*y <= b*d (uses the fact that x is pos (a is not negative) or y is pos (c is not negative))
r_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2;
r_deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2 | DEP_IN_LOWER1; // we can replace DEP_IN_LOWER1 with DEP_IN_LOWER2
r_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_LOWER2;
r_deps.m_upper_combine = DEP_IN_UPPER1 | DEP_IN_UPPER2 | DEP_IN_LOWER1; // we can replace DEP_IN_LOWER1 with DEP_IN_LOWER2
}
}
}
template<typename C>
void interval_manager<C>::mul(interval const & i1, interval const & i2, interval & r, interval_deps & r_deps) {
void interval_manager<C>::mul(interval const & i1, interval const & i2, interval & r, interval_deps_combine_rule & r_deps) {
mul_jst(i1, i2, r_deps);
mul(i1, i2, r);
}
@ -1223,55 +1223,55 @@ void interval_manager<C>::mul(interval const & i1, interval const & i2, interval
}
template<typename C>
void interval_manager<C>::power_jst(interval const & a, unsigned n, interval_deps & b_deps) {
void interval_manager<C>::power_jst(interval const & a, unsigned n, interval_deps_combine_rule & b_deps) {
if (n == 1) {
b_deps.m_lower_deps = DEP_IN_LOWER1;
b_deps.m_upper_deps = DEP_IN_UPPER1;
b_deps.m_lower_combine = DEP_IN_LOWER1;
b_deps.m_upper_combine = DEP_IN_UPPER1;
}
else if (n % 2 == 0) {
if (lower_is_pos(a)) {
// [l, u]^n = [l^n, u^n] if l > 0
// 0 < l <= x --> l^n <= x^n (lower bound guarantees that is positive)
// 0 < l <= x <= u --> x^n <= u^n (use lower and upper bound -- need the fact that x is positive)
b_deps.m_lower_deps = DEP_IN_LOWER1;
b_deps.m_lower_combine = DEP_IN_LOWER1;
if (upper_is_inf(a))
b_deps.m_upper_deps = 0;
b_deps.m_upper_combine = 0;
else
b_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
b_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1;
}
else if (upper_is_neg(a)) {
// [l, u]^n = [u^n, l^n] if u < 0
// l <= x <= u < 0 --> x^n <= l^n (use lower and upper bound -- need the fact that x is negative)
// x <= u < 0 --> u^n <= x^n
b_deps.m_lower_deps = DEP_IN_UPPER1;
b_deps.m_lower_combine = DEP_IN_UPPER1;
if (lower_is_inf(a))
b_deps.m_upper_deps = 0;
b_deps.m_upper_combine = 0;
else
b_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
b_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1;
}
else {
// [l, u]^n = [0, max{l^n, u^n}] otherwise
// we need both bounds to justify upper bound
b_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
b_deps.m_lower_deps = 0;
b_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1;
b_deps.m_lower_combine = 0;
}
}
else {
// Remark: when n is odd x^n is monotonic.
if (lower_is_inf(a))
b_deps.m_lower_deps = 0;
b_deps.m_lower_combine = 0;
else
b_deps.m_lower_deps = DEP_IN_LOWER1;
b_deps.m_lower_combine = DEP_IN_LOWER1;
if (upper_is_inf(a))
b_deps.m_upper_deps = 0;
b_deps.m_upper_combine = 0;
else
b_deps.m_upper_deps = DEP_IN_UPPER1;
b_deps.m_upper_combine = DEP_IN_UPPER1;
}
}
template<typename C>
void interval_manager<C>::power(interval const & a, unsigned n, interval & b, interval_deps & b_deps) {
void interval_manager<C>::power(interval const & a, unsigned n, interval & b, interval_deps_combine_rule & b_deps) {
power_jst(a, n, b_deps);
power(a, n, b);
}
@ -1392,7 +1392,7 @@ void interval_manager<C>::power(interval const & a, unsigned n, interval & b) {
template<typename C>
void interval_manager<C>::nth_root(interval const & a, unsigned n, numeral const & p, interval & b, interval_deps & b_deps) {
void interval_manager<C>::nth_root(interval const & a, unsigned n, numeral const & p, interval & b, interval_deps_combine_rule & b_deps) {
nth_root_jst(a, n, p, b_deps);
nth_root(a, n, p, b);
}
@ -1437,16 +1437,16 @@ void interval_manager<C>::nth_root(interval const & a, unsigned n, numeral const
}
template<typename C>
void interval_manager<C>::nth_root_jst(interval const & a, unsigned n, numeral const & p, interval_deps & b_deps) {
b_deps.m_lower_deps = DEP_IN_LOWER1;
void interval_manager<C>::nth_root_jst(interval const & a, unsigned n, numeral const & p, interval_deps_combine_rule & b_deps) {
b_deps.m_lower_combine = DEP_IN_LOWER1;
if (n % 2 == 0)
b_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
b_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1;
else
b_deps.m_upper_deps = DEP_IN_UPPER1;
b_deps.m_upper_combine = DEP_IN_UPPER1;
}
template<typename C>
void interval_manager<C>::xn_eq_y(interval const & y, unsigned n, numeral const & p, interval & x, interval_deps & x_deps) {
void interval_manager<C>::xn_eq_y(interval const & y, unsigned n, numeral const & p, interval & x, interval_deps_combine_rule & x_deps) {
xn_eq_y_jst(y, n, p, x_deps);
xn_eq_y(y, n, p, x);
}
@ -1486,29 +1486,29 @@ void interval_manager<C>::xn_eq_y(interval const & y, unsigned n, numeral const
}
template<typename C>
void interval_manager<C>::xn_eq_y_jst(interval const & y, unsigned n, numeral const & p, interval_deps & x_deps) {
void interval_manager<C>::xn_eq_y_jst(interval const & y, unsigned n, numeral const & p, interval_deps_combine_rule & x_deps) {
if (n % 2 == 0) {
x_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
x_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
x_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1;
x_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1;
}
else {
x_deps.m_lower_deps = DEP_IN_LOWER1;
x_deps.m_upper_deps = DEP_IN_UPPER1;
x_deps.m_lower_combine = DEP_IN_LOWER1;
x_deps.m_upper_combine = DEP_IN_UPPER1;
}
}
template<typename C>
void interval_manager<C>::inv_jst(interval const & a, interval_deps & b_deps) {
void interval_manager<C>::inv_jst(interval const & a, interval_deps_combine_rule & b_deps) {
SASSERT(!contains_zero(a));
if (is_P1(a)) {
b_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
b_deps.m_upper_deps = DEP_IN_LOWER1;
b_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1;
b_deps.m_upper_combine = DEP_IN_LOWER1;
}
else if (is_N1(a)) {
// x <= u < 0 --> 1/u <= 1/x
// l <= x <= u < 0 --> 1/l <= 1/x (use lower and upper bounds)
b_deps.m_lower_deps = DEP_IN_UPPER1;
b_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
b_deps.m_lower_combine = DEP_IN_UPPER1;
b_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER1;
}
else {
UNREACHABLE();
@ -1516,7 +1516,7 @@ void interval_manager<C>::inv_jst(interval const & a, interval_deps & b_deps) {
}
template<typename C>
void interval_manager<C>::inv(interval const & a, interval & b, interval_deps & b_deps) {
void interval_manager<C>::inv(interval const & a, interval & b, interval_deps_combine_rule & b_deps) {
inv_jst(a, b_deps);
inv(a, b);
}
@ -1602,16 +1602,16 @@ void interval_manager<C>::inv(interval const & a, interval & b) {
}
template<typename C>
void interval_manager<C>::div_jst(interval const & i1, interval const & i2, interval_deps & r_deps) {
void interval_manager<C>::div_jst(interval const & i1, interval const & i2, interval_deps_combine_rule & r_deps) {
SASSERT(!contains_zero(i2));
if (is_zero(i1)) {
if (is_P1(i2)) {
r_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2;
r_deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2;
r_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_LOWER2;
r_deps.m_upper_combine = DEP_IN_UPPER1 | DEP_IN_LOWER2;
}
else {
r_deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2;
r_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2;
r_deps.m_lower_combine = DEP_IN_UPPER1 | DEP_IN_UPPER2;
r_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER2;
}
}
else {
@ -1619,28 +1619,28 @@ void interval_manager<C>::div_jst(interval const & i1, interval const & i2, inte
if (is_N1(i2)) {
// x <= b <= 0, c <= y <= d < 0 --> b/c <= x/y
// a <= x <= b <= 0, y <= d < 0 --> x/y <= a/d
r_deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2;
r_deps.m_lower_combine = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER2;
}
else {
// a <= x, a < 0, 0 < c <= y --> a/c <= x/y
// x <= b <= 0, 0 < c <= y <= d --> x/y <= b/d
r_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2;
r_deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_LOWER2;
r_deps.m_upper_combine = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
}
}
else if (is_M(i1)) {
if (is_N1(i2)) {
// 0 < a <= x <= b < 0, y <= d < 0 --> b/d <= x/y
// 0 < a <= x <= b < 0, y <= d < 0 --> x/y <= a/d
r_deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2;
r_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2;
r_deps.m_lower_combine = DEP_IN_UPPER1 | DEP_IN_UPPER2;
r_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_UPPER2;
}
else {
// 0 < a <= x <= b < 0, 0 < c <= y --> a/c <= x/y
// 0 < a <= x <= b < 0, 0 < c <= y --> x/y <= b/c
r_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2;
r_deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2;
r_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_LOWER2;
r_deps.m_upper_combine = DEP_IN_UPPER1 | DEP_IN_LOWER2;
}
}
else {
@ -1648,22 +1648,22 @@ void interval_manager<C>::div_jst(interval const & i1, interval const & i2, inte
if (is_N1(i2)) {
// b > 0, x <= b, c <= y <= d < 0 --> b/d <= x/y
// 0 <= a <= x, c <= y <= d < 0 --> x/y <= a/c
r_deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2;
r_deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_lower_combine = DEP_IN_UPPER1 | DEP_IN_UPPER2;
r_deps.m_upper_combine = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
}
else {
SASSERT(is_P1(i2));
// 0 <= a <= x, 0 < c <= y <= d --> a/d <= x/y
// b > 0 x <= b, 0 < c <= y --> x/y <= b/c
r_deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2;
r_deps.m_lower_combine = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2;
r_deps.m_upper_combine = DEP_IN_UPPER1 | DEP_IN_LOWER2;
}
}
}
}
template<typename C>
void interval_manager<C>::div(interval const & i1, interval const & i2, interval & r, interval_deps & r_deps) {
void interval_manager<C>::div(interval const & i1, interval const & i2, interval & r, interval_deps_combine_rule & r_deps) {
div_jst(i1, i2, r_deps);
div(i1, i2, r);
}

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

@ -145,29 +145,31 @@ interv horner::interval_of_expr(const nex& e) {
interv horner::interval_of_mul(const nex& e) {
SASSERT(e.is_mul());
auto & es = e.children();
SASSERT(es.size());
TRACE("nla_horner_details", tout << "e=" << e << "\n";);
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);
TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
return a;
}
TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
for (unsigned k = 1; k < es.size(); k++) {
interval_deps deps;
if (m_intervals.is_zero(a)) {
interv t;
set_interval_for_scalar(t, rational(1));
m_intervals.mul(a, t, a, deps);
m_intervals.add_deps(a, t, deps, a);
TRACE("nla_horner_details", tout << "got zero\n"; );
break;
}
interv b = interval_of_expr(es[k]);
if (m_intervals.is_zero(b)) {
m_intervals.set_zero_interval_deps_for_mult(b);
TRACE("nla_horner_details", tout << "es[k]= "<< es[k] << std::endl << ", "; m_intervals.display(tout, b); );
TRACE("nla_horner_details", tout << "got zero\n"; );
return b;
}
TRACE("nla_horner_details", tout << "es[k]= "<< es[k] << std::endl << ", "; m_intervals.display(tout, b); );
interv c;
m_intervals.mul(a, b, c, deps);
m_intervals.add_deps(a, b, deps, a);
m_intervals.mul(a, b, c, comb_rule);
m_intervals.combine_deps(a, b, comb_rule, a);
m_intervals.set(a, c);
TRACE("nla_horner_details", tout << "es[" << k << "]=" << es[k] << ", "; m_intervals.display(tout, a) << "\n";);
TRACE("nla_horner_details", tout << "part mult "; m_intervals.display(tout, a) << "\n";);
}
TRACE("nla_horner_details", tout << "e=" << e << "\n";
tout << " interv = "; m_intervals.display(tout, a););
tout << " return "; m_intervals.display(tout, a););
return a;
}
@ -190,10 +192,10 @@ interv horner::interval_of_sum(const nex& e) {
return b;
}
interv c;
interval_deps deps;
interval_deps_combine_rule combine_rule;
TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";);
m_intervals.add(a, b, c, deps);
m_intervals.add_deps(a, b, deps, a);
m_intervals.add(a, b, c, combine_rule);
m_intervals.combine_deps(a, b, combine_rule, a);
m_intervals.set(a, c);
TRACE("nla_horner_details_sum", tout << es[k] << ", ";
m_intervals.display(tout, a); tout << "\n";);
@ -209,7 +211,7 @@ interv horner::interval_of_sum(const nex& e) {
// sets the dependencies also
void horner::set_var_interval(lpvar v, interv& b) {
m_intervals.set_var_interval_with_deps(v, b);
TRACE("nla_horner_details", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b););
TRACE("nla_horner_details_var", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b););
}
}

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

@ -32,6 +32,11 @@ void intervals::set_var_interval_with_deps(lpvar v, interval& b) {
}
}
void intervals::set_zero_interval_deps_for_mult(interval& a) {
a.m_lower_dep = m_dep_manager.mk_join(a.m_lower_dep, a.m_upper_dep);
a.m_upper_dep = a.m_lower_dep;
}
bool intervals::check_interval_for_conflict_on_zero(const interval & i) {
return check_interval_for_conflict_on_zero_lower(i) || check_interval_for_conflict_on_zero_upper(i);
}

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

@ -74,9 +74,9 @@ class intervals : common {
};
void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const {
i.m_lower_dep = mk_dependency(a, b, deps.m_lower_deps);
i.m_upper_dep = mk_dependency(a, b, deps.m_upper_deps);
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);
}
@ -118,7 +118,7 @@ class intervals : common {
im_config(numeral_manager & m, ci_dependency_manager& d):m_manager(m), m_dep_manager(d) {}
private:
ci_dependency* mk_dependency(interval const& a, interval const& b, bound_deps bd) const {
ci_dependency* mk_dependency(interval const& a, interval const& b, deps_combine_rule bd) const {
ci_dependency* dep = nullptr;
if (dep_in_lower1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
@ -173,16 +173,19 @@ public:
bool is_zero(const interval& a) const { return m_config.is_zero(a); }
void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); }
void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); }
void add(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.add(a, b, c, deps); }
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); }
void mul(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.mul(a, b, c, deps); }
void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const {
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 {
m_config.add_deps(a, b, deps, i);
}
bool upper_is_inf(const interval& a) const { return m_config.upper_is_inf(a); }
bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); }
void set_var_interval_with_deps(lpvar, interval &);
void set_zero_interval_deps_for_mult(interval&);
bool is_inf(const interval& i) const { return m_config.is_inf(i); }
bool check_interval_for_conflict_on_zero(const interval & i);
bool check_interval_for_conflict_on_zero_lower(const interval & i);