feat(assumptions): reorganize facts for new assumptions #21279

JSS95 · 2021-04-09T15:38:42Z

References to other Issues or PRs

Fixes #21228

Brief description of what is fixed or changed

Q.positive_infinite() and Q.negative_infinite() predicates are introduced.
Q.extended_positive(), Q.extended_negative(), Q.extended_nonzero(), Q.extended_nonpositive(), and Q.extended_nonnegative() predicates are introduced.
Q.positive() and Q.negative() now correctly implies the argument being finite.
Incorrect results from Q.hermitian() and Q.antihermitian() are fixed.
In order to reduce the complexity of sat solver, some predicates are now decomposed into a combination of primitive predicates.
Facts are now defined in assumptions/facts.py, instead of in assumptions/ask.py.

Other comments

Benchmark showed no slowdown.

Release Notes

assumptions
- Q.positive_infinite() and Q.negative_infinite() predicates are introduced.
- Q.extended_positive(), Q.extended_negative(), Q.extended_nonzero(), Q.extended_nonpositive(), and Q.extended_nonnegative() predicates are introduced.
- Q.positive() and Q.negative() now correctly implies the argument being finite.
- Incorrect results from Q.hermitian() and Q.antihermitian() are fixed.

Implement Q.positive_infinite Implement Q.negative_infinite Introduce predicate decomposition into primitive predicates Fix Q.hermitian and Q.antihermitian

Implement Q.extended_positive Implement Q.extended_negative Implement Q.extended_nonzero Implement Q.extended_nonpositive Implement Q.extended_nonnegative

Introduce assumptions/facts.py

Apply Q.extended_positive to FinitePredicate Uncomment commented tests in test_query

Fix test_args

sympy-bot · 2021-04-09T15:38:43Z

✅

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
- Q.positive_infinite() and Q.negative_infinite() predicates are introduced. (#21279 by @JSS95)
- Q.extended_positive(), Q.extended_negative(), Q.extended_nonzero(), Q.extended_nonpositive(), and Q.extended_nonnegative() predicates are introduced. (#21279 by @JSS95)
- Q.positive() and Q.negative() now correctly implies the argument being finite. (#21279 by @JSS95)
- Incorrect results from Q.hermitian() and Q.antihermitian() are fixed. (#21279 by @JSS95)

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

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

Fixes #21228

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

* `Q.positive_infinite()` and `Q.negative_infinite()` predicates are introduced.
* `Q.extended_positive()`, `Q.extended_negative()`, `Q.extended_nonzero()`, `Q.extended_nonpositive()`, and `Q.extended_nonnegative()` predicates are introduced.
* `Q.positive()` and `Q.negative()` now correctly implies the argument being finite.
* Incorrect results from `Q.hermitian()` and `Q.antihermitian()` are fixed.

* In order to reduce the complexity of sat solver, some predicates are now decomposed into a combination of primitive predicates.
* Facts are now defined in `assumptions/facts.py`, instead of in `assumptions/ask.py`.

#### Other comments
Benchmark showed no slowdown.

#### Release Notes

<!-- Write the release notes for this release below between the BEGIN and END
statements. The basic format is a bulleted list with the name of the subpackage
and the release note for this PR. For example:

* solvers
  * Added a new solver for logarithmic equations.

* functions
  * Fixed a bug with log of integers.

or if no release note(s) should be included use:

NO ENTRY

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
  * `Q.positive_infinite()` and `Q.negative_infinite()` predicates are introduced.
  * `Q.extended_positive()`, `Q.extended_negative()`, `Q.extended_nonzero()`, `Q.extended_nonpositive()`, and `Q.extended_nonnegative()` predicates are introduced.
  * `Q.positive()` and `Q.negative()` now correctly implies the argument being finite.
  * Incorrect results from `Q.hermitian()` and `Q.antihermitian()` are fixed.
<!-- END RELEASE NOTES -->

Update

The release notes on the wiki have been updated.

sympy-bot · 2021-04-09T15:38:45Z

🟠

Hi, I am the SymPy bot (v161). I've noticed that some of your commits add or delete files. Since this is sometimes done unintentionally, I wanted to alert you about it.

This is an experimental feature of SymPy Bot. If you have any feedback on it, please comment at sympy/sympy-bot#75.

The following commits add new files:

3ee4d02:
- sympy/assumptions/facts.py

If these files were added/deleted on purpose, you can ignore this message.

JSS95 · 2021-04-09T15:56:31Z

@oscarbenjamin

As you suggested in #21220, I implemented primitive predicates and confirmed that it reduced the complexity of sat CNF fact by ~7 items without slowdown. (Checked with benchmark.)

With primitive predicates, I implemented Q.extended_positive() and other predicates which are defined in old assumption system. Since new predicates are decomposed to primitive predicates, they do not complicate the sat solver. (Adding them did not change ask_generated.py, which is a great benefit from introducing predicate decomposition)

I also reorganized the facts and fixed bugs from Q.hermitian(), Q.antihermitian(). This also incidentally fixed Q.positive() and Q.negative(), which had not properly implied that the arguments are finite.

Finally, I moved all the fact-related features from ask.py to facts.py.

In test_query.py, test_bounded() function is marked as XFAIL for now. It is because this test is based on incorrect design of Q.positive() and Q.negative(). I have fixed it, but it will make the diff quite large so I will make another PR for that. Please review what have changed so far. Thanks!

Fix test_known_facts_consistent()

oscarbenjamin · 2021-04-09T23:52:12Z

sympy/assumptions/tests/test_query.py

@@ -595,13 +601,13 @@ def test_I():
    assert ask(Q.real(z)) is True


-
+@XFAIL  # definition for boundedness fixed! will be changed in next commit
 def test_bounded():


Why is this XFAIL?

It is because this test is based on incorrect design of Q.positive() and Q.negative(). I have fixed it, but it will make the diff quite large so I will open another PR for that.

sympy/assumptions/tests/test_query.py

oscarbenjamin · 2021-04-10T08:23:22Z

sympy/assumptions/cnf.py

+    (Literal(Q.even(x), False) & Literal(Q.positive(x), True))
+
+    ``to_NNF`` decomposes the predicate into a combination of primitive
+    predicates if possible.


It doesn't seem like this belongs as part of the to_NNF function.

Do you mean that predicate decomposition should be done by some other function?

It just seems messy to me to do it as part of this function which has a clearly defined purpose: take a logical expression and convert it to NNF (without applying any interpretation to the meaning of the literals).

What about giving keyword argument decompose=True/False to this function?

Perhaps it could take a composite_map argument or something like that.

Fix handlers of FinitePredicate

Add composite_map argument to to_NNF

oscarbenjamin · 2021-04-13T01:28:51Z

Looks good to me

JSS95 added 5 commits April 9, 2021 17:24

feat(assumptions) : reorganize new assumption fact

0e126d6

Implement Q.positive_infinite Implement Q.negative_infinite Introduce predicate decomposition into primitive predicates Fix Q.hermitian and Q.antihermitian

feat(assumptions) : reorganize new assumption fact

48cbea3

Implement Q.extended_positive Implement Q.extended_negative Implement Q.extended_nonzero Implement Q.extended_nonpositive Implement Q.extended_nonnegative

feat(assumptions) : reorganize new assumption fact

3ee4d02

Introduce assumptions/facts.py

feat(assumptions) : reorganize new assumption fact

2b39a21

Apply Q.extended_positive to FinitePredicate Uncomment commented tests in test_query

feat(assumptions) : reorganize new assumption fact

68957f6

Fix test_args

feat(assumptions) : reorganize new assumption fact

1c3b514

Fix test_known_facts_consistent()

JSS95 added the assumptions label Apr 9, 2021

oscarbenjamin reviewed Apr 9, 2021

View reviewed changes

sympy/assumptions/tests/test_query.py Show resolved Hide resolved

oscarbenjamin reviewed Apr 10, 2021

View reviewed changes

JSS95 added 2 commits April 11, 2021 08:26

feat(assumptions) : reorganize new assumption fact

248fb34

Fix handlers of FinitePredicate

feat(assumptions) : reorganize new assumption fact

d9eb785

Add composite_map argument to to_NNF

JSS95 requested a review from oscarbenjamin April 13, 2021 01:21

JSS95 merged commit 7ba571c into sympy:master Apr 13, 2021

JSS95 deleted the pred_posinf_neginf branch April 13, 2021 01:49

JSS95 mentioned this pull request Apr 13, 2021

fix(assumptions): fix test_bounded test #21306

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(assumptions): reorganize facts for new assumptions #21279

feat(assumptions): reorganize facts for new assumptions #21279

JSS95 commented Apr 9, 2021

sympy-bot commented Apr 9, 2021 •

edited

sympy-bot commented Apr 9, 2021 •

edited

JSS95 commented Apr 9, 2021 •

edited

oscarbenjamin Apr 9, 2021

JSS95 Apr 10, 2021 •

edited

oscarbenjamin Apr 10, 2021

JSS95 Apr 10, 2021

oscarbenjamin Apr 10, 2021

JSS95 Apr 11, 2021

oscarbenjamin Apr 11, 2021

JSS95 Apr 12, 2021

oscarbenjamin commented Apr 13, 2021

feat(assumptions): reorganize facts for new assumptions #21279

feat(assumptions): reorganize facts for new assumptions #21279

Conversation

JSS95 commented Apr 9, 2021

References to other Issues or PRs

Brief description of what is fixed or changed

Other comments

Release Notes

sympy-bot commented Apr 9, 2021 • edited

sympy-bot commented Apr 9, 2021 • edited

🟠

JSS95 commented Apr 9, 2021 • edited

oscarbenjamin Apr 9, 2021

Choose a reason for hiding this comment

JSS95 Apr 10, 2021 • edited

Choose a reason for hiding this comment

oscarbenjamin Apr 10, 2021

Choose a reason for hiding this comment

JSS95 Apr 10, 2021

Choose a reason for hiding this comment

oscarbenjamin Apr 10, 2021

Choose a reason for hiding this comment

JSS95 Apr 11, 2021

Choose a reason for hiding this comment

oscarbenjamin Apr 11, 2021

Choose a reason for hiding this comment

JSS95 Apr 12, 2021

Choose a reason for hiding this comment

oscarbenjamin commented Apr 13, 2021

sympy-bot commented Apr 9, 2021 •

edited

sympy-bot commented Apr 9, 2021 •

edited

JSS95 commented Apr 9, 2021 •

edited

JSS95 Apr 10, 2021 •

edited