-
Notifications
You must be signed in to change notification settings - Fork 0
/
literal_substitution.go
61 lines (59 loc) · 2.01 KB
/
literal_substitution.go
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
package transformation
import (
"github.com/booleworks/logicng-go/errorx"
f "github.com/booleworks/logicng-go/formula"
)
// SubstituteLiterals performs a special substitution from literal to literal
// on the given formula. In contrast to the standard Substitute function
// which can only map variables, this function can also map literals.
//
// Always the best fit is chosen. So if there are two mappings for e.g. a -> b
// and ~a -> c. Then ~a will be mapped to c and not to ~b. On the other hand if
// there is only the mapping a -> b, the literal ~a will be mapped to ~b.
func SubstituteLiterals(fac f.Factory, formula f.Formula, substitution *map[f.Literal]f.Literal) f.Formula {
switch fsort := formula.Sort(); fsort {
case f.SortTrue, f.SortFalse:
return formula
case f.SortLiteral:
lit, ok := (*substitution)[f.Literal(formula)]
if ok {
return lit.AsFormula()
}
if formula.IsNeg() {
variable := f.Literal(formula).Variable()
lit, ok = (*substitution)[variable.AsLiteral()]
if ok {
return lit.Negate(fac).AsFormula()
}
}
return formula
case f.SortNot:
op, _ := fac.NotOperand(formula)
return fac.Not(SubstituteLiterals(fac, op, substitution))
case f.SortEquiv, f.SortImpl:
left, right, _ := fac.BinaryLeftRight(formula)
binOp, _ := fac.BinaryOperator(
fsort,
SubstituteLiterals(fac, left, substitution),
SubstituteLiterals(fac, right, substitution),
)
return binOp
case f.SortOr, f.SortAnd:
ops, _ := fac.NaryOperands(formula)
operands := make([]f.Formula, len(ops))
for i, op := range ops {
operands[i] = SubstituteLiterals(fac, op, substitution)
}
naryOp, _ := fac.NaryOperator(fsort, operands...)
return naryOp
case f.SortCC, f.SortPBC:
csort, rhs, lits, coeffs, _ := fac.PBCOps(formula)
literals := make([]f.Literal, len(lits))
for i, originalOp := range lits {
literals[i] = f.Literal(SubstituteLiterals(fac, originalOp.AsFormula(), substitution))
}
return fac.PBC(csort, rhs, literals, coeffs)
default:
panic(errorx.UnknownEnumValue(fsort))
}
}