forked from sympy/sympy
-
Notifications
You must be signed in to change notification settings - Fork 1
/
boolalg.py
executable file
·208 lines (188 loc) · 6.23 KB
/
boolalg.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
"""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):
"""Logical AND function.
It evaluates its arguments in order, giving False immediately if any of them
are False, and True if they are all True.
Examples:
>>> from sympy import *
>>> x, y = symbols('xy')
>>> x & y
And(x, y)
"""
@classmethod
def eval(cls, *args):
out_args = []
for arg in 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):
"""Logical OR function
It evaluates its arguments in order, giving True immediately if any of them are
True, and False if they are all False.
"""
@classmethod
def eval(cls, *args):
out_args = []
for arg in 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 Xor(BooleanFunction):
"""Logical XOR (exclusive OR) function.
returns True if an odd number of the arguments are True, and the rest are False.
returns False if an even number of the arguments are True, and the rest are False.
"""
@classmethod
def eval(cls, *args):
if not args: return False
args = list(args)
A = args.pop()
while args:
B = args.pop()
A = Or(A & Not(B), (Not(A) & B))
return A
class Not(BooleanFunction):
"""Logical Not function (negation)
Note: De Morgan rules applied automatically"""
@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):
return arg.args[0]
class Nand(BooleanFunction):
"""Logical NAND function.
It evaluates its arguments in order, giving True immediately if any
of them are False, and False if they are all True.
"""
@classmethod
def eval(cls, *args):
if not args: return False
args = list(args)
A = Not(args.pop())
while args:
B = args.pop()
A = Or(A, Not(B))
return A
class Nor(BooleanFunction):
"""Logical NOR function.
It evaluates its arguments in order, giving False immediately if any
of them are True, and True if they are all False.
"""
@classmethod
def eval(cls, *args):
if not args: return False
args = list(args)
A = Not(args.pop())
while args:
B = args.pop()
A = And(A, Not(B))
return A
class Implies(BooleanFunction):
pass
class Equivalent(BooleanFunction):
"""Equivalence relation.
Equivalent(A, B) is True if and only if A and B are both True or both False
"""
@classmethod
def eval(cls, *args):
return Basic.__new__(cls, *sorted(args))
### 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.
"""
if isinstance(expr, Or):
for arg in expr.args:
if isinstance(arg, And):
conj = arg
break
else: return type(expr)(*expr.args)
rest = Or(*[a for a in expr.args if a is not conj])
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 | ...) & ...)
"""
expr = sympify(expr)
expr = eliminate_implications(expr)
return distribute_and_over_or(expr)
def eliminate_implications(expr):
"""Change >>, <<, and Equivalent into &, |, and ~. That is, return an
expression that is equivalent to s, but has only &, |, and ~ as logical
operators.
"""
expr = sympify(expr)
if expr.is_Atom: return expr ## (Atoms are unchanged.)
args = map(eliminate_implications, expr.args)
a, b = args[0], args[-1]
if isinstance(expr, Implies):
return (~a) | b
elif isinstance(expr, Equivalent):
return (a | Not(b)) & (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
TODO: can this be replaced by sympify ?
"""
import re
return eval(re.sub(r'([a-zA-Z0-9_.]+)', r'Symbol("\1")', s), {'Symbol' : Symbol})