sympy/sympy — pull request #2508 by asmeurer (2013-10-05 05:14:39+00:00)
Title: Proof of concept for the new assumptions

Here is a proof of concept of how I think the new assumptions should be done,
as per https://code.google.com/p/sympy/issues/detail?id=3929. Take a read of
the commit messages. The basic idea is that instead of writing handlers that
look for expressions like Q.zero(x*y) and return new expressions that it knows
are true like Q.zero(x) and Q.zero(y), the handler system returns a set of
predicate statements, and everything is done using satisfiable(). This not
only makes things cleaner, and gives us a single point of contact to make the
assumptions faster (the dpll algorithm), it also allows computing things that
are impossible to do under the current handler system. For instance

```py
>>> 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))
```

It's impossible to write a handler that says "x is zero or y is zero, but we
don't know which one".

I would like some feedback at this point. This code is completely proof of
concept. The API is terrible (basically nonexistant). What I've got now is
completely unscalable. It already is getting out of hand, and I've only got
four assumptions, real, positive, zero, and nonzero.

I've completely ignored the existing ask() code, because I didn't want to
spend a lot of time at this point trying to understand it (it's quite
complicated), so I basically wrote the prototype from scratch. Even so, it's
quite simple, and I think once you grok how the satisfiable bit works, it is
easy to understand the rest.

So my biggest questions now are, do people like this idea? Do you foresee any
major issues with it? Most importantly, what would be a good way to organize
the new-style "handlers" (relevant fact extraction) so that it is scalable,
extensible, and readable?