Introduce polyadic predicate based on multipledispatch

[JSS95]

References to other Issues or PRs

Closes #20209

Brief description of what is fixed or changed

This PR improves the predicate and handler design in assumptions module.

1. Assumption handlers are now multipledispatch instance. Predicate now uses a single handler instead of a list of handlers.
2. Predicate("...") now returns UndefinedPredicate, which cannot be evaluated. To make predicate that can be evaluated, subclass of Predicate must be defined.
3. Predicate can now take multiple arguments.

This PR does not break back compatibility. Existing handlers are not yet migrated to this new design. It will be done in succeeding PRs.

Also, printing of predicates is improved and tests are added.

Other comments

Previous handler design was very unstable. It made Predicate mutable, it filters the argument by its class "name", and could not take multiple arguments. This new multipledispatch design fixes these.

Just as Function('f') returns undefined function which cannot be evaluated, Predicate('...') returns UndefinedPredicate in this PR. This instance does not have handler and cannot be evaluated by its own, but it can be used to construct expressions like Not and evaluated by SAT solver.

To define a new predicate with handler, new predicate class must be defined and functions must be dispatched to its handler. For example,

    class SexyPredicate(Predicate):
        """https://en.wikipedia.org/wiki/Sexy_prime"""
        name = "sexyprime"
    Q.sexyprime = SexyPredicate()

    @Q.sexyprime.register(Integer, Integer)
    def _(int1, int2, assumptions):
        args = sorted([int1, int2])
        if not all(ask(Q.prime(a), assumptions) for a in args):
            return False
        return args[1] - args[0] == 6

    @Q.sexyprime.register(Integer, Integer, Integer)
    def _(int1, int2, int3, assumptions):
        args = sorted([int1, int2, int3])
        if not all(ask(Q.prime(a), assumptions) for a in args):
            return False
        return args[2] - args[1] == 6 and args[1] - args[0] == 6

Evaluating this to boolean is done by ask as usual.

>>> ask(Q.sexyprime(5, 11))
True
>>> ask(Q.sexyprime(7, 13, 19))
True

Release Notes

• assumptions
  • Predicate now uses a single handler which is multipledispatch instance.
  • Predicate can now take multiple arguments.
  • Predicate("...") now returns UndefinedPredicate instance. To define a predicate, you must make a subclass of Predicate.

[sympy-bot]

✅

Hi, I am the SymPy bot (v161). I'm here to help you write a release notes entry. Please read the guide on how to write release notes.

Your release notes are in good order.

Here is what the release notes will look like:

• assumptions

  • Predicate now uses a single handler which is multipledispatch instance. (#20656 by @JSS95)

  • Predicate can now take multiple arguments. (#20656 by @JSS95)

  • Predicate("...") now returns UndefinedPredicate instance. To define a predicate, you must make a subclass of Predicate. (#20656 by @JSS95)

This will be added to https://github.com/sympy/sympy/wiki/Release-Notes-for-1.8.

Click here to see the pull request description that was parsed.

<!-- Your title above should be a short description of what
was changed. Do not include the issue number in the title. -->

#### References to other Issues or PRs
<!-- If this pull request fixes an issue, write "Fixes #NNNN" in that exact
format, e.g. "Fixes #1234" (see
https://tinyurl.com/auto-closing for more information). Also, please
write a comment on that issue linking back to this pull request once it is
open. -->
Closes #20209

#### Brief description of what is fixed or changed

This PR improves the predicate and handler design in `assumptions` module.

1. Assumption handlers are now multipledispatch instance. Predicate now uses a single handler instead of a list of handlers.
2. `Predicate("...")` now returns `UndefinedPredicate`, which cannot be evaluated. To make predicate that can be evaluated, subclass of `Predicate` must be defined.
3. `Predicate` can now take multiple arguments.

This PR does not break back compatibility. Existing handlers are not yet migrated to this new design. It will be done in succeeding PRs.

Also, printing of predicates is improved and tests are added.

#### Other comments

Previous handler design was very unstable. It made `Predicate` mutable, it filters the argument by its class "name", and could not take multiple arguments. This new multipledispatch design fixes these.

Just as `Function('f')` returns undefined function which cannot be evaluated, `Predicate('...')` returns `UndefinedPredicate` in this PR. This instance does not have handler and cannot be evaluated by its own, but it can be used to construct expressions like `Not` and evaluated by SAT solver.

To define a new predicate with handler, new predicate class must be defined and functions must be dispatched to its handler. For example,

```python
    class SexyPredicate(Predicate):
        """https://en.wikipedia.org/wiki/Sexy_prime"""
        name = "sexyprime"
    Q.sexyprime = SexyPredicate()

    @Q.sexyprime.register(Integer, Integer)
    def _(int1, int2, assumptions):
        args = sorted([int1, int2])
        if not all(ask(Q.prime(a), assumptions) for a in args):
            return False
        return args[1] - args[0] == 6

    @Q.sexyprime.register(Integer, Integer, Integer)
    def _(int1, int2, int3, assumptions):
        args = sorted([int1, int2, int3])
        if not all(ask(Q.prime(a), assumptions) for a in args):
            return False
        return args[2] - args[1] == 6 and args[1] - args[0] == 6
```
Evaluating this to boolean is done by `ask` as usual.
```python
>>> ask(Q.sexyprime(5, 11))
True
>>> ask(Q.sexyprime(7, 13, 19))
True
```

#### Release Notes

<!-- Write the release notes for this release below. See
https://github.com/sympy/sympy/wiki/Writing-Release-Notes for more information
on how to write release notes. The bot will check your release notes
automatically to see if they are formatted correctly. -->

<!-- BEGIN RELEASE NOTES -->
- assumptions
    - `Predicate` now uses a single handler which is multipledispatch instance.
    - `Predicate` can now take multiple arguments.
    - `Predicate("...")` now returns `UndefinedPredicate` instance. To define a predicate, you must make a subclass of `Predicate`.
<!-- END RELEASE NOTES -->

Update

The release notes on the wiki have been updated.

[JSS95]

I collected some previous PRs to this one. Ping to the reviewers who participated in older versions - @oscarbenjamin @asmeurer @eric-wieser . Can you take a look at this, please?

[JSS95]

Ping again @oscarbenjamin , @asmeurer , @eric-wieser

[oscarbenjamin]

Why is this method needed? Can we not just let the Basic.args property return the args as normal?

[JSS95]

Normal way will return AppliedPredicate for Q.even(2).func and (Q.even, (2,)) for Q.even(2).args.

By overriding args like this, we can make Q.even(2).func return Q.even and Q.even(2).args return (2,). I think this way is better since we should give different heads for different predicates, such as Q.even(), Q.odd(), Q.positive(), ... etc.

[oscarbenjamin]

I think this way is better since we should give different heads for different predicates

I don't understand what this means.

I think that almost all cases where args is overridden like this in the sympy codebase are warts to be removed. This always leads to problems down the line and it would generally be better if we could just accept the Basic model of func and args rather than fighting it.

(I realise that this wasn't added by you)

[JSS95]

Makes sense. I will try fixing it.

[JSS95]

I tried to fix this, but func and args were used everywhere in assumptions module that it exceeds the scope of this PR. I will make another PR for this.

[oscarbenjamin]

Fair enough.

In general I think that if args is different from _args then something is wrong. At least they could be made equal and .func could be made to work with whatever is stored in _args.

Generally though everything is smoother if obj.func is type(obj) and _args is the args that would be passed to it. This eliminates the needs for a lot of hacky workarounds.

Having the predicate not in args means it can't be substituted e.g.:

In [1]: p = Q.even(x)

In [2]: p
Out[2]: Q.even(x)

In [3]: p.subs(Q.even, Q.odd)
Out[3]: Q.even(x)

The analogy with functions is

In [4]: sin(x).subs(sin, cos)
Out[4]: cos(x)

In [5]: f(x).subs(f, g)
Out[5]: g(x)

This is made to work in a hacky way because sin, cos, f and g are not Basic. If they were Basic and f(x) was just Call(Function('f'), Symbol('x')) then subs would work automatically. That's what what we want to aim for in Function and it's one of the chief advantages of having the function objects themselves be Basic. Disallowing that in the case of Predicate seems backward to me.

At the same time code should not make any presumptions about what obj.func is except that it can be called with the args as obj.func(*obj.args) so if obj.func is being used for anything else then that should be changed as well.

[oscarbenjamin]

I left some comments but broadly I think this looks good.

Should the docs recommend using UndefinedPredicate rather than Predicate as a way of creating undefined predicates?

[oscarbenjamin]

@asmeurer @eric-wieser do you want to review this?

[JSS95]

Should the docs recommend using UndefinedPredicate rather than Predicate as a way of creating undefined predicates?

I designed the Predicate to mimic Function. Since we encourage Function('f') to generate undefined function, I think we should encourage to use Predicate('P').

[JSS95]

@oscarbenjamin I introduced function property to return the predicate, and arguments property to return the arguments. I will remove the usage of overridden args and func in succeeding PR.

[oscarbenjamin]

It would be better if we could avoid using a metaclass but otherwise I think this looks good.

@asmeurer @eric-wieser do you want to review?

[JSS95]

Squashed the commits

[JSS95]

@oscarbenjamin
Considering that previous PRs had not been reviewed for months for the others, I doubt that there will be any more. Can this PR be merged?

[eric-wieser]

Some grammar fixes and documentation suggestions

[JSS95]

Thanks for the review!

[oscarbenjamin]

Okay this looks good. Thanks and sorry for the long wait on this!

[oscarbenjamin]

Does the new predicate system here fix this problem #20635 (comment)?