diff --git a/bin/ask_update.py b/bin/ask_update.py index 345d0e4759e8..cfe3da078216 100755 --- a/bin/ask_update.py +++ b/bin/ask_update.py @@ -1,10 +1,11 @@ #!/usr/bin/env python -""" Update the ask_generated.py file +""" Update the ``ask_generated.py`` file. -This must be run each time known_facts is changed +This must be run each time ``known_facts()`` in ``assumptions.facts`` module +is changed. -Should be run from sympy root directory +Should be run from sympy root directory. $ python bin/ask_update.py """ @@ -21,9 +22,77 @@ if os.path.isdir(sympy_dir): sys.path.insert(0, sympy_top) -from sympy.assumptions.facts import (compute_known_facts, - get_known_facts, get_known_facts_keys) +from sympy.assumptions.cnf import CNF, Literal +from sympy.assumptions.facts import (get_known_facts, + generate_known_facts_dict, get_known_facts_keys) +from sympy.core import Symbol + +def generate_code(): + from textwrap import dedent, wrap + + LINE = ",\n " + HANG = ' '*8 + code_string = dedent('''\ + """ + Do NOT manually edit this file. + Instead, run ./bin/ask_update.py. + """ + + from sympy.assumptions.ask import Q + from sympy.assumptions.cnf import Literal + from sympy.core.cache import cacheit + + @cacheit + def get_all_known_facts(): + """ + Known facts between unary predicates as CNF clauses. + """ + return { + %s + } + + @cacheit + def get_known_facts_dict(): + """ + Logical relations between unary predicates as dictionary. + + Each key is a predicate, and item is two groups of predicates. + First group contains the predicates which are implied by the key, and + second group contains the predicates which are rejected by the key. + + """ + return { + %s + } + ''') + + x = Symbol('x') + fact = get_known_facts(x) + + # Generate CNF of facts between known unary predicates + cnf = CNF.to_CNF(fact) + p = LINE.join(sorted([ + 'frozenset((' + + ', '.join(str(Literal(lit.arg.function, lit.is_Not)) + for lit in sorted(clause, key=str)) + + '))' for clause in cnf.clauses])) + + # Generate dictionary of facts between known unary predicates + keys = [pred(x) for pred in get_known_facts_keys()] + mapping = generate_known_facts_dict(keys, fact) + items = sorted(mapping.items(), key=str) + keys = [str(i[0]) for i in items] + values = ['(set(%s), set(%s))' % (sorted(i[1][0], key=str), + sorted(i[1][1], key=str)) + for i in items] + m = LINE.join(['\n'.join( + wrap("{}: {}".format(k, v), + subsequent_indent=HANG, + break_long_words=False)) + for k, v in zip(keys, values)]) + ',' + + return code_string % (p, m) with open('sympy/assumptions/ask_generated.py', 'w') as f: - code = compute_known_facts(get_known_facts(), get_known_facts_keys()) + code = generate_code() f.write(code) diff --git a/sympy/assumptions/ask.py b/sympy/assumptions/ask.py index 6dda47384236..9269e8951ada 100644 --- a/sympy/assumptions/ask.py +++ b/sympy/assumptions/ask.py @@ -6,7 +6,6 @@ from sympy.core import sympify from sympy.core.kind import BooleanKind from sympy.core.relational import Eq, Ne, Gt, Lt, Ge, Le -from sympy.logic.boolalg import Not from sympy.logic.inference import satisfiable from sympy.utilities.decorator import memoize_property from sympy.utilities.exceptions import SymPyDeprecationWarning @@ -554,20 +553,24 @@ def _ask_single_fact(key, local_facts): cl, = local_facts.clauses if len(cl) == 1: f, = cl - if f.is_Not and f.arg in known_facts_dict.get(key, []): + prop_facts = known_facts_dict.get(key, None) + prop_req = prop_facts[0] if prop_facts is not None else set() + if f.is_Not and f.arg in prop_req: # the prerequisite of proposition is rejected return False for clause in local_facts.clauses: if len(clause) == 1: f, = clause - fdict = known_facts_dict.get(f.arg, None) if not f.is_Not else None - if fdict is None: - pass - elif key in fdict: + prop_facts = known_facts_dict.get(f.arg, None) if not f.is_Not else None + if prop_facts is None: + continue + + prop_req, prop_rej = prop_facts + if key in prop_req: # assumption implies the proposition return True - elif Not(key) in fdict: + elif key in prop_rej: # proposition rejects the assumption return False @@ -617,5 +620,5 @@ def remove_handler(key, handler): getattr(Q, key).remove_handler(handler) -from sympy.assumptions.ask_generated import ( - get_known_facts_dict, get_all_known_facts) +from sympy.assumptions.ask_generated import (get_all_known_facts, + get_known_facts_dict) diff --git a/sympy/assumptions/ask_generated.py b/sympy/assumptions/ask_generated.py index 054f1579be21..656da63938d3 100644 --- a/sympy/assumptions/ask_generated.py +++ b/sympy/assumptions/ask_generated.py @@ -1,19 +1,16 @@ """ -The contents of this file are the return value of -``sympy.assumptions.ask.compute_known_facts``. - Do NOT manually edit this file. Instead, run ./bin/ask_update.py. """ -from sympy.core.cache import cacheit -from sympy.assumptions.cnf import Literal from sympy.assumptions.ask import Q +from sympy.assumptions.cnf import Literal +from sympy.core.cache import cacheit @cacheit def get_all_known_facts(): """ - Known facts as CNF clauses. Used by satask. + Known facts between unary predicates as CNF clauses. """ return { frozenset((Literal(Q.algebraic, False), Literal(Q.imaginary, True), Literal(Q.transcendental, False))), @@ -83,102 +80,107 @@ def get_all_known_facts(): frozenset((Literal(Q.triangular, False), Literal(Q.upper_triangular, True))) } -# -{ Known facts in compressed sets }- @cacheit def get_known_facts_dict(): """ - Logical implication as dictionary. Key implies every item in its value. - Used for quick lookup of single facts. + Logical relations between unary predicates as dictionary. + + Each key is a predicate, and item is two groups of predicates. + First group contains the predicates which are implied by the key, and + second group contains the predicates which are rejected by the key. + """ return { - Q.algebraic: set([Q.algebraic, Q.commutative, Q.finite, ~Q.infinite, - ~Q.negative_infinite, ~Q.positive_infinite, - ~Q.transcendental]), - Q.antihermitian: set([Q.antihermitian]), - Q.commutative: set([Q.commutative]), - Q.complex_elements: set([Q.complex_elements]), - Q.composite: set([Q.algebraic, Q.commutative, Q.composite, Q.finite, - Q.hermitian, Q.positive, Q.rational, ~Q.imaginary, - ~Q.infinite, ~Q.irrational, ~Q.negative, ~Q.negative_infinite, - ~Q.positive_infinite, ~Q.prime, ~Q.transcendental, ~Q.zero]), - Q.diagonal: set([Q.diagonal, Q.lower_triangular, Q.normal, Q.square, - Q.symmetric, Q.triangular, Q.upper_triangular]), - Q.even: set([Q.algebraic, Q.commutative, Q.even, Q.finite, - Q.hermitian, Q.rational, ~Q.imaginary, ~Q.infinite, - ~Q.irrational, ~Q.negative_infinite, ~Q.odd, - ~Q.positive_infinite, ~Q.transcendental]), - Q.finite: set([Q.commutative, Q.finite, ~Q.infinite, - ~Q.negative_infinite, ~Q.positive_infinite]), - Q.fullrank: set([Q.fullrank]), - Q.hermitian: set([Q.hermitian]), - Q.imaginary: set([Q.antihermitian, Q.commutative, Q.finite, - Q.imaginary, ~Q.composite, ~Q.even, ~Q.infinite, - ~Q.irrational, ~Q.negative, ~Q.negative_infinite, ~Q.odd, - ~Q.positive, ~Q.positive_infinite, ~Q.prime, ~Q.rational, - ~Q.zero]), - Q.infinite: set([Q.commutative, Q.infinite, ~Q.algebraic, - ~Q.composite, ~Q.even, ~Q.finite, ~Q.imaginary, ~Q.irrational, - ~Q.negative, ~Q.odd, ~Q.positive, ~Q.prime, ~Q.rational, - ~Q.transcendental, ~Q.zero]), - Q.integer_elements: set([Q.complex_elements, Q.integer_elements, - Q.real_elements]), - Q.invertible: set([Q.fullrank, Q.invertible, Q.square, ~Q.singular]), - Q.irrational: set([Q.commutative, Q.finite, Q.hermitian, Q.irrational, - ~Q.composite, ~Q.even, ~Q.imaginary, ~Q.infinite, - ~Q.negative_infinite, ~Q.odd, ~Q.positive_infinite, ~Q.prime, - ~Q.rational, ~Q.zero]), - Q.is_true: set([Q.is_true]), - Q.lower_triangular: set([Q.lower_triangular, Q.triangular]), - Q.negative: set([Q.commutative, Q.finite, Q.hermitian, Q.negative, - ~Q.composite, ~Q.imaginary, ~Q.infinite, ~Q.negative_infinite, - ~Q.positive, ~Q.positive_infinite, ~Q.prime, ~Q.zero]), - Q.negative_infinite: set([Q.commutative, Q.infinite, - Q.negative_infinite, ~Q.algebraic, ~Q.composite, ~Q.even, - ~Q.finite, ~Q.imaginary, ~Q.irrational, ~Q.negative, ~Q.odd, - ~Q.positive, ~Q.positive_infinite, ~Q.prime, ~Q.rational, - ~Q.transcendental, ~Q.zero]), - Q.normal: set([Q.normal, Q.square]), - Q.odd: set([Q.algebraic, Q.commutative, Q.finite, Q.hermitian, Q.odd, - Q.rational, ~Q.even, ~Q.imaginary, ~Q.infinite, ~Q.irrational, - ~Q.negative_infinite, ~Q.positive_infinite, ~Q.transcendental, - ~Q.zero]), - Q.orthogonal: set([Q.fullrank, Q.invertible, Q.normal, Q.orthogonal, - Q.positive_definite, Q.square, Q.unitary, ~Q.singular]), - Q.positive: set([Q.commutative, Q.finite, Q.hermitian, Q.positive, - ~Q.imaginary, ~Q.infinite, ~Q.negative, ~Q.negative_infinite, - ~Q.positive_infinite, ~Q.zero]), - Q.positive_definite: set([Q.fullrank, Q.invertible, - Q.positive_definite, Q.square, ~Q.singular]), - Q.positive_infinite: set([Q.commutative, Q.infinite, - Q.positive_infinite, ~Q.algebraic, ~Q.composite, ~Q.even, - ~Q.finite, ~Q.imaginary, ~Q.irrational, ~Q.negative, - ~Q.negative_infinite, ~Q.odd, ~Q.positive, ~Q.prime, - ~Q.rational, ~Q.transcendental, ~Q.zero]), - Q.prime: set([Q.algebraic, Q.commutative, Q.finite, Q.hermitian, - Q.positive, Q.prime, Q.rational, ~Q.composite, ~Q.imaginary, - ~Q.infinite, ~Q.irrational, ~Q.negative, ~Q.negative_infinite, - ~Q.positive_infinite, ~Q.transcendental, ~Q.zero]), - Q.rational: set([Q.algebraic, Q.commutative, Q.finite, Q.hermitian, - Q.rational, ~Q.imaginary, ~Q.infinite, ~Q.irrational, - ~Q.negative_infinite, ~Q.positive_infinite, - ~Q.transcendental]), - Q.real_elements: set([Q.complex_elements, Q.real_elements]), - Q.singular: set([Q.singular, ~Q.invertible, ~Q.orthogonal, - ~Q.positive_definite, ~Q.unitary]), - Q.square: set([Q.square]), - Q.symmetric: set([Q.square, Q.symmetric]), - Q.transcendental: set([Q.commutative, Q.finite, Q.transcendental, - ~Q.algebraic, ~Q.composite, ~Q.even, ~Q.infinite, - ~Q.negative_infinite, ~Q.odd, ~Q.positive_infinite, ~Q.prime, - ~Q.rational, ~Q.zero]), - Q.triangular: set([Q.triangular]), - Q.unit_triangular: set([Q.triangular, Q.unit_triangular]), - Q.unitary: set([Q.fullrank, Q.invertible, Q.normal, Q.square, - Q.unitary, ~Q.singular]), - Q.upper_triangular: set([Q.triangular, Q.upper_triangular]), - Q.zero: set([Q.algebraic, Q.commutative, Q.even, Q.finite, - Q.hermitian, Q.rational, Q.zero, ~Q.composite, ~Q.imaginary, - ~Q.infinite, ~Q.irrational, ~Q.negative, ~Q.negative_infinite, - ~Q.odd, ~Q.positive, ~Q.positive_infinite, ~Q.prime, - ~Q.transcendental]), + Q.algebraic: (set([Q.algebraic, Q.commutative, Q.finite]), + set([Q.infinite, Q.negative_infinite, Q.positive_infinite, + Q.transcendental])), + Q.antihermitian: (set([Q.antihermitian]), set([])), + Q.commutative: (set([Q.commutative]), set([])), + Q.complex_elements: (set([Q.complex_elements]), set([])), + Q.composite: (set([Q.algebraic, Q.commutative, Q.composite, Q.finite, + Q.hermitian, Q.positive, Q.rational]), set([Q.imaginary, + Q.infinite, Q.irrational, Q.negative, Q.negative_infinite, + Q.positive_infinite, Q.prime, Q.transcendental, Q.zero])), + Q.diagonal: (set([Q.diagonal, Q.lower_triangular, Q.normal, Q.square, + Q.symmetric, Q.triangular, Q.upper_triangular]), set([])), + Q.even: (set([Q.algebraic, Q.commutative, Q.even, Q.finite, + Q.hermitian, Q.rational]), set([Q.imaginary, Q.infinite, + Q.irrational, Q.negative_infinite, Q.odd, Q.positive_infinite, + Q.transcendental])), + Q.finite: (set([Q.commutative, Q.finite]), set([Q.infinite, + Q.negative_infinite, Q.positive_infinite])), + Q.fullrank: (set([Q.fullrank]), set([])), + Q.hermitian: (set([Q.hermitian]), set([])), + Q.imaginary: (set([Q.antihermitian, Q.commutative, Q.finite, + Q.imaginary]), set([Q.composite, Q.even, Q.infinite, + Q.irrational, Q.negative, Q.negative_infinite, Q.odd, + Q.positive, Q.positive_infinite, Q.prime, Q.rational, + Q.zero])), + Q.infinite: (set([Q.commutative, Q.infinite]), set([Q.algebraic, + Q.composite, Q.even, Q.finite, Q.imaginary, Q.irrational, + Q.negative, Q.odd, Q.positive, Q.prime, Q.rational, + Q.transcendental, Q.zero])), + Q.integer_elements: (set([Q.complex_elements, Q.integer_elements, + Q.real_elements]), set([])), + Q.invertible: (set([Q.fullrank, Q.invertible, Q.square]), + set([Q.singular])), + Q.irrational: (set([Q.commutative, Q.finite, Q.hermitian, + Q.irrational]), set([Q.composite, Q.even, Q.imaginary, + Q.infinite, Q.negative_infinite, Q.odd, Q.positive_infinite, + Q.prime, Q.rational, Q.zero])), + Q.is_true: (set([Q.is_true]), set([])), + Q.lower_triangular: (set([Q.lower_triangular, Q.triangular]), set([])), + Q.negative: (set([Q.commutative, Q.finite, Q.hermitian, Q.negative]), + set([Q.composite, Q.imaginary, Q.infinite, + Q.negative_infinite, Q.positive, Q.positive_infinite, Q.prime, + Q.zero])), + Q.negative_infinite: (set([Q.commutative, Q.infinite, + Q.negative_infinite]), set([Q.algebraic, Q.composite, Q.even, + Q.finite, Q.imaginary, Q.irrational, Q.negative, Q.odd, + Q.positive, Q.positive_infinite, Q.prime, Q.rational, + Q.transcendental, Q.zero])), + Q.normal: (set([Q.normal, Q.square]), set([])), + Q.odd: (set([Q.algebraic, Q.commutative, Q.finite, Q.hermitian, Q.odd, + Q.rational]), set([Q.even, Q.imaginary, Q.infinite, + Q.irrational, Q.negative_infinite, Q.positive_infinite, + Q.transcendental, Q.zero])), + Q.orthogonal: (set([Q.fullrank, Q.invertible, Q.normal, Q.orthogonal, + Q.positive_definite, Q.square, Q.unitary]), set([Q.singular])), + Q.positive: (set([Q.commutative, Q.finite, Q.hermitian, Q.positive]), + set([Q.imaginary, Q.infinite, Q.negative, Q.negative_infinite, + Q.positive_infinite, Q.zero])), + Q.positive_definite: (set([Q.fullrank, Q.invertible, + Q.positive_definite, Q.square]), set([Q.singular])), + Q.positive_infinite: (set([Q.commutative, Q.infinite, + Q.positive_infinite]), set([Q.algebraic, Q.composite, Q.even, + Q.finite, Q.imaginary, Q.irrational, Q.negative, + Q.negative_infinite, Q.odd, Q.positive, Q.prime, Q.rational, + Q.transcendental, Q.zero])), + Q.prime: (set([Q.algebraic, Q.commutative, Q.finite, Q.hermitian, + Q.positive, Q.prime, Q.rational]), set([Q.composite, + Q.imaginary, Q.infinite, Q.irrational, Q.negative, + Q.negative_infinite, Q.positive_infinite, Q.transcendental, + Q.zero])), + Q.rational: (set([Q.algebraic, Q.commutative, Q.finite, Q.hermitian, + Q.rational]), set([Q.imaginary, Q.infinite, Q.irrational, + Q.negative_infinite, Q.positive_infinite, Q.transcendental])), + Q.real_elements: (set([Q.complex_elements, Q.real_elements]), set([])), + Q.singular: (set([Q.singular]), set([Q.invertible, Q.orthogonal, + Q.positive_definite, Q.unitary])), + Q.square: (set([Q.square]), set([])), + Q.symmetric: (set([Q.square, Q.symmetric]), set([])), + Q.transcendental: (set([Q.commutative, Q.finite, Q.transcendental]), + set([Q.algebraic, Q.composite, Q.even, Q.infinite, + Q.negative_infinite, Q.odd, Q.positive_infinite, Q.prime, + Q.rational, Q.zero])), + Q.triangular: (set([Q.triangular]), set([])), + Q.unit_triangular: (set([Q.triangular, Q.unit_triangular]), set([])), + Q.unitary: (set([Q.fullrank, Q.invertible, Q.normal, Q.square, + Q.unitary]), set([Q.singular])), + Q.upper_triangular: (set([Q.triangular, Q.upper_triangular]), set([])), + Q.zero: (set([Q.algebraic, Q.commutative, Q.even, Q.finite, + Q.hermitian, Q.rational, Q.zero]), set([Q.composite, + Q.imaginary, Q.infinite, Q.irrational, Q.negative, + Q.negative_infinite, Q.odd, Q.positive, Q.positive_infinite, + Q.prime, Q.transcendental])), } diff --git a/sympy/assumptions/facts.py b/sympy/assumptions/facts.py index e609d8a5dcce..58f98e9158cd 100644 --- a/sympy/assumptions/facts.py +++ b/sympy/assumptions/facts.py @@ -1,21 +1,23 @@ """ Known facts in assumptions module. -This module defines the facts in ``get_known_facts()``, and supports functions -to generate the contents in ``sympy.assumptions.ask_generated`` file. +This module defines the facts between unary predicates in ``get_known_facts()``, +and supports functions to generate the contents in +``sympy.assumptions.ask_generated`` file. """ -from sympy.core.cache import cacheit from sympy.assumptions import Q -from sympy.assumptions.cnf import CNF +from sympy.assumptions.assume import AppliedPredicate +from sympy.core.cache import cacheit +from sympy.core.symbol import Symbol from sympy.logic.boolalg import (to_cnf, And, Not, Implies, Equivalent) from sympy.logic.inference import satisfiable @cacheit def get_composite_predicates(): - # To reduce the complexity of sat solver, these predicates never goes into facts - # but are transformed into the combination of primitive predicates. + # To reduce the complexity of sat solver, these predicates are + # transformed into the combination of primitive predicates. return { Q.real : Q.negative | Q.zero | Q.positive, Q.integer : Q.even | Q.odd, @@ -33,81 +35,152 @@ def get_composite_predicates(): @cacheit -def get_known_facts(): - # We build the facts starting with primitive predicates. - # DO NOT include the predicates in get_composite_predicates()'s keys here! - return And( +def get_known_facts(x=None): + """ + Facts between unary predicates. + + Parameters + ========== + x : Symbol, optional + Placeholder symbol for unary facts. Default is ``Symbol('x')``. + + Returns + ======= + + fact : Known facts in conjugated normal form. + + """ + if x is None: + x = Symbol('x') + fact = And( + # primitive predicates for extended real exclude each other. + # finite/infinite ones already reject each other so don't add here. # primitive predicates exclude each other - Implies(Q.negative_infinite, ~Q.positive_infinite), - Implies(Q.negative, ~Q.zero & ~Q.positive), - Implies(Q.positive, ~Q.zero), + Implies(Q.negative_infinite(x), ~Q.positive_infinite(x)), + Implies(Q.negative(x), ~Q.zero(x) & ~Q.positive(x)), + Implies(Q.positive(x), ~Q.zero(x)), # build real line and complex plane - Implies(Q.negative | Q.zero | Q.positive, ~Q.imaginary), - Implies(Q.negative | Q.zero | Q.positive | Q.imaginary, Q.algebraic | Q.transcendental), + Implies(Q.negative(x) | Q.zero(x) | Q.positive(x), ~Q.imaginary(x)), + Implies(Q.negative(x) | Q.zero(x) | Q.positive(x) | Q.imaginary(x), Q.algebraic(x) | Q.transcendental(x)), # other subsets of complex - Implies(Q.transcendental, ~Q.algebraic), - Implies(Q.irrational, ~Q.rational), - Equivalent(Q.rational | Q.irrational, Q.negative | Q.zero | Q.positive), - Implies(Q.rational, Q.algebraic), + Implies(Q.transcendental(x), ~Q.algebraic(x)), + Implies(Q.irrational(x), ~Q.rational(x)), + Equivalent(Q.rational(x) | Q.irrational(x), Q.negative(x) | Q.zero(x) | Q.positive(x)), + Implies(Q.rational(x), Q.algebraic(x)), # integers - Implies(Q.even, ~Q.odd), - Implies(Q.even | Q.odd, Q.rational), - Implies(Q.zero, Q.even), - Implies(Q.composite, ~Q.prime), - Implies(Q.composite | Q.prime, (Q.even | Q.odd) & Q.positive), - Implies(Q.even & Q.positive & ~Q.prime, Q.composite), + Implies(Q.even(x), ~Q.odd(x)), + Implies(Q.even(x) | Q.odd(x), Q.rational(x)), + Implies(Q.zero(x), Q.even(x)), + Implies(Q.composite(x), ~Q.prime(x)), + Implies(Q.composite(x) | Q.prime(x), (Q.even(x) | Q.odd(x)) & Q.positive(x)), + Implies(Q.even(x) & Q.positive(x) & ~Q.prime(x), Q.composite(x)), # hermitian and antihermitian - Implies(Q.negative | Q.zero | Q.positive, Q.hermitian), - Implies(Q.imaginary, Q.antihermitian), - Implies(Q.zero, Q.hermitian | Q.antihermitian), + Implies(Q.negative(x) | Q.zero(x) | Q.positive(x), Q.hermitian(x)), + Implies(Q.imaginary(x), Q.antihermitian(x)), + Implies(Q.zero(x), Q.hermitian(x) | Q.antihermitian(x)), # define finity and infinity, and build extended real line - Implies(Q.infinite, ~Q.finite), - Implies(Q.algebraic | Q.transcendental, Q.finite), - Implies(Q.negative_infinite | Q.positive_infinite, Q.infinite), + Implies(Q.infinite(x), ~Q.finite(x)), + Implies(Q.algebraic(x) | Q.transcendental(x), Q.finite(x)), + Implies(Q.negative_infinite(x) | Q.positive_infinite(x), Q.infinite(x)), # commutativity - Implies(Q.finite | Q.infinite, Q.commutative), + Implies(Q.finite(x) | Q.infinite(x), Q.commutative(x)), # matrices - Implies(Q.orthogonal, Q.positive_definite), - Implies(Q.orthogonal, Q.unitary), - Implies(Q.unitary & Q.real_elements, Q.orthogonal), - Implies(Q.unitary, Q.normal), - Implies(Q.unitary, Q.invertible), - Implies(Q.normal, Q.square), - Implies(Q.diagonal, Q.normal), - Implies(Q.positive_definite, Q.invertible), - Implies(Q.diagonal, Q.upper_triangular), - Implies(Q.diagonal, Q.lower_triangular), - Implies(Q.lower_triangular, Q.triangular), - Implies(Q.upper_triangular, Q.triangular), - Implies(Q.triangular, Q.upper_triangular | Q.lower_triangular), - Implies(Q.upper_triangular & Q.lower_triangular, Q.diagonal), - Implies(Q.diagonal, Q.symmetric), - Implies(Q.unit_triangular, Q.triangular), - Implies(Q.invertible, Q.fullrank), - Implies(Q.invertible, Q.square), - Implies(Q.symmetric, Q.square), - Implies(Q.fullrank & Q.square, Q.invertible), - Equivalent(Q.invertible, ~Q.singular), - Implies(Q.integer_elements, Q.real_elements), - Implies(Q.real_elements, Q.complex_elements), + Implies(Q.orthogonal(x), Q.positive_definite(x)), + Implies(Q.orthogonal(x), Q.unitary(x)), + Implies(Q.unitary(x) & Q.real_elements(x), Q.orthogonal(x)), + Implies(Q.unitary(x), Q.normal(x)), + Implies(Q.unitary(x), Q.invertible(x)), + Implies(Q.normal(x), Q.square(x)), + Implies(Q.diagonal(x), Q.normal(x)), + Implies(Q.positive_definite(x), Q.invertible(x)), + Implies(Q.diagonal(x), Q.upper_triangular(x)), + Implies(Q.diagonal(x), Q.lower_triangular(x)), + Implies(Q.lower_triangular(x), Q.triangular(x)), + Implies(Q.upper_triangular(x), Q.triangular(x)), + Implies(Q.triangular(x), Q.upper_triangular(x) | Q.lower_triangular(x)), + Implies(Q.upper_triangular(x) & Q.lower_triangular(x), Q.diagonal(x)), + Implies(Q.diagonal(x), Q.symmetric(x)), + Implies(Q.unit_triangular(x), Q.triangular(x)), + Implies(Q.invertible(x), Q.fullrank(x)), + Implies(Q.invertible(x), Q.square(x)), + Implies(Q.symmetric(x), Q.square(x)), + Implies(Q.fullrank(x) & Q.square(x), Q.invertible(x)), + Equivalent(Q.invertible(x), ~Q.singular(x)), + Implies(Q.integer_elements(x), Q.real_elements(x)), + Implies(Q.real_elements(x), Q.complex_elements(x)), ) + return fact + + +def generate_known_facts_dict(keys, fact): + """ + Computes and returns a dictionary which contains the relations between + unary predicates. + + Each key is a predicate, and item is two groups of predicates. + First group contains the predicates which are implied by the key, and + second group contains the predicates which are rejected by the key. + + All predicates in *keys* and *fact* must be unary and have same placeholder + symbol. + + Parameters + ========== + + keys : list of AppliedPredicate instances. + + fact : Fact between predicates in conjugated normal form. + + Examples + ======== + + >>> from sympy import Q + >>> from sympy.assumptions.facts import generate_known_facts_dict + >>> from sympy.logic.boolalg import And, Implies + >>> from sympy.abc import x + >>> keys = [Q.even(x), Q.odd(x), Q.zero(x)] + >>> fact = And(Implies(Q.even(x), ~Q.odd(x)), + ... Implies(Q.zero(x), Q.even(x))) + >>> generate_known_facts_dict(keys, fact) + {Q.even: ({Q.even}, {Q.odd}), + Q.odd: ({Q.odd}, {Q.even, Q.zero}), + Q.zero: ({Q.even, Q.zero}, {Q.odd})} + """ + fact_cnf = to_cnf(fact) + mapping = single_fact_lookup(keys, fact_cnf) + + ret = {} + for key, value in mapping.items(): + implied = set() + rejected = set() + for expr in value: + if isinstance(expr, AppliedPredicate): + implied.add(expr.function) + elif isinstance(expr, Not): + pred = expr.args[0] + rejected.add(pred.function) + ret[key.function] = (implied, rejected) + return ret @cacheit def get_known_facts_keys(): + """ + Return the unapplied unary predicates. + """ exclude = set() for pred in get_composite_predicates(): exclude.add(pred) for pred in [Q.eq, Q.ne, Q.gt, Q.lt, Q.ge, Q.le]: - # sat does not support polyadic predicates yet + # exclude polyadic predicates exclude.add(pred) result = [] @@ -121,71 +194,6 @@ def get_known_facts_keys(): return result -def compute_known_facts(known_facts, known_facts_keys): - """Compute the various forms of knowledge compilation used by the - assumptions system. - - Explanation - =========== - - This function is typically applied to the results of the ``get_known_facts`` - and ``get_known_facts_keys`` functions defined at the bottom of - this file. - """ - from textwrap import dedent, wrap - - fact_string = dedent('''\ - """ - The contents of this file are the return value of - ``sympy.assumptions.ask.compute_known_facts``. - - Do NOT manually edit this file. - Instead, run ./bin/ask_update.py. - """ - - from sympy.core.cache import cacheit - from sympy.assumptions.cnf import Literal - from sympy.assumptions.ask import Q - - @cacheit - def get_all_known_facts(): - """ - Known facts as CNF clauses. Used by satask. - """ - return { - %s - } - - # -{ Known facts in compressed sets }- - @cacheit - def get_known_facts_dict(): - """ - Logical implication as dictionary. Key implies every item in its value. - Used for quick lookup of single facts. - """ - return { - %s - } - ''') - # Compute the known facts in CNF form for logical inference - LINE = ",\n " - HANG = ' '*8 - cnf = to_cnf(known_facts) - cnf_ = CNF.to_CNF(known_facts) - - p = LINE.join(sorted(['frozenset((' + ', '.join(str(lit) for lit in sorted(clause, key=str)) +'))' for clause in cnf_.clauses])) - mapping = single_fact_lookup(known_facts_keys, cnf) - items = sorted(mapping.items(), key=str) - keys = [str(i[0]) for i in items] - values = ['set(%s)' % sorted(i[1], key=str) for i in items] - m = LINE.join(['\n'.join( - wrap("{}: {}".format(k, v), - subsequent_indent=HANG, - break_long_words=False)) - for k, v in zip(keys, values)]) + ',' - return fact_string % (p, m) - - def single_fact_lookup(known_facts_keys, known_facts_cnf): # Return the dictionary for quick lookup of single fact mapping = {} diff --git a/sympy/assumptions/satask.py b/sympy/assumptions/satask.py index 9d6ee2c19e17..f2a4563dc422 100644 --- a/sympy/assumptions/satask.py +++ b/sympy/assumptions/satask.py @@ -39,8 +39,8 @@ def satask(proposition, assumptions=True, context=global_assumptions, this is ``sympy.assumptions.global_assumptions`` variable. use_known_facts : bool, optional. - If ``True``, facts from ``sympy.assumptions.ask_generated`` module - are passed to SAT solver as well. + If ``True``, facts from ``sympy.assumptions.ask_generated`` + module are passed to SAT solver as well. iterations : int, optional. Number of times that relevant facts are recursively extracted. @@ -285,8 +285,8 @@ def get_all_relevant_facts(proposition, assumptions, context, CNF generated from assumptions context. use_known_facts : bool, optional. - If ``True``, facts from ``sympy.assumptions.ask_generated`` module - are encoded as well. + If ``True``, facts from ``sympy.assumptions.ask_generated`` + module are encoded as well. iterations : int, optional. Number of times that relevant facts are recursively extracted. diff --git a/sympy/assumptions/tests/test_query.py b/sympy/assumptions/tests/test_query.py index 39724c407d43..d0648472972e 100644 --- a/sympy/assumptions/tests/test_query.py +++ b/sympy/assumptions/tests/test_query.py @@ -2,8 +2,12 @@ from sympy.assumptions import (ask, AssumptionsContext, Q, register_handler, remove_handler) from sympy.assumptions.assume import assuming, global_assumptions, Predicate -from sympy.assumptions.facts import compute_known_facts, single_fact_lookup +from sympy.assumptions.cnf import CNF, Literal +from sympy.assumptions.facts import (single_fact_lookup, + get_known_facts, generate_known_facts_dict, get_known_facts_keys) from sympy.assumptions.handlers import AskHandler +from sympy.assumptions.ask_generated import (get_all_known_facts, + get_known_facts_dict) from sympy.core.add import Add from sympy.core.numbers import (I, Integer, Rational, oo, zoo, pi) from sympy.core.singleton import S @@ -2135,24 +2139,34 @@ def test_single_fact_lookup(): assert mapping[Q.rational] == {Q.real, Q.rational, Q.complex} -def test_compute_known_facts(): - known_facts = And(Implies(Q.integer, Q.rational), - Implies(Q.rational, Q.real), - Implies(Q.real, Q.complex)) - known_facts_keys = {Q.integer, Q.rational, Q.real, Q.complex} +def test_generate_known_facts_dict(): + known_facts = And(Implies(Q.integer(x), Q.rational(x)), + Implies(Q.rational(x), Q.real(x)), + Implies(Q.real(x), Q.complex(x))) + known_facts_keys = {Q.integer(x), Q.rational(x), Q.real(x), Q.complex(x)} - compute_known_facts(known_facts, known_facts_keys) + assert generate_known_facts_dict(known_facts_keys, known_facts) == \ + {Q.complex: ({Q.complex}, set()), + Q.integer: ({Q.complex, Q.integer, Q.rational, Q.real}, set()), + Q.rational: ({Q.complex, Q.rational, Q.real}, set()), + Q.real: ({Q.complex, Q.real}, set())} @slow def test_known_facts_consistent(): """"Test that ask_generated.py is up-to-date""" - from sympy.assumptions.facts import get_known_facts, get_known_facts_keys - from os.path import abspath, dirname, join - filename = join(dirname(dirname(abspath(__file__))), 'ask_generated.py') - with open(filename) as f: - assert f.read() == \ - compute_known_facts(get_known_facts(), get_known_facts_keys()) + x = Symbol('x') + fact = get_known_facts(x) + # test cnf clauses of fact between unary predicates + cnf = CNF.to_CNF(fact) + clauses = set() + for cl in cnf.clauses: + clauses.add(frozenset(Literal(lit.arg.function, lit.is_Not) for lit in sorted(cl, key=str))) + assert get_all_known_facts() == clauses + # test dictionary of fact between unary predicates + keys = [pred(x) for pred in get_known_facts_keys()] + mapping = generate_known_facts_dict(keys, fact) + assert get_known_facts_dict() == mapping def test_Add_queries():