raj_mathe/logik2021
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Compare commits

base: raj_mathe:73b7817dcd5ae871a71aefe95515473defeef4b0
Branches Tags
raj_mathe:master
..
compare: raj_mathe:6641946bad285b4785b2f5aeef0ecec3ca19992a
Branches Tags
raj_mathe:master

No commits in common. "73b7817dcd5ae871a71aefe95515473defeef4b0" and "6641946bad285b4785b2f5aeef0ecec3ca19992a" have entirely different histories.
73b7817dcd ... 6641946bad

20 changed files with 657 additions and 1113 deletions
Show Stats Expand all files Collapse all files

4
codego/.gitignore vendored
View File

@ -18,9 +18,9 @@
## Go Source ## Go Source
!/aussagenlogik !/aussagenlogik
!/aussagenlogik/recursion !/aussagenlogik/rekursion
!/aussagenlogik/schema !/aussagenlogik/schema
!/aussagenlogik/formulae !/aussagenlogik/syntaxbaum
!/core !/core
!/core/environment !/core/environment
!/core/utils !/core/utils

4
codego/README.md
View File

@ -64,7 +64,7 @@ run_programme;
## Offene Challenges ## ## Offene Challenges ##
In dem Ordner `aussagenlogik/recursion` (relativ zum aktuellen Ordner) findet man mehrere leere Methoden (mit dem Kommentar `// Herausforderung...`). Wer es mag, kann versuchen, an seinem Rechner diese Methoden zu definieren und auszuprobieren. In der Datei `aussagenlogik/rekursion.go` (relativ zu diesem Ordner) findet man mehrere leere Methoden (mit dem Kommentar `// Herausforderung...`). Wer es mag, kann versuchen, an seinem Rechner diese Methoden zu definieren und auszuprobieren.
### Händisch testen ### ### Händisch testen ###
@ -79,7 +79,7 @@ Diese Tests existieren parallel zu jedem Modul und folgen dem Namensschema `..._
```bash ```bash
chmod +x scripts/test.sh chmod +x scripts/test.sh
``` ```
- In `aussagenlogik/recursion/recursion_test.go` beim relevanten Testteil eine oder mehrere der Zeilen - In `aussagenlogik/rekursion/rekursion_test.go` beim relevanten Testteil eine oder mehrere der Zeilen
```go ```go
test.Skip("Methode noch nicht implementiert") test.Skip("Methode noch nicht implementiert")
``` ```

283
codego/aussagenlogik/formulae/formulae.go
View File

@ -1,283 +0,0 @@
package formulae
import (
"fmt"
"strings"
)
/* ---------------------------------------------------------------- *
* TYPE Formula
* ---------------------------------------------------------------- */
type Formula struct {
kind string
expr string
valence int
subformulae [](*Formula)
}
/* ---------------------------------------------------------------- *
* METHODS
* ---------------------------------------------------------------- */
func (fml *Formula) SetKind(kind string) {
fml.kind = kind
}
func (fml Formula) GetKind() string {
return fml.kind
}
func (fml *Formula) SetExpr(expr string) {
fml.expr = expr
}
func (fml Formula) GetExpr() string {
return fml.expr
}
func (fml *Formula) SetSubformulae(children [](*Formula)) {
fml.subformulae = children
fml.valence = len(children)
}
func (fml Formula) GetSubFormulae() []Formula {
var n int = fml.valence
var children = make([]Formula, n)
for i, subfml := range fml.subformulae {
children[i] = *subfml
}
return children
}
func (fml Formula) GetChild(indexOpt ...int) Formula {
var index int = 0
if len(indexOpt) > 0 {
index = indexOpt[0]
}
var subfml Formula
if 0 <= index && index < fml.valence {
subfml = *(fml.subformulae[index])
} else {
panic(fmt.Sprintf("Instance has no child of index %d !", index))
}
return subfml
}
func (fml Formula) Pretty(preindentOpt ...string) string {
var preindent string = ""
if len(preindentOpt) > 0 {
preindent = preindentOpt[0]
}
return fml.pretty(preindent, " ", "", 0)
}
func (fml Formula) pretty(preindent string, tab string, prepend string, depth int) string {
var indent string = preindent + strings.Repeat(tab, depth)
switch fml.valence {
case 0:
switch kind := fml.kind; kind {
case "atom", "generic":
return indent + prepend + kind + " " + fml.expr
default:
return indent + prepend + kind
}
default:
var lines string = indent + prepend + fml.kind
prepend = "|__ "
for _, subfml := range fml.subformulae {
lines += "\n" + subfml.pretty(preindent, tab, prepend, depth+1)
}
return lines
}
}
func (fml Formula) Deepcopy() Formula {
var children = make([](*Formula), len(fml.subformulae))
for i, child := range fml.subformulae {
childCopy := child.Deepcopy()
children[i] = &childCopy
}
return Formula{
expr: fml.expr,
kind: fml.kind,
valence: fml.valence,
subformulae: children,
}
}
/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
* METHODS: Basic constructions
* ---------------------------------------------------------------- */
var Tautology = Formula{
kind: "taut",
expr: "1",
valence: 0,
subformulae: [](*Formula){},
}
var Contradiction = Formula{
kind: "contradiction",
expr: "0",
valence: 0,
subformulae: [](*Formula){},
}
func Atom(expr string) Formula {
return Formula{
kind: "atom",
expr: expr,
valence: 0,
subformulae: [](*Formula){},
}
}
func NegatedAtom(expr string) Formula {
return Negation(Atom(expr))
}
func Generic(expr string) Formula {
return Formula{
kind: "generic",
expr: expr,
valence: 0,
subformulae: [](*Formula){},
}
}
func Negation(fml Formula) Formula {
return Formula{
kind: "not",
expr: "!" + " " + fml.expr,
valence: 1,
subformulae: [](*Formula){&fml},
}
}
func Conjunction2(fml1 Formula, fml2 Formula) Formula {
return Formula{
kind: "and2",
expr: "(" + fml1.expr + " && " + fml2.expr + ")",
valence: 2,
subformulae: [](*Formula){&fml1, &fml2},
}
}
func Conjunction(fmls []Formula) Formula {
var expr string = ""
var children = make([](*Formula), len(fmls))
for i, fml := range fmls {
if i > 0 {
expr += " && "
}
expr += fml.expr
children[i] = &fml
}
return Formula{
kind: "and",
expr: "(" + expr + ")",
valence: len(children),
subformulae: children,
}
}
func Disjunction2(fml1 Formula, fml2 Formula) Formula {
return Formula{
kind: "or2",
expr: "(" + fml1.expr + " || " + fml2.expr + ")",
valence: 2,
subformulae: [](*Formula){&fml1, &fml2},
}
}
func Disjunction(fmls []Formula) Formula {
var expr string = ""
var children = make([](*Formula), len(fmls))
for i, fml := range fmls {
if i > 0 {
expr += " || "
}
expr += fml.expr
children[i] = &fml
}
return Formula{
kind: "or",
expr: "(" + expr + ")",
valence: len(children),
subformulae: children,
}
}
func Implies(fml1 Formula, fml2 Formula) Formula {
return Formula{
kind: "implies",
expr: "(" + fml1.expr + " -> " + fml2.expr + ")",
valence: 2,
subformulae: [](*Formula){&fml1, &fml2},
}
}
/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
* METHODS: Recognition of Formula-Types
* ---------------------------------------------------------------- */
func (fml Formula) IsIrreducible() bool {
return fml.valence == 0
}
func (fml Formula) IsAtom() bool {
return fml.kind == "atom"
}
func (fml Formula) IsPositiveLiteral() bool {
return fml.IsAtom()
}
func (fml Formula) IsNegativeLiteral() bool {
return fml.IsNegation() && fml.GetChild().IsAtom()
}
func (fml Formula) IsLiteral() bool {
return fml.IsPositiveLiteral() || fml.IsNegativeLiteral()
}
func (fml Formula) IsGeneric() bool {
return fml.kind == "generic"
}
func (fml Formula) IsTautologySymbol() bool {
return fml.kind == "taut"
}
func (fml Formula) IsContradictionSymbol() bool {
return fml.kind == "contradiction"
}
func (fml Formula) IsConnective() bool {
return fml.valence > 0
}
func (fml Formula) IsNegation() bool {
return fml.kind == "not"
}
func (fml Formula) IsConjunction2() bool {
return fml.kind == "and2"
}
func (fml Formula) IsConjunction() bool {
return fml.kind == "and" || fml.kind == "and2"
}
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"
}

165
codego/aussagenlogik/formulae/formulae_generate.go
View File

@ -1,165 +0,0 @@
package formulae
// NOTE: GoLang hat noch keine generics. Erst 2022.
/* ---------------------------------------------------------------- *
* Generate int-value FN from scheme
* ---------------------------------------------------------------- */
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) }
fn = func(fml Formula) int {
var subfmls = fml.GetSubFormulae()
var n = len(subfmls)
var subChan = make([](chan int), n)
var prevValues = make([]int, len(subfmls))
// start parallel computations on subformulas
for i, subfml := range subfmls {
subChan[i] = make(chan int) // create Channel, since currently nil
go subFn(subChan[i], subfml)
}
// successively read values
for i := 0; i < n; i++ {
prevValues[i] = <-subChan[i]
}
// apply schema to get value for formula
return scheme(fml, prevValues)
}
return fn
}
/* ---------------------------------------------------------------- *
* Generate string-value FN from scheme
* ---------------------------------------------------------------- */
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) }
fn = func(fml Formula) string {
var subfmls = fml.GetSubFormulae()
var n = len(subfmls)
var subChan = make([](chan string), n)
var prevValues = make([]string, len(subfmls))
// start parallel computations on subformulas
for i, subfml := range subfmls {
subChan[i] = make(chan string) // create Channel, since currently nil
go subFn(subChan[i], subfml)
}
// successively read values
for i := 0; i < n; i++ {
prevValues[i] = <-subChan[i]
}
// apply schema to get value for formula
return scheme(fml, prevValues)
}
return fn
}
/* ---------------------------------------------------------------- *
* Generate *[]string-value Fn from scheme
* ---------------------------------------------------------------- */
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) }
fn = func(fml Formula) []string {
var subfmls = fml.GetSubFormulae()
var n = len(subfmls)
var subChan = make([](chan []string), n)
var prevValues = make([][]string, len(subfmls))
// start parallel computations on subformulas
for i, subfml := range subfmls {
subChan[i] = make(chan []string) // create Channel, since currently nil
go subFn(subChan[i], subfml)
}
// successively read values
for i := 0; i < n; i++ {
prevValues[i] = <-subChan[i]
}
// apply schema to get value for formula
return scheme(fml, prevValues)
}
return fn
}
/* ---------------------------------------------------------------- *
* Generate Formula-value Fn from scheme
* ---------------------------------------------------------------- */
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) }
fn = func(fml Formula) Formula {
var subfmls = fml.GetSubFormulae()
var n = len(subfmls)
var subChan = make([](chan Formula), n)
var prevValues = make([]Formula, len(subfmls))
// start parallel computations on subformulas
for i, subfml := range subfmls {
subChan[i] = make(chan Formula) // create Channel, since currently nil
go subFn(subChan[i], subfml)
}
// successively read values
for i := 0; i < n; i++ {
prevValues[i] = <-subChan[i]
}
// apply schema to get value for formula
return scheme(fml, prevValues)
}
return fn
}
/* ---------------------------------------------------------------- *
* Generate *[]Formula-value Fn from scheme
* ---------------------------------------------------------------- */
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) }
fn = func(fml Formula) *[]Formula {
var subfmls = fml.GetSubFormulae()
var n = len(subfmls)
var subChan = make([](chan *[]Formula), n)
var prevValues = make([](*[]Formula), len(subfmls))
// start parallel computations on subformulas
for i, subfml := range subfmls {
subChan[i] = make(chan *[]Formula) // create Channel, since currently nil
go subFn(subChan[i], subfml)
}
// successively read values
for i := 0; i < n; i++ {
prevValues[i] = <-subChan[i]
}
// apply schema to get value for formula
return scheme(fml, prevValues)
}
return fn
}
/* ---------------------------------------------------------------- *
* Generate {pos: Formula, ne: Formula}-value Fn from scheme
* ---------------------------------------------------------------- */
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) }
fn = func(fml Formula) FormulaPair {
var subfmls = fml.GetSubFormulae()
var n = len(subfmls)
var subChan = make([](chan FormulaPair), n)
var prevValues = make([]FormulaPair, len(subfmls))
// start parallel computations on subformulas
for i, subfml := range subfmls {
subChan[i] = make(chan FormulaPair) // create Channel, since currently nil
go subFn(subChan[i], subfml)
}
// successively read values
for i := 0; i < n; i++ {
prevValues[i] = <-subChan[i]
}
// apply schema to get value for formula
return scheme(fml, prevValues)
}
return fn
}

34
codego/aussagenlogik/formulae/formulae_types.go
View File

@ -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
}

20
codego/aussagenlogik/recursion/recursion_atoms.go
View File

@ -1,20 +0,0 @@
package recursion
import (
"logik/aussagenlogik/formulae"
)
/* ---------------------------------------------------------------- *
* METHOD: Atoms
* ---------------------------------------------------------------- */
func Atoms(tree formulae.Formula) []string {
// Definiere Schema:
var schema = func(tree formulae.Formula, prevValues [][]string) []string {
// Herausforderung: schreibe diese Funktion!
return []string{}
}
// Erzeuge Funktion aus Schema und berechne Wert:
fn := formulae.CreateFromSchemeStringsValued(schema)
return fn(tree)
}

49
codego/aussagenlogik/recursion/recursion_count.go
View File

@ -1,49 +0,0 @@
package recursion
import (
"logik/aussagenlogik/formulae"
)
/* ---------------------------------------------------------------- *
* METHOD: Formula Depth
* ---------------------------------------------------------------- */
func FmlDepth(tree formulae.Formula) int {
// Definiere Schema:
var schema = func(tree formulae.Formula, prevValues []int) int {
// Herausforderung: schreibe diese Funktion!
return 0
}
// Erzeuge Funktion aus Schema und berechne Wert:
fn := formulae.CreateFromSchemeIntValued(schema)
return fn(tree)
}
/* ---------------------------------------------------------------- *
* METHOD: Formula Length
* ---------------------------------------------------------------- */
func FmlLength(tree formulae.Formula) int {
// Definiere Schema:
var schema = func(tree formulae.Formula, prevValues []int) int {
// Herausforderung: schreibe diese Funktion!
return 0
}
// Erzeuge Funktion aus Schema und berechne Wert:
fn := formulae.CreateFromSchemeIntValued(schema)
return fn(tree)
}
/* ---------------------------------------------------------------- *
* METHOD: Number of Parentheses
* ---------------------------------------------------------------- */
func NrParentheses(tree formulae.Formula) int {
// Definiere Schema:
var schema = func(tree formulae.Formula, prevValues []int) int {
// Herausforderung: schreibe diese Funktion!
return 0
}
// Erzeuge Funktion aus Schema und berechne Wert:
fn := formulae.CreateFromSchemeIntValued(schema)
return fn(tree)
}

42
codego/aussagenlogik/recursion/recursion_eval.go
View File

@ -1,42 +0,0 @@
package recursion
import (
"logik/aussagenlogik/formulae"
"logik/core/utils"
)
/* ---------------------------------------------------------------- *
* METHOD: Evaluation of fomulae in models
* ---------------------------------------------------------------- */
func Eval(tree formulae.Formula, I []string) int {
// Definiere (parameterisiertes) Schema:
var schema = func(_I []string) func(formulae.Formula, []int) int {
return func(tree formulae.Formula, prevValues []int) int {
if tree.IsAtom() || tree.IsGeneric() {
return utils.BoolToInt(utils.StrListContains(_I, tree.GetExpr()))
} else if tree.IsTautologySymbol() {
return 1
} else if tree.IsContradictionSymbol() {
return 0
} else if tree.IsNegation() {
return 1 - prevValues[0]
} else if tree.IsConjunction2() {
return utils.Min2(prevValues[0], prevValues[1])
} else if tree.IsConjunction() {
return utils.MinList(prevValues)
} else if tree.IsDisjunction2() {
return utils.Max2(prevValues[0], prevValues[1])
} else if tree.IsDisjunction() {
return utils.MaxList(prevValues)
} else if tree.IsImplication() {
return utils.BoolToInt(prevValues[0] <= prevValues[1])
} else {
panic("Could not evaluate expression!")
}
}
}
// Erzeuge Funktion aus Schema und berechne Wert:
fn := formulae.CreateFromSchemeIntValued(schema(I))
return fn(tree)
}

77
codego/aussagenlogik/recursion/recursion_nnf.go
View File

@ -1,77 +0,0 @@
package recursion
import (
"logik/aussagenlogik/formulae"
)
/* ---------------------------------------------------------------- *
* METHOD: compute NNF
* ---------------------------------------------------------------- */
// NOTE: diese bedarf einer Art Doppeltrekursion
func NNF(tree formulae.Formula) formulae.Formula {
// Definiere Schema:
var schema = func(tree formulae.Formula, prevValues []formulae.FormulaPair) formulae.FormulaPair {
// separate out positive and negative parts:
var pairs = formulae.NewFormulaPairs(prevValues)
var prevPos = pairs.Pos()
var prevNeg = pairs.Neg()
// compute value from previous positive/negative parts:
if tree.IsPositiveLiteral() {
return formulae.FormulaPair{
Pos: tree.Deepcopy(),
Neg: formulae.Negation(tree),
}
} else if tree.IsNegativeLiteral() {
return formulae.FormulaPair{
Pos: tree.Deepcopy(),
Neg: prevPos[0],
}
} else if tree.IsTautologySymbol() {
return formulae.FormulaPair{
Pos: formulae.Tautology,
Neg: formulae.Contradiction,
}
} else if tree.IsContradictionSymbol() {
return formulae.FormulaPair{
Pos: formulae.Contradiction,
Neg: formulae.Tautology,
}
} else if tree.IsNegation() {
return formulae.FormulaPair{
Pos: prevNeg[0],
Neg: prevPos[0],
}
} else if tree.IsConjunction2() {
return formulae.FormulaPair{
Pos: formulae.Conjunction2(prevPos[0], prevPos[1]),
Neg: formulae.Disjunction2(prevNeg[0], prevNeg[1]),
}
} else if tree.IsConjunction() {
return formulae.FormulaPair{
Pos: formulae.Conjunction(prevPos),
Neg: formulae.Disjunction(prevNeg),
}
} else if tree.IsDisjunction2() {
return formulae.FormulaPair{
Pos: formulae.Disjunction2(prevPos[0], prevPos[1]),
Neg: formulae.Conjunction2(prevNeg[0], prevNeg[1]),
}
} else if tree.IsDisjunction() {
return formulae.FormulaPair{
Pos: formulae.Disjunction(prevPos),
Neg: formulae.Conjunction(prevNeg),
}
} else if tree.IsImplication() {
return formulae.FormulaPair{
Pos: formulae.Implies(prevPos[0], prevPos[1]),
Neg: formulae.Conjunction2(prevPos[0], prevNeg[1]),
}
} else {
panic("Could not evaluate expression!")
}
}
// Erzeuge Funktion aus Schema und berechne Wert:
fn := formulae.CreateFromSchemeFmlPairValued(schema)
return fn(tree).Pos
}

359
codego/aussagenlogik/recursion/recursion_test.go
View File

@ -1,359 +0,0 @@
package recursion_test
/* ---------------------------------------------------------------- *
* UNIT TESTING
* ---------------------------------------------------------------- */
import (
"logik/aussagenlogik/formulae"
"logik/aussagenlogik/recursion"
"logik/aussagenlogik/schema"
"logik/core/utils"
"testing"
"github.com/stretchr/testify/assert"
)
/* ---------------------------------------------------------------- *
* TESTCASE eval(·, ·)
* ---------------------------------------------------------------- */
func TestEvalLiteral(test *testing.T) {
var assert = assert.New(test)
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) {
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(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)
}
/* ---------------------------------------------------------------- *
* TESTCASE Atoms(·)
* ---------------------------------------------------------------- */
func TestAtomsNoduplicates(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var fml formulae.Formula
var val []string
fml = schema.ParseExpr("( A4 && ( A4 || A4 ))")
val = recursion.Atoms(fml)
var n int = len(utils.FilterStrings(&val, func(x string) bool { return x == "A4" }))
assert.Equal(1, n, "Atome dürfen nicht mehrfach vorkommen!")
}
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
fml = schema.ParseExpr("( {F} || A3 )")
val = recursion.Atoms(fml)
utils.SortStrings(&val)
assert.NotContains(val, "F", "Nichtatomare Formeln dürfen nicht vorkommen!")
}
func TestAtomsCalc1(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var fml formulae.Formula
var val []string
fml = schema.ParseExpr("A0")
val = recursion.Atoms(fml)
utils.SortStrings(&val)
assert.Equal([]string{"A0"}, val)
}
func TestAtomsCalc2(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var fml formulae.Formula
var val []string
fml = schema.ParseExpr("((( ! A8 && A3 ) || A4 ) && A0 )")
val = recursion.Atoms(fml)
utils.SortStrings(&val)
assert.Equal([]string{"A0", "A3", "A4", "A8"}, val)
}
/* ---------------------------------------------------------------- *
* TESTCASE depth(·, ·)
* ---------------------------------------------------------------- */
func TestDepthCalc1(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("A0")
val = recursion.FmlDepth(fml)
assert.Equal(0, val)
}
func TestDepthCalc2(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("!! A8")
val = recursion.FmlDepth(fml)
assert.Equal(2, val)
}
func TestDepthCalc3(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("( ! A0 && A3 )")
val = recursion.FmlDepth(fml)
assert.Equal(2, val)
}
func TestDepthCalc4(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
val = recursion.FmlDepth(fml)
assert.Equal(4, val)
}
func TestDepthCalc5(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
val = recursion.FmlDepth(fml)
assert.Equal(5, val)
}
/* ---------------------------------------------------------------- *
* TESTCASE length(·)
* ---------------------------------------------------------------- */
func TestLengthCalc1(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("A0")
val = recursion.FmlLength(fml)
assert.Equal(1, val)
}
func TestLengthCalc2(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("!! A8")
val = recursion.FmlLength(fml)
assert.Equal(3, val)
}
func TestLengthCalc3(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("( ! A0 && A3 )")
val = recursion.FmlLength(fml)
assert.Equal(4, val)
}
func TestLengthCalc4(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
val = recursion.FmlLength(fml)
assert.Equal(8, val)
}
func TestLengthCalc5(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
val = recursion.FmlLength(fml)
assert.Equal(9, val)
}
/* ---------------------------------------------------------------- *
* TESTCASE #Parentheses(·)
* ---------------------------------------------------------------- */
func TestParenthesesCalc1(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("A0")
val = recursion.NrParentheses(fml)
assert.Equal(0, val)
}
func TestParenthesesCalc2(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("!! A8")
val = recursion.NrParentheses(fml)
assert.Equal(0, val)
}
func TestParenthesesCalc3(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("( ! A0 && A3 )")
val = recursion.NrParentheses(fml)
assert.Equal(2, val)
}
func TestParenthesesCalc4(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
val = recursion.NrParentheses(fml)
assert.Equal(6, val)
}
func TestParenthesesCalc5(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var val int
var fml formulae.Formula
fml = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
val = recursion.NrParentheses(fml)
assert.Equal(6, val)
}
/* ---------------------------------------------------------------- *
* TESTCASE NNF
* ---------------------------------------------------------------- */
func TestNNFatoms(test *testing.T) {
var assert = assert.New(test)
var fml formulae.Formula
var nnf_expected formulae.Formula
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())
}
func TestNNFconj(test *testing.T) {
var assert = assert.New(test)
var fml formulae.Formula
var nnf_expected formulae.Formula
nnf_expected = formulae.Disjunction2(formulae.NegatedAtom("A0"), formulae.NegatedAtom("A1"))
fml = schema.ParseExpr("! (A0 && A1)")
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
nnf_expected = formulae.Disjunction2(formulae.Atom("A0"), formulae.Atom("A1"))
fml = schema.ParseExpr("! (! A0 && ! A1)")
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
nnf_expected = formulae.Conjunction2(formulae.Atom("A0"), formulae.NegatedAtom("A1"))
fml = schema.ParseExpr("(A0 && ! A1)")
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
}
func TestNNFdisj(test *testing.T) {
var assert = assert.New(test)
var fml formulae.Formula
var nnf_expected formulae.Formula
nnf_expected = formulae.Conjunction2(formulae.NegatedAtom("A0"), formulae.NegatedAtom("A1"))
fml = schema.ParseExpr("! (A0 || A1)")
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
nnf_expected = formulae.Conjunction2(formulae.Atom("A0"), formulae.Atom("A1"))
fml = schema.ParseExpr("! (! A0 || ! A1)")
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
nnf_expected = formulae.Disjunction2(formulae.Atom("A0"), formulae.NegatedAtom("A1"))
fml = schema.ParseExpr("(A0 || ! A1)")
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
}
func TestNNFcalcComplex(test *testing.T) {
var assert = assert.New(test)
var fml formulae.Formula
var nnf_expected formulae.Formula
fml = schema.ParseExpr("! (! (!A0 || A1) || ! ! A8)")
nnf_expected = schema.ParseExpr("((!A0 || A1) && ! A8)")
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
fml = schema.ParseExpr("! (! (!A0 || !(A1 && ! A7)) && ! A8)")
nnf_expected = schema.ParseExpr("((!A0 || (! A1 || A7)) || A8)")
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
}

70
codego/aussagenlogik/rekursion/rekursion.go Normal file
View File

@ -0,0 +1,70 @@
package rekursion
import (
"logik/aussagenlogik/syntaxbaum"
"logik/core/utils"
)
/* ---------------------------------------------------------------- *
* EXPORTS
* ---------------------------------------------------------------- */
type RekursiveChannelInt struct {
channel chan int
}
func RekursivEval(ch chan int, tree syntaxbaum.SyntaxBaum, I []string) {
// Werte für Teilformeln rekursiv berechnen
fn := func(_ch chan int, _tree syntaxbaum.SyntaxBaum) { RekursivEval(_ch, _tree, I) }
var values = RekursiveCallInt(fn, tree.GetChildren())
// Aus Werten für Teilformeln Wert für Formeln berechnen
if tree.IsAtom() || tree.IsGeneric() {
ch <- utils.BoolToInt(utils.StrListContains(I, tree.GetExpr()))
} else if tree.IsTautologySymbol() {
ch <- 1
} else if tree.IsContradictionSymbol() {
ch <- 0
} else if tree.IsNegation() {
ch <- 1 - values[0]
} else if tree.IsConjunction2() {
ch <- utils.Min2(values[0], values[1])
} else if tree.IsConjunction() {
ch <- utils.MinList(values)
} else if tree.IsDisjunction2() {
ch <- utils.Max2(values[0], values[1])
} else if tree.IsDisjunction() {
ch <- utils.MaxList(values)
} else if tree.IsImplication() {
ch <- utils.BoolToInt(values[0] <= values[1])
} else {
panic("Could not evaluate expression!")
}
}
func RekursivAtoms(ch chan []string, tree syntaxbaum.SyntaxBaum) {
// // Werte für Teilformeln rekursiv berechnen
// var values = RekursiveCallStringList(RekursivAtoms, tree.GetChildren())
// Herausforderung: schreibe diese Funktion!
ch <- []string{}
}
func RekursivDepth(ch chan int, tree syntaxbaum.SyntaxBaum) {
// // Werte für Teilformeln rekursiv berechnen
// var values = RekursiveCallInt(RekursivDepth, tree.GetChildren())
// Herausforderung: schreibe diese Funktion!
ch <- 0
}
func RekursivLength(ch chan int, tree syntaxbaum.SyntaxBaum) {
// // Werte für Teilformeln rekursiv berechnen
// var values = RekursiveCallInt(RekursivLength, tree.GetChildren())
// Herausforderung: schreibe diese Funktion!
ch <- 0
}
func RekursivParentheses(ch chan int, tree syntaxbaum.SyntaxBaum) {
// // Werte für Teilformeln rekursiv berechnen
// var values = RekursiveCallInt(RekursivParentheses, tree.GetChildren())
// Herausforderung: schreibe diese Funktion!
ch <- 0
}

51
codego/aussagenlogik/rekursion/rekursion_aux.go Normal file
View File

@ -0,0 +1,51 @@
package rekursion
import (
"logik/aussagenlogik/syntaxbaum"
)
/* ---------------------------------------------------------------- *
* EXPORTS
* ---------------------------------------------------------------- */
func RekursiveCallInt(fn func(ch chan int, tree syntaxbaum.SyntaxBaum), children []syntaxbaum.SyntaxBaum) []int {
subChannel := make(chan int)
values := make([]int, len(children))
// start parallel computations on subformulae
for _, subtree := range children {
go fn(subChannel, subtree)
}
// successively read values
for i := 0; i < len(children); i++ {
values[i] = <-subChannel
}
return values
}
func RekursiveCallString(fn func(ch chan string, tree syntaxbaum.SyntaxBaum), children []syntaxbaum.SyntaxBaum) []string {
subChannel := make(chan string)
values := make([]string, len(children))
// start parallel computations
for _, subtree := range children {
go fn(subChannel, subtree)
}
// successively read values
for i := 0; i < len(children); i++ {
values[i] = <-subChannel
}
return values
}
func RekursiveCallStringList(fn func(ch chan []string, tree syntaxbaum.SyntaxBaum), children []syntaxbaum.SyntaxBaum) [][]string {
subChannel := make(chan []string)
values := make([][]string, len(children))
// start parallel computations
for _, subtree := range children {
go fn(subChannel, subtree)
}
// successively read values
for i := 0; i < len(children); i++ {
values[i] = <-subChannel
}
return values
}

295
codego/aussagenlogik/rekursion/rekursion_test.go Normal file
View File

@ -0,0 +1,295 @@
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 ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
var I []string
tree = schema.ParseExpr("A0")
I = []string{"A0"}
go rekursion.RekursivEval(ch, tree, I)
assert.Equal(1, <-ch)
tree = schema.ParseExpr("A0")
I = []string{}
go rekursion.RekursivEval(ch, tree, I)
assert.Equal(0, <-ch)
tree = schema.ParseExpr("! A0")
I = []string{"A0"}
go rekursion.RekursivEval(ch, tree, I)
assert.Equal(0, <-ch)
tree = schema.ParseExpr("! A0")
I = []string{}
go rekursion.RekursivEval(ch, tree, I)
assert.Equal(1, <-ch)
}
func TestRekursivEvalComplex1(test *testing.T) {
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
var I []string
tree = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || A2 ))")
I = []string{"A0", "A2"}
go rekursion.RekursivEval(ch, tree, I)
assert.Equal(1, <-ch)
I = []string{"A0", "A3"}
go rekursion.RekursivEval(ch, tree, I)
assert.Equal(1, <-ch)
I = []string{"A0"}
go rekursion.RekursivEval(ch, tree, I)
assert.Equal(0, <-ch)
I = []string{"A4", "A8"}
go rekursion.RekursivEval(ch, tree, I)
assert.Equal(1, <-ch)
}
func TestRekursivEvalComplex2(test *testing.T) {
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
var I []string
tree = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || ! A2 ))")
I = []string{"A0", "A2"}
go rekursion.RekursivEval(ch, tree, I)
assert.Equal(0, <-ch)
I = []string{"A0", "A3"}
go rekursion.RekursivEval(ch, tree, I)
assert.Equal(1, <-ch)
}
/* ---------------------------------------------------------------- *
* TESTCASE Atoms(·)
* ---------------------------------------------------------------- */
func TestRekursivAtomsNoduplicates(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan []string)
var tree syntaxbaum.SyntaxBaum
var val []string
tree = schema.ParseExpr("( A4 && ( A4 || A4 ))")
go rekursion.RekursivAtoms(ch, tree)
val = <-ch
var n int = len(utils.FilterStrings(&val, func(x string) bool { return x == "A4" }))
assert.Equal(1, n, "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 ch = make(chan []string)
var tree syntaxbaum.SyntaxBaum
var val []string
tree = schema.ParseExpr("( {F} || A3 )")
go rekursion.RekursivAtoms(ch, tree)
val = <-ch
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 ch = make(chan []string)
var tree syntaxbaum.SyntaxBaum
var val []string
tree = schema.ParseExpr("A0")
go rekursion.RekursivAtoms(ch, tree)
val = <-ch
utils.SortStrings(&val)
assert.Equal([]string{"A0"}, val)
}
func TestRekursivAtomsCalc2(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan []string)
var tree syntaxbaum.SyntaxBaum
var val []string
tree = schema.ParseExpr("((( ! A8 && A3 ) || A4 ) && A0 )")
go rekursion.RekursivAtoms(ch, tree)
val = <-ch
utils.SortStrings(&val)
assert.Equal([]string{"A0", "A3", "A4", "A8"}, val)
}
/* ---------------------------------------------------------------- *
* TESTCASE depth(·, ·)
* ---------------------------------------------------------------- */
func TestRekursivDepthCalc1(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("A0")
go rekursion.RekursivDepth(ch, tree)
assert.Equal(0, <-ch)
}
func TestRekursivDepthCalc2(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("!! A8")
go rekursion.RekursivDepth(ch, tree)
assert.Equal(2, <-ch)
}
func TestRekursivDepthCalc3(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("( ! A0 && A3 )")
go rekursion.RekursivDepth(ch, tree)
assert.Equal(2, <-ch)
}
func TestRekursivDepthCalc4(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
go rekursion.RekursivDepth(ch, tree)
assert.Equal(4, <-ch)
}
func TestRekursivDepthCalc5(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
go rekursion.RekursivDepth(ch, tree)
assert.Equal(5, <-ch)
}
/* ---------------------------------------------------------------- *
* TESTCASE length(·)
* ---------------------------------------------------------------- */
func TestRekursivLengthCalc1(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("A0")
go rekursion.RekursivLength(ch, tree)
assert.Equal(1, <-ch)
}
func TestRekursivLengthCalc2(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("!! A8")
go rekursion.RekursivLength(ch, tree)
assert.Equal(3, <-ch)
}
func TestRekursivLengthCalc3(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("( ! A0 && A3 )")
go rekursion.RekursivLength(ch, tree)
assert.Equal(4, <-ch)
}
func TestRekursivLengthCalc4(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
go rekursion.RekursivLength(ch, tree)
assert.Equal(8, <-ch)
}
func TestRekursivLengthCalc5(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
go rekursion.RekursivLength(ch, tree)
assert.Equal(9, <-ch)
}
/* ---------------------------------------------------------------- *
* TESTCASE #Parentheses(·)
* ---------------------------------------------------------------- */
func TestRekursivParenthesesCalc1(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("A0")
go rekursion.RekursivParentheses(ch, tree)
assert.Equal(0, <-ch)
}
func TestRekursivParenthesesCalc2(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("!! A8")
go rekursion.RekursivParentheses(ch, tree)
assert.Equal(0, <-ch)
}
func TestRekursivParenthesesCalc3(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("( ! A0 && A3 )")
go rekursion.RekursivParentheses(ch, tree)
assert.Equal(2, <-ch)
}
func TestRekursivParenthesesCalc4(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
go rekursion.RekursivParentheses(ch, tree)
assert.Equal(6, <-ch)
}
func TestRekursivParenthesesCalc5(test *testing.T) {
test.Skip("Methode noch nicht implementiert")
var assert = assert.New(test)
var ch = make(chan int)
var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
go rekursion.RekursivParentheses(ch, tree)
assert.Equal(6, <-ch)
}

90
codego/aussagenlogik/schema/schema.go
View File

@ -1,8 +1,9 @@
package schema package schema
import ( import (
"logik/aussagenlogik/formulae" "logik/aussagenlogik/syntaxbaum"
parser "logik/grammars/aussagenlogik" parser "logik/grammars/aussagenlogik"
"strings"
"github.com/antlr/antlr4/runtime/Go/antlr" "github.com/antlr/antlr4/runtime/Go/antlr"
) )
@ -11,12 +12,12 @@ import (
* EXPORTS * EXPORTS
* ---------------------------------------------------------------- */ * ---------------------------------------------------------------- */
func ParseExpr(u string) formulae.Formula { func ParseExpr(u string) syntaxbaum.SyntaxBaum {
var lexer = createLexer(u) var lexer = createLexer(u)
var tokenStream = lexerToTokenStream(lexer) var tokenStream = lexerToTokenStream(lexer)
var prs = parser.NewaussagenlogikParser(tokenStream) var prs = parser.NewaussagenlogikParser(tokenStream)
var t = prs.Start() var t = prs.Start()
tree := createFormula(t, prs) tree := createSyntaxBaum(t, prs)
return tree return tree
} }
@ -37,9 +38,9 @@ func createLexer(u string) antlr.Lexer {
return parser.NewaussagenlogikLexer(stream) return parser.NewaussagenlogikLexer(stream)
} }
func createFormula(tree antlr.Tree, parser antlr.Parser) formulae.Formula { func createSyntaxBaum(tree antlr.Tree, parser antlr.Parser) syntaxbaum.SyntaxBaum {
var ant = antlrTree{tree: tree, parser: &parser} var ant = antlrTree{tree: tree, parser: &parser}
return ant.toFormula() return ant.toSyntaxBaum()
} }
/* ---------------------------------------------------------------- * /* ---------------------------------------------------------------- *
@ -85,7 +86,8 @@ func (ant antlrTree) getTextContentLeaves() string {
return expr return expr
} }
func (ant antlrTree) toFormula() formulae.Formula { func (ant antlrTree) toSyntaxBaum() syntaxbaum.SyntaxBaum {
var tree syntaxbaum.SyntaxBaum
var label string = ant.getLabel() var label string = ant.getLabel()
var subants = ant.getChildren() var subants = ant.getChildren()
var nChildren = len(subants) var nChildren = len(subants)
@ -93,73 +95,65 @@ func (ant antlrTree) toFormula() formulae.Formula {
switch label { switch label {
case "start": case "start":
if nChildren == 1 { if nChildren == 1 {
return subants[0].toFormula() return subants[0].toSyntaxBaum()
} }
case "open": case "open":
if nChildren == 1 { if nChildren == 1 {
return subants[0].toFormula() return subants[0].toSyntaxBaum()
} }
case "closed": case "closed":
switch nChildren { switch nChildren {
case 1: case 1:
return subants[0].toFormula() return subants[0].toSyntaxBaum()
// expr = ( expr )
case 3: case 3:
return subants[1].toFormula() return subants[1].toSyntaxBaum()
} }
case "atomic": case "atomic":
if nChildren == 1 { if nChildren == 1 {
return subants[0].toFormula() subant := subants[0]
tree = syntaxbaum.SyntaxBaum{}
tree.SetKind(subant.getLabel())
tree.SetExpr(subant.getTextContentLeaves())
tree.SetChildren([](*syntaxbaum.SyntaxBaum){})
return tree
} }
case "taut":
return formulae.Tautology
case "contradiction":
return formulae.Contradiction
case "atom":
return formulae.Atom(ant.getTextContentLeaves())
case "generic":
return formulae.Generic(ant.getTextContentLeaves())
case "not": case "not":
// NOTE: expr = ! expr
if nChildren == 2 { if nChildren == 2 {
return formulae.Negation(subants[1].toFormula()) // NOTE: Children = [NotSymbol, Teilformel]
subtree := subants[1].toSyntaxBaum()
tree = syntaxbaum.SyntaxBaum{}
tree.SetKind(label)
tree.SetExpr(subants[0].getTextContent() + " " + subtree.GetExpr())
tree.SetChildren([](*syntaxbaum.SyntaxBaum){&subtree})
return tree
} }
case "and2": case "and2", "and", "or2", "or", "implies":
// NOTE: expr = expr && expr
if nChildren == 3 {
return formulae.Conjunction2(subants[0].toFormula(), subants[2].toFormula())
}
case "or2":
// NOTE: expr = expr || expr
if nChildren == 3 {
return formulae.Disjunction2(subants[0].toFormula(), subants[2].toFormula())
}
case "implies":
// NOTE: expr = expr -> expr
if nChildren == 3 {
return formulae.Implies(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) var n int = int((len(subants) + 1) / 2)
if nChildren == 2*n-1 && n >= 2 { if nChildren == 2*n-1 && n >= 2 {
var subtrees = make([]formulae.Formula, n) var isSymb bool = false
var isSymb bool = true var subtrees = make([](*syntaxbaum.SyntaxBaum), n)
var i int = 0 var i int = 0
var expr string = ""
for _, subant := range subants { for _, subant := range subants {
if isSymb { if isSymb {
subtrees[i] = subant.toFormula() expr += " " + subant.getTextContent()
} else {
subtree := subant.toSyntaxBaum()
subtrees[i] = &subtree
expr += " " + subtree.GetExpr()
i++ i++
} }
// NOTE: infix notation: alternatives between expression and symbol // NOTE: infix notation: alternatives between expression and symbol
isSymb = !isSymb isSymb = !isSymb
} }
switch label { expr = strings.Trim(expr, " ")
case "and": var lbrace string = "("
return formulae.Conjunction(subtrees) var rbrace string = ")"
case "or": tree = syntaxbaum.SyntaxBaum{}
return formulae.Disjunction(subtrees) tree.SetKind(label)
} tree.SetExpr(lbrace + expr + rbrace)
tree.SetChildren(subtrees)
return tree
} }
} }

12
codego/aussagenlogik/schema/schema_test.go
View File

@ -5,8 +5,8 @@ package schema_test
* ---------------------------------------------------------------- */ * ---------------------------------------------------------------- */
import ( import (
"logik/aussagenlogik/formulae"
"logik/aussagenlogik/schema" "logik/aussagenlogik/schema"
"logik/aussagenlogik/syntaxbaum"
"testing" "testing"
"github.com/stretchr/testify/assert" "github.com/stretchr/testify/assert"
@ -18,25 +18,25 @@ import (
func TestParseExpr(test *testing.T) { func TestParseExpr(test *testing.T) {
var assert = assert.New(test) var assert = assert.New(test)
var tree formulae.Formula var tree syntaxbaum.SyntaxBaum
tree = schema.ParseExpr("A8712") tree = schema.ParseExpr("A8712")
assert.Equal("A8712", tree.GetExpr()) assert.Equal("A8712", tree.GetExpr())
assert.Equal("atom", tree.GetKind()) assert.Equal("atom", tree.GetKind())
assert.Equal(0, len(tree.GetSubFormulae())) assert.Equal(0, len(tree.GetChildren()))
tree = schema.ParseExpr(" ! A5 ") tree = schema.ParseExpr(" ! A5 ")
assert.Equal("! A5", tree.GetExpr()) assert.Equal("! A5", tree.GetExpr())
assert.Equal("not", tree.GetKind()) assert.Equal("not", tree.GetKind())
assert.Equal(1, len(tree.GetSubFormulae())) assert.Equal(1, len(tree.GetChildren()))
tree = schema.ParseExpr("A0 -> A1") tree = schema.ParseExpr("A0 -> A1")
assert.Equal("(A0 -> A1)", tree.GetExpr()) assert.Equal("(A0 -> A1)", tree.GetExpr())
assert.Equal("implies", tree.GetKind()) assert.Equal("implies", tree.GetKind())
assert.Equal(2, len(tree.GetSubFormulae())) assert.Equal(2, len(tree.GetChildren()))
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("or2", tree.GetKind())
assert.Equal(2, len(tree.GetSubFormulae())) assert.Equal(2, len(tree.GetChildren()))
} }

154
codego/aussagenlogik/syntaxbaum/syntaxbaum.go Normal file
View File

@ -0,0 +1,154 @@
package syntaxbaum
import (
"errors"
"fmt"
"strings"
)
type SyntaxBaum struct {
kind string
expr string
valence int
children [](*SyntaxBaum)
}
/* ---------------------------------------------------------------- *
* METHODS
* ---------------------------------------------------------------- */
func (tree *SyntaxBaum) SetKind(kind string) {
tree.kind = kind
}
func (tree SyntaxBaum) GetKind() string {
return tree.kind
}
func (tree *SyntaxBaum) SetExpr(expr string) {
tree.expr = expr
}
func (tree SyntaxBaum) GetExpr() string {
return tree.expr
}
func (tree *SyntaxBaum) SetChildren(children [](*SyntaxBaum)) {
tree.children = children
tree.valence = len(children)
}
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) IsIrreducible() bool {
return tree.valence == 0
}
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) IsGeneric() bool {
return tree.kind == "generic"
}
func (tree SyntaxBaum) IsTautologySymbol() bool {
return tree.kind == "taut"
}
func (tree SyntaxBaum) IsContradictionSymbol() bool {
return tree.kind == "contradiction"
}
func (tree SyntaxBaum) IsConnective() bool {
return tree.valence > 0
}
func (tree SyntaxBaum) IsNegation() bool {
return tree.kind == "not"
}
func (tree SyntaxBaum) IsConjunction2() bool {
return tree.kind == "and2"
}
func (tree SyntaxBaum) IsConjunction() bool {
return tree.kind == "and" || tree.kind == "and2"
}
func (tree SyntaxBaum) IsDisjunction2() bool {
return tree.kind == "or2"
}
func (tree SyntaxBaum) IsDisjunction() bool {
return tree.kind == "or" || tree.kind == "or2"
}
func (tree SyntaxBaum) IsImplication() bool {
return tree.kind == "implies"
}

4
codego/core/utils/utils.go
View File

@ -131,7 +131,7 @@ func UnionStrings2(list1 []string, list2 []string) []string {
} }
// assumes that listTo contains no duplicates // assumes that listTo contains no duplicates
func UnionStringsInPlace(listTo *[]string, listFrom []string) { func UnionStringsTo(listTo *[]string, listFrom []string) {
var mark = make(map[string]bool) var mark = make(map[string]bool)
for _, item := range listFrom { for _, item := range listFrom {
mark[item] = true mark[item] = true
@ -149,7 +149,7 @@ func UnionStringsInPlace(listTo *[]string, listFrom []string) {
func UnionStringsList(lists [][]string) []string { func UnionStringsList(lists [][]string) []string {
var list = []string{} var list = []string{}
for _, list_ := range lists { for _, list_ := range lists {
UnionStringsInPlace(&list, list_) UnionStringsTo(&list, list_)
} }
return list return list
} }

6
codego/core/utils/utils_test.go
View File

@ -89,7 +89,7 @@ func TestFilterStrings(test *testing.T) {
} }
/* ---------------------------------------------------------------- * /* ---------------------------------------------------------------- *
* TESTCASE UnionStrings2, UnionStringsInPlace, UnionStringsList * TESTCASE UnionStrings2, UnionStringsTo, UnionStringsList
* ---------------------------------------------------------------- */ * ---------------------------------------------------------------- */
func TestUnionStrings2(test *testing.T) { func TestUnionStrings2(test *testing.T) {
@ -101,11 +101,11 @@ func TestUnionStrings2(test *testing.T) {
assert.Equal([]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) { func TestUnionStringsTo(test *testing.T) {
var assert = assert.New(test) var assert = assert.New(test)
var list1 = []string{"red", "blue", "green"} var list1 = []string{"red", "blue", "green"}
var list2 = []string{"yellow", "red", "blue", "red", "black"} var list2 = []string{"yellow", "red", "blue", "red", "black"}
utils.UnionStringsInPlace(&list1, list2) utils.UnionStringsTo(&list1, list2)
utils.SortStrings(&list1) utils.SortStrings(&list1)
assert.Equal([]string{"black", "blue", "green", "red", "yellow"}, list1) assert.Equal([]string{"black", "blue", "green", "red", "yellow"}, list1)
} }

41
codego/main.go
View File

@ -2,9 +2,9 @@ package main
import ( import (
"fmt" "fmt"
"logik/aussagenlogik/formulae" "logik/aussagenlogik/rekursion"
"logik/aussagenlogik/recursion"
"logik/aussagenlogik/schema" "logik/aussagenlogik/schema"
"logik/aussagenlogik/syntaxbaum"
env "logik/core/environment" env "logik/core/environment"
"logik/core/utils" "logik/core/utils"
"strings" "strings"
@ -21,7 +21,6 @@ type dataType struct {
type resultsType struct { type resultsType struct {
eval int eval int
nnf formulae.Formula
atoms []string atoms []string
depth int depth int
length int length int
@ -51,18 +50,28 @@ func getData() {
utils.JsonToArrayOfStrings(s, &data.interpretation) utils.JsonToArrayOfStrings(s, &data.interpretation)
} }
func getResults(tree formulae.Formula) resultsType { func getResults(tree syntaxbaum.SyntaxBaum) resultsType {
ch1 := make(chan int)
ch2 := make(chan []string)
ch3 := make(chan int)
ch4 := make(chan int)
ch5 := make(chan int)
go rekursion.RekursivEval(ch1, tree, data.interpretation)
go rekursion.RekursivAtoms(ch2, tree)
go rekursion.RekursivDepth(ch3, tree)
go rekursion.RekursivLength(ch4, tree)
go rekursion.RekursivParentheses(ch5, tree)
// Methoden ausführen:
return resultsType{ return resultsType{
eval: recursion.Eval(tree, data.interpretation), eval: <-ch1,
nnf: recursion.NNF(tree), atoms: <-ch2,
atoms: recursion.Atoms(tree), depth: <-ch3,
depth: recursion.FmlDepth(tree), length: <-ch4,
length: recursion.FmlLength(tree), nParentheses: <-ch5,
nParentheses: recursion.NrParentheses(tree),
} }
} }
func displayResults(tree formulae.Formula, results resultsType) { func displayResults(tree syntaxbaum.SyntaxBaum, results resultsType) {
fmt.Println(fmt.Sprintf( fmt.Println(fmt.Sprintf(
dedent.Dedent(` dedent.Dedent(`
Syntaxbaum von Syntaxbaum von
@ -72,11 +81,10 @@ func displayResults(tree formulae.Formula, results resultsType) {
Für I = {%[3]s} und F wie oben gilt Für I = {%[3]s} und F wie oben gilt
eval(F, I) = %[4]d; eval(F, I) = %[4]d;
F^NNF = %[5]s; atoms(F) = {%[5]s}; <- *
atoms(F) = {%[6]s}; <- * depth(F) = %[6]d; <- *
depth(F) = %[7]d; <- * length(F) = %[7]d; <- *
length(F) = %[8]d; <- * #parentheses(F) = %[8]d; <- *
#parentheses(F) = %[9]d; <- *
* noch nicht implementiert! * noch nicht implementiert!
Challenge: schreibe diese Methoden! (siehe README.md) Challenge: schreibe diese Methoden! (siehe README.md)
@ -85,7 +93,6 @@ func displayResults(tree formulae.Formula, results resultsType) {
tree.Pretty(" "), tree.Pretty(" "),
strings.Join(data.interpretation, ", "), strings.Join(data.interpretation, ", "),
results.eval, results.eval,
results.nnf.GetExpr(),
// string(results.atoms), // string(results.atoms),
strings.Join(results.atoms, ", "), strings.Join(results.atoms, ", "),
results.depth, results.depth,

10
codego/scripts/build.sh
View File

@ -47,10 +47,12 @@ function precompile_grammars() {
} }
function compile_programme() { function compile_programme() {
[ -f "dist/main" ] && rm "dist/main"; [ -f "main" ] && rm "main";
echo -e "\033[92;1mGO\033[0m kompiliert \033[1mmain.go\033[0m"; echo -e "\033[92;1mGO\033[0m kompiliert \033[1mmain.go\033[0m";
call_go build -o dist/main "main.go"; call_go build "main.go";
! [ -f "dist/main" ] && exit 1; ! [ -f "main" ] && exit 1;
! [ -d "dist" ] && mkdir "dist";
mv "main" "dist";
} }
function run_programme() { function run_programme() {
@ -66,6 +68,6 @@ function run_programme() {
check_requirements; check_requirements;
# Code als Programm kompilieren und ausführen: # Code als Programm kompilieren und ausführen:
# precompile_grammars; precompile_grammars;
compile_programme; compile_programme;
run_programme; run_programme;