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 }
444 result = true;
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 }
|