- a
decent
number to iterate over directly.
But as Aaron suggests, maybe we don't want to add too much of
complexity? In
that direction, I do think we should deprecate dpll1. dpll2, with clause
learning involved, is certainly better.
On Friday, January 31, 2014 12:37:09 PM UTC+5:30, Christian
If the formulae are small, then the approach there is just fine. If the
formulae is huge but the number of variables small, then just enumerating
the models should be done. If neither of those cases hold, then the best
you could hope for is to try and detect how far the input is from either
CNF
The code says that is supports simple clause learning, but it seems to
always be disabled by default. Do you know why that is?
There are many forms of clause learning. The current implementation of
clause learning adds nothing to the solving power as the backtracking is
done in such a way
Proof of concept or not, it's already used by the new assumptions system
to detect inconsistencies. If you have any suggestions on how to improve
the algorithm in pure Python, we'd love to hear them.
There's always more that can be done ;). I'd say the next obvious step
would be to
I'm scrambling at a new post-doc spot, so I don't have much time to join in
the discussion, but wanted to mention a few things that came to mind:
1. SAT solvers are indeed mighty beasts. They can solve things you'd never
expect them to be able to in mere milliseconds (if configured right).
2.
know if there are many here who can answer your questions. I
recommend reading the blog of Christian Muise, who wrote the module as part
of his Google Summer of Code project (http://haz-tech.blogspot.com/**,
read the posts from 2010). I have also CC'd him in this email.
One thing I can tell you
A great idea -- plus you can share your screen in a hangout (something I
take advantage of quite frequently), which would be useful for demoing
something or showing spots of the code.
On Sat, Apr 27, 2013 at 6:20 PM, Aaron Meurer asmeu...@gmail.com wrote:
I see that IPython has started doing
:
You'll have to forgive me, I'm still a bit of novice programmer (an
enthusiastic novice), but can someone briefly explain what you all
mean by wrapping?
On Mar 23, 1:40 pm, Joachim Durchholz j...@durchholz.org wrote:
Am 23.03.2012 17:04, schrieb Christian Muise:
Aye, wrapping should
Would a GSOC proposal along the following lines make sense?
* Improve logic/boolalg.py to include Predicate logic, fuzzy logic and
useful functionality for manipulating them
See the other thread on predicates in Sympy -- they already exist to some
extent.
* Use statements in predicate
that there is currently no
support
beyond propositional logic. There is a dpll SAT solver implemented and
that's
about it. The logic stuff is handled by Christian Muise, my mentor for
GSoC
2011 and an all round nice guy. I contributed a few small patches as
well.
The idea is to develop
Aye, wrapping should be an obvious target (you could start by wrapping a
SAT solver to replace the prototype implementation currently in there). If
there's any simple theorem proving technique that could be implemented,
it's good to have something fully written in SymPy as shipping other solves
Hi Damien,
The problem is that SymPy likely cannot (and most probably should not)
try to compete with the state of the art (e.g., the DPLL implementation
that I put in will never reach the speed of MiniSAT and other solvers out
there). That said, if there is a need within SymPy to have some form
Shot in the dark, but if 1 means it will always just return result. If you
remove the entire if block, does it still not pickle? (then it isn't an
issue with the if)
On Tue, Sep 7, 2010 at 1:19 AM, smichr smi...@gmail.com wrote:
I need some extra eyes. I can't see how changing the if 1 to if 0
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
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 basti...@gmail.com
Date: Wed May 5 22:48:18 2010 +0200
Implement fast atomic substitution.
*
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 muddled
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 christian.mu...@gmail.com
When the old assumption system is replaced, you can add new assumptions to
the global context:
global_assumptions.add(Assume(x, Q.positive))
global_assumptions.remove(Assume(x, Q.positive))
You can do that now if you want to use the ask / refine / etc part of the
new assumptions system. The
I'm having issues with the branch:
from sympy import *
Traceback (most recent call last):
File input, line 1, in module
File /usr/local/lib/python2.6/dist-packages/sympy/__init__.py, line 24,
in module
from polys import *
File
',
'sympy.printing',
'sympy.printing.pretty',
'sympy.series',
cjmu...@haz:~/Projects/sympy$
On Thu, Aug 19, 2010 at 12:39 PM, Christian Muise christian.mu...@gmail.com
wrote:
I'm having issues with the branch:
from sympy import *
Traceback (most recent call last):
File input, line
at 12:50 PM, Christian Muise christian.mu...@gmail.com
wrote:
Apparently the setup.py is dated:
cjmu...@haz:~/Projects/sympy$ git diff
diff --git a/setup.py b/setup.py
index bdec104..538904d 100755
--- a/setup.py
+++ b/setup.py
@@ -71,6 +71,7 @@
'sympy.mpmath.matrices
By the way, why do you install the package? There is no need to do that.
Just run ./bin/isympy from the sympy directory.
Habit ;). I like running my python files from the command line, and
`bin/isympy ri.py` executes the file before the preface for isympy (setting
up the environment,
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
, 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 christian.mu...@gmail.com:
Ok, so I went through the growing pains of figuring all this git stuff
out,
at we should be good
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
http://github.com/haz/sympy/tree/soc-final-fixed The commits are linear,
all tests should be running clean (regardless of
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...you mean
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...you mean
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
Hello everyone,
I was hoping to get some input on people's thoughts regarding the SymPy
cache. In the branch I have going to remove the old assumption system, I run
into the problem of equations being simplified under a certain set of
assumptions, and then retrieved later on when those
On Tue, Jun 22, 2010 at 12:31 AM, Ondrej Certik ond...@certik.cz wrote:
I would be more than happy if we can remove all caching altogether,
but since it currently would slow sympy down, Well, maybe not anymore.
We should do some tests. But let's say we need to keep the cache (at
least
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
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:
-
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 ond...@certik.cz wrote:
On Thu, Jun 17, 2010 at 8:19 AM, Christian
17, 2010 at 2:17 PM, Christian Muise
christian.mu...@gmail.comwrote:
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
inherited from
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:
I was also kind of surprised by all those patches. It would be nice if
anyone could help out us newcomers with a hint about where the disussion
took place.
I just recently discovered the discussions I was missing:
- http://code.google.com/p/sympy/feeds
Just this one:
- http://planet.sympy.org/
http://planet.sympy.org/ Cheers
On Wed, Jun 16, 2010 at 10:08 AM, Øyvind Jensen jensen.oyv...@gmail.comwrote:
I just recently discovered the discussions I was missing:
- http://code.google.com/p/sympy/feeds
-- Check out the feed for Issue
I think the current suggested form is to fork the sympy/sympy (with
github's forking feature), and pull changes from the git.sympy.org repo
(with a remote repository set up). Forking the sympy/sympy puts you in a
github network that lets everyone track what's going on (to some extent).
Cheers
for merger.
What about Vinzent's stuff?
Cheers
On Tue, May 18, 2010 at 12:53 PM, Ondrej Certik ond...@certik.cz wrote:
On Tue, May 18, 2010 at 6:03 AM, Christian Muise
christian.mu...@gmail.com wrote:
I'm starting to get mighty confused with the parallel attempts. Fabian,
Ronan
I'm starting to get mighty confused with the parallel attempts. Fabian,
Ronan, and Ondrej all have at least one branch doing the same thing that is
very closely related to my SoC goals -- removing the old system and making
the new one uber fast. Any suggestions on how to unify all the threads?
Yowzas...
- Why the changes from self.new(...) to self.__class__(...)? (it happens
in a number of places)
- I never know about facts.py :p. I was just trying the disconnect by
removing the inheritance from Basic(AssumMeths)
- Is there a canonical way I can search through all the outstanding
So this is how the forking looks at the moment:
- http://github.com/certik/sympy/network/members
Should sympy/sympy be at the top of the chain or will that remain as
certik? Should we continue to pull changes from git.sympy.org, or just
the github sympy repo?
Thanks. Cheers
On May 3, 7:22
Hello,
Should the work us SoC'ers do this summer constantly pull from the master
so merging back at the end isn't a hassle? I was nailed for that a few years
back and as a result the code never made it back in.
Cheers
On Thu, Apr 29, 2010 at 4:32 PM, Ondrej Certik ond...@certik.cz wrote:
PM, Ondrej Certik ond...@certik.cz wrote:
On Wed, Apr 21, 2010 at 7:30 PM, Christian Muise
christian.mu...@gmail.com wrote:
Anyone planning on attending the Sage Days in Toronto by any chance?
- http://www.fields.utoronto.ca/programs/scientific/09-10/sage/
I can't go there, but you should
Anyone planning on attending the Sage Days in Toronto by any chance?
- http://www.fields.utoronto.ca/programs/scientific/09-10/sage/
--
You received this message because you are subscribed to the Google Groups
sympy group.
To post to this group, send email to sy...@googlegroups.com.
To
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
, Vinzent Steinberg
vinzent.steinb...@googlemail.com wrote:
2010/3/26 Christian Muise christian.mu...@gmail.com:
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
I think when cleaning up
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 christian.mu...@gmail.com:
That was intentional. Issue 1875 has since been marked invalid so I
removed
the branch
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,
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
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 christian.mu
wrote:
On Sun, Mar 21, 2010 at 9:00 PM, Christian Muise
christian.mu...@gmail.com 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, unless
, then is a
multi-tiered application acceptable or should separate applications be put
forward?
-
Again, thanks for putting this summary out. It helps clear things up quite
a bit.
Cheers,
Christian Muise
On Tue, Mar 23, 2010 at 1:10 PM, Fabian Pedregosa fab...@fseoane.netwrote:
Hi all
/17 Christian Muise christian.mu...@gmail.com:
---
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
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 Christian Muise christian.mu
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 unless
,
On Wed, Mar 17, 2010 at 08:25:15AM -0700, Christian Muise wrote:
Having dug deeper, it appears that first order logic isn't even
included in the current version of sympy. Is there some manner of
generic (existential and universal) quantification in the sympy core
that I'm missing
Having dug deeper, it appears that first order logic isn't even
included in the current version of sympy. Is there some manner of
generic (existential and universal) quantification in the sympy core
that I'm missing?
Thanks. Cheers
On Mar 16, 1:37 pm, Christian Muise christian.mu
Hello,
I was interested in applying for SoC this year, and as such I went
looking for issues to work on as part of the application process.
However, my main interest is primarily in logic, ie. anything that
goes under here:
- http://tinyurl.com/ylxkjdy
Issue 1545 is the only relevant looking
59 matches
Mail list logo
