binrel.py 6.2 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212
  1. """
  2. General binary relations.
  3. """
  4. from typing import Optional
  5. from sympy.core.singleton import S
  6. from sympy.assumptions import AppliedPredicate, ask, Predicate, Q # type: ignore
  7. from sympy.core.kind import BooleanKind
  8. from sympy.core.relational import Eq, Ne, Gt, Lt, Ge, Le
  9. from sympy.logic.boolalg import conjuncts, Not
  10. __all__ = ["BinaryRelation", "AppliedBinaryRelation"]
  11. class BinaryRelation(Predicate):
  12. """
  13. Base class for all binary relational predicates.
  14. Explanation
  15. ===========
  16. Binary relation takes two arguments and returns ``AppliedBinaryRelation``
  17. instance. To evaluate it to boolean value, use :obj:`~.ask()` or
  18. :obj:`~.refine()` function.
  19. You can add support for new types by registering the handler to dispatcher.
  20. See :obj:`~.Predicate()` for more information about predicate dispatching.
  21. Examples
  22. ========
  23. Applying and evaluating to boolean value:
  24. >>> from sympy import Q, ask, sin, cos
  25. >>> from sympy.abc import x
  26. >>> Q.eq(sin(x)**2+cos(x)**2, 1)
  27. Q.eq(sin(x)**2 + cos(x)**2, 1)
  28. >>> ask(_)
  29. True
  30. You can define a new binary relation by subclassing and dispatching.
  31. Here, we define a relation $R$ such that $x R y$ returns true if
  32. $x = y + 1$.
  33. >>> from sympy import ask, Number, Q
  34. >>> from sympy.assumptions import BinaryRelation
  35. >>> class MyRel(BinaryRelation):
  36. ... name = "R"
  37. ... is_reflexive = False
  38. >>> Q.R = MyRel()
  39. >>> @Q.R.register(Number, Number)
  40. ... def _(n1, n2, assumptions):
  41. ... return ask(Q.zero(n1 - n2 - 1), assumptions)
  42. >>> Q.R(2, 1)
  43. Q.R(2, 1)
  44. Now, we can use ``ask()`` to evaluate it to boolean value.
  45. >>> ask(Q.R(2, 1))
  46. True
  47. >>> ask(Q.R(1, 2))
  48. False
  49. ``Q.R`` returns ``False`` with minimum cost if two arguments have same
  50. structure because it is antireflexive relation [1] by
  51. ``is_reflexive = False``.
  52. >>> ask(Q.R(x, x))
  53. False
  54. References
  55. ==========
  56. .. [1] https://en.wikipedia.org/wiki/Reflexive_relation
  57. """
  58. is_reflexive: Optional[bool] = None
  59. is_symmetric: Optional[bool] = None
  60. def __call__(self, *args):
  61. if not len(args) == 2:
  62. raise ValueError("Binary relation takes two arguments, but got %s." % len(args))
  63. return AppliedBinaryRelation(self, *args)
  64. @property
  65. def reversed(self):
  66. if self.is_symmetric:
  67. return self
  68. return None
  69. @property
  70. def negated(self):
  71. return None
  72. def _compare_reflexive(self, lhs, rhs):
  73. # quick exit for structurally same arguments
  74. # do not check != here because it cannot catch the
  75. # equivalent arguements with different structures.
  76. # reflexivity does not hold to NaN
  77. if lhs is S.NaN or rhs is S.NaN:
  78. return None
  79. reflexive = self.is_reflexive
  80. if reflexive is None:
  81. pass
  82. elif reflexive and (lhs == rhs):
  83. return True
  84. elif not reflexive and (lhs == rhs):
  85. return False
  86. return None
  87. def eval(self, args, assumptions=True):
  88. # quick exit for structurally same arguments
  89. ret = self._compare_reflexive(*args)
  90. if ret is not None:
  91. return ret
  92. # don't perform simplify on args here. (done by AppliedBinaryRelation._eval_ask)
  93. # evaluate by multipledispatch
  94. lhs, rhs = args
  95. ret = self.handler(lhs, rhs, assumptions=assumptions)
  96. if ret is not None:
  97. return ret
  98. # check reversed order if the relation is reflexive
  99. if self.is_reflexive:
  100. types = (type(lhs), type(rhs))
  101. if self.handler.dispatch(*types) is not self.handler.dispatch(*reversed(types)):
  102. ret = self.handler(rhs, lhs, assumptions=assumptions)
  103. return ret
  104. class AppliedBinaryRelation(AppliedPredicate):
  105. """
  106. The class of expressions resulting from applying ``BinaryRelation``
  107. to the arguments.
  108. """
  109. @property
  110. def lhs(self):
  111. """The left-hand side of the relation."""
  112. return self.arguments[0]
  113. @property
  114. def rhs(self):
  115. """The right-hand side of the relation."""
  116. return self.arguments[1]
  117. @property
  118. def reversed(self):
  119. """
  120. Try to return the relationship with sides reversed.
  121. """
  122. revfunc = self.function.reversed
  123. if revfunc is None:
  124. return self
  125. return revfunc(self.rhs, self.lhs)
  126. @property
  127. def reversedsign(self):
  128. """
  129. Try to return the relationship with signs reversed.
  130. """
  131. revfunc = self.function.reversed
  132. if revfunc is None:
  133. return self
  134. if not any(side.kind is BooleanKind for side in self.arguments):
  135. return revfunc(-self.lhs, -self.rhs)
  136. return self
  137. @property
  138. def negated(self):
  139. neg_rel = self.function.negated
  140. if neg_rel is None:
  141. return Not(self, evaluate=False)
  142. return neg_rel(*self.arguments)
  143. def _eval_ask(self, assumptions):
  144. conj_assumps = set()
  145. binrelpreds = {Eq: Q.eq, Ne: Q.ne, Gt: Q.gt, Lt: Q.lt, Ge: Q.ge, Le: Q.le}
  146. for a in conjuncts(assumptions):
  147. if a.func in binrelpreds:
  148. conj_assumps.add(binrelpreds[type(a)](*a.args))
  149. else:
  150. conj_assumps.add(a)
  151. # After CNF in assumptions module is modified to take polyadic
  152. # predicate, this will be removed
  153. if any(rel in conj_assumps for rel in (self, self.reversed)):
  154. return True
  155. neg_rels = (self.negated, self.reversed.negated, Not(self, evaluate=False),
  156. Not(self.reversed, evaluate=False))
  157. if any(rel in conj_assumps for rel in neg_rels):
  158. return False
  159. # evaluation using multipledispatching
  160. ret = self.function.eval(self.arguments, assumptions)
  161. if ret is not None:
  162. return ret
  163. # simplify the args and try again
  164. args = tuple(a.simplify() for a in self.arguments)
  165. return self.function.eval(args, assumptions)
  166. def __bool__(self):
  167. ret = ask(self)
  168. if ret is None:
  169. raise TypeError("Cannot determine truth value of %s" % self)
  170. return ret