Yeah!!! On Fri, Oct 4, 2013 at 10:35 PM, Aaron Meurer <asmeu...@gmail.com> wrote: > 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.
-- Brian E. Granger Cal Poly State University, San Luis Obispo bgran...@calpoly.edu and elliso...@gmail.com -- 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.
