Repository: sympy/sympy
Pull request: Fix bug in `ask` related to custom AskHandler
<!-- 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. -->
Fixes #18106


#### Brief description of what is fixed or changed

Added `except KeyError: pass` condition in `ask`.

#### Other comments

This commit fixes bug in passing custom AskHandler as assumption of `ask`.

#### 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
    * Improved code in ask function using constructs from cnf module.
    * Fixed bug in ask function: In case of user-defined Predicates it generated KeyError while checking for local_facts. Now falls back to Handlers and satask.

<!-- END RELEASE NOTES -->


Problem statement:
`ask` function needs `except KeyError: ` condition
I am deeply interested in new assumption system, and trying with custom queries. But this led to an error when I meddled with assumptions.

I'll exemplify with `Q.mersenne`, which is provided as an example in sympy's documentation page.

```
>>> from sympy.assumptions import register_handler, ask, Q
>>> from sympy.assumptions.handlers import AskHandler
>>> class MersenneHandler(AskHandler):
...     # Mersenne numbers are in the form 2**n - 1, n integer
...     @staticmethod
...     def Integer(expr, assumptions):
...         from sympy import log
...         return ask(Q.integer(log(expr + 1, 2)))
>>> register_handler('mersenne', MersenneHandler)
>>> ask(Q.mersenne(7))
```

So far, so good.
But when I extended this to Symbol and taught it a silly fact: "If n is mersenne, then n is mersenne.", it raised an error.

```
>>> from sympy.assumptions import register_handler, ask, Q
>>> from sympy.assumptions.handlers import AskHandler
>>> from sympy.logic.boolalg import conjuncts
>>> class MersenneHandler(AskHandler):
...     # Mersenne numbers are in the form 2**n - 1, n integer
...     @staticmethod
...     def Integer(expr, assumptions):
...         from sympy import log
...         if ask(Q.integer(log(expr + 1, 2))):
...             return True
...     @staticmethod
...     def Symbol(expr, assumptions):
...         if expr in conjuncts(assumptions):
...             return True
>>> register_handler('mersenne', MersenneHandler)

>>> from sympy import Symbol
>>> n = Symbol('n', integer=True)
>>> ask(Q.mersenne(n), Q.mersenne(n))
```
This raised:
```
 Traceback (most recent call last)
   1300         # See if there's a straight-forward conclusion we can make for the inference
   1301         if local_facts_.is_Atom:
-> 1302             if key in known_facts_dict[local_facts_]:
   1303                 return True
   1304             if Not(key) in known_facts_dict[local_facts_]:

KeyError: Q.mersenne
```

(Of course, my original code wasn't about simply adding this kind of tautologic fact.)
I tested by adding `except KeyError: pass` condition and it resolved the error.

Maybe this small condition will be harmless to be added in the code?

Hints from issue discussion:
Hi @JSS95, I'm glad that you are interested in New Assumptions.

The whole system is still not mature. This error comes from the fact that the `straight-forward conclusion` portion of code checks on pre-compiled data stored in `ask_generated.py` file. This ask_generated file has to be manually generated from the already defined assumptions and clauses. Adding new facts or handlers doesn't update this pre-compiled list, but I agree this behavior should not happen.

Much of the code in `assumptions` was changed for speeding up the querying mechanism. We still require some cleaning up here and there, and this portion comes under that. AFAIK, this portion needs to be redone (or removed).

I will try to look up into that when I get time.

Commit message: Fixes #18106

Patch to review:
diff --git a/sympy/assumptions/ask.py b/sympy/assumptions/ask.py
index b699fdab8727..d3595be56cba 100644
--- a/sympy/assumptions/ask.py
+++ b/sympy/assumptions/ask.py
@@ -1294,32 +1294,35 @@ def ask(proposition, assumptions=True, context=global_assumptions):
     if local_facts.clauses and satisfiable(enc_cnf) is False:
         raise ValueError("inconsistent assumptions %s" % assumptions)
 
-    if local_facts.clauses:
-        local_facts_ = CNF.CNF_to_cnf(local_facts)
-
-        # See if there's a straight-forward conclusion we can make for the inference
-        if local_facts_.is_Atom:
-            if key in known_facts_dict[local_facts_]:
-                return True
-            if Not(key) in known_facts_dict[local_facts_]:
-                return False
-        elif (isinstance(local_facts_, And) and
-              all(k in known_facts_dict for k in local_facts_.args)):
-            for assum in local_facts_.args:
-                if assum.is_Atom:
-                    if key in known_facts_dict[assum]:
-                        return True
-                    if Not(key) in known_facts_dict[assum]:
-                        return False
-                elif isinstance(assum, Not) and assum.args[0].is_Atom:
-                    if key in known_facts_dict[assum]:
-                        return False
-                    if Not(key) in known_facts_dict[assum]:
-                        return True
-        elif (isinstance(key, Predicate) and
-              isinstance(local_facts_, Not) and local_facts_.args[0].is_Atom):
-            if local_facts_.args[0] in known_facts_dict[key]:
-                return False
+    try:
+        if local_facts.clauses:
+            local_facts_ = CNF.CNF_to_cnf(local_facts)
+
+            # See if there's a straight-forward conclusion we can make for the inference
+            if local_facts_.is_Atom:
+                if key in known_facts_dict[local_facts_]:
+                    return True
+                if Not(key) in known_facts_dict[local_facts_]:
+                    return False
+            elif (isinstance(local_facts_, And) and
+                  all(k in known_facts_dict for k in local_facts_.args)):
+                for assum in local_facts_.args:
+                    if assum.is_Atom:
+                        if key in known_facts_dict[assum]:
+                            return True
+                        if Not(key) in known_facts_dict[assum]:
+                            return False
+                    elif isinstance(assum, Not) and assum.args[0].is_Atom:
+                        if key in known_facts_dict[assum]:
+                            return False
+                        if Not(key) in known_facts_dict[assum]:
+                            return True
+            elif (isinstance(key, Predicate) and
+                  isinstance(local_facts_, Not) and local_facts_.args[0].is_Atom):
+                if local_facts_.args[0] in known_facts_dict[key]:
+                    return False
+    except KeyError:
+        pass
 
     # direct resolution method, no logic
     res = key(expr)._eval_ask(assumptions)


Code review comments:
diff_hunk: @@ -1294,32 +1294,35 @@ def ask(proposition, assumptions=True, context=global_assumptions):
     if local_facts.clauses and satisfiable(enc_cnf) is False:
         raise ValueError("inconsistent assumptions %s" % assumptions)
 
-    if local_facts.clauses:
-        local_facts_ = CNF.CNF_to_cnf(local_facts)
-
-        # See if there's a straight-forward conclusion we can make for the inference
-        if local_facts_.is_Atom:
-            if key in known_facts_dict[local_facts_]:
-                return True
-            if Not(key) in known_facts_dict[local_facts_]:
-                return False
-        elif (isinstance(local_facts_, And) and
-              all(k in known_facts_dict for k in local_facts_.args)):
-            for assum in local_facts_.args:
-                if assum.is_Atom:
-                    if key in known_facts_dict[assum]:
-                        return True
-                    if Not(key) in known_facts_dict[assum]:
-                        return False
-                elif isinstance(assum, Not) and assum.args[0].is_Atom:
-                    if key in known_facts_dict[assum]:
-                        return False
-                    if Not(key) in known_facts_dict[assum]:
-                        return True
-        elif (isinstance(key, Predicate) and
-              isinstance(local_facts_, Not) and local_facts_.args[0].is_Atom):
-            if local_facts_.args[0] in known_facts_dict[key]:
-                return False
+    try:
+        if local_facts.clauses:
+            local_facts_ = CNF.CNF_to_cnf(local_facts)
+
+            # See if there's a straight-forward conclusion we can make for the inference
+            if local_facts_.is_Atom:
+                if key in known_facts_dict[local_facts_]:
+                    return True
+                if Not(key) in known_facts_dict[local_facts_]:
+                    return False
+            elif (isinstance(local_facts_, And) and
+                  all(k in known_facts_dict for k in local_facts_.args)):
+                for assum in local_facts_.args:
+                    if assum.is_Atom:
+                        if key in known_facts_dict[assum]:
+                            return True
+                        if Not(key) in known_facts_dict[assum]:
+                            return False
+                    elif isinstance(assum, Not) and assum.args[0].is_Atom:
+                        if key in known_facts_dict[assum]:
+                            return False
+                        if Not(key) in known_facts_dict[assum]:
+                            return True
+            elif (isinstance(key, Predicate) and
+                  isinstance(local_facts_, Not) and local_facts_.args[0].is_Atom):
+                if local_facts_.args[0] in known_facts_dict[key]:
+                    return False
+    except KeyError:
+        pass
path: sympy/assumptions/ask.py
text: @user1:
This is a very broad try statement. Where does the error get raised? Can it not be caught there?

@author:
The error is raised when `ask` tries to find the custom `Predicate` object in `known_facts_dict`.  

As far as I understand, `known_facts_dict` only contains a few items such as `Q.even`, `Q.positive`, etc. Since it does not contain any user-defined predicates, the whole `if` blocks can raise `KeyError` when these predicates are passed to `assumptions` parameter of `ask`.

Please refer to #18106 for the example.

@user2:
This portion of code, tries to infer the proposition from given assumptions (using already defined known_facts_dict). Any new assumption and it's handler is not updated in the dict that raises `KeyError`.
I (inefficiently) let that stay. Since I already changed the structure of proposition & assumptions into CNF type, I had to convert them back to SymPy types ( `CNF.CNF_to_cnf`).This is all so costly and current system should be able to evaluate faster without this.
This whole portion can be removed and should be changed.

@author:
@user2 Even if this portion will be changed completely in the future, I believe that it would be better to resolve current issue anyway. How do you think of merging this as a temporary fix?


@user2:
I finally did take a look at it. I still want to do a whole revamp of the system but the following diff should do the work.

```diff
diff --git a/sympy/assumptions/ask.py b/sympy/assumptions/ask.py
index b699fdab87..532ad0ec55 100644
--- a/sympy/assumptions/ask.py
+++ b/sympy/assumptions/ask.py
@@ -1295,32 +1295,21 @@ def ask(proposition, assumptions=True, context=global_assumptions):
         raise ValueError("inconsistent assumptions %s" % assumptions)
 
     if local_facts.clauses:
-        local_facts_ = CNF.CNF_to_cnf(local_facts)
-
-        # See if there's a straight-forward conclusion we can make for the inference
-        if local_facts_.is_Atom:
-            if key in known_facts_dict[local_facts_]:
-                return True
-            if Not(key) in known_facts_dict[local_facts_]:
-                return False
-        elif (isinstance(local_facts_, And) and
-              all(k in known_facts_dict for k in local_facts_.args)):
-            for assum in local_facts_.args:
-                if assum.is_Atom:
-                    if key in known_facts_dict[assum]:
-                        return True
-                    if Not(key) in known_facts_dict[assum]:
-                        return False
-                elif isinstance(assum, Not) and assum.args[0].is_Atom:
-                    if key in known_facts_dict[assum]:
-                        return False
-                    if Not(key) in known_facts_dict[assum]:
-                        return True
-        elif (isinstance(key, Predicate) and
-              isinstance(local_facts_, Not) and local_facts_.args[0].is_Atom):
-            if local_facts_.args[0] in known_facts_dict[key]:
+        if len(local_facts.clauses) == 1:
+            cl, = local_facts.clauses
+            f, = cl if len(cl)==1 else [None]
+            if f and f.is_Not and f.arg in known_facts_dict.get(key, []):
                 return False
 
+        for clause in local_facts.clauses:
+            if len(clause) == 1:
+                f, = clause
+                fdict = known_facts_dict.get(f.arg, None) if not f.is_Not else None
+                if fdict and key in fdict:
+                    return True
+                if fdict and Not(key) in known_facts_dict[f.arg]:
+                    return False
+
     # direct resolution method, no logic
```

Please add tests related to the original issue and more if you find.