New assumption system
Fabian Pedregosa
consists of:
- preparatory stuff (patches 1-5)
- a logic module (much cleaner than the old one)
- new style-assumptions (very simple objects)
- query module, which substitutes the .is_* syntax
I tried hard to separate these 3 functionalities as much as possible.
This is more an initial implementation from whom we can star to work rather than a
finished product, so in case you have any objections, we can start discussing.
Thanks for the review,
- Fabian
pd: patch 3 was already approved, just that i did not push it in.
Fabian Pedregosa
variations is a routine that calculates all possible variations
of size n (with or without repetition) of a given set.
---
doc/src/modules.txt | 1 +
doc/src/modules/utilities/index.txt | 11 ++++++++
doc/src/modules/utilities/iterables.txt | 39 +++++++++++++++++++++++++++++++
sympy/utilities/iterables.py | 36 ++++++++++++++++++++++++++++
sympy/utilities/tests/test_iterables.py | 6 ++++-
5 files changed, 92 insertions(+), 1 deletions(-)
create mode 100644 doc/src/modules/utilities/index.txt
create mode 100644 doc/src/modules/utilities/iterables.txt
diff --git a/doc/src/modules.txt b/doc/src/modules.txt
index fca4eb6..6c46683 100644
--- a/doc/src/modules.txt
+++ b/doc/src/modules.txt
@@ -31,6 +31,7 @@ access any SymPy module, or use this contens:
modules/statistics.txt
modules/concrete.txt
modules/solvers.txt
+ modules/utilities/index.txt
Contributions to docs
---------------------
diff --git a/doc/src/modules/utilities/index.txt b/doc/src/modules/utilities/index.txt
new file mode 100644
index 0000000..3e1e692
--- /dev/null
+++ b/doc/src/modules/utilities/index.txt
@@ -0,0 +1,11 @@
+Utilities
+=========
+
+This module contains some general purpose utilities that are used across SymPy
+
+Contents:
+
+.. toctree::
+ :maxdepth: 2
+
+ iterables.txt
\ No newline at end of file
diff --git a/doc/src/modules/utilities/iterables.txt b/doc/src/modules/utilities/iterables.txt
new file mode 100644
index 0000000..023a3bc
--- /dev/null
+++ b/doc/src/modules/utilities/iterables.txt
@@ -0,0 +1,39 @@
+Iterables
+=========
+
+cartes
+------
+
+Returns the cartesian product of two sequences
+
+Examples::
+ >>> from sympy.utilities.iterables import cartes
+ >>> cartes([1,2,3], ['a', 'b', 'c'])
+ [[1, 'a'],
+ [1, 'b'],
+ [1, 'c'],
+ [2, 'a'],
+ [2, 'b'],
+ [2, 'c'],
+ [3, 'a'],
+ [3, 'b'],
+ [3, 'c']]
+
+
+
+variations
+----------
+
+variations(seq, n) Returns all the variations of the list of size n.
+
+Has an optional third argument. Must be a boolean value and makes the method
+return the variations with repetition if set to True, or the variations
+without repetition if set to False.
+
+Examples::
+ >>> from sympy.utilities.iterables import variations
+ >>> variations([1,2,3], 2)
+ [[1, 2], [1, 3], [2, 1], [2, 3], [3, 1], [3, 2]]
+ >>> variations([1,2,3], 2, True)
+ [[1, 1], [1, 2], [1, 3], [2, 1], [2, 2], [2, 3], [3, 1], [3, 2], [3, 3]]
+
diff --git a/sympy/utilities/iterables.py b/sympy/utilities/iterables.py
index 6179622..24ebcd0 100644
--- a/sympy/utilities/iterables.py
+++ b/sympy/utilities/iterables.py
@@ -173,3 +173,39 @@ def recursion(result, M, k):
for elem in recursion([item], M[i + 1:], k - 1):
yield elem
+
+def cartes(seq0, seq1, modus='pair'):
+ """Return the cartesian product of two sequences """
+ if modus == 'pair':
+ return [[item0, item1] for item0 in seq0 for item1 in seq1]
+ elif modus == 'triple':
+ return [item0 + [item1] for item0 in seq0 for item1 in seq1]
+
+def variations(seq, n, repetition=False):
+ """Returns all the variations of the list of size n.
+
+ variations(seq, n, True) will return all the variations of the list of
+ size n with repetitions
+
+ variations(seq, n, False) will return all the variations of the list of
+ size n without repetitions
+ """
+ def setrep(seq): # remove sets with duplicates (repetition is relevant)
+ def delrep(seq): # remove duplicates while maintaining order
+ result = []
+ for item in seq:
+ if item not in result:
+ result.append(item)
+ return result
+ return [item for item in seq if item == delrep(item)]
+
+ if n == 1:
+ return [[item] for item in seq]
+ result = range(len(seq))
+ cartesmodus = 'pair'
+ for i in range(n-1):
+ result = cartes(result, range(len(seq)), cartesmodus)
+ if not repetition:
+ result = setrep(result)
+ cartesmodus = 'triple'
+ return [[seq[index] for index in indices] for indices in result]
diff --git a/sympy/utilities/tests/test_iterables.py b/sympy/utilities/tests/test_iterables.py
index 1eea497..959c900 100644
--- a/sympy/utilities/tests/test_iterables.py
+++ b/sympy/utilities/tests/test_iterables.py
@@ -1,6 +1,6 @@
from sympy import symbols
from sympy.utilities.iterables import postorder_traversal, \
- preorder_traversal, flatten, subsets
+ preorder_traversal, flatten, subsets, variations
w,x,y,z= symbols('wxyz')
@@ -31,3 +31,7 @@ def test_subsets():
assert list(subsets([1, 2, 3], 2)) == [[1, 2], [1,3], [2, 3]]
assert list(subsets([1, 2, 3], 3)) == [[1, 2, 3]]
+def test_variations():
+ assert variations([1,2,3], 2) == [[1, 2], [1, 3], [2, 1], [2, 3], [3, 1], [3, 2]]
+ assert variations([1,2,3], 2, True) == [[1, 1], [1, 2], [1, 3], [2, 1], [2, 2], [2, 3], \
+ [3,1], [3,2], [3,3]]
--
1.6.1.2
Fabian Pedregosa
Function get_class returns a class from a given string. It makes use
of get_mod_func
Implemented after a function with same name in django's codebase
---
sympy/utilities/source.py | 30 ++++++++++++++++++++++++++++++
sympy/utilities/tests/test_source.py | 8 ++++++++
2 files changed, 38 insertions(+), 0 deletions(-)
create mode 100644 sympy/utilities/tests/test_source.py
diff --git a/sympy/utilities/source.py b/sympy/utilities/source.py
index 56ca7f7..213d3d8 100644
--- a/sympy/utilities/source.py
+++ b/sympy/utilities/source.py
@@ -10,3 +10,33 @@ def source(object):
"""
print 'In file: %s' % inspect.getsourcefile(object)
print inspect.getsource(object)
+
+def get_class(lookup_view):
+ """
+ Convert a string version of a class name to the object.
+
+ For example, get_class('sympy.core.Basic') will return
+ class Basic located in module sympy.core
+ """
+ if isinstance(lookup_view, str):
+ # Bail early for non-ASCII strings (they can't be functions).
+ lookup_view = lookup_view.encode('ascii')
+ mod_name, func_name = get_mod_func(lookup_view)
+ if func_name != '':
+ lookup_view = getattr(__import__(mod_name, {}, {}, ['']), func_name)
+ if not callable(lookup_view):
+ raise AttributeError("'%s.%s' is not a callable." % (mod_name, func_name))
+ return lookup_view
+
+def get_mod_func(callback):
+ """
+ splits the string path to a class into a string path to the module
+ and the name of the class. For example:
+ >>> get_mod_func('sympy.core.basic.Basic')
+ ('sympy.core.basic', 'Basic')
+ """
+ try:
+ dot = callback.rindex('.')
+ except ValueError:
+ return callback, ''
+ return callback[:dot], callback[dot+1:]
\ No newline at end of file
diff --git a/sympy/utilities/tests/test_source.py b/sympy/utilities/tests/test_source.py
new file mode 100644
index 0000000..0716d46
--- /dev/null
+++ b/sympy/utilities/tests/test_source.py
@@ -0,0 +1,8 @@
+from sympy.utilities.source import get_mod_func, get_class
+
+def test_get_mod_func():
+ assert get_mod_func('sympy.core.basic.Basic') == ('sympy.core.basic', 'Basic')
+
+def test_get_class():
+ _basic = get_class('sympy.core.basic.Basic')
+ assert _basic.__name__ == 'Basic'
\ No newline at end of file
--
1.6.1.2
Fabian Pedregosa
or tuples.
I don't know the reason of this behaviour, fortunately
changing it did not break any tests.
I added a test for this
---
sympy/core/function.py | 17 ++++++-----------
sympy/core/tests/test_functions.py | 7 +++++++
2 files changed, 13 insertions(+), 11 deletions(-)
diff --git a/sympy/core/function.py b/sympy/core/function.py
index aae869d..8331751 100644
--- a/sympy/core/function.py
+++ b/sympy/core/function.py
@@ -138,18 +138,13 @@ def __new__(cls, *args, **options):
# up to here.
if options.get('evaluate') is False:
return Basic.__new__(cls, *args, **options)
- r = cls.eval(*args)
- if isinstance(r, Basic):
+ evaluated = cls.eval(*args)
+ if evaluated is not None: return evaluated
+ # Just undefined functions have nargs == None
+ if not cls.nargs and hasattr(cls, 'undefined_Function'):
+ r = Basic.__new__(cls, *args, **options)
+ r.nargs = len(args)
return r
- elif r is None:
- # Just undefined functions have nargs == None
- if not cls.nargs and hasattr(cls, 'undefined_Function'):
- r = Basic.__new__(cls, *args, **options)
- r.nargs = len(args)
- return r
- pass
- elif not isinstance(r, tuple):
- args = (r,)
return Basic.__new__(cls, *args, **options)
@property
diff --git a/sympy/core/tests/test_functions.py b/sympy/core/tests/test_functions.py
index 8d7d165..94b08a6 100644
--- a/sympy/core/tests/test_functions.py
+++ b/sympy/core/tests/test_functions.py
@@ -290,3 +290,10 @@ def eq(a,b,eps):
assert eq(exp(-0.5+1.5*I).evalf(15), Real("0.0429042815937374") + Real("0.605011292285002")*I, 1e-13)
assert eq(log(pi+sqrt(2)*I).evalf(15), Real("1.23699044022052") + Real("0.422985442737893")*I, 1e-13)
assert eq(cos(100).evalf(15), Real("0.86231887228768"), 1e-13)
+
+def test_extensibility_eval():
+ class MyFunc(Function):
+ @classmethod
+ def eval(cls, *args):
+ return (0,0,0)
+ assert MyFunc(0) == (0,0,0)
Fabian Pedregosa
This will be used in the logic module to denest classes of the same type
(but I believe it will be useful also in other places)
---
sympy/utilities/iterables.py | 25 +++++++++++++++++++++----
sympy/utilities/tests/test_iterables.py | 6 ++++++
2 files changed, 27 insertions(+), 4 deletions(-)
diff --git a/sympy/utilities/iterables.py b/sympy/utilities/iterables.py
index 24ebcd0..8d96b04 100644
--- a/sympy/utilities/iterables.py
+++ b/sympy/utilities/iterables.py
@@ -65,7 +65,7 @@ def make_list(expr, kind):
return [expr]
-def flatten(iterable):
+def flatten(iterable, cls=None):
"""Recursively denest iterable containers.
>>> flatten([1, 2, 3])
@@ -77,13 +77,30 @@ def flatten(iterable):
>>> flatten( (1,2, (1, None)) )
[1, 2, 1, None]
+ If cls argument is specif, it will only flatten instances of that
+ class, for example:
+
+ >>> from sympy.core import Basic
+ >>> class MyOp(Basic):
+ ... pass
+ ...
+ >>> flatten([MyOp(1, MyOp(2, 3))], cls=MyOp)
+ [1, 2, 3]
+
+
+
adapted from http://kogs-www.informatik.uni-hamburg.de/~meine/python_tricks
"""
-
+ if cls is None:
+ reducible = lambda x: hasattr(x, "__iter__") and not isinstance(x, basestring)
+ else:
+ reducible = lambda x: isinstance(x, cls)
result = []
for el in iterable:
- if hasattr(el, "__iter__") and not isinstance(el, basestring):
- result.extend(flatten(el))
+ if reducible(el):
+ if hasattr(el, 'args'):
+ el = el.args
+ result.extend(flatten(el, cls=cls))
else:
result.append(el)
return result
diff --git a/sympy/utilities/tests/test_iterables.py b/sympy/utilities/tests/test_iterables.py
index 959c900..3aaf3be 100644
--- a/sympy/utilities/tests/test_iterables.py
+++ b/sympy/utilities/tests/test_iterables.py
@@ -25,6 +25,12 @@ def test_flatten():
assert flatten( (1,(1,)) ) == [1,1]
assert flatten( (x,(x,)) ) == [x,x]
+ from sympy.core.basic import Basic
+ class MyOp(Basic):
+ pass
+ assert flatten( [MyOp(x, y), z]) == [MyOp(x, y), z]
+ assert flatten( [MyOp(x, y), z], cls=MyOp) == [x, y, z]
+
def test_subsets():
assert list(subsets([1, 2, 3], 1)) == [[1], [2], [3]]
--
1.6.1.2
Fabian Pedregosa
but with the logic module with classes inheriting from basic, I need
to manipulate boolean expressions, so converting booleans to S.One
and S.Zero is in my oppinion wrong because of conceptual reasons
and efficiency.
The only module that used this behaviour was functions.elementary.piecewise,
and was adopted to use the new one.
---
sympy/core/sympify.py | 4 ++--
sympy/functions/elementary/piecewise.py | 18 +++++++++++-------
sympy/printing/ccode.py | 2 +-
sympy/printing/latex.py | 2 +-
sympy/printing/pretty/pretty.py | 2 +-
sympy/utilities/decorator.py | 3 ++-
6 files changed, 18 insertions(+), 13 deletions(-)
diff --git a/sympy/core/sympify.py b/sympy/core/sympify.py
index 8da69d2..b00961b 100644
--- a/sympy/core/sympify.py
+++ b/sympy/core/sympify.py
@@ -57,6 +57,8 @@ def sympify(a, locals=None, convert_xor=True):
return a
if isinstance(a, BasicType):
return a
+ elif isinstance(a, bool):
+ return a
elif isinstance(a, (int, long)):
return Integer(a)
elif isinstance(a, (float, decimal.Decimal)):
@@ -68,8 +70,6 @@ def sympify(a, locals=None, convert_xor=True):
if ireal + iimag*1j == a:
return ireal + iimag*S.ImaginaryUnit
return real + S.ImaginaryUnit * imag
- elif isinstance(a, bool):
- raise NotImplementedError("bool support")
elif isinstance(a, (list,tuple,set)):
return type(a)([sympify(x) for x in a])
diff --git a/sympy/functions/elementary/piecewise.py b/sympy/functions/elementary/piecewise.py
index d5afef7..3abbb1f 100644
--- a/sympy/functions/elementary/piecewise.py
+++ b/sympy/functions/elementary/piecewise.py
@@ -147,7 +147,7 @@ def _eval_interval(self, sym, a, b):
# - eg x < 1, x < 3 -> [oo,1],[1,3] instead of [oo,1],[oo,3]
# 3) Sort the intervals to make it easier to find correct exprs
for expr, cond in self.args:
- if cond.is_Number:
+ if isinstance(cond, bool) or cond.is_Number:
if cond:
default = expr
break
@@ -203,15 +203,19 @@ def _eval_derivative(self, s):
def _eval_subs(self, old, new):
if self == old:
return new
- return Piecewise(*[(e._eval_subs(old, new), c._eval_subs(old, new)) \
- for e, c in self.args])
+ new_args = []
+ for e, c in self.args:
+ if isinstance(c, bool):
+ new_args.append((e._eval_subs(old, new), c))
+ else:
+ new_args.append((e._eval_subs(old, new), c._eval_subs(old, new)))
+ return Piecewise( *new_args )
@classmethod
def __eval_cond(cls, cond):
"""Returns S.One if True, S.Zero if False, or None if undecidable."""
- if type(cond) == bool or cond.is_number:
- return sympify(bool(cond))
- if cond.args[0].is_Number and cond.args[1].is_Number:
- return sympify(bool(cond))
+ if type(cond) == bool or cond.is_number or (cond.args[0].is_Number and cond.args[1].is_Number):
+ if cond: return S.One
+ return S.Zero
return None
diff --git a/sympy/printing/ccode.py b/sympy/printing/ccode.py
index a1341b5..7a6ccf6 100644
--- a/sympy/printing/ccode.py
+++ b/sympy/printing/ccode.py
@@ -38,7 +38,7 @@ def _print_Piecewise(self, expr):
ecpairs = ["(%s) {\n%s\n}\n" % (self._print(c), self._print(e)) \
for e, c in expr.args[:-1]]
last_line = ""
- if expr.args[-1].cond is S.One:
+ if expr.args[-1].cond == True:
last_line = "else {\n%s\n}" % self._print(expr.args[-1].expr)
else:
ecpairs.append("(%s) {\n%s\n" % \
diff --git a/sympy/printing/latex.py b/sympy/printing/latex.py
index 6f2b089..02cdd00 100644
--- a/sympy/printing/latex.py
+++ b/sympy/printing/latex.py
@@ -521,7 +521,7 @@ def _print_Relational(self, expr):
def _print_Piecewise(self, expr):
ecpairs = [r"%s & for %s" % (self._print(e), self._print(c)) \
for e, c in expr.args[:-1]]
- if expr.args[-1].cond is S.One:
+ if expr.args[-1].cond == True:
ecpairs.append(r"%s & \textrm{otherwise}" % \
self._print(expr.args[-1].expr))
else:
diff --git a/sympy/printing/pretty/pretty.py b/sympy/printing/pretty/pretty.py
index 5065d6c..19ffff2 100644
--- a/sympy/printing/pretty/pretty.py
+++ b/sympy/printing/pretty/pretty.py
@@ -318,7 +318,7 @@ def _print_Piecewise(self, pexpr):
P = {}
for n, ec in enumerate(pexpr.args):
P[n,0] = self._print(ec.expr)
- if ec.cond is S.One:
+ if ec.cond == True:
P[n,1] = prettyForm('otherwise')
else:
P[n,1] = prettyForm(*prettyForm('for ').right(self._print(ec.cond)))
diff --git a/sympy/utilities/decorator.py b/sympy/utilities/decorator.py
index 1d022d6..489f781 100644
--- a/sympy/utilities/decorator.py
+++ b/sympy/utilities/decorator.py
@@ -39,6 +39,8 @@ def threaded_proxy(func):
def threaded_decorator(expr, *args, **kwargs):
if isinstance(expr, Matrix):
return expr.applyfunc(lambda f: func(f, *args, **kwargs))
+ elif isinstance(expr, bool):
+ return expr
elif hasattr(expr, '__iter__'):
return expr.__class__([ func(f, *args, **kwargs) for f in expr ])
else:
@@ -47,7 +49,6 @@ def threaded_decorator(expr, *args, **kwargs):
if isinstance(expr, Relational):
lhs = func(expr.lhs, *args, **kwargs)
rhs = func(expr.rhs, *args, **kwargs)
-
return Relational(lhs, rhs, expr.rel_op)
elif expr.is_Add and use_add:
return Add(*[ func(f, *args, **kwargs) for f in expr.args ])
--
1.6.1.2
Fabian Pedregosa
storing an expression, a key (string) and a value (boolean).
This will be used extensively by the query module
---
sympy/__init__.py | 1 +
sympy/assumptions/__init__.py | 1 +
sympy/assumptions/assumptions.py | 41 +++++++++++++++++++++++++
sympy/assumptions/known_facts.py | 21 +++++++++++++
sympy/assumptions/tests/test_assumptions_2.py | 23 ++++++++++++++
5 files changed, 87 insertions(+), 0 deletions(-)
create mode 100644 sympy/assumptions/__init__.py
create mode 100644 sympy/assumptions/assumptions.py
create mode 100644 sympy/assumptions/known_facts.py
create mode 100644 sympy/assumptions/tests/test_assumptions_2.py
diff --git a/sympy/__init__.py b/sympy/__init__.py
index f4c7d3a..d5b33fc 100644
--- a/sympy/__init__.py
+++ b/sympy/__init__.py
@@ -22,6 +22,7 @@ def __sympy_debug():
import symbol as stdlib_symbol
from sympy.core import *
+from assumptions import Assume
from polys import *
from series import *
from functions import *
diff --git a/sympy/assumptions/__init__.py b/sympy/assumptions/__init__.py
new file mode 100644
index 0000000..41e388a
--- /dev/null
+++ b/sympy/assumptions/__init__.py
@@ -0,0 +1 @@
+from assumptions import Assume
\ No newline at end of file
diff --git a/sympy/assumptions/assumptions.py b/sympy/assumptions/assumptions.py
new file mode 100644
index 0000000..473751d
--- /dev/null
+++ b/sympy/assumptions/assumptions.py
@@ -0,0 +1,41 @@
+from sympy.core.symbol import Symbol
+
+class Assume(object):
+ """New-style assumptions
+
+ >>> from sympy import Symbol, Assume
+ >>> x = Symbol('x')
+ >>> Assume(x, integer=True)
+ Assume( x, integer, True )
+ >>> Assume(x, integer=False)
+ Assume( x, integer, False )
+ """
+
+ __global_registry = {}
+
+ def __init__(self, expr, *args, **kwargs):
+ if not isinstance(expr, Symbol):
+ raise NotImplementedError
+ if len(kwargs) != 1:
+ raise ValueError('Wrong set of arguments')
+ self._args = (expr, kwargs.keys()[0], kwargs.values()[0])
+
+ @property
+ def expr(self):
+ return self._args[0]
+
+ @property
+ def key(self):
+ return self._args[1]
+
+ @property
+ def value(self):
+ return self._args[2]
+
+ def __repr__(self):
+ return u"Assume( %s, %s, %s )" % (self.expr, self.key, self.value)
+
+ def __eq__(self, other):
+ if isinstance(other, type(self)):
+ return self._args == other._args
+ return False
\ No newline at end of file
diff --git a/sympy/assumptions/known_facts.py b/sympy/assumptions/known_facts.py
new file mode 100644
index 0000000..cb2a9e9
--- /dev/null
+++ b/sympy/assumptions/known_facts.py
@@ -0,0 +1,21 @@
+
+known_facts_dict = {
+ 'even' : ['integer & ~odd'],
+ 'composite' : ['integer & ~prime'],
+ 'complex' : ['real | imaginary', 'rational | irrational | imaginary'], # this is not quite correct
+ 'integer' : ['rational & numerator_is_one'],
+ 'irrational' : ['real & ~rational'],
+ 'imaginary' : ['complex & ~real'],
+ 'rational' : ['real & ~irrational'],
+ 'real' : ['complex & ~imaginary', 'rational | irrational'],
+ 'unbounded' : ['extended_real & ~bounded'],
+ 'negative' : ['real & ~positive & ~zero'],
+ 'nonpositive': ['real & ~positive', 'zero | negative'],
+ 'nonnegative': ['real & ~negative', 'zero | positive'],
+ 'noninteger' : ['real & ~integer'],
+ 'nonzero' : ['real & ~zero'],
+ 'odd' : ['integer & ~even'],
+ 'prime' : ['integer & positive & ~composite'],
+ 'positive' : ['real & ~negative & ~zero'],
+ 'zero' : ['real & ~positive & ~negative']
+}
diff --git a/sympy/assumptions/tests/test_assumptions_2.py b/sympy/assumptions/tests/test_assumptions_2.py
new file mode 100644
index 0000000..768418d
--- /dev/null
+++ b/sympy/assumptions/tests/test_assumptions_2.py
@@ -0,0 +1,23 @@
+"""rename this to test_assumptions.py when the old assumptions system is deleted"""
+from sympy.core import Symbol
+from sympy.assumptions import Assume
+
+def test_assume():
+ x = Symbol('x')
+ assump = Assume(x, integer=True)
+ assert assump.expr == x
+ assert assump.key == 'integer'
+ assert assump.value == True
+
+def test_assume_False():
+ x = Symbol('x')
+ assump = Assume(x, integer=False)
+ assert assump.expr == x
+ assert assump.key == 'integer'
+ assert assump.value == False
+
+def test_assume_equal():
+ x = Symbol('x')
+ assert Assume(x, positive=True) == Assume(x, positive=True)
+ assert Assume(x, positive=True) != Assume(x, positive=False)
+ assert Assume(x, positive=False) == Assume(x, positive=False)
Fabian Pedregosa
The old query system (.is_* properties) has some limitations:
1. Can't assume relations. It is not possible to specify relations between different
objects. For example, you can assume that x>0 and y>0, but you can't
assume x>y
2. Verbose code splitted across multiple classes. Each class must override
query methods (.is_*).
3. Extensibility. To add new assumptions you have to add code to
the core
The assumption system implemented in this series of patches relies on these
principles:
1. Assumptions are separate from objects. Assumptions are instances of Assume, which is
a class that holds a reference to the expression and to the 'key' (what it assumes)
2. Queries out of the core. No more .is_* methods. Specific queries are implemented
as subclasses of QueryHandler, and the query function calls the appropriate
subclass of QueryHandler
query -> QueryHandler -> QueryNegativeHandler
-> QueryIntegerHandler
-> QueryBoundedHandler
...
That way, creating new queries is a matter of subclassing QueryHandler and override
the apropriate methods.
PD: note that this query module cannot use relations (yet), but at least the infraestructure
is ready to support them.
---
sympy/__init__.py | 1 +
sympy/query/__init__.py | 130 ++++++++
sympy/query/handlers/__init__.py | 103 +++++++
sympy/query/handlers/calculus.py | 118 ++++++++
sympy/query/handlers/ntheory.py | 114 +++++++
sympy/query/handlers/order.py | 156 ++++++++++
sympy/query/handlers/sets.py | 255 ++++++++++++++++
sympy/query/tests/test_query.py | 606 ++++++++++++++++++++++++++++++++++++++
8 files changed, 1483 insertions(+), 0 deletions(-)
create mode 100644 sympy/query/__init__.py
create mode 100644 sympy/query/handlers/__init__.py
create mode 100644 sympy/query/handlers/calculus.py
create mode 100644 sympy/query/handlers/ntheory.py
create mode 100644 sympy/query/handlers/order.py
create mode 100644 sympy/query/handlers/sets.py
create mode 100644 sympy/query/tests/test_query.py
diff --git a/sympy/__init__.py b/sympy/__init__.py
index d5b33fc..3f08748 100644
--- a/sympy/__init__.py
+++ b/sympy/__init__.py
@@ -34,6 +34,7 @@ def __sympy_debug():
from geometry import *
from utilities import *
from integrals import *
+from query import query
# This module is slow to import:
#from physics import units
from plotting import Plot, textplot
diff --git a/sympy/query/__init__.py b/sympy/query/__init__.py
new file mode 100644
index 0000000..6d7f228
--- /dev/null
+++ b/sympy/query/__init__.py
@@ -0,0 +1,130 @@
+# -*- coding: utf-8 -*-
+import inspect
+from sympy.core import Symbol, sympify
+from sympy.utilities.source import get_class
+from sympy.assumptions.known_facts import known_facts_dict
+from sympy.logic.kb import PropKB
+from sympy.logic.boolalg import compile_rule
+
+def query(expr, *args, **kwargs):
+ """
+ 1. We build a knowledge base
+ """
+ assumptions = kwargs.pop('assumptions', [])
+ if not isinstance(assumptions, (list, tuple)):
+ assumptions = [assumptions]
+
+ key, value = kwargs.popitem()
+ expr = sympify(expr)
+ if len(kwargs) > 0:
+ # split multiple queries
+ k = {key: value}
+ return query(expr, assumptions=assumptions, **k) and \
+ query(expr, assumptions=assumptions, **kwargs)
+ if not value: # only True queries from now on (e.g. prime=True)
+ k = {key: True}
+ result = query(expr, assumptions=assumptions, **k)
+ if result is not None:
+ return not result
+ return
+
+ # direct resolution method, no logic
+ resolutor = get_class(handlers_dict[key])(expr, key, assumptions)
+ if resolutor.resolution is not None:
+ return resolutor.resolution
+
+ # use logic inference
+ if not expr.is_Atom: return
+ kb = PropKB()
+ # add the knowledge base facts related to assumptions
+ for assump in assumptions:
+ if expr.has(assump.expr):
+ if assump.value:
+ kb.tell(Symbol(assump.key))
+ else:
+ kb.tell(~Symbol(assump.key))
+ for s in known_facts_dict.get(assump.key, []):
+ if assump.value:
+ kb.tell(compile_rule(s))
+ else:
+ kb.tell(~compile_rule(s))
+
+ if kb.ask(Symbol(key)): return True
+ if kb.ask(~Symbol(key)): return False
+
+ # try to prove some equivalent fact
+ equiv = known_facts_dict.get(key, [])
+ #if equiv is None: return
+ for s in equiv:
+ rule = compile_rule(s)
+ if kb.ask(rule):
+ return True
+ elif kb.ask(~rule):
+ return False
+
+ # try some depht-first search, we collect all info in the
+ # knowledge base
+ symbols = []
+ for clause in kb.clauses:
+ for s in clause.atoms(Symbol):
+ if str(s) == key: continue
+ if str(s) in [x.key for x in assumptions]: continue
+ if s not in symbols:
+ symbols.append(s)
+
+ for sym in symbols:
+ if kb.ask(sym) == True:
+ for s in known_facts_dict.get(str(sym), []):
+ kb.tell(compile_rule(s))
+
+ if kb.ask(Symbol(key)): return True
+ if kb.ask(~Symbol(key)): return False
+
+# query_dict tells us what query handler we should use
+# for a particular key
+handlers_dict = {
+ 'bounded' : 'sympy.query.handlers.calculus.QueryBoundedHandler',
+ 'commutative' : 'sympy.query.handlers.QueryCommutativeHandler',
+ 'comparable' : 'sympy.query.handlers.QueryComparableHadler',
+ 'complex' : 'sympy.query.handlers.sets.QueryComplexHandler',
+ 'composite' : 'sympy.query.handlers.ntheory.QueryCompositeHandler',
+ 'even' : 'sympy.query.handlers.ntheory.QueryEvenHandler',
+ 'extended_real' : 'sympy.query.handlers.sets.QueryExtendedRealHandler',
+ 'finite' : 'sympy.query.handlers.QueryFiniteHandler',
+ 'imaginary' : 'sympy.query.handlers.sets.QueryImaginaryHandler',
+ 'infinitesimal' : 'sympy.query.handlers.QueryInfinitesimalHandler',
+ 'integer' : 'sympy.query.handlers.sets.QueryIntegerHandler',
+ 'irrational' : 'sympy.query.handlers.sets.QueryIrrationalHandler',
+ 'rational' : 'sympy.query.handlers.sets.QueryRationalHandler',
+ 'nonnegative' : 'sympy.query.handlers.order.QueryNonNegativeHandler',
+ 'noninteger' : 'sympy.query.handlers.sets.QueryNonIntegerHandler',
+ 'nonpositive' : 'sympy.query.handlers.order.QueryNonPositiveHandler',
+ 'nonzero' : 'sympy.query.handlers.order.QueryNonZeroHandler',
+ 'negative' : 'sympy.query.handlers.order.QueryNegativeHandler',
+ 'positive' : 'sympy.query.handlers.order.QueryPositiveHandler',
+ 'prime' : 'sympy.query.handlers.ntheory.QueryPrimeHandler',
+ 'real' : 'sympy.query.handlers.sets.QueryRealHandler',
+ 'odd' : 'sympy.query.handlers.ntheory.QueryOddHandler',
+ 'unbounded' : 'sympy.query.handlers.calculus.QueryUnboundedHandler',
+ 'zero' : 'sympy.query.handlers.order.QueryZeroHandler'
+}
+
+class QueryHandler(object):
+ """Base class that all Query Handlers must inherit"""
+
+ facts = []
+ resolution = None
+
+ def __init__(self, expr, key, assumptions=None):
+ """
+ TODO
+ """
+ self.expr = expr
+ self.key = key
+ self.assumptions = assumptions
+
+ mro = inspect.getmro(type(self.expr))
+ for subclass in mro:
+ if hasattr(self, subclass.__name__):
+ self.resolution = getattr(self, subclass.__name__)()
+ break
diff --git a/sympy/query/handlers/__init__.py b/sympy/query/handlers/__init__.py
new file mode 100644
index 0000000..8945a0b
--- /dev/null
+++ b/sympy/query/handlers/__init__.py
@@ -0,0 +1,103 @@
+
+from sympy.query import query, QueryHandler
+
+
+"""Facts must only have one level of indirection to avoid infinite recursion"""
+
+class CommonHandler(QueryHandler):
+ """Defines some useful methods common to most Handlers """
+ def Symbol(self):
+ if self.assumptions is None:
+ return None
+ for assump in self.assumptions:
+ if assump.expr == self.expr and assump.key == self.key:
+ return assump.value
+ return None
+
+ def NaN(self):
+ return False
+
+
+class QueryCommutativeHandler(CommonHandler):
+ def Basic(self):
+ for a in self.expr.args:
+ if query(a, commutative=True, assumptions=self.assumptions) == False:
+ return False
+ else:
+ return True
+
+ def NaN(self):
+ return True
+
+class QueryFiniteHandler(CommonHandler):
+
+ def Mul(self):
+ for arg in self.expr.args:
+ _result = query(arg, finite=True, assumptions=self.assumptions)
+ if not _result:
+ return _result
+ return True
+
+ Add = Mul
+
+ def Number(self):
+ return True
+
+ def Infinity(self):
+ return False
+
+ def NegativeInfinity(self):
+ return False
+
+ def NumberSymbol(self):
+ return True
+
+ def ImaginaryUnit(self):
+ return True
+
+class QueryInfinitesimalHandler(CommonHandler):
+
+ def Mul(self):
+ for arg in self.expr.args:
+ _result = query(arg, infinitesimal=True, assumptions=self.assumptions)
+ if not _result:
+ return _result
+ return True
+
+ Add = Mul
+
+ def Number(self):
+ return self.expr == 0
+
+ def Pi(self):
+ return False
+
+ def Exp1(self):
+ return False
+
+ def ImaginaryUnit(self):
+ return False
+
+class QueryComparableHadler(CommonHandler):
+
+ def Mul(self):
+ for arg in self.expr.args:
+ _result = query(arg, comparable=True, assumptions=self.assumptions)
+ if not _result:
+ return _result
+ return True
+
+ Add = Mul
+
+ def Number(self):
+ return True
+
+ def ImaginaryUnit(self):
+ return False
+
+ def Pi(self):
+ return True
+
+ def Exp1(self):
+ return True
+
diff --git a/sympy/query/handlers/calculus.py b/sympy/query/handlers/calculus.py
new file mode 100644
index 0000000..c9988b1
--- /dev/null
+++ b/sympy/query/handlers/calculus.py
@@ -0,0 +1,118 @@
+"""This module contains query handlers resposible for calculus queries:
+infinitesimal, bounded, etc.
+"""
+from sympy.query import query
+from sympy.query.handlers import CommonHandler
+
+class QueryInfinitesimalHandler(CommonHandler):
+
+ def Mul(self):
+ for arg in self.expr.args:
+ _result = query(arg, infinitesimal=True, assumptions=self.assumptions)
+ if not _result:
+ return _result
+ return True
+
+ Add = Mul
+
+ def Number(self):
+ return self.expr == 0
+
+ def Pi(self):
+ return False
+
+ def Exp1(self):
+ return False
+
+ def ImaginaryUnit(self):
+ return False
+
+
+class QueryBoundedHandler(CommonHandler):
+
+ def Add(self):
+ """
+ Bounded + Bounded -> Bounded
+ Unbounded + Bounded -> Unbounded
+ Unbounded + Unbounded -> ?
+ """
+ _output = True
+ for arg in self.expr.args:
+ _result = query(arg, bounded=True, assumptions=self.assumptions)
+ if _result is None:
+ return
+ elif _result is False:
+ if _output:
+ _output = False
+ else:
+ return
+ return _output
+
+ def Mul(self):
+ """
+ Bounded * Bounded -> Bounded
+ (NotInfinitesimal & Bounded) * Unbounded -> Unbounded
+ Bounded * Unbounded -> ?
+ """
+ _output = True
+ for arg in self.expr.args:
+ if not query(arg, bounded=True, assumptions=self.assumptions):
+ if not query(arg, infinitesimal=True, assumptions=self.assumptions):
+ if _output:
+ _output = False
+ else:
+ return
+ else:
+ return
+ return _output
+
+ def Number(self):
+ return True
+
+ def Infinity(self):
+ return False
+
+ def NegativeInfinity(self):
+ return False
+
+ def Pi(self):
+ return True
+
+ def Exp1(self):
+ return True
+
+ def ImaginaryUnit(self):
+ return True
+
+
+class QueryUnboundedHandler(CommonHandler):
+ def __init__(self, expr, key, assumptions=None):
+ CommonHandler.__init__(self, expr, key, assumptions)
+ self.resolution = query(expr, bounded=False, extended_real=True, \
+ assumptions=assumptions)
+
+class QueryFiniteHandler(CommonHandler):
+
+ def Mul(self):
+ for arg in self.expr.args:
+ _result = query(arg, key=self.key, assumptions=self.assumptions)
+ if not _result:
+ return _result
+ return True
+
+ Add = Mul
+
+ def Number(self):
+ return True
+
+ def Infinity(self):
+ return False
+
+ def NegativeInfinity(self):
+ return False
+
+ def NumberSymbol(self):
+ return True
+
+ def ImaginaryUnit(self):
+ return True
diff --git a/sympy/query/handlers/ntheory.py b/sympy/query/handlers/ntheory.py
new file mode 100644
index 0000000..8a46a14
--- /dev/null
+++ b/sympy/query/handlers/ntheory.py
@@ -0,0 +1,114 @@
+from sympy.query import query
+from sympy.query.handlers import CommonHandler
+from sympy.ntheory import isprime
+from sympy.core import Symbol
+
+class QueryPrimeHandler(CommonHandler):
+
+ def Add(self):
+ if len((self.expr).atoms(Symbol)) == 0:
+ if (self.expr.evalf(1) - self.expr.evalf()) == 0:
+ return isprime(int(self.expr.evalf())) == 0
+ return False
+
+ Mul = Add
+
+ def Integer(self):
+ return isprime(self.expr)
+
+ def Rational(self):
+ return False
+
+ def Real(self):
+ if (int(self.expr) - self.expr).evalf() == 0:
+ return isprime(int(self.expr))
+ return False
+
+ def Infinity(self):
+ return False
+
+ def NegativeInfinity(self):
+ return False
+
+ def ImaginaryUnit(self):
+ return False
+
+ def NumberSymbol(self):
+ if (self.expr - self.expr.evalf(1)) == 0:
+ return isprime(int(self.expr.evalf(1)))
+ return False
+
+class QueryCompositeHandler(CommonHandler):
+ def __init__(self, expr, key, assumptions):
+ CommonHandler.__init__(self, expr, key, assumptions)
+ self.resolution = query(expr, positive=True, integer=True, prime=False, \
+ assumptions=assumptions)
+
+
+class QueryEvenHandler(CommonHandler):
+ def Mul(self):
+ """
+ Even*Integer -> Even
+ """
+ _result = None
+ for arg in self.expr.args:
+ if query(arg, integer=True, assumptions=self.assumptions):
+ if query(arg, even=True, assumptions=self.assumptions):
+ _result = True #one even is enough
+ else:
+ if query(arg, irrational=True, assumptions=self.assumptions):
+ #TODO: could this have any counter-example ?
+ return False
+ return None
+ return _result
+
+ def Add(self):
+ """
+ Even + Odd -> Odd
+ Even + Even -> Even
+ """
+ if len((self.expr).atoms(Symbol)) == 0:
+ if (int(self.expr.evalf()) - self.expr.evalf()) == 0:
+ return self.expr.evalf() % 2 == 0
+ return False
+ _result = True
+ for arg in self.expr.args:
+ if query(arg, even=True, assumptions=self.assumptions):
+ _result = not (True ^ _result)
+ elif query(arg, odd=True, assumptions=self.assumptions):
+ _result = not (False ^ _result)
+ else:
+ return None
+ return _result
+
+ def Integer(self):
+ return self.expr % 2 == 0
+
+ def Rational(self):
+ return False
+
+ def Real(self):
+ if (self.expr - int(self.expr)).evalf() == 0 :
+ return int(self.expr) % 2 == 0
+ else:
+ return False
+
+ def Infinity(self):
+ return False
+
+ def NegativeInfinity(self):
+ return False
+
+ def NumberSymbol(self):
+ if query(self.expr, integer=True):
+ return query(int(self.expr), even=True)
+ return False
+
+ def ImaginaryUnit(self):
+ return False
+
+class QueryOddHandler(CommonHandler):
+ def __init__(self, expr, key, assumptions):
+ CommonHandler.__init__(self, expr, key, assumptions)
+ self.resolution = query(expr, integer=True, even=False, \
+ assumptions=assumptions)
diff --git a/sympy/query/handlers/order.py b/sympy/query/handlers/order.py
new file mode 100644
index 0000000..33affbd
--- /dev/null
+++ b/sympy/query/handlers/order.py
@@ -0,0 +1,156 @@
+from sympy.core import Symbol
+from sympy.query import query
+from sympy.query.handlers import CommonHandler
+
+
+class QueryNegativeHandler(CommonHandler):
+ """http://en.wikipedia.org/wiki/Negative_number"""
+
+ def __init__(self, expr, key, assumptions=None):
+ CommonHandler.__init__(self, expr, key, assumptions)
+ if len(self.expr.atoms(Symbol)) == 0 and query(expr, comparable=True):
+ # if there are no symbols just evalf
+ self.resolution = self.expr.evalf() < 0
+
+ def Mul(self):
+ _nonpositives = 0
+ for arg in self.expr.args:
+ _result = query(arg, nonpositive=True, assumptions=self.assumptions)
+ if _result == True:
+ _nonpositives += 1
+ elif _result is None:
+ return
+ if _nonpositives % 2 == 0:
+ # we don't care about zero
+ return False
+ else:
+ if query(self.expr, zero=True, assumptions=self.assumptions) == False:
+ return True
+ else:
+ return None
+
+ def Add(self):
+ """
+ Positive + Positive -> Positive,
+ Negative + Negative -> Negative
+ """
+ for arg in self.expr.args:
+ if query(arg, negative=True, assumptions=self.assumptions) != True:
+ break
+ else:
+ # if all argument's are positive
+ return True
+
+ def Power(self):
+ if query(self.expr.base, negative=True, assumptions=self.assumptions):
+ if query(self.expr.exp, odd=True, assumptions=self.assumptions):
+ return True
+ if query(self.expr.exp, even=True, assumptions=self.assumptions):
+ return False
+ elif query(self.expr.base, positive=True):
+ if query(self.expr.exp, real=True):
+ return False
+ return None
+
+ def ImaginaryUnit(self):
+ return False
+
+ def abs(self):
+ return False
+
+class QueryNonNegativeHandler(CommonHandler):
+ def __init__(self, expr, key, assumptions=None):
+ CommonHandler.__init__(self, expr, key, assumptions)
+ self.resolution = query(expr, extended_real=True, negative=False, \
+ assumptions=assumptions)
+
+class QueryZeroHandler(CommonHandler):
+ def __init__(self, expr, key, assumptions=None):
+ CommonHandler.__init__(self, expr, key, assumptions)
+ if len(expr.atoms(Symbol)) == 0 and query(expr, comparable=True, assumptions=assumptions):
+ # if there are no symbols just evalf
+ self.resolution = expr.evalf() == 0
+
+ def Add(self):
+ if all([query(x, positive=True, assumptions=self.assumptions) for x in self.expr.args]) \
+ or all([query(x, negative=True, assumptions=self.assumptions) for x in self.expr.args]):
+ return True
+
+ def Mul(self):
+ for arg in self.expr.args:
+ result = query(arg, zero=True, assumptions=self.assumptions)
+ if result == True:
+ return True
+ elif result is None:
+ return None
+ else:
+ return False
+
+ def Pow(self):
+ if query(self.expr.exp, zero=True, assumptions=self.assumptions) == False:
+ return query(self.expr.base, zero=True, assumptions=self.assumptions)
+
+class QueryNonZeroHandler(CommonHandler):
+ pass
+
+class QueryPositiveHandler(CommonHandler):
+
+ def __init__(self, expr, key, assumptions=None):
+ CommonHandler.__init__(self, expr, key, assumptions)
+ if len(self.expr.atoms(Symbol)) == 0 and query(expr, comparable=True):
+ # if there are no symbols just evalf
+ self.resolution = self.expr.evalf() > 0
+
+ def Mul(self):
+ _result = True
+ parity = 0
+ for arg in self.expr.args:
+ _result = query(arg, positive=True, assumptions=self.assumptions)
+ if _result == False:
+ _is_zero = query(arg, zero=True, assumptions=self.assumptions)
+ if _is_zero or (_is_zero is None):
+ # if this is True or None
+ return None
+ parity += 1
+ elif _result is None:
+ return None
+ return parity % 2 == 0
+
+ def Add(self):
+ for arg in self.expr.args:
+ if query(arg, positive=True, assumptions=self.assumptions) != True:
+ break
+ else:
+ # if all argument's are positive
+ return True
+
+ def Power(self):
+ if query(self.expr.base, positive=True, assumptions=self.assumptions):
+ if query(self.expr.exp, odd=True, assumptions=self.assumptions):
+ return False
+ if query(self.expr.exp, even=True, assumptions=self.assumptions):
+ return False
+ elif query(self.expr.base, positive=True):
+ if query(self.expr.exp, real=True):
+ return True
+ return None
+
+ def abs(self):
+ return True
+
+ def exp(self):
+ if query(self.expr.args[0], real=True, assumptions=self.assumptions):
+ return True
+
+ def ImaginaryUnit(self):
+ return False
+
+class QueryNonPositiveHandler(CommonHandler):
+ def __init__(self, expr, key, assumptions=None):
+ CommonHandler.__init__(self, expr, key, assumptions)
+ if self.resolution is not None: return
+ self.resolution = query(expr, extended_real=True, positive=False, \
+ assumptions=assumptions)
+ def Add(self):
+ if all([query(x, nonpositive=True, assumptions=self.assumptions) for x in self.expr.args]):
+ return True
diff --git a/sympy/query/handlers/sets.py b/sympy/query/handlers/sets.py
new file mode 100644
index 0000000..19d7919
--- /dev/null
+++ b/sympy/query/handlers/sets.py
@@ -0,0 +1,255 @@
+from sympy.query import query
+from sympy.query.handlers import CommonHandler
+
+class QueryIntegerHandler(CommonHandler):
+ def Add(self):
+ """
+ Integer + Integer -> Integer
+ NonInteger + Integer -> Noninteger
+ NonInteger + NonInteger -> ?
+ """
+ _output = True
+ for arg in self.expr.args:
+ _result = query(arg, integer=True, assumptions=self.assumptions)
+ if _result is None:
+ return
+ elif _result is False:
+ if _output:
+ _output = False
+ else:
+ return
+ else:
+ return _output
+
+ def Mul(self):
+ """
+ Integer*Integer -> Integer
+ Integer*Irrational -> NonInteger
+ Integer*Rational -> ?
+ """
+ _output = True
+ for arg in self.expr.args:
+ if not query(arg, integer=True, assumptions=self.assumptions):
+ if query(arg, irrational=True, assumptions=self.assumptions):
+ if _output:
+ _output = False
+ else:
+ return
+ else:
+ return
+ else:
+ return _output
+
+ def Pow(self):
+ for arg in self.expr.args:
+ if not query(arg, integer=True, assumptions=self.assumptions):
+ return
+ else:
+ return True
+
+ def int(self):
+ return True
+
+ def Integer(self):
+ return True
+
+ def Rational(self):
+ # rationals with denominator one get
+ # evaluated to Integers
+ return False
+
+ def Real(self):
+ return int(self.expr) == self.expr
+
+ def Pi(self):
+ return False
+
+ def Exp1(self):
+ return False
+
+ def Infinity(self):
+ return False
+
+ def NegativeInfinity(self):
+ return False
+
+ def ImaginaryUnit(self):
+ return False
+
+
+class QueryNonIntegerHandler(CommonHandler):
+ def __init__(self, expr, key, assumptions):
+ CommonHandler.__init__(self, expr, key, assumptions)
+ self.resolution = query(expr, real=True, integer=False, \
+ assumptions=assumptions)
+
+class QueryRationalHandler(CommonHandler):
+
+ def Add(self):
+ """
+ Rational + Rational -> Integer
+ Irrational + Rational -> Rational
+ Irrational + Irrational -> ?
+ """
+ _output = True
+ for arg in self.expr.args:
+ _result = query(arg, rational=True, assumptions=self.assumptions)
+ if _result is None:
+ return
+ elif _result is False:
+ if _output:
+ _output = False
+ else:
+ return
+ else:
+ return _output
+
+ def Mul(self):
+ """
+ Rational*Rational -> Rational
+ Rational*Irrational -> Irrational
+ Irrational*Irrational -> ?
+ """
+ _output = True
+ for arg in self.expr.args:
+ _result = query(arg, rational=True, assumptions=self.assumptions)
+ if _result is None:
+ return
+ elif _result is False:
+ if _output:
+ _output = False
+ else:
+ return
+ else:
+ return _output
+
+ def Rational(self):
+ return True
+
+ def Real(self):
+ # it's finite-precission
+ return True
+
+ def ImaginaryUnit(self):
+ return False
+
+ def Infinity(self):
+ return False
+
+ def NegativeInfinity(self):
+ return False
+
+ def Pi(self):
+ return False
+
+ def Exp1(self):
+ return False
+
+class QueryIrrationalHandler(CommonHandler):
+
+ def __init__(self, expr, key, assumptions):
+ CommonHandler.__init__(self, expr, key, assumptions)
+ self.resolution = query(expr, real=True, rational=False, \
+ assumptions=assumptions)
+
+class QueryRealHandler(CommonHandler):
+ def Add(self):
+ for arg in self.expr.args:
+ if query(arg, real=True, assumptions=self.assumptions) != True:
+ break
+ else:
+ return True
+
+ def Mul(self):
+ for arg in self.expr.args:
+ if query(arg, real=True, assumptions=self.assumptions) != True:
+ break
+ else:
+ return True
+
+ def Rational(self):
+ return True
+
+ def Real(self):
+ return True
+
+ def Pi(self):
+ return True
+
+ def Exp1(self):
+ return True
+
+ def abs(self):
+ return True
+
+ def ImaginaryUnit(self):
+ return False
+
+ def Infinity(self):
+ return False
+
+ def NegativeInfinity(self):
+ return False
+
+ def sin(self):
+ if query(self.expr.args[0], real=True, assumptions=self.assumptions):
+ return True
+ cos = sin
+
+class QueryExtendedRealHandler(QueryRealHandler):
+
+ def Infinity(self):
+ return True
+
+ def NegativeInfinity(self):
+ return True
+
+class QueryComplexHandler(CommonHandler):
+
+ def Add(self):
+ for arg in self.expr.args:
+ if not query(arg, real=True, assumptions=self.assumptions):
+ return None
+ else:
+ return True
+
+ Mul = Add
+
+ def Number(self):
+ return True
+
+ def NumberSymbol(self):
+ return True
+
+ def abs(self):
+ return True
+
+ def ImaginaryUnit(self):
+ return True
+
+ def Infinity(self):
+ return False
+
+ def NegativeInfinity(self):
+ return False
+
+class QueryImaginaryHandler(CommonHandler):
+
+ def Add(self):
+ for arg in self.expr.args:
+ if query(arg, complex=True, real=False, assumptions=self.assumptions) == False:
+ return False
+ else:
+ return True
+
+ Mul = Add
+
+ def Number(self):
+ return not (self.expr.as_real_imag()[1] == 0)
+
+ NumberSymbol = Number
+
+ def ImaginaryUnit(self):
+ return True
+
+
diff --git a/sympy/query/tests/test_query.py b/sympy/query/tests/test_query.py
new file mode 100644
index 0000000..ed56e28
--- /dev/null
+++ b/sympy/query/tests/test_query.py
@@ -0,0 +1,606 @@
+from sympy.core import Symbol, S, Rational, Integer
+from sympy.assumptions import Assume
+from sympy.query import query
+
+def test_integer():
+ z = 1
+ assert query(z, commutative=True) == True
+ assert query(z, integer=True) == True
+ assert query(z, rational=True) == True
+ assert query(z, real=True) == True
+ assert query(z, complex=True) == True
+ assert query(z, noninteger=True) == False
+ assert query(z, irrational=True) == False
+ assert query(z, imaginary=True) == False
+ assert query(z, positive=True) == True
+ assert query(z, negative=True) == False
+ assert query(z, nonpositive=True) == False
+ assert query(z, nonnegative=True) == True
+ assert query(z, even=True) == False
+ assert query(z, odd=True) == True
+ assert query(z, bounded=True) == True
+ assert query(z, unbounded=True) == False
+ assert query(z, finite=True) == True
+ assert query(z, infinitesimal=True) == False
+ assert query(z, comparable=True) == True
+ assert query(z, prime=True) == False
+ assert query(z, composite=True) == True
+
+def test_float():
+ z = 1.0
+ assert query(z, commutative=True) == True
+ assert query(z, integer=True) == True
+ assert query(z, rational=True) == True
+ assert query(z, real=True) == True
+ assert query(z, complex=True) == True
+ assert query(z, noninteger=True) == False
+ assert query(z, irrational=True) == False
+ assert query(z, imaginary=True) == False
+ assert query(z, positive=True) == True
+ assert query(z, negative=True) == False
+ assert query(z, nonpositive=True) == False
+ assert query(z, nonnegative=True) == True
+ assert query(z, even=True) == False
+ assert query(z, odd=True) == True
+ assert query(z, bounded=True) == True
+ assert query(z, unbounded=True) == False
+ assert query(z, finite=True) == True
+ assert query(z, infinitesimal=True) == False
+ assert query(z, comparable=True) == True
+ assert query(z, prime=True) == False
+ assert query(z, composite=True) == True
+
+def test_zero():
+ z = Integer(0)
+ assert query(z, zero=True) == True
+ assert query(z, commutative=True) == True
+ assert query(z, integer=True) == True
+ assert query(z, rational=True) == True
+ assert query(z, real=True) == True
+ assert query(z, complex=True) == True
+ assert query(z, imaginary=True) == False
+ assert query(z, positive=True) == False
+ assert query(z, negative=True) == False
+ assert query(z, even=True) == True
+ assert query(z, odd=True) == False
+ assert query(z, bounded=True) == True
+ assert query(z, finite=True) == True
+ assert query(z, infinitesimal=True) == True
+ assert query(z, comparable=True) == True
+ assert query(z, prime=True) == False
+ assert query(z, composite=True) == False
+
+def test_one():
+ z = Integer(1)
+ assert query(z, commutative=True) == True
+ assert query(z, integer=True) == True
+ assert query(z, rational=True) == True
+ assert query(z, real=True) == True
+ assert query(z, complex=True) == True
+ assert query(z, noninteger=True) == False
+ assert query(z, irrational=True) == False
+ assert query(z, imaginary=True) == False
+ assert query(z, positive=True) == True
+ assert query(z, negative=True) == False
+ assert query(z, nonpositive=True) == False
+ assert query(z, nonnegative=True) == True
+ assert query(z, even=True) == False
+ assert query(z, odd=True) == True
+ assert query(z, bounded=True) == True
+ assert query(z, unbounded=True) == False
+ assert query(z, finite=True) == True
+ assert query(z, infinitesimal=True) == False
+ assert query(z, comparable=True) == True
+ assert query(z, prime=True) == False
+ assert query(z, composite=True) == True
+
+def test_negativeone():
+ z = Integer(-1)
+ assert query(z, commutative=True) == True
+ assert query(z, integer=True) == True
+ assert query(z, rational=True) == True
+ assert query(z, real=True) == True
+ assert query(z, complex=True) == True
+ assert query(z, noninteger=True) == False
+ assert query(z, irrational=True) == False
+ assert query(z, imaginary=True) == False
+ assert query(z, positive=True) == False
+ assert query(z, negative=True) == True
+ assert query(z, nonpositive=True) == True
+ assert query(z, nonnegative=True) == False
+ assert query(z, even=True) == False
+ assert query(z, odd=True) == True
+ assert query(z, bounded=True) == True
+ assert query(z, unbounded=True) == False
+ assert query(z, finite=True) == True
+ assert query(z, infinitesimal=True) == False
+ assert query(z, comparable=True) == True
+ assert query(z, prime=True) == False
+ assert query(z, composite=True) == False
+
+def test_infinity():
+ oo = S.Infinity
+
+ assert query(oo, commutative=True) == True
+ assert query(oo, integer=True) == False
+ assert query(oo, rational=True) == False
+ assert query(oo, real=True) == False
+ assert query(oo, extended_real=True) == True
+ assert query(oo, complex=True) == False
+ assert query(oo, noninteger=True) == False
+ assert query(oo, irrational=True) == False
+ assert query(oo, imaginary=True) == False
+ assert query(oo, positive=True) == True
+ assert query(oo, negative=True) == False
+ assert query(oo, nonpositive=True) == False
+ assert query(oo, nonnegative=True) == True
+ assert query(oo, even=True) == False
+ assert query(oo, odd=True) == False
+ assert query(oo, bounded=True) == False
+ assert query(oo, unbounded=True) == True
+ assert query(oo, finite=True) == False
+ assert query(oo, infinitesimal=True) == False
+ assert query(oo, comparable=True) == True
+ assert query(oo, prime=True) == False
+ assert query(oo, composite=True) == False
+
+def test_neg_infinity():
+ mm = S.NegativeInfinity
+
+ assert query(mm, commutative=True) == True
+ assert query(mm, integer=True) == False
+ assert query(mm, rational=True) == False
+ assert query(mm, real=True) == False
+ assert query(mm, extended_real=True) == True
+ assert query(mm, complex=True) == False
+ assert query(mm, noninteger=True) == False
+ assert query(mm, irrational=True) == False
+ assert query(mm, imaginary=True) == False
+ assert query(mm, positive=True) == False
+ assert query(mm, negative=True) == True
+ assert query(mm, nonpositive=True) == True
+ assert query(mm, nonnegative=True) == False
+ assert query(mm, even=True) == False
+ assert query(mm, odd=True) == False
+ assert query(mm, bounded=True) == False
+ assert query(mm, unbounded=True) == True
+ assert query(mm, finite=True) == False
+ assert query(mm, infinitesimal=True) == False
+ assert query(mm, comparable=True) == True
+ assert query(mm, prime=True) == False
+ assert query(mm, composite=True) == False
+
+def test_nan():
+ nan = S.NaN
+
+ assert query(nan, commutative=True) == True
+ assert query(nan, integer=True) == False
+ assert query(nan, rational=True) == False
+ assert query(nan, real=True) == False
+ assert query(nan, extended_real=True) == False
+ assert query(nan, complex=True) == False
+ assert query(nan, noninteger=True) == False
+ assert query(nan, irrational=True) == False
+ assert query(nan, imaginary=True) == False
+ assert query(nan, positive=True) == False
+ assert query(nan, negative=True) == False
+ assert query(nan, nonpositive=True) == False
+ assert query(nan, zero=True) == False
+ assert query(nan, nonnegative=True) == False
+ assert query(nan, even=True) == False
+ assert query(nan, odd=True) == False
+ assert query(nan, bounded=True) == False
+ assert query(nan, unbounded=True) == False
+ assert query(nan, finite=True) == False
+ assert query(nan, infinitesimal=True) == False
+ assert query(nan, comparable=True) == False
+ assert query(nan, prime=True) == False
+ assert query(nan, composite=True) == False
+
+def test_pos_rational():
+ r = Rational(3,4)
+ assert query(r, commutative=True) == True
+ assert query(r, integer=True) == False
+ assert query(r, rational=True) == True
+ assert query(r, real=True) == True
+ assert query(r, complex=True) == True
+ assert query(r, noninteger=True) == True
+ assert query(r, irrational=True) == False
+ assert query(r, imaginary=True) == False
+ assert query(r, positive=True) == True
+ assert query(r, negative=True) == False
+ assert query(r, nonpositive=True) == False
+ assert query(r, nonnegative=True) == True
+ assert query(r, even=True) == False
+ assert query(r, odd=True) == False
+ assert query(r, bounded=True) == True
+ assert query(r, unbounded=True) == False
+ assert query(r, finite=True) == True
+ assert query(r, infinitesimal=True) == False
+ assert query(r, comparable=True) == True
+ assert query(r, prime=True) == False
+ assert query(r, composite=True) == False
+
+ r = Rational(1,4)
+ assert query(r, nonpositive=True) == False
+ assert query(r, positive=True) == True
+ assert query(r, negative=True) == False
+ assert query(r, nonnegative=True) == True
+
+ r = Rational(5,4)
+ assert query(r, negative=True) == False
+ assert query(r, positive=True) == True
+ assert query(r, nonpositive=True) == False
+ assert query(r, nonnegative=True) == True
+
+ r = Rational(5,3)
+ assert query(r, nonnegative=True) == True
+ assert query(r, positive=True) == True
+ assert query(r, negative=True) == False
+ assert query(r, nonpositive=True) == False
+
+def test_neg_rational():
+ r = Rational(-3,4)
+ assert query(r, positive=True) == False
+ assert query(r, nonpositive=True) == True
+ assert query(r, negative=True) == True
+ assert query(r, nonnegative=True) == False
+
+ r = Rational(-1,4)
+ assert query(r, nonpositive=True) == True
+ assert query(r, positive=True) == False
+ assert query(r, negative=True) == True
+ assert query(r, nonnegative=True) == False
+
+ r = Rational(-5,4)
+ assert query(r, negative=True) == True
+ assert query(r, positive=True) == False
+ assert query(r, nonpositive=True) == True
+ assert query(r, nonnegative=True) == False
+
+ r = Rational(-5,3)
+ assert query(r, nonnegative=True) == False
+ assert query(r, positive=True) == False
+ assert query(r, negative=True) == True
+ assert query(r, nonpositive=True) == True
+
+def test_pi():
+ z = S.Pi
+ assert query(z, commutative=True) == True
+ assert query(z, integer=True) == False
+ assert query(z, rational=True) == False
+ assert query(z, real=True) == True
+ assert query(z, complex=True) == True
+ assert query(z, noninteger=True) == True
+ assert query(z, irrational=True) == True
+ assert query(z, imaginary=True) == False
+ assert query(z, positive=True) == True
+ assert query(z, negative=True) == False
+ assert query(z, nonpositive=True) == False
+ assert query(z, nonnegative=True) == True
+ assert query(z, even=True) == False
+ assert query(z, odd=True) == False
+ assert query(z, bounded=True) == True
+ assert query(z, unbounded=True) == False
+ assert query(z, finite=True) == True
+ assert query(z, infinitesimal=True) == False
+ assert query(z, comparable=True) == True
+ assert query(z, prime=True) == False
+ assert query(z, composite=True) == False
+
+def test_pi_add():
+ z = S.Pi + 1
+ assert query(z, commutative=True) == True
+ assert query(z, integer=True) == False
+ assert query(z, rational=True) == False
+ assert query(z, real=True) == True
+ assert query(z, complex=True) == True
+ assert query(z, noninteger=True) == True
+ assert query(z, irrational=True) == True
+ assert query(z, imaginary=True) == False
+ assert query(z, positive=True) == True
+ assert query(z, negative=True) == False
+ assert query(z, nonpositive=True) == False
+ assert query(z, nonnegative=True) == True
+ assert query(z, even=True) == False
+ assert query(z, odd=True) == False
+ assert query(z, bounded=True) == True
+ assert query(z, unbounded=True) == False
+ assert query(z, finite=True) == True
+ assert query(z, infinitesimal=True) == False
+ assert query(z, comparable=True) == True
+ assert query(z, prime=True) == False
+ assert query(z, composite=True) == False
+
+def test_pi_mul():
+ z = 2*S.Pi
+ assert query(z, commutative=True) == True
+ assert query(z, integer=True) == False
+ assert query(z, rational=True) == False
+ assert query(z, real=True) == True
+ assert query(z, complex=True) == True
+ assert query(z, noninteger=True) == True
+ assert query(z, irrational=True) == True
+ assert query(z, imaginary=True) == False
+ assert query(z, positive=True) == True
+ assert query(z, negative=True) == False
+ assert query(z, nonpositive=True) == False
+ assert query(z, nonnegative=True) == True
+ assert query(z, even=True) == False
+ assert query(z, odd=True) == False
+ assert query(z, bounded=True) == True
+ assert query(z, unbounded=True) == False
+ assert query(z, finite=True) == True
+ assert query(z, infinitesimal=True) == False
+ assert query(z, comparable=True) == True
+ assert query(z, prime=True) == False
+ assert query(z, composite=True) == False
+
+def test_E():
+ z = S.Exp1
+ assert query(z, commutative=True) == True
+ assert query(z, integer=True) == False
+ assert query(z, rational=True) == False
+ assert query(z, real=True) == True
+ assert query(z, complex=True) == True
+ assert query(z, noninteger=True) == True
+ assert query(z, irrational=True) == True
+ assert query(z, imaginary=True) == False
+ assert query(z, positive=True) == True
+ assert query(z, negative=True) == False
+ assert query(z, nonpositive=True) == False
+ assert query(z, nonnegative=True) == True
+ assert query(z, even=True) == False
+ assert query(z, odd=True) == False
+ assert query(z, bounded=True) == True
+ assert query(z, unbounded=True) == False
+ assert query(z, finite=True) == True
+ assert query(z, infinitesimal=True) == False
+ assert query(z, comparable=True) == True
+ assert query(z, prime=True) == False
+ assert query(z, composite=True) == False
+
+def test_I():
+ z = S.ImaginaryUnit
+ assert query(z, comparable=True) == False
+ assert query(z, commutative=True) == True
+ assert query(z, integer=True) == False
+ assert query(z, rational=True) == False
+ assert query(z, real=True) == False
+ assert query(z, complex=True) == True
+ assert query(z, noninteger=True) == False
+ assert query(z, irrational=True) == False
+ assert query(z, imaginary=True) == True
+ assert query(z, positive=True) == False
+ assert query(z, negative=True) == False
+ assert query(z, nonpositive=True) == False
+ assert query(z, nonnegative=True) == False
+ assert query(z, even=True) == False
+ assert query(z, odd=True) == False
+ assert query(z, bounded=True) == True
+ assert query(z, unbounded=True) == False
+ assert query(z, finite=True) == True
+ assert query(z, infinitesimal=True) == False
+ assert query(z, prime=True) == False
+ assert query(z, composite=True) == False
+
+def test_symbol_zero():
+ x = Symbol('x')
+ assumptions = Assume(x, zero=True)
+ assert query(x, zero=True, assumptions=assumptions) == True
+ assert query(x, nonpositive=True, assumptions=assumptions) == True
+ assert query(x, negative=True, assumptions=assumptions) == False
+ assert query(x, nonnegative=True, assumptions=assumptions) == True
+ assert query(x, zero=True, assumptions=assumptions) == True
+ assert query(x, nonzero=True, assumptions=assumptions) == False
+
+def test_symbol_complex():
+ x = Symbol('x')
+ assert query(x, complex=True, assumptions=Assume(x, real=True)) == True
+
+def test_symbol_positive():
+ x = Symbol('x')
+ assumptions = Assume(x, positive=True)
+ assert query( x, positive=True, assumptions=assumptions) == True
+ assert query( x, nonpositive=True, assumptions=assumptions) == False
+ assert query( x, negative=True, assumptions=assumptions) == False
+ assert query( x, nonnegative=True, assumptions=assumptions) == True
+ assert query( x, zero=True, assumptions=assumptions) == False
+ assert query( x, nonzero=True, assumptions=assumptions) == True
+
+ #test -x
+ assert query(-x, positive=True, assumptions=assumptions) == False
+ assert query(-x, nonpositive=True, assumptions=assumptions) == True
+ assert query(-x, negative=True, assumptions=assumptions) == True
+ assert query(-x, nonnegative=True, assumptions=assumptions) == False
+ assert query(-x, zero=True, assumptions=assumptions) == False
+
+def test_symbol_positive_multiple():
+ #test with multiple symbols
+ x, y, z, w = Symbol('x'), Symbol('y'), Symbol('z'), Symbol('w')
+ assumptions = [ Assume(x, positive=True),
+ Assume(y, negative=True),
+ Assume(z, negative=True),
+ Assume(w, positive=True)]
+ assert query( x*y*z, positive=True) == None
+ assert query( x*y*z, positive=True, assumptions=assumptions) == True
+ assert query(-x*y*z, positive=True, assumptions=assumptions) == False
+ assert query( y+z, zero =True, assumptions=assumptions) == True
+ assert query( y+z, negative=True, assumptions=assumptions) == True
+ assert query( y+z, nonpositive=True, assumptions=assumptions) == True
+ assert query( x+y, positive=True, assumptions=assumptions) == None
+ assert query( x+y, negative=True, assumptions=assumptions) == None
+
+def test_symbol_nonpositive():
+ x = Symbol('x')
+ assumptions = Assume(x, nonpositive=True)
+ assert query(x, nonpositive=True) == None
+ assert query(x, positive=True, assumptions=assumptions) == False
+ assert query(x, nonpositive=True, assumptions=assumptions) == True
+ assert query(x, negative=True, assumptions=assumptions) == None
+ assert query(x, nonnegative=True, assumptions=assumptions) == None
+ assert query(x, zero=True, assumptions=assumptions) == None
+ assert query(x, nonzero=True, assumptions=assumptions) == None
+
+def test_neg__symbol_nonpositive():
+ x = Symbol('x')
+ assumptions = Assume(x, nonpositive=True)
+ assert query(-x, positive=True, assumptions=assumptions) == None
+ assert query(-x, nonpositive=True, assumptions=assumptions) == None
+ assert query(-x, negative=True, assumptions=assumptions) == False
+ assert query(-x, nonnegative=True, assumptions=assumptions) == True
+ assert query(-x, zero=True, assumptions=assumptions) == None
+ assert query(-x, nonzero=True, assumptions=assumptions) == None
+
+def test_symbol_negative():
+ x = Symbol('x')
+ y = Symbol('y')
+ assert query(x, negative=True, assumptions=Assume(x, negative=True)) == True
+ assert query(x, negative=True, assumptions=Assume(x, positive=True)) == False
+ assert query(x+y, negative=True, assumptions=[Assume(x, negative=True), Assume(y, negative=True)]) == True
+
+def test_prime_symbol():
+ x = Symbol('x')
+ assumptions = Assume(x, prime=True)
+ assert query(x, prime=True, assumptions=assumptions) == True
+ assert query(x, integer=True, assumptions=assumptions) == True
+ assert query(x, positive=True, assumptions=assumptions) == True
+ assert query(x, negative=True, assumptions=assumptions) == False
+ assert query(x, nonpositive=True, assumptions=assumptions) == False
+ assert query(x, nonnegative=True, assumptions=assumptions) == True
+
+def test_not_prime_symbol():
+ # assumptions with False bool_key are not implemented
+ x = Symbol('x')
+ assumptions = Assume(x, prime=False)
+ assert query(x, prime=True, assumptions=assumptions) == False
+ assert query(x, integer=True, assumptions=assumptions) == None
+ assert query(x, positive=True, assumptions=assumptions) == None
+ assert query(x, negative=True, assumptions=assumptions) == None
+ assert query(x, nonpositive=True, assumptions=assumptions) == None
+ assert query(x, nonnegative=True, assumptions=assumptions) == None
+
+def test_symbol_integer():
+ x = Symbol('x')
+ assumptions = Assume(x, integer=True)
+ assert query(x, integer=True, assumptions=assumptions) == True
+ assert query(x, real=True, assumptions=assumptions) == True
+ assert query(x, complex=True, assumptions=assumptions) == True
+ assert query(2*x, integer=True, assumptions=assumptions) == True
+ assert query(2*x, odd=True, assumptions=assumptions) == False
+ assert query(2*x, even=True, assumptions=assumptions) == True
+ assert query(2*x+1, odd=True, assumptions=assumptions) == True
+ assert query(2*x+1, even=True, assumptions=assumptions) == False
+ assert query(x**2, integer=True, assumptions=assumptions) == True
+ assert query(x**x, integer=True, assumptions=assumptions) == True
+
+def test_symbol_integer_nonnegative():
+ x = Symbol('x')
+ assumptions = [Assume(x, integer=True), Assume(x, nonnegative=True)]
+ assert query(x, integer=True, assumptions=assumptions) == True
+ assert query(x, nonnegative=True, assumptions=assumptions) == True
+ assert query(x, negative=True, assumptions=assumptions) == False
+ assert query(x, positive=True, assumptions=assumptions) == None
+
+def test_symbol_integer_nonpositive():
+ x = Symbol('x')
+ assumptions = [Assume(x, integer=True), Assume(x, nonpositive=True)]
+ assert query(x, integer=True, assumptions=assumptions) == True
+ assert query(x, nonpositive=True, assumptions=assumptions) == True
+ assert query(x, positive=True, assumptions=assumptions) == False
+ assert query(x, negative=True, assumptions=assumptions) == None
+
+def test_symbol_odd():
+ x = Symbol('x')
+ assumptions = Assume(x, odd=True)
+ assert query(x, odd=True, assumptions=assumptions) == True
+ assert query(x, even=True, assumptions=assumptions) == False
+ assert query(x, integer=True, assumptions=assumptions) == True
+
+ n = Symbol('n')
+ assumptions = [Assume(x, odd=True), Assume(n, integer=True)]
+ assert query(n*x, odd=True, assumptions=assumptions) == None
+
+def test_symbol_even():
+ x = Symbol('x')
+ assumptions = Assume(x, even=True)
+ assert query(x, even=True, assumptions=assumptions) == True
+ assert query(x, odd=True, assumptions=assumptions) == False
+ assert query(x, integer=True, assumptions=assumptions) == True
+
+ n = Symbol('n')
+ assumptions = [Assume(x, even=True), Assume(n, integer=True)]
+ assert query(n*x, even=True, assumptions=assumptions) == True
+
+def test_symbol_integer_nonnegative():
+ x = Symbol('x')
+ assumptions = [Assume(x, integer=True), Assume(x, nonnegative=True)]
+ assert query(x, integer=True, assumptions=assumptions) == True
+ assert query(x, nonnegative=True, assumptions=assumptions) == True
+
+def test_symbol_integer_nonpositive():
+ x = Symbol('x')
+ assumptions = [Assume(x, integer=True), Assume(x, nonpositive=True)]
+ assert query(x, integer=True, assumptions=assumptions) == True
+ assert query(x, nonpositive=True, assumptions=assumptions) == True
+
+def test_symbol_odd_False():
+ x = Symbol('x')
+ assumptions = Assume(x, odd=False)
+ assert query(x, odd=True, assumptions=assumptions) == False
+ assert query(x, even=True, assumptions=assumptions) == None
+ assert query(x, integer=True, assumptions=assumptions) == None
+
+def test_symbol_even_False():
+ x = Symbol('x')
+ assumptions = Assume(x, even=False)
+ assert query(x, even=True, assumptions=assumptions) == False
+ assert query(x, odd=True, assumptions=assumptions) == None
+ assert query(x, integer=True, assumptions=assumptions) == None
+
+def test_symbol_real_False():
+ a = Symbol('a')
+ assumptions = Assume(a, real=False)
+ assert query(a, real=True, assumptions=assumptions) == False
+ assert query(a, integer=True, assumptions=assumptions) == False
+ assert query(a, negative=True, assumptions=assumptions) == False
+ assert query(a, positive=True, assumptions=assumptions) == False
+ assert query(a, nonnegative=True, assumptions=assumptions) == False
+ assert query(a, nonpositive=True, assumptions=assumptions) == False
+ assert query(a, zero=True, assumptions=assumptions) == False
+
+def test_abs():
+ x = Symbol('x')
+ assert query(abs(x), positive=True) == True
+ assert query(abs(x), positive=True, assumptions=Assume(x, negative=True)) == True
+ assert query(abs(x), negative=True) == False
+ assert query(abs(x), real=True) == True
+ assert query(abs(x), complex=True) == True
+ assert query(abs(x), odd=True) == None
+
+def test_trigonometric():
+ from sympy.functions import sin, cos
+ x = Symbol('x')
+ assert query(sin(x), real=True) == None
+ assert query(cos(x), real=True) == None
+ assert query(sin(x), real=True, assumptions=Assume(x, real=True)) == True
+ assert query(cos(x), real=True, assumptions=Assume(x, real=True)) == True
+
+def test_x_exp():
+ from sympy.functions import exp
+ x = Symbol('x')
+ assert query(exp(x), positive=True, assumptions=Assume(x, real=True)) == True
+ assert query(x + exp(x), positive=True, assumptions=Assume(x, real=True)) == None
+
+def test_hash_vs_eq():
+ """catch: different hash for equal objects"""
+ a = 1 + S.Pi # important: do not fold it into a Number instance
+ ha= hash(a) # it should be Add/Mul/... to trigger the bug
+ b = a.expand(trig=True)
+ hb= hash(b)
+
+ assert query(a, positive=True) == True # this uses .evalf() and deduces it is positive
+ # be sure that hash stayed the same
+ assert a == b
+ assert ha == hash(a)
+ assert ha== hb
--
1.6.1.2
Fabian Pedregosa
extensively by the query module. The old logic module can be
removed once the old assumption system is removed.
Contents
--------
sympy.logic.boolalg
- Operators for boolean algebra on symbols {And: &, Or: |, Not: ~}
- some useful methods, mainly used to convert expressions to
conjunctive normal form (CNF)
sympy.logic.inference
- Rules for inference in propositional logic. Main method here is
satisfiable(expr), which checks satisfiability of a propositional
sentence (for now using dpll algorithm)
sympy.logic.kb
- Definition of a knowledge base
sympy.algorithms
- some algorithms used by higher order methods (just DPLL for now),
but in a future we should also have Quine-McCluskey for simplification
of boolean expressions
Most of the methods in this module are implementations of algorithms described
in the book "AI: A modern approach", http://aima.cs.berkeley.edu/
---
sympy/core/basic.py | 26 ++++++-
sympy/logic/__init__.py | 2 +
sympy/logic/algorithms/dpll.py | 49 +++++++++++
sympy/logic/boolalg.py | 155 +++++++++++++++++++++++++++++++++++
sympy/logic/inference.py | 119 +++++++++++++++++++++++++++
sympy/logic/kb.py | 36 ++++++++
sympy/logic/tests/test_boolalg.py | 110 +++++++++++++++++++++++++
sympy/logic/tests/test_inference.py | 46 ++++++++++
8 files changed, 541 insertions(+), 2 deletions(-)
create mode 100644 sympy/logic/__init__.py
create mode 100644 sympy/logic/algorithms/__init__.py
create mode 100644 sympy/logic/algorithms/dpll.py
create mode 100755 sympy/logic/boolalg.py
create mode 100755 sympy/logic/inference.py
create mode 100644 sympy/logic/kb.py
create mode 100755 sympy/logic/tests/test_boolalg.py
create mode 100755 sympy/logic/tests/test_inference.py
diff --git a/sympy/core/basic.py b/sympy/core/basic.py
index b48e633..6ab3101 100644
--- a/sympy/core/basic.py
+++ b/sympy/core/basic.py
@@ -680,8 +680,30 @@ def __rdiv__(self, other):
__truediv__ = __div__
__rtruediv__ = __rdiv__
-
-
+ # *******************
+ # * Logic operators *
+ # *******************
+
+ def __and__(self, other):
+ """Overloading for & operator"""
+ from sympy.logic.boolalg import And
+ return And(self, other)
+ def __or__(self, other):
+ """Overloading for |"""
+ from sympy.logic.boolalg import Or
+ return Or(self, other)
+ def __invert__(self):
+ """Overloading for ~"""
+ from sympy.logic.boolalg import Not
+ return Not(self)
+ def __rshift__(self, other):
+ """Overloading for >>"""
+ from sympy.logic.boolalg import Implies
+ return Implies(self, other)
+ def __lshift__(self, other):
+ """Overloading for <<"""
+ from sympy.logic.boolalg import Implies
+ return Implies(other, self)
def __repr__(self):
diff --git a/sympy/logic/__init__.py b/sympy/logic/__init__.py
new file mode 100644
index 0000000..5076249
--- /dev/null
+++ b/sympy/logic/__init__.py
@@ -0,0 +1,2 @@
+from boolalg import *
+from inference import *
\ No newline at end of file
diff --git a/sympy/logic/algorithms/__init__.py b/sympy/logic/algorithms/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/sympy/logic/algorithms/dpll.py b/sympy/logic/algorithms/dpll.py
new file mode 100644
index 0000000..77d92ed
--- /dev/null
+++ b/sympy/logic/algorithms/dpll.py
@@ -0,0 +1,49 @@
+from sympy.core import Symbol
+from sympy.logic.boolalg import conjuncts, to_cnf
+from sympy.logic.inference import find_pure_symbol, find_unit_clause, pl_true
+
+def dpll_satisfiable(expr):
+ """Check satisfiability of a propositional sentence.
+ It returns a model rather than True when it succeeds
+ >>> from sympy import symbols
+ >>> A, B = symbols('AB')
+ >>> dpll_satisfiable(A & ~B)
+ {A: True, B: False}
+ >>> dpll_satisfiable(A & ~A)
+ False
+
+ References: Implemented as described in http://aima.cs.berkeley.edu/
+ """
+ clauses = conjuncts(to_cnf(expr))
+ symbols = list(expr.atoms(Symbol))
+ return dpll(clauses, symbols, {})
+
+def dpll(clauses, symbols, model):
+ """See if the clauses are true in a partial model.
+ http://en.wikipedia.org/wiki/DPLL_algorithm
+ """
+ unknown_clauses = [] ## clauses with an unknown truth value
+ for c in clauses:
+ val = pl_true(c, model)
+ if val == False:
+ return False
+ if val != True:
+ unknown_clauses.append(c)
+ if not unknown_clauses:
+ return model
+ P, value = find_pure_symbol(symbols, unknown_clauses)
+ if P:
+ model.update({P: value})
+ syms = [x for x in symbols if x != P]
+ return dpll(clauses, syms, model)
+ P, value = find_unit_clause(clauses, model)
+ if P:
+ model.update({P: value})
+ syms = [x for x in symbols if x != P]
+ return dpll(clauses, syms, model)
+ P = symbols.pop()
+ model_1, model_2 = model.copy(), model.copy()
+ model_1.update({P: True})
+ model_2.update({P: False})
+ return (dpll(clauses, symbols, model_1) or
+ dpll(clauses, symbols, model_2))
\ No newline at end of file
diff --git a/sympy/logic/boolalg.py b/sympy/logic/boolalg.py
new file mode 100755
index 0000000..1a57740
--- /dev/null
+++ b/sympy/logic/boolalg.py
@@ -0,0 +1,155 @@
+"""Boolean algebra module for SymPy"""
+from sympy.core import Basic, Function, sympify, Symbol
+from sympy.utilities import flatten
+
+
+class BooleanFunction(Function):
+ """Boolean function is a function that lives in a boolean space
+ It is used as base class for And, Or, Not, etc.
+ """
+ pass
+
+class And(BooleanFunction):
+ """Evaluates to True if all it's arguments are True,
+ False otherwise"""
+ @classmethod
+ def eval(cls, *args):
+ if len(args) < 2: raise ValueError("And must have at least two arguments")
+ out_args = []
+ for i, arg in enumerate(args): # we iterate over a copy or args
+ if isinstance(arg, bool):
+ if not arg: return False
+ else: continue
+ out_args.append(arg)
+ if len(out_args) == 0: return True
+ if len(out_args) == 1: return out_args[0]
+ sargs = sorted(flatten(out_args, cls=cls))
+ return Basic.__new__(cls, *sargs)
+
+class Or(BooleanFunction):
+ @classmethod
+ def eval(cls, *args):
+ if len(args) < 2: raise ValueError("And must have at least two arguments")
+ out_args = []
+ for i, arg in enumerate(args): # we iterate over a copy or args
+ if isinstance(arg, bool):
+ if arg: return True
+ else: continue
+ out_args.append(arg)
+ if len(out_args) == 0: return False
+ if len(out_args) == 1: return out_args[0]
+ sargs = sorted(flatten(out_args, cls=cls))
+ return Basic.__new__(cls, *sargs)
+
+class Not(BooleanFunction):
+ """De Morgan rules applied automatically, so Not is moved inward"""
+ @classmethod
+ def eval(cls, *args):
+ if len(args) > 1:
+ return map(cls, args)
+ arg = args[0]
+ # apply De Morgan Rules
+ if isinstance(arg, And):
+ return Or( *[Not(a) for a in arg.args])
+ if isinstance(arg, Or):
+ return And(*[Not(a) for a in arg.args])
+ if isinstance(arg, bool): return not arg
+ if isinstance(arg, Not):
+ if len(arg.args) == 1: return arg.args[0]
+ return arg.args
+
+class Implies(BooleanFunction):
+ def __init__(self, *args, **kwargs):
+ if len(args) != 2: raise ValueError("Wrong set of arguments")
+ return super(BooleanFunction, self).__init__(*args, **kwargs)
+
+class Equivalent(BooleanFunction):
+ pass
+
+### end class definitions. Some useful methods
+
+def conjuncts(expr):
+ """Return a list of the conjuncts in the expr s.
+ >>> from sympy import symbols
+ >>> A, B = symbols('AB')
+ >>> conjuncts(A & B)
+ [A, B]
+ >>> conjuncts(A | B)
+ [Or(A, B)]
+ """
+ if isinstance(expr, And):
+ return list(expr.args)
+ else:
+ return [expr]
+
+def disjuncts(expr):
+ """Return a list of the disjuncts in the sentence s.
+ >>> from sympy import symbols
+ >>> A, B = symbols('AB')
+ >>> disjuncts(A | B)
+ [A, B]
+ >>> disjuncts(A & B)
+ [And(A, B)]
+ """
+ if isinstance(expr, Or):
+ return list(expr.args)
+ else:
+ return [expr]
+
+def distribute_and_over_or(expr):
+ """Given a sentence s consisting of conjunctions and disjunctions
+ of literals, return an equivalent sentence in CNF.
+ """
+ if isinstance(expr, Or):
+ expr = Or(*expr.args)
+ if len(expr.args) == 0:
+ return False
+ if len(expr.args) == 1:
+ return distribute_and_over_or(expr.args[0])
+ for arg in expr.args:
+ if isinstance(arg, And):
+ conj = arg
+ break
+ else: return type(expr)(*expr.args)
+ others = [a for a in expr.args if a is not conj]
+ if len(others) == 1:
+ rest = others[0]
+ else:
+ rest = Or(*others)
+ return And(*map(distribute_and_over_or,
+ [Or(c, rest) for c in conj.args]))
+ elif isinstance(expr, And):
+ return And(*map(distribute_and_over_or, expr.args))
+ else:
+ return expr
+
+def to_cnf(expr):
+ """Convert a propositional logical sentence s to conjunctive normal form.
+ That is, of the form ((A | ~B | ...) & (B | C | ...) & ...)
+ """
+ expr = sympify(expr)
+ expr = eliminate_implications(expr)
+ return distribute_and_over_or(expr)
+
+def eliminate_implications(expr):
+ """Change >>, <<, and <=> into &, |, and ~. That is, return an Expr
+ that is equivalent to s, but has only &, |, and ~ as logical operators.
+ """
+ expr = sympify(expr)
+ if expr.is_Atom: return expr ## (Atoms are unchanged.)
+ args = map(eliminate_implications, expr.args)
+ a, b = args[0], args[-1] # TODO: multiple implications?
+ if isinstance(expr, Implies):
+ return Or(b, Not(a))
+ elif isinstance(expr, Equivalent):
+ return And(Or(a, Not(b)), Or(b, Not(a)))
+ else:
+ return type(expr)(*args)
+
+def compile_rule(s):
+ """Transforms a rule into a sympy expression
+ A rule is a string of the form "symbol1 & symbol2 | ..."
+ See sympy.assumptions.known_facts for examples of rules
+ """
+ import re
+ return eval(re.sub(r'([a-zA-Z0-9_.]+)', r'Symbol("\1")', s), {'Symbol' : Symbol})
\ No newline at end of file
diff --git a/sympy/logic/inference.py b/sympy/logic/inference.py
new file mode 100755
index 0000000..a638ee2
--- /dev/null
+++ b/sympy/logic/inference.py
@@ -0,0 +1,119 @@
+"""Inference in propositional logic"""
+from sympy.core import Symbol
+from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent, disjuncts, \
+ to_cnf
+
+
+def find_pure_symbol(symbols, unknown_clauses):
+ """Find a symbol and its value if it appears only as a positive literal
+ (or only as a negative) in clauses.
+ >>> from sympy import symbols
+ >>> A, B, C = symbols('ABC')
+ >>> find_pure_symbol([A, B, C], [A|~B,~B|~C,C|A])
+ (A, True)
+ """
+ for sym in symbols:
+ found_pos, found_neg = False, False
+ for c in unknown_clauses:
+ if not found_pos and sym in disjuncts(c): found_pos = True
+ if not found_neg and Not(sym) in disjuncts(c): found_neg = True
+ if found_pos != found_neg: return sym, found_pos
+ return None, None
+
+def find_unit_clause(clauses, model):
+ """A unit clause has only 1 variable that is not bound in the model.
+ >>> from sympy import symbols
+ >>> A, B, C = symbols('ABC')
+ >>> find_unit_clause([A | B | C, B | ~C, A | ~B], {A:True})
+ (B, True)
+ """
+ for clause in clauses:
+ num_not_in_model = 0
+ for literal in disjuncts(clause):
+ sym = literal_symbol(literal)
+ if sym not in model:
+ num_not_in_model += 1
+ P, value = sym, (isinstance(literal, Not))
+ if num_not_in_model == 1:
+ return P, value
+ return None, None
+
+def literal_symbol(literal):
+ """The symbol in this literal (without the negation).
+ >>> from sympy import Symbol
+ >>> A = Symbol('A')
+ >>> literal_symbol(A)
+ A
+ >>> literal_symbol(~A)
+ A
+ """
+ if isinstance(literal, Not):
+ return literal.args[0]
+ else:
+ return literal
+
+def satisfiable(expr, algorithm="dpll"):
+ """Check satisfiability of a propositional sentence.
+ Returns a model when it succeeds
+
+ Examples
+ >>> from sympy import symbols
+ >>> A, B = symbols('AB')
+ >>> satisfiable(A & ~B)
+ {A: True, B: False}
+ >>> satisfiable(A & ~A)
+ False
+ """
+ expr = to_cnf(expr)
+ if algorithm == "dpll":
+ from sympy.logic.algorithms.dpll import dpll_satisfiable
+ return dpll_satisfiable(expr)
+ raise NotImplementedError
+
+def pl_true(expr, model={}):
+ """Return True if the propositional logic expression is true in the model,
+ and False if it is false. If the model does not specify the value for
+ every proposition, this may return None to indicate 'not obvious';
+ this may happen even when the expression is tautological.
+
+ The model is implemented as a dict containing the pair symbol, boolean value.
+
+ Examples:
+ >>> from sympy import symbols
+ >>> A, B = symbols('AB')
+ >>> pl_true( A & B, {A: True, B : True})
+ True
+ """
+ args = expr.args
+ if isinstance(expr, bool):
+ return expr
+ if expr.is_Atom: return model.get(expr)
+ elif isinstance(expr, Not):
+ p = pl_true(args[0], model)
+ if p is None: return None
+ else: return not p
+ elif isinstance(expr, Or):
+ result = False
+ for arg in args:
+ p = pl_true(arg, model)
+ if p == True: return True
+ if p == None: result = None
+ return result
+ elif isinstance(expr, And):
+ result = True
+ for arg in args:
+ p = pl_true(arg, model)
+ if p == False: return False
+ if p == None: result = None
+ return result
+ p, q = args
+ if isinstance(expr, Implies):
+ return pl_true(Or(Not(p), q), model)
+ pt = pl_true(p, model)
+ if pt == None: return None
+ qt = pl_true(q, model)
+ if qt == None: return None
+ if isinstance(expr, Equivalent):
+ return pt == qt
+ else:
+ raise ValueError, "Illegal operator in logic expression" + str(exp)
\ No newline at end of file
diff --git a/sympy/logic/kb.py b/sympy/logic/kb.py
new file mode 100644
index 0000000..267af91
--- /dev/null
+++ b/sympy/logic/kb.py
@@ -0,0 +1,36 @@
+from sympy.logic.boolalg import And, conjuncts, to_cnf
+from sympy.logic.inference import satisfiable
+
+class KB(object):
+ pass
+
+class PropKB(KB):
+ "A KB for Propositional Logic. Inefficient, with no indexing."
+
+ def __init__(self, sentence=None):
+ self.clauses = []
+ if sentence:
+ self.tell(sentence)
+
+ def tell(self, sentence):
+ "Add the sentence's clauses to the KB"
+ self.clauses.extend(conjuncts(to_cnf(sentence)))
+
+ def ask(self, query):
+ """TODO: examples"""
+ if len(self.clauses) == 0: return {}
+ query_conjuncts = conjuncts(to_cnf(~query))
+ query_conjuncts.extend(self.clauses)
+ return not satisfiable(And(*query_conjuncts))
+
+ def ask_generator(self, query):
+ "Yield the empty substitution if KB implies query; else False"
+ if not tt_entails(Expr('&', *self.clauses), query):
+ return
+ yield {}
+
+ def retract(self, sentence):
+ "Remove the sentence's clauses from the KB"
+ for c in conjuncts(to_cnf(sentence)):
+ if c in self.clauses:
+ self.clauses.remove(c)
\ No newline at end of file
diff --git a/sympy/logic/tests/test_boolalg.py b/sympy/logic/tests/test_boolalg.py
new file mode 100755
index 0000000..e4f1c32
--- /dev/null
+++ b/sympy/logic/tests/test_boolalg.py
@@ -0,0 +1,110 @@
+from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent, to_cnf, \
+ eliminate_implications, distribute_and_over_or
+from sympy import symbols
+from sympy.utilities.pytest import raises
+
+def test_overloading():
+ """Test that |, & are overloaded as expected"""
+ A, B, C = symbols('ABC')
+ assert A & B == And(A, B)
+ assert A | B == Or(A, B)
+ assert (A & B) | C == Or(And(A, B), C)
+ assert A >> B == Implies(A, B)
+ assert A << B == Implies(B, A)
+ assert ~A == Not(A)
+
+def test_bool_unary():
+ """Test boolean functions with one argument
+ Only Not is well defined in this case.
+ All other functions should raise a ValueError
+ """
+ A = symbols('A')
+ assert Not(True ) == False
+ assert Not(False) == True
+ raises(ValueError, "And(True)")
+ raises(ValueError, "And(False)")
+ raises(ValueError, "And(A)")
+ raises(ValueError, "Or(True)")
+ raises(ValueError, "Or(False)")
+ raises(ValueError, "Or(A)")
+
+def test_And_bool_2():
+ """Test And with two boolean arguments"""
+ assert And(True, True ) == True
+ assert And(True, False) == False
+ assert And(False, False) == False
+
+def test_Or_bool():
+ assert Or(True, True ) == True
+ assert Or(True, False) == True
+ assert Or(False, False) == False
+
+def test_Not_bool():
+ assert Not(True, True ) == [False, False]
+ assert Not(True, False) == [False, True ]
+ assert Not(False,False) == [True, True ]
+
+def test_Implies():
+ A, B, C = symbols('ABC')
+ raises(ValueError, "Implies()")
+ raises(ValueError, "Implies(A)")
+ raises(ValueError, "Implies(A, B, C)")
+
+def test_bool_symbol():
+ """Test that mixing symbols with boolean values
+ works as expected"""
+ A, B, C = symbols('ABC')
+ assert And(A, True) == A
+ assert And(A, True, True) == A
+ assert And(A, False) == False
+ assert And(A, True, False) == False
+ assert Or(A, True) == True
+ assert Or(A, False) == A
+
+"""
+we test for axioms of boolean algebra
+see http://en.wikipedia.org/wiki/Boolean_algebra_(structure)
+"""
+
+def test_commutative():
+ """Test for commutativity of And and Not"""
+ A, B = symbols('AB')
+ assert A & B == B & A
+ assert A | B == B | A
+
+def test_and_associativity():
+ """Test for associativity of And"""
+ A, B, C = symbols('ABC')
+ assert (A & B) & C == A & (B & C)
+
+def test_or_assicativity():
+ A, B, C = symbols('ABC')
+ assert ((A | B) | C) == (A | (B | C))
+
+def test_double_negation():
+ a = symbols('a')
+ assert ~(~a) == a
+
+def test_De_Morgan():
+ A, B = symbols('AB')
+ assert ~(A & B) == (~A) | (~B)
+ assert ~(A | B) == (~A) & (~B)
+
+
+# test methods
+def test_eliminate_implications():
+ A, B, C = symbols('ABC')
+ assert eliminate_implications( A >> B) == (~A) | B
+ assert eliminate_implications(A >> (C >>Not(B))) \
+ == Or(Or(Not(B), Not(C)), Not(A))
+
+def test_distribute():
+ A, B, C = symbols('ABC')
+ assert distribute_and_over_or(Or(And(A, B), C)) == And(Or(A, C), Or(B, C))
+
+
+def test_to_cnf():
+ A, B, C = symbols('ABC')
+ assert to_cnf(Not(Or(B, C))) == And(Not(B), Not(C))
+ assert to_cnf(Equivalent(A, Or(B,C))) == \
+ And(Or(Not(B), A), Or(Not(C), A), Or(B, C, Not(A)))
diff --git a/sympy/logic/tests/test_inference.py b/sympy/logic/tests/test_inference.py
new file mode 100755
index 0000000..6667e15
--- /dev/null
+++ b/sympy/logic/tests/test_inference.py
@@ -0,0 +1,46 @@
+from sympy import symbols
+from sympy.logic.boolalg import And, Not, Or, Equivalent, Implies, to_cnf
+from sympy.logic.inference import pl_true, satisfiable
+from sympy.logic.algorithms.dpll import dpll
+from sympy.logic.kb import PropKB
+
+
+def test_satisfiable():
+ A, B, C = symbols('ABC')
+ assert satisfiable( A & ~A ) == False
+ assert satisfiable( A & ~B ) == {A: True, B: False}
+ assert satisfiable( A & B & C ) == {A: True, B: True, C: True}
+ assert satisfiable( A | B ) in ({A: True}, {B: True})
+
+def test_satisfiable_1():
+ """We prove expr entails alpha proving expr & ~B is unsatisfiable"""
+ A, B, C = symbols('ABC')
+ assert satisfiable(A & (A >> B) & ~B) == False
+
+def test_pl_true():
+ A, B, C = symbols('ABC')
+ assert pl_true( And(A, B), {A : True, B : True}) == True
+ assert pl_true( Or(A, B), {A : True}) == True
+ assert pl_true( Or(A, B), {B : True}) == True
+
+ # test for false
+ assert pl_true ( And(A, B), {A: False, B: False}) == False
+ assert pl_true ( And(A, B), {A: False}) == False
+ assert pl_true ( And(A, B), {B: False}) == False
+ assert pl_true ( Or(A, B), {A: False, B: False}) == False
+
+def test_PropKB():
+ A, B, C = symbols('ABC')
+ kb = PropKB()
+ kb.tell(A)
+ kb.tell(A >> B)
+ kb.tell(B >> C)
+ assert kb.ask(B) == True
+ assert kb.ask(C) == True
+ "TODO: test for api: .clauses etc"
+
+def test_propKB_tolerant():
+ """"Test that it is tolerant to bad input"""
+ kb = PropKB()
+ A, B, C = symbols('ABC')
+ assert kb.ask(B) == {}
--
1.6.1.2
fseoane
Anyway, I believe it is nice and can be useful in a future ..., please
review ...
Ondrej Certik
>
> The following are a series of patches that implement the new assumption system, which
> consists of:
>
> - preparatory stuff (patches 1-5)
> - a logic module (much cleaner than the old one)
> - new style-assumptions (very simple objects)
> - query module, which substitutes the .is_* syntax
>
> I tried hard to separate these 3 functionalities as much as possible.
>
> This is more an initial implementation from whom we can star to work rather than a
> finished product, so in case you have any objections, we can start discussing.
>
> Thanks for the review,
Could you also push this to some branch to github? I'll play with it.
Ondrej
Fabian Pedregosa
git pull http://fseoane.net/git/sympy.git assumptions
but currently the server seems to be down ... i'll ping you when it
comes back
>
> Ondrej
>
> >
>
--
http://fseoane.net/blog/
Fabian Pedregosa
> Ondrej Certik wrote:
>> On Wed, Jun 10, 2009 at 9:20 AM, Fabian Pedregosa<fab...@fseoane.net> wrote:
>>> The following are a series of patches that implement the new assumption system, which
>>> consists of:
>>>
>>> - preparatory stuff (patches 1-5)
>>> - a logic module (much cleaner than the old one)
>>> - new style-assumptions (very simple objects)
>>> - query module, which substitutes the .is_* syntax
>>>
>>> I tried hard to separate these 3 functionalities as much as possible.
>>>
>>> This is more an initial implementation from whom we can star to work rather than a
>>> finished product, so in case you have any objections, we can start discussing.
>>>
>>> Thanks for the review,
>> Could you also push this to some branch to github? I'll play with it.
>
> should be in the usual location:
>
> git pull http://fseoane.net/git/sympy.git assumptions
git pull http://fseoane.net/git/sympy.git master
(notice branch is master, not assumptions) should be working now,
~Fabian
Ondrej Certik
> This will be used in the logic module to denest classes of the same type
> (but I believe it will be useful also in other places)
> ---
> sympy/utilities/iterables.py | 25 +++++++++++++++++++++----
> sympy/utilities/tests/test_iterables.py | 6 ++++++
> 2 files changed, 27 insertions(+), 4 deletions(-)
>
> diff --git a/sympy/utilities/iterables.py b/sympy/utilities/iterables.py
> index 24ebcd0..8d96b04 100644
> --- a/sympy/utilities/iterables.py
> +++ b/sympy/utilities/iterables.py
> @@ -65,7 +65,7 @@ def make_list(expr, kind):
> return [expr]
>
>
> -def flatten(iterable):
> +def flatten(iterable, cls=None):
> """Recursively denest iterable containers.
>
> >>> flatten([1, 2, 3])
> @@ -77,13 +77,30 @@ def flatten(iterable):
> >>> flatten( (1,2, (1, None)) )
> [1, 2, 1, None]
>
> + If cls argument is specif, it will only flatten instances of that
also be tested in regular tests. Add tests with more nested stuff.
Ondrej Certik
> extensively by the query module. The old logic module can be
> removed once the old assumption system is removed.
so that it's easier for users to understand what each function is
doing. I marked the functions where I would add a doctest below:
> + @classmethod
> + def eval(cls, *args):
> + if len(args) < 2: raise ValueError("And must have at least two arguments")
> + out_args = []
> + for i, arg in enumerate(args): # we iterate over a copy or args
> + if isinstance(arg, bool):
> + if not arg: return False
> + else: continue
> + out_args.append(arg)
> + if len(out_args) == 0: return True
> + if len(out_args) == 1: return out_args[0]
> + sargs = sorted(flatten(out_args, cls=cls))
> + return Basic.__new__(cls, *sargs)
> +
> +class Or(BooleanFunction):
> + @classmethod
> + def eval(cls, *args):
> + if len(args) < 2: raise ValueError("And must have at least two arguments")
> + out_args = []
> + for i, arg in enumerate(args): # we iterate over a copy or args
> + if isinstance(arg, bool):
> + if arg: return True
> + else: continue
> + out_args.append(arg)
> + if len(out_args) == 0: return False
> + if len(out_args) == 1: return out_args[0]
> + sargs = sorted(flatten(out_args, cls=cls))
> + return Basic.__new__(cls, *sargs)
> +
> +class Not(BooleanFunction):
> + """De Morgan rules applied automatically, so Not is moved inward"""
> + @classmethod
> + def eval(cls, *args):
> + if len(args) > 1:
> + return map(cls, args)
> + arg = args[0]
> + # apply De Morgan Rules
> + if isinstance(arg, And):
> + return Or( *[Not(a) for a in arg.args])
> + if isinstance(arg, Or):
> + return And(*[Not(a) for a in arg.args])
> + if isinstance(arg, bool): return not arg
> + if isinstance(arg, Not):
> + if len(arg.args) == 1: return arg.args[0]
> + return arg.args
> +
> +class Implies(BooleanFunction):
> + """
> + expr = sympify(expr)
> + expr = eliminate_implications(expr)
> + return distribute_and_over_or(expr)
> +
> +def eliminate_implications(expr):
> + """Change >>, <<, and <=> into &, |, and ~. That is, return an Expr
> + that is equivalent to s, but has only &, |, and ~ as logical operators.
> + """
> + expr = sympify(expr)
> + if expr.is_Atom: return expr ## (Atoms are unchanged.)
> + args = map(eliminate_implications, expr.args)
> + a, b = args[0], args[-1] # TODO: multiple implications?
> + if isinstance(expr, Implies):
> + return Or(b, Not(a))
> + elif isinstance(expr, Equivalent):
> + return And(Or(a, Not(b)), Or(b, Not(a)))
> + else:
> + return type(expr)(*args)
> +
> +def compile_rule(s):
> + """Transforms a rule into a sympy expression
> + A rule is a string of the form "symbol1 & symbol2 | ..."
> + See sympy.assumptions.known_facts for examples of rules
Ondrej Certik
Ondrej Certik
that we already have in
sympy/core/facts.py
? Is it a duplicate functionality, or a new functionality, etc.? Is
it better/worse, what are your plans with facts.py (should we remove
it or maintain both)?
Ondrej
Ondrej Certik
Couple minor comments:
* add more documentation and doctests to the classes below
Put the lines (in the log):
> The assumption system implemented in this series of patches relies on these
> principles:
...
as a module docstring.
Otherwise +1.
Ondrej
Ondrej Certik
Ondrej Certik
Ondrej Certik
Otherwise +1
Ondrej Certik
Ondrej Certik
>
> Fabian Pedregosa wrote:
>> Ondrej Certik wrote:
>>> On Wed, Jun 10, 2009 at 9:20 AM, Fabian Pedregosa<fab...@fseoane.net> wrote:
>>>> The following are a series of patches that implement the new assumption system, which
>>>> consists of:
>>>>
>>>> - preparatory stuff (patches 1-5)
>>>> - a logic module (much cleaner than the old one)
>>>> - new style-assumptions (very simple objects)
>>>> - query module, which substitutes the .is_* syntax
>>>>
>>>> I tried hard to separate these 3 functionalities as much as possible.
>>>>
>>>> This is more an initial implementation from whom we can star to work rather than a
>>>> finished product, so in case you have any objections, we can start discussing.
>>>>
>>>> Thanks for the review,
>>> Could you also push this to some branch to github? I'll play with it.
>>
>> should be in the usual location:
>>
>> git pull http://fseoane.net/git/sympy.git assumptions
>
> git pull http://fseoane.net/git/sympy.git master
>
> (notice branch is master, not assumptions) should be working now,
Patches are ok, tests pass. Code is ok too, I only had some minor
remarks regarding docstrings and doctests. It's important to write
nice docstrings, because they show up in our documentation. Those
should not serve as tests though, only to guide the user, so that he
has an idea what the function does.
Ondrej
Brian Granger
Looks like very exciting work. I have a few questions about the new system...
One thing that really bothered me about the old .is_* syntax is that
it made it very difficult for users to create their own Sympy
subclasses and have them be true equals with the built-in Sympy types.
The reason is that for each new type you created, you would have to
modify the Sympy core to add the appropriate is_* syntax for your new
types.
It look like your patches will make it much easier for users to create
custom Sympy types that are on equal grounds as the built in ones. Is
this the case? If I create a new type, will I be able to implement
queries for that type and will I be able to tell the Sympy core about
my objects without modifying the Sympy core?
I think we should make it a goal that new sympy types can be created
without modifying Sympy core. Another area that currently violates
this idea is the printing system. But, this will have to be modified
anyways to get it to work with the Sage notebook's handling of latex
output.
Cheers,
Brian
Ondrej Certik
>
> Fabian,
>
> Looks like very exciting work. I have a few questions about the new system...
>
> One thing that really bothered me about the old .is_* syntax is that
> it made it very difficult for users to create their own Sympy
> subclasses and have them be true equals with the built-in Sympy types.
> The reason is that for each new type you created, you would have to
> modify the Sympy core to add the appropriate is_* syntax for your new
> types.
>
> It look like your patches will make it much easier for users to create
> custom Sympy types that are on equal grounds as the built in ones. Is
> this the case? If I create a new type, will I be able to implement
> queries for that type and will I be able to tell the Sympy core about
> my objects without modifying the Sympy core?
Yes, definitely!
>
> I think we should make it a goal that new sympy types can be created
> without modifying Sympy core. Another area that currently violates
> this idea is the printing system. But, this will have to be modified
> anyways to get it to work with the Sage notebook's handling of latex
> output.
It has to be fixed for the sage notebook, but otherwise how does it violate it?
If you create your own class and want to hook it up let's say in the
latex printer, just override the _latex_ method.
The same way, if you want to create your own printer, just override or
create a new Printer class from scratch. That way, sympy can be
extented both by new classes and new printers. What is your idea to do
it some other way?
Ondrej
Brian Granger
>> custom Sympy types that are on equal grounds as the built in ones. Is
>> this the case? If I create a new type, will I be able to implement
>> queries for that type and will I be able to tell the Sympy core about
>> my objects without modifying the Sympy core?
>
> Yes, definitely!
Great!
>> I think we should make it a goal that new sympy types can be created
>> without modifying Sympy core. Another area that currently violates
>> this idea is the printing system. But, this will have to be modified
>> anyways to get it to work with the Sage notebook's handling of latex
>> output.
>
> It has to be fixed for the sage notebook, but otherwise how does it violate it?
Currently, I don't think it does . But, the naive fix for the sage
notebook issue introduces an infinite recursion (_latex_ calls
Printer._print, calls _latex). We just have to make we resolve this
in a way that doesn't break user's ability to create both new Printers
and new Sympy types. I know this because I have a hack in my local
branch that fixes the sage notebook issue but breaks the overall
printing model.
Brian
Ondrej Certik
If there is an infinite recursion, then it's a bug, it should work
nice. I think the problem is that _latex_ is not designed to be called
directly. You should call Basic.__str__(), or just Printer.doprint().
So if the notebook is calling _latex_, then it's just a coincidence,
and we should either rename the sympy method, or fix the Sage
notebook.
Ondrej
Brian Granger
> nice. I think the problem is that _latex_ is not designed to be called
> directly. You should call Basic.__str__(), or just Printer.doprint().
> So if the notebook is calling _latex_, then it's just a coincidence,
> and we should either rename the sympy method, or fix the Sage
> notebook.
The Sage notebook looks for a _latex_ methods and then calls it
directly to get the latex rep of an object. I agree this is a bug.
To fix this issue we will have to:
1) Add a _latex_ method to each class we want to be printable from the
Sage notebook.
2) Rename the Sympy print method for Sympy from _latex_ to something else.
If we don't want to rename the method, we will have to do some more
careful thinking about the Printing system.
Cheers,
Brian
Ondrej Certik
I would just rename the _latex_ method, which currently means to apply
this patch:
$ git diff
diff --git a/sympy/printing/latex.py b/sympy/printing/latex.py
index 02cdd00..fec85ee 100644
--- a/sympy/printing/latex.py
+++ b/sympy/printing/latex.py
@@ -12,7 +12,7 @@ from sympy.mpmath.settings import prec_to_dps
import re
class LatexPrinter(Printer):
- printmethod = "_latex_"
+ printmethod = "_sympylatex_"
def __init__(self, profile=None):
Printer.__init__(self)
and then we need to implement _latex_ in Basic *only*, so this
currently means the following patch:
diff --git a/sympy/core/basic.py b/sympy/core/basic.py
index 6ab3101..b5b2111 100644
--- a/sympy/core/basic.py
+++ b/sympy/core/basic.py
@@ -712,6 +712,9 @@ class Basic(AssumeMeths):
def __str__(self):
return StrPrinter.doprint(self)
+ def _latex_(self):
+ return latex(self)
+
def atoms(self, *types):
"""Returns the atoms that form the current object.
An atom is the smallest piece in which we can divide an
So you can see things are really easy with the print system.
Ondrej
Fabian Pedregosa
> Fabian,
>
> Looks like very exciting work. I have a few questions about the new system...
>
> One thing that really bothered me about the old .is_* syntax is that
> it made it very difficult for users to create their own Sympy
> subclasses and have them be true equals with the built-in Sympy types.
> The reason is that for each new type you created, you would have to
> modify the Sympy core to add the appropriate is_* syntax for your new
> types.
>
> It look like your patches will make it much easier for users to create
> custom Sympy types that are on equal grounds as the built in ones. Is
> this the case? If I create a new type, will I be able to implement
> queries for that type and will I be able to tell the Sympy core about
> my objects without modifying the Sympy core?
>
> I think we should make it a goal that new sympy types can be created
> without modifying Sympy core. Another area that currently violates
> this idea is the printing system. But, this will have to be modified
> anyways to get it to work with the Sage notebook's handling of latex
> output.
I'll show by example how to create a new query without touching any file
in sympy's codebase :
In [1]: from sympy.query import QueryHandler, handlers_dict
In [2]: class AssociativeQueryHandler(QueryHandler):
...: def Symbol(self):
...: return True # we know Symbols are associative
...: def Number(self):
...: return True
...:
In [3]: handlers_dict.update({'associative': AssociativeQueryHandler}) #
we tell the assumptions system that the associative query will be
handled by our class
In [4]: query(x, associative=True) # voilá !
Out[4]: True
In [5]: query(3, associative=True)
Out[5]: True
As you see, you can add/remove query handlers at runtime without much
trouble.
PS: this whole structure is similar to the one you described in (3) in
the thread "expansion refactoring"
>
> Cheers,
>
> Brian
>
>
>
> On Wed, Jun 10, 2009 at 8:20 AM, Fabian Pedregosa<fab...@fseoane.net> wrote:
>> The following are a series of patches that implement the new assumption system, which
>> consists of:
>>
>> - preparatory stuff (patches 1-5)
>> - a logic module (much cleaner than the old one)
>> - new style-assumptions (very simple objects)
>> - query module, which substitutes the .is_* syntax
>>
>> I tried hard to separate these 3 functionalities as much as possible.
>>
>> This is more an initial implementation from whom we can star to work rather than a
>> finished product, so in case you have any objections, we can start discussing.
>>
>> Thanks for the review,
>>
>> - Fabian
>>
>> pd: patch 3 was already approved, just that i did not push it in.
>>
>>
>
> >
>
http://fseoane.net/blog/
Brian Granger
> I'll show by example how to create a new query without touching any file
> in sympy's codebase :
>
> In [1]: from sympy.query import QueryHandler, handlers_dict
>
> In [2]: class AssociativeQueryHandler(QueryHandler):
> ...: def Symbol(self):
> ...: return True # we know Symbols are associative
> ...: def Number(self):
> ...: return True
> ...:
>
> In [3]: handlers_dict.update({'associative': AssociativeQueryHandler}) #
> we tell the assumptions system that the associative query will be
> handled by our class
>
> In [4]: query(x, associative=True) # voilá !
> Out[4]: True
>
> In [5]: query(3, associative=True)
> Out[5]: True
>
> As you see, you can add/remove query handlers at runtime without much
> trouble.
two different packages define some new Sympy objects and some queries
along with them. And let's say that merely importing those packages
causes them to register their queries under the same key.
Making it more concrete, if package foo and bar both call:
handlers_dict.update({'associative': FooAssociativeQueryHandler})
handlers_dict.update({'associative': BarAssociativeQueryHandler})
What will happen? If I am reading your code correctly, the last one
wins. If I need to use package foo and package bar (written by
different folks possibly) in my own code, I can't.
Am I understanding this correctly? If so, I would consider this a bug.
This usage case could be very common as we make it easier for others
to create sympy types with assumptions.
Overall though, I think this will be a huge improvement over the
current assumption system. Great job!
Cheers,
Brian
> PS: this whole structure is similar to the one you described in (3) in
> the thread "expansion refactoring"
Ondrej Certik
Yes, this is a bug. Does anyone have an idea how to fix it? Maybe the
handlers_dict.update should be our own method and it should raise an
exception if one key is updated twice? E.g. one would first have to
remove the key, then register it. Then the user will know that two
packages use the same key at least.
Ondrej
Brian Granger
> handlers_dict.update should be our own method and it should raise an
> exception if one key is updated twice? E.g. one would first have to
> remove the key, then register it. Then the user will know that two
> packages use the same key at least.
Does it make logical sense to have more than 1 query for an assumption type:
register_query_handler('associative',FooAssociativeQueryHandler)
register_query_handler('associative',BarAssociativeQueryHandler)
The internal data structure would be a dict of lists, keyed by things
like 'associative'.
I guess what I don't know is if the assumption system is setup to go
through a sequence
of handlers or if that makes sense. Thinking out loud here...
If different QueryHandlers implement methods for different types:
class FooAssociativeQueryHandler(QueryHandler):
def Symbol(self):
return True
class BarAssociativeQueryHandler(QueryHandler):
def Number(self):
return True
I can imagine that you can go through and try each handler. The issue
is when more than one handler tries to handle a single type. The only
thing I can think of then is to have a priority system, where the
handlers are tried in order of increasing priority and the final value
(the highest priority one) wins.
Cheers,
Brian
Ondrej Certik
Yes, I think this makes sense to me. It's just like linux boot up scripts.
Ondrej
Fabian Pedregosa
> Looks good, please add doctests.
>
http://fseoane.net/blog/
Fabian Pedregosa
problem !!. The problem of extensibility with respect to user-defined
types (as opposed to extensibility with respect to user-defined queries)
Suppose you have a self-defined type and you want to use existing query
keys with that type, for example:
>>> x = MySymbol('x')
>>> query(x, commutative=True)
None
Now, having multiple QueryHandlers for one query would permit us to define:
class xCommutativeHandler(QueryHandler):
def MySymbol(self):
return True
then
>>> register_query_handler('commutative',xCommutativeQueryHandler)
and queries would work with class MySymbol:
>>> query(x, commutative=True)
True
I think it's a clever way of solving both extensibility on types and on
queries.
As to your original question, when two queryhandlers clash on a specific
method, for consistency I think we should evaluate both and return the
most specific result, or raise an exception if they contradict, that is:
1. If both handlers return None --> return None
3. If one returns a bool and the other one None --> return the bool
4. If both handlers return the same bool --> return that bool
5. If they return different booleans --> raise Exception
Thanks,
>
> Cheers,
>
> Brian
>
> >
>
--
http://fseoane.net/blog/
Vinzent Steinberg
[...]
+known_facts_dict = {
+ 'even' : ['integer & ~odd'],
+ 'composite' : ['integer & ~prime'],
+ 'complex' : ['real | imaginary', 'rational | irrational | imaginary'], # this is not quite correct
+ 'integer' : ['rational & numerator_is_one'],
+ 'irrational' : ['real & ~rational'],
+ 'imaginary' : ['complex & ~real'],
+ 'rational' : ['real & ~irrational'],
+ 'real' : ['complex & ~imaginary', 'rational | irrational'],
+ 'unbounded' : ['extended_real & ~bounded'],
+ 'negative' : ['real & ~positive & ~zero'],
+ 'nonpositive': ['real & ~positive', 'zero | negative'],
+ 'nonnegative': ['real & ~negative', 'zero | positive'],
+ 'noninteger' : ['real & ~integer'],
+ 'nonzero' : ['real & ~zero'],
+ 'odd' : ['integer & ~even'],
+ 'prime' : ['integer & positive & ~composite'],
+ 'positive' : ['real & ~negative & ~zero'],
+ 'zero' : ['real & ~positive & ~negative']
+}
Why are you using a string-based mini-language rather than using native Python objects and operators?
Is this intended for the configuration only or also for the user interface?
Vinzent
Fabian Pedregosa
> 2009/6/10 Fabian Pedregosa <fab...@fseoane.net <mailto:fab...@fseoane.net>>
parsed by compile_rule and they are converted to standard sympy
expressions.
I originally did it this way for performance reasons, this way no
computations are done at load time, because if I had done it with
expressions, I would have to define 18 symbols and create lots of And,
Or classes, code that would be executed at load time.
As to the second question, it is not intended for the user interface. In
fact, a function should be added to manage adding/removing facts so that
this is properly encapsulated.
BTW, I'll put this info as a docstring in the module.
> Vinzent
>
>
>
>
> >
--
http://fseoane.net/blog/
Brian Granger
> Knowing it or not, you gave me the answer to a far more important
> problem !!. The problem of extensibility with respect to user-defined
> types (as opposed to extensibility with respect to user-defined queries)
Glad me idea helps - I wasn't sure it was appropriate for the queries,
but I like this design pattern in general (having a registration API).
Just a question: would it simplify the handling of new sympy types to
have a more detailed registration API:
register_type(MySymbol)
register_printer(MyPrinter)
This might enable us to move to a more dynamic model for other aspects
of Sympy as well. Thoughts?
> Suppose you have a self-defined type and you want to use existing query
> keys with that type, for example:
>
> >>> x = MySymbol('x')
> >>> query(x, commutative=True)
> None
>
>
> Now, having multiple QueryHandlers for one query would permit us to define:
>
> class xCommutativeHandler(QueryHandler):
> def MySymbol(self):
> return True
>
> then
>
> >>> register_query_handler('commutative',xCommutativeQueryHandler)
>
> and queries would work with class MySymbol:
>
> >>> query(x, commutative=True)
> True
>
> I think it's a clever way of solving both extensibility on types and on
> queries.
That is beautiful and it should definitely work that way. My feeling
is that if we get design aspects like this right, Sympy is going to be
extremely powerful (and it already is!)
> As to your original question, when two queryhandlers clash on a specific
> method, for consistency I think we should evaluate both and return the
> most specific result, or raise an exception if they contradict, that is:
>
> 1. If both handlers return None --> return None
> 3. If one returns a bool and the other one None --> return the bool
> 4. If both handlers return the same bool --> return that bool
> 5. If they return different booleans --> raise Exception
I think that if we don't want to go the extra step and introduce
priorities (which would enable us to resolve issue 5), this is a god
choice.
Cheers,
Brian
Fabian Pedregosa
sympify accepts booleans.
http://fseoane.net/blog/
Ondrej Certik
Only, I am not a native speaker, but:
"
Before of this, sympy would convert True --> S.One, False --> S.Zero,
but with the logic module with classes inheriting from basic, I need
"
Ondrej
Fabian Pedregosa
>> extensively by the query module. The old logic module can be
>> removed once the old assumption system is removed.
>
>
> The code is good, tests are ok, but please try to add more doctests,
> so that it's easier for users to understand what each function is
> doing. I marked the functions where I would add a doctest below:
makes it to return unsatisfiable for expressions that are known to be
satisfiable. I don't know if it's a known issue of the algorithm or just
a programming error. As this can have a negative impact on the query
module, i'm holding this from merging until I solve the bug.
>> index b48e633..6ab3101 100644
>> --- a/sympy/core/basic.py
>> +++ b/sympy/core/basic.py
>> --- /dev/null
>> +++ b/sympy/logic/__init__.py
>> @@ -0,0 +1,2 @@
>> +from boolalg import *
>> +from inference import *
>> new file mode 100644
>> diff --git a/sympy/logic/algorithms/dpll.py b/sympy/logic/algorithms/dpll.py
>> --- /dev/null
>> +++ b/sympy/logic/algorithms/dpll.py
>> @@ -0,0 +1,49 @@
>> + return False
>> + unknown_clauses.append(c)
>> + if not unknown_clauses:
>> + return model
>> + P, value = find_pure_symbol(symbols, unknown_clauses)
>> + if P:
>> + model.update({P: value})
>> + syms = [x for x in symbols if x != P]
>> + return dpll(clauses, syms, model)
>> + P, value = find_unit_clause(clauses, model)
>> + if P:
>> + model.update({P: value})
>> + syms = [x for x in symbols if x != P]
>> + return dpll(clauses, syms, model)
>> + P = symbols.pop()
>> + model_1, model_2 = model.copy(), model.copy()
>> + model_1.update({P: True})
>> + model_2.update({P: False})
>> + return (dpll(clauses, symbols, model_1) or
>> + dpll(clauses, symbols, model_2))
>> new file mode 100755
>> index 0000000..1a57740
>> --- /dev/null
>> +++ b/sympy/logic/boolalg.py
>> @@ -0,0 +1,155 @@
>> +"""Boolean algebra module for SymPy"""
>> +from sympy.core import Basic, Function, sympify, Symbol
>> +from sympy.utilities import flatten
>> +
>> +
>> +class BooleanFunction(Function):
>> + """Boolean function is a function that lives in a boolean space
>> + It is used as base class for And, Or, Not, etc.
>> + """
>> + pass
>> +
>> +class And(BooleanFunction):
>> + """Evaluates to True if all it's arguments are True,
>> + False otherwise"""
>
> Add couple doctests
>
>> + def eval(cls, *args):
>> + out_args = []
>> + for i, arg in enumerate(args): # we iterate over a copy or args
>> + if isinstance(arg, bool):
>> + if not arg: return False
>> + else: continue
>> + out_args.append(arg)
>> + if len(out_args) == 0: return True
>> + if len(out_args) == 1: return out_args[0]
>> + sargs = sorted(flatten(out_args, cls=cls))
>> + return Basic.__new__(cls, *sargs)
>> +
>> +class Or(BooleanFunction):
>
> Add couple doctests
>
>> + def eval(cls, *args):
>> + out_args = []
>> + for i, arg in enumerate(args): # we iterate over a copy or args
>> + if isinstance(arg, bool):
>> + if arg: return True
>> + else: continue
>> + out_args.append(arg)
>> + if len(out_args) == 0: return False
>> + if len(out_args) == 1: return out_args[0]
>> + sargs = sorted(flatten(out_args, cls=cls))
>> + return Basic.__new__(cls, *sargs)
>> +
>> +class Not(BooleanFunction):
>> + """De Morgan rules applied automatically, so Not is moved inward"""
>
> Add couple doctests
>
>> + def eval(cls, *args):
>> + return False
>> + return distribute_and_over_or(expr.args[0])
>> + for arg in expr.args:
>> + if isinstance(arg, And):
>> + conj = arg
>> + break
>> + else: return type(expr)(*expr.args)
>> + others = [a for a in expr.args if a is not conj]
>> + if len(others) == 1:
>> + rest = others[0]
>> + else:
>> + rest = Or(*others)
>> + return And(*map(distribute_and_over_or,
>> + [Or(c, rest) for c in conj.args]))
>> + elif isinstance(expr, And):
>> + return And(*map(distribute_and_over_or, expr.args))
>> + else:
>> + return expr
>> +
>> +def to_cnf(expr):
>> + """Convert a propositional logical sentence s to conjunctive normal form.
>> + That is, of the form ((A | ~B | ...) & (B | C | ...) & ...)
>
> Add couple doctests
>
>> + """
>> + return distribute_and_over_or(expr)
>> +
>> +def eliminate_implications(expr):
>> + """Change >>, <<, and <=> into &, |, and ~. That is, return an Expr
>> + that is equivalent to s, but has only &, |, and ~ as logical operators.
>
> Add couple doctests
>
>> + """
>> + args = map(eliminate_implications, expr.args)
>> + a, b = args[0], args[-1] # TODO: multiple implications?
>> + if isinstance(expr, Implies):
>> + return Or(b, Not(a))
>> + elif isinstance(expr, Equivalent):
>> + return And(Or(a, Not(b)), Or(b, Not(a)))
>> + else:
>> + return type(expr)(*args)
>> +
>> +def compile_rule(s):
>> + """Transforms a rule into a sympy expression
>> + A rule is a string of the form "symbol1 & symbol2 | ..."
>> + See sympy.assumptions.known_facts for examples of rules
>
> Add couple doctests
>
>> + """
>> + import re
>> + return eval(re.sub(r'([a-zA-Z0-9_.]+)', r'Symbol("\1")', s), {'Symbol' : Symbol})
>> new file mode 100755
>> index 0000000..a638ee2
>> --- /dev/null
>> +++ b/sympy/logic/inference.py
>> @@ -0,0 +1,119 @@
>> +"""Inference in propositional logic"""
>> + to_cnf
>> +
>> +
>> +def find_pure_symbol(symbols, unknown_clauses):
>> + """Find a symbol and its value if it appears only as a positive literal
>> + (or only as a negative) in clauses.
>> + >>> from sympy import symbols
>> + >>> A, B, C = symbols('ABC')
>> + >>> find_pure_symbol([A, B, C], [A|~B,~B|~C,C|A])
>> + (A, True)
>> + for sym in symbols:
>> + else:
>> + return expr
>> new file mode 100644
>> + kb.tell(A >> B)
>> + kb.tell(B >> C)
>> + assert kb.ask(B) == True
>> + assert kb.ask(C) == True
>> + "TODO: test for api: .clauses etc"
>> +
>> +def test_propKB_tolerant():
>> + """"Test that it is tolerant to bad input"""
>> + assert kb.ask(B) == {}
Vinzent Steinberg
Thanks for the review, but I found a bug in the dpll algorithm that
makes it to return unsatisfiable for expressions that are known to be
satisfiable. I don't know if it's a known issue of the algorithm or just
a programming error.
Vinzent
Fabian Pedregosa
> 2009/6/16 Fabian Pedregosa <fab...@fseoane.net <mailto:fab...@fseoane.net>>
>
> Vinzent
>
> >
--
http://fseoane.net/blog/
Vinzent Steinberg
Now it's +1
Only, I am not a native speaker, but:
shouldn't this be just "Before this (patch), sympy would ..."
"
Before of this, sympy would convert True --> S.One, False --> S.Zero,
but with the logic module with classes inheriting from basic, I need
"
Intuitively I'd say both variants are okay, but looking at a dictionary it seems that 'before' is not used in conjunction with 'of'.
Vinzent
Fabian Pedregosa
> 2009/6/12 Ondrej Certik <ond...@certik.cz <mailto:ond...@certik.cz>>
> Vinzent
>
>
> >
--
http://fseoane.net/blog/