Re: SAT Solver and Improvements to the Assumptions System

> > So your merge commit 5ca928 is a merge between dcbc2d (the below commit) > and e2d81ab, which is an old commit of mine. I'm not sure how that > happened. Did you try doing any rebases on your history that contained > merges maybe? > I don't believe so, but that span of 3 days is quite mudd

Re: SAT Solver and Improvements to the Assumptions System

> > This is indeed very strange. According to issue 2046 (and my own bisecting > as well) it comes from this commit: > commit dcbc2da31324e98c9cb3a4bf17c50f029774ae06 > Author: Sebastian Krämer > Date: Wed May 5 22:48:18 2010 +0200 > >Implement fast atomic substitution. > >* The main

Re: SAT Solver and Improvements to the Assumptions System

> > It seems that this has finally been pushed in (including, unfortunately, > a large mess of meaningless merges). Large mess? There shouldn't be so many since it was cleaned up with the help of Vinzent and Aaron. I think there are still a few > things that should be addressed before the next

Re: SAT Solver and Improvements to the Assumptions System

Vinzent, et al, does the branch seem alright to go in at this point? I'm sitting on this merge request before bringing up the more debatable points surrounding the removal of the old assumption system. Thanks. Cheers Christian On Aug 15, 11:39 pm, Christian Muise wrote: > >

Re: SAT Solver and Improvements to the Assumptions System

> > > Escaping newlines is not necessary if you got parentheses, > > Ahh, ok. I'll fix in the most recent commit that adds them. > This is in now. soc-final-fixed has all fixes in it now. Cheers Christian -- You received this message because you are subscribed to the Google Groups "symp

Re: SAT Solver and Improvements to the Assumptions System

On Sunday, August 15, 2010, Vinzent Steinberg wrote: > Thanks, this is much better. Doctests would be great, but I think the > solver is rarely ever exposed to the user, so this is probably low > priority. Aye, the only interface they use is the 'satisfiable' function, which already has doctest

Re: SAT Solver and Improvements to the Assumptions System

ug 13, 2010 at 1:33 PM, Vinzent Steinberg < vinzent.steinb...@googlemail.com> wrote: > I posted some comments on github, I'll yet have to run the tests however. > > Vinzent > > 2010/8/11 Christian Muise : > > Ok, so I went through the growing pains of figuring all thi

Re: SAT Solver and Improvements to the Assumptions System

> > Cool. So the next step is to make this work: >> >> x = Symbol('x') >> assert ask(x, Q.integer) is None >> local_context = AssumptionsContext() >> local_context.add(Assume(x, Q.integer)) >> with local_context: >> assert ask(x, Q.integer) is True >> > > It doesn't really need any setup / t

Re: SAT Solver and Improvements to the Assumptions System

> > Cool. So the next step is to make this work: > > x = Symbol('x') > assert ask(x, Q.integer) is None > local_context = AssumptionsContext() > local_context.add(Assume(x, Q.integer)) > with local_context: > assert ask(x, Q.integer) is True > It doesn't really need any setup / tear-down...

Re: SAT Solver and Improvements to the Assumptions System

Ok, so I went through the growing pains of figuring all this git stuff out, at we should be good to go with this branch: - http://github.com/haz/sympy/tree/soc-final-fixed The commits are linear, all tests should be running clean (regardless of c

Re: SAT Solver and Improvements to the Assumptions System

> > I really don't think that static compilation to Python > code is a good idea. It prevents any extension to the system and makes > it very hard to maintain. It would be much more useful to compute > known_facts_dict at import time and to have the possibility to recompute > it at runtime if fact

SAT Solver and Improvements to the Assumptions System

Hello, I'd like to formally request that this branch be merged into the SymPy trunk: - http://github.com/haz/sympy/tree/soc-final It contains a new SAT solver, and improvements to the assumptions system (specifically in the ask function). Info on the work done in this branch has been periodica

Re: disconnect-assumptions branch comments

Sounds good to me. It should be noted that speeding up the reasoner is almost entirely disjoint from the assumption interface rewrite -- finished or not, the sat solver improvements don't depend on how you create your assumptions...just what they are. Cheers On Friday, June 18, 2010, Ondrej Cer

Re: disconnect-assumptions branch comments

I think the idea was the compatibility will indeed be broken -- assumptions are to be stripped from object constructors altogether. At least this is the impression I was under after speaking with Ondrej. On Thu, Jun 17, 2010 at 4:43 PM, Vinzent Steinberg < vinzent.steinb...@googlemail.com> wrote:

Re: disconnect-assumptions branch comments

n Thu, Jun 17, 2010 at 2:17 PM, Christian Muise wrote: > I'll see what I can do, but fixing those tests will likely cause more to > fail. I've attached the 7 errors that occur at d25877c: > - Two are because Symbols is trying to use assumptions0, something that was > inherite

Re: disconnect-assumptions branch comments

rvals with symbols -- these no longer have a is_real assumption associated with them, and thus throw a ValueError in the Interval constructor. - Final one I'm still figuring out. Cheers On Thu, Jun 17, 2010 at 12:11 PM, Ondrej Certik wrote: > On Thu, Jun 17, 2010 at 8:19 AM, Christ

Re: disconnect-assumptions branch comments

So the main problems start to crop up when you start stripping out assumptions from the constructor of basic sympy objects. This breaks compatibility, and very quickly the number of errors goes up. You can view the natural progression of what you suggest on this branch: - http://github.com/haz/sy

Re: Fix for the polynomials docstring test.

Ahh, well that explains things. Please ignore then ;). Cheers On Tue, Apr 6, 2010 at 4:36 PM, Vinzent Steinberg < vinzent.steinb...@googlemail.com> wrote: > 2010/4/6 Christian Muise : > > The output from the following polynomials function has the order of > > argu

Fix for the polynomials docstring test.

The output from the following polynomials function has the order of arguments wrong (although mathematically correct): - solve_poly_system([y**2 - x**3 + 1, y*x], x, y) This was causing a test to fail. Git repo: git://github.com/haz/sympy.git Branch: doc-test Cheers -- You received this me

Re: Put unit propagation and pure literal rules inside the same loop (reducing the number of choices needed).

It got the +1, but never made it into the repo. On Fri, Apr 2, 2010 at 2:07 PM, Vinzent Steinberg < vinzent.steinb...@googlemail.com> wrote: > 2010/4/2 Christian Muise : > > That was intentional. Issue 1875 has since been marked invalid so I > removed > > the branch

Re: Put unit propagation and pure literal rules inside the same loop (reducing the number of choices needed).

, Vinzent Steinberg < vinzent.steinb...@googlemail.com> wrote: > 2010/3/26 Christian Muise : > > This corresponds to issue 1875 ( > http://code.google.com/p/sympy/issues/detail?id=1875 > > ). > > > > Branch is 'unit-prop' at git://github.com/haz/sympy.

Fixed a bug causing DPLL to think satisfiable theories are unsat.

There was a critical bug in the DPLL procedure for sat theories that didn't contain any unit clauses or pure literals. - git://github.com/haz/sympy.git - Branch: sat-bug -- You received this message because you are subscribed to the Google Groups "sympy-patches" group. To post to this group, se

Put unit propagation and pure literal rules inside the same loop (reducing the number of choices needed).

This corresponds to issue 1875 ( http://code.google.com/p/sympy/issues/detail?id=1875 ). Branch is 'unit-prop' at git://github.com/haz/sympy.git -- You received this message because you are subscribed to the Google Groups "sympy-patches" group. To post to this group, send email to sympy-patc

Re: [PATCH 2/2] Removing the option for passing in a list of pairs, since the outcome is ambiguous when two pairs are given as arguments.

It did. The branch was the combination of the two patches that made it to this list with git-email, plus an extra test case that you had suggested. Cheers On Thu, Mar 25, 2010 at 6:20 PM, Vinzent Steinberg < vinzent.steinb...@googlemail.com> wrote: > 2010/3/25 Christian Muise &g

Re: [PATCH 2/2] Removing the option for passing in a list of pairs, since the outcome is ambiguous when two pairs are given as arguments.

> > Yeah, I also prefer branches, it's trivial to push and pull. The patch > is +1 from me, I pushed it in. Thanks! Woot! Thanks guys. I had a number of git questions, but all has been cleared up via IRC. Next patch will be much smoother. Cheers -- You received this message because you a

Re: [PATCH 2/2] Removing the option for passing in a list of pairs, since the outcome is ambiguous when two pairs are given as arguments.

On Sun, Mar 21, 2010 at 9:00 PM, Christian Muise > wrote: > > Thanks for all the feedback. I've just submitted a new combined patch > with > > the suggested test case included (makes sense to me to include it). > > Where is the combined patch? Let me review it, un

Re: [PATCH 2/2] Removing the option for passing in a list of pairs, since the outcome is ambiguous when two pairs are given as arguments.

ld do it if you > think it makes sense. There is however a policy that every new > functionality has to be tested. In this case I would be fine if there > is no test (I leave this up to you), but your commit message could > explain the "ambiguous outcome". > > Thanks! &g

Re: [PATCH 1/2] Implemented the Implies class to compile away in the same sense as Xor, Nand, etc. One of the tests led to misleading results ('Implies(False, False) == False' should not hold), and

> > I see, so I'm +1 on this patch. > Probably best to still get Fabian's input -- I haven't contributed to sympy before now so there may be some "bigger picture" issues that I'm failing to see. > Is there an advantage of having all in negation normal form? > For querying the theory? Not un

Re: [PATCH 2/2] Removing the option for passing in a list of pairs, since the outcome is ambiguous when two pairs are given as arguments.

Not sure what such a test would look like...other oddities are left unhandled such as Not(). What's the policy for sympy on testing thrown errors? Cheers On Fri, Mar 19, 2010 at 4:53 PM, Vinzent Steinberg < vinzent.steinb...@googlemail.com> wrote: > 2010/3/17 C

Re: [PATCH 1/2] Implemented the Implies class to compile away in the same sense as Xor, Nand, etc. One of the tests led to misleading results ('Implies(False, False) == False' should not hold), and

t is your opinion about this? > > Vinzent > > 2010/3/17 Christian Muise : > > --- > > doc/src/modules/logic.txt |7 --- > > sympy/logic/boolalg.py| 12 +++- > > sympy/logic/tests/test_boolalg.py |6 -- > > 3 f

[PATCH 1/2] Implemented the Implies class to compile away in the same sense as Xor, Nand, etc. One of the tests led to misleading results ('Implies(False, False) == False' should not hold), and the te

--- doc/src/modules/logic.txt |7 --- sympy/logic/boolalg.py| 12 +++- sympy/logic/tests/test_boolalg.py |6 -- 3 files changed, 19 insertions(+), 6 deletions(-) diff --git a/doc/src/modules/logic.txt b/doc/src/modules/logic.txt index 2487d57..e466d5a

[PATCH 2/2] Removing the option for passing in a list of pairs, since the outcome is ambiguous when two pairs are given as arguments.

--- sympy/logic/boolalg.py |6 ++ 1 files changed, 2 insertions(+), 4 deletions(-) diff --git a/sympy/logic/boolalg.py b/sympy/logic/boolalg.py index 0a45e42..97c47b7 100755 --- a/sympy/logic/boolalg.py +++ b/sympy/logic/boolalg.py @@ -109,10 +109,8 @@ class Implies(BooleanFunction):