refact(assump) : parametrize the facts

Parametrize get_known_facts()
Enhance generate_code()
Modify facts

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)

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)

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])),
     }