001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.service.heuristic;
017
018 import java.util.Map;
019
020 import org.qedeq.base.io.IoUtility;
021 import org.qedeq.base.trace.Trace;
022 import org.qedeq.kernel.bo.common.PluginExecutor;
023 import org.qedeq.kernel.bo.log.QedeqLog;
024 import org.qedeq.kernel.bo.logic.model.DynamicDirectInterpreter;
025 import org.qedeq.kernel.bo.logic.model.DynamicModel;
026 import org.qedeq.kernel.bo.logic.model.FourDynamicModel;
027 import org.qedeq.kernel.bo.logic.model.HeuristicErrorCodes;
028 import org.qedeq.kernel.bo.logic.model.HeuristicException;
029 import org.qedeq.kernel.bo.logic.model.ModelFunctionConstant;
030 import org.qedeq.kernel.bo.logic.model.ModelPredicateConstant;
031 import org.qedeq.kernel.bo.module.ControlVisitor;
032 import org.qedeq.kernel.bo.module.KernelQedeqBo;
033 import org.qedeq.kernel.bo.module.PluginBo;
034 import org.qedeq.kernel.se.base.list.Element;
035 import org.qedeq.kernel.se.base.module.Axiom;
036 import org.qedeq.kernel.se.base.module.FormalProofLine;
037 import org.qedeq.kernel.se.base.module.FunctionDefinition;
038 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
039 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
040 import org.qedeq.kernel.se.base.module.Latex;
041 import org.qedeq.kernel.se.base.module.LatexList;
042 import org.qedeq.kernel.se.base.module.Node;
043 import org.qedeq.kernel.se.base.module.PredicateDefinition;
044 import org.qedeq.kernel.se.base.module.Proposition;
045 import org.qedeq.kernel.se.base.module.Rule;
046 import org.qedeq.kernel.se.common.ModuleContext;
047 import org.qedeq.kernel.se.common.ModuleDataException;
048 import org.qedeq.kernel.se.common.SourceFileExceptionList;
049
050
051 /**
052 * Check if formulas are valid in our model.
053 *
054 * @author Michael Meyling
055 */
056 public final class DynamicHeuristicCheckerExecutor extends ControlVisitor implements PluginExecutor {
057
058 /** This class. */
059 private static final Class CLASS = DynamicHeuristicCheckerExecutor.class;
060
061 /** Interpretation for variables. */
062 private final DynamicDirectInterpreter interpreter;
063
064 /**
065 * Constructor.
066 *
067 * @param plugin This plugin we work for.
068 * @param qedeq QEDEQ module object.
069 * @param parameters Execution parameters.
070 */
071 DynamicHeuristicCheckerExecutor(final PluginBo plugin, final KernelQedeqBo qedeq,
072 final Map parameters) {
073 super(plugin, qedeq);
074 final String method = "DynamicHeuristicChecker(PluginBo, QedeqBo, Map)";
075 final String modelClass
076 = (parameters != null ? (String) parameters.get("model") : null);
077 DynamicModel model = null;
078 if (modelClass != null && modelClass.length() > 0) {
079 try {
080 Class cl = Class.forName(modelClass);
081 model = (DynamicModel) cl.newInstance();
082 } catch (ClassNotFoundException e) {
083 Trace.fatal(CLASS, this, method, "Model class not in class path: "
084 + modelClass, e);
085 } catch (InstantiationException e) {
086 Trace.fatal(CLASS, this, method, "Model class could not be instanciated: "
087 + modelClass, e);
088 } catch (IllegalAccessException e) {
089 Trace.fatal(CLASS, this, method,
090 "Programming error, access for instantiation failed for model: "
091 + modelClass, e);
092 } catch (RuntimeException e) {
093 Trace.fatal(CLASS, this, method,
094 "Programming error, instantiation failed for model: " + modelClass, e);
095 }
096 }
097 // fallback is the default model
098 if (model == null) {
099 model = new FourDynamicModel();
100 }
101 this.interpreter = new DynamicDirectInterpreter(qedeq, model);
102 }
103
104 public Object executePlugin() {
105 final String method = "executePlugin()";
106 final String ref = "\"" + IoUtility.easyUrl(getQedeqBo().getUrl()) + "\"";
107 try {
108 QedeqLog.getInstance().logRequest("Dynamic heuristic test for " + ref);
109 // first we try to get more information about required modules and their predicates..
110 try {
111 getServices().checkModule(getQedeqBo().getModuleAddress());
112 } catch (Exception e) {
113 // we continue and ignore external predicates
114 Trace.trace(CLASS, method, e);
115 }
116 traverse();
117 QedeqLog.getInstance().logSuccessfulReply(
118 "Heuristic test succesfull for " + ref);
119 } catch (final SourceFileExceptionList e) {
120 final String msg = "Test failed for " + ref;
121 Trace.fatal(CLASS, this, method, msg, e);
122 QedeqLog.getInstance().logFailureReply(msg, e.getMessage());
123 } catch (final RuntimeException e) {
124 Trace.fatal(CLASS, this, method, "unexpected problem", e);
125 QedeqLog.getInstance().logFailureReply(
126 "Test failed for " + ref, "unexpected problem: "
127 + (e.getMessage() != null ? e.getMessage() : e.toString()));
128 } finally {
129 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
130 }
131 return null;
132 }
133
134 /**
135 * Check truth value in our model. If it is no tautology an warning is added.
136 * This also happens if our model doesn't support an operator found in the formula.
137 *
138 * @param test Test formula.
139 */
140 private void test(final Element test) {
141 try {
142 if (!isTautology(getCurrentContext(), test)) {
143 addWarning(new HeuristicException(HeuristicErrorCodes.EVALUATED_NOT_TRUE_CODE,
144 HeuristicErrorCodes.EVALUATED_NOT_TRUE_TEXT + " (\""
145 + interpreter.getModel().getName() + "\")", getCurrentContext()));
146 }
147 } catch (HeuristicException h) {
148 // TODO 20101015 m31: better exception handling would be better!
149 if (getCurrentContext().getModuleLocation().equals(h.getContext().getModuleLocation())) {
150 addWarning(h);
151 } else {
152 addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(),
153 getCurrentContext()));
154 }
155 } catch (RuntimeException e) {
156 Trace.fatal(CLASS, this, "test(Element)", "unexpected runtime exception", e);
157 if (e.getCause() != null && e.getCause() instanceof HeuristicException) {
158 // TODO 20101015 m31: better exception handling would be better!
159 HeuristicException h = (HeuristicException) e.getCause();
160 addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(),
161 getCurrentContext()));
162 } else {
163 addWarning(new HeuristicException(HeuristicErrorCodes.RUNTIME_EXCEPTION_CODE,
164 HeuristicErrorCodes.RUNTIME_EXCEPTION_TEXT + e, getCurrentContext()));
165 }
166 }
167 }
168
169 /**
170 * Test if given formula is a tautology. This is done by checking a model and
171 * iterating through variable values.
172 *
173 * @param moduleContext Here we are within a module.
174 * @param formula Formula.
175 * @return Is this formula a tautology according to our tests.
176 * @throws HeuristicException Evaluation failed.
177 */
178 private boolean isTautology(final ModuleContext moduleContext, final Element formula)
179 throws HeuristicException {
180 boolean result = true;
181 ModuleContext context = moduleContext;
182 try {
183 do {
184 result &= interpreter.calculateValue(new ModuleContext(context), formula);
185 // System.out.println(interpreter.toString());
186 } while (result && interpreter.next());
187 // if (!result) {
188 // System.out.println(interpreter);
189 // }
190 // System.out.println("interpretation finished - and result is = " + result);
191 } finally {
192 interpreter.clearVariables();
193 }
194 return result;
195 }
196
197
198 public void visitEnter(final Axiom axiom) throws ModuleDataException {
199 if (axiom == null) {
200 return;
201 }
202 final String context = getCurrentContext().getLocationWithinModule();
203 System.out.println("\ttesting axiom");
204 if (axiom.getFormula() != null) {
205 setLocationWithinModule(context + ".getFormula().getElement()");
206 final Element test = axiom.getFormula().getElement();
207 test(test);
208 }
209 setLocationWithinModule(context);
210 setBlocked(true);
211 }
212
213 public void visitLeave(final Axiom axiom) {
214 setBlocked(false);
215 }
216
217 public void visitEnter(final InitialPredicateDefinition definition)
218 throws ModuleDataException {
219 final String method = "visitEnter(InitialPredicateDefinition)";
220 if (definition == null) {
221 return;
222 }
223 System.out.println("\ttesting initial predicate definition");
224 final String context = getCurrentContext().getLocationWithinModule();
225 try {
226 ModelPredicateConstant predicate = new ModelPredicateConstant(
227 definition.getName(), Integer.parseInt(definition
228 .getArgumentNumber()));
229 // check if model contains predicate
230 if (!interpreter.hasPredicateConstant(predicate)) {
231 setLocationWithinModule(context + ".getName()");
232 addWarning(new HeuristicException(
233 HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE,
234 HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT
235 + predicate, getCurrentContext()));
236 }
237 } catch (NumberFormatException e) {
238 Trace.fatal(CLASS, this, method, "not suported argument number: "
239 + definition.getArgumentNumber(), e);
240 setLocationWithinModule(context + ".getArgumentNumber()");
241 addWarning(new HeuristicException(
242 HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE,
243 HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT
244 + definition.getArgumentNumber(),
245 getCurrentContext()));
246 }
247 setLocationWithinModule(context);
248 setBlocked(true);
249 }
250
251 public void visitLeave(final InitialPredicateDefinition definition) {
252 setBlocked(false);
253 }
254
255 public void visitEnter(final PredicateDefinition definition)
256 throws ModuleDataException {
257 final String method = "visitEnter(PredicateDefinition)";
258 if (definition == null) {
259 return;
260 }
261 System.out.println("\ttesting predicate definition");
262 final String context = getCurrentContext().getLocationWithinModule();
263 try {
264 // test new predicate constant: must always be successful otherwise there
265 // must be a programming error or the predicate definition is not formal correct
266 setLocationWithinModule(context + ".getFormula().getElement()");
267 test(definition.getFormula().getElement());
268 } catch (NumberFormatException e) {
269 Trace.fatal(CLASS, this, method, "not suported argument number: "
270 + definition.getArgumentNumber(), e);
271 setLocationWithinModule(context + ".getArgumentNumber()");
272 addWarning(new HeuristicException(HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE,
273 HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT + definition.getArgumentNumber(),
274 getCurrentContext()));
275 }
276 setLocationWithinModule(context);
277 setBlocked(true);
278 }
279
280 public void visitLeave(final PredicateDefinition definition) {
281 setBlocked(false);
282 }
283
284 public void visitEnter(final InitialFunctionDefinition definition)
285 throws ModuleDataException {
286 final String method = "visitEnter(InitialFunctionDefinition)";
287 if (definition == null) {
288 return;
289 }
290 System.out.println("\ttesting initial function definition");
291 final String context = getCurrentContext().getLocationWithinModule();
292 try {
293 ModelFunctionConstant function = new ModelFunctionConstant(definition.getName(),
294 Integer.parseInt(definition.getArgumentNumber()));
295 if (!interpreter.hasFunctionConstant(function)) {
296 // check if model contains predicate
297 setLocationWithinModule(context + ".getName()");
298 addWarning(new HeuristicException(
299 HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE,
300 HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT
301 + function, getCurrentContext()));
302 }
303 } catch (NumberFormatException e) {
304 Trace.fatal(CLASS, this, method, "not suported argument number: "
305 + definition.getArgumentNumber(), e);
306 setLocationWithinModule(context + ".getArgumentNumber()");
307 addWarning(new HeuristicException(
308 HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE,
309 HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT
310 + definition.getArgumentNumber(),
311 getCurrentContext()));
312 }
313 setLocationWithinModule(context);
314 setBlocked(true);
315 }
316
317 public void visitLeave(final InitialFunctionDefinition definition) {
318 setBlocked(false);
319 }
320
321 public void visitEnter(final FunctionDefinition definition)
322 throws ModuleDataException {
323 final String method = "visitEnter(FunctionDefinition)";
324 if (definition == null) {
325 return;
326 }
327 System.out.println("\ttesting function definition");
328 final String context = getCurrentContext().getLocationWithinModule();
329 // test new predicate constant: must always be successful otherwise there
330 // must be a programming error or the predicate definition is not formal correct
331 setLocationWithinModule(context + ".getFormula().getElement()");
332 test(definition.getFormula().getElement());
333 setLocationWithinModule(context);
334 setBlocked(true);
335 }
336
337 public void visitLeave(final FunctionDefinition definition) {
338 setBlocked(false);
339 }
340
341 public void visitEnter(final Node node) {
342 System.out.println(getLatexListEntry(node.getTitle()) + " " + node.getId());
343 }
344
345 public void visitEnter(final Proposition proposition)
346 throws ModuleDataException {
347 if (proposition == null) {
348 return;
349 }
350 System.out.println("\ttesting proposition");
351 final String context = getCurrentContext().getLocationWithinModule();
352 if (proposition.getFormula() != null) {
353 setLocationWithinModule(context + ".getFormula().getElement()");
354 final Element test = proposition.getFormula().getElement();
355 test(test);
356 }
357 setLocationWithinModule(context);
358 }
359
360 public void visitLeave(final Proposition definition) {
361 }
362
363 public void visitEnter(final FormalProofLine line)
364 throws ModuleDataException {
365 if (line == null) {
366 return;
367 }
368 System.out.println("\t\ttesting line " + line.getLabel());
369 final String context = getCurrentContext().getLocationWithinModule();
370 if (line.getFormula() != null) {
371 setLocationWithinModule(context + ".getFormula().getElement()");
372 final Element test = line.getFormula().getElement();
373 test(test);
374 }
375 setLocationWithinModule(context);
376 setBlocked(true);
377 }
378
379 public void visitLeave(final FormalProofLine line) {
380 setBlocked(false);
381 }
382
383 public void visitEnter(final Rule rule) throws ModuleDataException {
384 setBlocked(true);
385 }
386
387 public void visitLeave(final Rule rule) {
388 setBlocked(false);
389 }
390
391 public String getExecutionActionDescription() {
392 return super.getExecutionActionDescription() + "\n" + interpreter.toString();
393 }
394 /**
395 * Set location information where are we within the original module.
396 *
397 * @param locationWithinModule Location within module.
398 */
399 public void setLocationWithinModule(final String locationWithinModule) {
400 getCurrentContext().setLocationWithinModule(locationWithinModule);
401 }
402
403 /**
404 * Filters correct entry out of LaTeX list. Filter criterion is for example the correct
405 * language.
406 *
407 * @param list List of LaTeX entries.
408 * @return Filtered text.
409 */
410 private String getLatexListEntry(final LatexList list) {
411 if (list == null) {
412 return "";
413 }
414 for (int i = 0; i < list.size(); i++) {
415 if (list.get(i) != null && "en".equals(list.get(i).getLanguage())) {
416 return getLatex(list.get(i));
417 }
418 }
419 // assume entry with missing language as default
420 for (int i = 0; i < list.size(); i++) {
421 if (list.get(i) != null && list.get(i).getLanguage() == null) {
422 return getLatex(list.get(i));
423 }
424 }
425 for (int i = 0; i < list.size(); i++) {
426 if (list.get(i) != null) {
427 return getLatex(list.get(i));
428 }
429 }
430 return "";
431 }
432
433 private String getLatex(final Latex latex) {
434 String result = latex.getLatex();
435 if (result == null) {
436 result = "";
437 }
438 result = result.trim();
439 result = result.replaceAll("\\\\index\\{.*\\}", "");
440 return result.trim();
441 }
442
443 }
|