Proof of concept for the new assumptions #2508

asmeurer · 2013-10-05T05:14:39Z

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

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

Update: newask has been changed to satask

This is a basic prototype of a new ask, currently accessible as sympy.assumptions.newask.newask(), that uses satisfiable() entirely to determine the truth or falsehood of the given proposition under the given assumptions. See https://code.google.com/p/sympy/issues/detail?id=3929 for more details on the idea. As a first prototype, this is still in a very proof-of-concept stage. In particular: - I don't reuse any of the existing ask logic or machinery. As such, almost everything that works currently with ask() won't work with newask(). - I have so far only implemented the fact positive implies real. Unless a given proposition can be deduced from this fact, or is a tautology or a contradiction, newask will return None. - I have in no way attempted to make a nice API for this. In fact, the current API is rather terrible: it's just a chain of if statements. But the basic idea is there, namely, that ask() should extract all relevant facts based on the predicates present in the proposition and the assumptions, and then use satisfiable() to determine satisfiable(And(proposition, assumptions, relevant_facts)) and satisfiable(And(~proposition, assumptions, relevant_facts)). If one is True and the other False, then we know that proposition is True (or False); if both are True, we return None, and if both are False, we conclude that the assumptions and the relevant_facts give a contradiction. At this point, I would like some input on how to structure this API so that it becomes scalable, extensible, and readable.

This is required because some relevant facts may in turn generate new relevant facts, which didn't appear before. This happens as soon as you start to add non-trivial facts, like Equivalent(Q.zero(x*y), Q.zero(x) | Q.zero(y)), because they add new predicates to the system.

We always add relevant facts because they might be needed. For instance, if we only added the fact Equivalent(Q.zero(x*y), ~Q.nonzero(x*y)) when both predicates appeared in the system, we would never be able to compute newask(Q.zero(x) | Q.zero(y), Q.nonzero(x*y)), because it requires going from two steps, first, adding the fact Equivalent(Q.nonzero(x*y), ~Q.zero(x*y)), and second, adding the fact Equivalent(Q.zero(x*y), Q.zero(x) | Q.zero(y)). This second fact can only be added after the first is added, because only at that point do we have Q.zero(x*y). Without this, we would have to add many redundant facts (like Equivalent(Q.nonzero(x*y), ~Q.zero(x) & ~Q.zero(y))). On the other hand, we now avoid adding completely redundant implications. The Q.zero fact, aside from the obvious implications on the already existing Q.positive and Q.real, and the new Q.nonzero, includes one nontrivial fact, namely Q.zero(Mul) is equivalent to Or([Q.zero(arg) for arg in Mul.args]). This fact, while easy to add, allows for very powerful new assumptions, all of which don't work with ask(), but more importantly, are either very difficult or impossible to add to ask() because the way the current handler system works, it is not so easy to add handler to make things like ask(Or(x, y)) give True when neither ask(x) nor ask(y) would give True (as is the case for ask(Q.zero(x) | Q.zero(y), Q.zero(x*y))). For instance: >>> 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)) >>> Notice how the use of satisfiable() lets us ask essentially equivalent things in different ways, and still get the right answer, even though we only told the system about the fact in one way.

… ask() And add one test that I forgot (that does work with ask(), since it's so simple).

mrocklin · 2013-10-05T14:18:12Z

sympy/assumptions/newask.py

+    while relevant_facts != old_relevant_facts:
+        old_relevant_facts, relevant_facts = (relevant_facts,
+            get_relevant_facts(proposition, assumptions & old_relevant_facts,
+                context))


So newask works by forward chaining? How efficient is this as the number of active propositions increases? What is performance like? I can imagine the set of facts becoming large as we extend this system to all of Q.

Maybe we need a dependency graph between predicates. Does even-ness help you to predict zero-ness? Sparsity in this graph would help performance.

We could also group predicates by valid classes on which they relate. Can MatrixExprs be positive? Can Bools be even?

mrocklin · 2013-10-05T14:29:09Z

What is performance like? Have you benchmarked? How does SymPy's SAT solver compare to other C-based SAT solvers. Is this something we could include as an optional dependency like matplotlib?

mrocklin · 2013-10-05T14:31:20Z

The main issue I see is that this method forward chains all known facts at runtime. As you've demonstrated this is very powerful but I'm concerned that it will become very slow as we add all of the predicates.

I wonder if there is a way to restrict the set of active predicates intelligently (or by hand). I also wonder if this is important or not.

mrocklin · 2013-10-05T14:31:54Z

In general though I'm excited. The code is much more understandable and capable of a number of things which felt broken in old-new assumptions.

asmeurer · 2013-10-05T17:29:38Z

Thanks for your comments Matthew.

Yes, you are right, this is forward chaining. I'm glad you pointed that out, because I think with this realization we can look into how other systems manage their data structures for forward chaining. The important thing to note here is that we are not forward chaining on assumptions. This is basically what the old assumptions do (and I guess basically the new ones as well). So for instance, if we know that Q.positive(x) >> Q.real(x) and we assume Q.positive(x), we would get by forward chaining Q.real(x). This is not what this is doing. What it is doing, is forward chaining on facts, which you can think of as meta-assumptions. We know that if we have the key Q.positive(x) then we (might) care about the fact Q.positive >> Q.real(x).

Regarding the data-structure, yes, it absolutely needs to be represented in data. I stated that the current API is terrible. Not only is it non-scalable and non-extensible, we may be missing out on some things that we can only do if we are represented as data (similar to how the current handlers misses out on things by not representing facts as data). For instance, if we represent our facts as data correctly, it should be possible to generate the graph you mentioned automatically. This means we need to be careful about our data structures, though. If we represent "Q.zero(Mul(*args)) iff any(Q.zero(arg))" as a lambda (for instance), then the fact that we have a graph relationship between Q.zero and Q.zero will be impossible to see, unless we have an explicit example.

I think the known_facts_dict will be the easiest to generalize here, because those are very special facts that are free of the expression in the predicate. Unlike "Q.zero(Mul(*args)) iff any(Q.zero(arg))", which cannot be written down without explicitly mentioning exactly what is zero, Q.zero >> Q.real doesn't require such knowledge. The current assumptions work by removing all arguments and checking satisfiability on these free assumptions; newask works by taking such facts and producing the relevant instances for the expression. I like the newask way better because it avoids questionable logic like https://github.com/sympy/sympy/blob/master/sympy/assumptions/ask.py#L76 (that function works by removing None clauses from And and so on, but that doesn't work for binary operations like Implies: Implies(Q.real(x)) is meaningless).

Regarding performance, I didn't look at it at all, for a few reasons:

For the small bit that I've implemented, and the small examples I tried the performance was fine.
I'm assuming we won't even be able to tell what the performance issues really are until we implement a lot more.
I really want to avoid premature optimization. You can see I initially had some nested if blocks to try to only put in the relevant facts that really were relevant (e.g., only add Q.zero(x) >> Q.real(x) if both Q.zero(x) and Q.real(x) appeared, but I removed this because it didn't take into account that later parts of the function could introduce new facts, like Equivalent(Q.zero(x*y), Q.zero(x) | Q.zero(y)).

Also, from what I've heard, with good SAT solvers, you should just dump everything you know into them, and they will do a pretty good job of ignoring the irrelevant stuff. We'll have to wait until we have much more relevant fact extraction to see if this really is true, but if it is, then trying to avoid inserting irrelevant facts may actually waste time, and worse, may prevent some answer from being deduced that otherwise would be.

I also have no idea what really would be the performance bottlenecks. I basically put one piece of heavy machinery, satisfiable, so ideally we can improve the performance of this exactly by improving the performance of it. I like this, because the SAT solver hasn't really seen any love since @haz's GSoC project, but I know that there are all sorts of things that can be done there.

You may be right though that the actual fact extraction will be the bottleneck. I can't really speak to the performance of this yet because I know that the data structures used for this will be completely different than my if chain when it's done right.

How does SymPy's SAT solver compare to other C-based SAT solvers. Is this something we could include as an optional dependency like matplotlib?

It's much slower. Compare python sympy/logic/benchmarks/run-solvers.py to python -m test_pycosat sympy/logic/benchmarks/input/*. Note that run-solvers.py only tries to get one solution, whereas test_pycosat actually finds all solutions (so really you care about the time to the first .). So once we finish this, we should definitely look into creating an optional backend for pycosat.

asmeurer · 2013-10-05T17:30:25Z

By the way, it would be more like the optional dependency of gmpy, in that it wouldn't really add any new behavior, but it would automatically make parts of SymPy much faster if installed.

asmeurer · 2013-10-05T17:43:28Z

Another thing that requires some thought is how to properly handle handlers that aren't really logical facts, but are rather computations. A simple example is https://github.com/sympy/sympy/blob/master/sympy/assumptions/handlers/order.py#L121. A more complicated example might be using solve to deduce some fact about a set of equations (for instance, we could use diop_solve to answer questions like ask(Q.zero(x - 3), Q.zero(x**2 + y**2 - 10))).

Previously it wasn't really finding the fixed point. Now it does the right thing.

Also add a test that uses several levels of forward chaining.

asmeurer · 2013-10-05T18:17:30Z

Does even-ness help you to predict zero-ness?

The answer to this is yes. Knowing about even-ness doesn't mean that we know something is even. It could also mean that we know something is not even, in which case we know that it is not zero. Two concepts in the graph should be connected if there is an implication in either direction, and in fact it's pointless to make the graph directed.

Remember that Q.even(x) appearing in an expression could really mean that ~Q.even(x) appears, and it could appear in a hidden way, like Implies(Q.even(x), Q.real(x) or ~And(Q.even(x), Q.positive(x)). We could probably try to find it, but it's pointless. That's what the SAT solver is good at; let's avoid doing things that the SAT solver can do at all costs, unless it is really killing our performance (and even then, let's try to make the SAT solver faster first).

asmeurer · 2013-10-05T18:22:37Z

sympy/assumptions/newask.py

+    # infinite loop in the future.
+    relevant_facts = True
+    old_relevant_facts = False
+    while relevant_facts != old_relevant_facts:


I suspect we may run into problems here at some point. The only reason we hit a fixed point is that And removes (exact) duplicate arguments automatically. But what happens when we start adding an infinite number of duplicate arguments none of which look exactly like each other? Or even if not infinite, many? We already are starting to do this: the relevant_facts will always contain both Equivalent(Q.zero(x), ~Q.nonzero(x)) and Equivalent(Q.nonzero(x), ~Q.zero(x)) if it contains one. Maybe we don't need to care, if the SAT solver really is good at ignoring redundancies, but I highly suspect that we will.

I think the more rigorous way (if we run into this problem) will be to use satisfiable to determine if the new part really does contain new logical information.

The only reason we hit a fixed point is that And removes (exact) duplicate arguments automatically

Do we want And to perform logic here? If we're doing a lot of this each round it may make sense to drop out of SymPy within a lot of Assumptions. I'm imagining a polys type infrastructure here.

I think the only reason And does this is that it uses a frozenset internally, so by design it cannot hold duplicate arguments.

I don't know what the code of using full expressions is here. I do know that in the SAT solver, everything is converted to a much more efficient set of integers representation, so you don't need to worry about that.

This gives the simplest example yet of something that doesn't work with ask() (simplest in the sense that there are no logical operators involved) >>> from sympy.assumptions.newask import * >>> ask(Q.zero(x), Q.zero(x**2)) >>> newask(Q.zero(x), Q.zero(x**2)) True This one probably could be made to work with the ask() handlers system, but it would require digging through the expressions to find the x**2, and it would be messy.

asmeurer · 2013-10-05T19:43:32Z

I just started playing with using known_facts_cnf and, yeah, things slow down a lot. So I guess the SAT solver isn't so hot at redundancies.

Also, apparently Q.nonzero means Q.real and ~Q.zero, not just ~Q.zero, so some of what I had was wrong (leading to "inconsistent assumptions").

mrocklin · 2013-10-05T19:53:16Z

Regarding the data-structure, yes, it absolutely needs to be represented in data

I can imagine a few major relations that you'd want to be able to describe including

What we have now in new assumptions, Implies/Equivalent(Predicate1, Predicate2)
A sort of any mapping down to arguments. E.g. Q.zero(Mul(args)) iff any(map(Q.zero, args))
A similar all mapping Q.positive(Mul(args)) if all(map(Q.positive, args)), note the lack of iff

But we're sure to want more and we're almost certainly not going to get all of them at design time (presumably this was a problem with oldnew assumptions). Which means that we need some sort of interface or infrastructure to describe these later on. Or at worst we need the part of the code in which all of these systems are implemented to be easy to add to in the vein of Mul.flatten.

mrocklin · 2013-10-05T19:55:59Z

I really want to avoid premature optimization.

I respect this, but I also think that some long-range thinking about what might be or not be feasible is, I think, worth thinking about now to make sure that this is a path worth pursuing. Such thoughts might also push us in the right directions.

mrocklin · 2013-10-05T19:58:22Z

Also, from what I've heard, with good SAT solvers, you should just dump everything you know into them, and they will do a pretty good job of ignoring the irrelevant stuff. We'll have to wait until we have much more relevant fact extraction to see if this really is true, but if it is, then trying to avoid inserting irrelevant facts may actually waste time, and worse, may prevent some answer from being deduced that otherwise would be.

I'm not worried about the SAT solver's performance. I'm worried about how much time it will take Python/SympPy to construct all of the facts. I'm worried about the linear time part of this algorithm, not the NP hard part :)

If we use more complex fact finders (e.g. things that depend on solve as you mention) then we'll really want to be intelligent about which paths we pursue.

mrocklin · 2013-10-05T20:00:14Z

Also, apparently Q.nonzero means Q.real and ~Q.zero, not just ~Q.zero, so some of what I had was wrong (leading to "inconsistent assumptions").

But it's kind of awesome that it told you.

asmeurer · 2013-10-05T20:28:29Z

I guess I'm worried about the SAT solver performance because to me, that's the harder one to improve.

But it's kind of awesome that it told you.

Yes, though it didn't actually tell me why. I only knew that was what was wrong because I had already noticed it.

A sort of any mapping down to arguments. E.g. Q.zero(Mul(args)) iff any(map(Q.zero, args))
A similar all mapping Q.positive(Mul(args)) if all(map(Q.positive, args)), note the lack of iff

To me, these are the same thing (one uses Equivalent and one uses Implies, but that's it).

Again, remember that we need to do forward chaining against both directions of implications, because we don't know if an assumption will end up being true or false. In terms of classical logic, we need to think about both modus ponens and modus tollens.

Update this branch with master, fix merge conflicts and replace deprecated is_bounded with is_finite

debugger22 · 2015-04-02T21:06:30Z

sympy/assumptions/ask.py

@@ -129,6 +131,9 @@ def ask(proposition, assumptions=True, context=global_assumptions):
    else:
        key, expr = Q.is_true, sympify(proposition)

+    if isinstance(proposition, (bool, BooleanAtom)):
+        return sympify(proposition)


Why BooleanTrue instead of bool?

This makes the output less consistent. In both branches, master and this one, ask returns bool.

This change is making ask(True) is True False.

I don't remember why I made this change. I agree that ask should return a bool, since it doesn't make sense in a boolean context (

sympy/sympy/logic/boolalg.py

Lines 90 to 93 in 98459c5

# The rule of thumb is:

# "If the boolean in question can be replaced by an arbitrary symbolic

# Boolean, like Or(x, y) or x > 1, use S.true. Otherwise, use True"

). The commit this comes from doesn't specify why it was done. I'm assuming I put it in there because something was not working without it. I would try to remove it and if the tests pass then it can be removed.

Ok. You changed two tests to respect this change. https://github.com/sympy/sympy/pull/2508/files#diff-abc5430bcb3f79fa33a7df36470717fcR1950

Fix formatting and typos

ask(bool) now returns bool instead of BooleanAtom

debugger22 · 2015-05-29T00:10:21Z

sympy/assumptions/sathandlers.py

+    A singly applied predicate is a free predicate applied everywhere to a
+    single expression. For instance, Q.zero(x) and Or(Q.positive(x*y),
+    Q.negative(x*y)) are singly applied, but Or(Q.positive(x), Q.negative(y))
+    and Or(Q.positive, Q.negative(y)) are not.


Is this a typo? Or(Q.positive, Q.negative(y))

I don't think so. I'm pointing out that this predicate is not singly applied because Q.positive is not applied and Q.negative(y) is.

Oh! Got that.

Updated with master

tjl · 2015-06-06T06:00:28Z

sympy/assumptions/tests/test_satask.py

+    Everything in this test doesn't work with ask, and most things would be
+    very difficult or impossible to make work under the current handlers
+    model.
+    """


I'm not entirely clear about this docstring. I'm assuming that it's saying that everything in the test doesn't work with the old assumptions, but it does with the new assumptions? If so, I think it could be clearer. Especially since the definition of the word "current" once this is merged is ambiguous.

Ah, this must have been written before I integrated the stuff with ask itself.

I modified it.

That looks good. I'm okay with the merge now.

On 6 Jun 2015, at 19:34, Aaron Meurer wrote:

assert satask(~Q.positive(x)) is False

raises(ValueError, lambda: satask(Q.real(x),
~Q.positive(x)))
+

assert satask(Q.zero(x), Q.nonzero(x)) is False

assert satask(Q.positive(x), Q.zero(x)) is False

assert satask(Q.real(x), Q.zero(x)) is True

assert satask(Q.zero(x), Q.zero(x*y)) is None

assert satask(Q.zero(x*y), Q.zero(x))

+def test_zero():

"""

Everything in this test doesn't work with ask, and most things
would be

very difficult or impossible to make work under the current
handlers

model.

"""

I modified it.

Reply to this email directly or view it on GitHub:
https://github.com/sympy/sympy/pull/2508/files#r31872394

tjl · 2015-06-06T06:02:17Z

Aside from the few comments above, I'm okay with this.

debugger22 · 2015-06-08T04:41:45Z

I'll merge this in some time if no objections are raised.

Proof of concept for the new assumptions

Arpan612 · 2020-04-17T13:26:08Z

@asmeurer In SymPy's SAT solver have we included any optional dependency like suggested here? Also, if you have some suggestion of any dependency which we may use, please tell me, I will research on it.

What is performance like? Have you benchmarked? How does SymPy's SAT solver compare to other C-based SAT solvers. Is this something we could include as an optional dependency like matplotlib?

asmeurer · 2020-04-17T19:37:28Z

Yes, I believe we currently use pycosat as an optional dependency.

Arpan612 · 2020-04-18T04:14:49Z

@asmeurer Great. Could you tell me the PRs where it is implemented?

Arpan612 · 2020-04-19T18:42:32Z

@asmeurer Also, in this PR thread could you point out if any issue is not solved which is of immediate attention for us?

asmeurer · 2020-04-21T19:27:36Z

The biggest question here is how far we can get this to scale without changing the way the algorithm works. Last year's GSoC project helped a lot, but I still don't know if it will scale to the full set of assumptions used by SymPy.

I think the general idea of writing down facts as logical expressions is a good one, although I think we should use a better syntax for them (#2508 (comment)). It's also unclear to me how to represent certain facts without having a combinatorial explosion of clauses (like certain facts that use XOR). We also will eventually want some way to extend the facts externally, so that not everything has to go in sathandlers.py, though that should probably be left until we know it can scale.

haz · 2020-04-21T19:33:58Z

Hi all, I read maybe 0.1% of all the conversations coming through my inbox for sympy, but this one caught my eye.

It's also unclear to me how to represent certain facts without having a

combinatorial explosion of clauses (like certain facts that use XOR). @aaron: you can manage the encoding to CNF quite readily - https://en.wikipedia.org/wiki/Tseytin_transformation Hope you are all doing well! Cheers, Christian

…

On Tue, Apr 21, 2020 at 3:27 PM Aaron Meurer ***@***.***> wrote: The biggest question here is how far we can get this to scale without changing the way the algorithm works. Last year's GSoC project helped a lot, but I still don't know if it will scale to the full set of assumptions used by SymPy. I think the general idea of writing down facts as logical expressions is a good one, although I think we should use a better syntax for them (#2508 (comment) <#2508 (comment)>). It's also unclear to me how to represent certain facts without having a combinatorial explosion of clauses (like certain facts that use XOR). We also will eventually want some way to extend the facts externally, so that not everything has to go in sathandlers.py, though that should probably be left until we know it can scale. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#2508 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABW56ZJJ6QZ7CAEHRLP4BTRNXXTRANCNFSM4AIRMJTQ> .

asmeurer · 2020-04-21T19:46:37Z

It's good to see that you still follow SymPy, if only 0.1%.

Yes, we've had an open issue for Tseitin for a while. It just hasn't been implemented. I'm also not sure if the extra variables from it would end up causing their own problems. Maybe the solution is to only use it for instances where it really saves a lot, like XOR, and not bother for simple things like small expressions that can just be distributed into CNF.

haz · 2020-04-22T14:18:01Z

Problems in solving or in actual handling? If you aren't using model counting, but just SAT checks (with solution extraction) you should be able to safely project away those auxiliary variables. Though you are right in terms of the problems with solving -- the extra variables may make it more difficult to solve. Crude estimates of the expanded formula should be easy enough to compute, and perhaps you could use that to only partially Tseiten-ize...also an option to expand until you hit a limit and then Tseiten from then on. But exploration here, and exploration on improving the CNF encoding (in the other thread related to this) *all* should be informed by proper data: i.e., what actually needs improving. Solving time? Encoding time? Something else? Need some decent profiling before diving in I reckon. Cheers!

…

On Tue, Apr 21, 2020 at 3:46 PM Aaron Meurer ***@***.***> wrote: It's good to see that you still follow SymPy, if only 0.1%. Yes, we've had an open issue for Tseitin for a while. It just hasn't been implemented. I'm also not sure if the extra variables from it would end up causing their own problems. Maybe the solution is to only use it for instances where it really saves a lot, like XOR, and not bother for simple things like small expressions that can just be distributed into CNF. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#2508 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABW564TIDED43ZFFCY6Z53RNXZ23ANCNFSM4AIRMJTQ> .

asmeurer added 6 commits October 4, 2013 22:13

Merge branch 'satisfiable_expr' into newassump

d3d93b0

Rearrange tests so that test_zero is only things that don't work with…

83dc028

… ask() And add one test that I forgot (that does work with ask(), since it's so simple).

Add another test, which is the actual one that started this whole thing

eb0c9c8

mrocklin reviewed Oct 5, 2013
View reviewed changes

asmeurer added 3 commits October 5, 2013 12:03

Extract the get_relevant_facts fixed point finder, fix it to be correct

7d3b1cc

Previously it wasn't really finding the fixed point. Now it does the right thing.

Simplify some logic

38556d0

Add fact x and y positive implies x + y nonzero to newask

5fadd26

Also add a test that uses several levels of forward chaining.

asmeurer reviewed Oct 5, 2013
View reviewed changes

asmeurer added 2 commits October 5, 2013 13:12

Merge branch 'rcall-Basic' into newassump

e8c98f1

sift keys by predicate

a9ca1e3

Merge pull request #68 from debugger22/aaron-assumptions

f13ed6d

Update this branch with master, fix merge conflicts and replace deprecated is_bounded with is_finite

debugger22 reviewed Apr 2, 2015
View reviewed changes

debugger22 and others added 4 commits April 3, 2015 03:59

Fix formatting and typos

53fc46b

Merge pull request #70 from debugger22/aaron-assumptions

27c9d26

Fix formatting and typos

ask(bool) now returns bool instead of BooleanAtom

52c143e

Merge pull request #71 from debugger22/aaron-assumptions

1896e70

ask(bool) now returns bool instead of BooleanAtom

debugger22 reviewed May 29, 2015
View reviewed changes

debugger22 and others added 2 commits June 5, 2015 22:05

Fix merge conflicts

b5abe2d

Merge pull request #72 from debugger22/aaron-assumptions

838b3bb

Updated with master

tjl reviewed Jun 6, 2015
View reviewed changes

Clarify a docstring

9e4ef60

debugger22 added a commit that referenced this pull request Jun 8, 2015

Merge pull request #2508 from asmeurer/newassump

a58a03b

Proof of concept for the new assumptions

debugger22 merged commit a58a03b into sympy:master Jun 8, 2015

This was referenced Jul 22, 2015

Added performance regression test to refine sympy/sympy_benchmarks#12

Merged

Since new assumptions refine is horribly slow (2000x slower) #9714

Open

rwst mentioned this pull request Jul 23, 2015

sync elementary assumptions on expressions with Sage pynac/pynac#81

Closed

asmeurer mentioned this pull request Nov 1, 2016

[WIP] Improve satask() performance #11789

Merged

4 tasks

asmeurer mentioned this pull request Mar 2, 2019

Improvements to logic module #7175

Open

9 tasks

asmeurer mentioned this pull request Apr 16, 2019

Sympy hangs on fairly simple expression #7129

Open

	# The rule of thumb is:

	# "If the boolean in question can be replaced by an arbitrary symbolic
	# Boolean, like Or(x, y) or x > 1, use S.true. Otherwise, use True"

Proof of concept for the new assumptions #2508

Proof of concept for the new assumptions #2508

Conversation

asmeurer commented Oct 5, 2013

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mrocklin commented Oct 5, 2013

mrocklin commented Oct 5, 2013

mrocklin commented Oct 5, 2013

asmeurer commented Oct 5, 2013

asmeurer commented Oct 5, 2013

asmeurer commented Oct 5, 2013

asmeurer commented Oct 5, 2013

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

asmeurer commented Oct 5, 2013

mrocklin commented Oct 5, 2013

mrocklin commented Oct 5, 2013

mrocklin commented Oct 5, 2013

mrocklin commented Oct 5, 2013

asmeurer commented Oct 5, 2013

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

debugger22 May 29, 2015 via email

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tjl commented Jun 6, 2015

debugger22 commented Jun 8, 2015

Arpan612 commented Apr 17, 2020

asmeurer commented Apr 17, 2020

Arpan612 commented Apr 18, 2020

Arpan612 commented Apr 19, 2020

asmeurer commented Apr 21, 2020

haz commented Apr 21, 2020 via email

asmeurer commented Apr 21, 2020

haz commented Apr 22, 2020 via email