master > master: codego - utils + unit tests, A1[0-9]+ mit testen

codego/aussagenlogik/formulae/formulae_advanced.go

@@ -1,5 +1,7 @@
 package formulae
 
+import "logik/core/utils"
+
 /* ---------------------------------------------------------------- *
  * METHOD Get Atoms
  * ---------------------------------------------------------------- */
@@ -21,3 +23,156 @@ var fnGetAtoms = CreateFromSchemeFmlsValued(schemeGetAtoms)
 func (fml Formula) GetAtoms() []Formula {
 	return *fnGetAtoms(fml)
 }
+
+/* ---------------------------------------------------------------- *
+ * TYPE FormulaPair, FormulaPairs
+ * ---------------------------------------------------------------- */
+
+type FormulaPair struct {
+	Pos Formula
+	Neg Formula
+}
+
+type FormulaPairs []FormulaPair
+
+/* ---------------------------------------------------------------- *
+ * Methods for FormulaPairs
+ * ---------------------------------------------------------------- */
+
+func NewFormulaPairs(pairs []FormulaPair) FormulaPairs { return pairs }
+
+func (pairs FormulaPairs) Pos() []Formula {
+	var fmls = make([]Formula, len(pairs))
+	for i, pair := range pairs {
+		fmls[i] = pair.Pos
+	}
+	return fmls
+}
+
+func (pairs FormulaPairs) Neg() []Formula {
+	var fmls = make([]Formula, len(pairs))
+	for i, pair := range pairs {
+		fmls[i] = pair.Neg
+	}
+	return fmls
+}
+
+/* ---------------------------------------------------------------- *
+ * TYPE KNF, DNF, Horn
+ * ---------------------------------------------------------------- */
+
+type FormulaConjunct []Formula
+type FormulaDisjunct []Formula
+type FormulaKNF []FormulaDisjunct
+type FormulaDNF []FormulaConjunct
+type FormulaHornClause struct {
+	Pos FormulaDisjunct
+	Neg FormulaConjunct
+}
+type FormulaHorn []FormulaHornClause
+
+/* ---------------------------------------------------------------- *
+ * Methods for KNF, DNF, Horn
+ * ---------------------------------------------------------------- */
+
+func (fml FormulaDisjunct) ToFormula() Formula {
+	return Disjunction(fml)
+}
+
+func (fml FormulaConjunct) ToFormula() Formula {
+	return Conjunction(fml)
+}
+
+func (fml FormulaKNF) ToFormula() Formula {
+	var termsAsFormulae = make([]Formula, len(fml))
+	for i, term := range fml {
+		termsAsFormulae[i] = term.ToFormula()
+	}
+	return Conjunction(termsAsFormulae)
+}
+
+func (fml FormulaDNF) ToFormula() Formula {
+	var termsAsFormulae = make([]Formula, len(fml))
+	for i, term := range fml {
+		termsAsFormulae[i] = term.ToFormula()
+	}
+	return Disjunction(termsAsFormulae)
+}
+
+func (fml FormulaHornClause) ToFormula() Formula {
+	return Implies(fml.Neg.ToFormula(), fml.Pos.ToFormula())
+}
+
+func (fml FormulaHorn) ToFormula() Formula {
+	var hornclausesAsFormulae = make([]Formula, len(fml))
+	for i, hornclause := range fml {
+		hornclausesAsFormulae[i] = hornclause.ToFormula()
+	}
+	return Conjunction(hornclausesAsFormulae)
+}
+
+func getAtomsFromArrayOfLiterals(fmls []Formula) []string {
+	var atoms = []string{}
+	var m = map[string]bool{}
+	for _, fml := range fmls {
+		if fml.IsLiteral() {
+			m[fml.GetName()] = true
+		}
+	}
+	for name, _ := range m {
+		atoms = append(atoms, name)
+	}
+	utils.SortStrings(&atoms)
+	return atoms
+}
+
+func getAtomsFromArrayOfArraysOfLiterals(fmlArrays [][]Formula) []string {
+	var atoms = []string{}
+	var m = map[string]bool{}
+	for _, fmls := range fmlArrays {
+		for _, atom := range getAtomsFromArrayOfLiterals(fmls) {
+			m[atom] = true
+		}
+	}
+	for name, _ := range m {
+		atoms = append(atoms, name)
+	}
+	utils.SortStrings(&atoms)
+	return atoms
+}
+
+func (fml FormulaConjunct) GetAtoms() []string {
+	return getAtomsFromArrayOfLiterals(fml)
+}
+
+func (fml FormulaDisjunct) GetAtoms() []string {
+	return getAtomsFromArrayOfLiterals(fml)
+}
+
+func (fml FormulaHornClause) GetAtoms() []string {
+	return getAtomsFromArrayOfArraysOfLiterals([][]Formula{fml.Pos, fml.Neg})
+}
+
+func (fml FormulaKNF) GetAtoms() []string {
+	var fmlArrays = make([][]Formula, len(fml))
+	for i, term := range fml {
+		fmlArrays[i] = term
+	}
+	return getAtomsFromArrayOfArraysOfLiterals(fmlArrays)
+}
+
+func (fml FormulaDNF) GetAtoms() []string {
+	var fmlArrays = make([][]Formula, len(fml))
+	for i, term := range fml {
+		fmlArrays[i] = term
+	}
+	return getAtomsFromArrayOfArraysOfLiterals(fmlArrays)
+}
+
+func (fml FormulaHorn) GetAtoms() []string {
+	var fmlArrays = make([][]Formula, 2*len(fml))
+	for i, hornclause := range fml {
+		fmlArrays[i] = append(hornclause.Neg, hornclause.Pos...)
+	}
+	return getAtomsFromArrayOfArraysOfLiterals(fmlArrays)
+}

codego/aussagenlogik/formulae/formulae_basic.go

@@ -31,33 +31,33 @@ func (fml Formula) GetExpr() string { return fml.expr }
 
 func (fml Formula) GetName() string { return fml.name }
 
-func (fml *Formula) SetSubformulae(subfmls [](*Formula)) {
+func (fml *Formula) SetSubformulae(subFmls [](*Formula)) {
-	fml.subformulae = subfmls
+	fml.subformulae = subFmls
-	fml.valence = len(subfmls)
+	fml.valence = len(subFmls)
 }
 
 func (fml Formula) GetSubFormulae() []Formula {
 	var n int = fml.valence
-	var subfmls = make([]Formula, n)
+	var subFmls = make([]Formula, n)
-	for i, subfml := range fml.subformulae {
+	for i, subFml := range fml.subformulae {
-		subfmls[i] = *subfml
+		subFmls[i] = *subFml
 	}
-	return subfmls
+	return subFmls
 }
 
 func (fml Formula) GetAllSubFormulae() []Formula {
-	var subfml = fml.GetSubFormulae()
+	var subFml = fml.GetSubFormulae()
 	var result = []Formula{fml.Copy()}
-	for _, child := range subfml {
+	for _, child := range subFml {
 		result = append(result, child.GetAllSubFormulae()...)
 	}
 	return result
 }
 
 func (fml Formula) GetAllSubFormulaeStrict() []Formula {
-	var subfml = fml.GetSubFormulae()
+	var subFml = fml.GetSubFormulae()
 	var result = []Formula{}
-	for _, child := range subfml {
+	for _, child := range subFml {
 		result = append(result, child.GetAllSubFormulae()...)
 	}
 	return result
@@ -68,13 +68,13 @@ func (fml Formula) GetChild(indexOpt ...int) Formula {
 	if len(indexOpt) > 0 {
 		index = indexOpt[0]
 	}
-	var subfml Formula
+	var subFml Formula
 	if 0 <= index && index < fml.valence {
-		subfml = *(fml.subformulae[index])
+		subFml = *(fml.subformulae[index])
 	} else {
 		panic(fmt.Sprintf("Instance has no child of index %d !", index))
 	}
-	return subfml
+	return subFml
 }
 
 func (fml Formula) Pretty(preindentOpt ...string) string {
@@ -98,8 +98,8 @@ func (fml Formula) pretty(preindent string, tab string, prepend string, depth in
 	default:
 		var lines string = indent + prepend + fml.kind
 		prepend = "|__ "
-		for _, subfml := range fml.subformulae {
+		for _, subFml := range fml.subformulae {
-			lines += "\n" + subfml.pretty(preindent, tab, prepend, depth+1)
+			lines += "\n" + subFml.pretty(preindent, tab, prepend, depth+1)
 		}
 		return lines
 	}
@@ -116,16 +116,16 @@ func (fml Formula) Copy() Formula {
 }
 
 func (fml Formula) Deepcopy() Formula {
-	var subfmls = make([](*Formula), len(fml.subformulae))
+	var subFmls = make([](*Formula), len(fml.subformulae))
-	for i, subfml := range fml.subformulae {
+	for i, subFml := range fml.subformulae {
-		subfmlCopy := subfml.Deepcopy()
+		subFmlCopy := subFml.Deepcopy()
-		subfmls[i] = &subfmlCopy
+		subFmls[i] = &subFmlCopy
 	}
 	return Formula{
 		expr:        fml.expr,
 		kind:        fml.kind,
 		valence:     fml.valence,
-		subformulae: subfmls,
+		subformulae: subFmls,
 	}
 }
 

codego/aussagenlogik/formulae/formulae_construction.go

@@ -47,9 +47,16 @@ func Generic(name string) Formula {
 }
 
 func Negation(fml Formula) Formula {
+	var name string
+	if fml.IsAtom() {
+		name = fml.GetName()
+	}
+	var expr = fml.expr
+	expr = "!" + expr
 	return Formula{
 		kind:        "not",
-		expr:        "!" + " " + fml.expr,
+		name:        name, // preserves name of negated atoms
+		expr:        expr,
 		valence:     1,
 		subformulae: [](*Formula){&fml},
 	}
@@ -65,20 +72,26 @@ func Conjunction2(fml1 Formula, fml2 Formula) Formula {
 }
 
 func Conjunction(fmls []Formula) Formula {
+	switch len(fmls) {
+	case 0:
+		return Tautology
+	case 1:
+		return fmls[0]
+	}
 	var expr string = ""
-	var children = make([](*Formula), len(fmls))
+	var subFmls = make([](*Formula), len(fmls))
 	for i, fml := range fmls {
+		(func(i int, subFml Formula) { subFmls[i] = &subFml })(i, fml)
 		if i > 0 {
 			expr += " && "
 		}
 		expr += fml.expr
-		children[i] = &fml
 	}
 	return Formula{
 		kind:        "and",
 		expr:        "(" + expr + ")",
-		valence:     len(children),
+		valence:     len(subFmls),
-		subformulae: children,
+		subformulae: subFmls,
 	}
 }
 
@@ -92,20 +105,26 @@ func Disjunction2(fml1 Formula, fml2 Formula) Formula {
 }
 
 func Disjunction(fmls []Formula) Formula {
+	switch len(fmls) {
+	case 0:
+		return Contradiction
+	case 1:
+		return fmls[0]
+	}
 	var expr string = ""
-	var children = make([](*Formula), len(fmls))
+	var subFmls = make([](*Formula), len(fmls))
 	for i, fml := range fmls {
+		(func(i int, subFml Formula) { subFmls[i] = &subFml })(i, fml)
 		if i > 0 {
 			expr += " || "
 		}
 		expr += fml.expr
-		children[i] = &fml
 	}
 	return Formula{
 		kind:        "or",
 		expr:        "(" + expr + ")",
-		valence:     len(children),
+		valence:     len(subFmls),
-		subformulae: children,
+		subformulae: subFmls,
 	}
 }
 

codego/aussagenlogik/formulae/formulae_generate.go

@@ -8,16 +8,16 @@ package formulae
 
 func CreateFromSchemeIntValued(scheme func(fml Formula, prevValues []int) int) func(fml Formula) int {
 	var fn func(fml Formula) int
-	var subFn = func(ch chan int, subfml Formula) { ch <- fn(subfml) }
+	var subFn = func(ch chan int, subFml Formula) { ch <- fn(subFml) }
 	fn = func(fml Formula) int {
-		var subfmls = fml.GetSubFormulae()
+		var subFmls = fml.GetSubFormulae()
-		var n = len(subfmls)
+		var n = len(subFmls)
 		var subChan = make([](chan int), n)
-		var prevValues = make([]int, len(subfmls))
+		var prevValues = make([]int, len(subFmls))
 		// start parallel computations on subformulas
-		for i, subfml := range subfmls {
+		for i, subFml := range subFmls {
 			subChan[i] = make(chan int) // create Channel, since currently nil
-			go subFn(subChan[i], subfml)
+			go subFn(subChan[i], subFml)
 		}
 		// successively read values
 		for i := 0; i < n; i++ {
@@ -35,16 +35,16 @@ func CreateFromSchemeIntValued(scheme func(fml Formula, prevValues []int) int) f
 
 func CreateFromSchemeStringValued(scheme func(fml Formula, prevValues []string) string) func(fml Formula) string {
 	var fn func(fml Formula) string
-	var subFn = func(ch chan string, subfml Formula) { ch <- fn(subfml) }
+	var subFn = func(ch chan string, subFml Formula) { ch <- fn(subFml) }
 	fn = func(fml Formula) string {
-		var subfmls = fml.GetSubFormulae()
+		var subFmls = fml.GetSubFormulae()
-		var n = len(subfmls)
+		var n = len(subFmls)
 		var subChan = make([](chan string), n)
-		var prevValues = make([]string, len(subfmls))
+		var prevValues = make([]string, len(subFmls))
 		// start parallel computations on subformulas
-		for i, subfml := range subfmls {
+		for i, subFml := range subFmls {
 			subChan[i] = make(chan string) // create Channel, since currently nil
-			go subFn(subChan[i], subfml)
+			go subFn(subChan[i], subFml)
 		}
 		// successively read values
 		for i := 0; i < n; i++ {
@@ -62,16 +62,16 @@ func CreateFromSchemeStringValued(scheme func(fml Formula, prevValues []string)
 
 func CreateFromSchemeStringsValued(scheme func(fml Formula, prevValues [][]string) []string) func(fml Formula) []string {
 	var fn func(fml Formula) []string
-	var subFn = func(ch chan []string, subfml Formula) { ch <- fn(subfml) }
+	var subFn = func(ch chan []string, subFml Formula) { ch <- fn(subFml) }
 	fn = func(fml Formula) []string {
-		var subfmls = fml.GetSubFormulae()
+		var subFmls = fml.GetSubFormulae()
-		var n = len(subfmls)
+		var n = len(subFmls)
 		var subChan = make([](chan []string), n)
-		var prevValues = make([][]string, len(subfmls))
+		var prevValues = make([][]string, len(subFmls))
 		// start parallel computations on subformulas
-		for i, subfml := range subfmls {
+		for i, subFml := range subFmls {
 			subChan[i] = make(chan []string) // create Channel, since currently nil
-			go subFn(subChan[i], subfml)
+			go subFn(subChan[i], subFml)
 		}
 		// successively read values
 		for i := 0; i < n; i++ {
@@ -89,16 +89,16 @@ func CreateFromSchemeStringsValued(scheme func(fml Formula, prevValues [][]strin
 
 func CreateFromSchemeFmlValued(scheme func(fml Formula, prevValues []Formula) Formula) func(fml Formula) Formula {
 	var fn func(fml Formula) Formula
-	var subFn = func(ch chan Formula, subfml Formula) { ch <- fn(subfml) }
+	var subFn = func(ch chan Formula, subFml Formula) { ch <- fn(subFml) }
 	fn = func(fml Formula) Formula {
-		var subfmls = fml.GetSubFormulae()
+		var subFmls = fml.GetSubFormulae()
-		var n = len(subfmls)
+		var n = len(subFmls)
 		var subChan = make([](chan Formula), n)
-		var prevValues = make([]Formula, len(subfmls))
+		var prevValues = make([]Formula, len(subFmls))
 		// start parallel computations on subformulas
-		for i, subfml := range subfmls {
+		for i, subFml := range subFmls {
 			subChan[i] = make(chan Formula) // create Channel, since currently nil
-			go subFn(subChan[i], subfml)
+			go subFn(subChan[i], subFml)
 		}
 		// successively read values
 		for i := 0; i < n; i++ {
@@ -116,16 +116,16 @@ func CreateFromSchemeFmlValued(scheme func(fml Formula, prevValues []Formula) Fo
 
 func CreateFromSchemeFmlsValued(scheme func(fml Formula, prevValues [](*[]Formula)) *[]Formula) func(fml Formula) *[]Formula {
 	var fn func(fml Formula) *[]Formula
-	var subFn = func(ch chan *[]Formula, subfml Formula) { ch <- fn(subfml) }
+	var subFn = func(ch chan *[]Formula, subFml Formula) { ch <- fn(subFml) }
 	fn = func(fml Formula) *[]Formula {
-		var subfmls = fml.GetSubFormulae()
+		var subFmls = fml.GetSubFormulae()
-		var n = len(subfmls)
+		var n = len(subFmls)
 		var subChan = make([](chan *[]Formula), n)
-		var prevValues = make([](*[]Formula), len(subfmls))
+		var prevValues = make([](*[]Formula), len(subFmls))
 		// start parallel computations on subformulas
-		for i, subfml := range subfmls {
+		for i, subFml := range subFmls {
 			subChan[i] = make(chan *[]Formula) // create Channel, since currently nil
-			go subFn(subChan[i], subfml)
+			go subFn(subChan[i], subFml)
 		}
 		// successively read values
 		for i := 0; i < n; i++ {
@@ -143,16 +143,16 @@ func CreateFromSchemeFmlsValued(scheme func(fml Formula, prevValues [](*[]Formul
 
 func CreateFromSchemeFmlPairValued(scheme func(fml Formula, prevValues []FormulaPair) FormulaPair) func(fml Formula) FormulaPair {
 	var fn func(fml Formula) FormulaPair
-	var subFn = func(ch chan FormulaPair, subfml Formula) { ch <- fn(subfml) }
+	var subFn = func(ch chan FormulaPair, subFml Formula) { ch <- fn(subFml) }
 	fn = func(fml Formula) FormulaPair {
-		var subfmls = fml.GetSubFormulae()
+		var subFmls = fml.GetSubFormulae()
-		var n = len(subfmls)
+		var n = len(subFmls)
 		var subChan = make([](chan FormulaPair), n)
-		var prevValues = make([]FormulaPair, len(subfmls))
+		var prevValues = make([]FormulaPair, len(subFmls))
 		// start parallel computations on subformulas
-		for i, subfml := range subfmls {
+		for i, subFml := range subFmls {
 			subChan[i] = make(chan FormulaPair) // create Channel, since currently nil
-			go subFn(subChan[i], subfml)
+			go subFn(subChan[i], subFml)
 		}
 		// successively read values
 		for i := 0; i < n; i++ {

codego/aussagenlogik/formulae/formulae_normalforms.go

@@ -0,0 +1,151 @@
+package formulae
+
+/* ---------------------------------------------------------------- *
+ * METHODS: get KNF/DNF
+ * ---------------------------------------------------------------- */
+
+func (fml Formula) GetKNFparts() FormulaKNF {
+	var subFmls []Formula
+	if fml.IsDisjunctOfLiterals() {
+		subFmls = []Formula{fml}
+	} else if fml.IsKNF() {
+		subFmls = fml.GetSubFormulae()
+	} else {
+		panic("Formula not in KNF!")
+	}
+	var terms = make([]FormulaDisjunct, len(subFmls))
+	for i, subFml := range subFmls {
+		if subFml.IsLiteral() {
+			terms[i] = []Formula{subFml}
+		} else {
+			terms[i] = subFml.GetSubFormulae()
+		}
+	}
+	return terms
+}
+
+func (fml Formula) GetDNFparts() FormulaDNF {
+	var subFmls []Formula
+	if fml.IsDisjunctOfLiterals() {
+		subFmls = []Formula{fml}
+	} else if fml.IsKNF() {
+		subFmls = fml.GetSubFormulae()
+	} else {
+		panic("Formula not in DNF!")
+	}
+	var terms = make([]FormulaConjunct, len(subFmls))
+	for i, subFml := range subFmls {
+		if subFml.IsLiteral() {
+			terms[i] = []Formula{subFml}
+		} else {
+			terms[i] = subFml.GetSubFormulae()
+		}
+	}
+	return terms
+}
+
+func (fml Formula) GetHornParts() FormulaHorn {
+	var subFmls []Formula
+	if fml.IsHornClause() {
+		subFmls = []Formula{fml}
+	} else if fml.IsHornFml() {
+		subFmls = fml.GetSubFormulae()
+	} else {
+		panic("Formula not a Horn-Formula!")
+	}
+	var parts = make([]FormulaHornClause, len(subFmls))
+	for i, subFml := range subFmls {
+		Pos := []Formula{}
+		Neg := []Formula{}
+		var subSubFml []Formula
+		if subFml.IsLiteral() {
+			subSubFml = []Formula{subFml}
+		} else {
+			subSubFml = subFml.GetSubFormulae()
+		}
+		for _, L := range subSubFml {
+			if L.IsPositiveLiteral() {
+				Pos = append(Pos, L)
+			} else {
+				Neg = append(Neg, L.GetChild())
+			}
+		}
+		parts[i] = FormulaHornClause{Pos, Neg}
+	}
+	return parts
+}
+
+/* ---------------------------------------------------------------- *
+ * METHODS: check if KNF/DNF
+ * ---------------------------------------------------------------- */
+
+func onlyLiterals(fmls []Formula) bool {
+	for _, fml := range fmls {
+		if !fml.IsLiteral() {
+			return false
+		}
+	}
+	return true
+}
+
+func numPositiveLiterals(fmls []Formula) int {
+	var n = 0
+	for _, fml := range fmls {
+		if fml.IsPositiveLiteral() {
+			n++
+		}
+	}
+	return n
+}
+
+func (fml Formula) IsConjunctOfLiterals() bool {
+	return fml.IsLiteral() || (fml.IsConjunction() && onlyLiterals(fml.GetSubFormulae()))
+}
+
+func (fml Formula) IsDisjunctOfLiterals() bool {
+	return fml.IsLiteral() || (fml.IsDisjunction() && onlyLiterals(fml.GetSubFormulae()))
+}
+
+func (fml Formula) IsHornClause() bool {
+	var literals = fml.GetSubFormulae()
+	return fml.IsLiteral() || (fml.IsDisjunction() && onlyLiterals(literals) && (numPositiveLiterals(literals) <= 1))
+}
+
+func (fml Formula) IsKNF() bool {
+	if fml.IsConjunction() {
+		for _, subFml := range fml.GetSubFormulae() {
+			if !subFml.IsDisjunctOfLiterals() {
+				return false
+			}
+		}
+		return true
+	} else {
+		return fml.IsDisjunctOfLiterals()
+	}
+}
+
+func (fml Formula) IsDNF() bool {
+	if fml.IsDisjunction() {
+		for _, subFml := range fml.GetSubFormulae() {
+			if !subFml.IsConjunctOfLiterals() {
+				return false
+			}
+		}
+		return true
+	} else {
+		return fml.IsConjunctOfLiterals()
+	}
+}
+
+func (fml Formula) IsHornFml() bool {
+	if fml.IsConjunction() {
+		for _, subFml := range fml.GetSubFormulae() {
+			if !subFml.IsHornClause() {
+				return false
+			}
+		}
+		return true
+	} else {
+		return fml.IsHornClause()
+	}
+}

codego/aussagenlogik/formulae/formulae_pairs.go

@@ -1,34 +0,0 @@
-package formulae
-
-/* ---------------------------------------------------------------- *
- * TYPE FormulaPair, FormulaPairs
- * ---------------------------------------------------------------- */
-
-type FormulaPair struct {
-	Pos Formula
-	Neg Formula
-}
-
-type FormulaPairs []FormulaPair
-
-/* ---------------------------------------------------------------- *
- * Methods for FormulaPairs
- * ---------------------------------------------------------------- */
-
-func NewFormulaPairs(pairs []FormulaPair) FormulaPairs { return pairs }
-
-func (pairs FormulaPairs) Pos() []Formula {
-	var fmls = make([]Formula, len(pairs))
-	for i, pair := range pairs {
-		fmls[i] = pair.Pos
-	}
-	return fmls
-}
-
-func (pairs FormulaPairs) Neg() []Formula {
-	var fmls = make([]Formula, len(pairs))
-	for i, pair := range pairs {
-		fmls[i] = pair.Neg
-	}
-	return fmls
-}

codego/aussagenlogik/formulae/formulae_test.go

@@ -0,0 +1,158 @@
+package formulae_test
+
+/* ---------------------------------------------------------------- *
+ * UNIT TESTING
+ * ---------------------------------------------------------------- */
+
+import (
+	"logik/aussagenlogik/formulae"
+	"logik/aussagenlogik/schema"
+	"testing"
+
+	"github.com/stretchr/testify/assert"
+)
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE KNF
+ * ---------------------------------------------------------------- */
+
+func TestRecogniseKNF(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+
+	fml = schema.ParseExpr("A7")
+	assert.True(fml.IsKNF())
+	fml = schema.ParseExpr("! A7")
+	assert.True(fml.IsKNF())
+	fml = schema.ParseExpr("!! A7")
+	assert.False(fml.IsKNF())
+
+	fml = schema.ParseExpr("(A0 || ! A1 || A7)")
+	assert.True(fml.IsKNF())
+	fml = schema.ParseExpr("(A0 && ! A1 && A7)")
+	assert.True(fml.IsKNF())
+	fml = schema.ParseExpr("(A0 && !! A1 && A7)")
+	assert.False(fml.IsKNF())
+
+	fml = schema.ParseExpr("(A0 || ! A1 || A7) && (A4 || ! A5) && A1")
+	assert.True(fml.IsKNF())
+	fml = schema.ParseExpr("(A0 && ! A1 && A7) || (A4 && ! A5) || A1")
+	assert.False(fml.IsKNF())
+	fml = schema.ParseExpr("((A0 || ! A1 || A7) && (A4 || ! A5)) || A8")
+	assert.False(fml.IsKNF())
+}
+
+func TestRecogniseDNF(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+
+	fml = schema.ParseExpr("A7")
+	assert.True(fml.IsDNF())
+	fml = schema.ParseExpr("! A7")
+	assert.True(fml.IsDNF())
+	fml = schema.ParseExpr("!! A7")
+	assert.False(fml.IsDNF())
+
+	fml = schema.ParseExpr("(A0 && ! A1 && A7)")
+	assert.True(fml.IsDNF())
+	fml = schema.ParseExpr("(A0 || ! A1 || A7)")
+	assert.True(fml.IsDNF())
+	fml = schema.ParseExpr("(A0 || !! A1 || A7)")
+	assert.False(fml.IsDNF())
+
+	fml = schema.ParseExpr("(A0 && ! A1 && A7) || (A4 && ! A5) || A1")
+	assert.True(fml.IsDNF())
+	fml = schema.ParseExpr("(A0 || ! A1 || A7) && (A4 || ! A5) && A1")
+	assert.False(fml.IsDNF())
+	fml = schema.ParseExpr("((A0 && ! A1 && A7) || (A4 && ! A5)) && A8")
+	assert.False(fml.IsDNF())
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE Horn
+ * ---------------------------------------------------------------- */
+
+func TestRecogniseHorn(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+
+	fml = schema.ParseExpr("A7")
+	assert.True(fml.IsHornFml())
+	fml = schema.ParseExpr("! A7")
+	assert.True(fml.IsHornFml())
+	fml = schema.ParseExpr("!! A7")
+	assert.False(fml.IsHornFml())
+
+	fml = schema.ParseExpr("(! A0 || ! A1 || A7)")
+	assert.True(fml.IsHornFml())
+	fml = schema.ParseExpr("(A0 && ! A1 && A7)")
+	assert.True(fml.IsHornFml())
+	fml = schema.ParseExpr("(A0 && !! A1 && A7)")
+	assert.False(fml.IsHornFml())
+
+	fml = schema.ParseExpr("(A0 && ! A1 && ! A7) || (A4 && ! A5) || (! A1 && ! A8)")
+	assert.False(fml.IsHornFml())
+	fml = schema.ParseExpr("(A0 && ! A1 && ! A7) || (A4 && ! A5) || (! A1 && ! A8)")
+	assert.False(fml.IsHornFml())
+	fml = schema.ParseExpr("(A0 || ! A1 || ! A7) && (A4 || ! A5) && (! A1 || ! A8)")
+	assert.True(fml.IsHornFml())
+	fml = schema.ParseExpr("((A0 || ! A1 || A7) && (A4 || ! A5)) || A8")
+	assert.False(fml.IsHornFml())
+}
+
+func TestTransformHornToFormula(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+	var horn formulae.FormulaHorn
+	var hornClauses []formulae.FormulaHornClause
+
+	fml = schema.ParseExpr("A8")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(1, len(hornClauses))
+	assert.ElementsMatch([]string{"A8"}, hornClauses[0].Pos.GetAtoms())
+	assert.ElementsMatch([]string{}, hornClauses[0].Neg.GetAtoms())
+	assert.Equal("(1 -> A8)", horn.ToFormula().GetExpr())
+
+	fml = schema.ParseExpr("!A8")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(1, len(hornClauses))
+	assert.ElementsMatch([]string{}, hornClauses[0].Pos.GetAtoms())
+	assert.ElementsMatch([]string{"A8"}, hornClauses[0].Neg.GetAtoms())
+	assert.Equal("(A8 -> 0)", horn.ToFormula().GetExpr())
+
+	fml = schema.ParseExpr("!A3 || A2 || !A7 || !A9")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(1, len(hornClauses))
+	assert.ElementsMatch([]string{"A2"}, hornClauses[0].Pos.GetAtoms())
+	assert.ElementsMatch([]string{"A3", "A7", "A9"}, hornClauses[0].Neg.GetAtoms())
+	assert.Equal("((A3 && A7 && A9) -> A2)", horn.ToFormula().GetExpr())
+
+	fml = schema.ParseExpr("!A3 || !A2 || !A7 || !A9")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(1, len(hornClauses))
+	assert.ElementsMatch([]string{}, hornClauses[0].Pos.GetAtoms())
+	assert.ElementsMatch([]string{"A2", "A3", "A7", "A9"}, hornClauses[0].Neg.GetAtoms())
+	assert.Equal("((A3 && A2 && A7 && A9) -> 0)", horn.ToFormula().GetExpr())
+
+	fml = schema.ParseExpr("!A3 && A2 && !A7 && A9 && A7")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(5, len(hornClauses))
+	assert.Equal("((A3 -> 0) && (1 -> A2) && (A7 -> 0) && (1 -> A9) && (1 -> A7))", horn.ToFormula().GetExpr())
+
+	fml = schema.ParseExpr("(A0 || ! A1 || ! A7) && (A4 || ! A5) && (! A1 || ! A8)")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(3, len(hornClauses))
+	assert.Equal("(((A1 && A7) -> A0) && (A5 -> A4) && ((A1 && A8) -> 0))", horn.ToFormula().GetExpr())
+}

codego/aussagenlogik/recursion/recursion_test.go

@@ -205,8 +205,7 @@ func TestAtomsCalc1(test *testing.T) {
 	var val []string
 	fml = schema.ParseExpr("A0")
 	val = recursion.Atoms(fml)
-	utils.SortStrings(&val)
+	assert.ElementsMatch([]string{"A0"}, val)
-	assert.Equal([]string{"A0"}, val)
 }
 
 func TestAtomsCalc2(test *testing.T) {
@@ -216,8 +215,7 @@ func TestAtomsCalc2(test *testing.T) {
 	var val []string
 	fml = schema.ParseExpr("((( ! A8 && A3 ) || A4 ) && A0 )")
 	val = recursion.Atoms(fml)
-	utils.SortStrings(&val)
+	assert.ElementsMatch([]string{"A0", "A3", "A4", "A8"}, val)
-	assert.Equal([]string{"A0", "A3", "A4", "A8"}, val)
 }
 
 /* ---------------------------------------------------------------- *

codego/aussagenlogik/schema/schema_test.go

@@ -25,8 +25,13 @@ func TestParseExpr(test *testing.T) {
 	assert.Equal("atom", tree.GetKind())
 	assert.Equal(0, len(tree.GetSubFormulae()))
 
+	tree = schema.ParseExpr("A12")
+	assert.Equal("A12", tree.GetExpr())
+	assert.Equal("atom", tree.GetKind())
+	assert.Equal(0, len(tree.GetSubFormulae()))
+
 	tree = schema.ParseExpr("  ! A5  ")
-	assert.Equal("! A5", tree.GetExpr())
+	assert.Equal("!A5", tree.GetExpr())
 	assert.Equal("not", tree.GetKind())
 	assert.Equal(1, len(tree.GetSubFormulae()))
 
@@ -35,8 +40,8 @@ func TestParseExpr(test *testing.T) {
 	assert.Equal("implies", tree.GetKind())
 	assert.Equal(2, len(tree.GetSubFormulae()))
 
-	tree = schema.ParseExpr("(  A0 &&   A1) || A2")
+	tree = schema.ParseExpr("(  A0 && ! !  A1) || A2")
-	assert.Equal("((A0 && A1) || A2)", tree.GetExpr())
+	assert.Equal("((A0 && !!A1) || A2)", tree.GetExpr())
 	assert.Equal("or2", tree.GetKind())
 	assert.Equal(2, len(tree.GetSubFormulae()))
 }

codego/core/utils/utils.go

@@ -85,6 +85,14 @@ func SumList(x []int) int {
  * METHODS: for string lists
  * ---------------------------------------------------------------- */
 
+func CopyStringList(list []string) []string {
+	var listCopy = make([]string, len(list))
+	for i, value := range list {
+		listCopy[i] = value
+	}
+	return listCopy
+}
+
 func StrListContains(list []string, x string) bool {
 	for _, obj := range list {
 		if obj == x {
@@ -153,3 +161,15 @@ func UnionStringsList(lists [][]string) []string {
 	}
 	return list
 }
+
+/* ---------------------------------------------------------------- *
+ * METHODS: for maps
+ * ---------------------------------------------------------------- */
+
+func CopyMapStringBool(m map[string]bool) map[string]bool {
+	var mCopy = map[string]bool{}
+	for key, value := range m {
+		mCopy[key] = value
+	}
+	return mCopy
+}

codego/core/utils/utils_test.go

@@ -20,11 +20,11 @@ func TestJsonToArrayOfStrings(test *testing.T) {
 	var assert = assert.New(test)
 	var result []string
 	utils.JsonToArrayOfStrings("[]", &result)
-	assert.Equal([]string{}, result)
+	assert.ElementsMatch([]string{}, result)
 	utils.JsonToArrayOfStrings("[ \"ganymed\" ]", &result)
-	assert.Equal([]string{"ganymed"}, result)
+	assert.ElementsMatch([]string{"ganymed"}, result)
 	utils.JsonToArrayOfStrings("[ \"ganymed\", \"io\" ]", &result)
-	assert.Equal([]string{"ganymed", "io"}, result)
+	assert.ElementsMatch([]string{"ganymed", "io"}, result)
 	assert.Panics(func() { utils.JsonToArrayOfStrings("[ 178 ]", &result) }, "Should panic if converting not a JSON-encoded array of strings!")
 	assert.Panics(func() { utils.JsonToArrayOfStrings("true", &result) }, "Should panic if converting not a JSON-encoded array of strings!")
 	assert.Panics(func() { utils.JsonToArrayOfStrings("", &result) }, "Should panic if converting not a JSON-encoded array of strings!")
@@ -73,6 +73,7 @@ func TestSumList(test *testing.T) {
 func TestSortStrings(test *testing.T) {
 	var assert = assert.New(test)
 	var list = []string{"katze", "Hund", "baby", "Pluto", "Saturn", "Mond"}
+	// NOTE: here use .Equal and not .ElementsMatch, since order important.
 	utils.SortStrings(&list)
 	assert.Equal([]string{"baby", "Hund", "katze", "Mond", "Pluto", "Saturn"}, list)
 }
@@ -85,7 +86,7 @@ func TestFilterStrings(test *testing.T) {
 	var assert = assert.New(test)
 	var list = []string{"abram", "aaron", "aardvark", "aarhus", "alaska", "eel", "aal"}
 	var list2 = utils.FilterStrings(&list, func(x string) bool { return strings.HasPrefix(x, "aa") })
-	assert.Equal([]string{"aaron", "aardvark", "aarhus", "aal"}, list2)
+	assert.ElementsMatch([]string{"aaron", "aardvark", "aarhus", "aal"}, list2)
 }
 
 /* ---------------------------------------------------------------- *
@@ -97,8 +98,7 @@ func TestUnionStrings2(test *testing.T) {
 	var list1 = []string{"red", "blue", "blue", "green", "blue", "grey", "black", "green"}
 	var list2 = []string{"yellow", "orange", "lila", "red"}
 	var list = utils.UnionStrings2(list1, list2)
-	utils.SortStrings(&list)
+	assert.ElementsMatch([]string{"black", "blue", "green", "grey", "lila", "orange", "red", "yellow"}, list)
-	assert.Equal([]string{"black", "blue", "green", "grey", "lila", "orange", "red", "yellow"}, list)
 }
 
 func TestUnionStringsInPlace(test *testing.T) {
@@ -106,8 +106,7 @@ func TestUnionStringsInPlace(test *testing.T) {
 	var list1 = []string{"red", "blue", "green"}
 	var list2 = []string{"yellow", "red", "blue", "red", "black"}
 	utils.UnionStringsInPlace(&list1, list2)
-	utils.SortStrings(&list1)
+	assert.ElementsMatch([]string{"black", "blue", "green", "red", "yellow"}, list1)
-	assert.Equal([]string{"black", "blue", "green", "red", "yellow"}, list1)
 }
 
 func TestUnionStringsList(test *testing.T) {
@@ -116,6 +115,5 @@ func TestUnionStringsList(test *testing.T) {
 	var lists [][]string
 	lists = [][]string{{"red", "blue", "blue", "green"}, {"yellow", "red", "black"}}
 	list = utils.UnionStringsList(lists)
-	utils.SortStrings(&list)
+	assert.ElementsMatch([]string{"black", "blue", "green", "red", "yellow"}, list)
-	assert.Equal([]string{"black", "blue", "green", "red", "yellow"}, list)
 }

codego/grammars/aussagenlogik.g4

@@ -1,7 +1,9 @@
 grammar aussagenlogik;
 
 // Standardtokens:
-NUMBER: [0-9]+;
+NUMBER: [0-9];
+ZERO: ~[a-zA-Z0-9][0]; // negatives Look-Behind nötig, um konfliktierendes Lexing zu vermeiden
+ONE: ~[a-zA-Z0-9][1];  // ""
 WHITESPACE: [ \r\n\t]+ -> skip;
 LBRACE: '(';
 RBRACE: ')';
@@ -24,9 +26,9 @@ open: and2 | and | or2 | or | implies | iff;
 
 // Schemata für atomische Ausdrücke
 atomic: taut | contradiction | atom | generic;
-taut:  ('1'|'true');
+taut:  (ONE|'true');
-contradiction: ('0'|'false');
+contradiction: (ZERO|'false');
-atom: 'A0' | 'A1' | 'A' NUMBER; // muss A0, A1 wegen falsum/verum extra auflisten
+atom: 'A' NUMBER+;
 // als 'generische' Formeln schreibe bspw. {F}, {G}, usw.
 generic: LCURLYBRACE TEXT+ RCURLYBRACE | LCURLYBRACE TEXT* ( generic TEXT* )+ RCURLYBRACE;
 // FIXME: liest Zahlen schlecht ein

codego/scripts/test.sh

@@ -9,7 +9,7 @@
 ################################
 
 export TEST_VERBOSE=false # <- true: unittest mit verbose output
-export TEST_TIMEOUT="60s"
+export TEST_TIMEOUT="10s"
 
 function call_go() {
     go $@;