1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
package org.qedeq.kernel.bo.logic.proof.finder; |
17 |
|
|
18 |
|
import java.util.ArrayList; |
19 |
|
import java.util.List; |
20 |
|
|
21 |
|
import org.qedeq.kernel.bo.common.Element2Utf8; |
22 |
|
import org.qedeq.kernel.bo.log.ModuleLogListener; |
23 |
|
import org.qedeq.kernel.se.base.list.Element; |
24 |
|
import org.qedeq.kernel.se.base.module.Add; |
25 |
|
import org.qedeq.kernel.se.base.module.FormalProofLineList; |
26 |
|
import org.qedeq.kernel.se.base.module.Reason; |
27 |
|
import org.qedeq.kernel.se.base.module.SubstPred; |
28 |
|
import org.qedeq.kernel.se.dto.module.AddVo; |
29 |
|
import org.qedeq.kernel.se.dto.module.FormalProofLineListVo; |
30 |
|
import org.qedeq.kernel.se.dto.module.FormalProofLineVo; |
31 |
|
import org.qedeq.kernel.se.dto.module.FormulaVo; |
32 |
|
import org.qedeq.kernel.se.dto.module.ModusPonensVo; |
33 |
|
import org.qedeq.kernel.se.dto.module.SubstPredVo; |
34 |
|
|
35 |
|
|
36 |
|
|
37 |
|
|
38 |
|
|
39 |
|
@author |
40 |
|
|
|
|
| 92.7% |
Uncovered Elements: 8 (109) |
Complexity: 24 |
Complexity Density: 0.35 |
|
41 |
|
public final class ProofFinderUtility { |
42 |
|
|
43 |
|
|
44 |
|
private List new2Old; |
45 |
|
|
46 |
|
|
47 |
|
|
48 |
|
|
49 |
|
|
|
|
| - |
Uncovered Elements: 0 (0) |
Complexity: 1 |
Complexity Density: - |
|
50 |
8
|
private ProofFinderUtility() {... |
51 |
|
|
52 |
|
} |
53 |
|
|
54 |
|
|
55 |
|
|
56 |
|
|
57 |
|
@param |
58 |
|
@param |
59 |
|
@param |
60 |
|
@param |
61 |
|
@return |
62 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
63 |
8
|
public static FormalProofLineList shortenProof(final List lines, final List reasons,... |
64 |
|
final ModuleLogListener log, final Element2Utf8 trans) { |
65 |
8
|
return (new ProofFinderUtility()).shorten(lines, reasons, log, trans); |
66 |
|
} |
67 |
|
|
|
|
| 94.3% |
Uncovered Elements: 4 (70) |
Complexity: 15 |
Complexity Density: 0.36 |
|
68 |
8
|
private FormalProofLineList shorten(final List lines, final List reasons,... |
69 |
|
final ModuleLogListener log, final Element2Utf8 trans) { |
70 |
8
|
final boolean[] used = new boolean[lines.size()]; |
71 |
8
|
int n = lines.size() - 1; |
72 |
8
|
used[n] = true; |
73 |
45109
|
while (n >= 0) { |
74 |
45101
|
if (used[n]) { |
75 |
68
|
Reason r = (Reason) reasons.get(n); |
76 |
68
|
if (r instanceof ModusPonensBo) { |
77 |
16
|
final ModusPonensBo mp = (ModusPonensBo) reasons.get(n); |
78 |
16
|
used[mp.getN1()] = true; |
79 |
16
|
used[mp.getN2()] = true; |
80 |
52
|
} else if (r instanceof SubstPredBo) { |
81 |
28
|
final SubstPredBo substPred = (SubstPredBo) reasons.get(n); |
82 |
28
|
used[substPred.getN()] = true; |
83 |
24
|
} else if (r instanceof Add) { |
84 |
|
|
85 |
|
} else { |
86 |
0
|
throw new IllegalStateException("unexpected reason class: " + r.getClass()); |
87 |
|
} |
88 |
|
} |
89 |
45101
|
n--; |
90 |
|
} |
91 |
45109
|
for (int j = 0; j < lines.size(); j++) { |
92 |
45101
|
if (used[j]) { |
93 |
68
|
log.logMessageState(getUtf8Line(lines, reasons, j, trans)); |
94 |
|
} |
95 |
|
} |
96 |
8
|
new2Old = new ArrayList(); |
97 |
45109
|
for (int j = 0; j < lines.size(); j++) { |
98 |
45101
|
if (used[j]) { |
99 |
68
|
new2Old.add(new Integer(j)); |
100 |
|
} |
101 |
|
} |
102 |
8
|
final FormalProofLineListVo result = new FormalProofLineListVo(); |
103 |
76
|
for (int j = 0; j < new2Old.size(); j++) { |
104 |
68
|
n = ((Integer) new2Old.get(j)).intValue(); |
105 |
68
|
final Reason r = (Reason) reasons.get(n); |
106 |
68
|
final Reason newReason; |
107 |
68
|
if (r instanceof ModusPonensBo) { |
108 |
16
|
final ModusPonensBo mp = (ModusPonensBo) reasons.get(n); |
109 |
16
|
newReason = new ModusPonensVo("" + (1 + old2new(mp.getN1())), |
110 |
|
"" + (1 + old2new(mp.getN2()))); |
111 |
52
|
} else if (r instanceof SubstPredBo) { |
112 |
28
|
final SubstPredBo substPred = (SubstPredBo) reasons.get(n); |
113 |
28
|
newReason = new SubstPredVo("" + (1 + old2new(substPred.getN())), |
114 |
|
substPred.getPredicateVariable(), substPred.getSubstituteFormula()); |
115 |
24
|
} else if (r instanceof Add) { |
116 |
24
|
final Add add = (Add) reasons.get(n); |
117 |
24
|
newReason = new AddVo(add.getReference()); |
118 |
|
} else { |
119 |
0
|
throw new IllegalStateException("unexpected reason class: " + r.getClass()); |
120 |
|
} |
121 |
68
|
result.add(new FormalProofLineVo("" + (1 + j), |
122 |
|
new FormulaVo((Element) lines.get(new2old(j))), |
123 |
|
newReason)); |
124 |
|
} |
125 |
76
|
for (int j = 0; j < result.size(); j++) { |
126 |
68
|
log.logMessageState(result.get(j).getLabel() + ": " |
127 |
|
+ trans.getUtf8(result.get(j).getFormula().getElement()) |
128 |
|
+ " " + result.get(j).getReason()); |
129 |
|
} |
130 |
8
|
return result; |
131 |
|
} |
132 |
|
|
|
|
| 66.7% |
Uncovered Elements: 2 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
133 |
60
|
private int old2new(final int old) {... |
134 |
60
|
int result = new2Old.indexOf(new Integer(old)); |
135 |
60
|
if (result < 0) { |
136 |
0
|
throw new IllegalArgumentException("not found: " + old); |
137 |
|
} |
138 |
60
|
return result; |
139 |
|
} |
140 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (2) |
Complexity: 1 |
Complexity Density: 0.5 |
|
141 |
68
|
private int new2old(final int n) {... |
142 |
68
|
final int result = ((Integer) new2Old.get(n)).intValue(); |
143 |
68
|
return result; |
144 |
|
} |
145 |
|
|
146 |
|
|
147 |
|
|
148 |
|
|
149 |
|
@param |
150 |
|
@param |
151 |
|
@param |
152 |
|
@param |
153 |
|
@return |
154 |
|
|
|
|
| 77.8% |
Uncovered Elements: 2 (9) |
Complexity: 2 |
Complexity Density: 0.29 |
|
155 |
101
|
public static String getUtf8Line(final List lines, final List reasons, final int i,... |
156 |
|
final Element2Utf8 trans) { |
157 |
101
|
if (i < 0) { |
158 |
0
|
return "beginning to prove"; |
159 |
|
} |
160 |
101
|
final StringBuffer result = new StringBuffer(); |
161 |
101
|
result.append((i + 1) + ": "); |
162 |
101
|
Reason reason = (Reason) reasons.get(i); |
163 |
101
|
Element formula = (Element) lines.get(i); |
164 |
101
|
return getUtf8Line(formula, reason, i, trans); |
165 |
|
} |
166 |
|
|
167 |
|
|
168 |
|
|
169 |
|
|
170 |
|
@param |
171 |
|
@param |
172 |
|
@param |
173 |
|
@param |
174 |
|
@return |
175 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (14) |
Complexity: 2 |
Complexity Density: 0.17 |
|
176 |
138
|
public static String getUtf8Line(final Element formula, final Reason reason, final int i,... |
177 |
|
final Element2Utf8 trans) { |
178 |
138
|
final StringBuffer result = new StringBuffer(); |
179 |
138
|
result.append((i + 1) + ": "); |
180 |
138
|
result.append(trans.getUtf8(formula)); |
181 |
138
|
result.append(" : "); |
182 |
138
|
if (reason instanceof SubstPred) { |
183 |
61
|
SubstPred s = (SubstPred) reason; |
184 |
61
|
result.append("Subst " + s.getReference() + " "); |
185 |
61
|
result.append(trans.getUtf8(s.getPredicateVariable())); |
186 |
61
|
result.append(" by "); |
187 |
61
|
result.append(trans.getUtf8(s.getSubstituteFormula())); |
188 |
|
} else { |
189 |
77
|
result.append(reason); |
190 |
|
} |
191 |
138
|
return result.toString(); |
192 |
|
} |
193 |
|
|
194 |
|
} |