1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
package org.qedeq.kernel.bo.logic.proof.finder; |
16 |
|
|
17 |
|
import java.io.File; |
18 |
|
import java.io.IOException; |
19 |
|
import java.io.OutputStream; |
20 |
|
import java.io.PrintStream; |
21 |
|
import java.util.HashMap; |
22 |
|
import java.util.Map; |
23 |
|
|
24 |
|
import org.qedeq.base.io.Parameters; |
25 |
|
import org.qedeq.kernel.bo.KernelContext; |
26 |
|
import org.qedeq.kernel.bo.log.ModuleLogListenerImpl; |
27 |
|
import org.qedeq.kernel.bo.logic.proof.common.ProofFinder; |
28 |
|
import org.qedeq.kernel.bo.logic.proof.common.ProofFoundException; |
29 |
|
import org.qedeq.kernel.bo.logic.proof.common.ProofNotFoundException; |
30 |
|
import org.qedeq.kernel.bo.module.KernelNodeBo; |
31 |
|
import org.qedeq.kernel.bo.module.KernelQedeqBo; |
32 |
|
import org.qedeq.kernel.bo.test.QedeqBoTestCase; |
33 |
|
import org.qedeq.kernel.se.base.module.FormalProofLineList; |
34 |
|
import org.qedeq.kernel.se.base.module.Proposition; |
35 |
|
import org.qedeq.kernel.se.common.DefaultModuleAddress; |
36 |
|
import org.qedeq.kernel.se.common.ModuleAddress; |
37 |
|
import org.qedeq.kernel.se.dto.module.FormalProofLineListVo; |
38 |
|
|
39 |
|
|
40 |
|
|
41 |
|
|
42 |
|
@author |
43 |
|
|
|
|
| 96.1% |
Uncovered Elements: 4 (102) |
Complexity: 13 |
Complexity Density: 0.14 |
|
44 |
|
public class ProofFinderImplTest extends QedeqBoTestCase { |
45 |
|
|
46 |
|
|
47 |
|
|
48 |
|
|
49 |
|
@throws |
50 |
|
|
|
|
| 96.9% |
Uncovered Elements: 1 (32) |
Complexity: 3 |
Complexity Density: 0.1 |
1
PASS
|
|
51 |
1
|
public void testFind() throws Exception {... |
52 |
1
|
final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(), |
53 |
|
"sample/qedeq_sample3.xml")); |
54 |
1
|
KernelContext.getInstance().checkWellFormedness(address); |
55 |
1
|
final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address); |
56 |
1
|
assertTrue(bo.isWellFormed()); |
57 |
1
|
assertNotNull(bo.getWarnings()); |
58 |
1
|
assertEquals(0, bo.getWarnings().size()); |
59 |
1
|
assertEquals(0, bo.getErrors().size()); |
60 |
1
|
final KernelNodeBo node = bo.getLabels().getNode("proposition:one"); |
61 |
1
|
final Proposition prop = node.getNodeVo().getNodeType().getProposition(); |
62 |
1
|
final ProofFinder finder = new ProofFinderImpl(); |
63 |
1
|
final FormalProofLineList original = prop.getFormalProofList().get(0) |
64 |
|
.getFormalProofLineList(); |
65 |
1
|
final FormalProofLineListVo list = new FormalProofLineListVo(); |
66 |
5
|
for (int i = 0; i < 4; i++) { |
67 |
4
|
list.add(original.get(i)); |
68 |
|
} |
69 |
1
|
final Map parameters = new HashMap(); |
70 |
1
|
parameters.put("extraVars", "0"); |
71 |
1
|
parameters.put("maximumProofLines", "100000"); |
72 |
1
|
parameters.put("propositionVariableOrder", "2"); |
73 |
1
|
parameters.put("propositionVariableWeight", "3"); |
74 |
1
|
parameters.put("partFormulaWeight", "0"); |
75 |
1
|
parameters.put("disjunctionOrder", "1"); |
76 |
1
|
parameters.put("disjunctionWeight", "3"); |
77 |
1
|
parameters.put("implicationWeight", "0"); |
78 |
1
|
parameters.put("negationWeight", "0"); |
79 |
1
|
parameters.put("conjunctionWeight", "0"); |
80 |
1
|
parameters.put("equivalenceWeight", "0"); |
81 |
1
|
try { |
82 |
1
|
finder.findProof(prop.getFormula().getElement(), list, |
83 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), new Parameters(parameters), |
84 |
|
new ModuleLogListenerImpl("memory", new PrintStream(new OutputStream() { |
|
|
| - |
Uncovered Elements: 0 (0) |
Complexity: 1 |
Complexity Density: - |
|
85 |
2339
|
public void write(int b) throws IOException {... |
86 |
|
}})), bo.getElement2Utf8()); |
87 |
0
|
fail("no proof found"); |
88 |
|
} catch (ProofFoundException e) { |
89 |
1
|
assertNotNull(e.getProofLines()); |
90 |
|
} |
91 |
|
} |
92 |
|
|
93 |
|
|
94 |
|
|
95 |
|
|
96 |
|
@throws |
97 |
|
|
|
|
| 96.9% |
Uncovered Elements: 1 (32) |
Complexity: 3 |
Complexity Density: 0.1 |
1
PASS
|
|
98 |
1
|
public void testFind2() throws Exception {... |
99 |
1
|
final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(), |
100 |
|
"sample/qedeq_sample3.xml")); |
101 |
1
|
KernelContext.getInstance().checkWellFormedness(address); |
102 |
1
|
final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address); |
103 |
1
|
assertTrue(bo.isWellFormed()); |
104 |
1
|
assertNotNull(bo.getWarnings()); |
105 |
1
|
assertEquals(0, bo.getWarnings().size()); |
106 |
1
|
assertEquals(0, bo.getErrors().size()); |
107 |
1
|
final KernelNodeBo node = bo.getLabels().getNode("proposition:two"); |
108 |
1
|
final Proposition prop = node.getNodeVo().getNodeType().getProposition(); |
109 |
1
|
final ProofFinder finder = new ProofFinderImpl(); |
110 |
1
|
final FormalProofLineList original = prop.getFormalProofList().get(0) |
111 |
|
.getFormalProofLineList(); |
112 |
1
|
final FormalProofLineListVo list = new FormalProofLineListVo(); |
113 |
4
|
for (int i = 0; i < 3; i++) { |
114 |
3
|
list.add(original.get(i)); |
115 |
|
} |
116 |
1
|
final Map parameters = new HashMap(); |
117 |
1
|
parameters.put("extraVars", "0"); |
118 |
1
|
parameters.put("maximumProofLines", "100000"); |
119 |
1
|
parameters.put("propositionVariableOrder", "2"); |
120 |
1
|
parameters.put("propositionVariableWeight", "3"); |
121 |
1
|
parameters.put("partFormulaWeight", "0"); |
122 |
1
|
parameters.put("disjunctionOrder", "1"); |
123 |
1
|
parameters.put("disjunctionWeight", "3"); |
124 |
1
|
parameters.put("implicationWeight", "0"); |
125 |
1
|
parameters.put("negationWeight", "0"); |
126 |
1
|
parameters.put("conjunctionWeight", "0"); |
127 |
1
|
parameters.put("equivalenceWeight", "0"); |
128 |
1
|
try { |
129 |
1
|
finder.findProof(prop.getFormula().getElement(), list, |
130 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), new Parameters(parameters), |
131 |
|
new ModuleLogListenerImpl("memory", new PrintStream(new OutputStream() { |
|
|
| - |
Uncovered Elements: 0 (0) |
Complexity: 1 |
Complexity Density: - |
|
132 |
2281
|
public void write(int b) throws IOException {... |
133 |
|
}})), bo.getElement2Utf8()); |
134 |
0
|
fail("no proof found"); |
135 |
|
} catch (ProofFoundException e) { |
136 |
1
|
assertNotNull(e.getProofLines()); |
137 |
|
} |
138 |
|
} |
139 |
|
|
140 |
|
|
141 |
|
|
142 |
|
|
143 |
|
@throws |
144 |
|
|
|
|
| 93.8% |
Uncovered Elements: 2 (32) |
Complexity: 4 |
Complexity Density: 0.13 |
1
PASS
|
|
145 |
1
|
public void testFind3() throws Exception {... |
146 |
1
|
final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(), |
147 |
|
"sample/qedeq_sample3.xml")); |
148 |
1
|
KernelContext.getInstance().checkWellFormedness(address); |
149 |
1
|
final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address); |
150 |
1
|
assertTrue(bo.isWellFormed()); |
151 |
1
|
assertNotNull(bo.getWarnings()); |
152 |
1
|
assertEquals(0, bo.getWarnings().size()); |
153 |
1
|
assertEquals(0, bo.getErrors().size()); |
154 |
1
|
final KernelNodeBo node = bo.getLabels().getNode("proposition:one"); |
155 |
1
|
final Proposition prop = node.getNodeVo().getNodeType().getProposition(); |
156 |
1
|
final ProofFinder finder = new ProofFinderImpl(); |
157 |
1
|
final FormalProofLineList original = prop.getFormalProofList().get(0) |
158 |
|
.getFormalProofLineList(); |
159 |
1
|
final FormalProofLineListVo list = new FormalProofLineListVo(); |
160 |
5
|
for (int i = 0; i < 4; i++) { |
161 |
4
|
list.add(original.get(i)); |
162 |
|
} |
163 |
1
|
final Map parameters = new HashMap(); |
164 |
1
|
parameters.put("extraVars", "0"); |
165 |
1
|
parameters.put("maximumProofLines", "10"); |
166 |
1
|
parameters.put("propositionVariableOrder", "2"); |
167 |
1
|
parameters.put("propositionVariableWeight", "3"); |
168 |
1
|
parameters.put("partFormulaWeight", "0"); |
169 |
1
|
parameters.put("disjunctionOrder", "1"); |
170 |
1
|
parameters.put("disjunctionWeight", "3"); |
171 |
1
|
parameters.put("implicationWeight", "0"); |
172 |
1
|
parameters.put("negationWeight", "0"); |
173 |
1
|
parameters.put("conjunctionWeight", "0"); |
174 |
1
|
parameters.put("equivalenceWeight", "0"); |
175 |
1
|
try { |
176 |
1
|
finder.findProof(prop.getFormula().getElement(), list, |
177 |
|
DefaultModuleAddress.MEMORY.createModuleContext(), new Parameters(parameters), |
178 |
|
new ModuleLogListenerImpl("memory", new PrintStream(new OutputStream() { |
|
|
| - |
Uncovered Elements: 0 (0) |
Complexity: 1 |
Complexity Density: - |
|
179 |
562
|
public void write(int b) throws IOException {... |
180 |
|
}})), bo.getElement2Utf8()); |
181 |
0
|
fail("no proof found"); |
182 |
|
} catch (ProofFoundException e) { |
183 |
0
|
fail("should not find a proof"); |
184 |
|
} catch (ProofNotFoundException e) { |
185 |
|
|
186 |
|
} |
187 |
|
} |
188 |
|
|
189 |
|
} |