Spaces:
Sleeping
Sleeping
""" | |
This module contains query handlers responsible for calculus queries: | |
infinitesimal, finite, etc. | |
""" | |
from sympy.assumptions import Q, ask | |
from sympy.core import Add, Mul, Pow, Symbol | |
from sympy.core.numbers import (NegativeInfinity, GoldenRatio, | |
Infinity, Exp1, ComplexInfinity, ImaginaryUnit, NaN, Number, Pi, E, | |
TribonacciConstant) | |
from sympy.functions import cos, exp, log, sign, sin | |
from sympy.logic.boolalg import conjuncts | |
from ..predicates.calculus import (FinitePredicate, InfinitePredicate, | |
PositiveInfinitePredicate, NegativeInfinitePredicate) | |
# FinitePredicate | |
def _(expr, assumptions): | |
""" | |
Handles Symbol. | |
""" | |
if expr.is_finite is not None: | |
return expr.is_finite | |
if Q.finite(expr) in conjuncts(assumptions): | |
return True | |
return None | |
def _(expr, assumptions): | |
""" | |
Return True if expr is bounded, False if not and None if unknown. | |
Truth Table: | |
+-------+-----+-----------+-----------+ | |
| | | | | | |
| | B | U | ? | | |
| | | | | | |
+-------+-----+---+---+---+---+---+---+ | |
| | | | | | | | | | |
| | |'+'|'-'|'x'|'+'|'-'|'x'| | |
| | | | | | | | | | |
+-------+-----+---+---+---+---+---+---+ | |
| | | | | | |
| B | B | U | ? | | |
| | | | | | |
+---+---+-----+---+---+---+---+---+---+ | |
| | | | | | | | | | | |
| |'+'| | U | ? | ? | U | ? | ? | | |
| | | | | | | | | | | |
| +---+-----+---+---+---+---+---+---+ | |
| | | | | | | | | | | |
| U |'-'| | ? | U | ? | ? | U | ? | | |
| | | | | | | | | | | |
| +---+-----+---+---+---+---+---+---+ | |
| | | | | | | |
| |'x'| | ? | ? | | |
| | | | | | | |
+---+---+-----+---+---+---+---+---+---+ | |
| | | | | | |
| ? | | | ? | | |
| | | | | | |
+-------+-----+-----------+---+---+---+ | |
* 'B' = Bounded | |
* 'U' = Unbounded | |
* '?' = unknown boundedness | |
* '+' = positive sign | |
* '-' = negative sign | |
* 'x' = sign unknown | |
* All Bounded -> True | |
* 1 Unbounded and the rest Bounded -> False | |
* >1 Unbounded, all with same known sign -> False | |
* Any Unknown and unknown sign -> None | |
* Else -> None | |
When the signs are not the same you can have an undefined | |
result as in oo - oo, hence 'bounded' is also undefined. | |
""" | |
sign = -1 # sign of unknown or infinite | |
result = True | |
for arg in expr.args: | |
_bounded = ask(Q.finite(arg), assumptions) | |
if _bounded: | |
continue | |
s = ask(Q.extended_positive(arg), assumptions) | |
# if there has been more than one sign or if the sign of this arg | |
# is None and Bounded is None or there was already | |
# an unknown sign, return None | |
if sign != -1 and s != sign or \ | |
s is None and None in (_bounded, sign): | |
return None | |
else: | |
sign = s | |
# once False, do not change | |
if result is not False: | |
result = _bounded | |
return result | |
def _(expr, assumptions): | |
""" | |
Return True if expr is bounded, False if not and None if unknown. | |
Truth Table: | |
+---+---+---+--------+ | |
| | | | | | |
| | B | U | ? | | |
| | | | | | |
+---+---+---+---+----+ | |
| | | | | | | |
| | | | s | /s | | |
| | | | | | | |
+---+---+---+---+----+ | |
| | | | | | |
| B | B | U | ? | | |
| | | | | | |
+---+---+---+---+----+ | |
| | | | | | | |
| U | | U | U | ? | | |
| | | | | | | |
+---+---+---+---+----+ | |
| | | | | | |
| ? | | | ? | | |
| | | | | | |
+---+---+---+---+----+ | |
* B = Bounded | |
* U = Unbounded | |
* ? = unknown boundedness | |
* s = signed (hence nonzero) | |
* /s = not signed | |
""" | |
result = True | |
for arg in expr.args: | |
_bounded = ask(Q.finite(arg), assumptions) | |
if _bounded: | |
continue | |
elif _bounded is None: | |
if result is None: | |
return None | |
if ask(Q.extended_nonzero(arg), assumptions) is None: | |
return None | |
if result is not False: | |
result = None | |
else: | |
result = False | |
return result | |
def _(expr, assumptions): | |
""" | |
* Unbounded ** NonZero -> Unbounded | |
* Bounded ** Bounded -> Bounded | |
* Abs()<=1 ** Positive -> Bounded | |
* Abs()>=1 ** Negative -> Bounded | |
* Otherwise unknown | |
""" | |
if expr.base == E: | |
return ask(Q.finite(expr.exp), assumptions) | |
base_bounded = ask(Q.finite(expr.base), assumptions) | |
exp_bounded = ask(Q.finite(expr.exp), assumptions) | |
if base_bounded is None and exp_bounded is None: # Common Case | |
return None | |
if base_bounded is False and ask(Q.extended_nonzero(expr.exp), assumptions): | |
return False | |
if base_bounded and exp_bounded: | |
return True | |
if (abs(expr.base) <= 1) == True and ask(Q.extended_positive(expr.exp), assumptions): | |
return True | |
if (abs(expr.base) >= 1) == True and ask(Q.extended_negative(expr.exp), assumptions): | |
return True | |
if (abs(expr.base) >= 1) == True and exp_bounded is False: | |
return False | |
return None | |
def _(expr, assumptions): | |
return ask(Q.finite(expr.exp), assumptions) | |
def _(expr, assumptions): | |
# After complex -> finite fact is registered to new assumption system, | |
# querying Q.infinite may be removed. | |
if ask(Q.infinite(expr.args[0]), assumptions): | |
return False | |
return ask(~Q.zero(expr.args[0]), assumptions) | |
def _(expr, assumptions): | |
return True | |
def _(expr, assumptions): | |
return False | |
def _(expr, assumptions): | |
return None | |
# InfinitePredicate | |
def _(expr, assumptions): | |
return True | |
# PositiveInfinitePredicate | |
def _(expr, assumptions): | |
return True | |
def _(expr, assumptions): | |
return False | |
# NegativeInfinitePredicate | |
def _(expr, assumptions): | |
return True | |
def _(expr, assumptions): | |
return False | |