001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, 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.logic.model;
017
018 import java.util.ArrayList;
019 import java.util.List;
020
021 import org.qedeq.base.trace.Trace;
022 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
023 import org.qedeq.kernel.bo.logic.common.FunctionKey;
024 import org.qedeq.kernel.bo.logic.common.Operators;
025 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
026 import org.qedeq.kernel.bo.logic.common.PredicateKey;
027 import org.qedeq.kernel.bo.logic.common.SubjectVariable;
028 import org.qedeq.kernel.bo.module.KernelQedeqBo;
029 import org.qedeq.kernel.bo.service.DefaultKernelQedeqBo;
030 import org.qedeq.kernel.bo.service.unicode.Latex2UnicodeParser;
031 import org.qedeq.kernel.se.base.list.Element;
032 import org.qedeq.kernel.se.base.list.ElementList;
033 import org.qedeq.kernel.se.common.ModuleContext;
034
035
036 /**
037 * This class calculates a new truth value for a given formula for a given interpretation.
038 *
039 * @author Michael Meyling
040 */
041 public class DynamicDirectInterpreter {
042
043 /** This class. */
044 private static final Class CLASS = DynamicDirectInterpreter.class;
045
046 /** We work with this module. */
047 private KernelQedeqBo qedeq;
048
049 /** Module context. Here were are currently. */
050 private ModuleContext moduleContext;
051
052 /** For formatting debug trace output. */
053 private final StringBuffer deepness = new StringBuffer();
054
055 /** Model contains entities, functions, predicates. */
056 private final DynamicModel model;
057
058 /** Interpret subject variables. */
059 private final SubjectVariableInterpreter subjectVariableInterpreter;
060
061 /** Interpret predicate variables. */
062 private final PredicateVariableInterpreter predicateVariableInterpreter;
063
064 /** Interpret function variables. */
065 private final FunctionVariableInterpreter functionVariableInterpreter;
066
067 /**
068 * Constructor.
069 *
070 * @param qedeq We work with this module.
071 * @param model We work with this model.
072 */
073 public DynamicDirectInterpreter(final KernelQedeqBo qedeq, final DynamicModel model) {
074 this(qedeq, model, new SubjectVariableInterpreter(model), new PredicateVariableInterpreter(
075 model), new FunctionVariableInterpreter(model));
076 }
077
078 /**
079 * Constructor.
080 *
081 * @param qedeq We work with this module.
082 * @param model We work with this model.
083 * @param subjectVariableInterpreter Subject variable interpreter.
084 * @param predicateVariableInterpreter Predicate variable interpreter.
085 * @param functionVariableInterpreter Function variable interpreter.
086 */
087 public DynamicDirectInterpreter(final KernelQedeqBo qedeq, final DynamicModel model,
088 final SubjectVariableInterpreter subjectVariableInterpreter,
089 final PredicateVariableInterpreter predicateVariableInterpreter,
090 final FunctionVariableInterpreter functionVariableInterpreter) {
091 this.qedeq = qedeq;
092 this.model = model;
093 this.subjectVariableInterpreter = subjectVariableInterpreter;
094 this.predicateVariableInterpreter = predicateVariableInterpreter;
095 this.functionVariableInterpreter = functionVariableInterpreter;
096 }
097
098 /**
099 * Calculate function value.
100 *
101 * @param constant This is the function definition.
102 * @param entities Function arguments.
103 * @return Result of calculation;
104 * @throws HeuristicException Calculation of function value failed.
105 */
106 public Entity calculateFunctionValue(final FunctionConstant constant,
107 final Entity[] entities) throws HeuristicException {
108 final List params = constant.getSubjectVariables();
109 for (int i = 0; i < entities.length; i++) {
110 final SubjectVariable var = (SubjectVariable) params.get(i);
111 subjectVariableInterpreter.forceAddSubjectVariable(var, entities[i].getValue());
112 }
113 Entity result;
114 try {
115 result = calculateTerm(constant.getDefiningTerm());
116 } finally {
117 for (int i = entities.length - 1; i >= 0; i--) {
118 final SubjectVariable var = (SubjectVariable) params.get(i);
119 subjectVariableInterpreter.forceRemoveSubjectVariable(var);
120 }
121 }
122 return result;
123 }
124
125 /**
126 * Calculate function value.
127 *
128 * @param constant This is the predicate definition.
129 * @param entities Function arguments.
130 * @return Result of calculation;
131 * @throws HeuristicException Calculation failed.
132 */
133 public boolean calculatePredicateValue(final PredicateConstant constant,
134 final Entity[] entities) throws HeuristicException {
135 final List params = constant.getSubjectVariables();
136 for (int i = 0; i < entities.length; i++) {
137 final SubjectVariable var = (SubjectVariable) params.get(i);
138 subjectVariableInterpreter.forceAddSubjectVariable(var, entities[i].getValue());
139 }
140 boolean result;
141 try {
142 result = calculateValue(constant.getDefiningFormula());
143 } finally {
144 for (int i = entities.length - 1; i >= 0; i--) {
145 final SubjectVariable var = (SubjectVariable) params.get(i);
146 subjectVariableInterpreter.forceRemoveSubjectVariable(var);
147 }
148 }
149 return result;
150 }
151
152 /**
153 * Calculate the truth value of a given formula is a tautology. This is done by checking with
154 * a model and certain variable values.
155 *
156 * @param moduleContext Where we are within an module.
157 * @param formula Formula.
158 * @return Truth value of formula.
159 * @throws HeuristicException We couldn't calculate the value.
160 */
161 public boolean calculateValue(final ModuleContext moduleContext, final Element formula)
162 throws HeuristicException {
163 // this.startElement = formula;
164 this.moduleContext = new ModuleContext(moduleContext);
165 // this.startContext = new ModuleContext(moduleContext);
166 return calculateValue(formula);
167 }
168
169 /**
170 * Calculate the truth value of a given formula is a tautology. This is done by checking with
171 * a model and certain variable values.
172 *
173 * @param formula Formula.
174 * @return Truth value of formula.
175 * @throws HeuristicException We couldn't calculate the value.
176 */
177 private boolean calculateValue(final Element formula) throws HeuristicException {
178 final String method = "calculateValue(Element)";
179 if (Trace.isDebugEnabled(CLASS)) {
180 Trace.param(CLASS, this, method, deepness.toString() + "formula",
181 Latex2UnicodeParser.transform(null, qedeq.getElement2Latex().getLatex(formula), 0));
182 deepness.append("-");
183 }
184 if (formula.isAtom()) {
185 throw new HeuristicException(HeuristicErrorCodes.WRONG_CALLING_CONVENTION_CODE,
186 HeuristicErrorCodes.WRONG_CALLING_CONVENTION_TEXT, moduleContext);
187 }
188 final KernelQedeqBo qedeqOld = qedeq;
189 final ModuleContext moduleContextOld = new ModuleContext(moduleContext);
190 final String context = getLocationWithinModule();
191 boolean result;
192 try {
193 final ElementList list = formula.getList();
194 setLocationWithinModule(context + ".getList()");
195 final String op = list.getOperator();
196 if (Operators.CONJUNCTION_OPERATOR.equals(op)) {
197 result = true;
198 for (int i = 0; i < list.size() && result; i++) {
199 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
200 result &= calculateValue(list.getElement(i));
201 }
202 } else if (Operators.DISJUNCTION_OPERATOR.equals(op)) {
203 result = false;
204 for (int i = 0; i < list.size() && !result; i++) {
205 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
206 result |= calculateValue(list.getElement(i));
207 }
208 } else if (Operators.EQUIVALENCE_OPERATOR.equals(op)) {
209 result = true;
210 boolean value = false;
211 for (int i = 0; i < list.size() && result; i++) {
212 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
213 if (i > 0) {
214 if (value != calculateValue(list.getElement(i))) {
215 result = false;
216 }
217 } else {
218 value = calculateValue(list.getElement(i));
219 }
220 }
221 } else if (Operators.IMPLICATION_OPERATOR.equals(op)) {
222 result = false;
223 for (int i = 0; i < list.size() && !result; i++) {
224 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
225 if (i < list.size() - 1) {
226 result |= !calculateValue(list.getElement(i));
227 } else {
228 result |= calculateValue(list.getElement(i));
229 }
230 }
231 } else if (Operators.NEGATION_OPERATOR.equals(op)) {
232 result = true;
233 for (int i = 0; i < list.size() && result; i++) {
234 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
235 result &= !calculateValue(list.getElement(i));
236 }
237 } else if (Operators.PREDICATE_VARIABLE.equals(op)) {
238 setLocationWithinModule(context + ".getList()");
239 final Entity[] arguments = getEntities(list);
240 final PredicateVariable var = new PredicateVariable(
241 list.getElement(0).getAtom().getString(), list.size() - 1);
242 result = predicateVariableInterpreter.getPredicate(var)
243 .calculate(arguments);
244 } else if (Operators.UNIVERSAL_QUANTIFIER_OPERATOR.equals(op)) {
245 result = handleUniversalQuantifier(list);
246 } else if (Operators.EXISTENTIAL_QUANTIFIER_OPERATOR.equals(op)) {
247 result = handleExistentialQuantifier(list);
248 } else if (Operators.UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR.equals(op)) {
249 result = handleUniqueExistentialQuantifier(list);
250 } else if (Operators.PREDICATE_CONSTANT.equals(op)) {
251 final String label = list.getElement(0).getAtom().getString();
252 String name = label;
253 // System.out.println(label);
254 KernelQedeqBo newProp = qedeq;
255 while (name.indexOf(".") >= 0) {
256 name = name.substring(label.indexOf(".") + 1);
257 final String external = label.substring(0, label.indexOf("."));
258 newProp = null;
259 if (qedeq.getKernelRequiredModules() != null) {
260 newProp = (DefaultKernelQedeqBo)
261 qedeq.getKernelRequiredModules().getQedeqBo(external);
262 }
263 if (newProp == null) {
264 setLocationWithinModule(context + ".getList().getOperator()");
265 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_CODE,
266 HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT + "\"" + external + "\""
267 + HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT_2 + "\"" + external
268 + "." + name + "\"",
269 moduleContext);
270 }
271 }
272 final PredicateKey predicateKey = new PredicateKey(name, "" + (list.size() - 1));
273 final PredicateConstant constant = (newProp.getExistenceChecker() != null
274 ? newProp.getExistenceChecker().get(predicateKey) : null);
275 if (constant != null) {
276 setLocationWithinModule(context + ".getList()");
277 final Entity[] arguments = getEntities(list);
278 setModuleContext(newProp);
279 moduleContext = new ModuleContext(constant.getContext());
280 // we must get the second argument of equivalence
281 moduleContext.setLocationWithinModule(moduleContext.getLocationWithinModule()
282 + ".getElement(1)");
283 try {
284 result = calculatePredicateValue(constant, arguments);
285 } catch (HeuristicException e) {
286 setModuleContext(qedeqOld);
287 moduleContext = moduleContextOld;
288 setLocationWithinModule(context + ".getList().getElement(1)");
289 throw new HeuristicException(
290 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
291 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + predicateKey,
292 moduleContext, e.getContext());
293 }
294 } else { // should be initial predicate, must be in the model
295 final ModelPredicateConstant var = new ModelPredicateConstant(name, list.size()
296 - 1);
297 final Predicate predicate = model.getPredicateConstant(var);
298 if (predicate == null) {
299 setLocationWithinModule(context + ".getList().getOperator()");
300 throw new HeuristicException(
301 HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE,
302 HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT + var,
303 moduleContext);
304 }
305 setLocationWithinModule(context + ".getList()");
306 final Entity[] arguments = getEntities(list);
307 result = predicate.calculate(arguments);
308 }
309 } else {
310 setLocationWithinModule(context + ".getList().getOperator()");
311 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_OPERATOR_CODE,
312 HeuristicErrorCodes.UNKNOWN_OPERATOR_TEXT + op, moduleContext);
313 }
314 } finally {
315 // qedeq = qedeqOld;
316 setModuleContext(qedeqOld);
317 moduleContext = moduleContextOld;
318 setLocationWithinModule(context);
319 }
320 if (Trace.isDebugEnabled(CLASS)) {
321 deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
322 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(
323 null, qedeq.getElement2Latex().getLatex(formula), 0), result);
324 }
325 return result;
326 }
327
328 /**
329 * Handle universal quantifier operator.
330 *
331 * @param list Work on this formula.
332 * @return result Calculated truth value.
333 * @throws HeuristicException Calculation not possible.
334 */
335 private boolean handleUniversalQuantifier(final ElementList list)
336 throws HeuristicException {
337 final String method = "handleUniversalQuantifier(ElementList)";
338 final String context = getLocationWithinModule();
339 boolean result = true;
340 final ElementList variable = list.getElement(0).getList();
341 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
342 subjectVariableInterpreter.addSubjectVariable(var);
343 for (int i = 0; i < model.getEntitiesSize(); i++) {
344 if (Trace.isDebugEnabled(CLASS)) {
345 Trace.param(CLASS, this, method, deepness.toString()
346 + Latex2UnicodeParser.transform(null, qedeq.getElement2Latex()
347 .getLatex(variable), 0), model.getEntity(i));
348 }
349 if (list.size() == 2) {
350 setLocationWithinModule(context + ".getElement(1)");
351 result &= calculateValue(list.getElement(1));
352 } else { // must be 3
353 setLocationWithinModule(context + ".getElement(1)");
354 final boolean result1 = calculateValue(list.getElement(1));
355 setLocationWithinModule(context + ".getElement(2)");
356 final boolean result2 = calculateValue(list.getElement(2));
357 result &= !result1 || result2;
358 }
359 if (!result) {
360 break;
361 }
362 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
363 }
364 subjectVariableInterpreter.removeSubjectVariable(var);
365 return result;
366 }
367
368 /**
369 * Handle existential quantifier operator.
370 *
371 * @param list Work on this formula.
372 * @return result Calculated truth value.
373 * @throws HeuristicException Calculation not possible.
374 */
375 private boolean handleExistentialQuantifier(final ElementList list)
376 throws HeuristicException {
377 final String method = "handleExistentialQuantifier(ElementList)";
378 final String context = getLocationWithinModule();
379 boolean result = false;
380 final ElementList variable = list.getElement(0).getList();
381 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
382 subjectVariableInterpreter.addSubjectVariable(var);
383 for (int i = 0; i < model.getEntitiesSize(); i++) {
384 if (Trace.isDebugEnabled(CLASS)) {
385 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser
386 .transform(null, qedeq.getElement2Latex().getLatex(variable), 0),
387 model.getEntity(i));
388 }
389 if (list.size() == 2) {
390 setLocationWithinModule(context + ".getElement(1)");
391 result |= calculateValue(list.getElement(1));
392 } else { // must be 3
393 setLocationWithinModule(context + ".getElement(1)");
394 final boolean result1 = calculateValue(list.getElement(1));
395 setLocationWithinModule(context + ".getElement(2)");
396 final boolean result2 = calculateValue(list.getElement(2));
397 result |= result1 && result2;
398 }
399 if (result) {
400 break;
401 }
402 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
403 }
404 subjectVariableInterpreter.removeSubjectVariable(var);
405 return result;
406 }
407
408 /**
409 * Handle unique existential quantifier operator.
410 *
411 * @param list Work on this formula.
412 * @return result Calculated truth value.
413 * @throws HeuristicException Calculation not possible.
414 */
415 private boolean handleUniqueExistentialQuantifier(final ElementList list)
416 throws HeuristicException {
417 final String method = "handleUniqueExistentialQuantifier(ElementList)";
418 final String context = getLocationWithinModule();
419 boolean result = false;
420 final ElementList variable = list.getElement(0).getList();
421 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
422 subjectVariableInterpreter.addSubjectVariable(var);
423 for (int i = 0; i < model.getEntitiesSize(); i++) {
424 if (Trace.isDebugEnabled(CLASS)) {
425 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
426 qedeq.getElement2Latex().getLatex(variable), 0), model.getEntity(i));
427 }
428 boolean val;
429 if (list.size() == 2) {
430 setLocationWithinModule(context + ".getList().getElement(1)");
431 val = calculateValue(list.getElement(1));
432 } else { // must be 3
433 setLocationWithinModule(context + ".getList().getElement(1)");
434 final boolean result1 = calculateValue(list.getElement(1));
435 setLocationWithinModule(context + ".getList().getElement(2)");
436 final boolean result2 = calculateValue(list.getElement(2));
437 val = result1 && result2;
438 }
439 if (val) {
440 if (result) {
441 result = false;
442 break;
443 } else {
444 result = true;
445 }
446 }
447 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
448 }
449 subjectVariableInterpreter.removeSubjectVariable(var);
450 return result;
451 }
452
453 /**
454 * Interpret terms.
455 *
456 * @param terms Interpret these terms. The first entry is stripped.
457 * @return Values.
458 * @throws HeuristicException evaluation failed.
459 */
460 private Entity[] getEntities(final ElementList terms)
461 throws HeuristicException {
462 // System.out.println(terms);
463 final String context = getLocationWithinModule();
464 final Entity[] result = new Entity[terms.size() - 1]; // strip first argument
465 for (int i = 0; i < result.length; i++) {
466 // System.out.println(i + " " + terms.getElement(i + 1));
467 setLocationWithinModule(context + ".getElement(" + (i + 1) + ")");
468 result[i] = calculateTerm(terms.getElement(i + 1));
469 }
470 setLocationWithinModule(context);
471 return result;
472 }
473
474 /**
475 * Calculate the term value of a given term. This is done by checking with
476 * a model and certain variable values.
477 *
478 * @param moduleContext Where we are within an module.
479 * @param term Term.
480 * @return Entity of model.
481 * @throws HeuristicException We couldn't calculate the value.
482 */
483 public Entity calculateTerm(final ModuleContext moduleContext, final Element term)
484 throws HeuristicException {
485 this.moduleContext = moduleContext;
486 return calculateTerm(term);
487 }
488
489 /**
490 * Interpret term.
491 *
492 * @param term Interpret this term.
493 * @return Value.
494 * @throws HeuristicException evaluation failed.
495 */
496 private Entity calculateTerm(final Element term)
497 throws HeuristicException {
498 final String method = "calculateTerm(Element) ";
499 if (Trace.isDebugEnabled(CLASS)) {
500 Trace.param(CLASS, this, method, deepness.toString() + "term ", Latex2UnicodeParser.transform(null,
501 qedeq.getElement2Latex().getLatex(term), 0));
502 deepness.append("-");
503 }
504 if (!term.isList()) {
505 throw new RuntimeException("a term should be a list: " + term);
506 }
507 final KernelQedeqBo qedeqOld = qedeq;
508 final ModuleContext moduleContextOld = new ModuleContext(moduleContext);
509 final String context = getLocationWithinModule();
510 Entity result = null;
511 try {
512 final ElementList termList = term.getList();
513 final String op = termList.getOperator();
514 if (Operators.SUBJECT_VARIABLE.equals(op)) {
515 final String text = termList.getElement(0).getAtom().getString();
516 final SubjectVariable var = new SubjectVariable(text);
517 result = subjectVariableInterpreter.getEntity(var);
518 } else if (Operators.FUNCTION_VARIABLE.equals(op)) {
519 final FunctionVariable var = new FunctionVariable(termList.getElement(0).getAtom().getString(),
520 termList.size() - 1);
521 Function function = functionVariableInterpreter.getFunction(var);
522 setLocationWithinModule(context + ".getList()");
523 result = function.map(getEntities(termList));
524 } else if (Operators.FUNCTION_CONSTANT.equals(op)) {
525 final String label = termList.getElement(0).getAtom().getString();
526 String name = label;
527 KernelQedeqBo newProp = qedeq;
528 if (label.indexOf(".") >= 0) {
529 name = label.substring(label.indexOf(".") + 1);
530 final String external = label.substring(0, label.indexOf("."));
531 newProp = null;
532 if (qedeq.getKernelRequiredModules() != null) {
533 newProp = (DefaultKernelQedeqBo)
534 qedeq.getKernelRequiredModules().getQedeqBo(external);
535 }
536 if (newProp == null) {
537 setLocationWithinModule(context + ".getList().getOperator()");
538 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_CODE,
539 HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT + "\"" + external + "\""
540 + HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT_2 + "\"" + label + "\"",
541 moduleContext);
542 }
543 }
544 final FunctionKey functionKey = new FunctionKey(name, "" + (termList.size() - 1));
545 FunctionConstant constant
546 = newProp.getExistenceChecker().get(functionKey);
547 if (constant != null) {
548 setLocationWithinModule(context + ".getList()");
549 final Entity[] arguments = getEntities(termList);
550 setModuleContext(newProp);
551 moduleContext = new ModuleContext(constant.getContext());
552 // we must get the second argument of equal relation
553 moduleContext.setLocationWithinModule(moduleContext.getLocationWithinModule() + ".getElement(2)");
554 try {
555 result = calculateFunctionValue(constant, arguments);
556 } catch (HeuristicException e) {
557 setModuleContext(qedeqOld);
558 moduleContext = moduleContextOld;
559 setLocationWithinModule(context + ".getList().getElement(1)");
560 throw new HeuristicException(HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
561 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + functionKey,
562 moduleContext, e.getContext());
563 }
564 } else {
565 final ModelFunctionConstant var = new ModelFunctionConstant(name,
566 termList.size() - 1);
567 Function function = model.getFunctionConstant(var);
568 if (function == null) {
569 setLocationWithinModule(context + ".getList().getOperator()");
570 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE,
571 HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT + var, moduleContext);
572 }
573 setLocationWithinModule(context + ".getList()");
574 final Entity[] arguments = getEntities(termList);
575 result = function.map(arguments);
576 }
577 } else if (Operators.CLASS_OP.equals(op)) {
578 List fullfillers = new ArrayList();
579 ElementList variable = termList.getElement(0).getList();
580 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
581 subjectVariableInterpreter.addSubjectVariable(var);
582 KernelQedeqBo newProp = qedeq;
583 if (qedeq.getExistenceChecker() != null) {
584 newProp = qedeq.getExistenceChecker().getClassOperatorModule();
585 }
586 final PredicateConstant isSet = newProp.getExistenceChecker().getPredicate("isSet", 1);
587 if (isSet == null) {
588 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
589 HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + "isSet(*)", moduleContext);
590 }
591 for (int i = 0; i < model.getEntitiesSize(); i++) {
592 setModuleContext(qedeqOld);
593 moduleContext = moduleContextOld;
594 setLocationWithinModule(context + ".getList().getElement(1)");
595 if (calculateValue(termList.getElement(1))) {
596 setModuleContext(newProp);
597 moduleContext = newProp.getLabels().getPredicateContext("isSet", 1);
598 setLocationWithinModule(moduleContext.getLocationWithinModule()
599 + ".getFormula().getElement().getList().getElement(1)");
600 try {
601 if (calculatePredicateValue(isSet, new Entity[] {model.getEntity(i)})) {
602 fullfillers.add(model.getEntity(i));
603 }
604 } catch (HeuristicException e) {
605 setModuleContext(qedeqOld);
606 moduleContext = moduleContextOld;
607 setLocationWithinModule(context + ".getList().getElement(1)");
608 throw new HeuristicException(HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
609 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + isSet,
610 moduleContext, e.getContext());
611 }
612 }
613 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
614 }
615 result = model.comprehension((Entity[]) fullfillers.toArray(new Entity[] {}));
616 subjectVariableInterpreter.removeSubjectVariable(var);
617 } else {
618 setLocationWithinModule(context + ".getList().getOperator()");
619 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
620 HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + op, moduleContext);
621 }
622 } finally {
623 // qedeq = qedeqOld;
624 setModuleContext(qedeqOld);
625 moduleContext = moduleContextOld;
626 // System.out.println("module context old: " + moduleContextOld);
627 setLocationWithinModule(context);
628 }
629 if (Trace.isDebugEnabled(CLASS)) {
630 deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
631 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
632 qedeq.getElement2Latex().getLatex(term), 0), result);
633 }
634 return result;
635 }
636
637 private String getLocationWithinModule() {
638 return moduleContext.getLocationWithinModule();
639 }
640
641 protected ModuleContext getModuleContext() {
642 return moduleContext;
643 }
644
645 protected void setModuleContext(final KernelQedeqBo qedeq) {
646 this.qedeq = qedeq;
647 moduleContext = new ModuleContext(qedeq.getModuleAddress());
648 }
649
650 protected void setLocationWithinModule(final String localContext) {
651 moduleContext.setLocationWithinModule(localContext);
652 }
653
654 /**
655 * Change to next valuation.
656 *
657 * @return Is there a next new valuation?
658 */
659 public boolean next() {
660 return subjectVariableInterpreter.next() || predicateVariableInterpreter.next()
661 || functionVariableInterpreter.next();
662 }
663
664 public String toString() {
665 final StringBuffer buffer = new StringBuffer();
666 buffer.append("Current interpretation:\n");
667 buffer.append("\t" + predicateVariableInterpreter + "\n");
668 buffer.append("\t" + subjectVariableInterpreter + "\n");
669 buffer.append("\t" + functionVariableInterpreter);
670 return buffer.toString();
671 }
672
673 /**
674 * Strips the reference to external modules.
675 *
676 * @param operator Might have reference to an external module.
677 * @return Operator as local reference.
678 */
679 public String stripReference(final String operator) {
680 final int index = operator.lastIndexOf(".");
681 if (index >= 0 && index + 1 < operator.length()) {
682 return operator.substring(index + 1);
683 }
684 return operator;
685 }
686
687
688 /**
689 * Is the given predicate constant already defined?
690 *
691 * @param constant Predicate constant to check for.
692 * @return Is the given predicate constant already defined?
693 */
694 public boolean hasPredicateConstant(final ModelPredicateConstant constant) {
695 return null != model.getPredicateConstant(constant);
696 }
697
698 /**
699 * Is the given function constant already defined?
700 *
701 * @param constant Function constant to check for.
702 * @return Is the given function constant already defined?
703 */
704 public boolean hasFunctionConstant(final ModelFunctionConstant constant) {
705 return null != model.getFunctionConstant(constant);
706 }
707
708 /**
709 * Clear all variable settings.
710 */
711 public void clearVariables() {
712 subjectVariableInterpreter.clear();
713 predicateVariableInterpreter.clear();
714 functionVariableInterpreter.clear();
715 }
716
717 /**
718 * Get model.
719 *
720 * @return Model we work with.
721 */
722 public DynamicModel getModel() {
723 return model;
724 }
725
726
727 }
|