|
|
"""
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
|