Hi all. I got bored, so I spent this evening hacking together a proof of concept for the new assumptions system, based on my ideas from https://code.google.com/p/sympy/issues/detail?id=3929. The code is at https://github.com/sympy/sympy/pull/2508.
Basically, I realised this summer when I was hacking on the assumptions that the way the handlers currently work is fundamentally broken. For instance, if you do something like ask(Q.zero(x*y), Q.zero(x)), the way the handlers currently work is they see the Q.zero(x*y), and they know that this means Q.zero(x) or Q.zero(y), so they basically say "if any(ask(Q.zero(i)) for i in (x*y).args): return True". This works fine, except if you then do something a little more complicated, like ask(Q.zero(x*y), Q.zero(x) | Q.zero(y)), it falls apart, because neither ask(Q.zero(x)) nor ask(Q.zero(y) is true. What *is* true is that at least one of them is true. But since the logic in the handlers is done as a Python "or", not a SymPy "Or", there's no way to represent this. What I also learned this summer is that SAT solvers are awesome, and if your problem can be solved by one, you should do as little work as possible and basically let the SAT solver do the heavy lifting. Well, SymPy has a SAT solver, accessible from the satisfiable() function, so I realized that this problem (ask(Q.zero(x*y), Q.zero(x) | Q.zero(y))) could be solved using one, by simply knowing the fact Equivalent(Q.zero(x*y), Q.zero(x) | Q.zero(y)). At https://github.com/sympy/sympy/pull/2508, I've implemented this idea. The most annoying thing I've found when working with the new assumptions is that the code is very complicated, especially the code in ask.py, so instead of spending all night trying to understand it, I opted for the funner way that actually involved writing new code, which was to write a proof of concept from scratch. This code doesn't use anything from ask.py (except for the Q object of course). The result is that only those assumptions that I have manually entered will work, which are basically the obvious relationships between real, positive, zero, and nonzero, and the one non-trivial fact about a multiplication being zero if and only if one of the terms is zero. The good news is that the code for newask() is incredibly simple to understand (I think). To get you excited about what's possible, here are some simple things that work with newask() that don't work with ask(): >>> from sympy.assumptions.newask import newask >>> newask(Q.zero(x) | Q.zero(y), Q.zero(x*y)) True >>> newask(Implies(Q.zero(x), Q.zero(x*y))) True >>> newask(Q.zero(x) | Q.zero(y), Q.nonzero(x*y)) False >>> ask(Q.zero(x) | Q.zero(y), Q.zero(x*y)) >>> ask(Implies(Q.zero(x), Q.zero(x*y))) >>> ask(Q.zero(x) | Q.zero(y), Q.nonzero(x*y)) >>> newask(Q.zero(x*y), Q.zero(x) | Q.zero(y)) True >>> ask(Q.zero(x*y), Q.zero(x) | Q.zero(y)) >>> newask(Q.zero(x*y*z), Q.zero(x) | Q.zero(y)) True >>> ask(Q.zero(x*y*y), Q.zero(x) | Q.zero(y)) >>> and more importantly, as noted above, it is very difficult to impossible to make these work with ask(), because it doesn't know how to deal with implications with non-atomic premises, basically. Also note how I am able to ask what is basically the same thing in three different ways, and get the right answer in every case. Even if we could hack together something to make ask(Q.zero(x*y), Q.zero(x) | Q.zero(y)) work, ask(Implies(Q.zero(x), Q.zero(x*y)) or ask(Q.zero(x) | Q.zero(y), Q.zero(x*y)) might not (note that this second one wouldn't, because it is the reverse implication; but in newask, it's as easy as using Equivalent instead of Implies). So I'd like some feedback. It's getting late now, so hopefully I haven't written anything stupid as my brain is starting to shut down. I'd particularly like some feedback on how to structure the API for this, since what I have now is completely hacked together and won't scale at all. Please read the commit messages on my pull request if you want more information. Aaron Meurer -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to sympy+unsubscr...@googlegroups.com. To post to this group, send email to sympy@googlegroups.com. Visit this group at http://groups.google.com/group/sympy. For more options, visit https://groups.google.com/groups/opt_out.
