Merge pull request #21152 from JSS95/binrelpreds

feat(assumptions) : Implement relational predicates

sympy/assumptions/__init__.py

@@ -8,11 +8,11 @@
 )
 from .ask import Q, ask, register_handler, remove_handler
 from .refine import refine
-from .relation import BinaryRelation
+from .relation import BinaryRelation, AppliedBinaryRelation
 
 __all__ = [
     'AppliedPredicate', 'Predicate', 'AssumptionsContext', 'assuming',
     'global_assumptions', 'Q', 'ask', 'register_handler', 'remove_handler',
     'refine',
-    'BinaryRelation'
+    'BinaryRelation', 'AppliedBinaryRelation'
 ]

sympy/assumptions/ask.py

@@ -249,6 +249,26 @@ def ne(self):
         from .relation.equality import UnequalityPredicate
         return UnequalityPredicate()
 
+    @memoize_property
+    def gt(self):
+        from .relation.equality import StrictGreaterThanPredicate
+        return StrictGreaterThanPredicate()
+
+    @memoize_property
+    def ge(self):
+        from .relation.equality import GreaterThanPredicate
+        return GreaterThanPredicate()
+
+    @memoize_property
+    def lt(self):
+        from .relation.equality import StrictLessThanPredicate
+        return StrictLessThanPredicate()
+
+    @memoize_property
+    def le(self):
+        from .relation.equality import LessThanPredicate
+        return LessThanPredicate()
+
 
 Q = AssumptionKeys()
 
@@ -318,8 +338,10 @@ def ask(proposition, assumptions=True, context=global_assumptions):
 
     This function evaluates the proposition to ``True`` or ``False`` if
     the truth value can be determined. If not, it returns ``None``.
-    It should be discerned from :func:`~.refine()` which does not reduce
-    the expression to ``None``.
+
+    It should be discerned from :func:`~.refine()` which, when applied to a
+    proposition, simplifies the argument to symbolic ``Boolean`` instead of
+    Python built-in ``True``, ``False`` or ``None``.
 
     Parameters
     ==========

sympy/assumptions/ask_generated.py

@@ -185,6 +185,8 @@ def get_known_facts_dict():
         Q.extended_real: set([Q.extended_real]),
         Q.finite: set([Q.finite]),
         Q.fullrank: set([Q.fullrank]),
+        Q.ge: set([Q.ge]),
+        Q.gt: set([Q.gt]),
         Q.hermitian: set([Q.hermitian]),
         Q.imaginary: set([Q.antihermitian, Q.complex, Q.imaginary]),
         Q.infinite: set([Q.extended_real, Q.infinite]),
@@ -196,7 +198,9 @@ def get_known_facts_dict():
         Q.irrational: set([Q.complex, Q.extended_real, Q.finite, Q.hermitian,
         Q.irrational, Q.nonzero, Q.real]),
         Q.is_true: set([Q.is_true]),
+        Q.le: set([Q.le]),
         Q.lower_triangular: set([Q.lower_triangular, Q.triangular]),
+        Q.lt: set([Q.lt]),
         Q.ne: set([Q.ne]),
         Q.negative: set([Q.complex, Q.extended_real, Q.hermitian, Q.negative,
         Q.nonpositive, Q.nonzero, Q.real]),

sympy/assumptions/predicates/common.py

@@ -1,4 +1,4 @@
-from sympy.assumptions import Predicate
+from sympy.assumptions import Predicate, AppliedPredicate
 from sympy.multipledispatch import Dispatcher
 
 
@@ -26,19 +26,37 @@ class IsTruePredicate(Predicate):
     ===========
 
     ``ask(Q.is_true(x))`` is true iff ``x`` is true. This only makes
-    sense if ``x`` is a predicate.
+    sense if ``x`` is a boolean object.
 
     Examples
     ========
 
-    >>> from sympy import ask, Q, symbols
-    >>> x = symbols('x')
+    >>> from sympy import ask, Q
+    >>> from sympy.abc import x
     >>> ask(Q.is_true(True))
     True
 
+    Wrapping another applied predicate just returns the applied predicate.
+
+    >>> Q.is_true(Q.even(x))
+    Q.even(x)
+
+    Notes
+    =====
+
+    This class is designed to wrap the boolean objects so that they can
+    behave as if they are applied predicates. Consequently, wrapping another
+    applied predicate is unnecessary and thus it just returns the argument.
+
     """
     name = 'is_true'
     handler = Dispatcher(
         "IsTrueHandler",
         doc="Wrapper allowing to query the truth value of a boolean expression."
     )
+
+    def __call__(self, arg):
+        # No need to wrap another predicate
+        if isinstance(arg, AppliedPredicate):
+            return arg
+        return super().__call__(arg)

sympy/assumptions/refine.py

@@ -18,8 +18,8 @@ def refine(expr, assumptions=True):
     the form which is only valid under certain assumptions. Note that
     ``simplify()`` is generally not done in refining process.
 
-    Refining boolean expression involves reducing it to ``True`` or
-    ``False``. Unlike :func:~.`ask()`, the expression will not be reduced
+    Refining boolean expression involves reducing it to ``S.true`` or
+    ``S.false``. Unlike :func:`~.ask()`, the expression will not be reduced
     if the truth value cannot be determined.
 
     Examples

sympy/assumptions/relation/binrel.py

@@ -4,8 +4,8 @@
 
 from sympy import S
 from sympy.assumptions import AppliedPredicate, ask, Predicate
-from sympy.core.compatibility import ordered
 from sympy.core.kind import BooleanKind
+from sympy.logic.boolalg import conjuncts, Not
 
 __all__ = ["BinaryRelation", "AppliedBinaryRelation"]
 
@@ -32,38 +32,38 @@ class BinaryRelation(Predicate):
     >>> from sympy import Q, ask, sin, cos
     >>> from sympy.abc import x
     >>> Q.eq(sin(x)**2+cos(x)**2, 1)
-    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
+    >>> from sympy import ask, Number, Q
     >>> from sympy.assumptions import BinaryRelation
     >>> class MyRel(BinaryRelation):
     ...     name = "R"
     ...     is_reflexive = False
-    >>> R = MyRel()
-    >>> @R.register(Number, Number)
+    >>> Q.R = MyRel()
+    >>> @Q.R.register(Number, Number)
     ... def _(n1, n2, assumptions):
     ...     return ask(Q.zero(n1 - n2 - 1), assumptions)
-    >>> R(2, 1)
-    2 R 1
+    >>> Q.R(2, 1)
+    Q.R(2, 1)
 
     Now, we can use ``ask()`` to evaluate it to boolean value.
 
-    >>> ask(R(2, 1))
+    >>> ask(Q.R(2, 1))
     True
-    >>> ask(R(1, 2))
+    >>> ask(Q.R(1, 2))
     False
 
-    ``R`` returns ``False`` with minimum cost if two arguments have same
-    structure because R is antireflexive relation [1] by
+    ``Q.R`` returns ``False`` with minimum cost if two arguments have same
+    structure because it is antireflexive relation [1] by
     ``is_reflexive = False``.
 
-    >>> ask(R(x, x))
+    >>> ask(Q.R(x, x))
     False
 
     References
@@ -114,7 +114,7 @@ def eval(self, args, assumptions=True):
         if ret is not None:
             return ret
 
-        # don't perform simplify here. (done by AppliedBinaryRelation._eval_ask)
+        # 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)
@@ -129,14 +129,6 @@ def eval(self, args, assumptions=True):
 
         return ret
 
-    def _simplify_applied(self, lhs, rhs, **kwargs):
-        lhs, rhs = lhs.simplify(**kwargs), rhs.simplify(**kwargs)
-        return self(lhs, rhs)
-
-    def _eval_binary_symbols(self, lhs, rhs):
-        # override where necessary
-        return set()
-
 
 class AppliedBinaryRelation(AppliedPredicate):
     """
@@ -181,68 +173,30 @@ def reversedsign(self):
     def negated(self):
         neg_rel = self.function.negated
         if neg_rel is None:
-            return ~self
+            return Not(self, evaluate=False)
         return neg_rel(*self.arguments)
 
-    @property
-    def canonical(self):
-        """
-        Return a canonical form of the relational by putting a
-        number on the rhs, canonically removing a sign or else
-        ordering the args canonically. No other simplification is
-        attempted.
-        """
-        args = self.arguments
-        r = self
-        if r.rhs.is_number:
-            if any(side is S.NaN for side in (r.lhs, r.rhs)):
-                pass
-            elif r.rhs.is_Number and r.lhs.is_Number and r.lhs > r.rhs:
-                r = r.reversed
-        elif r.lhs.is_number:
-            r = r.reversed
-        elif tuple(ordered(args)) != args:
-            r = r.reversed
-
-        LHS_CEMS = getattr(r.lhs, 'could_extract_minus_sign', None)
-        RHS_CEMS = getattr(r.rhs, 'could_extract_minus_sign', None)
-
-        if any(side.kind is BooleanKind for side in r.arguments):
-            return r
-
-        # Check if first value has negative sign
-        if LHS_CEMS and LHS_CEMS():
-            return r.reversedsign
-        elif not r.rhs.is_number and RHS_CEMS and RHS_CEMS():
-            # Right hand side has a minus, but not lhs.
-            # How does the expression with reversed signs behave?
-            # This is so that expressions of the type
-            # Eq(x, -y) and Eq(-x, y)
-            # have the same canonical representation
-            expr1, _ = ordered([r.lhs, -r.rhs])
-            if expr1 != r.lhs:
-                return r.reversed.reversedsign
-
-        return r
-
     def _eval_ask(self, assumptions):
+        # After CNF in assumptions module is modified to take polyadic
+        # predicate, this will be removed
+        if any(rel in conjuncts(assumptions) 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 conjuncts(assumptions) 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 and try again
-        rel = self.simplify()
-        return rel.function.eval(rel.arguments, assumptions)
-
-    def _eval_simplify(self, **kwargs):
-        return self.function._simplify_applied(self.lhs, self.rhs, **kwargs)
+        # 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
-
-    @property
-    def binary_symbols(self):
-        return self.function._eval_binary_symbols(*self.arguments)