1 | /* This file is part of the project "Hilbert II" - http://www.qedeq.org |
2 | * |
3 | * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>. |
4 | * |
5 | * "Hilbert II" is free software; you can redistribute |
6 | * it and/or modify it under the terms of the GNU General Public |
7 | * License as published by the Free Software Foundation; either |
8 | * version 2 of the License, or (at your option) any later version. |
9 | * |
10 | * This program is distributed in the hope that it will be useful, |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
13 | * GNU General Public License for more details. |
14 | */ |
15 | |
16 | package org.qedeq.kernel.bo.service.heuristic; |
17 | |
18 | import org.qedeq.base.io.Parameters; |
19 | import org.qedeq.base.trace.Trace; |
20 | import org.qedeq.kernel.bo.log.QedeqLog; |
21 | import org.qedeq.kernel.bo.logic.common.Operators; |
22 | import org.qedeq.kernel.bo.logic.model.DynamicDirectInterpreter; |
23 | import org.qedeq.kernel.bo.logic.model.DynamicModel; |
24 | import org.qedeq.kernel.bo.logic.model.FourDynamicModel; |
25 | import org.qedeq.kernel.bo.logic.model.HeuristicErrorCodes; |
26 | import org.qedeq.kernel.bo.logic.model.HeuristicException; |
27 | import org.qedeq.kernel.bo.logic.model.ModelFunctionConstant; |
28 | import org.qedeq.kernel.bo.logic.model.ModelPredicateConstant; |
29 | import org.qedeq.kernel.bo.module.InternalModuleServiceCall; |
30 | import org.qedeq.kernel.bo.module.KernelQedeqBo; |
31 | import org.qedeq.kernel.bo.service.basis.ControlVisitor; |
32 | import org.qedeq.kernel.bo.service.basis.ModuleServicePlugin; |
33 | import org.qedeq.kernel.bo.service.basis.ModuleServicePluginExecutor; |
34 | import org.qedeq.kernel.se.base.list.Element; |
35 | import org.qedeq.kernel.se.base.module.Axiom; |
36 | import org.qedeq.kernel.se.base.module.ConditionalProof; |
37 | import org.qedeq.kernel.se.base.module.FormalProofLine; |
38 | import org.qedeq.kernel.se.base.module.FunctionDefinition; |
39 | import org.qedeq.kernel.se.base.module.InitialFunctionDefinition; |
40 | import org.qedeq.kernel.se.base.module.InitialPredicateDefinition; |
41 | import org.qedeq.kernel.se.base.module.Node; |
42 | import org.qedeq.kernel.se.base.module.PredicateDefinition; |
43 | import org.qedeq.kernel.se.base.module.Proposition; |
44 | import org.qedeq.kernel.se.base.module.Rule; |
45 | import org.qedeq.kernel.se.common.ModuleContext; |
46 | import org.qedeq.kernel.se.common.ModuleDataException; |
47 | import org.qedeq.kernel.se.common.ModuleService; |
48 | import org.qedeq.kernel.se.common.SourceFileExceptionList; |
49 | import org.qedeq.kernel.se.dto.list.DefaultElementList; |
50 | |
51 | |
52 | /** |
53 | * Check if formulas are valid in our model. |
54 | * |
55 | * @author Michael Meyling |
56 | */ |
57 | public final class DynamicHeuristicCheckerExecutor extends ControlVisitor implements ModuleServicePluginExecutor { |
58 | |
59 | /** This class. */ |
60 | private static final Class CLASS = DynamicHeuristicCheckerExecutor.class; |
61 | |
62 | /** Interpretation for variables. */ |
63 | private final DynamicDirectInterpreter interpreter; |
64 | |
65 | /** Current condition. */ |
66 | private DefaultElementList condition; |
67 | |
68 | /** |
69 | * Constructor. |
70 | * |
71 | * @param plugin This plugin we work for. |
72 | * @param qedeq QEDEQ module object. |
73 | * @param parameters Execution parameters. |
74 | */ |
75 | DynamicHeuristicCheckerExecutor(final ModuleServicePlugin plugin, final KernelQedeqBo qedeq, |
76 | final Parameters parameters) { |
77 | super(plugin, qedeq); |
78 | final String method = "DynamicHeuristicChecker(PluginBo, QedeqBo, Map)"; |
79 | final String modelClass = parameters.getString("model"); |
80 | DynamicModel model = null; |
81 | if (modelClass != null && modelClass.length() > 0) { |
82 | try { |
83 | Class cl = Class.forName(modelClass); |
84 | model = (DynamicModel) cl.newInstance(); |
85 | } catch (ClassNotFoundException e) { |
86 | Trace.fatal(CLASS, this, method, "Model class not in class path: " |
87 | + modelClass, e); |
88 | } catch (InstantiationException e) { |
89 | Trace.fatal(CLASS, this, method, "Model class could not be instanciated: " |
90 | + modelClass, e); |
91 | } catch (IllegalAccessException e) { |
92 | Trace.fatal(CLASS, this, method, |
93 | "Programming error, access for instantiation failed for model: " |
94 | + modelClass, e); |
95 | } catch (RuntimeException e) { |
96 | Trace.fatal(CLASS, this, method, |
97 | "Programming error, instantiation failed for model: " + modelClass, e); |
98 | } |
99 | } |
100 | // fallback is the default model |
101 | if (model == null) { |
102 | model = new FourDynamicModel(); |
103 | } |
104 | this.interpreter = new DynamicDirectInterpreter(qedeq, model); |
105 | } |
106 | |
107 | private ModuleService getPlugin() { |
108 | return (ModuleService) getService(); |
109 | } |
110 | |
111 | public Object executePlugin(final InternalModuleServiceCall call, final Object data) { |
112 | final String method = "executePlugin()"; |
113 | try { |
114 | QedeqLog.getInstance().logRequest("Dynamic heuristic test", getKernelQedeqBo().getUrl()); |
115 | // first we try to get more information about required modules and their predicates.. |
116 | try { |
117 | getServices().checkWellFormedness(call.getInternalServiceProcess(), getKernelQedeqBo()); |
118 | } catch (Exception e) { |
119 | // we continue and ignore external predicates |
120 | Trace.trace(CLASS, method, e); |
121 | } |
122 | condition = new DefaultElementList(Operators.CONJUNCTION_OPERATOR); |
123 | traverse(call.getInternalServiceProcess()); |
124 | QedeqLog.getInstance().logSuccessfulReply( |
125 | "Heuristic test succesfull", getKernelQedeqBo().getUrl()); |
126 | } catch (final SourceFileExceptionList e) { |
127 | final String msg = "Test failed"; |
128 | Trace.fatal(CLASS, this, method, msg, e); |
129 | QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(), e.getMessage()); |
130 | } catch (final RuntimeException e) { |
131 | Trace.fatal(CLASS, this, method, "unexpected problem", e); |
132 | QedeqLog.getInstance().logFailureReply( |
133 | "Test failed", getKernelQedeqBo().getUrl(), "unexpected problem: " |
134 | + (e.getMessage() != null ? e.getMessage() : e.toString())); |
135 | } finally { |
136 | getKernelQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList()); |
137 | } |
138 | return null; |
139 | } |
140 | |
141 | /** |
142 | * Check truth value in our model. If it is no tautology an warning is added. |
143 | * This also happens if our model doesn't support an operator found in the formula. |
144 | * |
145 | * @param test Test formula. |
146 | */ |
147 | private void test(final Element test) { |
148 | boolean useCondition = condition.size() > 0; //Assume that we start with an implication, |
149 | // but the real context begins after skipping ".getList().getElement(1)" |
150 | try { |
151 | Element toast = test; |
152 | if (condition.size() > 0) { |
153 | final DefaultElementList withCondition = new DefaultElementList(Operators.IMPLICATION_OPERATOR); |
154 | withCondition.add(condition); |
155 | withCondition.add(test); |
156 | toast = withCondition; |
157 | } |
158 | if (!isTautology(getCurrentContext(), toast)) { |
159 | addWarning(new HeuristicException(HeuristicErrorCodes.EVALUATED_NOT_TRUE_CODE, |
160 | HeuristicErrorCodes.EVALUATED_NOT_TRUE_TEXT + " (\"" |
161 | + interpreter.getModel().getName() + "\")", getCurrentContext())); |
162 | } |
163 | } catch (HeuristicException h) { |
164 | // TODO 20101015 m31: better exception handling would be better! |
165 | final String begin = getCurrentContext().getLocationWithinModule(); |
166 | // is the error context at the same location? if not we have a problem with a referenced |
167 | // predicate or function constant and we take the currrent context instead |
168 | if (!getCurrentContext().getModuleLocation().equals(h.getContext().getModuleLocation()) |
169 | || !h.getContext().getLocationWithinModule().startsWith(begin)) { |
170 | addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(), |
171 | getCurrentContext())); |
172 | } else { |
173 | String further = h.getContext().getLocationWithinModule().substring(begin.length()); |
174 | if (useCondition) { |
175 | if (further.startsWith(".getList().getElement(1)")) { |
176 | further = further.substring(".getList().getElement(1)".length()); |
177 | addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(), |
178 | new ModuleContext(h.getContext().getModuleLocation(), begin + further))); |
179 | } else { // must be an error in the condition and for that we have no context |
180 | addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(), |
181 | getCurrentContext())); |
182 | } |
183 | } else { |
184 | addWarning(h); |
185 | } |
186 | } |
187 | } catch (RuntimeException e) { |
188 | Trace.fatal(CLASS, this, "test(Element)", "unexpected runtime exception", e); |
189 | if (e.getCause() != null && e.getCause() instanceof HeuristicException) { |
190 | // TODO 20101015 m31: better exception handling would be better! |
191 | HeuristicException h = (HeuristicException) e.getCause(); |
192 | addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(), |
193 | getCurrentContext())); |
194 | } else { |
195 | addWarning(new HeuristicException(HeuristicErrorCodes.RUNTIME_EXCEPTION_CODE, |
196 | HeuristicErrorCodes.RUNTIME_EXCEPTION_TEXT + e, getCurrentContext())); |
197 | } |
198 | } |
199 | } |
200 | |
201 | /** |
202 | * Test if given formula is a tautology. This is done by checking a model and |
203 | * iterating through variable values. |
204 | * |
205 | * @param moduleContext Here we are within a module. |
206 | * @param formula Formula. |
207 | * @return Is this formula a tautology according to our tests. |
208 | * @throws HeuristicException Evaluation failed. |
209 | */ |
210 | private boolean isTautology(final ModuleContext moduleContext, final Element formula) |
211 | throws HeuristicException { |
212 | boolean result = true; |
213 | ModuleContext context = moduleContext; |
214 | try { |
215 | do { |
216 | result &= interpreter.calculateValue(new ModuleContext(context), formula); |
217 | // System.out.println(interpreter.toString()); |
218 | } while (result && interpreter.next()); |
219 | // if (!result) { |
220 | // System.out.println(interpreter); |
221 | // } |
222 | // System.out.println("interpretation finished - and result is = " + result); |
223 | } finally { |
224 | interpreter.clearVariables(); |
225 | } |
226 | return result; |
227 | } |
228 | |
229 | |
230 | public void visitEnter(final Axiom axiom) throws ModuleDataException { |
231 | if (axiom == null) { |
232 | return; |
233 | } |
234 | final String context = getCurrentContext().getLocationWithinModule(); |
235 | QedeqLog.getInstance().logMessageState("\ttesting axiom", getKernelQedeqBo().getUrl()); |
236 | if (axiom.getFormula() != null) { |
237 | setLocationWithinModule(context + ".getFormula().getElement()"); |
238 | final Element test = axiom.getFormula().getElement(); |
239 | test(test); |
240 | } |
241 | setLocationWithinModule(context); |
242 | setBlocked(true); |
243 | } |
244 | |
245 | public void visitLeave(final Axiom axiom) { |
246 | setBlocked(false); |
247 | } |
248 | |
249 | public void visitEnter(final InitialPredicateDefinition definition) |
250 | throws ModuleDataException { |
251 | final String method = "visitEnter(InitialPredicateDefinition)"; |
252 | if (definition == null) { |
253 | return; |
254 | } |
255 | QedeqLog.getInstance().logMessageState("\ttesting initial predicate definition", |
256 | getKernelQedeqBo().getUrl()); |
257 | final String context = getCurrentContext().getLocationWithinModule(); |
258 | try { |
259 | ModelPredicateConstant predicate = new ModelPredicateConstant( |
260 | definition.getName(), Integer.parseInt(definition |
261 | .getArgumentNumber())); |
262 | // check if model contains predicate |
263 | if (!interpreter.hasPredicateConstant(predicate)) { |
264 | setLocationWithinModule(context + ".getName()"); |
265 | addWarning(new HeuristicException( |
266 | HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE, |
267 | HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT |
268 | + predicate, getCurrentContext())); |
269 | } |
270 | } catch (NumberFormatException e) { |
271 | Trace.fatal(CLASS, this, method, "not suported argument number: " |
272 | + definition.getArgumentNumber(), e); |
273 | setLocationWithinModule(context + ".getArgumentNumber()"); |
274 | addWarning(new HeuristicException( |
275 | HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE, |
276 | HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT |
277 | + definition.getArgumentNumber(), |
278 | getCurrentContext())); |
279 | } |
280 | setLocationWithinModule(context); |
281 | setBlocked(true); |
282 | } |
283 | |
284 | public void visitLeave(final InitialPredicateDefinition definition) { |
285 | setBlocked(false); |
286 | } |
287 | |
288 | public void visitEnter(final PredicateDefinition definition) |
289 | throws ModuleDataException { |
290 | final String method = "visitEnter(PredicateDefinition)"; |
291 | if (definition == null) { |
292 | return; |
293 | } |
294 | QedeqLog.getInstance().logMessageState("\ttesting predicate definition", |
295 | getKernelQedeqBo().getUrl()); |
296 | final String context = getCurrentContext().getLocationWithinModule(); |
297 | try { |
298 | // test new predicate constant: must always be successful otherwise there |
299 | // must be a programming error or the predicate definition is not formal correct |
300 | setLocationWithinModule(context + ".getFormula().getElement()"); |
301 | test(definition.getFormula().getElement()); |
302 | } catch (NumberFormatException e) { |
303 | Trace.fatal(CLASS, this, method, "not suported argument number: " |
304 | + definition.getArgumentNumber(), e); |
305 | setLocationWithinModule(context + ".getArgumentNumber()"); |
306 | addWarning(new HeuristicException(HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE, |
307 | HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT + definition.getArgumentNumber(), |
308 | getCurrentContext())); |
309 | } |
310 | setLocationWithinModule(context); |
311 | setBlocked(true); |
312 | } |
313 | |
314 | public void visitLeave(final PredicateDefinition definition) { |
315 | setBlocked(false); |
316 | } |
317 | |
318 | public void visitEnter(final InitialFunctionDefinition definition) |
319 | throws ModuleDataException { |
320 | final String method = "visitEnter(InitialFunctionDefinition)"; |
321 | if (definition == null) { |
322 | return; |
323 | } |
324 | QedeqLog.getInstance().logMessageState("\ttesting initial function definition", |
325 | getKernelQedeqBo().getUrl()); |
326 | final String context = getCurrentContext().getLocationWithinModule(); |
327 | try { |
328 | ModelFunctionConstant function = new ModelFunctionConstant(definition.getName(), |
329 | Integer.parseInt(definition.getArgumentNumber())); |
330 | if (!interpreter.hasFunctionConstant(function)) { |
331 | // check if model contains predicate |
332 | setLocationWithinModule(context + ".getName()"); |
333 | addWarning(new HeuristicException( |
334 | HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE, |
335 | HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT |
336 | + function, getCurrentContext())); |
337 | } |
338 | } catch (NumberFormatException e) { |
339 | Trace.fatal(CLASS, this, method, "not suported argument number: " |
340 | + definition.getArgumentNumber(), e); |
341 | setLocationWithinModule(context + ".getArgumentNumber()"); |
342 | addWarning(new HeuristicException( |
343 | HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE, |
344 | HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT |
345 | + definition.getArgumentNumber(), |
346 | getCurrentContext())); |
347 | } |
348 | setLocationWithinModule(context); |
349 | setBlocked(true); |
350 | } |
351 | |
352 | public void visitLeave(final InitialFunctionDefinition definition) { |
353 | setBlocked(false); |
354 | } |
355 | |
356 | public void visitEnter(final FunctionDefinition definition) |
357 | throws ModuleDataException { |
358 | if (definition == null) { |
359 | return; |
360 | } |
361 | QedeqLog.getInstance().logMessageState("\ttesting function definition", |
362 | getKernelQedeqBo().getUrl()); |
363 | final String context = getCurrentContext().getLocationWithinModule(); |
364 | // test new predicate constant: must always be successful otherwise there |
365 | // must be a programming error or the predicate definition is not formal correct |
366 | setLocationWithinModule(context + ".getFormula().getElement()"); |
367 | test(definition.getFormula().getElement()); |
368 | setLocationWithinModule(context); |
369 | setBlocked(true); |
370 | } |
371 | |
372 | public void visitLeave(final FunctionDefinition definition) { |
373 | setBlocked(false); |
374 | } |
375 | |
376 | public void visitEnter(final Node node) { |
377 | QedeqLog.getInstance().logMessageState(super.getLocationDescription(), |
378 | getKernelQedeqBo().getUrl()); |
379 | } |
380 | |
381 | public void visitEnter(final Proposition proposition) |
382 | throws ModuleDataException { |
383 | if (proposition == null) { |
384 | return; |
385 | } |
386 | QedeqLog.getInstance().logMessageState("\ttesting proposition", getKernelQedeqBo().getUrl()); |
387 | final String context = getCurrentContext().getLocationWithinModule(); |
388 | if (proposition.getFormula() != null) { |
389 | setLocationWithinModule(context + ".getFormula().getElement()"); |
390 | final Element test = proposition.getFormula().getElement(); |
391 | test(test); |
392 | } |
393 | setLocationWithinModule(context); |
394 | } |
395 | |
396 | public void visitLeave(final Proposition definition) { |
397 | // nothing to do |
398 | } |
399 | |
400 | public void visitEnter(final FormalProofLine line) |
401 | throws ModuleDataException { |
402 | if (line == null) { |
403 | return; |
404 | } |
405 | QedeqLog.getInstance().logMessageState("\t\ttesting line " + line.getLabel(), |
406 | getKernelQedeqBo().getUrl()); |
407 | final String context = getCurrentContext().getLocationWithinModule(); |
408 | if (line.getFormula() != null) { |
409 | setLocationWithinModule(context + ".getFormula().getElement()"); |
410 | test(line.getFormula().getElement()); |
411 | } |
412 | setLocationWithinModule(context); |
413 | setBlocked(true); |
414 | } |
415 | |
416 | public void visitLeave(final FormalProofLine line) { |
417 | setBlocked(false); |
418 | } |
419 | |
420 | public void visitEnter(final ConditionalProof line) |
421 | throws ModuleDataException { |
422 | if (line == null) { |
423 | return; |
424 | } |
425 | // add hypothesis to list of conditions |
426 | if (line.getHypothesis() != null && line.getHypothesis().getFormula() != null |
427 | && line.getHypothesis().getFormula().getElement() != null) { |
428 | condition.add(line.getHypothesis().getFormula().getElement()); |
429 | QedeqLog.getInstance().logMessageState("\t\tadd condit. " |
430 | + line.getHypothesis().getLabel(), getKernelQedeqBo().getUrl()); |
431 | } |
432 | } |
433 | |
434 | public void visitLeave(final ConditionalProof line) { |
435 | if (line == null) { |
436 | return; |
437 | } |
438 | // remove hypothesis of list of conditions |
439 | if (line.getHypothesis() != null && line.getHypothesis().getFormula() != null |
440 | && line.getHypothesis().getFormula().getElement() != null) { |
441 | condition.remove(condition.size() - 1); |
442 | } |
443 | QedeqLog.getInstance().logMessageState("\t\ttesting line " |
444 | + line.getConclusion().getLabel(), getKernelQedeqBo().getUrl()); |
445 | final String context = getCurrentContext().getLocationWithinModule(); |
446 | if (line.getConclusion().getFormula() != null) { |
447 | setLocationWithinModule(context + ".getConclusion().getFormula().getElement()"); |
448 | final Element test = line.getConclusion().getFormula().getElement(); |
449 | test(test); |
450 | } |
451 | } |
452 | |
453 | public void visitEnter(final Rule rule) throws ModuleDataException { |
454 | setBlocked(true); |
455 | } |
456 | |
457 | public void visitLeave(final Rule rule) { |
458 | setBlocked(false); |
459 | } |
460 | |
461 | public String getLocationDescription() { |
462 | return super.getLocationDescription() + "\n" + interpreter.toString(); |
463 | } |
464 | |
465 | } |