On Wed, Jun 10, 2009 at 9:20 AM, Fabian Pedregosa<fab...@fseoane.net> wrote:
>
> This is a replacement for sympy.core.logic and will be used
> extensively by the query module. The old logic module can be
> removed once the old assumption system is removed.
The code is good, tests are ok, but please try to add more doctests,
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:
>
> 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
Add couple doctests
> + """
> + 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"""
Add couple doctests
> + �...@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):
Add couple doctests
> + �...@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"""
Add couple doctests
> + �...@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):
Add couple doctests
> + 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.
Add couple doctests
> + """
> + 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 | ...) & ...)
Add couple doctests
> + """
> + 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.
Add couple doctests
> + """
> + 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
Add couple doctests
> + """
> + 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."
Add couple doctests
> +
> + 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
>
>
> >
>
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups
"sympy-patches" group.
To post to this group, send email to sympy-patches@googlegroups.com
To unsubscribe from this group, send email to
sympy-patches+unsubscr...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/sympy-patches?hl=en
-~----------~----~----~----~------~----~------~--~---
