""" Boolean algebra module for SymPy """ from collections import defaultdict from itertools import chain, combinations, product from sympy.core.add import Add from sympy.core.basic import Basic from sympy.core.cache import cacheit from sympy.core.compatibility import ordered, as_int from sympy.core.decorators import sympify_method_args, sympify_return from sympy.core.function import Application, Derivative from sympy.core.numbers import Number from sympy.core.operations import LatticeOp from sympy.core.singleton import Singleton, S from sympy.core.sympify import converter, _sympify, sympify from sympy.core.kind import BooleanKind from sympy.utilities.iterables import sift, ibin from sympy.utilities.misc import filldedent def as_Boolean(e): """Like bool, return the Boolean value of an expression, e, which can be any instance of Boolean or bool. Examples ======== >>> from sympy import true, false, nan >>> from sympy.logic.boolalg import as_Boolean >>> from sympy.abc import x >>> as_Boolean(0) is false True >>> as_Boolean(1) is true True >>> as_Boolean(x) x >>> as_Boolean(2) Traceback (most recent call last): ... TypeError: expecting bool or Boolean, not `2`. >>> as_Boolean(nan) Traceback (most recent call last): ... TypeError: expecting bool or Boolean, not `nan`. """ from sympy.core.symbol import Symbol if e == True: return S.true if e == False: return S.false if isinstance(e, Symbol): z = e.is_zero if z is None: return e return S.false if z else S.true if isinstance(e, Boolean): return e raise TypeError('expecting bool or Boolean, not `%s`.' % e) @sympify_method_args class Boolean(Basic): """A boolean object is an object for which logic operations make sense.""" __slots__ = () kind = BooleanKind @sympify_return([('other', 'Boolean')], NotImplemented) def __and__(self, other): return And(self, other) __rand__ = __and__ @sympify_return([('other', 'Boolean')], NotImplemented) def __or__(self, other): return Or(self, other) __ror__ = __or__ def __invert__(self): """Overloading for ~""" return Not(self) @sympify_return([('other', 'Boolean')], NotImplemented) def __rshift__(self, other): return Implies(self, other) @sympify_return([('other', 'Boolean')], NotImplemented) def __lshift__(self, other): return Implies(other, self) __rrshift__ = __lshift__ __rlshift__ = __rshift__ @sympify_return([('other', 'Boolean')], NotImplemented) def __xor__(self, other): return Xor(self, other) __rxor__ = __xor__ def equals(self, other): """ Returns True if the given formulas have the same truth table. For two formulas to be equal they must have the same literals. Examples ======== >>> from sympy.abc import A, B, C >>> from sympy.logic.boolalg import And, Or, Not >>> (A >> B).equals(~B >> ~A) True >>> Not(And(A, B, C)).equals(And(Not(A), Not(B), Not(C))) False >>> Not(And(A, Not(A))).equals(Or(B, Not(B))) False """ from sympy.logic.inference import satisfiable from sympy.core.relational import Relational if self.has(Relational) or other.has(Relational): raise NotImplementedError('handling of relationals') return self.atoms() == other.atoms() and \ not satisfiable(Not(Equivalent(self, other))) def to_nnf(self, simplify=True): # override where necessary return self def as_set(self): """ Rewrites Boolean expression in terms of real sets. Examples ======== >>> from sympy import Symbol, Eq, Or, And >>> x = Symbol('x', real=True) >>> Eq(x, 0).as_set() {0} >>> (x > 0).as_set() Interval.open(0, oo) >>> And(-2 < x, x < 2).as_set() Interval.open(-2, 2) >>> Or(x < -2, 2 < x).as_set() Union(Interval.open(-oo, -2), Interval.open(2, oo)) """ from sympy.calculus.util import periodicity from sympy.core.relational import Relational free = self.free_symbols if len(free) == 1: x = free.pop() reps = {} for r in self.atoms(Relational): if periodicity(r, x) not in (0, None): s = r._eval_as_set() if s in (S.EmptySet, S.UniversalSet, S.Reals): reps[r] = s.as_relational(x) continue raise NotImplementedError(filldedent(''' as_set is not implemented for relationals with periodic solutions ''')) return self.subs(reps)._eval_as_set() else: raise NotImplementedError("Sorry, as_set has not yet been" " implemented for multivariate" " expressions") @property def binary_symbols(self): from sympy.core.relational import Eq, Ne return set().union(*[i.binary_symbols for i in self.args if i.is_Boolean or i.is_Symbol or isinstance(i, (Eq, Ne))]) def _eval_refine(self, assumptions): from sympy.assumptions import ask ret = ask(self, assumptions) if ret is True: return true elif ret is False: return false return None class BooleanAtom(Boolean): """ Base class of BooleanTrue and BooleanFalse. """ is_Boolean = True is_Atom = True _op_priority = 11 # higher than Expr def simplify(self, *a, **kw): return self def expand(self, *a, **kw): return self @property def canonical(self): return self def _noop(self, other=None): raise TypeError('BooleanAtom not allowed in this context.') __add__ = _noop __radd__ = _noop __sub__ = _noop __rsub__ = _noop __mul__ = _noop __rmul__ = _noop __pow__ = _noop __rpow__ = _noop __truediv__ = _noop __rtruediv__ = _noop __mod__ = _noop __rmod__ = _noop _eval_power = _noop # /// drop when Py2 is no longer supported def __lt__(self, other): raise TypeError(filldedent(''' A Boolean argument can only be used in Eq and Ne; all other relationals expect real expressions. ''')) __le__ = __lt__ __gt__ = __lt__ __ge__ = __lt__ # \\\ class BooleanTrue(BooleanAtom, metaclass=Singleton): """ SymPy version of True, a singleton that can be accessed via S.true. This is the SymPy version of True, for use in the logic module. The primary advantage of using true instead of True is that shorthand boolean operations like ~ and >> will work as expected on this class, whereas with True they act bitwise on 1. Functions in the logic module will return this class when they evaluate to true. Notes ===== There is liable to be some confusion as to when ``True`` should be used and when ``S.true`` should be used in various contexts throughout SymPy. An important thing to remember is that ``sympify(True)`` returns ``S.true``. This means that for the most part, you can just use ``True`` and it will automatically be converted to ``S.true`` when necessary, similar to how you can generally use 1 instead of ``S.One``. The rule of thumb is: "If the boolean in question can be replaced by an arbitrary symbolic ``Boolean``, like ``Or(x, y)`` or ``x > 1``, use ``S.true``. Otherwise, use ``True``" In other words, use ``S.true`` only on those contexts where the boolean is being used as a symbolic representation of truth. For example, if the object ends up in the ``.args`` of any expression, then it must necessarily be ``S.true`` instead of ``True``, as elements of ``.args`` must be ``Basic``. On the other hand, ``==`` is not a symbolic operation in SymPy, since it always returns ``True`` or ``False``, and does so in terms of structural equality rather than mathematical, so it should return ``True``. The assumptions system should use ``True`` and ``False``. Aside from not satisfying the above rule of thumb, the assumptions system uses a three-valued logic (``True``, ``False``, ``None``), whereas ``S.true`` and ``S.false`` represent a two-valued logic. When in doubt, use ``True``. "``S.true == True is True``." While "``S.true is True``" is ``False``, "``S.true == True``" is ``True``, so if there is any doubt over whether a function or expression will return ``S.true`` or ``True``, just use ``==`` instead of ``is`` to do the comparison, and it will work in either case. Finally, for boolean flags, it's better to just use ``if x`` instead of ``if x is True``. To quote PEP 8: Don't compare boolean values to ``True`` or ``False`` using ``==``. * Yes: ``if greeting:`` * No: ``if greeting == True:`` * Worse: ``if greeting is True:`` Examples ======== >>> from sympy import sympify, true, false, Or >>> sympify(True) True >>> _ is True, _ is true (False, True) >>> Or(true, false) True >>> _ is true True Python operators give a boolean result for true but a bitwise result for True >>> ~true, ~True (False, -2) >>> true >> true, True >> True (True, 0) Python operators give a boolean result for true but a bitwise result for True >>> ~true, ~True (False, -2) >>> true >> true, True >> True (True, 0) See Also ======== sympy.logic.boolalg.BooleanFalse """ def __bool__(self): return True def __hash__(self): return hash(True) @property def negated(self): return S.false def as_set(self): """ Rewrite logic operators and relationals in terms of real sets. Examples ======== >>> from sympy import true >>> true.as_set() UniversalSet """ return S.UniversalSet class BooleanFalse(BooleanAtom, metaclass=Singleton): """ SymPy version of False, a singleton that can be accessed via S.false. This is the SymPy version of False, for use in the logic module. The primary advantage of using false instead of False is that shorthand boolean operations like ~ and >> will work as expected on this class, whereas with False they act bitwise on 0. Functions in the logic module will return this class when they evaluate to false. Notes ====== See the notes section in :py:class:`sympy.logic.boolalg.BooleanTrue` Examples ======== >>> from sympy import sympify, true, false, Or >>> sympify(False) False >>> _ is False, _ is false (False, True) >>> Or(true, false) True >>> _ is true True Python operators give a boolean result for false but a bitwise result for False >>> ~false, ~False (True, -1) >>> false >> false, False >> False (True, 0) See Also ======== sympy.logic.boolalg.BooleanTrue """ def __bool__(self): return False def __hash__(self): return hash(False) @property def negated(self): return S.true def as_set(self): """ Rewrite logic operators and relationals in terms of real sets. Examples ======== >>> from sympy import false >>> false.as_set() EmptySet """ return S.EmptySet true = BooleanTrue() false = BooleanFalse() # We want S.true and S.false to work, rather than S.BooleanTrue and # S.BooleanFalse, but making the class and instance names the same causes some # major issues (like the inability to import the class directly from this # file). S.true = true S.false = false converter[bool] = lambda x: S.true if x else S.false class BooleanFunction(Application, Boolean): """Boolean function is a function that lives in a boolean space It is used as base class for And, Or, Not, etc. """ is_Boolean = True def _eval_simplify(self, **kwargs): rv = self.func(*[a.simplify(**kwargs) for a in self.args]) return simplify_logic(rv) def simplify(self, **kwargs): from sympy.simplify.simplify import simplify return simplify(self, **kwargs) def __lt__(self, other): raise TypeError(filldedent(''' A Boolean argument can only be used in Eq and Ne; all other relationals expect real expressions. ''')) __le__ = __lt__ __ge__ = __lt__ __gt__ = __lt__ @classmethod def binary_check_and_simplify(self, *args): from sympy.core.relational import Relational, Eq, Ne args = [as_Boolean(i) for i in args] bin_syms = set().union(*[i.binary_symbols for i in args]) rel = set().union(*[i.atoms(Relational) for i in args]) reps = {} for x in bin_syms: for r in rel: if x in bin_syms and x in r.free_symbols: if isinstance(r, (Eq, Ne)): if not ( S.true in r.args or S.false in r.args): reps[r] = S.false else: raise TypeError(filldedent(''' Incompatible use of binary symbol `%s` as a real variable in `%s` ''' % (x, r))) return [i.subs(reps) for i in args] def to_nnf(self, simplify=True): return self._to_nnf(*self.args, simplify=simplify) def to_anf(self, deep=True): return self._to_anf(*self.args, deep=deep) @classmethod def _to_nnf(cls, *args, **kwargs): simplify = kwargs.get('simplify', True) argset = set() for arg in args: if not is_literal(arg): arg = arg.to_nnf(simplify) if simplify: if isinstance(arg, cls): arg = arg.args else: arg = (arg,) for a in arg: if Not(a) in argset: return cls.zero argset.add(a) else: argset.add(arg) return cls(*argset) @classmethod def _to_anf(cls, *args, **kwargs): deep = kwargs.get('deep', True) argset = set() for arg in args: if deep: if not is_literal(arg) or isinstance(arg, Not): arg = arg.to_anf(deep=deep) argset.add(arg) else: argset.add(arg) return cls(*argset, remove_true=False) # the diff method below is copied from Expr class def diff(self, *symbols, **assumptions): assumptions.setdefault("evaluate", True) return Derivative(self, *symbols, **assumptions) def _eval_derivative(self, x): if x in self.binary_symbols: from sympy.core.relational import Eq from sympy.functions.elementary.piecewise import Piecewise return Piecewise( (0, Eq(self.subs(x, 0), self.subs(x, 1))), (1, True)) elif x in self.free_symbols: # not implemented, see https://www.encyclopediaofmath.org/ # index.php/Boolean_differential_calculus pass else: return S.Zero def _apply_patternbased_simplification(self, rv, patterns, measure, dominatingvalue, replacementvalue=None): """ Replace patterns of Relational Parameters ========== rv : Expr Boolean expression patterns : tuple Tuple of tuples, with (pattern to simplify, simplified pattern) measure : function Simplification measure dominatingvalue : boolean or None The dominating value for the function of consideration. For example, for And S.false is dominating. As soon as one expression is S.false in And, the whole expression is S.false. replacementvalue : boolean or None, optional The resulting value for the whole expression if one argument evaluates to dominatingvalue. For example, for Nand S.false is dominating, but in this case the resulting value is S.true. Default is None. If replacementvalue is None and dominatingvalue is not None, replacementvalue = dominatingvalue """ from sympy.core.relational import Relational, _canonical from sympy.functions.elementary.miscellaneous import Min, Max if replacementvalue is None and dominatingvalue is not None: replacementvalue = dominatingvalue # Use replacement patterns for Relationals changed = True Rel, nonRel = sift(rv.args, lambda i: isinstance(i, Relational), binary=True) if len(Rel) <= 1: return rv Rel, nonRealRel = sift(Rel, lambda i: all(s.is_real is not False for s in i.free_symbols), binary=True) Rel = [i.canonical for i in Rel] while changed and len(Rel) >= 2: changed = False # Sort based on ordered Rel = list(ordered(Rel)) # Create a list of possible replacements results = [] # Try all combinations for ((i, pi), (j, pj)) in combinations(enumerate(Rel), 2): for pattern, simp in patterns: res = [] # use SymPy matching oldexpr = rv.func(pi, pj) tmpres = oldexpr.match(pattern) if tmpres: res.append((tmpres, oldexpr)) # Try reversing first relational # This and the rest should not be required with a better # canonical oldexpr = rv.func(pi.reversed, pj) tmpres = oldexpr.match(pattern) if tmpres: res.append((tmpres, oldexpr)) # Try reversing second relational oldexpr = rv.func(pi, pj.reversed) tmpres = oldexpr.match(pattern) if tmpres: res.append((tmpres, oldexpr)) # Try reversing both relationals oldexpr = rv.func(pi.reversed, pj.reversed) tmpres = oldexpr.match(pattern) if tmpres: res.append((tmpres, oldexpr)) if res: for tmpres, oldexpr in res: # we have a matching, compute replacement np = simp.subs(tmpres) if np == dominatingvalue: # if dominatingvalue, the whole expression # will be replacementvalue return replacementvalue # add replacement if not isinstance(np, ITE) and not np.has(Min, Max): # We only want to use ITE and Min/Max # replacements if they simplify away costsaving = measure(oldexpr) - measure(np) if costsaving > 0: results.append((costsaving, (i, j, np))) if results: # Sort results based on complexity results = list(reversed(sorted(results, key=lambda pair: pair[0]))) # Replace the one providing most simplification replacement = results[0][1] i, j, newrel = replacement # Remove the old relationals del Rel[j] del Rel[i] if dominatingvalue is None or newrel != ~dominatingvalue: # Insert the new one (no need to insert a value that will # not affect the result) Rel.append(newrel) # We did change something so try again changed = True rv = rv.func(*([_canonical(i) for i in ordered(Rel)] + nonRel + nonRealRel)) return rv class And(LatticeOp, 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.abc import x, y >>> from sympy.logic.boolalg import And >>> x & y x & y Notes ===== The ``&`` operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise and. Hence, ``And(a, b)`` and ``a & b`` will return different things if ``a`` and ``b`` are integers. >>> And(x, y).subs(x, 1) y """ zero = false identity = true nargs = None @classmethod def _new_args_filter(cls, args): args = BooleanFunction.binary_check_and_simplify(*args) args = LatticeOp._new_args_filter(args, And) newargs = [] rel = set() for x in ordered(args): if x.is_Relational: c = x.canonical if c in rel: continue elif c.negated.canonical in rel: return [S.false] else: rel.add(c) newargs.append(x) return newargs def _eval_subs(self, old, new): args = [] bad = None for i in self.args: try: i = i.subs(old, new) except TypeError: # store TypeError if bad is None: bad = i continue if i == False: return S.false elif i != True: args.append(i) if bad is not None: # let it raise bad.subs(old, new) # If old is And, replace the parts of the arguments with new if all # are there if isinstance(old, And): old_set = set(old.args) if old_set.issubset(args): args = set(args) - old_set args.add(new) return self.func(*args) def _eval_simplify(self, **kwargs): from sympy.core.relational import Equality, Relational from sympy.solvers.solveset import linear_coeffs # standard simplify rv = super()._eval_simplify(**kwargs) if not isinstance(rv, And): return rv # simplify args that are equalities involving # symbols so x == 0 & x == y -> x==0 & y == 0 Rel, nonRel = sift(rv.args, lambda i: isinstance(i, Relational), binary=True) if not Rel: return rv eqs, other = sift(Rel, lambda i: isinstance(i, Equality), binary=True) measure = kwargs['measure'] if eqs: ratio = kwargs['ratio'] reps = {} sifted = {} # group by length of free symbols sifted = sift(ordered([ (i.free_symbols, i) for i in eqs]), lambda x: len(x[0])) eqs = [] nonlineqs = [] while 1 in sifted: for free, e in sifted.pop(1): x = free.pop() if (e.lhs != x or x in e.rhs.free_symbols) and x not in reps: try: m, b = linear_coeffs( e.rewrite(Add, evaluate=False), x) enew = e.func(x, -b/m) if measure(enew) <= ratio*measure(e): e = enew else: eqs.append(e) continue except ValueError: pass if x in reps: eqs.append(e.subs(x, reps[x])) elif e.lhs == x and x not in e.rhs.free_symbols: reps[x] = e.rhs eqs.append(e) else: # x is not yet identified, but may be later nonlineqs.append(e) resifted = defaultdict(list) for k in sifted: for f, e in sifted[k]: e = e.xreplace(reps) f = e.free_symbols resifted[len(f)].append((f, e)) sifted = resifted for k in sifted: eqs.extend([e for f, e in sifted[k]]) nonlineqs = [ei.subs(reps) for ei in nonlineqs] other = [ei.subs(reps) for ei in other] rv = rv.func(*([i.canonical for i in (eqs + nonlineqs + other)] + nonRel)) patterns = simplify_patterns_and() return self._apply_patternbased_simplification(rv, patterns, measure, False) def _eval_as_set(self): from sympy.sets.sets import Intersection return Intersection(*[arg.as_set() for arg in self.args]) def _eval_rewrite_as_Nor(self, *args, **kwargs): return Nor(*[Not(arg) for arg in self.args]) def to_anf(self, deep=True): if deep: result = And._to_anf(*self.args, deep=deep) return distribute_xor_over_and(result) return self class Or(LatticeOp, 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. Examples ======== >>> from sympy.abc import x, y >>> from sympy.logic.boolalg import Or >>> x | y x | y Notes ===== The ``|`` operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise or. Hence, ``Or(a, b)`` and ``a | b`` will return different things if ``a`` and ``b`` are integers. >>> Or(x, y).subs(x, 0) y """ zero = true identity = false @classmethod def _new_args_filter(cls, args): newargs = [] rel = [] args = BooleanFunction.binary_check_and_simplify(*args) for x in args: if x.is_Relational: c = x.canonical if c in rel: continue nc = c.negated.canonical if any(r == nc for r in rel): return [S.true] rel.append(c) newargs.append(x) return LatticeOp._new_args_filter(newargs, Or) def _eval_subs(self, old, new): args = [] bad = None for i in self.args: try: i = i.subs(old, new) except TypeError: # store TypeError if bad is None: bad = i continue if i == True: return S.true elif i != False: args.append(i) if bad is not None: # let it raise bad.subs(old, new) # If old is Or, replace the parts of the arguments with new if all # are there if isinstance(old, Or): old_set = set(old.args) if old_set.issubset(args): args = set(args) - old_set args.add(new) return self.func(*args) def _eval_as_set(self): from sympy.sets.sets import Union return Union(*[arg.as_set() for arg in self.args]) def _eval_rewrite_as_Nand(self, *args, **kwargs): return Nand(*[Not(arg) for arg in self.args]) def _eval_simplify(self, **kwargs): # standard simplify rv = super()._eval_simplify(**kwargs) if not isinstance(rv, Or): return rv patterns = simplify_patterns_or() return self._apply_patternbased_simplification(rv, patterns, kwargs['measure'], S.true) def to_anf(self, deep=True): args = range(1, len(self.args) + 1) args = (combinations(self.args, j) for j in args) args = chain.from_iterable(args) # powerset args = (And(*arg) for arg in args) args = map(lambda x: to_anf(x, deep=deep) if deep else x, args) return Xor(*list(args), remove_true=False) class Not(BooleanFunction): """ Logical Not function (negation) Returns True if the statement is False Returns False if the statement is True Examples ======== >>> from sympy.logic.boolalg import Not, And, Or >>> from sympy.abc import x, A, B >>> Not(True) False >>> Not(False) True >>> Not(And(True, False)) True >>> Not(Or(True, False)) False >>> Not(And(And(True, x), Or(x, False))) ~x >>> ~x ~x >>> Not(And(Or(A, B), Or(~A, ~B))) ~((A | B) & (~A | ~B)) Notes ===== - The ``~`` operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise not. In particular, ``~a`` and ``Not(a)`` will be different if ``a`` is an integer. Furthermore, since bools in Python subclass from ``int``, ``~True`` is the same as ``~1`` which is ``-2``, which has a boolean value of True. To avoid this issue, use the SymPy boolean types ``true`` and ``false``. >>> from sympy import true >>> ~True -2 >>> ~true False """ is_Not = True @classmethod def eval(cls, arg): if isinstance(arg, Number) or arg in (True, False): return false if arg else true if arg.is_Not: return arg.args[0] # Simplify Relational objects. if arg.is_Relational: return arg.negated def _eval_as_set(self): """ Rewrite logic operators and relationals in terms of real sets. Examples ======== >>> from sympy import Not, Symbol >>> x = Symbol('x') >>> Not(x > 0).as_set() Interval(-oo, 0) """ return self.args[0].as_set().complement(S.Reals) def to_nnf(self, simplify=True): if is_literal(self): return self expr = self.args[0] func, args = expr.func, expr.args if func == And: return Or._to_nnf(*[~arg for arg in args], simplify=simplify) if func == Or: return And._to_nnf(*[~arg for arg in args], simplify=simplify) if func == Implies: a, b = args return And._to_nnf(a, ~b, simplify=simplify) if func == Equivalent: return And._to_nnf(Or(*args), Or(*[~arg for arg in args]), simplify=simplify) if func == Xor: result = [] for i in range(1, len(args)+1, 2): for neg in combinations(args, i): clause = [~s if s in neg else s for s in args] result.append(Or(*clause)) return And._to_nnf(*result, simplify=simplify) if func == ITE: a, b, c = args return And._to_nnf(Or(a, ~c), Or(~a, ~b), simplify=simplify) raise ValueError("Illegal operator %s in expression" % func) def to_anf(self, deep=True): return Xor._to_anf(true, self.args[0], deep=deep) 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. Examples ======== >>> from sympy.logic.boolalg import Xor >>> from sympy import symbols >>> x, y = symbols('x y') >>> Xor(True, False) True >>> Xor(True, True) False >>> Xor(True, False, True, True, False) True >>> Xor(True, False, True, False) False >>> x ^ y x ^ y Notes ===== The ``^`` operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise xor. In particular, ``a ^ b`` and ``Xor(a, b)`` will be different if ``a`` and ``b`` are integers. >>> Xor(x, y).subs(y, 0) x """ def __new__(cls, *args, remove_true=True, **kwargs): argset = set() obj = super().__new__(cls, *args, **kwargs) for arg in obj._args: if isinstance(arg, Number) or arg in (True, False): if arg: arg = true else: continue if isinstance(arg, Xor): for a in arg.args: argset.remove(a) if a in argset else argset.add(a) elif arg in argset: argset.remove(arg) else: argset.add(arg) rel = [(r, r.canonical, r.negated.canonical) for r in argset if r.is_Relational] odd = False # is number of complimentary pairs odd? start 0 -> False remove = [] for i, (r, c, nc) in enumerate(rel): for j in range(i + 1, len(rel)): rj, cj = rel[j][:2] if cj == nc: odd = ~odd break elif cj == c: break else: continue remove.append((r, rj)) if odd: argset.remove(true) if true in argset else argset.add(true) for a, b in remove: argset.remove(a) argset.remove(b) if len(argset) == 0: return false elif len(argset) == 1: return argset.pop() elif True in argset and remove_true: argset.remove(True) return Not(Xor(*argset)) else: obj._args = tuple(ordered(argset)) obj._argset = frozenset(argset) return obj # XXX: This should be cached on the object rather than using cacheit # Maybe it can be computed in __new__? @property # type: ignore @cacheit def args(self): return tuple(ordered(self._argset)) def to_nnf(self, simplify=True): args = [] for i in range(0, len(self.args)+1, 2): for neg in combinations(self.args, i): clause = [~s if s in neg else s for s in self.args] args.append(Or(*clause)) return And._to_nnf(*args, simplify=simplify) def _eval_rewrite_as_Or(self, *args, **kwargs): a = self.args return Or(*[_convert_to_varsSOP(x, self.args) for x in _get_odd_parity_terms(len(a))]) def _eval_rewrite_as_And(self, *args, **kwargs): a = self.args return And(*[_convert_to_varsPOS(x, self.args) for x in _get_even_parity_terms(len(a))]) def _eval_simplify(self, **kwargs): # as standard simplify uses simplify_logic which writes things as # And and Or, we only simplify the partial expressions before using # patterns rv = self.func(*[a.simplify(**kwargs) for a in self.args]) if not isinstance(rv, Xor): # This shouldn't really happen here return rv patterns = simplify_patterns_xor() return self._apply_patternbased_simplification(rv, patterns, kwargs['measure'], None) def _eval_subs(self, old, new): # If old is Xor, replace the parts of the arguments with new if all # are there if isinstance(old, Xor): old_set = set(old.args) if old_set.issubset(self.args): args = set(self.args) - old_set args.add(new) return self.func(*args) 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. Returns True if any of the arguments are False Returns False if all arguments are True Examples ======== >>> from sympy.logic.boolalg import Nand >>> from sympy import symbols >>> x, y = symbols('x y') >>> Nand(False, True) True >>> Nand(True, True) False >>> Nand(x, y) ~(x & y) """ @classmethod def eval(cls, *args): return Not(And(*args)) 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. Returns False if any argument is True Returns True if all arguments are False Examples ======== >>> from sympy.logic.boolalg import Nor >>> from sympy import symbols >>> x, y = symbols('x y') >>> Nor(True, False) False >>> Nor(True, True) False >>> Nor(False, True) False >>> Nor(False, False) True >>> Nor(x, y) ~(x | y) """ @classmethod def eval(cls, *args): return Not(Or(*args)) class Xnor(BooleanFunction): """ Logical XNOR function. Returns False if an odd number of the arguments are True and the rest are False. Returns True if an even number of the arguments are True and the rest are False. Examples ======== >>> from sympy.logic.boolalg import Xnor >>> from sympy import symbols >>> x, y = symbols('x y') >>> Xnor(True, False) False >>> Xnor(True, True) True >>> Xnor(True, False, True, True, False) False >>> Xnor(True, False, True, False) True """ @classmethod def eval(cls, *args): return Not(Xor(*args)) class Implies(BooleanFunction): """ Logical implication. A implies B is equivalent to !A v B Accepts two Boolean arguments; A and B. Returns False if A is True and B is False Returns True otherwise. Examples ======== >>> from sympy.logic.boolalg import Implies >>> from sympy import symbols >>> x, y = symbols('x y') >>> Implies(True, False) False >>> Implies(False, False) True >>> Implies(True, True) True >>> Implies(False, True) True >>> x >> y Implies(x, y) >>> y << x Implies(x, y) Notes ===== The ``>>`` and ``<<`` operators are provided as a convenience, but note that their use here is different from their normal use in Python, which is bit shifts. Hence, ``Implies(a, b)`` and ``a >> b`` will return different things if ``a`` and ``b`` are integers. In particular, since Python considers ``True`` and ``False`` to be integers, ``True >> True`` will be the same as ``1 >> 1``, i.e., 0, which has a truth value of False. To avoid this issue, use the SymPy objects ``true`` and ``false``. >>> from sympy import true, false >>> True >> False 1 >>> true >> false False """ @classmethod def eval(cls, *args): try: newargs = [] for x in args: if isinstance(x, Number) or x in (0, 1): newargs.append(bool(x)) else: newargs.append(x) A, B = newargs except ValueError: raise ValueError( "%d operand(s) used for an Implies " "(pairs are required): %s" % (len(args), str(args))) if A == True or A == False or B == True or B == False: return Or(Not(A), B) elif A == B: return S.true elif A.is_Relational and B.is_Relational: if A.canonical == B.canonical: return S.true if A.negated.canonical == B.canonical: return B else: return Basic.__new__(cls, *args) def to_nnf(self, simplify=True): a, b = self.args return Or._to_nnf(~a, b, simplify=simplify) def to_anf(self, deep=True): a, b = self.args return Xor._to_anf(true, a, And(a, b), deep=deep) class Equivalent(BooleanFunction): """ Equivalence relation. Equivalent(A, B) is True iff A and B are both True or both False Returns True if all of the arguments are logically equivalent. Returns False otherwise. Examples ======== >>> from sympy.logic.boolalg import Equivalent, And >>> from sympy.abc import x >>> Equivalent(False, False, False) True >>> Equivalent(True, False, False) False >>> Equivalent(x, And(x, True)) True """ def __new__(cls, *args, **options): from sympy.core.relational import Relational args = [_sympify(arg) for arg in args] argset = set(args) for x in args: if isinstance(x, Number) or x in [True, False]: # Includes 0, 1 argset.discard(x) argset.add(bool(x)) rel = [] for r in argset: if isinstance(r, Relational): rel.append((r, r.canonical, r.negated.canonical)) remove = [] for i, (r, c, nc) in enumerate(rel): for j in range(i + 1, len(rel)): rj, cj = rel[j][:2] if cj == nc: return false elif cj == c: remove.append((r, rj)) break for a, b in remove: argset.remove(a) argset.remove(b) argset.add(True) if len(argset) <= 1: return true if True in argset: argset.discard(True) return And(*argset) if False in argset: argset.discard(False) return And(*[~arg for arg in argset]) _args = frozenset(argset) obj = super().__new__(cls, _args) obj._argset = _args return obj # XXX: This should be cached on the object rather than using cacheit # Maybe it can be computed in __new__? @property # type: ignore @cacheit def args(self): return tuple(ordered(self._argset)) def to_nnf(self, simplify=True): args = [] for a, b in zip(self.args, self.args[1:]): args.append(Or(~a, b)) args.append(Or(~self.args[-1], self.args[0])) return And._to_nnf(*args, simplify=simplify) def to_anf(self, deep=True): a = And(*self.args) b = And(*[to_anf(Not(arg), deep=False) for arg in self.args]) b = distribute_xor_over_and(b) return Xor._to_anf(a, b, deep=deep) class ITE(BooleanFunction): """ If then else clause. ITE(A, B, C) evaluates and returns the result of B if A is true else it returns the result of C. All args must be Booleans. Examples ======== >>> from sympy.logic.boolalg import ITE, And, Xor, Or >>> from sympy.abc import x, y, z >>> ITE(True, False, True) False >>> ITE(Or(True, False), And(True, True), Xor(True, True)) True >>> ITE(x, y, z) ITE(x, y, z) >>> ITE(True, x, y) x >>> ITE(False, x, y) y >>> ITE(x, y, y) y Trying to use non-Boolean args will generate a TypeError: >>> ITE(True, [], ()) Traceback (most recent call last): ... TypeError: expecting bool, Boolean or ITE, not `[]` """ def __new__(cls, *args, **kwargs): from sympy.core.relational import Eq, Ne if len(args) != 3: raise ValueError('expecting exactly 3 args') a, b, c = args # check use of binary symbols if isinstance(a, (Eq, Ne)): # in this context, we can evaluate the Eq/Ne # if one arg is a binary symbol and the other # is true/false b, c = map(as_Boolean, (b, c)) bin_syms = set().union(*[i.binary_symbols for i in (b, c)]) if len(set(a.args) - bin_syms) == 1: # one arg is a binary_symbols _a = a if a.lhs is S.true: a = a.rhs elif a.rhs is S.true: a = a.lhs elif a.lhs is S.false: a = ~a.rhs elif a.rhs is S.false: a = ~a.lhs else: # binary can only equal True or False a = S.false if isinstance(_a, Ne): a = ~a else: a, b, c = BooleanFunction.binary_check_and_simplify( a, b, c) rv = None if kwargs.get('evaluate', True): rv = cls.eval(a, b, c) if rv is None: rv = BooleanFunction.__new__(cls, a, b, c, evaluate=False) return rv @classmethod def eval(cls, *args): from sympy.core.relational import Eq, Ne # do the args give a singular result? a, b, c = args if isinstance(a, (Ne, Eq)): _a = a if S.true in a.args: a = a.lhs if a.rhs is S.true else a.rhs elif S.false in a.args: a = ~a.lhs if a.rhs is S.false else ~a.rhs else: _a = None if _a is not None and isinstance(_a, Ne): a = ~a if a is S.true: return b if a is S.false: return c if b == c: return b else: # or maybe the results allow the answer to be expressed # in terms of the condition if b is S.true and c is S.false: return a if b is S.false and c is S.true: return Not(a) if [a, b, c] != args: return cls(a, b, c, evaluate=False) def to_nnf(self, simplify=True): a, b, c = self.args return And._to_nnf(Or(~a, b), Or(a, c), simplify=simplify) def _eval_as_set(self): return self.to_nnf().as_set() def _eval_rewrite_as_Piecewise(self, *args, **kwargs): from sympy.functions import Piecewise return Piecewise((args[1], args[0]), (args[2], True)) class Exclusive(BooleanFunction): """ True if only one or no argument is true. ``Exclusive(A, B, C)`` is equivalent to ``~(A & B) & ~(A & C) & ~(B & C)``. Examples ======== >>> from sympy.logic.boolalg import Exclusive >>> Exclusive(False, False, False) True >>> Exclusive(False, True, False) True >>> Exclusive(False, True, True) False """ @classmethod def eval(cls, *args): and_args = [] for a, b in combinations(args, 2): and_args.append(Not(And(a, b))) return And(*and_args) # end class definitions. Some useful methods def conjuncts(expr): """Return a list of the conjuncts in the expr s. Examples ======== >>> from sympy.logic.boolalg import conjuncts >>> from sympy.abc import A, B >>> conjuncts(A & B) frozenset({A, B}) >>> conjuncts(A | B) frozenset({A | B}) """ return And.make_args(expr) def disjuncts(expr): """Return a list of the disjuncts in the sentence s. Examples ======== >>> from sympy.logic.boolalg import disjuncts >>> from sympy.abc import A, B >>> disjuncts(A | B) frozenset({A, B}) >>> disjuncts(A & B) frozenset({A & B}) """ return Or.make_args(expr) def distribute_and_over_or(expr): """ Given a sentence s consisting of conjunctions and disjunctions of literals, return an equivalent sentence in CNF. Examples ======== >>> from sympy.logic.boolalg import distribute_and_over_or, And, Or, Not >>> from sympy.abc import A, B, C >>> distribute_and_over_or(Or(A, And(Not(B), Not(C)))) (A | ~B) & (A | ~C) """ return _distribute((expr, And, Or)) def distribute_or_over_and(expr): """ Given a sentence s consisting of conjunctions and disjunctions of literals, return an equivalent sentence in DNF. Note that the output is NOT simplified. Examples ======== >>> from sympy.logic.boolalg import distribute_or_over_and, And, Or, Not >>> from sympy.abc import A, B, C >>> distribute_or_over_and(And(Or(Not(A), B), C)) (B & C) | (C & ~A) """ return _distribute((expr, Or, And)) def distribute_xor_over_and(expr): """ Given a sentence s consisting of conjunction and exclusive disjunctions of literals, return an equivalent exclusive disjunction. Note that the output is NOT simplified. Examples ======== >>> from sympy.logic.boolalg import distribute_xor_over_and, And, Xor, Not >>> from sympy.abc import A, B, C >>> distribute_xor_over_and(And(Xor(Not(A), B), C)) (B & C) ^ (C & ~A) """ return _distribute((expr, Xor, And)) def _distribute(info): """ Distributes info[1] over info[2] with respect to info[0]. """ if isinstance(info[0], info[2]): for arg in info[0].args: if isinstance(arg, info[1]): conj = arg break else: return info[0] rest = info[2](*[a for a in info[0].args if a is not conj]) return info[1](*list(map(_distribute, [(info[2](c, rest), info[1], info[2]) for c in conj.args])), remove_true=False) elif isinstance(info[0], info[1]): return info[1](*list(map(_distribute, [(x, info[1], info[2]) for x in info[0].args])), remove_true=False) else: return info[0] def to_anf(expr, deep=True): r""" Converts expr to Algebraic Normal Form (ANF). ANF is a canonical normal form, which means that two equivalent formulas will convert to the same ANF. A logical expression is in ANF if it has the form .. math:: 1 \oplus a \oplus b \oplus ab \oplus abc i.e. it can be: - purely true, - purely false, - conjunction of variables, - exclusive disjunction. The exclusive disjunction can only contain true, variables or conjunction of variables. No negations are permitted. If ``deep`` is ``False``, arguments of the boolean expression are considered variables, i.e. only the top-level expression is converted to ANF. Examples ======== >>> from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent >>> from sympy.logic.boolalg import to_anf >>> from sympy.abc import A, B, C >>> to_anf(Not(A)) A ^ True >>> to_anf(And(Or(A, B), Not(C))) A ^ B ^ (A & B) ^ (A & C) ^ (B & C) ^ (A & B & C) >>> to_anf(Implies(Not(A), Equivalent(B, C)), deep=False) True ^ ~A ^ (~A & (Equivalent(B, C))) """ expr = sympify(expr) if is_anf(expr): return expr return expr.to_anf(deep=deep) def to_nnf(expr, simplify=True): """ Converts expr to Negation Normal Form. A logical expression is in Negation Normal Form (NNF) if it contains only And, Or and Not, and Not is applied only to literals. If simplify is True, the result contains no redundant clauses. Examples ======== >>> from sympy.abc import A, B, C, D >>> from sympy.logic.boolalg import Not, Equivalent, to_nnf >>> to_nnf(Not((~A & ~B) | (C & D))) (A | B) & (~C | ~D) >>> to_nnf(Equivalent(A >> B, B >> A)) (A | ~B | (A & ~B)) & (B | ~A | (B & ~A)) """ if is_nnf(expr, simplify): return expr return expr.to_nnf(simplify) def to_cnf(expr, simplify=False, force=False): """ Convert a propositional logical sentence s to conjunctive normal form: ((A | ~B | ...) & (B | C | ...) & ...). If simplify is True, the expr is evaluated to its simplest CNF form using the Quine-McCluskey algorithm; this may take a long time if there are more than 8 variables and requires that the ``force`` flag be set to True (default is False). Examples ======== >>> from sympy.logic.boolalg import to_cnf >>> from sympy.abc import A, B, D >>> to_cnf(~(A | B) | D) (D | ~A) & (D | ~B) >>> to_cnf((A | B) & (A | ~A), True) A | B """ expr = sympify(expr) if not isinstance(expr, BooleanFunction): return expr if simplify: if not force and len(_find_predicates(expr)) > 8: raise ValueError(filldedent(''' To simplify a logical expression with more than 8 variables may take a long time and requires the use of `force=True`.''')) return simplify_logic(expr, 'cnf', True, force=force) # Don't convert unless we have to if is_cnf(expr): return expr expr = eliminate_implications(expr) res = distribute_and_over_or(expr) return res def to_dnf(expr, simplify=False, force=False): """ Convert a propositional logical sentence s to disjunctive normal form: ((A & ~B & ...) | (B & C & ...) | ...). If simplify is True, the expr is evaluated to its simplest DNF form using the Quine-McCluskey algorithm; this may take a long time if there are more than 8 variables and requires that the ``force`` flag be set to True (default is False). Examples ======== >>> from sympy.logic.boolalg import to_dnf >>> from sympy.abc import A, B, C >>> to_dnf(B & (A | C)) (A & B) | (B & C) >>> to_dnf((A & B) | (A & ~B) | (B & C) | (~B & C), True) A | C """ expr = sympify(expr) if not isinstance(expr, BooleanFunction): return expr if simplify: if not force and len(_find_predicates(expr)) > 8: raise ValueError(filldedent(''' To simplify a logical expression with more than 8 variables may take a long time and requires the use of `force=True`.''')) return simplify_logic(expr, 'dnf', True, force=force) # Don't convert unless we have to if is_dnf(expr): return expr expr = eliminate_implications(expr) return distribute_or_over_and(expr) def is_anf(expr): r""" Checks if expr is in Algebraic Normal Form (ANF). A logical expression is in ANF if it has the form .. math:: 1 \oplus a \oplus b \oplus ab \oplus abc i.e. it is purely true, purely false, conjunction of variables or exclusive disjunction. The exclusive disjunction can only contain true, variables or conjunction of variables. No negations are permitted. Examples ======== >>> from sympy.logic.boolalg import And, Not, Xor, true, is_anf >>> from sympy.abc import A, B, C >>> is_anf(true) True >>> is_anf(A) True >>> is_anf(And(A, B, C)) True >>> is_anf(Xor(A, Not(B))) False """ expr = sympify(expr) if is_literal(expr) and not isinstance(expr, Not): return True if isinstance(expr, And): for arg in expr.args: if not arg.is_Symbol: return False return True elif isinstance(expr, Xor): for arg in expr.args: if isinstance(arg, And): for a in arg.args: if not a.is_Symbol: return False elif is_literal(arg): if isinstance(arg, Not): return False else: return False return True else: return False def is_nnf(expr, simplified=True): """ Checks if expr is in Negation Normal Form. A logical expression is in Negation Normal Form (NNF) if it contains only And, Or and Not, and Not is applied only to literals. If simplified is True, checks if result contains no redundant clauses. Examples ======== >>> from sympy.abc import A, B, C >>> from sympy.logic.boolalg import Not, is_nnf >>> is_nnf(A & B | ~C) True >>> is_nnf((A | ~A) & (B | C)) False >>> is_nnf((A | ~A) & (B | C), False) True >>> is_nnf(Not(A & B) | C) False >>> is_nnf((A >> B) & (B >> A)) False """ expr = sympify(expr) if is_literal(expr): return True stack = [expr] while stack: expr = stack.pop() if expr.func in (And, Or): if simplified: args = expr.args for arg in args: if Not(arg) in args: return False stack.extend(expr.args) elif not is_literal(expr): return False return True def is_cnf(expr): """ Test whether or not an expression is in conjunctive normal form. Examples ======== >>> from sympy.logic.boolalg import is_cnf >>> from sympy.abc import A, B, C >>> is_cnf(A | B | C) True >>> is_cnf(A & B & C) True >>> is_cnf((A & B) | C) False """ return _is_form(expr, And, Or) def is_dnf(expr): """ Test whether or not an expression is in disjunctive normal form. Examples ======== >>> from sympy.logic.boolalg import is_dnf >>> from sympy.abc import A, B, C >>> is_dnf(A | B | C) True >>> is_dnf(A & B & C) True >>> is_dnf((A & B) | C) True >>> is_dnf(A & (B | C)) False """ return _is_form(expr, Or, And) def _is_form(expr, function1, function2): """ Test whether or not an expression is of the required form. """ expr = sympify(expr) vals = function1.make_args(expr) if isinstance(expr, function1) else [expr] for lit in vals: if isinstance(lit, function2): vals2 = function2.make_args(lit) if isinstance(lit, function2) else [lit] for l in vals2: if is_literal(l) is False: return False elif is_literal(lit) is False: return False return True 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. Examples ======== >>> from sympy.logic.boolalg import Implies, Equivalent, \ eliminate_implications >>> from sympy.abc import A, B, C >>> eliminate_implications(Implies(A, B)) B | ~A >>> eliminate_implications(Equivalent(A, B)) (A | ~B) & (B | ~A) >>> eliminate_implications(Equivalent(A, B, C)) (A | ~C) & (B | ~A) & (C | ~B) """ return to_nnf(expr, simplify=False) def is_literal(expr): """ Returns True if expr is a literal, else False. Examples ======== >>> from sympy import Or, Q >>> from sympy.abc import A, B >>> from sympy.logic.boolalg import is_literal >>> is_literal(A) True >>> is_literal(~A) True >>> is_literal(Q.zero(A)) True >>> is_literal(A + B) True >>> is_literal(Or(A, B)) False """ from sympy.assumptions import AppliedPredicate if isinstance(expr, Not): return is_literal(expr.args[0]) elif expr in (True, False) or isinstance(expr, AppliedPredicate) or expr.is_Atom: return True elif not isinstance(expr, BooleanFunction) and all( (isinstance(expr, AppliedPredicate) or a.is_Atom) for a in expr.args): return True return False def to_int_repr(clauses, symbols): """ Takes clauses in CNF format and puts them into an integer representation. Examples ======== >>> from sympy.logic.boolalg import to_int_repr >>> from sympy.abc import x, y >>> to_int_repr([x | y, y], [x, y]) == [{1, 2}, {2}] True """ # Convert the symbol list into a dict symbols = dict(list(zip(symbols, list(range(1, len(symbols) + 1))))) def append_symbol(arg, symbols): if isinstance(arg, Not): return -symbols[arg.args[0]] else: return symbols[arg] return [{append_symbol(arg, symbols) for arg in Or.make_args(c)} for c in clauses] def term_to_integer(term): """ Return an integer corresponding to the base-2 digits given by ``term``. Parameters ========== term : a string or list of ones and zeros Examples ======== >>> from sympy.logic.boolalg import term_to_integer >>> term_to_integer([1, 0, 0]) 4 >>> term_to_integer('100') 4 """ return int(''.join(list(map(str, list(term)))), 2) def integer_to_term(k, n_bits=None): """ Return a list of the base-2 digits in the integer, ``k``. Parameters ========== k : int n_bits : int If ``n_bits`` is given and the number of digits in the binary representation of ``k`` is smaller than ``n_bits`` then left-pad the list with 0s. Examples ======== >>> from sympy.logic.boolalg import integer_to_term >>> integer_to_term(4) [1, 0, 0] >>> integer_to_term(4, 6) [0, 0, 0, 1, 0, 0] """ s = '{0:0{1}b}'.format(abs(as_int(k)), as_int(abs(n_bits or 0))) return list(map(int, s)) def truth_table(expr, variables, input=True): """ Return a generator of all possible configurations of the input variables, and the result of the boolean expression for those values. Parameters ========== expr : string or boolean expression variables : list of variables input : boolean (default True) indicates whether to return the input combinations. Examples ======== >>> from sympy.logic.boolalg import truth_table >>> from sympy.abc import x,y >>> table = truth_table(x >> y, [x, y]) >>> for t in table: ... print('{0} -> {1}'.format(*t)) [0, 0] -> True [0, 1] -> True [1, 0] -> False [1, 1] -> True >>> table = truth_table(x | y, [x, y]) >>> list(table) [([0, 0], False), ([0, 1], True), ([1, 0], True), ([1, 1], True)] If input is false, truth_table returns only a list of truth values. In this case, the corresponding input values of variables can be deduced from the index of a given output. >>> from sympy.logic.boolalg import integer_to_term >>> vars = [y, x] >>> values = truth_table(x >> y, vars, input=False) >>> values = list(values) >>> values [True, False, True, True] >>> for i, value in enumerate(values): ... print('{0} -> {1}'.format(list(zip( ... vars, integer_to_term(i, len(vars)))), value)) [(y, 0), (x, 0)] -> True [(y, 0), (x, 1)] -> False [(y, 1), (x, 0)] -> True [(y, 1), (x, 1)] -> True """ variables = [sympify(v) for v in variables] expr = sympify(expr) if not isinstance(expr, BooleanFunction) and not is_literal(expr): return table = product((0, 1), repeat=len(variables)) for term in table: term = list(term) value = expr.xreplace(dict(zip(variables, term))) if input: yield term, value else: yield value def _check_pair(minterm1, minterm2): """ Checks if a pair of minterms differs by only one bit. If yes, returns index, else returns -1. """ # Early termination seems to be faster than list comprehension, # at least for large examples. index = -1 for x, i in enumerate(minterm1): # zip(minterm1, minterm2) is slower if i != minterm2[x]: if index == -1: index = x else: return -1 return index def _convert_to_varsSOP(minterm, variables): """ Converts a term in the expansion of a function from binary to its variable form (for SOP). """ temp = [variables[n] if val == 1 else Not(variables[n]) for n, val in enumerate(minterm) if val != 3] return And(*temp) def _convert_to_varsPOS(maxterm, variables): """ Converts a term in the expansion of a function from binary to its variable form (for POS). """ temp = [variables[n] if val == 0 else Not(variables[n]) for n, val in enumerate(maxterm) if val != 3] return Or(*temp) def _convert_to_varsANF(term, variables): """ Converts a term in the expansion of a function from binary to it's variable form (for ANF). Parameters ========== term : list of 1's and 0's (complementation patter) variables : list of variables """ temp = [variables[n] for n, t in enumerate(term) if t == 1] if not temp: return true return And(*temp) def _get_odd_parity_terms(n): """ Returns a list of lists, with all possible combinations of n zeros and ones with an odd number of ones. """ return [e for e in [ibin(i, n) for i in range(2**n)] if sum(e) % 2 == 1] def _get_even_parity_terms(n): """ Returns a list of lists, with all possible combinations of n zeros and ones with an even number of ones. """ return [e for e in [ibin(i, n) for i in range(2**n)] if sum(e) % 2 == 0] def _simplified_pairs(terms): """ Reduces a set of minterms, if possible, to a simplified set of minterms with one less variable in the terms using QM method. """ if not terms: return [] simplified_terms = [] todo = list(range(len(terms))) # Count number of ones as _check_pair can only potentially match if there # is at most a difference of a single one termdict = defaultdict(list) for n, term in enumerate(terms): ones = sum([1 for t in term if t == 1]) termdict[ones].append(n) variables = len(terms[0]) for k in range(variables): for i in termdict[k]: for j in termdict[k+1]: index = _check_pair(terms[i], terms[j]) if index != -1: # Mark terms handled todo[i] = todo[j] = None # Copy old term newterm = terms[i][:] # Set differing position to don't care newterm[index] = 3 # Add if not already there if newterm not in simplified_terms: simplified_terms.append(newterm) if simplified_terms: # Further simplifications only among the new terms simplified_terms = _simplified_pairs(simplified_terms) # Add remaining, non-simplified, terms simplified_terms.extend([terms[i] for i in todo if i is not None]) return simplified_terms def _rem_redundancy(l1, terms): """ After the truth table has been sufficiently simplified, use the prime implicant table method to recognize and eliminate redundant pairs, and return the essential arguments. """ if not terms: return [] nterms = len(terms) nl1 = len(l1) # Create dominating matrix dommatrix = [[0]*nl1 for n in range(nterms)] colcount = [0]*nl1 rowcount = [0]*nterms for primei, prime in enumerate(l1): for termi, term in enumerate(terms): # Check prime implicant covering term if all(t == 3 or t == mt for t, mt in zip(prime, term)): dommatrix[termi][primei] = 1 colcount[primei] += 1 rowcount[termi] += 1 # Keep track if anything changed anythingchanged = True # Then, go again while anythingchanged: anythingchanged = False for rowi in range(nterms): # Still non-dominated? if rowcount[rowi]: row = dommatrix[rowi] for row2i in range(nterms): # Still non-dominated? if rowi != row2i and rowcount[rowi] and (rowcount[rowi] <= rowcount[row2i]): row2 = dommatrix[row2i] if all(row2[n] >= row[n] for n in range(nl1)): # row2 dominating row, remove row2 rowcount[row2i] = 0 anythingchanged = True for primei, prime in enumerate(row2): if prime: # Make corresponding entry 0 dommatrix[row2i][primei] = 0 colcount[primei] -= 1 colcache = dict() for coli in range(nl1): # Still non-dominated? if colcount[coli]: if coli in colcache: col = colcache[coli] else: col = [dommatrix[i][coli] for i in range(nterms)] colcache[coli] = col for col2i in range(nl1): # Still non-dominated? if coli != col2i and colcount[col2i] and (colcount[coli] >= colcount[col2i]): if col2i in colcache: col2 = colcache[col2i] else: col2 = [dommatrix[i][col2i] for i in range(nterms)] colcache[col2i] = col2 if all(col[n] >= col2[n] for n in range(nterms)): # col dominating col2, remove col2 colcount[col2i] = 0 anythingchanged = True for termi, term in enumerate(col2): if term and dommatrix[termi][col2i]: # Make corresponding entry 0 dommatrix[termi][col2i] = 0 rowcount[termi] -= 1 if not anythingchanged: # Heuristically select the prime implicant covering most terms maxterms = 0 bestcolidx = -1 for coli in range(nl1): s = colcount[coli] if s > maxterms: bestcolidx = coli maxterms = s # In case we found a prime implicant covering at least two terms if bestcolidx != -1 and maxterms > 1: for primei, prime in enumerate(l1): if primei != bestcolidx: for termi, term in enumerate(colcache[bestcolidx]): if term and dommatrix[termi][primei]: # Make corresponding entry 0 dommatrix[termi][primei] = 0 anythingchanged = True rowcount[termi] -= 1 colcount[primei] -= 1 return [l1[i] for i in range(nl1) if colcount[i]] def _input_to_binlist(inputlist, variables): binlist = [] bits = len(variables) for val in inputlist: if isinstance(val, int): binlist.append(ibin(val, bits)) elif isinstance(val, dict): nonspecvars = list(variables) for key in val.keys(): nonspecvars.remove(key) for t in product((0, 1), repeat=len(nonspecvars)): d = dict(zip(nonspecvars, t)) d.update(val) binlist.append([d[v] for v in variables]) elif isinstance(val, (list, tuple)): if len(val) != bits: raise ValueError("Each term must contain {bits} bits as there are" "\n{bits} variables (or be an integer)." "".format(bits=bits)) binlist.append(list(val)) else: raise TypeError("A term list can only contain lists," " ints or dicts.") return binlist def SOPform(variables, minterms, dontcares=None): """ The SOPform function uses simplified_pairs and a redundant group- eliminating algorithm to convert the list of all input combos that generate '1' (the minterms) into the smallest Sum of Products form. The variables must be given as the first argument. Return a logical Or function (i.e., the "sum of products" or "SOP" form) that gives the desired outcome. If there are inputs that can be ignored, pass them as a list, too. The result will be one of the (perhaps many) functions that satisfy the conditions. Examples ======== >>> from sympy.logic import SOPform >>> from sympy import symbols >>> w, x, y, z = symbols('w x y z') >>> minterms = [[0, 0, 0, 1], [0, 0, 1, 1], ... [0, 1, 1, 1], [1, 0, 1, 1], [1, 1, 1, 1]] >>> dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]] >>> SOPform([w, x, y, z], minterms, dontcares) (y & z) | (~w & ~x) The terms can also be represented as integers: >>> minterms = [1, 3, 7, 11, 15] >>> dontcares = [0, 2, 5] >>> SOPform([w, x, y, z], minterms, dontcares) (y & z) | (~w & ~x) They can also be specified using dicts, which does not have to be fully specified: >>> minterms = [{w: 0, x: 1}, {y: 1, z: 1, x: 0}] >>> SOPform([w, x, y, z], minterms) (x & ~w) | (y & z & ~x) Or a combination: >>> minterms = [4, 7, 11, [1, 1, 1, 1]] >>> dontcares = [{w : 0, x : 0, y: 0}, 5] >>> SOPform([w, x, y, z], minterms, dontcares) (w & y & z) | (~w & ~y) | (x & z & ~w) References ========== .. [1] https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm """ if minterms == []: return false variables = tuple(map(sympify, variables)) minterms = _input_to_binlist(minterms, variables) dontcares = _input_to_binlist((dontcares or []), variables) for d in dontcares: if d in minterms: raise ValueError('%s in minterms is also in dontcares' % d) new = _simplified_pairs(minterms + dontcares) essential = _rem_redundancy(new, minterms) return Or(*[_convert_to_varsSOP(x, variables) for x in essential]) def POSform(variables, minterms, dontcares=None): """ The POSform function uses simplified_pairs and a redundant-group eliminating algorithm to convert the list of all input combinations that generate '1' (the minterms) into the smallest Product of Sums form. The variables must be given as the first argument. Return a logical And function (i.e., the "product of sums" or "POS" form) that gives the desired outcome. If there are inputs that can be ignored, pass them as a list, too. The result will be one of the (perhaps many) functions that satisfy the conditions. Examples ======== >>> from sympy.logic import POSform >>> from sympy import symbols >>> w, x, y, z = symbols('w x y z') >>> minterms = [[0, 0, 0, 1], [0, 0, 1, 1], [0, 1, 1, 1], ... [1, 0, 1, 1], [1, 1, 1, 1]] >>> dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]] >>> POSform([w, x, y, z], minterms, dontcares) z & (y | ~w) The terms can also be represented as integers: >>> minterms = [1, 3, 7, 11, 15] >>> dontcares = [0, 2, 5] >>> POSform([w, x, y, z], minterms, dontcares) z & (y | ~w) They can also be specified using dicts, which does not have to be fully specified: >>> minterms = [{w: 0, x: 1}, {y: 1, z: 1, x: 0}] >>> POSform([w, x, y, z], minterms) (x | y) & (x | z) & (~w | ~x) Or a combination: >>> minterms = [4, 7, 11, [1, 1, 1, 1]] >>> dontcares = [{w : 0, x : 0, y: 0}, 5] >>> POSform([w, x, y, z], minterms, dontcares) (w | x) & (y | ~w) & (z | ~y) References ========== .. [1] https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm """ if minterms == []: return false variables = tuple(map(sympify, variables)) minterms = _input_to_binlist(minterms, variables) dontcares = _input_to_binlist((dontcares or []), variables) for d in dontcares: if d in minterms: raise ValueError('%s in minterms is also in dontcares' % d) maxterms = [] for t in product((0, 1), repeat=len(variables)): t = list(t) if (t not in minterms) and (t not in dontcares): maxterms.append(t) new = _simplified_pairs(maxterms + dontcares) essential = _rem_redundancy(new, maxterms) return And(*[_convert_to_varsPOS(x, variables) for x in essential]) def ANFform(variables, truthvalues): """ The ANFform function converts the list of truth values to Algebraic Normal Form (ANF). The variables must be given as the first argument. Return True, False, logical And funciton (i.e., the "Zhegalkin monomial") or logical Xor function (i.e., the "Zhegalkin polynomial"). When True and False are represented by 1 and 0, respectively, then And is multiplication and Xor is addition. Formally a "Zhegalkin monomial" is the product (logical And) of a finite set of distinct variables, including the empty set whose product is denoted 1 (True). A "Zhegalkin polynomial" is the sum (logical Xor) of a set of Zhegalkin monomials, with the empty set denoted by 0 (False). Parameters ========== variables : list of variables truthvalues : list of 1's and 0's (result column of truth table) Examples ======== >>> from sympy.logic.boolalg import ANFform >>> from sympy.abc import x, y >>> ANFform([x], [1, 0]) x ^ True >>> ANFform([x, y], [0, 1, 1, 1]) x ^ y ^ (x & y) References ========== .. [2] https://en.wikipedia.org/wiki/Zhegalkin_polynomial """ n_vars = len(variables) n_values = len(truthvalues) if n_values != 2 ** n_vars: raise ValueError("The number of truth values must be equal to 2^%d, " "got %d" % (n_vars, n_values)) variables = tuple(map(sympify, variables)) coeffs = anf_coeffs(truthvalues) terms = [] for i, t in enumerate(product((0, 1), repeat=n_vars)): if coeffs[i] == 1: terms.append(t) return Xor(*[_convert_to_varsANF(x, variables) for x in terms], remove_true=False) def anf_coeffs(truthvalues): """ Convert a list of truth values of some boolean expression to the list of coefficients of the polynomial mod 2 (exclusive disjunction) representing the boolean expression in ANF (i.e., the "Zhegalkin polynomial"). There are 2^n possible Zhegalkin monomials in n variables, since each monomial is fully specified by the presence or absence of each variable. We can enumerate all the monomials. For example, boolean function with four variables (a, b, c, d) can contain up to 2^4 = 16 monomials. The 13-th monomial is the product a & b & d, because 13 in binary is 1, 1, 0, 1. A given monomial's presence or absence in a polynomial corresponds to that monomial's coefficient being 1 or 0 respectively. Examples ======== >>> from sympy.logic.boolalg import anf_coeffs, bool_monomial, Xor >>> from sympy.abc import a, b, c >>> truthvalues = [0, 1, 1, 0, 0, 1, 0, 1] >>> coeffs = anf_coeffs(truthvalues) >>> coeffs [0, 1, 1, 0, 0, 0, 1, 0] >>> polynomial = Xor(*[ ... bool_monomial(k, [a, b, c]) ... for k, coeff in enumerate(coeffs) if coeff == 1 ... ]) >>> polynomial b ^ c ^ (a & b) """ s = '{:b}'.format(len(truthvalues)) n = len(s) - 1 if len(truthvalues) != 2**n: raise ValueError("The number of truth values must be a power of two, " "got %d" % len(truthvalues)) coeffs = [[v] for v in truthvalues] for i in range(n): tmp = [] for j in range(2 ** (n-i-1)): tmp.append(coeffs[2*j] + list(map(lambda x, y: x^y, coeffs[2*j], coeffs[2*j+1]))) coeffs = tmp return coeffs[0] def bool_minterm(k, variables): """ Return the k-th minterm. Minterms are numbered by a binary encoding of the complementation pattern of the variables. This convention assigns the value 1 to the direct form and 0 to the complemented form. Parameters ========== k : int or list of 1's and 0's (complementation patter) variables : list of variables Examples ======== >>> from sympy.logic.boolalg import bool_minterm >>> from sympy.abc import x, y, z >>> bool_minterm([1, 0, 1], [x, y, z]) x & z & ~y >>> bool_minterm(6, [x, y, z]) x & y & ~z References ========== .. [3] https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_minterms """ if isinstance(k, int): k = integer_to_term(k, len(variables)) variables = tuple(map(sympify, variables)) return _convert_to_varsSOP(k, variables) def bool_maxterm(k, variables): """ Return the k-th maxterm. Each maxterm is assigned an index based on the opposite conventional binary encoding used for minterms. The maxterm convention assigns the value 0 to the direct form and 1 to the complemented form. Parameters ========== k : int or list of 1's and 0's (complementation pattern) variables : list of variables Examples ======== >>> from sympy.logic.boolalg import bool_maxterm >>> from sympy.abc import x, y, z >>> bool_maxterm([1, 0, 1], [x, y, z]) y | ~x | ~z >>> bool_maxterm(6, [x, y, z]) z | ~x | ~y References ========== .. [4] https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_maxterms """ if isinstance(k, int): k = integer_to_term(k, len(variables)) variables = tuple(map(sympify, variables)) return _convert_to_varsPOS(k, variables) def bool_monomial(k, variables): """ Return the k-th monomial. Monomials are numbered by a binary encoding of the presence and absences of the variables. This convention assigns the value 1 to the presence of variable and 0 to the absence of variable. Each boolean function can be uniquely represented by a Zhegalkin Polynomial (Algebraic Normal Form). The Zhegalkin Polynomial of the boolean function with n variables can contain up to 2^n monomials. We can enumarate all the monomials. Each monomial is fully specified by the presence or absence of each variable. For example, boolean function with four variables (a, b, c, d) can contain up to 2^4 = 16 monomials. The 13-th monomial is the product a & b & d, because 13 in binary is 1, 1, 0, 1. Parameters ========== k : int or list of 1's and 0's variables : list of variables Examples ======== >>> from sympy.logic.boolalg import bool_monomial >>> from sympy.abc import x, y, z >>> bool_monomial([1, 0, 1], [x, y, z]) x & z >>> bool_monomial(6, [x, y, z]) x & y """ if isinstance(k, int): k = integer_to_term(k, len(variables)) variables = tuple(map(sympify, variables)) return _convert_to_varsANF(k, variables) def _find_predicates(expr): """Helper to find logical predicates in BooleanFunctions. A logical predicate is defined here as anything within a BooleanFunction that is not a BooleanFunction itself. """ if not isinstance(expr, BooleanFunction): return {expr} return set().union(*(map(_find_predicates, expr.args))) def simplify_logic(expr, form=None, deep=True, force=False): """ This function simplifies a boolean function to its simplified version in SOP or POS form. The return type is an Or or And object in SymPy. Parameters ========== expr : string or boolean expression form : string ('cnf' or 'dnf') or None (default). If 'cnf' or 'dnf', the simplest expression in the corresponding normal form is returned; if None, the answer is returned according to the form with fewest args (in CNF by default). deep : boolean (default True) Indicates whether to recursively simplify any non-boolean functions contained within the input. force : boolean (default False) As the simplifications require exponential time in the number of variables, there is by default a limit on expressions with 8 variables. When the expression has more than 8 variables only symbolical simplification (controlled by ``deep``) is made. By setting force to ``True``, this limit is removed. Be aware that this can lead to very long simplification times. Examples ======== >>> from sympy.logic import simplify_logic >>> from sympy.abc import x, y, z >>> from sympy import S >>> b = (~x & ~y & ~z) | ( ~x & ~y & z) >>> simplify_logic(b) ~x & ~y >>> S(b) (z & ~x & ~y) | (~x & ~y & ~z) >>> simplify_logic(_) ~x & ~y """ if form not in (None, 'cnf', 'dnf'): raise ValueError("form can be cnf or dnf only") expr = sympify(expr) # check for quick exit if form is given: right form and all args are # literal and do not involve Not if form: form_ok = False if form == 'cnf': form_ok = is_cnf(expr) elif form == 'dnf': form_ok = is_dnf(expr) if form_ok and all(is_literal(a) for a in expr.args): return expr if deep: variables = _find_predicates(expr) from sympy.simplify.simplify import simplify s = tuple(map(simplify, variables)) expr = expr.xreplace(dict(zip(variables, s))) if not isinstance(expr, BooleanFunction): return expr # get variables in case not deep or after doing # deep simplification since they may have changed variables = _find_predicates(expr) if not force and len(variables) > 8: return expr # group into constants and variable values c, v = sift(ordered(variables), lambda x: x in (True, False), binary=True) variables = c + v truthtable = [] # standardize constants to be 1 or 0 in keeping with truthtable c = [1 if i == True else 0 for i in c] for t in product((0, 1), repeat=len(v)): if expr.xreplace(dict(zip(v, t))) == True: truthtable.append(c + list(t)) big = len(truthtable) >= (2 ** (len(variables) - 1)) if form == 'dnf' or form is None and big: return SOPform(variables, truthtable) return POSform(variables, truthtable) def _finger(eq): """ Assign a 5-item fingerprint to each symbol in the equation: [ # of times it appeared as a Symbol; # of times it appeared as a Not(symbol); # of times it appeared as a Symbol in an And or Or; # of times it appeared as a Not(Symbol) in an And or Or; a sorted tuple of tuples, (i, j, k), where i is the number of arguments in an And or Or with which it appeared as a Symbol, and j is the number of arguments that were Not(Symbol); k is the number of times that (i, j) was seen. ] Examples ======== >>> from sympy.logic.boolalg import _finger as finger >>> from sympy import And, Or, Not, Xor, to_cnf, symbols >>> from sympy.abc import a, b, x, y >>> eq = Or(And(Not(y), a), And(Not(y), b), And(x, y)) >>> dict(finger(eq)) {(0, 0, 1, 0, ((2, 0, 1),)): [x], (0, 0, 1, 0, ((2, 1, 1),)): [a, b], (0, 0, 1, 2, ((2, 0, 1),)): [y]} >>> dict(finger(x & ~y)) {(0, 1, 0, 0, ()): [y], (1, 0, 0, 0, ()): [x]} In the following, the (5, 2, 6) means that there were 6 Or functions in which a symbol appeared as itself amongst 5 arguments in which there were also 2 negated symbols, e.g. ``(a0 | a1 | a2 | ~a3 | ~a4)`` is counted once for a0, a1 and a2. >>> dict(finger(to_cnf(Xor(*symbols('a:5'))))) {(0, 0, 8, 8, ((5, 0, 1), (5, 2, 6), (5, 4, 1))): [a0, a1, a2, a3, a4]} The equation must not have more than one level of nesting: >>> dict(finger(And(Or(x, y), y))) {(0, 0, 1, 0, ((2, 0, 1),)): [x], (1, 0, 1, 0, ((2, 0, 1),)): [y]} >>> dict(finger(And(Or(x, And(a, x)), y))) Traceback (most recent call last): ... NotImplementedError: unexpected level of nesting So y and x have unique fingerprints, but a and b do not. """ f = eq.free_symbols d = dict(list(zip(f, [[0]*4 + [defaultdict(int)] for fi in f]))) for a in eq.args: if a.is_Symbol: d[a][0] += 1 elif a.is_Not: d[a.args[0]][1] += 1 else: o = len(a.args), sum(isinstance(ai, Not) for ai in a.args) for ai in a.args: if ai.is_Symbol: d[ai][2] += 1 d[ai][-1][o] += 1 elif ai.is_Not: d[ai.args[0]][3] += 1 else: raise NotImplementedError('unexpected level of nesting') inv = defaultdict(list) for k, v in ordered(iter(d.items())): v[-1] = tuple(sorted([i + (j,) for i, j in v[-1].items()])) inv[tuple(v)].append(k) return inv def bool_map(bool1, bool2): """ Return the simplified version of bool1, and the mapping of variables that makes the two expressions bool1 and bool2 represent the same logical behaviour for some correspondence between the variables of each. If more than one mappings of this sort exist, one of them is returned. For example, And(x, y) is logically equivalent to And(a, b) for the mapping {x: a, y:b} or {x: b, y:a}. If no such mapping exists, return False. Examples ======== >>> from sympy import SOPform, bool_map, Or, And, Not, Xor >>> from sympy.abc import w, x, y, z, a, b, c, d >>> function1 = SOPform([x, z, y],[[1, 0, 1], [0, 0, 1]]) >>> function2 = SOPform([a, b, c],[[1, 0, 1], [1, 0, 0]]) >>> bool_map(function1, function2) (y & ~z, {y: a, z: b}) The results are not necessarily unique, but they are canonical. Here, ``(w, z)`` could be ``(a, d)`` or ``(d, a)``: >>> eq = Or(And(Not(y), w), And(Not(y), z), And(x, y)) >>> eq2 = Or(And(Not(c), a), And(Not(c), d), And(b, c)) >>> bool_map(eq, eq2) ((x & y) | (w & ~y) | (z & ~y), {w: a, x: b, y: c, z: d}) >>> eq = And(Xor(a, b), c, And(c,d)) >>> bool_map(eq, eq.subs(c, x)) (c & d & (a | b) & (~a | ~b), {a: a, b: b, c: d, d: x}) """ def match(function1, function2): """Return the mapping that equates variables between two simplified boolean expressions if possible. By "simplified" we mean that a function has been denested and is either an And (or an Or) whose arguments are either symbols (x), negated symbols (Not(x)), or Or (or an And) whose arguments are only symbols or negated symbols. For example, And(x, Not(y), Or(w, Not(z))). Basic.match is not robust enough (see issue 4835) so this is a workaround that is valid for simplified boolean expressions """ # do some quick checks if function1.__class__ != function2.__class__: return None # maybe simplification makes them the same? if len(function1.args) != len(function2.args): return None # maybe simplification makes them the same? if function1.is_Symbol: return {function1: function2} # get the fingerprint dictionaries f1 = _finger(function1) f2 = _finger(function2) # more quick checks if len(f1) != len(f2): return False # assemble the match dictionary if possible matchdict = {} for k in f1.keys(): if k not in f2: return False if len(f1[k]) != len(f2[k]): return False for i, x in enumerate(f1[k]): matchdict[x] = f2[k][i] return matchdict a = simplify_logic(bool1) b = simplify_logic(bool2) m = match(a, b) if m: return a, m return m def simplify_patterns_and(): from sympy.functions.elementary.miscellaneous import Min, Max from sympy.core import Wild from sympy.core.relational import Eq, Ne, Ge, Gt, Le, Lt a = Wild('a') b = Wild('b') c = Wild('c') # With a better canonical fewer results are required _matchers_and = ((And(Eq(a, b), Ge(a, b)), Eq(a, b)), (And(Eq(a, b), Gt(a, b)), S.false), (And(Eq(a, b), Le(a, b)), Eq(a, b)), (And(Eq(a, b), Lt(a, b)), S.false), (And(Ge(a, b), Gt(a, b)), Gt(a, b)), (And(Ge(a, b), Le(a, b)), Eq(a, b)), (And(Ge(a, b), Lt(a, b)), S.false), (And(Ge(a, b), Ne(a, b)), Gt(a, b)), (And(Gt(a, b), Le(a, b)), S.false), (And(Gt(a, b), Lt(a, b)), S.false), (And(Gt(a, b), Ne(a, b)), Gt(a, b)), (And(Le(a, b), Lt(a, b)), Lt(a, b)), (And(Le(a, b), Ne(a, b)), Lt(a, b)), (And(Lt(a, b), Ne(a, b)), Lt(a, b)), # Min/max (And(Ge(a, b), Ge(a, c)), Ge(a, Max(b, c))), (And(Ge(a, b), Gt(a, c)), ITE(b > c, Ge(a, b), Gt(a, c))), (And(Gt(a, b), Gt(a, c)), Gt(a, Max(b, c))), (And(Le(a, b), Le(a, c)), Le(a, Min(b, c))), (And(Le(a, b), Lt(a, c)), ITE(b < c, Le(a, b), Lt(a, c))), (And(Lt(a, b), Lt(a, c)), Lt(a, Min(b, c))), # Sign (And(Eq(a, b), Eq(a, -b)), And(Eq(a, S.Zero), Eq(b, S.Zero))), ) return _matchers_and def simplify_patterns_or(): from sympy.functions.elementary.miscellaneous import Min, Max from sympy.core import Wild from sympy.core.relational import Eq, Ne, Ge, Gt, Le, Lt a = Wild('a') b = Wild('b') c = Wild('c') _matchers_or = ((Or(Eq(a, b), Ge(a, b)), Ge(a, b)), (Or(Eq(a, b), Gt(a, b)), Ge(a, b)), (Or(Eq(a, b), Le(a, b)), Le(a, b)), (Or(Eq(a, b), Lt(a, b)), Le(a, b)), (Or(Ge(a, b), Gt(a, b)), Ge(a, b)), (Or(Ge(a, b), Le(a, b)), S.true), (Or(Ge(a, b), Lt(a, b)), S.true), (Or(Ge(a, b), Ne(a, b)), S.true), (Or(Gt(a, b), Le(a, b)), S.true), (Or(Gt(a, b), Lt(a, b)), Ne(a, b)), (Or(Gt(a, b), Ne(a, b)), Ne(a, b)), (Or(Le(a, b), Lt(a, b)), Le(a, b)), (Or(Le(a, b), Ne(a, b)), S.true), (Or(Lt(a, b), Ne(a, b)), Ne(a, b)), # Min/max (Or(Ge(a, b), Ge(a, c)), Ge(a, Min(b, c))), (Or(Ge(a, b), Gt(a, c)), ITE(b > c, Gt(a, c), Ge(a, b))), (Or(Gt(a, b), Gt(a, c)), Gt(a, Min(b, c))), (Or(Le(a, b), Le(a, c)), Le(a, Max(b, c))), (Or(Le(a, b), Lt(a, c)), ITE(b >= c, Le(a, b), Lt(a, c))), (Or(Lt(a, b), Lt(a, c)), Lt(a, Max(b, c))), ) return _matchers_or def simplify_patterns_xor(): from sympy.functions.elementary.miscellaneous import Min, Max from sympy.core import Wild from sympy.core.relational import Eq, Ne, Ge, Gt, Le, Lt a = Wild('a') b = Wild('b') c = Wild('c') _matchers_xor = ((Xor(Eq(a, b), Ge(a, b)), Gt(a, b)), (Xor(Eq(a, b), Gt(a, b)), Ge(a, b)), (Xor(Eq(a, b), Le(a, b)), Lt(a, b)), (Xor(Eq(a, b), Lt(a, b)), Le(a, b)), (Xor(Ge(a, b), Gt(a, b)), Eq(a, b)), (Xor(Ge(a, b), Le(a, b)), Ne(a, b)), (Xor(Ge(a, b), Lt(a, b)), S.true), (Xor(Ge(a, b), Ne(a, b)), Le(a, b)), (Xor(Gt(a, b), Le(a, b)), S.true), (Xor(Gt(a, b), Lt(a, b)), Ne(a, b)), (Xor(Gt(a, b), Ne(a, b)), Lt(a, b)), (Xor(Le(a, b), Lt(a, b)), Eq(a, b)), (Xor(Le(a, b), Ne(a, b)), Ge(a, b)), (Xor(Lt(a, b), Ne(a, b)), Gt(a, b)), # Min/max (Xor(Ge(a, b), Ge(a, c)), And(Ge(a, Min(b, c)), Lt(a, Max(b, c)))), (Xor(Ge(a, b), Gt(a, c)), ITE(b > c, And(Gt(a, c), Lt(a, b)), And(Ge(a, b), Le(a, c)))), (Xor(Gt(a, b), Gt(a, c)), And(Gt(a, Min(b, c)), Le(a, Max(b, c)))), (Xor(Le(a, b), Le(a, c)), And(Le(a, Max(b, c)), Gt(a, Min(b, c)))), (Xor(Le(a, b), Lt(a, c)), ITE(b < c, And(Lt(a, c), Gt(a, b)), And(Le(a, b), Ge(a, c)))), (Xor(Lt(a, b), Lt(a, c)), And(Lt(a, Max(b, c)), Ge(a, Min(b, c)))), ) return _matchers_xor