Also, how does this module compare to the assumptions logic module
that we already have in
sympy/core/facts.py
? Is it a duplicate functionality, or a new functionality, etc.? Is
it better/worse, what are your plans with facts.py (should we remove
it or maintain both)?
Ondrej
On Wed, Jun 10, 2009 at 11:41 AM, Ondrej Certik<ond...@certik.cz> wrote:
> 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
-~----------~----~----~----~------~----~------~--~---
