master > master: codego initialisiert

codego/aussagenlogik/rekursion/rekursion.go

@@ -0,0 +1,82 @@
+package rekursion
+
+import (
+	"log"
+	"logik/aussagenlogik/syntaxbaum"
+	"logik/core/utils"
+)
+
+/* ---------------------------------------------------------------- *
+ * EXPORTS
+ * ---------------------------------------------------------------- */
+
+func RekursivEval(tree syntaxbaum.SyntaxBaum, I []string) int {
+	var children = tree.GetChildren()
+	switch tree.Kind {
+	case "atom", "generic":
+		if utils.StrListContains(I, tree.Expr) {
+			return 1
+		}
+		return 0
+	case "taut":
+		return 1
+	case "contradiction":
+		return 0
+	case "not":
+		subtree0, _ := tree.GetChild()
+		val0 := RekursivEval(subtree0, I)
+		return 1 - val0
+	case "and2":
+		val0 := RekursivEval(children[0], I)
+		val1 := RekursivEval(children[1], I)
+		return utils.Min2(val0, val1)
+	case "and":
+		var val = 1
+		for _, subtree := range children {
+			var val_ = RekursivEval(subtree, I)
+			val = utils.Min2(val, val_)
+		}
+		return val
+	case "or2":
+		val0 := RekursivEval(children[0], I)
+		val1 := RekursivEval(children[1], I)
+		return utils.Max2(val0, val1)
+	case "or":
+		var val = 0
+		for _, subtree := range children {
+			var val_ = RekursivEval(subtree, I)
+			val = utils.Max2(val, val_)
+		}
+		return val
+	case "implies":
+		val0 := RekursivEval(children[0], I)
+		val1 := RekursivEval(children[1], I)
+		if val0 <= val1 {
+			return 1
+		}
+		return 0
+	default:
+		log.Fatal("Could not evaluate expression!")
+		return 0
+	}
+}
+
+func RekursivAtoms(tree syntaxbaum.SyntaxBaum) []string {
+	// Herausforderung: schreibe diese Funktion!
+	return []string{}
+}
+
+func RekursivDepth(tree syntaxbaum.SyntaxBaum) int {
+	// Herausforderung: schreibe diese Funktion!
+	return 0
+}
+
+func RekursivLength(tree syntaxbaum.SyntaxBaum) int {
+	// Herausforderung: schreibe diese Funktion!
+	return 0
+}
+
+func RekursivParentheses(tree syntaxbaum.SyntaxBaum) int {
+	// Herausforderung: schreibe diese Funktion!
+	return 0
+}

codego/aussagenlogik/rekursion/rekursion_test.go

@@ -0,0 +1,287 @@
+package rekursion_test
+
+/* ---------------------------------------------------------------- *
+ * UNIT TESTING
+ * ---------------------------------------------------------------- */
+
+import (
+	"logik/aussagenlogik/rekursion"
+	"logik/aussagenlogik/schema"
+	"logik/aussagenlogik/syntaxbaum"
+	"logik/core/utils"
+	"testing"
+
+	"github.com/stretchr/testify/assert"
+)
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE eval(·, ·)
+ * ---------------------------------------------------------------- */
+
+func TestRekursivEvalLiteral(test *testing.T) {
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var I []string
+	var val int
+	tree, _ = schema.ParseExpr("A0")
+	I = []string{"A0"}
+	val = rekursion.RekursivEval(tree, I)
+	assert.Equal(val, 1)
+	tree, _ = schema.ParseExpr("A0")
+	I = []string{}
+	val = rekursion.RekursivEval(tree, I)
+	assert.Equal(val, 0)
+	tree, _ = schema.ParseExpr("! A0")
+	I = []string{"A0"}
+	val = rekursion.RekursivEval(tree, I)
+	assert.Equal(val, 0)
+	tree, _ = schema.ParseExpr("! A0")
+	I = []string{}
+	val = rekursion.RekursivEval(tree, I)
+	assert.Equal(val, 1)
+}
+
+func TestRekursivEvalComplex1(test *testing.T) {
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var I []string
+	var val int
+	tree, _ = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || A2 ))")
+	I = []string{"A0", "A2"}
+	val = rekursion.RekursivEval(tree, I)
+	assert.Equal(val, 1)
+	I = []string{"A0", "A3"}
+	val = rekursion.RekursivEval(tree, I)
+	assert.Equal(val, 1)
+	I = []string{"A0"}
+	val = rekursion.RekursivEval(tree, I)
+	assert.Equal(val, 0)
+	I = []string{"A4", "A8"}
+	val = rekursion.RekursivEval(tree, I)
+	assert.Equal(val, 1)
+}
+
+func TestRekursivEvalComplex2(test *testing.T) {
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var I []string
+	var val int
+	tree, _ = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || ! A2 ))")
+	I = []string{"A0", "A2"}
+	val = rekursion.RekursivEval(tree, I)
+	assert.Equal(val, 0)
+	I = []string{"A0", "A3"}
+	val = rekursion.RekursivEval(tree, I)
+	assert.Equal(val, 1)
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE Atoms(·)
+ * ---------------------------------------------------------------- */
+
+func TestRekursivAtomsNoduplicates(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val []string
+	tree, _ = schema.ParseExpr("( A4 && ( A4 || A4 ))")
+	val = rekursion.RekursivAtoms(tree)
+	var n int = len(utils.FilterStrings(&val, func(x string) bool { return x == "A4" }))
+	assert.Equal(n, 1, "Atome dürfen nicht mehrfach vorkommen!")
+}
+
+func TestRekursivAtomsNononatoms(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	test.Skip("Syntax for generic expressions in ANTLR4 g4 needs to be implemented.")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val []string
+	tree, _ = schema.ParseExpr("( {F} || A3 )")
+	val = rekursion.RekursivAtoms(tree)
+	utils.SortStrings(&val)
+	assert.NotContains(val, "F", "Nichtatomare Formeln dürfen nicht vorkommen!")
+}
+
+func TestRekursivAtomsCalc1(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val []string
+	tree, _ = schema.ParseExpr("A0")
+	val = rekursion.RekursivAtoms(tree)
+	utils.SortStrings(&val)
+	assert.Equal(val, []string{"A0"})
+}
+
+func TestRekursivAtomsCalc2(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val []string
+	tree, _ = schema.ParseExpr("((( ! A8 && A3 ) || A4 ) && A0 )")
+	val = rekursion.RekursivAtoms(tree)
+	utils.SortStrings(&val)
+	assert.Equal(val, []string{"A0", "A3", "A4", "A8"})
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE depth(·, ·)
+ * ---------------------------------------------------------------- */
+
+func TestRekursivDepthCalc1(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("A0")
+	val = rekursion.RekursivDepth(tree)
+	assert.Equal(val, 0)
+}
+
+func TestRekursivDepthCalc2(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("!! A8")
+	val = rekursion.RekursivDepth(tree)
+	assert.Equal(val, 2)
+}
+
+func TestRekursivDepthCalc3(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("( ! A0 && A3 )")
+	val = rekursion.RekursivDepth(tree)
+	assert.Equal(val, 2)
+}
+
+func TestRekursivDepthCalc4(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = rekursion.RekursivDepth(tree)
+	assert.Equal(val, 4)
+}
+
+func TestRekursivDepthCalc5(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = rekursion.RekursivDepth(tree)
+	assert.Equal(val, 5)
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE length(·)
+ * ---------------------------------------------------------------- */
+
+func TestRekursivLengthCalc1(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("A0")
+	val = rekursion.RekursivLength(tree)
+	assert.Equal(val, 1)
+}
+
+func TestRekursivLengthCalc2(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("!! A8")
+	val = rekursion.RekursivLength(tree)
+	assert.Equal(val, 3)
+}
+
+func TestRekursivLengthCalc3(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("( ! A0 && A3 )")
+	val = rekursion.RekursivLength(tree)
+	assert.Equal(val, 4)
+}
+
+func TestRekursivLengthCalc4(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = rekursion.RekursivLength(tree)
+	assert.Equal(val, 8)
+}
+
+func TestRekursivLengthCalc5(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = rekursion.RekursivLength(tree)
+	assert.Equal(val, 9)
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE #Parentheses(·)
+ * ---------------------------------------------------------------- */
+
+func TestRekursivParenthesesCalc1(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("A0")
+	val = rekursion.RekursivParentheses(tree)
+	assert.Equal(val, 0)
+}
+
+func TestRekursivParenthesesCalc2(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("!! A8")
+	val = rekursion.RekursivParentheses(tree)
+	assert.Equal(val, 0)
+}
+
+func TestRekursivParenthesesCalc3(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("( ! A0 && A3 )")
+	val = rekursion.RekursivParentheses(tree)
+	assert.Equal(val, 2)
+}
+
+func TestRekursivParenthesesCalc4(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = rekursion.RekursivParentheses(tree)
+	assert.Equal(val, 6)
+}
+
+func TestRekursivParenthesesCalc5(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var tree syntaxbaum.SyntaxBaum
+	var val int
+	tree, _ = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = rekursion.RekursivParentheses(tree)
+	assert.Equal(val, 6)
+}

codego/aussagenlogik/schema/schema.go

@@ -0,0 +1,175 @@
+package schema
+
+import (
+	"errors"
+	"logik/aussagenlogik/syntaxbaum"
+	parser "logik/grammars/aussagenlogik"
+	"strings"
+
+	"github.com/antlr/antlr4/runtime/Go/antlr"
+)
+
+/* ---------------------------------------------------------------- *
+ * EXPORTS
+ * ---------------------------------------------------------------- */
+
+func ParseExpr(u string) (syntaxbaum.SyntaxBaum, error) {
+	var lexer = createLexer(u)
+	var tokenStream = lexerToTokenStream(lexer)
+	var prs = parser.NewaussagenlogikParser(tokenStream)
+	var t = prs.Start()
+	tree, err := createSyntaxBaum(t, prs)
+	return tree, err
+}
+
+/* ---------------------------------------------------------------- *
+ * PRIVATE
+ * ---------------------------------------------------------------- */
+
+func exprToStream(u string) *antlr.InputStream {
+	return antlr.NewInputStream(u)
+}
+
+func lexerToTokenStream(lexer antlr.Lexer) antlr.TokenStream {
+	return antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)
+}
+
+func createLexer(u string) antlr.Lexer {
+	stream := exprToStream(u)
+	return parser.NewaussagenlogikLexer(stream)
+}
+
+func createSyntaxBaum(tree antlr.Tree, parser antlr.Parser) (syntaxbaum.SyntaxBaum, error) {
+	var ant = antlrTree{tree: tree, parser: &parser}
+	return ant.toSyntaxBaum()
+}
+
+/* ---------------------------------------------------------------- *
+ * Struct: antlrTree + Methods
+ * ---------------------------------------------------------------- */
+
+type antlrTree struct {
+	tree   antlr.Tree
+	parser *antlr.Parser
+}
+
+func (ant antlrTree) getChildren() []antlrTree {
+	var nodes = ant.tree.GetChildren()
+	var subants = make([]antlrTree, len(nodes))
+	for i, node := range nodes {
+		subants[i] = antlrTree{tree: node, parser: ant.parser}
+	}
+	return subants
+}
+
+func (ant antlrTree) getLabel() string {
+	return antlr.TreesGetNodeText(ant.tree, []string{}, *ant.parser)
+}
+
+func (ant antlrTree) getTextContent() string {
+	var expr string = ant.getLabel()
+	for _, subant := range ant.getChildren() {
+		expr += subant.getTextContent()
+	}
+	return expr
+}
+
+func (ant antlrTree) getTextContentLeaves() string {
+	var expr string = ""
+	var subants = ant.getChildren()
+	if len(subants) == 0 {
+		expr = ant.getLabel()
+	} else {
+		for _, subant := range subants {
+			expr += subant.getTextContent()
+		}
+	}
+	return expr
+}
+
+func (ant antlrTree) toSyntaxBaum() (syntaxbaum.SyntaxBaum, error) {
+	var tree syntaxbaum.SyntaxBaum
+	var err error
+	var label string = ant.getLabel()
+	var subants = ant.getChildren()
+	var nChildren = len(subants)
+
+	switch label {
+	case "start":
+		if nChildren == 1 {
+			return subants[0].toSyntaxBaum()
+		}
+	case "open":
+		if nChildren == 1 {
+			return subants[0].toSyntaxBaum()
+		}
+	case "closed":
+		switch nChildren {
+		case 1:
+			return subants[0].toSyntaxBaum()
+		case 3:
+			return subants[1].toSyntaxBaum()
+		}
+	case "atomic":
+		if nChildren == 1 {
+			subant := subants[0]
+			tree = syntaxbaum.SyntaxBaum{}
+			tree.Expr = subant.getTextContentLeaves()
+			tree.Kind = subant.getLabel()
+			tree.Children = [](*syntaxbaum.SyntaxBaum){}
+			tree.Valence = 0
+			return tree, nil
+		}
+	case "not":
+		if nChildren == 2 { // Children: [NotSymbol, Teilformel]
+			subtree, err := subants[1].toSyntaxBaum()
+			tree = syntaxbaum.SyntaxBaum{}
+			tree.Expr = subants[0].getTextContent() + " " + subtree.Expr
+			tree.Kind = label
+			tree.Children = [](*syntaxbaum.SyntaxBaum){&subtree}
+			tree.Valence = 1
+			return tree, err
+		}
+	case "and2", "and", "or2", "or", "implies":
+		var n int = int((len(subants) + 1) / 2)
+		if nChildren == 2*n-1 && n >= 2 {
+			var isSymb bool = false
+			var subtrees = make([](*syntaxbaum.SyntaxBaum), n)
+			var i int = 0
+			var expr string = ""
+			for _, subant := range subants {
+				if isSymb {
+					expr += " " + subant.getTextContent() + " "
+				} else {
+					subtree, err_ := subant.toSyntaxBaum()
+					if err_ != nil {
+						err = err_
+					}
+					subtrees[i] = &subtree
+					expr += " " + subtree.Expr + " "
+					i++
+				}
+				isSymb = !isSymb
+			}
+			expr = strings.Trim(expr, " ")
+			var lbrace string = "("
+			var rbrace string = ")"
+			// var lbrace string = "( "
+			// var rbrace string = " )"
+			// if strings.HasPrefix(expr, "(") {
+			// 	lbrace = "("
+			// }
+			// if strings.HasSuffix(expr, ")") {
+			// 	rbrace = ")"
+			// }
+			tree = syntaxbaum.SyntaxBaum{}
+			tree.Expr = lbrace + expr + rbrace
+			tree.Kind = label
+			tree.Children = subtrees
+			tree.Valence = n
+			return tree, err
+		}
+	}
+
+	return tree, errors.New("Could not parse expression")
+}

codego/aussagenlogik/schema/schema_test.go

@@ -0,0 +1,22 @@
+package schema_test
+
+/* ---------------------------------------------------------------- *
+ * UNIT TESTING
+ * ---------------------------------------------------------------- */
+
+import (
+	"logik/aussagenlogik/schema"
+	"testing"
+
+	"github.com/stretchr/testify/assert"
+)
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE ParseExpr
+ * ---------------------------------------------------------------- */
+
+func TestParseExpr(test *testing.T) {
+	var assert = assert.New(test)
+	assert.Equal(0, 0)
+	schema.ParseExpr("A0")
+}

codego/aussagenlogik/syntaxbaum/syntaxbaum.go

@@ -0,0 +1,136 @@
+package syntaxbaum
+
+import (
+	"errors"
+	"fmt"
+	"strings"
+)
+
+type SyntaxBaum struct {
+	Kind     string
+	Expr     string
+	Valence  int
+	Children [](*SyntaxBaum)
+}
+
+/* ---------------------------------------------------------------- *
+ * METHODS
+ * ---------------------------------------------------------------- */
+
+func (tree SyntaxBaum) GetChildren() []SyntaxBaum {
+	var n int = tree.Valence
+	var children = make([]SyntaxBaum, n)
+	for i, subtreePtr := range tree.Children {
+		children[i] = *subtreePtr
+	}
+	return children
+}
+
+func (tree SyntaxBaum) GetChild(indexOpt ...int) (SyntaxBaum, error) {
+	var index int = 0
+	if len(indexOpt) > 0 {
+		index = indexOpt[0]
+	}
+	var subtree SyntaxBaum
+	var err error
+	if 0 <= index && index < tree.Valence {
+		subtree = *(tree.Children[index])
+	} else {
+		err = errors.New(fmt.Sprintf("Instance has no child of index %d !", index))
+	}
+	return subtree, err
+}
+
+func (tree SyntaxBaum) Pretty(preindentOpt ...string) string {
+	var preindent string = ""
+	if len(preindentOpt) > 0 {
+		preindent = preindentOpt[0]
+	}
+	return tree.pretty(preindent, "  ", "", 0)
+}
+
+func (tree SyntaxBaum) pretty(preindent string, tab string, prepend string, depth int) string {
+	var indent string = preindent + strings.Repeat(tab, depth)
+	switch tree.Valence {
+	case 0:
+		switch kind := tree.Kind; kind {
+		case "atom", "generic":
+			return indent + prepend + kind + " " + tree.Expr
+		default:
+			return indent + prepend + kind
+		}
+	default:
+		var lines string = indent + prepend + tree.Kind
+		prepend = "|__ "
+		for _, subtree := range tree.Children {
+			lines += "\n" + subtree.pretty(preindent, tab, prepend, depth+1)
+		}
+		return lines
+	}
+}
+
+// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// METHODS: Recognitong of Formula-Types
+// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+func (tree SyntaxBaum) isAtom() bool {
+	return tree.Kind == "atom"
+}
+
+func (tree SyntaxBaum) isLiteral() bool {
+	if tree.isAtom() {
+		return true
+	} else if tree.isNegation() {
+		subtree, err := tree.GetChild()
+		if err == nil {
+			return subtree.isAtom()
+		}
+	}
+	return false
+}
+
+func (tree SyntaxBaum) isBeliebig() bool {
+	return tree.Kind == "generic"
+}
+
+func (tree SyntaxBaum) isTrueSymbol() bool {
+	return tree.Kind == "taut"
+}
+
+func (tree SyntaxBaum) isFalseSymbol() bool {
+	return tree.Kind == "contradiction"
+}
+
+func (tree SyntaxBaum) isNegation() bool {
+	return tree.Kind == "not"
+}
+
+func (tree SyntaxBaum) isConjunction() bool {
+	return tree.Kind == "and2"
+}
+
+func (tree SyntaxBaum) isLongConjunction() bool {
+	switch tree.Kind {
+	case "and", "and2":
+		return true
+	default:
+		return false
+	}
+}
+
+func (tree SyntaxBaum) isDisjunction() bool {
+	return tree.Kind == "or2"
+}
+
+func (tree SyntaxBaum) isLongDisjunction() bool {
+	switch tree.Kind {
+	case "or", "or2":
+		return true
+	default:
+		return false
+	}
+}
+
+func (tree SyntaxBaum) isImplication() bool {
+	return tree.Kind == "implies"
+}