Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

floor and ceiling inequality simplification #17313

Merged
merged 1 commit into from Aug 19, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
100 changes: 99 additions & 1 deletion sympy/functions/elementary/integers.py
Expand Up @@ -142,6 +142,12 @@ def _eval_nseries(self, x, n, logx):
else:
return r

def _eval_is_negative(self):
return self.args[0].is_negative

def _eval_is_nonnegative(self):
return self.args[0].is_nonnegative

def _eval_rewrite_as_ceiling(self, arg, **kwargs):
return -ceiling(-arg)

Expand All @@ -155,17 +161,60 @@ def _eval_Eq(self, other):
return S.true

def __le__(self, other):
other = S(other)
if self.args[0].is_real:
if other.is_integer:
return self.args[0] < other + 1
if other.is_number and other.is_real:
return self.args[0] < ceiling(other)
if self.args[0] == other and other.is_real:
return S.true
if other is S.Infinity and self.is_finite:
return S.true

return Le(self, other, evaluate=False)

def __ge__(self, other):
other = S(other)
if self.args[0].is_real:
if other.is_integer:
return self.args[0] >= other
if other.is_number and other.is_real:
return self.args[0] >= ceiling(other)
if self.args[0] == other and other.is_real:
return S.false
if other is S.NegativeInfinity and self.is_finite:
return S.true

return Ge(self, other, evaluate=False)

def __gt__(self, other):
other = S(other)
if self.args[0].is_real:
if other.is_integer:
return self.args[0] >= other + 1
if other.is_number and other.is_real:
return self.args[0] >= ceiling(other)
if self.args[0] == other and other.is_real:
return S.false
if other is S.NegativeInfinity and self.is_finite:
return S.true

return Gt(self, other, evaluate=False)

def __lt__(self, other):
other = S(other)
if self.args[0].is_real:
if other.is_integer:
return self.args[0] < other
if other.is_number and other.is_real:
return self.args[0] < ceiling(other)
if self.args[0] == other and other.is_real:
return S.false
if other is S.Infinity and self.is_finite:
return S.true

return Lt(self, other, evaluate=False)

class ceiling(RoundFunction):
"""
Expand Down Expand Up @@ -234,24 +283,73 @@ def _eval_rewrite_as_floor(self, arg, **kwargs):
def _eval_rewrite_as_frac(self, arg, **kwargs):
return arg + frac(-arg)

def _eval_is_positive(self):
return self.args[0].is_positive

ethankward marked this conversation as resolved.
Show resolved Hide resolved
def _eval_is_nonpositive(self):
return self.args[0].is_nonpositive

def _eval_Eq(self, other):
if isinstance(self, ceiling):
if (self.rewrite(floor) == other) or \
(self.rewrite(frac) == other):
return S.true

def __lt__(self, other):
other = S(other)
if self.args[0].is_real:
if other.is_integer:
return self.args[0] <= other - 1
if other.is_number and other.is_real:
return self.args[0] <= floor(other)
if self.args[0] == other and other.is_real:
return S.false
if other is S.Infinity and self.is_finite:
return S.true

return Lt(self, other, evaluate=False)

def __gt__(self, other):
other = S(other)
if self.args[0].is_real:
if other.is_integer:
return self.args[0] > other
if other.is_number and other.is_real:
return self.args[0] > floor(other)
if self.args[0] == other and other.is_real:
return S.false
if other is S.NegativeInfinity and self.is_finite:
return S.true

return Gt(self, other, evaluate=False)

def __ge__(self, other):
other = S(other)
if self.args[0].is_real:
if other.is_integer:
return self.args[0] > other - 1
if other.is_number and other.is_real:
return self.args[0] > floor(other)
if self.args[0] == other and other.is_real:
return S.true
if other is S.NegativeInfinity and self.is_real:
if other is S.NegativeInfinity and self.is_finite:
return S.true

return Ge(self, other, evaluate=False)

def __le__(self, other):
other = S(other)
if self.args[0].is_real:
if other.is_integer:
return self.args[0] <= other
if other.is_number and other.is_real:
return self.args[0] <= floor(other)
if self.args[0] == other and other.is_real:
return S.false
oscargus marked this conversation as resolved.
Show resolved Hide resolved
if other is S.Infinity and self.is_finite:
return S.true

return Le(self, other, evaluate=False)

class frac(Function):
r"""Represents the fractional part of x
Expand Down
138 changes: 138 additions & 0 deletions sympy/functions/elementary/tests/test_integers.py
Expand Up @@ -108,13 +108,18 @@ def test_floor():
assert floor(factorial(50)/exp(1)) == \
11188719610782480504630258070757734324011354208865721592720336800

assert (floor(y) < y) == False
assert (floor(y) <= y) == True
assert (floor(y) > y) == False
assert (floor(y) >= y) == False
assert (floor(x) <= x).is_Relational # x could be non-real
assert (floor(x) > x).is_Relational
assert (floor(x) <= y).is_Relational # arg is not same as rhs
assert (floor(x) > y).is_Relational
assert (floor(y) <= oo) == True
assert (floor(y) < oo) == True
assert (floor(y) >= -oo) == True
assert (floor(y) > -oo) == True

assert floor(y).rewrite(frac) == y - frac(y)
assert floor(y).rewrite(ceiling) == -ceiling(-y)
Expand All @@ -126,6 +131,70 @@ def test_floor():
assert Eq(floor(y), y - frac(y))
assert Eq(floor(y), -ceiling(-y))

neg = Symbol('neg', negative=True)
nn = Symbol('nn', nonnegative=True)
pos = Symbol('pos', positive=True)
np = Symbol('np', nonpositive=True)

assert (floor(neg) < 0) == True
assert (floor(neg) <= 0) == True
assert (floor(neg) > 0) == False
assert (floor(neg) >= 0) == False
assert (floor(neg) <= -1) == True
assert (floor(neg) >= -3) == (neg >= -3)
assert (floor(neg) < 5) == (neg < 5)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this not be True?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just tested with this PR and (neg < 5) evaluates to True so it would be best to change the test here.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not a big deal though and this looks good so I'll merge.


assert (floor(nn) < 0) == False
assert (floor(nn) >= 0) == True

assert (floor(pos) < 0) == False
assert (floor(pos) <= 0) == (pos < 1)
assert (floor(pos) > 0) == (pos >= 1)
assert (floor(pos) >= 0) == True
assert (floor(pos) >= 3) == (pos >= 3)

assert (floor(np) <= 0) == True
assert (floor(np) > 0) == False

ethankward marked this conversation as resolved.
Show resolved Hide resolved
assert floor(neg).is_negative == True
assert floor(neg).is_nonnegative == False
assert floor(nn).is_negative == False
assert floor(nn).is_nonnegative == True
assert floor(pos).is_negative == False
assert floor(pos).is_nonnegative == True
assert floor(np).is_negative is None
assert floor(np).is_nonnegative is None

assert (floor(7, evaluate=False) >= 7) == True
assert (floor(7, evaluate=False) > 7) == False
assert (floor(7, evaluate=False) <= 7) == True
assert (floor(7, evaluate=False) < 7) == False

assert (floor(7, evaluate=False) >= 6) == True
assert (floor(7, evaluate=False) > 6) == True
assert (floor(7, evaluate=False) <= 6) == False
assert (floor(7, evaluate=False) < 6) == False

assert (floor(7, evaluate=False) >= 8) == False
assert (floor(7, evaluate=False) > 8) == False
assert (floor(7, evaluate=False) <= 8) == True
assert (floor(7, evaluate=False) < 8) == True

assert (floor(x) <= 5.5) == Le(floor(x), 5.5, evaluate=False)
assert (floor(x) >= -3.2) == Ge(floor(x), -3.2, evaluate=False)
assert (floor(x) < 2.9) == Lt(floor(x), 2.9, evaluate=False)
assert (floor(x) > -1.7) == Gt(floor(x), -1.7, evaluate=False)

assert (floor(y) <= 5.5) == (y < 6)
assert (floor(y) >= -3.2) == (y >= -3)
assert (floor(y) < 2.9) == (y < 3)
assert (floor(y) > -1.7) == (y >= -1)

assert (floor(y) <= n) == (y < n + 1)
assert (floor(y) >= n) == (y >= n)
assert (floor(y) < n) == (y < n)
assert (floor(y) > n) == (y >= n + 1)


def test_ceiling():

Expand Down Expand Up @@ -225,12 +294,17 @@ def test_ceiling():
11188719610782480504630258070757734324011354208865721592720336801

assert (ceiling(y) >= y) == True
assert (ceiling(y) > y) == False
assert (ceiling(y) < y) == False
assert (ceiling(y) <= y) == False
assert (ceiling(x) >= x).is_Relational # x could be non-real
assert (ceiling(x) < x).is_Relational
assert (ceiling(x) >= y).is_Relational # arg is not same as rhs
assert (ceiling(x) < y).is_Relational
assert (ceiling(y) >= -oo) == True
assert (ceiling(y) > -oo) == True
assert (ceiling(y) <= oo) == True
assert (ceiling(y) < oo) == True

assert ceiling(y).rewrite(floor) == -floor(-y)
assert ceiling(y).rewrite(frac) == y + frac(-y)
Expand All @@ -242,6 +316,70 @@ def test_ceiling():
assert Eq(ceiling(y), y + frac(-y))
assert Eq(ceiling(y), -floor(-y))

neg = Symbol('neg', negative=True)
nn = Symbol('nn', nonnegative=True)
pos = Symbol('pos', positive=True)
np = Symbol('np', nonpositive=True)

assert (ceiling(neg) <= 0) == True
assert (ceiling(neg) < 0) == (neg <= -1)
assert (ceiling(neg) > 0) == False
assert (ceiling(neg) >= 0) == (neg > -1)
assert (ceiling(neg) > -3) == (neg > -3)
assert (ceiling(neg) <= 10) == (neg <= 10)

assert (ceiling(nn) < 0) == False
assert (ceiling(nn) >= 0) == True

ethankward marked this conversation as resolved.
Show resolved Hide resolved
assert (ceiling(pos) < 0) == False
assert (ceiling(pos) <= 0) == False
assert (ceiling(pos) > 0) == True
assert (ceiling(pos) >= 0) == True
assert (ceiling(pos) >= 1) == True
assert (ceiling(pos) > 5) == (pos > 5)

assert (ceiling(np) <= 0) == True
assert (ceiling(np) > 0) == False

assert ceiling(neg).is_positive == False
assert ceiling(neg).is_nonpositive == True
assert ceiling(nn).is_positive is None
assert ceiling(nn).is_nonpositive is None
assert ceiling(pos).is_positive == True
assert ceiling(pos).is_nonpositive == False
assert ceiling(np).is_positive == False
assert ceiling(np).is_nonpositive == True

assert (ceiling(7, evaluate=False) >= 7) == True
assert (ceiling(7, evaluate=False) > 7) == False
assert (ceiling(7, evaluate=False) <= 7) == True
assert (ceiling(7, evaluate=False) < 7) == False

assert (ceiling(7, evaluate=False) >= 6) == True
assert (ceiling(7, evaluate=False) > 6) == True
assert (ceiling(7, evaluate=False) <= 6) == False
assert (ceiling(7, evaluate=False) < 6) == False

assert (ceiling(7, evaluate=False) >= 8) == False
assert (ceiling(7, evaluate=False) > 8) == False
assert (ceiling(7, evaluate=False) <= 8) == True
assert (ceiling(7, evaluate=False) < 8) == True

assert (ceiling(x) <= 5.5) == Le(ceiling(x), 5.5, evaluate=False)
assert (ceiling(x) >= -3.2) == Ge(ceiling(x), -3.2, evaluate=False)
assert (ceiling(x) < 2.9) == Lt(ceiling(x), 2.9, evaluate=False)
assert (ceiling(x) > -1.7) == Gt(ceiling(x), -1.7, evaluate=False)

assert (ceiling(y) <= 5.5) == (y <= 5)
assert (ceiling(y) >= -3.2) == (y > -4)
assert (ceiling(y) < 2.9) == (y <= 2)
assert (ceiling(y) > -1.7) == (y > -2)

assert (ceiling(y) <= n) == (y <= n)
assert (ceiling(y) >= n) == (y > n - 1)
assert (ceiling(y) < n) == (y <= n - 1)
assert (ceiling(y) > n) == (y > n)


def test_frac():
assert isinstance(frac(x), frac)
Expand Down