master > master: codego - test nicht mehr wegen generics überspringen

codego/aussagenlogik/formulae/formulae_advanced.go

@@ -0,0 +1,23 @@
+package formulae
+
+/* ---------------------------------------------------------------- *
+ * METHOD Get Atoms
+ * ---------------------------------------------------------------- */
+
+func schemeGetAtoms(fml Formula, prevValues [](*[]Formula)) *[]Formula {
+	if fml.IsAtom() {
+		return &[]Formula{fml.Copy()}
+	} else {
+		var results = []Formula{}
+		for _, prevValue := range prevValues {
+			results = append(results, *prevValue...)
+		}
+		return &results
+	}
+}
+
+var fnGetAtoms = CreateFromSchemeFmlsValued(schemeGetAtoms)
+
+func (fml Formula) GetAtoms() []Formula {
+	return *fnGetAtoms(fml)
+}

codego/aussagenlogik/formulae/formulae_basic.go

@@ -11,6 +11,7 @@ import (
 
 type Formula struct {
 	kind        string
+	name        string
 	expr        string
 	valence     int
 	subformulae [](*Formula)
@@ -28,18 +29,38 @@ func (fml *Formula) SetExpr(expr string) { fml.expr = expr }
 
 func (fml Formula) GetExpr() string { return fml.expr }
 
-func (fml *Formula) SetSubformulae(children [](*Formula)) {
+func (fml Formula) GetName() string { return fml.name }
-	fml.subformulae = children
+
-	fml.valence = len(children)
+func (fml *Formula) SetSubformulae(subfmls [](*Formula)) {
+	fml.subformulae = subfmls
+	fml.valence = len(subfmls)
 }
 
 func (fml Formula) GetSubFormulae() []Formula {
 	var n int = fml.valence
-	var children = make([]Formula, n)
+	var subfmls = make([]Formula, n)
 	for i, subfml := range fml.subformulae {
-		children[i] = *subfml
+		subfmls[i] = *subfml
 	}
-	return children
+	return subfmls
+}
+
+func (fml Formula) GetAllSubFormulae() []Formula {
+	var subfml = fml.GetSubFormulae()
+	var result = []Formula{fml.Copy()}
+	for _, child := range subfml {
+		result = append(result, child.GetAllSubFormulae()...)
+	}
+	return result
+}
+
+func (fml Formula) GetAllSubFormulaeStrict() []Formula {
+	var subfml = fml.GetSubFormulae()
+	var result = []Formula{}
+	for _, child := range subfml {
+		result = append(result, child.GetAllSubFormulae()...)
+	}
+	return result
 }
 
 func (fml Formula) GetChild(indexOpt ...int) Formula {
@@ -84,17 +105,27 @@ func (fml Formula) pretty(preindent string, tab string, prepend string, depth in
 	}
 }
 
+// shallow copy
+func (fml Formula) Copy() Formula {
+	return Formula{
+		expr:        fml.expr,
+		kind:        fml.kind,
+		valence:     fml.valence,
+		subformulae: fml.subformulae,
+	}
+}
+
 func (fml Formula) Deepcopy() Formula {
-	var children = make([](*Formula), len(fml.subformulae))
+	var subfmls = make([](*Formula), len(fml.subformulae))
-	for i, child := range fml.subformulae {
+	for i, subfml := range fml.subformulae {
-		childCopy := child.Deepcopy()
+		subfmlCopy := subfml.Deepcopy()
-		children[i] = &childCopy
+		subfmls[i] = &subfmlCopy
 	}
 	return Formula{
 		expr:        fml.expr,
 		kind:        fml.kind,
 		valence:     fml.valence,
-		subformulae: children,
+		subformulae: subfmls,
 	}
 }
 
@@ -117,3 +148,4 @@ func (fml Formula) IsConjunction() bool         { return fml.kind == "and" || fm
 func (fml Formula) IsDisjunction2() bool        { return fml.kind == "or2" }
 func (fml Formula) IsDisjunction() bool         { return fml.kind == "or" || fml.kind == "or2" }
 func (fml Formula) IsImplication() bool         { return fml.kind == "implies" }
+func (fml Formula) IsDoubleImplication() bool   { return fml.kind == "iff" }

codego/aussagenlogik/formulae/formulae_construction.go

@@ -22,23 +22,25 @@ var Contradiction = Formula{
  * METHODS: Constructions
  * ---------------------------------------------------------------- */
 
-func Atom(expr string) Formula {
+func Atom(name string) Formula {
 	return Formula{
 		kind:        "atom",
-		expr:        expr,
+		name:        name,
+		expr:        name,
 		valence:     0,
 		subformulae: [](*Formula){},
 	}
 }
 
-func NegatedAtom(expr string) Formula {
+func NegatedAtom(name string) Formula {
-	return Negation(Atom(expr))
+	return Negation(Atom(name))
 }
 
-func Generic(expr string) Formula {
+func Generic(name string) Formula {
 	return Formula{
 		kind:        "generic",
-		expr:        expr,
+		name:        name,
+		expr:        "{" + name + "}",
 		valence:     0,
 		subformulae: [](*Formula){},
 	}
@@ -115,3 +117,12 @@ func Implies(fml1 Formula, fml2 Formula) Formula {
 		subformulae: [](*Formula){&fml1, &fml2},
 	}
 }
+
+func DoubleImplication(fml1 Formula, fml2 Formula) Formula {
+	return Formula{
+		kind:        "iff",
+		expr:        "(" + fml1.expr + " <-> " + fml2.expr + ")",
+		valence:     2,
+		subformulae: [](*Formula){&fml1, &fml2},
+	}
+}

codego/aussagenlogik/recursion/recursion_eval.go

@@ -14,7 +14,7 @@ func Eval(fml formulae.Formula, I []string) int {
 	var schema = func(_I []string) func(formulae.Formula, []int) int {
 		return func(fml formulae.Formula, prevValues []int) int {
 			if fml.IsAtom() || fml.IsGeneric() {
-				return utils.BoolToInt(utils.StrListContains(_I, fml.GetExpr()))
+				return utils.BoolToInt(utils.StrListContains(_I, fml.GetName()))
 			} else if fml.IsTautologySymbol() {
 				return 1
 			} else if fml.IsContradictionSymbol() {
@@ -31,6 +31,8 @@ func Eval(fml formulae.Formula, I []string) int {
 				return utils.MaxList(prevValues)
 			} else if fml.IsImplication() {
 				return utils.BoolToInt(prevValues[0] <= prevValues[1])
+			} else if fml.IsDoubleImplication() {
+				return utils.BoolToInt(prevValues[0] == prevValues[1])
 			} else {
 				panic("Could not evaluate expression!")
 			}

codego/aussagenlogik/recursion/recursion_nnf.go

@@ -64,9 +64,20 @@ func NNF(fml formulae.Formula) formulae.Formula {
 			}
 		} else if fml.IsImplication() {
 			return formulae.FormulaPair{
-				Pos: formulae.Implies(prevPos[0], prevPos[1]),
+				Pos: formulae.Disjunction2(prevNeg[0], prevPos[1]),
 				Neg: formulae.Conjunction2(prevPos[0], prevNeg[1]),
 			}
+		} else if fml.IsDoubleImplication() {
+			return formulae.FormulaPair{
+				Pos: formulae.Conjunction2(
+					formulae.Disjunction2(prevNeg[0], prevPos[1]),
+					formulae.Disjunction2(prevNeg[1], prevPos[0]),
+				),
+				Neg: formulae.Disjunction2(
+					formulae.Conjunction2(prevPos[0], prevNeg[1]),
+					formulae.Conjunction2(prevPos[1], prevNeg[0]),
+				),
+			}
 		} else {
 			panic("Could not evaluate expression!")
 		}

codego/aussagenlogik/recursion/recursion_test.go

@@ -23,25 +23,124 @@ func TestEvalLiteral(test *testing.T) {
 	var val int
 	var fml formulae.Formula
 	var I []string
+
 	fml = schema.ParseExpr("A0")
 	I = []string{"A0"}
 	val = recursion.Eval(fml, I)
 	assert.Equal(1, val)
+
 	fml = schema.ParseExpr("A0")
 	I = []string{}
 	val = recursion.Eval(fml, I)
 	assert.Equal(0, val)
+
 	fml = schema.ParseExpr("! A0")
 	I = []string{"A0"}
 	val = recursion.Eval(fml, I)
 	assert.Equal(0, val)
+
 	fml = schema.ParseExpr("! A0")
 	I = []string{}
 	val = recursion.Eval(fml, I)
 	assert.Equal(1, val)
 }
 
-func TestEvalComplex1(test *testing.T) {
+func TestEvalNegation(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A4 || ! A4")
+	I = []string{}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	fml = schema.ParseExpr("A4 && ! A4")
+	I = []string{}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+}
+
+func TestEvalConjunction(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A0 && A1")
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+
+	fml = schema.ParseExpr("A0 && A1")
+	I = []string{"A0", "A1"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+}
+
+func TestEvalDisjunction(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A0 || A1")
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	fml = schema.ParseExpr("A0 || A1")
+	I = []string{"A7"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+}
+
+func TestEvalImplication(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A0 -> A1")
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+
+	fml = schema.ParseExpr("A0 -> A1")
+	I = []string{"A0", "A1"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	fml = schema.ParseExpr("A0 -> A1")
+	I = []string{"A7"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+}
+
+func TestEvalIff(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A0 <-> A1")
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+
+	fml = schema.ParseExpr("A0 <-> A1")
+	I = []string{"A0", "A1"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	fml = schema.ParseExpr("A0 <-> A1")
+	I = []string{"A7"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+}
+
+func TestEvalComplex(test *testing.T) {
 	var assert = assert.New(test)
 	var val int
 	var fml formulae.Formula
@@ -50,26 +149,24 @@ func TestEvalComplex1(test *testing.T) {
 	I = []string{"A0", "A2"}
 	val = recursion.Eval(fml, I)
 	assert.Equal(1, val)
+
 	I = []string{"A0", "A3"}
 	val = recursion.Eval(fml, I)
 	assert.Equal(1, val)
+
 	I = []string{"A0"}
 	val = recursion.Eval(fml, I)
 	assert.Equal(0, val)
+
 	I = []string{"A4", "A8"}
 	val = recursion.Eval(fml, I)
 	assert.Equal(1, val)
-}
 
-func TestEvalComplex2(test *testing.T) {
-	var assert = assert.New(test)
-	var val int
-	var fml formulae.Formula
-	var I []string
 	fml = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || ! A2 ))")
 	I = []string{"A0", "A2"}
 	val = recursion.Eval(fml, I)
 	assert.Equal(0, val)
+
 	I = []string{"A0", "A3"}
 	val = recursion.Eval(fml, I)
 	assert.Equal(1, val)
@@ -90,9 +187,8 @@ func TestAtomsNoduplicates(test *testing.T) {
 	assert.Equal(1, n, "Atome dürfen nicht mehrfach vorkommen!")
 }
 
-func TestAtomsNononatoms(test *testing.T) {
+func TestAtomsNoNonAtoms(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 fml formulae.Formula
 	var val []string
@@ -298,12 +394,14 @@ func TestNNFatoms(test *testing.T) {
 	nnf_expected = formulae.Atom("A7")
 	fml = schema.ParseExpr("A7")
 	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+
 	fml = schema.ParseExpr("!! A7")
 	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
 
 	nnf_expected = formulae.NegatedAtom("A7")
 	fml = schema.ParseExpr("! A7")
 	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+
 	fml = schema.ParseExpr("!!! A7")
 	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
 }

codego/aussagenlogik/schema/schema.go

@@ -3,6 +3,7 @@ package schema
 import (
 	"logik/aussagenlogik/formulae"
 	parser "logik/grammars/aussagenlogik"
+	"regexp"
 
 	"github.com/antlr/antlr4/runtime/Go/antlr"
 )
@@ -65,23 +66,14 @@ func (ant antlrTree) getLabel() string {
 }
 
 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()
+		return ant.getLabel()
-	} else {
+	}
 	for _, subant := range subants {
 		expr += subant.getTextContent()
 	}
-	}
 	return expr
 }
 
@@ -116,9 +108,12 @@ func (ant antlrTree) toFormula() formulae.Formula {
 	case "contradiction":
 		return formulae.Contradiction
 	case "atom":
-		return formulae.Atom(ant.getTextContentLeaves())
+		name := ant.getTextContent()
+		return formulae.Atom(name)
 	case "generic":
-		return formulae.Generic(ant.getTextContentLeaves())
+		re := regexp.MustCompile(`^{|}$`)
+		name := string(re.ReplaceAll([]byte(ant.getTextContent()), []byte("")))
+		return formulae.Generic(name)
 	case "not":
 		// NOTE: expr = ! expr
 		if nChildren == 2 {
@@ -139,6 +134,11 @@ func (ant antlrTree) toFormula() formulae.Formula {
 		if nChildren == 3 {
 			return formulae.Implies(subants[0].toFormula(), subants[2].toFormula())
 		}
+	case "iff":
+		// NOTE: expr = expr <=> expr
+		if nChildren == 3 {
+			return formulae.DoubleImplication(subants[0].toFormula(), subants[2].toFormula())
+		}
 	case "and", "or":
 		// NOTE: expr = expr op expr op ... op expr
 		var n int = int((len(subants) + 1) / 2)

codego/grammars/aussagenlogik.g4

@@ -7,27 +7,29 @@ LBRACE: '(';
 RBRACE: ')';
 LCURLYBRACE: '{';
 RCURLYBRACE: '}';
+TEXT: [a-zA-Z0-9\\_];
 
 // Symbole (erlaube mehrere Varianten)
 SYMB_NOT:  ('!'|'~'|'not');
 SYMB_AND:  ('&'+|'^'|'and');
 SYMB_OR:   ('|'+|'v'|'or');
-SYMB_IMPL: ('->'|'=>');
+SYMB_IFF:  ([<][-]+[>]|[<][=]+[>]|'iff');
+SYMB_IMPL: (~[<][-]+[>]|~[<][=]+[>]);
 
 // Rules
 start: open <EOF> | closed <EOF>;
 
 closed: atomic | not | LBRACE open RBRACE;
-open: and2 | and | or2 | or | implies;
+open: and2 | and | or2 | or | implies | iff;
 
 // Schemata für atomische Ausdrücke
-atomic: taut | contradiction | atom; //| generic;
+atomic: taut | contradiction | atom | generic;
 taut:  ('1'|'true');
 contradiction: ('0'|'false');
 atom: 'A0' | 'A1' | 'A' NUMBER; // muss A0, A1 wegen falsum/verum extra auflisten
-// // als 'generische' Formeln schreibe bspw. {F}, {G}, {F1}, usw.
+// als 'generische' Formeln schreibe bspw. {F}, {G}, usw.
-// // generic: LCURLYBRACE (.*?) RCURLYBRACE;
+generic: LCURLYBRACE TEXT+ RCURLYBRACE | LCURLYBRACE TEXT* ( generic TEXT* )+ RCURLYBRACE;
-// FIXME: dieses Schema führt zu Konflikten
+// FIXME: liest Zahlen schlecht ein
 
 // Schema für Negation: ¬ F
 not:                symb=SYMB_NOT  closed;
@@ -39,3 +41,5 @@ or2:       closed   symb=SYMB_OR   closed;
 or:      ( closed ( symb=SYMB_OR   closed )+ );
 // Schema für Implikation: F1 ⟶ F2
 implies:   closed   symb=SYMB_IMPL closed;
+// Schema für Implikation: F1 ⟷ F2
+iff:       closed   symb=SYMB_IFF  closed;

codego/scripts/test.sh

@@ -16,7 +16,6 @@ function call_go() {
 }
 
 function check_requirements() {
-    [ -f "go.sum" ] && rm "go.sum";
     call_go get "$( cat scripts/requirements )";
 }