4 changed files with 236 additions and 283 deletions
@ -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" |
||||
} |
@ -0,0 +1,119 @@
|
||||
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: 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" } |
@ -0,0 +1,117 @@
|
||||
package formulae |
||||
|
||||
/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * |
||||
* CONSTANTS |
||||
* ---------------------------------------------------------------- */ |
||||
|
||||
var Tautology = Formula{ |
||||
kind: "taut", |
||||
expr: "1", |
||||
valence: 0, |
||||
subformulae: [](*Formula){}, |
||||
} |
||||
|
||||
var Contradiction = Formula{ |
||||
kind: "contradiction", |
||||
expr: "0", |
||||
valence: 0, |
||||
subformulae: [](*Formula){}, |
||||
} |
||||
|
||||
/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * |
||||
* METHODS: Constructions |
||||
* ---------------------------------------------------------------- */ |
||||
|
||||
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}, |
||||
} |
||||
} |
Loading…
Reference in new issue