123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212 |
- """
- General binary relations.
- """
- from typing import Optional
- from sympy.core.singleton import S
- from sympy.assumptions import AppliedPredicate, ask, Predicate, Q # type: ignore
- from sympy.core.kind import BooleanKind
- from sympy.core.relational import Eq, Ne, Gt, Lt, Ge, Le
- from sympy.logic.boolalg import conjuncts, Not
- __all__ = ["BinaryRelation", "AppliedBinaryRelation"]
- class BinaryRelation(Predicate):
- """
- Base class for all binary relational predicates.
- Explanation
- ===========
- Binary relation takes two arguments and returns ``AppliedBinaryRelation``
- instance. To evaluate it to boolean value, use :obj:`~.ask()` or
- :obj:`~.refine()` function.
- You can add support for new types by registering the handler to dispatcher.
- See :obj:`~.Predicate()` for more information about predicate dispatching.
- Examples
- ========
- Applying and evaluating to boolean value:
- >>> from sympy import Q, ask, sin, cos
- >>> from sympy.abc import x
- >>> Q.eq(sin(x)**2+cos(x)**2, 1)
- Q.eq(sin(x)**2 + cos(x)**2, 1)
- >>> ask(_)
- True
- You can define a new binary relation by subclassing and dispatching.
- Here, we define a relation $R$ such that $x R y$ returns true if
- $x = y + 1$.
- >>> from sympy import ask, Number, Q
- >>> from sympy.assumptions import BinaryRelation
- >>> class MyRel(BinaryRelation):
- ... name = "R"
- ... is_reflexive = False
- >>> Q.R = MyRel()
- >>> @Q.R.register(Number, Number)
- ... def _(n1, n2, assumptions):
- ... return ask(Q.zero(n1 - n2 - 1), assumptions)
- >>> Q.R(2, 1)
- Q.R(2, 1)
- Now, we can use ``ask()`` to evaluate it to boolean value.
- >>> ask(Q.R(2, 1))
- True
- >>> ask(Q.R(1, 2))
- False
- ``Q.R`` returns ``False`` with minimum cost if two arguments have same
- structure because it is antireflexive relation [1] by
- ``is_reflexive = False``.
- >>> ask(Q.R(x, x))
- False
- References
- ==========
- .. [1] https://en.wikipedia.org/wiki/Reflexive_relation
- """
- is_reflexive: Optional[bool] = None
- is_symmetric: Optional[bool] = None
- def __call__(self, *args):
- if not len(args) == 2:
- raise ValueError("Binary relation takes two arguments, but got %s." % len(args))
- return AppliedBinaryRelation(self, *args)
- @property
- def reversed(self):
- if self.is_symmetric:
- return self
- return None
- @property
- def negated(self):
- return None
- def _compare_reflexive(self, lhs, rhs):
- # quick exit for structurally same arguments
- # do not check != here because it cannot catch the
- # equivalent arguements with different structures.
- # reflexivity does not hold to NaN
- if lhs is S.NaN or rhs is S.NaN:
- return None
- reflexive = self.is_reflexive
- if reflexive is None:
- pass
- elif reflexive and (lhs == rhs):
- return True
- elif not reflexive and (lhs == rhs):
- return False
- return None
- def eval(self, args, assumptions=True):
- # quick exit for structurally same arguments
- ret = self._compare_reflexive(*args)
- if ret is not None:
- return ret
- # don't perform simplify on args here. (done by AppliedBinaryRelation._eval_ask)
- # evaluate by multipledispatch
- lhs, rhs = args
- ret = self.handler(lhs, rhs, assumptions=assumptions)
- if ret is not None:
- return ret
- # check reversed order if the relation is reflexive
- if self.is_reflexive:
- types = (type(lhs), type(rhs))
- if self.handler.dispatch(*types) is not self.handler.dispatch(*reversed(types)):
- ret = self.handler(rhs, lhs, assumptions=assumptions)
- return ret
- class AppliedBinaryRelation(AppliedPredicate):
- """
- The class of expressions resulting from applying ``BinaryRelation``
- to the arguments.
- """
- @property
- def lhs(self):
- """The left-hand side of the relation."""
- return self.arguments[0]
- @property
- def rhs(self):
- """The right-hand side of the relation."""
- return self.arguments[1]
- @property
- def reversed(self):
- """
- Try to return the relationship with sides reversed.
- """
- revfunc = self.function.reversed
- if revfunc is None:
- return self
- return revfunc(self.rhs, self.lhs)
- @property
- def reversedsign(self):
- """
- Try to return the relationship with signs reversed.
- """
- revfunc = self.function.reversed
- if revfunc is None:
- return self
- if not any(side.kind is BooleanKind for side in self.arguments):
- return revfunc(-self.lhs, -self.rhs)
- return self
- @property
- def negated(self):
- neg_rel = self.function.negated
- if neg_rel is None:
- return Not(self, evaluate=False)
- return neg_rel(*self.arguments)
- def _eval_ask(self, assumptions):
- conj_assumps = set()
- binrelpreds = {Eq: Q.eq, Ne: Q.ne, Gt: Q.gt, Lt: Q.lt, Ge: Q.ge, Le: Q.le}
- for a in conjuncts(assumptions):
- if a.func in binrelpreds:
- conj_assumps.add(binrelpreds[type(a)](*a.args))
- else:
- conj_assumps.add(a)
- # After CNF in assumptions module is modified to take polyadic
- # predicate, this will be removed
- if any(rel in conj_assumps for rel in (self, self.reversed)):
- return True
- neg_rels = (self.negated, self.reversed.negated, Not(self, evaluate=False),
- Not(self.reversed, evaluate=False))
- if any(rel in conj_assumps for rel in neg_rels):
- return False
- # evaluation using multipledispatching
- ret = self.function.eval(self.arguments, assumptions)
- if ret is not None:
- return ret
- # simplify the args and try again
- args = tuple(a.simplify() for a in self.arguments)
- return self.function.eval(args, assumptions)
- def __bool__(self):
- ret = ask(self)
- if ret is None:
- raise TypeError("Cannot determine truth value of %s" % self)
- return ret
|