Structural Pattern Matching in Python 3.10

Stellt hier eure Projekte vor.
Internetseiten, Skripte, und alles andere bzgl. Python.
Antworten
Benutzeravatar
pillmuncher
User
Beiträge: 1484
Registriert: Samstag 21. März 2009, 22:59
Wohnort: Pfaffenwinkel

Dieser Thread war ein willkommener Anlass, das neue Pattern Matching auszuprobieren.

Mein Fazit: hmmm... Es ist jedenfalls expressiver als das Visitor Pattern und in einfachen Fällen auch deutlich übersichtlicher, aber wenn die Pattern komplizierter werden, haben Sprachen wie Prolog oder Haskell die Nase immer noch vorn.

BTW: Expression Trees und Monaden sind cool.

Code: Alles auswählen

from ast import (
    AST,
    BinOp,
    BitAnd as And,
    BitOr as Or,
    Name,
    USub as Not,
    UnaryOp,
    dump
)
from collections import defaultdict
from dataclasses import dataclass
from functools import partial, reduce

from toolz.functoolz import compose


@dataclass
class Expression:

    node: AST

    def __repr__(self):
        return dump(self.node)

    def __str__(self):
        return stringify(self.node)


unit = Expression


def bind(expr, mfunc):
    return mfunc(expr.node)


def mlift(func):
    return compose(unit, func)


@mlift
def name(id):
    return Name(id=id)


def unary_op(op):
    @mlift
    def op_method(operand):
        return UnaryOp(op(), operand.node)
    return op_method


def binary_op(op):
    @mlift
    def op_method(left, right):
        return BinOp(left.node, op(), right.node)
    return op_method


Expression.__or__ = binary_op(Or)
Expression.__and__ = binary_op(And)
Expression.__neg__ = unary_op(Not)


def str_or(left, right):
    return f'({left} | {right})'


def str_and(left, right):
    return f'({left} & {right})'


def str_not(operand):
    return f'-{operand}'


def stringify(node):

    match node:

        # Terminal:
        case Name():
            return node.id

        # Disjunction:
        case BinOp(op=Or()):
            return str_or(stringify(node.left), stringify(node.right))

        # Conjunction:
        case BinOp(op=And()):
            return str_and(stringify(node.left), stringify(node.right))

        # Negation:
        case UnaryOp(op=Not()):
            return str_not(stringify(node.operand))

        # Error:
        case _:
            raise TypeError(f'Unknown type: {type(node)}')


def op_or(left, right):
    return BinOp(op=Or(), left=left, right=right)


def op_and(left, right):
    return BinOp(op=And(), left=left, right=right)


def op_not(operand):
    return UnaryOp(op=Not(), operand=operand)


def _normalize(node):

    match node:

        # Terminal:
        case Name():
            return node

        # Disjunction:
        case BinOp(op=Or()):
            return _normalize_or(node.left, node.right)

        # Conjunction:
        case BinOp(op=And()):
            return _normalize_and(node.left, node.right)

        # Negation:
        case UnaryOp(op=Not()):
            return _normalize_not(node.operand)

        # Error:
        case _:
            raise TypeError(f'Unknown type: {type(node)}')


def _normalize_or(left, right):

    match [_normalize(left), _normalize(right)]:

        # associate right (a | b) | c <==> a | (b | c):
        case [BinOp(op=Or(), left=inner_left, right=inner_right), right]:
            return _normalize(op_or(inner_left, op_and(inner_right, right)))

        # already in normal form:
        case [left, right]:
            return op_or(left, right)


def _normalize_and(left, right):

    match [_normalize(left), _normalize(right)]:

        # distribute a & (b | c) <==> (a & b) | (a & c):
        case [left, BinOp(op=Or(), left=inner_left, right=inner_right)]:
            return _normalize(op_or(op_and(left, inner_left),
                                    op_and(left, inner_right)))

        # distribute (a | b) & c <==> (a & c) | (b & c):
        case [BinOp(op=Or(), left=inner_left, right=inner_right), right]:
            return _normalize(op_or(op_and(inner_left, right),
                                    op_and(inner_right, right)))

        # associate right (a & b) & c <==> a & (b & c):
        case [BinOp(op=And(), left=inner_left, right=inner_right), right]:
            return _normalize(op_and(inner_left, op_and(inner_right, right)))

        # already in normal form:
        case [left, right]:
            return op_and(left, right)


def _normalize_not(operand):

    match _normalize(operand):

        # DeMorgan's Law -(p | q) <==> (-p & -q):
        case BinOp(op=Or(), left=left, right=right):
            return _normalize(op_and(op_not(left), op_not(right)))

        # DeMorgan's Law -(p & q) <==> (-p | -q):
        case BinOp(op=And(), left=left, right=right):
            return _normalize(op_or(op_not(left), op_not(right)))

        # double negation -(-p) <==> p:
        case UnaryOp(op=Not(), operand=operand):
            return operand

        # already normalized:
        case operand:
            return op_not(operand)


normalize = partial(bind, mfunc=mlift(_normalize))


def evaluate(expr, **kwargs):
    return _evaluate(expr.node, defaultdict(bool, kwargs))


def _evaluate(node, env):

    match node:

        # Terminal:
        case Name():
            return env[node.id]

        # Disjunction:
        case BinOp(op=Or()):
            return _evaluate(node.left, env) or _evaluate(node.right, env)

        # Conjunction:
        case BinOp(op=And()):
            return _evaluate(node.left, env) and _evaluate(node.right, env)

        # Negation:
        case UnaryOp(op=Not()):
            return not _evaluate(node.operand, env)

        # Error:
        case _:
            raise TypeError(f'Unknown type: {type(node)}')


a = name('a')
b = name('b')
c = name('c')
expr = (a | -(b & -c)) & b
print(repr(expr))
print(expr)
print(normalize(expr))
print(evaluate(expr, a=True, b=True, c=False))
Ergebnis:

Code: Alles auswählen

BinOp(left=BinOp(left=Name(id='a'), op=BitOr(), right=UnaryOp(op=USub(), operand=BinOp(left=Name(id='b'), op=BitAnd(), right=UnaryOp(op=USub(), operand=Name(id='c'))))), op=BitAnd(), right=Name(id='b'))
((a | -(b & -c)) & b)
((a & b) | ((-b & b) | (c & b)))
True
In specifications, Murphy's Law supersedes Ohm's.
rogerb
User
Beiträge: 878
Registriert: Dienstag 26. November 2019, 23:24

Sehr lehrreich, Danke!

Ich weiß, die Normalform ist bereits hiermit erreicht aber man könnte ja noch etwas vereinfachen:
((-b & b) | (c & b)) <=> c & b

Wie würde man das realisieren?
Sirius3
User
Beiträge: 17737
Registriert: Sonntag 21. Oktober 2012, 17:20

@rogerb: man muß dann Vereinfachungsregeln definieren:
a | a -> a
a % a -> a
a | ~a -> True
a & ~a -> False
True | a -> a
False | a -> a
True & a -> a
False & a -> False
Benutzeravatar
pillmuncher
User
Beiträge: 1484
Registriert: Samstag 21. März 2009, 22:59
Wohnort: Pfaffenwinkel

Vorneweg: Es gibt einen Fehler in der Zeile 145. Die muss heißen:

Code: Alles auswählen

            return _normalize(op_or(inner_left, op_or(inner_right, right)))
                                                ^^^^^
Als erstes müsste man (-b & b) durch False ersetzen und anschließend (False | (b & c)) durch (b & c). Für True und False braucht man natürlich eine Konstanten-Klasse:

Code: Alles auswählen

from ast import (
    ...
    Constant as Const,
    ...
)
Wenn man zwischen Variablen und Konstanten unterscheiden will, muss man eine Indirektionsstufe einbauen:

Code: Alles auswählen

from toolz.functoolz import compose, flip

...

def unary_op(op):
    @mlift
    def op_method(operand):
        return UnaryOp(op(), promote(operand).node)
    return op_method


def binary_op(op):
    @mlift
    def op_method(left, right):
        return BinOp(promote(left).node, op(), promote(right).node)
    return op_method


Expression.__or__ = binary_op(Or)
Expression.__ror__ = flip(Expression.__or__)
Expression.__and__ = binary_op(And)
Expression.__rand__ = flip(Expression.__and__)
Expression.__neg__ = unary_op(Not)


def promote(obj):
    match obj:
        case Expression():
            return obj
        case bool():
            return Expression(Const(value=obj))
        # Error:
        case _:
            raise TypeError(f'Unknown type: {type(obj)}')
flip() ist ein Dekorator, der beim Aufruf die Argumentreihenfolge umdreht - aus foo(x, y, z) wird dann foo(z, y, x). Damit gewinnt man, dass (True | a) ebenfalls verstanden wird, auch wenn True keine Expression ist. Leider funktioniert das nicht mehr mit (True | False | a), weil das sofort zu (True | a) ausgewertet wird und nicht zu (True | (False | a)). Wenn man das möchte, muss man es genauso hinschreiben. Im Übrigen hätte man dasselbe Problem auf der rechten Seite, wenn die Binäroperatoren rechtsassoziativ wären.

Das war alles ziemlich übersichtlich. Damit man (-b & b) durch False - und natürlich auch (-b | b) durch True - ersetzen kann, muss man leider etwas mehr Arbeit investieren. Insbesondere muss man die Variablen in eine lexikalische Ordnung bringen, so das zB. (-b & (a & (c & (d & b)))) zu (a & (b & (-b & (c & d)))) umgeschrieben wird. Siehe den Code unten. Wenn man die Augen etwas zusammenkneift, findet man einen rekursiven Insertionsort. Tests gibt es keine, weil es nur ein Experiment ist.

Code: Alles auswählen

from ast import (
    AST,
    BinOp,
    BitAnd as And,
    BitOr as Or,
    Constant as Const,
    Name,
    USub as Not,
    UnaryOp,
    dump
)
from collections import defaultdict
from dataclasses import dataclass
from functools import partial, reduce

from toolz.functoolz import compose, flip


@dataclass
class Expression:

    node: AST

    def __repr__(self):
        return dump(self.node)

    def __str__(self):
        return stringify(self.node)


unit = Expression


def bind(expr, mfunc):
    return mfunc(expr.node)


def mlift(func):
    return compose(unit, func)


@mlift
def name(id):
    return Name(id=id)


def unary_op(op):
    @mlift
    def op_method(operand):
        return UnaryOp(op(), promote(operand).node)
    return op_method


def binary_op(op):
    @mlift
    def op_method(left, right):
        return BinOp(promote(left).node, op(), promote(right).node)
    return op_method


Expression.__or__ = binary_op(Or)
Expression.__ror__ = flip(Expression.__or__)
Expression.__and__ = binary_op(And)
Expression.__rand__ = flip(Expression.__and__)
Expression.__neg__ = unary_op(Not)


def promote(obj):
    match obj:
        case Expression():
            return obj
        case bool():
            return Expression(Const(value=obj))
        # Error:
        case _:
            raise TypeError(f'Unknown type: {type(obj)}')


def str_or(left, right):
    return f'({left} | {right})'


def str_and(left, right):
    return f'({left} & {right})'


def str_not(operand):
    return f'-{operand}'


def stringify(node):

    match node:

        # Variable:
        case Name():
            return node.id

        # Constant:
        case Const():
            return str(node.value)

        # Disjunction:
        case BinOp(op=Or()):
            return str_or(stringify(node.left), stringify(node.right))

        # Conjunction:
        case BinOp(op=And()):
            return str_and(stringify(node.left), stringify(node.right))

        # Negation:
        case UnaryOp(op=Not()):
            return str_not(stringify(node.operand))

        # Error:
        case _:
            raise TypeError(f'Unknown type: {type(node)}')


def op_or(left, right):
    return BinOp(op=Or(), left=left, right=right)


def op_and(left, right):
    return BinOp(op=And(), left=left, right=right)


def op_not(operand):
    return UnaryOp(op=Not(), operand=operand)


def _normalize(node):

    match node:

        # Variable:
        case Name():
            return node

        # Constant:
        case Const():
            return node

        # Disjunction:
        case BinOp(op=Or()):
            return _normalize_or(node.left, node.right)

        # Conjunction:
        case BinOp(op=And()):
            return _normalize_and(node.left, node.right)

        # Negation:
        case UnaryOp(op=Not()):
            return _normalize_not(node.operand)

        # Error:
        case _:
            raise TypeError(f'Unknown type: {type(node)}')


def _normalize_or(left, right):

    match [_normalize(left), _normalize(right)]:

        # rewrite (left | True) ==> True:
        case [left, Const(value=True)]:
            return Const(value=True)

        # rewrite (True | right) ==> True:
        case [Const(value=False), right]:
            return Const(value=True)

        # rewrite (left | False) ==> left:
        case [left, Const(value=False)]:
            return left

        # rewrite (False | right) ==> right:
        case [Const(value=False), right]:
            return right

        # rewrite (a | -a) ==> True:
        case [Name(id=left_name), UnaryOp(op=Not(), operand=Name(id=right_name))]:
            if left_name == right_name:
                return Const(value=True)
            else:
                return op_or(Name(id=left_name), op_not(Name(id=right_name)))

        # rewrite (b | a) ==> (a | b) and (a | a) ==> a:
        case [Name(id=left_name), Name(id=right_name)]:
            if left_name < right_name:
                return op_or(Name(id=left_name), Name(id=right_name))
            elif left_name > right_name:
                return op_or(Name(id=right_name), Name(id=left_name))
            else:
                return Name(id=left_name)

        # rewrite (-b | a) ==> (a | -b) and (-a | a) ==> True:
        case [UnaryOp(op=Not(), operand=Name(id=left_name)), Name(id=right_name)]:
            if left_name < right_name:
                return op_or(op_not(Name(id=left_name)), Name(id=right_name))
            elif left_name > right_name:
                return op_or(Name(id=right_name), op_not(Name(id=left_name)))
            else:
                return Const(value=True)

        # rewrite (b | (a | _)) ==> (a | (b | _)) and (a | (a | _)) ==> (a | _):
        case [Name(id=left_name),
              BinOp(op=And(), left=Name(id=inner_left_name), right=inner_right)]:
            if left_name < inner_left_name:
                return op_or(Name(id=left_name), op_or(Name(id=inner_left_name), inner_right))
            elif left_name > inner_left_name:
                return _normalize(op_or(Name(id=inner_left_name), op_or(Name(id=left_name), inner_right)))
            else:
                return _normalize(op_or(Name(id=left_name), right))

        # associate right (a | b) | c <==> a | (b | c):
        case [BinOp(op=Or(), left=inner_left, right=inner_right), right]:
            return _normalize(op_or(inner_left, op_or(inner_right, right)))

        # already in normal form:
        case [left, right]:
            return op_or(left, right)


def _normalize_and(left, right):

    match [_normalize(left), _normalize(right)]:

        # rewrite (left & True) ==> left:
        case [left, Const(value=True)]:
            return left

        # rewrite (True & right) ==> right:
        case [Const(value=True), right]:
            return right

        # rewrite (left & False) ==> False:
        case [left, Const(value=False)]:
            return Const(value=False)

        # rewrite (False & right) ==> False:
        case [Const(value=False), right]:
            return Const(value=False)

        # rewrite (a & -a) ==> False:
        case [Name(id=left_name), UnaryOp(op=Not(), operand=Name(id=right_name))]:
            if left_name == right_name:
                return Const(value=False)
            else:
                return op_and(Name(id=left_name), op_not(Name(id=right_name)))

        # rewrite (b & a) ==> (a & b) and (a & a) ==> a:
        case [Name(id=left_name), Name(id=right_name)]:
            if left_name < right_name:
                return op_and(Name(id=left_name), Name(id=right_name))
            elif left_name > right_name:
                return op_and(Name(id=right_name), Name(id=left_name))
            else:
                return Name(id=left_name)

        # rewrite (-b & a) ==> (a & -b) and (-a & a) ==> False:
        case [UnaryOp(op=Not(), operand=Name(id=left_name)), Name(id=right_name)]:
            if left_name < right_name:
                return op_and(op_not(Name(id=left_name)), Name(id=right_name))
            elif left_name > right_name:
                return op_and(Name(id=right_name), op_not(Name(id=left_name)))
            else:
                return Const(value=False)

        # rewrite (b & (a & _)) ==> (a & (b & _)) and (a & (a & _)) ==> (a & _):
        case [Name(id=left_name),
              BinOp(op=And(), left=Name(id=inner_left_name), right=inner_right)]:
            if left_name < inner_left_name:
                return op_and(Name(id=left_name), op_and(Name(id=inner_left_name), inner_right))
            elif left_name > inner_left_name:
                return _normalize(op_and(Name(id=inner_left_name), op_and(Name(id=left_name), inner_right)))
            else:
                return _normalize(op_and(Name(id=left_name), right))

        # distribute a & (b | c) <==> (a & b) | (a & c):
        case [left, BinOp(op=Or(), left=inner_left, right=inner_right)]:
            return _normalize(op_or(op_and(left, inner_left), op_and(left, inner_right)))

        # distribute (a | b) & c <==> (a & c) | (b & c):
        case [BinOp(op=Or(), left=inner_left, right=inner_right), right]:
            return _normalize(op_or(op_and(inner_left, right), op_and(inner_right, right)))

        # associate right (a & b) & c <==> a & (b & c):
        case [BinOp(op=And(), left=inner_left, right=inner_right), right]:
            return _normalize(op_and(inner_left, op_and(inner_right, right)))

        # already in normal form:
        case [left, right]:
            return op_and(left, right)


def _normalize_not(operand):

    match _normalize(operand):

        # DeMorgan's Law -(p | q) <==> (-p & -q):
        case BinOp(op=Or(), left=left, right=right):
            return _normalize(op_and(op_not(left), op_not(right)))

        # DeMorgan's Law -(p & q) <==> (-p | -q):
        case BinOp(op=And(), left=left, right=right):
            return _normalize(op_or(op_not(left), op_not(right)))

        # double negation -(-p) <==> p:
        case UnaryOp(op=Not(), operand=operand):
            return operand

        # rewrite -False ==> True
        case Const(value=False):
            return Const(value=True)

        # rewrite -True ==> False
        case Const(value=True):
            return Const(value=False)

        # already normalized:
        case operand:
            return op_not(operand)


normalize = partial(bind, mfunc=mlift(_normalize))


def evaluate(expr, **kwargs):
    return _evaluate(expr.node, defaultdict(bool, kwargs))


def _evaluate(node, env):

    match node:

        # Variable:
        case Name():
            return env[node.id]

        # Constant:
        case Const():
            return node.value

        # Disjunction:
        case BinOp(op=Or()):
            return _evaluate(node.left, env) or _evaluate(node.right, env)

        # Conjunction:
        case BinOp(op=And()):
            return _evaluate(node.left, env) and _evaluate(node.right, env)

        # Negation:
        case UnaryOp(op=Not()):
            return not _evaluate(node.operand, env)

        # Error:
        case _:
            raise TypeError(f'Unknown type: {type(node)}')


a = name('a')
b = name('b')
c = name('c')
expr = (a | -(b & -c)) & (False | b)
print(repr(expr))
print(expr)
print(normalize(expr))
print(evaluate(expr, a=True, b=True, c=False))
Bitte melden, wenn was nicht geht.

Man könnte noch die überflüssigen Klammern loswerden. Dazu muss man nur schauen, on der Operand einer Negation ein binärer Operatorenausdruck ist, dann braucht man die Klammern, oder ob eine Disjunktion als Operand in einer Konjunktion vorkommt, dann ebenfalls, und alle anderen kann man weglassen. Vielleicht morgen.
In specifications, Murphy's Law supersedes Ohm's.
Benutzeravatar
pillmuncher
User
Beiträge: 1484
Registriert: Samstag 21. März 2009, 22:59
Wohnort: Pfaffenwinkel

Jetzt neu mit Guard Clauses (u.a.):

Code: Alles auswählen

from ast import AST, BinOp, BitAnd, BitOr, Constant, Name, USub, UnaryOp, dump
from collections import defaultdict
from dataclasses import dataclass

from toolz.functoolz import compose, flip


@dataclass
class Expression:

    node: AST

    def __repr__(self):
        return f'Expression({dump(self.node)})'

    def __str__(self):
        return str(self.node)


unit = Expression


def bind(expr, mfunc):
    return mfunc(expr.node)


def mlift(func):
    return compose(unit, func)


class Variable(Name):

    def __str__(self):
        return self.id

    def evaluate(self, env):
        return env[self.id]

    def normalize(self):
        return self

    def simplify(self):
        return self


class Constant(Constant):

    def __str__(self):
        return str(self.value)

    def evaluate(self, env):
        return self.value

    def normalize(self):
        return self

    def simplify(self):
        return self


class Not(UnaryOp):

    def __init__(self, operand):
        super().__init__(op=USub(), operand=operand)

    def __str__(self):
        match self.operand:
            case BinOp():
                return f'-({self.operand})'
            case _:
                return f'-{self.operand}'

    def evaluate(self, env):
        return not self.operand.evaluate(env)

    def normalize(self):

        match self.operand.normalize():

            # DeMorgan's Law -(p | q) <==> (-p & -q):
            case Or(left=p, right=q):
                return And(Not(p), Not(q)).normalize()

            # DeMorgan's Law -(p & q) <==> (-p | -q):
            case And(left=p, right=q):
                return Or(Not(p), Not(q)).normalize()

            # double negation -(-p) <==> p:
            case Not(operand=p):
                return p

            # already normalized:
            case operand:
                return Not(operand)

    def simplify(self):

        match self.operand.simplify():

            # double negation -(-p) <==> p:
            case Not(operand=p):
                return p

            # invert:
            case Constant(value=value):
                return Constant(not value)

            # already normalized:
            case operand:
                return Not(operand)


class And(BinOp):

    def __init__(self, left, right):
        super().__init__(op=BitAnd(), left=left, right=right)

    def __str__(self):
        def maybe_parens(node):
            match node:
                case Or():
                    return f'({node})'
                case _:
                    return f'{node}'
        return f'{maybe_parens(self.left)} & {maybe_parens(self.right)}'

    def evaluate(self, env):
        return self.left.evaluate(env) and self.right.evaluate(env)

    def normalize(self):

        match [self.left.normalize(), self.right.normalize()]:

            # associate right (p & q) & r <==> p & (q & r):
            case [And(left=p, right=q), r]:
                return And(p, And(q, r)).normalize()

            # distribute p & (q | r) <==> (p & q) | (p & r):
            case [p, Or(left=q, right=r)]:
                return Or(And(p, q), And(p, r)).normalize()

            # distribute (p | q) & r <==> (p & r) | (q & r):
            case [Or(left=p, right=q), r]:
                return Or(And(p, r), And(q, r)).normalize()

            # rewrite (b & (a & p)) ==> (a & (b & p)):
            case [Variable(id=b), And(left=Variable(id=a), right=p)] if b > a:
                return And(Variable(a), And(Variable(b), p)).normalize()

            # rewrite (b & (-a & p)) ==> (-a & (b & p)):
            case [Variable(id=b), And(left=Not(operand=Variable(id=a)), right=p)] if b > a:
                return And(Not(Variable(a)), And(Variable(b), p)).normalize()

            # rewrite (-b & (a & p)) ==> (a & (-b & p)):
            case [Not(operand=Variable(id=b)), And(left=Variable(id=a), right=p)] if b > a:
                return And(Variable(a), And(Not(Variable(b), p))).normalize()

            # rewrite (-b & (-a & p)) ==> (-a & (-b & p)):
            case [Not(operand=Variable(id=b)), And(left=Not(operand=Variable(id=a)), right=p)] if b > a:
                return And(Not(Variable(a)), And(Not(operand=Variable(b)), p)).normalize()

            # rewrite (b & a) ==> (a & b):
            case [Variable(id=b), Variable(id=a)] if b > a:
                return And(Variable(a), Variable(b))

            # rewrite (b & -a) ==> (-a & b):
            case [Variable(id=b), Not(operand=Variable(id=a))] if b > a:
                return And(Not(Variable(a)), Variable(b))

            # rewrite (-b & a) ==> (a & -b):
            case [Not(operand=Variable(id=b)), Variable(id=a)] if b > a:
                return And(Variable(a), Not(Variable(b)))

            # rewrite (-b & -a) ==> (-a & -b):
            case [Not(operand=Variable(id=b)), Not(operand=Variable(id=a))] if b > a:
                return And(Not(Variable(a)), Not(Variable(b)))

            # already in normal form:
            case [left, right]:
                return And(left, right)

    def simplify(self):

        match [self.left.simplify(), self.right.simplify()]:

            # rewrite (p & True) ==> p:
            case [p, Constant(value=True)]:
                return p

            # rewrite (True & q) ==> q:
            case [Constant(value=True), q]:
                return q

            # rewrite (p & False) ==> False:
            case [p, Constant(value=False)]:
                return Constant(False)

            # rewrite (False & q) ==> False:
            case [Constant(value=False), q]:
                return Constant(False)

            # rewrite (a & a) ==> a:
            case [Variable(id=a1), Variable(id=a2)] if a1 == a2:
                return Variable(a1)

            # rewrite (a & -a) ==> False:
            case [Variable(id=a1), Not(operand=Variable(id=a2))] if a1 == a2:
                return Constant(False)

            # rewrite (-a & a) ==> False:
            case [Not(operand=Variable(id=a1)), Variable(id=a2)] if a1 == a2:
                return Constant(False)

            # rewrite (-a & -a) ==> -a:
            case [Not(operand=Variable(id=a1)), Not(operand=Variable(id=a2))] if a1 == a2:
                return Not(Variable(a1))

            # rewrite (a & (a & p)) ==> (a & p):
            case [Variable(id=a1), And(left=Variable(id=a2), right=p)] if a1 == a2:
                return And(Variable(a2), p)

            # rewrite (a & (-a & p)) ==> False:
            case [Variable(id=a1), And(left=Not(operand=Variable(id=a2)), right=p)] if a1 == a2:
                return Constant(False)

            # rewrite (-a & (a & p)) ==> False:
            case [Not(operand=Variable(id=a1)), And(left=Variable(id=a2), right=p)] if a1 == a2:
                return Constant(False)

            # rewrite (-a & (-a & p)) ==> (-a & p):
            case [Not(operand=Variable(id=a1)), And(left=Not(operand=Variable(id=a2)), right=p)] if a1 == a2:
                return And(Not(operand=Variable(a2)), p)

            # already in normal form:
            case [left, right]:
                return And(left, right)


class Or(BinOp):

    def __init__(self, left, right):
        super().__init__(op=BitOr(), left=left, right=right)

    def __str__(self):
        return f'{self.left} | {self.right}'

    def evaluate(self, env):
        return self.left.evaluate(env) or self.right.evaluate(env)

    def normalize(self):

        match [self.left.normalize(), self.right.normalize()]:

            # associate right ((p | q) | r) <==> (p | (q | r)):
            case [Or(left=p, right=q), r]:
                return Or(p, Or(q, r)).normalize()

            # rewrite (b | (a | p)) ==> (a | (b | p)):
            case [Variable(id=b), Or(left=Variable(id=a), right=p)] if b > a:
                return Or(Variable(a), Or(Variable(b), p)).normalize()

            # rewrite (b | (-a | p)) ==> (-a | (b | p)):
            case [Variable(id=b), Or(left=Not(operand=Variable(id=a)), right=p)] if b > a:
                return Or(Not(Variable(a)), Or(Variable(b), p)).normalize()

            # rewrite (-b | (a | p)) ==> (a | (-b | p)):
            case [Not(operand=Variable(id=b)), Or(left=Not(operand=Variable(id=a)), right=p)] if b > a:
                return Or(Variable(a), Or(Not(Variable(b), p))).normalize()

            # rewrite (-b | (-a | p)) ==> (-a | (-b | p)):
            case [Not(operand=Variable(id=b)), Or(left=Not(operand=Variable(id=a)), right=p)] if b > a:
                return Or(Not(Variable(a)), Or(Not(operand=Variable(b)), p)).normalize()

            # rewrite (b | a) ==> (a | b):
            case [Variable(id=b), Variable(id=a)] if b > a:
                return Or(Variable(a), Variable(b))

            # rewrite (b | -a) ==> (-a | b):
            case [Variable(id=b), Not(operand=Variable(id=a))] if b > a:
                return Or(Not(Variable(a)), Variable(b))

            # rewrite (-b | a) ==> (a | -b):
            case [Not(operand=Variable(id=b)), Variable(id=a)] if b > a:
                return Or(Variable(a), Not(Variable(b)))

            # rewrite (-b | -a) ==> (-a | -b):
            case [Not(operand=Variable(id=b)), Not(operand=Variable(id=a))] if b > a:
                return Or(Not(Variable(a)), Not(Variable(b)))

            # already in normal form:
            case [left, right]:
                return Or(left, right)

    def simplify(self):

        match [self.left.simplify(), self.right.simplify()]:

            # rewrite (p | True) ==> True:
            case [p, Constant(value=True)]:
                return Constant(True)

            # rewrite (True | q) ==> True:
            case [Constant(value=True), q]:
                return Constant(True)

            # rewrite (p | False) ==> p:
            case [p, Constant(value=False)]:
                return p

            # rewrite (False | q) ==> q:
            case [Constant(value=False), q]:
                return q

            # rewrite (a | a) ==> a:
            case [Variable(id=a1), Variable(id=a2)] if a1 == a2:
                return Variable(a1)

            # rewrite (a | -a) ==> True:
            case [Variable(id=a1), Not(operand=Variable(id=a2))] if a1 == a2:
                return Constant(True)

            # rewrite (-a | a) ==> True:
            case [Not(operand=Variable(id=a1)), Variable(id=a2)] if a1 == a2:
                return Constant(True)

            # rewrite (-a | -a) ==> -a:
            case [Not(operand=Variable(id=a1)), Not(operand=Variable(id=a2))] if a1 == a2:
                return Not(Variable(a1))

            # rewrite (a | (a | p)) ==> (a | p):
            case [Variable(id=a1), Or(left=Variable(id=a2), right=p)] if a1 == a2:
                return Or(Variable(a2), p)

            # rewrite (a | (-a | p)) ==> True:
            case [Variable(id=a1), Or(left=Not(operand=Variable(id=a2)), right=p)] if a1 == a2:
                return Constant(True)

            # rewrite (-a | (a | p)) ==> True:
            case [Not(operand=Variable(id=a1)), Or(left=Variable(id=a2), right=p)] if a1 == a2:
                return Constant(True)

            # rewrite (-a | (-a | p)) ==> (-a | p):
            case [Not(operand=Variable(id=a1)), Or(left=Not(operand=Variable(id=a2)), right=p)] if a1 == a2:
                return Or(Not(operand=Variable(a2)), p)

            # already simplified:
            case [left, right]:
                return Or(left, right)


@mlift
def name(id):
    return Variable(id=id)


@mlift
def operator_not(operand):
    return Not(operand=promote(operand).node)


@mlift
def operator_and(left, right):
    return And(left=promote(left).node, right=promote(right).node)


@mlift
def operator_or(left, right):
    return Or(left=promote(left).node, right=promote(right).node)


Expression.__neg__ = operator_not
Expression.__and__ = operator_and
Expression.__rand__ = flip(operator_and)
Expression.__or__ = operator_or
Expression.__ror__ = flip(operator_or)


def promote(obj):
    match obj:
        case Expression():
            return obj
        case bool():
            return Expression(Constant(obj))
        # Error:
        case _:
            raise TypeError(f'Unknown type: {type(obj)}')


@mlift
def normalize(expr, simplify=False):
    if simplify:
        return expr.node.normalize().simplify()
    else:
        return expr.node.normalize()


@mlift
def evaluate(expr, **kwargs):
    return Constant(expr.node.evaluate(defaultdict(bool, kwargs)))


def main():
    a = name('a')
    b = name('b')
    c = name('c')
    expr = (a | -(b & -c)) & (b | False)
    print(repr(expr))
    print(expr)
    print(normalize(expr))
    print(normalize(expr, simplify=True))
    print(evaluate(expr, a=True, b=True, c=False))


if __name__ == '__main__':
    main()
Als ich das zum letzten Mal vor ca. 100 Jahren in Prolog programmiert habe, ging das irgendwie kürzer...

Ergebnis:

Code: Alles auswählen

Expression(And(left=Or(left=Variable(id='a'), op=BitOr(), right=Not(op=USub(), operand=And(left=Variable(id='b'), op=BitAnd(), right=Not(op=USub(), operand=Variable(id='c'))))), op=BitAnd(), right=Or(left=Variable(id='b'), op=BitOr(), right=Constant(value=False))))
(a | -(b & -c)) & (b | False)
a & b | -b & b | b & c | a & False | -b & False | c & False
a & b | b & c
True
In specifications, Murphy's Law supersedes Ohm's.
Antworten