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 TestEvalNegation(test *testing.T) {
	var assert = assert.New(test)
	var val int
	var fml formulae.Formula
	var I []string

	fml = schema.ParseExpr("A4 || ! A4")
	I = []string{}
	val = recursion.Eval(fml, I)
	assert.Equal(1, val)

	fml = schema.ParseExpr("A4 && ! A4")
	I = []string{}
	val = recursion.Eval(fml, I)
	assert.Equal(0, val)
}

func TestEvalConjunction(test *testing.T) {
	var assert = assert.New(test)
	var val int
	var fml formulae.Formula
	var I []string

	fml = schema.ParseExpr("A0 && A1")
	I = []string{"A0"}
	val = recursion.Eval(fml, I)
	assert.Equal(0, val)

	fml = schema.ParseExpr("A0 && A1")
	I = []string{"A0", "A1"}
	val = recursion.Eval(fml, I)
	assert.Equal(1, val)
}

func TestEvalDisjunction(test *testing.T) {
	var assert = assert.New(test)
	var val int
	var fml formulae.Formula
	var I []string

	fml = schema.ParseExpr("A0 || A1")
	I = []string{"A0"}
	val = recursion.Eval(fml, I)
	assert.Equal(1, val)

	fml = schema.ParseExpr("A0 || A1")
	I = []string{"A7"}
	val = recursion.Eval(fml, I)
	assert.Equal(0, val)
}

func TestEvalImplication(test *testing.T) {
	var assert = assert.New(test)
	var val int
	var fml formulae.Formula
	var I []string

	fml = schema.ParseExpr("A0 -> A1")
	I = []string{"A0"}
	val = recursion.Eval(fml, I)
	assert.Equal(0, val)

	fml = schema.ParseExpr("A0 -> A1")
	I = []string{"A0", "A1"}
	val = recursion.Eval(fml, I)
	assert.Equal(1, val)

	fml = schema.ParseExpr("A0 -> A1")
	I = []string{"A7"}
	val = recursion.Eval(fml, I)
	assert.Equal(1, val)
}

func TestEvalIff(test *testing.T) {
	var assert = assert.New(test)
	var val int
	var fml formulae.Formula
	var I []string

	fml = schema.ParseExpr("A0 <-> A1")
	I = []string{"A0"}
	val = recursion.Eval(fml, I)
	assert.Equal(0, val)

	fml = schema.ParseExpr("A0 <-> A1")
	I = []string{"A0", "A1"}
	val = recursion.Eval(fml, I)
	assert.Equal(1, val)

	fml = schema.ParseExpr("A0 <-> A1")
	I = []string{"A7"}
	val = recursion.Eval(fml, I)
	assert.Equal(1, val)
}

func TestEvalComplex(test *testing.T) {
	var assert = assert.New(test)
	var val int
	var fml formulae.Formula
	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)

	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")
	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())
}