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.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 KernelQedeqBo newProp = qedeq;
254 while (name.indexOf(".") >= 0) {
255 name = name.substring(label.indexOf(".") + 1);
256 final String external = label.substring(0, label.indexOf("."));
257 newProp = null;
258 if (qedeq.getKernelRequiredModules() != null) {
259 newProp = (DefaultKernelQedeqBo)
260 qedeq.getKernelRequiredModules().getQedeqBo(external);
261 }
262 if (newProp == null) {
263 setLocationWithinModule(context + ".getList().getOperator()");
264 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_CODE,
265 HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT + "\"" + external + "\""
266 + HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT_2 + "\"" + external
267 + "." + name + "\"",
268 moduleContext);
269 }
270 }
271 final PredicateKey predicateKey = new PredicateKey(name, "" + (list.size() - 1));
272 final PredicateConstant constant = (newProp.getExistenceChecker() != null
273 ? newProp.getExistenceChecker().get(predicateKey) : null);
274 if (constant != null) {
275 setLocationWithinModule(context + ".getList()");
276 final Entity[] arguments = getEntities(list);
277 setModuleContext(newProp);
278 moduleContext = new ModuleContext(constant.getContext());
279 // we must get the second argument of equivalence
280 moduleContext.setLocationWithinModule(moduleContext.getLocationWithinModule()
281 + ".getElement(1)");
282 try {
283 result = calculatePredicateValue(constant, arguments);
284 } catch (HeuristicException e) {
285 setModuleContext(qedeqOld);
286 moduleContext = moduleContextOld;
287 setLocationWithinModule(context + ".getList().getElement(1)");
288 throw new HeuristicException(
289 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
290 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + predicateKey,
291 moduleContext, e.getContext());
292 }
293 } else { // should be initial predicate, must be in the model
294 final ModelPredicateConstant var = new ModelPredicateConstant(name, list.size()
295 - 1);
296 final Predicate predicate = model.getPredicateConstant(var);
297 if (predicate == null) {
298 setLocationWithinModule(context + ".getList().getOperator()");
299 throw new HeuristicException(
300 HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE,
301 HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT + var,
302 moduleContext);
303 }
304 setLocationWithinModule(context + ".getList()");
305 final Entity[] arguments = getEntities(list);
306 result = predicate.calculate(arguments);
307 }
308 } else {
309 setLocationWithinModule(context + ".getList().getOperator()");
310 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_OPERATOR_CODE,
311 HeuristicErrorCodes.UNKNOWN_OPERATOR_TEXT + op, moduleContext);
312 }
313 } finally {
314 // qedeq = qedeqOld;
315 setModuleContext(qedeqOld);
316 moduleContext = moduleContextOld;
317 setLocationWithinModule(context);
318 }
319 if (Trace.isDebugEnabled(CLASS)) {
320 deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
321 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(
322 null, qedeq.getElement2Latex().getLatex(formula), 0), result);
323 }
324 return result;
325 }
326
327 /**
328 * Handle universal quantifier operator.
329 *
330 * @param list Work on this formula.
331 * @return result Calculated truth value.
332 * @throws HeuristicException Calculation not possible.
333 */
334 private boolean handleUniversalQuantifier(final ElementList list)
335 throws HeuristicException {
336 final String method = "handleUniversalQuantifier(ElementList)";
337 final String context = getLocationWithinModule();
338 boolean result = true;
339 final ElementList variable = list.getElement(0).getList();
340 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
341 subjectVariableInterpreter.addSubjectVariable(var);
342 for (int i = 0; i < model.getEntitiesSize(); i++) {
343 if (Trace.isDebugEnabled(CLASS)) {
344 Trace.param(CLASS, this, method, deepness.toString()
345 + Latex2UnicodeParser.transform(null, qedeq.getElement2Latex()
346 .getLatex(variable), 0), model.getEntity(i));
347 }
348 if (list.size() == 2) {
349 setLocationWithinModule(context + ".getList().getElement(1)");
350 result &= calculateValue(list.getElement(1));
351 } else { // must be 3
352 setLocationWithinModule(context + ".getList().getElement(1)");
353 final boolean result1 = calculateValue(list.getElement(1));
354 setLocationWithinModule(context + ".getList().getElement(2)");
355 final boolean result2 = calculateValue(list.getElement(2));
356 result &= !result1 || result2;
357 }
358 if (!result) {
359 break;
360 }
361 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
362 }
363 subjectVariableInterpreter.removeSubjectVariable(var);
364 return result;
365 }
366
367 /**
368 * Handle existential quantifier operator.
369 *
370 * @param list Work on this formula.
371 * @return result Calculated truth value.
372 * @throws HeuristicException Calculation not possible.
373 */
374 private boolean handleExistentialQuantifier(final ElementList list)
375 throws HeuristicException {
376 final String method = "handleExistentialQuantifier(ElementList)";
377 final String context = getLocationWithinModule();
378 boolean result = false;
379 final ElementList variable = list.getElement(0).getList();
380 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
381 subjectVariableInterpreter.addSubjectVariable(var);
382 for (int i = 0; i < model.getEntitiesSize(); i++) {
383 if (Trace.isDebugEnabled(CLASS)) {
384 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser
385 .transform(null, qedeq.getElement2Latex().getLatex(variable), 0),
386 model.getEntity(i));
387 }
388 if (list.size() == 2) {
389 setLocationWithinModule(context + ".getList().getElement(1)");
390 result |= calculateValue(list.getElement(1));
391 } else { // must be 3
392 setLocationWithinModule(context + ".getList().getElement(1)");
393 final boolean result1 = calculateValue(list.getElement(1));
394 setLocationWithinModule(context + ".getList().getElement(2)");
395 final boolean result2 = calculateValue(list.getElement(2));
396 result |= result1 && result2;
397 }
398 if (result) {
399 break;
400 }
401 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
402 }
403 subjectVariableInterpreter.removeSubjectVariable(var);
404 return result;
405 }
406
407 /**
408 * Handle unique existential quantifier operator.
409 *
410 * @param list Work on this formula.
411 * @return result Calculated truth value.
412 * @throws HeuristicException Calculation not possible.
413 */
414 private boolean handleUniqueExistentialQuantifier(final ElementList list)
415 throws HeuristicException {
416 final String method = "handleUniqueExistentialQuantifier(ElementList)";
417 final String context = getLocationWithinModule();
418 boolean result = false;
419 final ElementList variable = list.getElement(0).getList();
420 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
421 subjectVariableInterpreter.addSubjectVariable(var);
422 for (int i = 0; i < model.getEntitiesSize(); i++) {
423 if (Trace.isDebugEnabled(CLASS)) {
424 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
425 qedeq.getElement2Latex().getLatex(variable), 0), model.getEntity(i));
426 }
427 boolean val;
428 if (list.size() == 2) {
429 setLocationWithinModule(context + ".getList().getElement(1)");
430 val = calculateValue(list.getElement(1));
431 } else { // must be 3
432 setLocationWithinModule(context + ".getList().getElement(1)");
433 final boolean result1 = calculateValue(list.getElement(1));
434 setLocationWithinModule(context + ".getList().getElement(2)");
435 final boolean result2 = calculateValue(list.getElement(2));
436 val = result1 && result2;
437 }
438 if (val) {
439 if (result) {
440 result = false;
441 break;
442 } else {
443 result = true;
444 }
445 }
446 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
447 }
448 subjectVariableInterpreter.removeSubjectVariable(var);
449 return result;
450 }
451
452 /**
453 * Interpret terms.
454 *
455 * @param terms Interpret these terms. The first entry is stripped.
456 * @return Values.
457 * @throws HeuristicException evaluation failed.
458 */
459 private Entity[] getEntities(final ElementList terms)
460 throws HeuristicException {
461 // System.out.println(terms);
462 final String context = getLocationWithinModule();
463 final Entity[] result = new Entity[terms.size() - 1]; // strip first argument
464 for (int i = 0; i < result.length; i++) {
465 // System.out.println(i + " " + terms.getElement(i + 1));
466 setLocationWithinModule(context + ".getElement(" + (i + 1) + ")");
467 result[i] = calculateTerm(terms.getElement(i + 1));
468 }
469 setLocationWithinModule(context);
470 return result;
471 }
472
473 /**
474 * Calculate the term value of a given term. This is done by checking with
475 * a model and certain variable values.
476 *
477 * @param moduleContext Where we are within an module.
478 * @param term Term.
479 * @return Entity of model.
480 * @throws HeuristicException We couldn't calculate the value.
481 */
482 public Entity calculateTerm(final ModuleContext moduleContext, final Element term)
483 throws HeuristicException {
484 this.moduleContext = moduleContext;
485 return calculateTerm(term);
486 }
487
488 /**
489 * Interpret term.
490 *
491 * @param term Interpret this term.
492 * @return Value.
493 * @throws HeuristicException evaluation failed.
494 */
495 private Entity calculateTerm(final Element term)
496 throws HeuristicException {
497 final String method = "calculateTerm(Element) ";
498 if (Trace.isDebugEnabled(CLASS)) {
499 Trace.param(CLASS, this, method, deepness.toString() + "term ", Latex2UnicodeParser.transform(null,
500 qedeq.getElement2Latex().getLatex(term), 0));
501 deepness.append("-");
502 }
503 if (!term.isList()) {
504 throw new RuntimeException("a term should be a list: " + term);
505 }
506 final KernelQedeqBo qedeqOld = qedeq;
507 final ModuleContext moduleContextOld = new ModuleContext(moduleContext);
508 final String context = getLocationWithinModule();
509 Entity result = null;
510 try {
511 final ElementList termList = term.getList();
512 final String op = termList.getOperator();
513 if (Operators.SUBJECT_VARIABLE.equals(op)) {
514 final String text = termList.getElement(0).getAtom().getString();
515 final SubjectVariable var = new SubjectVariable(text);
516 result = subjectVariableInterpreter.getEntity(var);
517 } else if (Operators.FUNCTION_VARIABLE.equals(op)) {
518 final FunctionVariable var = new FunctionVariable(termList.getElement(0).getAtom().getString(),
519 termList.size() - 1);
520 Function function = functionVariableInterpreter.getFunction(var);
521 setLocationWithinModule(context + ".getList()");
522 result = function.map(getEntities(termList));
523 } else if (Operators.FUNCTION_CONSTANT.equals(op)) {
524 final String label = termList.getElement(0).getAtom().getString();
525 String name = label;
526 KernelQedeqBo newProp = qedeq;
527 if (label.indexOf(".") >= 0) {
528 name = label.substring(label.indexOf(".") + 1);
529 final String external = label.substring(0, label.indexOf("."));
530 newProp = null;
531 if (qedeq.getKernelRequiredModules() != null) {
532 newProp = (DefaultKernelQedeqBo)
533 qedeq.getKernelRequiredModules().getQedeqBo(external);
534 }
535 if (newProp == null) {
536 setLocationWithinModule(context + ".getList().getOperator()");
537 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_CODE,
538 HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT + "\"" + external + "\""
539 + HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT_2 + "\"" + label + "\"",
540 moduleContext);
541 }
542 }
543 final FunctionKey functionKey = new FunctionKey(name, "" + (termList.size() - 1));
544 FunctionConstant constant
545 = newProp.getExistenceChecker().get(functionKey);
546 if (constant != null) {
547 setLocationWithinModule(context + ".getList()");
548 final Entity[] arguments = getEntities(termList);
549 setModuleContext(newProp);
550 moduleContext = new ModuleContext(constant.getContext());
551 // we must get the second argument of equal relation
552 moduleContext.setLocationWithinModule(moduleContext.getLocationWithinModule() + ".getElement(2)");
553 try {
554 result = calculateFunctionValue(constant, arguments);
555 } catch (HeuristicException e) {
556 setModuleContext(qedeqOld);
557 moduleContext = moduleContextOld;
558 setLocationWithinModule(context + ".getList().getElement(1)");
559 throw new HeuristicException(HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
560 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + functionKey,
561 moduleContext, e.getContext());
562 }
563 } else {
564 final ModelFunctionConstant var = new ModelFunctionConstant(name,
565 termList.size() - 1);
566 Function function = model.getFunctionConstant(var);
567 if (function == null) {
568 setLocationWithinModule(context + ".getList().getOperator()");
569 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE,
570 HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT + var, moduleContext);
571 }
572 setLocationWithinModule(context + ".getList()");
573 final Entity[] arguments = getEntities(termList);
574 result = function.map(arguments);
575 }
576 } else if (Operators.CLASS_OP.equals(op)) {
577 List fullfillers = new ArrayList();
578 ElementList variable = termList.getElement(0).getList();
579 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
580 subjectVariableInterpreter.addSubjectVariable(var);
581 KernelQedeqBo newProp = qedeq;
582 if (qedeq.getExistenceChecker() != null) {
583 newProp = qedeq.getExistenceChecker().getClassOperatorModule();
584 }
585 final PredicateConstant isSet = newProp.getExistenceChecker().getPredicate("isSet", 1);
586 if (isSet == null) {
587 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
588 HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + "isSet(*)", moduleContext);
589 }
590 for (int i = 0; i < model.getEntitiesSize(); i++) {
591 setModuleContext(qedeqOld);
592 moduleContext = moduleContextOld;
593 setLocationWithinModule(context + ".getList().getElement(1)");
594 if (calculateValue(termList.getElement(1))) {
595 setModuleContext(newProp);
596 moduleContext = newProp.getLabels().getPredicateContext("isSet", 1);
597 setLocationWithinModule(moduleContext.getLocationWithinModule()
598 + ".getFormula().getElement().getList().getElement(1)");
599 try {
600 if (calculatePredicateValue(isSet, new Entity[] {model.getEntity(i)})) {
601 fullfillers.add(model.getEntity(i));
602 }
603 } catch (HeuristicException e) {
604 setModuleContext(qedeqOld);
605 moduleContext = moduleContextOld;
606 setLocationWithinModule(context + ".getList().getElement(1)");
607 throw new HeuristicException(HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
608 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + isSet,
609 moduleContext, e.getContext());
610 }
611 }
612 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
613 }
614 result = model.comprehension((Entity[]) fullfillers.toArray(new Entity[] {}));
615 subjectVariableInterpreter.removeSubjectVariable(var);
616 } else {
617 setLocationWithinModule(context + ".getList().getOperator()");
618 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
619 HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + op, moduleContext);
620 }
621 } finally {
622 // qedeq = qedeqOld;
623 setModuleContext(qedeqOld);
624 moduleContext = moduleContextOld;
625 // System.out.println("module context old: " + moduleContextOld);
626 setLocationWithinModule(context);
627 }
628 if (Trace.isDebugEnabled(CLASS)) {
629 deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
630 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
631 qedeq.getElement2Latex().getLatex(term), 0), result);
632 }
633 return result;
634 }
635
636 private String getLocationWithinModule() {
637 return moduleContext.getLocationWithinModule();
638 }
639
640 protected ModuleContext getModuleContext() {
641 return moduleContext;
642 }
643
644 protected void setModuleContext(final KernelQedeqBo qedeq) {
645 this.qedeq = qedeq;
646 moduleContext = new ModuleContext(qedeq.getModuleAddress());
647 }
648
649 protected void setLocationWithinModule(final String localContext) {
650 moduleContext.setLocationWithinModule(localContext);
651 }
652
653 /**
654 * Change to next valuation.
655 *
656 * @return Is there a next new valuation?
657 */
658 public boolean next() {
659 return subjectVariableInterpreter.next() || predicateVariableInterpreter.next()
660 || functionVariableInterpreter.next();
661 }
662
663 public String toString() {
664 final StringBuffer buffer = new StringBuffer();
665 buffer.append("Current interpretation:\n");
666 buffer.append("\t" + predicateVariableInterpreter + "\n");
667 buffer.append("\t" + subjectVariableInterpreter + "\n");
668 buffer.append("\t" + functionVariableInterpreter);
669 return buffer.toString();
670 }
671
672 /**
673 * Strips the reference to external modules.
674 *
675 * @param operator Might have reference to an external module.
676 * @return Operator as local reference.
677 */
678 public String stripReference(final String operator) {
679 final int index = operator.lastIndexOf(".");
680 if (index >= 0 && index + 1 < operator.length()) {
681 return operator.substring(index + 1);
682 }
683 return operator;
684 }
685
686
687 /**
688 * Is the given predicate constant already defined?
689 *
690 * @param constant Predicate constant to check for.
691 * @return Is the given predicate constant already defined?
692 */
693 public boolean hasPredicateConstant(final ModelPredicateConstant constant) {
694 return null != model.getPredicateConstant(constant);
695 }
696
697 /**
698 * Is the given function constant already defined?
699 *
700 * @param constant Function constant to check for.
701 * @return Is the given function constant already defined?
702 */
703 public boolean hasFunctionConstant(final ModelFunctionConstant constant) {
704 return null != model.getFunctionConstant(constant);
705 }
706
707 /**
708 * Clear all variable settings.
709 */
710 public void clearVariables() {
711 subjectVariableInterpreter.clear();
712 predicateVariableInterpreter.clear();
713 functionVariableInterpreter.clear();
714 }
715
716 /**
717 * Get model.
718 *
719 * @return Model we work with.
720 */
721 public DynamicModel getModel() {
722 return model;
723 }
724
725
726 }
|