123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323 |
- from collections import defaultdict
- from sympy.assumptions.ask import Q
- from sympy.core import (Add, Mul, Pow, Number, NumberSymbol, Symbol)
- from sympy.core.numbers import ImaginaryUnit
- from sympy.functions.elementary.complexes import Abs
- from sympy.logic.boolalg import (Equivalent, And, Or, Implies)
- from sympy.matrices.expressions import MatMul
- # APIs here may be subject to change
- ### Helper functions ###
- def allargs(symbol, fact, expr):
- """
- Apply all arguments of the expression to the fact structure.
- Parameters
- ==========
- symbol : Symbol
- A placeholder symbol.
- fact : Boolean
- Resulting ``Boolean`` expression.
- expr : Expr
- Examples
- ========
- >>> from sympy import Q
- >>> from sympy.assumptions.sathandlers import allargs
- >>> from sympy.abc import x, y
- >>> allargs(x, Q.negative(x) | Q.positive(x), x*y)
- (Q.negative(x) | Q.positive(x)) & (Q.negative(y) | Q.positive(y))
- """
- return And(*[fact.subs(symbol, arg) for arg in expr.args])
- def anyarg(symbol, fact, expr):
- """
- Apply any argument of the expression to the fact structure.
- Parameters
- ==========
- symbol : Symbol
- A placeholder symbol.
- fact : Boolean
- Resulting ``Boolean`` expression.
- expr : Expr
- Examples
- ========
- >>> from sympy import Q
- >>> from sympy.assumptions.sathandlers import anyarg
- >>> from sympy.abc import x, y
- >>> anyarg(x, Q.negative(x) & Q.positive(x), x*y)
- (Q.negative(x) & Q.positive(x)) | (Q.negative(y) & Q.positive(y))
- """
- return Or(*[fact.subs(symbol, arg) for arg in expr.args])
- def exactlyonearg(symbol, fact, expr):
- """
- Apply exactly one argument of the expression to the fact structure.
- Parameters
- ==========
- symbol : Symbol
- A placeholder symbol.
- fact : Boolean
- Resulting ``Boolean`` expression.
- expr : Expr
- Examples
- ========
- >>> from sympy import Q
- >>> from sympy.assumptions.sathandlers import exactlyonearg
- >>> from sympy.abc import x, y
- >>> exactlyonearg(x, Q.positive(x), x*y)
- (Q.positive(x) & ~Q.positive(y)) | (Q.positive(y) & ~Q.positive(x))
- """
- pred_args = [fact.subs(symbol, arg) for arg in expr.args]
- res = Or(*[And(pred_args[i], *[~lit for lit in pred_args[:i] +
- pred_args[i+1:]]) for i in range(len(pred_args))])
- return res
- ### Fact registry ###
- class ClassFactRegistry:
- """
- Register handlers against classes.
- Explanation
- ===========
- ``register`` method registers the handler function for a class. Here,
- handler function should return a single fact. ``multiregister`` method
- registers the handler function for multiple classes. Here, handler function
- should return a container of multiple facts.
- ``registry(expr)`` returns a set of facts for *expr*.
- Examples
- ========
- Here, we register the facts for ``Abs``.
- >>> from sympy import Abs, Equivalent, Q
- >>> from sympy.assumptions.sathandlers import ClassFactRegistry
- >>> reg = ClassFactRegistry()
- >>> @reg.register(Abs)
- ... def f1(expr):
- ... return Q.nonnegative(expr)
- >>> @reg.register(Abs)
- ... def f2(expr):
- ... arg = expr.args[0]
- ... return Equivalent(~Q.zero(arg), ~Q.zero(expr))
- Calling the registry with expression returns the defined facts for the
- expression.
- >>> from sympy.abc import x
- >>> reg(Abs(x))
- {Q.nonnegative(Abs(x)), Equivalent(~Q.zero(x), ~Q.zero(Abs(x)))}
- Multiple facts can be registered at once by ``multiregister`` method.
- >>> reg2 = ClassFactRegistry()
- >>> @reg2.multiregister(Abs)
- ... def _(expr):
- ... arg = expr.args[0]
- ... return [Q.even(arg) >> Q.even(expr), Q.odd(arg) >> Q.odd(expr)]
- >>> reg2(Abs(x))
- {Implies(Q.even(x), Q.even(Abs(x))), Implies(Q.odd(x), Q.odd(Abs(x)))}
- """
- def __init__(self):
- self.singlefacts = defaultdict(frozenset)
- self.multifacts = defaultdict(frozenset)
- def register(self, cls):
- def _(func):
- self.singlefacts[cls] |= {func}
- return func
- return _
- def multiregister(self, *classes):
- def _(func):
- for cls in classes:
- self.multifacts[cls] |= {func}
- return func
- return _
- def __getitem__(self, key):
- ret1 = self.singlefacts[key]
- for k in self.singlefacts:
- if issubclass(key, k):
- ret1 |= self.singlefacts[k]
- ret2 = self.multifacts[key]
- for k in self.multifacts:
- if issubclass(key, k):
- ret2 |= self.multifacts[k]
- return ret1, ret2
- def __call__(self, expr):
- ret = set()
- handlers1, handlers2 = self[type(expr)]
- for h in handlers1:
- ret.add(h(expr))
- for h in handlers2:
- ret.update(h(expr))
- return ret
- class_fact_registry = ClassFactRegistry()
- ### Class fact registration ###
- x = Symbol('x')
- ## Abs ##
- @class_fact_registry.multiregister(Abs)
- def _(expr):
- arg = expr.args[0]
- return [Q.nonnegative(expr),
- Equivalent(~Q.zero(arg), ~Q.zero(expr)),
- Q.even(arg) >> Q.even(expr),
- Q.odd(arg) >> Q.odd(expr),
- Q.integer(arg) >> Q.integer(expr),
- ]
- ### Add ##
- @class_fact_registry.multiregister(Add)
- def _(expr):
- return [allargs(x, Q.positive(x), expr) >> Q.positive(expr),
- allargs(x, Q.negative(x), expr) >> Q.negative(expr),
- allargs(x, Q.real(x), expr) >> Q.real(expr),
- allargs(x, Q.rational(x), expr) >> Q.rational(expr),
- allargs(x, Q.integer(x), expr) >> Q.integer(expr),
- exactlyonearg(x, ~Q.integer(x), expr) >> ~Q.integer(expr),
- ]
- @class_fact_registry.register(Add)
- def _(expr):
- allargs_real = allargs(x, Q.real(x), expr)
- onearg_irrational = exactlyonearg(x, Q.irrational(x), expr)
- return Implies(allargs_real, Implies(onearg_irrational, Q.irrational(expr)))
- ### Mul ###
- @class_fact_registry.multiregister(Mul)
- def _(expr):
- return [Equivalent(Q.zero(expr), anyarg(x, Q.zero(x), expr)),
- allargs(x, Q.positive(x), expr) >> Q.positive(expr),
- allargs(x, Q.real(x), expr) >> Q.real(expr),
- allargs(x, Q.rational(x), expr) >> Q.rational(expr),
- allargs(x, Q.integer(x), expr) >> Q.integer(expr),
- exactlyonearg(x, ~Q.rational(x), expr) >> ~Q.integer(expr),
- allargs(x, Q.commutative(x), expr) >> Q.commutative(expr),
- ]
- @class_fact_registry.register(Mul)
- def _(expr):
- # Implicitly assumes Mul has more than one arg
- # Would be allargs(x, Q.prime(x) | Q.composite(x)) except 1 is composite
- # More advanced prime assumptions will require inequalities, as 1 provides
- # a corner case.
- allargs_prime = allargs(x, Q.prime(x), expr)
- return Implies(allargs_prime, ~Q.prime(expr))
- @class_fact_registry.register(Mul)
- def _(expr):
- # General Case: Odd number of imaginary args implies mul is imaginary(To be implemented)
- allargs_imag_or_real = allargs(x, Q.imaginary(x) | Q.real(x), expr)
- onearg_imaginary = exactlyonearg(x, Q.imaginary(x), expr)
- return Implies(allargs_imag_or_real, Implies(onearg_imaginary, Q.imaginary(expr)))
- @class_fact_registry.register(Mul)
- def _(expr):
- allargs_real = allargs(x, Q.real(x), expr)
- onearg_irrational = exactlyonearg(x, Q.irrational(x), expr)
- return Implies(allargs_real, Implies(onearg_irrational, Q.irrational(expr)))
- @class_fact_registry.register(Mul)
- def _(expr):
- # Including the integer qualification means we don't need to add any facts
- # for odd, since the assumptions already know that every integer is
- # exactly one of even or odd.
- allargs_integer = allargs(x, Q.integer(x), expr)
- anyarg_even = anyarg(x, Q.even(x), expr)
- return Implies(allargs_integer, Equivalent(anyarg_even, Q.even(expr)))
- ### MatMul ###
- @class_fact_registry.register(MatMul)
- def _(expr):
- allargs_square = allargs(x, Q.square(x), expr)
- allargs_invertible = allargs(x, Q.invertible(x), expr)
- return Implies(allargs_square, Equivalent(Q.invertible(expr), allargs_invertible))
- ### Pow ###
- @class_fact_registry.multiregister(Pow)
- def _(expr):
- base, exp = expr.base, expr.exp
- return [
- (Q.real(base) & Q.even(exp) & Q.nonnegative(exp)) >> Q.nonnegative(expr),
- (Q.nonnegative(base) & Q.odd(exp) & Q.nonnegative(exp)) >> Q.nonnegative(expr),
- (Q.nonpositive(base) & Q.odd(exp) & Q.nonnegative(exp)) >> Q.nonpositive(expr),
- Equivalent(Q.zero(expr), Q.zero(base) & Q.positive(exp))
- ]
- ### Numbers ###
- _old_assump_getters = {
- Q.positive: lambda o: o.is_positive,
- Q.zero: lambda o: o.is_zero,
- Q.negative: lambda o: o.is_negative,
- Q.rational: lambda o: o.is_rational,
- Q.irrational: lambda o: o.is_irrational,
- Q.even: lambda o: o.is_even,
- Q.odd: lambda o: o.is_odd,
- Q.imaginary: lambda o: o.is_imaginary,
- Q.prime: lambda o: o.is_prime,
- Q.composite: lambda o: o.is_composite,
- }
- @class_fact_registry.multiregister(Number, NumberSymbol, ImaginaryUnit)
- def _(expr):
- ret = []
- for p, getter in _old_assump_getters.items():
- pred = p(expr)
- prop = getter(expr)
- if prop is not None:
- ret.append(Equivalent(pred, prop))
- return ret
|