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