Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] Improvement in satask: Adds support for querying Relational expressions. #17392

Open
wants to merge 5 commits into
base: master
Choose a base branch
from

Conversation

@ShubhamKJha
Copy link
Member

@ShubhamKJha ShubhamKJha commented Aug 12, 2019

References to other Issues or PRs

Uses #17118

Brief description of what is fixed or changed

[ Work In Progress - Do not merge ]
This is an attempt to allow simple queries related to Relationals in satask. E.g. the following now works:

from sympy import *
from sympy.abc import x,y,z
from sympy.assumptions.satask import satask

satask(Q.is_true(x>y), Q.positive(x) & Q.negative(y))  # True

However, more advanced queries ( satask(Q.is_true(x>y), Q.is_true(x>z) & Q.is_true(z>y)) ) are still not possible. It is similar to how old assumptions handles them.

Other comments

Release Notes

  • assumptions
    • Added support for using a single relational query in satask (similar to what is done in old assumptions).
@sympy-bot
Copy link

@sympy-bot sympy-bot commented Aug 12, 2019

Hi, I am the SymPy bot (v147). 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
    • Added support for using a single relational query in satask (similar to what is done in old assumptions). (#17392 by @oscargus and @ShubhamKJha)

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

Note: This comment will be updated with the latest check if you edit the pull request. You need to reload the page to see it.

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://github.com/blog/1506-closing-issues-via-pull-requests . Please also
write a comment on that issue linking back to this pull request once it is
open. -->
Uses #17118 

#### Brief description of what is fixed or changed
**[ Work In Progress - Do not merge ]**
This is an attempt to allow simple queries related to Relationals in satask. E.g. the following now works:
```py
from sympy import *
from sympy.abc import x,y,z
from sympy.assumptions.satask import satask

satask(Q.is_true(x>y), Q.positive(x) & Q.negative(y))  # True
```
However, more advanced queries ( `satask(Q.is_true(x>y), Q.is_true(x>z) & Q.is_true(z>y))` ) are still not possible. It is similar to how old assumptions handles them.

#### Other comments


#### 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
  * Added support for using a single relational query in satask (similar to what is done in old assumptions).
<!-- END RELEASE NOTES -->

@@ -298,6 +311,8 @@ def register_fact(klass, fact, registry=fact_registry):
(Add, Implies(AllArgs(Q.positive), Q.positive)),
(Add, Implies(AllArgs(Q.negative), Q.negative)),
(Mul, Implies(AllArgs(Q.positive), Q.positive)),
(Mul, Implies(AllArgs(~Q.zero) & OddNumberArgs(Q.negative), Q.negative)),
Copy link
Member

@asmeurer asmeurer Aug 12, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this generate an exponential number of predicates for an n-arg Mul? If so, that could be a major slowdown for ask if anyone uses a large Mul in an expression.

Copy link
Member Author

@ShubhamKJha ShubhamKJha Aug 12, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The other approach would be using something like this:
Q.negative(x*y*z) == Q.negative(x) ^ Q.negative(y * z)
and similarly for y * z. The number of symbols would then be increased but we can keep the number of clauses in check.

Copy link
Member

@asmeurer asmeurer Aug 12, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You mean Equivalent for == in that expression? I think that's basically what Tseitin does. It adds auxiliary variables to reduce the total number of clauses. #7174

We should benchmark which is faster for different sized Mul. In the worse case, we may need to limit OddNumberOfArgs to only generate a predicate for n < some value.

@asmeurer
Copy link
Member

@asmeurer asmeurer commented Aug 12, 2019

I think ask should support relationals as boolean predicates directly (like ask(x > y) instead of ask(Q.is_true(x>y)). I don't know if it's better to also allow those at the handler level, or to translate them to is_true so that everything uses Predicate objects, or to remove is_true and have x > y handled directly.

@asmeurer
Copy link
Member

@asmeurer asmeurer commented Aug 21, 2019

Make sure to update the docstring of ask() here.

@czgdp1807
Copy link
Member

@czgdp1807 czgdp1807 commented Feb 25, 2020

@ShubhamKJha Any news on this? Please let me know if someone can take this over.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

None yet

5 participants