python-sympy 0.7.1.rc1-3 / usr / share / pyshared / sympy / assumptions / ask.py

"""Module for querying SymPy objects about assumptions."""
from sympy.core import sympify
from sympy.logic.boolalg import to_cnf, And, Not, Or, Implies, Equivalent
from sympy.logic.inference import satisfiable
from sympy.assumptions.assume import (global_assumptions, Predicate,
        AppliedPredicate)

class Q:
    """Supported ask keys."""
    bounded = Predicate('bounded')
    commutative = Predicate('commutative')
    complex = Predicate('complex')
    composite = Predicate('composite')
    even = Predicate('even')
    extended_real = Predicate('extended_real')
    imaginary = Predicate('imaginary')
    infinitesimal = Predicate('infinitesimal')
    infinity = Predicate('infinity')
    integer = Predicate('integer')
    irrational = Predicate('irrational')
    rational = Predicate('rational')
    negative = Predicate('negative')
    nonzero = Predicate('nonzero')
    positive = Predicate('positive')
    prime = Predicate('prime')
    real = Predicate('real')
    odd = Predicate('odd')
    is_true = Predicate('is_true')



def _extract_facts(expr, symbol):
    """
    Helper for ask().

    Extracts the facts relevant to the symbol from an assumption.
    Returns None if there is nothing to extract.
    """
    if not expr.has(symbol):
        return None
    if isinstance(expr, AppliedPredicate):
        return expr.func
    return expr.func(*filter(lambda x: x is not None,
                [_extract_facts(arg, symbol) for arg in expr.args]))

def ask(proposition, assumptions=True, context=global_assumptions):
    """
    Method for inferring properties about objects.

    **Syntax**

        * ask(proposition)

        * ask(proposition, assumptions)

            where ``proposition`` is any boolean expression

    **Examples**
        >>> from sympy import ask, Q, pi
        >>> from sympy.abc import x, y
        >>> ask(Q.rational(pi))
        False
        >>> ask(Q.even(x*y), Q.even(x) & Q.integer(y))
        True
        >>> ask(Q.prime(x*y), Q.integer(x) &  Q.integer(y))
        False

    **Remarks**
        Relations in assumptions are not implemented (yet), so the following
        will not give a meaningful result.

        >>> ask(Q.positive(x), Q.is_true(x > 0)) # doctest: +SKIP

        It is however a work in progress and should be available before
        the official release

    """
    assumptions = And(assumptions, And(*context))
    if isinstance(proposition, AppliedPredicate):
        key, expr = proposition.func, sympify(proposition.arg)
    else:
        key, expr = Q.is_true, sympify(proposition)

    # direct resolution method, no logic
    res = key(expr)._eval_ask(assumptions)
    if res is not None:
        return res

    if assumptions is True:
        return

    if not expr.is_Atom:
        return

    local_facts = _extract_facts(assumptions, expr)
    if local_facts is None or local_facts is True:
        return

    # See if there's a straight-forward conclusion we can make for the inference
    if local_facts.is_Atom:
        if key in known_facts_dict[local_facts]:
            return True
        if Not(key) in known_facts_dict[local_facts]:
            return False
    elif local_facts.func is And:
        for assum in local_facts.args:
            if assum.is_Atom:
                if key in known_facts_dict[assum]:
                    return True
                if Not(key) in known_facts_dict[assum]:
                    return False
            elif assum.func is Not and assum.args[0].is_Atom:
                if key in known_facts_dict[assum]:
                    return False
                if Not(key) in known_facts_dict[assum]:
                    return True
    elif (isinstance(key, Predicate) and
            local_facts.func is Not and local_facts.args[0].is_Atom):
        if local_facts.args[0] in known_facts_dict[key]:
            return False

    # Failing all else, we do a full logical inference
    return ask_full_inference(key, local_facts)


def ask_full_inference(proposition, assumptions):
    """
    Method for inferring properties about objects.

    """
    if not satisfiable(And(known_facts_cnf, assumptions, proposition)):
        return False
    if not satisfiable(And(known_facts_cnf, assumptions, Not(proposition))):
        return True
    return None



def register_handler(key, handler):
    """Register a handler in the ask system. key must be a string and handler a
    class inheriting from AskHandler.

        >>> from sympy.assumptions import register_handler, ask, Q
        >>> from sympy.assumptions.handlers import AskHandler
        >>> class MersenneHandler(AskHandler):
        ...     # Mersenne numbers are in the form 2**n + 1, n integer
        ...     @staticmethod
        ...     def Integer(expr, assumptions):
        ...         import math
        ...         return ask(Q.integer(math.log(expr + 1, 2)))
        >>> register_handler('mersenne', MersenneHandler)
        >>> ask(Q.mersenne(7))
        True

    """
    if type(key) is Predicate:
        key = key.name
    try:
        getattr(Q, key).add_handler(handler)
    except AttributeError:
        setattr(Q, key, Predicate(key, handlers=[handler]))

def remove_handler(key, handler):
    """Removes a handler from the ask system. Same syntax as register_handler"""
    if type(key) is Predicate:
        key = key.name
    getattr(Q, key).remove_handler(handler)

def compute_known_facts():
    """Compute the various forms of knowledge compilation used by the
    assumptions system.
    """
    # Compute the known facts in CNF form for logical inference
    fact_string = "# -{ Known facts in CNF }-\n"
    cnf = to_cnf(known_facts)
    fact_string += "known_facts_cnf = And(\n    "
    fact_string += ",\n    ".join(map(str, cnf.args))
    fact_string += "\n)\n"

    # Compute the quick lookup for single facts
    mapping = {}
    for key in known_facts_keys:
        mapping[key] = set([key])
        for other_key in known_facts_keys:
            if other_key != key:
                if ask_full_inference(other_key, key):
                    mapping[key].add(other_key)
    fact_string += "\n# -{ Known facts in compressed sets }-\n"
    fact_string += "known_facts_dict = {\n    "
    fact_string += ",\n    ".join(["%s: %s" % item for item in mapping.items()])
    fact_string += "\n}\n"
    return fact_string

# handlers_dict tells us what ask handler we should use
# for a particular key
_handlers_dict = {
    'bounded'        : ['sympy.assumptions.handlers.calculus.AskBoundedHandler'],
    'commutative'    : ['sympy.assumptions.handlers.AskCommutativeHandler'],
    'complex'        : ['sympy.assumptions.handlers.sets.AskComplexHandler'],
    'composite'      : ['sympy.assumptions.handlers.ntheory.AskCompositeHandler'],
    'even'           : ['sympy.assumptions.handlers.ntheory.AskEvenHandler'],
    'extended_real'  : ['sympy.assumptions.handlers.sets.AskExtendedRealHandler'],
    'imaginary'      : ['sympy.assumptions.handlers.sets.AskImaginaryHandler'],
    'infinitesimal'  : ['sympy.assumptions.handlers.calculus.AskInfinitesimalHandler'],
    'integer'        : ['sympy.assumptions.handlers.sets.AskIntegerHandler'],
    'irrational'     : ['sympy.assumptions.handlers.sets.AskIrrationalHandler'],
    'rational'       : ['sympy.assumptions.handlers.sets.AskRationalHandler'],
    'negative'       : ['sympy.assumptions.handlers.order.AskNegativeHandler'],
    'nonzero'        : ['sympy.assumptions.handlers.order.AskNonZeroHandler'],
    'positive'       : ['sympy.assumptions.handlers.order.AskPositiveHandler'],
    'prime'          : ['sympy.assumptions.handlers.ntheory.AskPrimeHandler'],
    'real'           : ['sympy.assumptions.handlers.sets.AskRealHandler'],
    'odd'            : ['sympy.assumptions.handlers.ntheory.AskOddHandler'],
    'algebraic'      : ['sympy.assumptions.handlers.sets.AskAlgebraicHandler'],
    'is_true'        : ['sympy.assumptions.handlers.TautologicalHandler']
}
for name, value in _handlers_dict.iteritems():
    register_handler(name, value[0])


known_facts_keys = [getattr(Q, attr) for attr in Q.__dict__ \
                                                if not attr.startswith('__')]
known_facts = And(
    Implies   (Q.real, Q.complex),
    Equivalent(Q.even, Q.integer & ~Q.odd),
    Equivalent(Q.extended_real, Q.real | Q.infinity),
    Equivalent(Q.odd, Q.integer & ~Q.even),
    Equivalent(Q.prime, Q.integer & Q.positive & ~Q.composite),
    Implies   (Q.integer, Q.rational),
    Implies   (Q.imaginary, Q.complex & ~Q.real),
    Equivalent(Q.negative, Q.nonzero & ~Q.positive),
    Equivalent(Q.positive, Q.nonzero & ~Q.negative),
    Equivalent(Q.rational, Q.real & ~Q.irrational),
    Equivalent(Q.real, Q.rational | Q.irrational),
    Implies   (Q.nonzero, Q.real),
    Equivalent(Q.nonzero, Q.positive | Q.negative)
)

################################################################################
# Note: The following facts are generated by the compute_known_facts function. #
################################################################################
# -{ Known facts in CNF }-
known_facts_cnf = And(
    Or(Not(Q.integer), Q.even, Q.odd),
    Or(Not(Q.extended_real), Q.infinity, Q.real),
    Or(Not(Q.real), Q.irrational, Q.rational),
    Or(Not(Q.real), Q.complex),
    Or(Not(Q.integer), Not(Q.positive), Q.composite, Q.prime),
    Or(Not(Q.integer), Q.rational),
    Or(Not(Q.imaginary), Q.complex),
    Or(Not(Q.even), Q.integer),
    Or(Not(Q.positive), Q.nonzero),
    Or(Not(Q.nonzero), Q.negative, Q.positive),
    Or(Not(Q.prime), Q.positive),
    Or(Not(Q.rational), Q.real),
    Or(Not(Q.imaginary), Not(Q.real)),
    Or(Not(Q.odd), Q.integer),
    Or(Not(Q.real), Q.extended_real),
    Or(Not(Q.composite), Not(Q.prime)),
    Or(Not(Q.negative), Q.nonzero),
    Or(Not(Q.negative), Not(Q.positive)),
    Or(Not(Q.prime), Q.integer),
    Or(Not(Q.even), Not(Q.odd)),
    Or(Not(Q.nonzero), Q.real),
    Or(Not(Q.irrational), Q.real),
    Or(Not(Q.irrational), Not(Q.rational)),
    Or(Not(Q.infinity), Q.extended_real)
)

# -{ Known facts in compressed sets }-
known_facts_dict = {
    Q.is_true: set([Q.is_true]),
    Q.complex: set([Q.complex]),
    Q.odd: set([Q.complex, Q.odd, Q.real, Q.rational, Q.extended_real, Q.integer]),
    Q.positive: set([Q.real, Q.complex, Q.extended_real, Q.positive, Q.nonzero]),
    Q.real: set([Q.real, Q.complex, Q.extended_real]),
    Q.composite: set([Q.composite]),
    Q.bounded: set([Q.bounded]),
    Q.prime: set([Q.real, Q.complex, Q.positive, Q.nonzero, Q.prime, Q.rational, Q.extended_real, Q.integer]),
    Q.infinitesimal: set([Q.infinitesimal]),
    Q.even: set([Q.complex, Q.real, Q.even, Q.rational, Q.extended_real, Q.integer]),
    Q.negative: set([Q.real, Q.negative, Q.complex, Q.extended_real, Q.nonzero]),
    Q.rational: set([Q.real, Q.rational, Q.complex, Q.extended_real]),
    Q.extended_real: set([Q.extended_real]),
    Q.nonzero: set([Q.nonzero, Q.complex, Q.extended_real, Q.real]),
    Q.integer: set([Q.real, Q.rational, Q.complex, Q.extended_real, Q.integer]),
    Q.irrational: set([Q.real, Q.irrational, Q.complex, Q.extended_real]),
    Q.commutative: set([Q.commutative]),
    Q.infinity: set([Q.extended_real, Q.infinity]),
    Q.algebraic: set([Q.algebraic]),
    Q.imaginary: set([Q.complex, Q.imaginary])
}