calculus.py 7.6 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273
  1. """
  2. This module contains query handlers responsible for calculus queries:
  3. infinitesimal, finite, etc.
  4. """
  5. from sympy.assumptions import Q, ask
  6. from sympy.core import Expr, Add, Mul, Pow, Symbol
  7. from sympy.core.numbers import (NegativeInfinity, GoldenRatio,
  8. Infinity, Exp1, ComplexInfinity, ImaginaryUnit, NaN, Number, Pi, E,
  9. TribonacciConstant)
  10. from sympy.functions import cos, exp, log, sign, sin
  11. from sympy.logic.boolalg import conjuncts
  12. from ..predicates.calculus import (FinitePredicate, InfinitePredicate,
  13. PositiveInfinitePredicate, NegativeInfinitePredicate)
  14. # FinitePredicate
  15. @FinitePredicate.register(Symbol)
  16. def _(expr, assumptions):
  17. """
  18. Handles Symbol.
  19. """
  20. if expr.is_finite is not None:
  21. return expr.is_finite
  22. if Q.finite(expr) in conjuncts(assumptions):
  23. return True
  24. return None
  25. @FinitePredicate.register(Add)
  26. def _(expr, assumptions):
  27. """
  28. Return True if expr is bounded, False if not and None if unknown.
  29. Truth Table:
  30. +-------+-----+-----------+-----------+
  31. | | | | |
  32. | | B | U | ? |
  33. | | | | |
  34. +-------+-----+---+---+---+---+---+---+
  35. | | | | | | | | |
  36. | | |'+'|'-'|'x'|'+'|'-'|'x'|
  37. | | | | | | | | |
  38. +-------+-----+---+---+---+---+---+---+
  39. | | | | |
  40. | B | B | U | ? |
  41. | | | | |
  42. +---+---+-----+---+---+---+---+---+---+
  43. | | | | | | | | | |
  44. | |'+'| | U | ? | ? | U | ? | ? |
  45. | | | | | | | | | |
  46. | +---+-----+---+---+---+---+---+---+
  47. | | | | | | | | | |
  48. | U |'-'| | ? | U | ? | ? | U | ? |
  49. | | | | | | | | | |
  50. | +---+-----+---+---+---+---+---+---+
  51. | | | | | |
  52. | |'x'| | ? | ? |
  53. | | | | | |
  54. +---+---+-----+---+---+---+---+---+---+
  55. | | | | |
  56. | ? | | | ? |
  57. | | | | |
  58. +-------+-----+-----------+---+---+---+
  59. * 'B' = Bounded
  60. * 'U' = Unbounded
  61. * '?' = unknown boundedness
  62. * '+' = positive sign
  63. * '-' = negative sign
  64. * 'x' = sign unknown
  65. * All Bounded -> True
  66. * 1 Unbounded and the rest Bounded -> False
  67. * >1 Unbounded, all with same known sign -> False
  68. * Any Unknown and unknown sign -> None
  69. * Else -> None
  70. When the signs are not the same you can have an undefined
  71. result as in oo - oo, hence 'bounded' is also undefined.
  72. """
  73. sign = -1 # sign of unknown or infinite
  74. result = True
  75. for arg in expr.args:
  76. _bounded = ask(Q.finite(arg), assumptions)
  77. if _bounded:
  78. continue
  79. s = ask(Q.extended_positive(arg), assumptions)
  80. # if there has been more than one sign or if the sign of this arg
  81. # is None and Bounded is None or there was already
  82. # an unknown sign, return None
  83. if sign != -1 and s != sign or \
  84. s is None and None in (_bounded, sign):
  85. return None
  86. else:
  87. sign = s
  88. # once False, do not change
  89. if result is not False:
  90. result = _bounded
  91. return result
  92. @FinitePredicate.register(Mul)
  93. def _(expr, assumptions):
  94. """
  95. Return True if expr is bounded, False if not and None if unknown.
  96. Truth Table:
  97. +---+---+---+--------+
  98. | | | | |
  99. | | B | U | ? |
  100. | | | | |
  101. +---+---+---+---+----+
  102. | | | | | |
  103. | | | | s | /s |
  104. | | | | | |
  105. +---+---+---+---+----+
  106. | | | | |
  107. | B | B | U | ? |
  108. | | | | |
  109. +---+---+---+---+----+
  110. | | | | | |
  111. | U | | U | U | ? |
  112. | | | | | |
  113. +---+---+---+---+----+
  114. | | | | |
  115. | ? | | | ? |
  116. | | | | |
  117. +---+---+---+---+----+
  118. * B = Bounded
  119. * U = Unbounded
  120. * ? = unknown boundedness
  121. * s = signed (hence nonzero)
  122. * /s = not signed
  123. """
  124. result = True
  125. possible_zero = False
  126. for arg in expr.args:
  127. _bounded = ask(Q.finite(arg), assumptions)
  128. if _bounded:
  129. if ask(Q.zero(arg), assumptions) is not False:
  130. if result is False:
  131. return None
  132. possible_zero = True
  133. elif _bounded is None:
  134. if result is None:
  135. return None
  136. if ask(Q.extended_nonzero(arg), assumptions) is None:
  137. return None
  138. if result is not False:
  139. result = None
  140. else:
  141. if possible_zero:
  142. return None
  143. result = False
  144. return result
  145. @FinitePredicate.register(Pow)
  146. def _(expr, assumptions):
  147. """
  148. * Unbounded ** NonZero -> Unbounded
  149. * Bounded ** Bounded -> Bounded
  150. * Abs()<=1 ** Positive -> Bounded
  151. * Abs()>=1 ** Negative -> Bounded
  152. * Otherwise unknown
  153. """
  154. if expr.base == E:
  155. return ask(Q.finite(expr.exp), assumptions)
  156. base_bounded = ask(Q.finite(expr.base), assumptions)
  157. exp_bounded = ask(Q.finite(expr.exp), assumptions)
  158. if base_bounded is None and exp_bounded is None: # Common Case
  159. return None
  160. if base_bounded is False and ask(Q.extended_nonzero(expr.exp), assumptions):
  161. return False
  162. if base_bounded and exp_bounded:
  163. is_base_zero = ask(Q.zero(expr.base),assumptions)
  164. is_exp_negative = ask(Q.negative(expr.exp),assumptions)
  165. if is_base_zero is True and is_exp_negative is True:
  166. return False
  167. if is_base_zero is not False and is_exp_negative is not False:
  168. return None
  169. return True
  170. if (abs(expr.base) <= 1) == True and ask(Q.extended_positive(expr.exp), assumptions):
  171. return True
  172. if (abs(expr.base) >= 1) == True and ask(Q.extended_negative(expr.exp), assumptions):
  173. return True
  174. if (abs(expr.base) >= 1) == True and exp_bounded is False:
  175. return False
  176. return None
  177. @FinitePredicate.register(exp)
  178. def _(expr, assumptions):
  179. return ask(Q.finite(expr.exp), assumptions)
  180. @FinitePredicate.register(log)
  181. def _(expr, assumptions):
  182. # After complex -> finite fact is registered to new assumption system,
  183. # querying Q.infinite may be removed.
  184. if ask(Q.infinite(expr.args[0]), assumptions):
  185. return False
  186. return ask(~Q.zero(expr.args[0]), assumptions)
  187. @FinitePredicate.register_many(cos, sin, Number, Pi, Exp1, GoldenRatio,
  188. TribonacciConstant, ImaginaryUnit, sign)
  189. def _(expr, assumptions):
  190. return True
  191. @FinitePredicate.register_many(ComplexInfinity, Infinity, NegativeInfinity)
  192. def _(expr, assumptions):
  193. return False
  194. @FinitePredicate.register(NaN)
  195. def _(expr, assumptions):
  196. return None
  197. # InfinitePredicate
  198. @InfinitePredicate.register(Expr)
  199. def _(expr, assumptions):
  200. is_finite = Q.finite(expr)._eval_ask(assumptions)
  201. if is_finite is None:
  202. return None
  203. return not is_finite
  204. # PositiveInfinitePredicate
  205. @PositiveInfinitePredicate.register(Infinity)
  206. def _(expr, assumptions):
  207. return True
  208. @PositiveInfinitePredicate.register_many(NegativeInfinity, ComplexInfinity)
  209. def _(expr, assumptions):
  210. return False
  211. # NegativeInfinitePredicate
  212. @NegativeInfinitePredicate.register(NegativeInfinity)
  213. def _(expr, assumptions):
  214. return True
  215. @NegativeInfinitePredicate.register_many(Infinity, ComplexInfinity)
  216. def _(expr, assumptions):
  217. return False