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