Spaces:
Sleeping
Sleeping
File size: 6,313 Bytes
6a86ad5 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 |
"""
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 arguments 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
|