|
|
|
@ -9,60 +9,60 @@ import (
|
|
|
|
|
* ---------------------------------------------------------------- */ |
|
|
|
|
|
|
|
|
|
// NOTE: diese bedarf einer Art Doppeltrekursion
|
|
|
|
|
func NNF(tree formulae.Formula) formulae.Formula { |
|
|
|
|
func NNF(fml formulae.Formula) formulae.Formula { |
|
|
|
|
// Definiere Schema:
|
|
|
|
|
var schema = func(tree formulae.Formula, prevValues []formulae.FormulaPair) formulae.FormulaPair { |
|
|
|
|
var schema = func(fml 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() { |
|
|
|
|
if fml.IsPositiveLiteral() { |
|
|
|
|
return formulae.FormulaPair{ |
|
|
|
|
Pos: tree.Deepcopy(), |
|
|
|
|
Neg: formulae.Negation(tree), |
|
|
|
|
Pos: fml.Deepcopy(), |
|
|
|
|
Neg: formulae.Negation(fml), |
|
|
|
|
} |
|
|
|
|
} else if tree.IsNegativeLiteral() { |
|
|
|
|
} else if fml.IsNegativeLiteral() { |
|
|
|
|
return formulae.FormulaPair{ |
|
|
|
|
Pos: tree.Deepcopy(), |
|
|
|
|
Pos: fml.Deepcopy(), |
|
|
|
|
Neg: prevPos[0], |
|
|
|
|
} |
|
|
|
|
} else if tree.IsTautologySymbol() { |
|
|
|
|
} else if fml.IsTautologySymbol() { |
|
|
|
|
return formulae.FormulaPair{ |
|
|
|
|
Pos: formulae.Tautology, |
|
|
|
|
Neg: formulae.Contradiction, |
|
|
|
|
} |
|
|
|
|
} else if tree.IsContradictionSymbol() { |
|
|
|
|
} else if fml.IsContradictionSymbol() { |
|
|
|
|
return formulae.FormulaPair{ |
|
|
|
|
Pos: formulae.Contradiction, |
|
|
|
|
Neg: formulae.Tautology, |
|
|
|
|
} |
|
|
|
|
} else if tree.IsNegation() { |
|
|
|
|
} else if fml.IsNegation() { |
|
|
|
|
return formulae.FormulaPair{ |
|
|
|
|
Pos: prevNeg[0], |
|
|
|
|
Neg: prevPos[0], |
|
|
|
|
} |
|
|
|
|
} else if tree.IsConjunction2() { |
|
|
|
|
} else if fml.IsConjunction2() { |
|
|
|
|
return formulae.FormulaPair{ |
|
|
|
|
Pos: formulae.Conjunction2(prevPos[0], prevPos[1]), |
|
|
|
|
Neg: formulae.Disjunction2(prevNeg[0], prevNeg[1]), |
|
|
|
|
} |
|
|
|
|
} else if tree.IsConjunction() { |
|
|
|
|
} else if fml.IsConjunction() { |
|
|
|
|
return formulae.FormulaPair{ |
|
|
|
|
Pos: formulae.Conjunction(prevPos), |
|
|
|
|
Neg: formulae.Disjunction(prevNeg), |
|
|
|
|
} |
|
|
|
|
} else if tree.IsDisjunction2() { |
|
|
|
|
} else if fml.IsDisjunction2() { |
|
|
|
|
return formulae.FormulaPair{ |
|
|
|
|
Pos: formulae.Disjunction2(prevPos[0], prevPos[1]), |
|
|
|
|
Neg: formulae.Conjunction2(prevNeg[0], prevNeg[1]), |
|
|
|
|
} |
|
|
|
|
} else if tree.IsDisjunction() { |
|
|
|
|
} else if fml.IsDisjunction() { |
|
|
|
|
return formulae.FormulaPair{ |
|
|
|
|
Pos: formulae.Disjunction(prevPos), |
|
|
|
|
Neg: formulae.Conjunction(prevNeg), |
|
|
|
|
} |
|
|
|
|
} else if tree.IsImplication() { |
|
|
|
|
} else if fml.IsImplication() { |
|
|
|
|
return formulae.FormulaPair{ |
|
|
|
|
Pos: formulae.Implies(prevPos[0], prevPos[1]), |
|
|
|
|
Neg: formulae.Conjunction2(prevPos[0], prevNeg[1]), |
|
|
|
@ -73,5 +73,5 @@ func NNF(tree formulae.Formula) formulae.Formula {
|
|
|
|
|
} |
|
|
|
|
// Erzeuge Funktion aus Schema und berechne Wert:
|
|
|
|
|
fn := formulae.CreateFromSchemeFmlPairValued(schema) |
|
|
|
|
return fn(tree).Pos |
|
|
|
|
return fn(fml).Pos |
|
|
|
|
} |
|
|
|
|