calculus.py 7.0 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258
  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 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. for arg in expr.args:
  126. _bounded = ask(Q.finite(arg), assumptions)
  127. if _bounded:
  128. continue
  129. elif _bounded is None:
  130. if result is None:
  131. return None
  132. if ask(Q.extended_nonzero(arg), assumptions) is None:
  133. return None
  134. if result is not False:
  135. result = None
  136. else:
  137. result = False
  138. return result
  139. @FinitePredicate.register(Pow)
  140. def _(expr, assumptions):
  141. """
  142. * Unbounded ** NonZero -> Unbounded
  143. * Bounded ** Bounded -> Bounded
  144. * Abs()<=1 ** Positive -> Bounded
  145. * Abs()>=1 ** Negative -> Bounded
  146. * Otherwise unknown
  147. """
  148. if expr.base == E:
  149. return ask(Q.finite(expr.exp), assumptions)
  150. base_bounded = ask(Q.finite(expr.base), assumptions)
  151. exp_bounded = ask(Q.finite(expr.exp), assumptions)
  152. if base_bounded is None and exp_bounded is None: # Common Case
  153. return None
  154. if base_bounded is False and ask(Q.extended_nonzero(expr.exp), assumptions):
  155. return False
  156. if base_bounded and exp_bounded:
  157. return True
  158. if (abs(expr.base) <= 1) == True and ask(Q.extended_positive(expr.exp), assumptions):
  159. return True
  160. if (abs(expr.base) >= 1) == True and ask(Q.extended_negative(expr.exp), assumptions):
  161. return True
  162. if (abs(expr.base) >= 1) == True and exp_bounded is False:
  163. return False
  164. return None
  165. @FinitePredicate.register(exp)
  166. def _(expr, assumptions):
  167. return ask(Q.finite(expr.exp), assumptions)
  168. @FinitePredicate.register(log)
  169. def _(expr, assumptions):
  170. # After complex -> finite fact is registered to new assumption system,
  171. # querying Q.infinite may be removed.
  172. if ask(Q.infinite(expr.args[0]), assumptions):
  173. return False
  174. return ask(~Q.zero(expr.args[0]), assumptions)
  175. @FinitePredicate.register_many(cos, sin, Number, Pi, Exp1, GoldenRatio,
  176. TribonacciConstant, ImaginaryUnit, sign)
  177. def _(expr, assumptions):
  178. return True
  179. @FinitePredicate.register_many(ComplexInfinity, Infinity, NegativeInfinity)
  180. def _(expr, assumptions):
  181. return False
  182. @FinitePredicate.register(NaN)
  183. def _(expr, assumptions):
  184. return None
  185. # InfinitePredicate
  186. @InfinitePredicate.register_many(ComplexInfinity, Infinity, NegativeInfinity)
  187. def _(expr, assumptions):
  188. return True
  189. # PositiveInfinitePredicate
  190. @PositiveInfinitePredicate.register(Infinity)
  191. def _(expr, assumptions):
  192. return True
  193. @PositiveInfinitePredicate.register_many(NegativeInfinity, ComplexInfinity)
  194. def _(expr, assumptions):
  195. return False
  196. # NegativeInfinitePredicate
  197. @NegativeInfinitePredicate.register(NegativeInfinity)
  198. def _(expr, assumptions):
  199. return True
  200. @NegativeInfinitePredicate.register_many(Infinity, ComplexInfinity)
  201. def _(expr, assumptions):
  202. return False