diff --git a/.gitignore b/.gitignore index cc266fc..37c7e11 100644 --- a/.gitignore +++ b/.gitignore @@ -6,3 +6,5 @@ !/notes !/protocol !/protocol/*.md + +!/code diff --git a/code/.gitignore b/code/.gitignore new file mode 100644 index 0000000..bf7b032 --- /dev/null +++ b/code/.gitignore @@ -0,0 +1,3 @@ +* +!/.gitignore +!/*.py diff --git a/code/__init__.py b/code/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/code/main.py b/code/main.py new file mode 100644 index 0000000..f16a6b6 --- /dev/null +++ b/code/main.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- + +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +# IMPORTS +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +from __future__ import annotations; +import os; +import sys; +sys.tracebacklimit = 0; +from itertools import product; +from typing import Dict; +from typing import Generator; +from typing import List; +from typing import Tuple; +from typing import Union; +from lark import Tree; + +sys.path.insert(0, os.getcwd()); + +from schema import string_to_parts; + +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +# GLOBAL CONSTANTS +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +# zeichenkette = 'A0'; +# zeichenkette = '! A0'; +# zeichenkette = '( A0 && A1 )'; +# zeichenkette = '( A0 || A1 )'; +# zeichenkette = '( A0 -> A1 )'; +zeichenkette = '( A0 -> ((A0 && A3) || ! A2) )'; +# zeichenkette = '(( {G} || !{G} ) -> A5)'; + +I = ['A0', 'A2']; + +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +# HAUPTVORGANG +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +def main(): + tree = string_to_parts(zeichenkette); + print('Syntaxbaum von \033[1m{}\033[0m:\n'.format(zeichenkette)); + print(tree.pretty()); + val = rekursiv_eval(tree, I) + print('eval(Formel, I) = \033[1m{}\033[0m'.format(val)); + return; + +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +# SEKUNDÄRVORGÄNGE +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +def rekursiv_eval(fml: Tree, I: List[str]) -> bool: + if fml.data == 'atom': + index = fml.children[0]; + return 'A{}'.format(index) in I; + elif fml.data == 'beliebig': + name = fml.children[0]; + return '{}'.format(name) in I; + elif fml.data == 'wahr': + return True; + elif fml.data == 'falsch': + return False; + elif fml.data == 'negation': + teilformel1 = fml.children[1]; + if isinstance(teilformel1, Tree): + val1 = rekursiv_eval(teilformel1, I); + return not val1; + elif fml.data == 'konjunktion': + teilformel1 = fml.children[0]; + teilformel2 = fml.children[2]; + if isinstance(teilformel1, Tree) and isinstance(teilformel2, Tree): + val1 = rekursiv_eval(teilformel1, I); + val2 = rekursiv_eval(teilformel2, I); + return min(val1, val2); + elif fml.data == 'disjunktion': + teilformel1 = fml.children[0]; + teilformel2 = fml.children[2]; + if isinstance(teilformel1, Tree) and isinstance(teilformel2, Tree): + val1 = rekursiv_eval(teilformel1, I); + val2 = rekursiv_eval(teilformel2, I); + return max(val1, val2); + elif fml.data == 'implikation': + teilformel1 = fml.children[0]; + teilformel2 = fml.children[2]; + if isinstance(teilformel1, Tree) and isinstance(teilformel2, Tree): + val1 = rekursiv_eval(teilformel1, I); + val2 = rekursiv_eval(teilformel2, I); + return (val1 <= val2); + else: + raise Exception('Evaluation nicht möglich!'); + return True; + +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +# CODE AUSFÜHREN +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +if __name__ == '__main__': + main(); diff --git a/code/schema.py b/code/schema.py new file mode 100644 index 0000000..9ebe38d --- /dev/null +++ b/code/schema.py @@ -0,0 +1,64 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- + +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +# IMPORTS +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +from __future__ import annotations; +import re; +# install: lark; lark-parser; lark-parser[regex]. +# https://lark-parser.readthedocs.io/en/latest/grammar.html +from lark import Lark; +from lark import Tree; + +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +# GLOBAL CONSTANTS +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +## lexer +lexerAussagenlogik = Lark( + ''' + %import common.WS + %import common.NUMBER + %import common.WORD + %ignore WS + + ?start: expr + + ?expr: atomic | expr_not | expr_and | expr_or | expr_implies + ?literal: atomic | "not" atomic + + // atomische Ausdrücke + ?atomic: false | true | atom | generic + ?false: "0" -> wahr + ?true: "1" -> falsch + ?atom: "A" /[0-9]+/ -> atom + ?generic: "{" /((?!({|})).)+/ "}" -> beliebig + + // Symbole + ?conn_not: "!" -> junktor + ?conn_and: /&+/ -> junktor + ?conn_or: /\\|+/ -> junktor + ?conn_impl: /->|=>/ -> junktor + + // Junktoren + ?expr_not: conn_not expr -> negation + ?expr_and: "(" expr conn_or expr ")" -> konjunktion + ?expr_or: "(" expr conn_and expr ")" -> disjunktion + ?expr_implies: "(" expr conn_impl expr ")" -> implikation + ''', + start="expr", + regex=True +); + +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +# MAIN METHOD string -> parts +# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +def string_to_parts(u: str) -> Tree: + try: + u_lexed = lexerAussagenlogik.parse(u); + return u_lexed; + except: + raise Exception('Ausdruck \033[1m{}\033[0m konnte nicht erkannt werden!'.format(u));