/
VariablesFunction.java
89 lines (81 loc) · 2.82 KB
/
VariablesFunction.java
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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
package org.logicng.functions;
import static org.logicng.formulas.cache.FunctionCacheEntry.VARIABLES;
import org.logicng.formulas.BinaryOperator;
import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaFunction;
import org.logicng.formulas.Literal;
import org.logicng.formulas.NAryOperator;
import org.logicng.formulas.Not;
import org.logicng.formulas.PBConstraint;
import org.logicng.formulas.Variable;
import org.logicng.util.FormulaHelper;
import java.util.Collections;
import java.util.SortedSet;
import java.util.TreeSet;
/**
* A function that computes all variables occurring in a given formula.
* @version 2.2.0
* @since 2.2.0
*/
public class VariablesFunction implements FormulaFunction<SortedSet<Variable>> {
private final static VariablesFunction INSTANCE = new VariablesFunction();
/**
* Private empty constructor. Singleton class.
*/
private VariablesFunction() {
// Intentionally left empty
}
/**
* Returns the singleton of the function.
* @return the function instance
*/
public static VariablesFunction get() {
return INSTANCE;
}
@Override
public SortedSet<Variable> apply(final Formula formula, final boolean cache) {
final Object cached = formula.functionCacheEntry(VARIABLES);
if (cached != null) {
return (SortedSet<Variable>) cached;
}
SortedSet<Variable> result = new TreeSet<>();
switch (formula.type()) {
case FALSE:
case TRUE:
result = new TreeSet<>();
break;
case LITERAL:
final Literal lit = (Literal) formula;
result.add(lit.variable());
break;
case NOT:
final Not not = (Not) formula;
result = apply(not.operand(), cache);
break;
case IMPL:
case EQUIV:
final BinaryOperator binary = (BinaryOperator) formula;
result.addAll(apply(binary.left(), cache));
result.addAll(apply(binary.right(), cache));
break;
case OR:
case AND:
final NAryOperator nary = (NAryOperator) formula;
for (final Formula op : nary) {
result.addAll(apply(op, cache));
}
break;
case PBC:
final PBConstraint pbc = (PBConstraint) formula;
result = FormulaHelper.variables(pbc.literals());
break;
default:
throw new IllegalStateException("Unknown formula type " + formula.type());
}
result = Collections.unmodifiableSortedSet(result);
if (cache) {
formula.setFunctionCacheEntry(VARIABLES, result);
}
return result;
}
}