View Javadoc

1   /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org
2    *
3    * Copyright 2000-2014,  Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10   * This program is distributed in the hope that it will be useful,
11   * but WITHOUT ANY WARRANTY; without even the implied warranty of
12   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13   * GNU General Public License for more details.
14   */
15  
16  package org.qedeq.kernel.bo.logic.model;
17  
18  import java.util.ArrayList;
19  import java.util.List;
20  
21  import org.qedeq.base.trace.Trace;
22  import org.qedeq.kernel.bo.logic.common.FunctionConstant;
23  import org.qedeq.kernel.bo.logic.common.FunctionKey;
24  import org.qedeq.kernel.bo.logic.common.Operators;
25  import org.qedeq.kernel.bo.logic.common.PredicateConstant;
26  import org.qedeq.kernel.bo.logic.common.PredicateKey;
27  import org.qedeq.kernel.bo.logic.common.SubjectVariable;
28  import org.qedeq.kernel.bo.module.KernelQedeqBo;
29  import org.qedeq.kernel.bo.service.unicode.Latex2UnicodeParser;
30  import org.qedeq.kernel.se.base.list.Element;
31  import org.qedeq.kernel.se.base.list.ElementList;
32  import org.qedeq.kernel.se.common.ModuleContext;
33  
34  
35  /**
36   * This class calculates a new truth value for a given formula for a given interpretation.
37   *
38   * @author  Michael Meyling
39   */
40  public class DynamicDirectInterpreter {
41  
42      /** This class. */
43      private static final Class CLASS = DynamicDirectInterpreter.class;
44  
45      /** We work with this module. */
46      private KernelQedeqBo qedeq;
47  
48      /** Module context. Here were are currently. */
49      private ModuleContext moduleContext;
50  
51      /** For formatting debug trace output. */
52      private final StringBuffer deepness = new StringBuffer();
53  
54      /** Model contains entities, functions, predicates. */
55      private final DynamicModel model;
56  
57      /** Interpret subject variables. */
58      private final SubjectVariableInterpreter subjectVariableInterpreter;
59  
60      /** Interpret predicate variables. */
61      private final PredicateVariableInterpreter predicateVariableInterpreter;
62  
63      /** Interpret function variables. */
64      private final FunctionVariableInterpreter functionVariableInterpreter;
65  
66     /**
67      * Constructor.
68      *
69      * @param   qedeq       We work with this module.
70      * @param   model       We work with this model.
71      */
72     public DynamicDirectInterpreter(final KernelQedeqBo qedeq, final DynamicModel model) {
73         this(qedeq, model, new SubjectVariableInterpreter(model), new PredicateVariableInterpreter(
74             model), new FunctionVariableInterpreter(model));
75     }
76  
77      /**
78       * Constructor.
79       *
80       * @param   qedeq                           We work with this module.
81       * @param   model                           We work with this model.
82       * @param   subjectVariableInterpreter      Subject variable interpreter.
83       * @param   predicateVariableInterpreter    Predicate variable interpreter.
84       * @param   functionVariableInterpreter     Function variable interpreter.
85       */
86      public DynamicDirectInterpreter(final KernelQedeqBo qedeq, final DynamicModel model,
87              final SubjectVariableInterpreter subjectVariableInterpreter,
88              final PredicateVariableInterpreter predicateVariableInterpreter,
89              final FunctionVariableInterpreter functionVariableInterpreter) {
90          this.qedeq = qedeq;
91          this.model = model;
92          this.subjectVariableInterpreter = subjectVariableInterpreter;
93          this.predicateVariableInterpreter = predicateVariableInterpreter;
94          this.functionVariableInterpreter = functionVariableInterpreter;
95      }
96  
97      /**
98       * Calculate function value.
99       *
100      * @param   constant            This is the function definition.
101      * @param   entities            Function arguments.
102      * @return  Result of calculation;
103      * @throws  HeuristicException  Calculation of function value failed.
104      */
105     public Entity calculateFunctionValue(final FunctionConstant constant,
106             final Entity[] entities) throws  HeuristicException {
107         final List params = constant.getSubjectVariables();
108         for (int i = 0; i < entities.length; i++) {
109             final SubjectVariable var = (SubjectVariable) params.get(i);
110             subjectVariableInterpreter.forceAddSubjectVariable(var, entities[i].getValue());
111         }
112         Entity result;
113         try {
114             result = calculateTerm(constant.getDefiningTerm());
115         } finally {
116             for (int i = entities.length - 1; i >= 0; i--) {
117                 final SubjectVariable var = (SubjectVariable) params.get(i);
118                 subjectVariableInterpreter.forceRemoveSubjectVariable(var);
119             }
120         }
121         return result;
122     }
123 
124     /**
125      * Calculate function value.
126      *
127      * @param   constant        This is the predicate definition.
128      * @param   entities        Function arguments.
129      * @return  Result of calculation;
130      * @throws  HeuristicException  Calculation failed.
131      */
132     public boolean calculatePredicateValue(final PredicateConstant constant,
133         final Entity[] entities) throws HeuristicException {
134         final List params = constant.getSubjectVariables();
135         for (int i = 0; i < entities.length; i++) {
136             final SubjectVariable var = (SubjectVariable) params.get(i);
137             subjectVariableInterpreter.forceAddSubjectVariable(var, entities[i].getValue());
138         }
139         boolean result;
140         try {
141             result = calculateValue(constant.getDefiningFormula());
142         } finally {
143             for (int i = entities.length - 1; i >= 0; i--) {
144                 final SubjectVariable var = (SubjectVariable) params.get(i);
145                 subjectVariableInterpreter.forceRemoveSubjectVariable(var);
146             }
147         }
148         return result;
149     }
150 
151     /**
152      * Calculate the truth value of a given formula is a tautology. This is done by checking with
153      * a model and certain variable values.
154      *
155      * @param   moduleContext   Where we are within an module.
156      * @param   formula         Formula.
157      * @return  Truth value of formula.
158      * @throws  HeuristicException      We couldn't calculate the value.
159      */
160     public boolean calculateValue(final ModuleContext moduleContext, final Element formula)
161             throws  HeuristicException {
162 //        this.startElement = formula;
163         this.moduleContext = new ModuleContext(moduleContext);
164 //        this.startContext = new ModuleContext(moduleContext);
165         return calculateValue(formula);
166     }
167 
168     /**
169      * Calculate the truth value of a given formula is a tautology. This is done by checking with
170      * a model and certain variable values.
171      *
172      * @param   formula         Formula.
173      * @return  Truth value of formula.
174      * @throws  HeuristicException      We couldn't calculate the value.
175      */
176     private boolean calculateValue(final Element formula) throws  HeuristicException {
177         final String method = "calculateValue(Element)";
178         if (Trace.isDebugEnabled(CLASS)) {
179             Trace.param(CLASS, this, method, deepness.toString() + "formula",
180                 Latex2UnicodeParser.transform(null, qedeq.getElement2Latex().getLatex(formula), 0));
181             deepness.append("-");
182         }
183         if (formula.isAtom()) {
184             throw new HeuristicException(HeuristicErrorCodes.WRONG_CALLING_CONVENTION_CODE,
185                 HeuristicErrorCodes.WRONG_CALLING_CONVENTION_TEXT, moduleContext);
186         }
187         final KernelQedeqBo qedeqOld = qedeq;
188         final ModuleContext moduleContextOld = new ModuleContext(moduleContext);
189         final String context = getLocationWithinModule();
190         boolean result;
191         try {
192             final ElementList list = formula.getList();
193             setLocationWithinModule(context + ".getList()");
194             final String op = list.getOperator();
195             if (Operators.CONJUNCTION_OPERATOR.equals(op)) {
196                 result = true;
197                 for (int i = 0; i < list.size() && result; i++) {
198                     setLocationWithinModule(context + ".getList().getElement(" + i + ")");
199                     result &= calculateValue(list.getElement(i));
200                 }
201             } else if (Operators.DISJUNCTION_OPERATOR.equals(op)) {
202                 result = false;
203                 for (int i = 0; i < list.size() && !result; i++) {
204                     setLocationWithinModule(context + ".getList().getElement(" + i + ")");
205                     result |= calculateValue(list.getElement(i));
206                 }
207             } else if (Operators.EQUIVALENCE_OPERATOR.equals(op)) {
208                 result = true;
209                 boolean value = false;
210                 for (int i = 0; i < list.size() && result; i++) {
211                     setLocationWithinModule(context + ".getList().getElement(" + i + ")");
212                     if (i > 0) {
213                         if (value != calculateValue(list.getElement(i))) {
214                             result = false;
215                         }
216                     } else {
217                         value = calculateValue(list.getElement(i));
218                     }
219                 }
220             } else if (Operators.IMPLICATION_OPERATOR.equals(op)) {
221                 result = false;
222                 for (int i = 0; i < list.size() && !result; i++) {
223                     setLocationWithinModule(context + ".getList().getElement(" + i + ")");
224                     if (i < list.size() - 1) {
225                         result |= !calculateValue(list.getElement(i));
226                     } else {
227                         result |= calculateValue(list.getElement(i));
228                     }
229                 }
230             } else if (Operators.NEGATION_OPERATOR.equals(op)) {
231                 result = true;
232                 for (int i = 0; i < list.size() && result; i++) {
233                     setLocationWithinModule(context + ".getList().getElement(" + i + ")");
234                     result &= !calculateValue(list.getElement(i));
235                 }
236             } else if (Operators.PREDICATE_VARIABLE.equals(op)) {
237                 setLocationWithinModule(context + ".getList()");
238                 final Entity[] arguments = getEntities(list);
239                 final PredicateVariable var = new PredicateVariable(
240                     list.getElement(0).getAtom().getString(), list.size() - 1);
241                 result = predicateVariableInterpreter.getPredicate(var)
242                     .calculate(arguments);
243             } else if (Operators.UNIVERSAL_QUANTIFIER_OPERATOR.equals(op)) {
244                 result = handleUniversalQuantifier(list);
245             } else if (Operators.EXISTENTIAL_QUANTIFIER_OPERATOR.equals(op)) {
246                 result = handleExistentialQuantifier(list);
247             } else if (Operators.UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR.equals(op)) {
248                 result = handleUniqueExistentialQuantifier(list);
249             } else if (Operators.PREDICATE_CONSTANT.equals(op)) {
250                 final String label = list.getElement(0).getAtom().getString();
251                 String name = label;
252 //                System.out.println(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 = qedeq.getKernelRequiredModules().getKernelQedeqBo(external);
260                     }
261                     if (newProp == null) {
262                         setLocationWithinModule(context + ".getList().getOperator()");
263                         throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_CODE,
264                             HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT + "\"" + external + "\""
265                             + HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT_2 + "\"" + external
266                             + "." + name + "\"",
267                             moduleContext);
268                     }
269                 }
270                 final PredicateKey predicateKey = new PredicateKey(name, "" + (list.size() - 1));
271                 final PredicateConstant constant = (newProp.getExistenceChecker() != null
272                     ? newProp.getExistenceChecker().get(predicateKey) : null);
273                 if (constant != null) {
274                     setLocationWithinModule(context + ".getList()");
275                     final Entity[] arguments = getEntities(list);
276                     setModuleContext(newProp);
277                     moduleContext = new ModuleContext(constant.getContext());
278                     // we must get the second argument of equivalence
279                     moduleContext.setLocationWithinModule(moduleContext.getLocationWithinModule()
280                         + ".getElement(1)");
281                     try {
282                         result = calculatePredicateValue(constant, arguments);
283                     } catch (HeuristicException e) {
284                         setModuleContext(qedeqOld);
285                         moduleContext = moduleContextOld;
286                         setLocationWithinModule(context + ".getList().getElement(1)");
287                         throw new HeuristicException(
288                             HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
289                             HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + predicateKey,
290                             moduleContext, e.getContext());
291                     }
292                 } else {  // should be initial predicate, must be in the model
293                     final ModelPredicateConstant var = new ModelPredicateConstant(name, list.size()
294                         - 1);
295                     final Predicate predicate = model.getPredicateConstant(var);
296                     if (predicate == null) {
297                         setLocationWithinModule(context + ".getList().getOperator()");
298                         throw new HeuristicException(
299                             HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE,
300                             HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT + var,
301                             moduleContext);
302                     }
303                     setLocationWithinModule(context + ".getList()");
304                     final Entity[] arguments = getEntities(list);
305                     result = predicate.calculate(arguments);
306                 }
307             } else {
308                 setLocationWithinModule(context + ".getList().getOperator()");
309                 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_OPERATOR_CODE,
310                     HeuristicErrorCodes.UNKNOWN_OPERATOR_TEXT + op, moduleContext);
311             }
312         } finally {
313 //            qedeq = qedeqOld;
314             setModuleContext(qedeqOld);
315             moduleContext = moduleContextOld;
316             setLocationWithinModule(context);
317         }
318         if (Trace.isDebugEnabled(CLASS)) {
319             deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
320             Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(
321                 null, qedeq.getElement2Latex().getLatex(formula), 0), result);
322         }
323         return result;
324     }
325 
326     /**
327      * Handle universal quantifier operator.
328      *
329      * @param   list    Work on this formula.
330      * @return  result  Calculated truth value.
331      * @throws  HeuristicException  Calculation not possible.
332      */
333     private boolean handleUniversalQuantifier(final ElementList list)
334             throws HeuristicException {
335         final String method = "handleUniversalQuantifier(ElementList)";
336         final String context = getLocationWithinModule();
337         boolean result = true;
338         final ElementList variable = list.getElement(0).getList();
339         final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
340         subjectVariableInterpreter.addSubjectVariable(var);
341         for (int i = 0; i < model.getEntitiesSize(); i++) {
342             if (Trace.isDebugEnabled(CLASS)) {
343                 Trace.param(CLASS, this, method, deepness.toString()
344                     + Latex2UnicodeParser.transform(null, qedeq.getElement2Latex()
345                     .getLatex(variable), 0), model.getEntity(i));
346             }
347             if (list.size() == 2) {
348                 setLocationWithinModule(context + ".getElement(1)");
349                 result &= calculateValue(list.getElement(1));
350             } else {  // must be 3
351                 setLocationWithinModule(context + ".getElement(1)");
352                 final boolean result1 = calculateValue(list.getElement(1));
353                 setLocationWithinModule(context + ".getElement(2)");
354                 final boolean result2 = calculateValue(list.getElement(2));
355                 result &= !result1 || result2;
356             }
357             if (!result) {
358                 break;
359             }
360             subjectVariableInterpreter.increaseSubjectVariableSelection(var);
361         }
362         subjectVariableInterpreter.removeSubjectVariable(var);
363         return result;
364     }
365 
366     /**
367      * Handle existential quantifier operator.
368      *
369      * @param   list    Work on this formula.
370      * @return  result  Calculated truth value.
371      * @throws  HeuristicException  Calculation not possible.
372      */
373     private boolean handleExistentialQuantifier(final ElementList list)
374             throws HeuristicException {
375         final String method = "handleExistentialQuantifier(ElementList)";
376         final String context = getLocationWithinModule();
377         boolean result = false;
378         final ElementList variable = list.getElement(0).getList();
379         final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
380         subjectVariableInterpreter.addSubjectVariable(var);
381         for (int i = 0; i < model.getEntitiesSize(); i++) {
382             if (Trace.isDebugEnabled(CLASS)) {
383                 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser
384                     .transform(null, qedeq.getElement2Latex().getLatex(variable), 0),
385                     model.getEntity(i));
386             }
387             if (list.size() == 2) {
388                 setLocationWithinModule(context + ".getElement(1)");
389                 result |= calculateValue(list.getElement(1));
390             } else {  // must be 3
391                 setLocationWithinModule(context + ".getElement(1)");
392                 final boolean result1 = calculateValue(list.getElement(1));
393                 setLocationWithinModule(context + ".getElement(2)");
394                 final boolean result2 = calculateValue(list.getElement(2));
395                 result |= result1 && result2;
396             }
397             if (result) {
398                 break;
399             }
400             subjectVariableInterpreter.increaseSubjectVariableSelection(var);
401         }
402         subjectVariableInterpreter.removeSubjectVariable(var);
403         return result;
404     }
405 
406     /**
407      * Handle unique existential quantifier operator.
408      *
409      * @param   list            Work on this formula.
410      * @return  result          Calculated truth value.
411      * @throws  HeuristicException  Calculation not possible.
412      */
413     private boolean handleUniqueExistentialQuantifier(final ElementList list)
414             throws HeuristicException {
415         final String method = "handleUniqueExistentialQuantifier(ElementList)";
416         final String context = getLocationWithinModule();
417         boolean result = false;
418         final ElementList variable = list.getElement(0).getList();
419         final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
420         subjectVariableInterpreter.addSubjectVariable(var);
421         for (int i = 0; i < model.getEntitiesSize(); i++) {
422             if (Trace.isDebugEnabled(CLASS)) {
423                 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
424                         qedeq.getElement2Latex().getLatex(variable), 0), model.getEntity(i));
425             }
426             boolean val;
427             if (list.size() == 2) {
428                 setLocationWithinModule(context + ".getList().getElement(1)");
429                 val = calculateValue(list.getElement(1));
430             } else {  // must be 3
431                 setLocationWithinModule(context + ".getList().getElement(1)");
432                 final boolean result1 = calculateValue(list.getElement(1));
433                 setLocationWithinModule(context + ".getList().getElement(2)");
434                 final boolean result2 = calculateValue(list.getElement(2));
435                 val = result1 && result2;
436             }
437             if (val) {
438                 if (result) {
439                     result = false;
440                     break;
441                 }
442                 result = true;
443             }
444             subjectVariableInterpreter.increaseSubjectVariableSelection(var);
445         }
446         subjectVariableInterpreter.removeSubjectVariable(var);
447         return result;
448     }
449 
450     /**
451      * Interpret terms.
452      *
453      * @param   terms           Interpret these terms. The first entry is stripped.
454      * @return  Values.
455      * @throws  HeuristicException evaluation failed.
456      */
457     private Entity[] getEntities(final ElementList terms)
458             throws HeuristicException {
459 //        System.out.println(terms);
460         final String context = getLocationWithinModule();
461         final Entity[] result =  new Entity[terms.size() - 1];    // strip first argument
462         for (int i = 0; i < result.length; i++) {
463 //            System.out.println(i + " " + terms.getElement(i + 1));
464             setLocationWithinModule(context + ".getElement(" + (i + 1) + ")");
465             result[i] = calculateTerm(terms.getElement(i + 1));
466         }
467         setLocationWithinModule(context);
468         return result;
469     }
470 
471     /**
472      * Calculate the term value of a given term. This is done by checking with
473      * a model and certain variable values.
474      *
475      * @param   moduleContext   Where we are within an module.
476      * @param   term            Term.
477      * @return  Entity of model.
478      * @throws  HeuristicException      We couldn't calculate the value.
479      */
480     public Entity calculateTerm(final ModuleContext moduleContext, final Element term)
481             throws  HeuristicException {
482         this.moduleContext = moduleContext;
483         return calculateTerm(term);
484     }
485 
486     /**
487      * Interpret term.
488      *
489      * @param   term    Interpret this term.
490      * @return  Value.
491      * @throws  HeuristicException evaluation failed.
492      */
493     private Entity calculateTerm(final Element term)
494             throws  HeuristicException {
495         final String method = "calculateTerm(Element) ";
496         if (Trace.isDebugEnabled(CLASS)) {
497             Trace.param(CLASS, this, method, deepness.toString() + "term   ", Latex2UnicodeParser.transform(null,
498                     qedeq.getElement2Latex().getLatex(term), 0));
499             deepness.append("-");
500         }
501         if (!term.isList()) {
502             throw new RuntimeException("a term should be a list: " + term);
503         }
504         final KernelQedeqBo qedeqOld = qedeq;
505         final ModuleContext moduleContextOld = new ModuleContext(moduleContext);
506         final String context = getLocationWithinModule();
507         Entity result = null;
508         try {
509             final ElementList termList = term.getList();
510             final String op = termList.getOperator();
511             if (Operators.SUBJECT_VARIABLE.equals(op)) {
512                 final String text = termList.getElement(0).getAtom().getString();
513                 final SubjectVariable var = new SubjectVariable(text);
514                 result = subjectVariableInterpreter.getEntity(var);
515             } else if (Operators.FUNCTION_VARIABLE.equals(op)) {
516                 final FunctionVariable var = new FunctionVariable(termList.getElement(0).getAtom().getString(),
517                     termList.size() - 1);
518                 Function function = functionVariableInterpreter.getFunction(var);
519                 setLocationWithinModule(context + ".getList()");
520                 result = function.map(getEntities(termList));
521             } else if (Operators.FUNCTION_CONSTANT.equals(op)) {
522                 final String label = termList.getElement(0).getAtom().getString();
523                 String name = label;
524                 KernelQedeqBo newProp = qedeq;
525                 if (label.indexOf(".") >= 0) {
526                     name = label.substring(label.indexOf(".") + 1);
527                     final String external = label.substring(0, label.indexOf("."));
528                     newProp = null;
529                     if (qedeq.getKernelRequiredModules() != null) {
530                         newProp = qedeq.getKernelRequiredModules().getKernelQedeqBo(external);
531                     }
532                     if (newProp == null) {
533                         setLocationWithinModule(context + ".getList().getOperator()");
534                         throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_CODE,
535                             HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT + "\"" + external + "\""
536                                 + HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT_2 + "\"" + label + "\"",
537                                 moduleContext);
538                     }
539                 }
540                 final FunctionKey functionKey = new FunctionKey(name, "" + (termList.size() - 1));
541                 FunctionConstant constant
542                     =  newProp.getExistenceChecker().get(functionKey);
543                 if (constant != null) {
544                     setLocationWithinModule(context + ".getList()");
545                     final Entity[] arguments = getEntities(termList);
546                     setModuleContext(newProp);
547                     moduleContext = new ModuleContext(constant.getContext());
548                     // we must get the second argument of equal relation
549                     moduleContext.setLocationWithinModule(moduleContext.getLocationWithinModule() + ".getElement(2)");
550                     try {
551                         result = calculateFunctionValue(constant, arguments);
552                     } catch (HeuristicException e) {
553                         setModuleContext(qedeqOld);
554                         moduleContext = moduleContextOld;
555                         setLocationWithinModule(context + ".getList().getElement(1)");
556                         throw new HeuristicException(HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
557                             HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + functionKey,
558                             moduleContext, e.getContext());
559                     }
560                 } else {
561                     final ModelFunctionConstant var = new ModelFunctionConstant(name,
562                         termList.size() - 1);
563                     Function function = model.getFunctionConstant(var);
564                     if (function == null) {
565                         setLocationWithinModule(context + ".getList().getOperator()");
566                         throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE,
567                             HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT + var, moduleContext);
568                     }
569                     setLocationWithinModule(context + ".getList()");
570                     final Entity[] arguments = getEntities(termList);
571                     result = function.map(arguments);
572                 }
573             } else if (Operators.CLASS_OP.equals(op)) {
574                 List fullfillers = new ArrayList();
575                 ElementList variable = termList.getElement(0).getList();
576                 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
577                 subjectVariableInterpreter.addSubjectVariable(var);
578                 KernelQedeqBo newProp = qedeq;
579                 if (qedeq.getExistenceChecker() != null) {
580                     newProp = qedeq.getExistenceChecker().getClassOperatorModule();
581                 }
582                 final PredicateConstant isSet = newProp.getExistenceChecker().getPredicate("isSet", 1);
583                 if (isSet == null) {
584                     throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
585                             HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + "isSet(*)", moduleContext);
586                 }
587                 for (int i = 0; i < model.getEntitiesSize(); i++) {
588                     setModuleContext(qedeqOld);
589                     moduleContext = moduleContextOld;
590                     setLocationWithinModule(context + ".getList().getElement(1)");
591                     if (calculateValue(termList.getElement(1))) {
592                         setModuleContext(newProp);
593                         moduleContext = newProp.getLabels().getPredicateContext("isSet", 1);
594                         setLocationWithinModule(moduleContext.getLocationWithinModule()
595                             + ".getFormula().getElement().getList().getElement(1)");
596                         try {
597                             if (calculatePredicateValue(isSet, new Entity[] {model.getEntity(i)})) {
598                                 fullfillers.add(model.getEntity(i));
599                             }
600                         } catch (HeuristicException e) {
601                             setModuleContext(qedeqOld);
602                             moduleContext = moduleContextOld;
603                             setLocationWithinModule(context + ".getList().getElement(1)");
604                             throw new HeuristicException(HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
605                                 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + isSet,
606                                 moduleContext, e.getContext());
607                         }
608                     }
609                     subjectVariableInterpreter.increaseSubjectVariableSelection(var);
610                 }
611                 result = model.comprehension((Entity[]) fullfillers.toArray(new Entity[] {}));
612                 subjectVariableInterpreter.removeSubjectVariable(var);
613             } else {
614                 setLocationWithinModule(context + ".getList().getOperator()");
615                 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
616                     HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + op, moduleContext);
617             }
618         } finally {
619 //            qedeq = qedeqOld;
620             setModuleContext(qedeqOld);
621             moduleContext = moduleContextOld;
622 //            System.out.println("module context old: " + moduleContextOld);
623             setLocationWithinModule(context);
624         }
625         if (Trace.isDebugEnabled(CLASS)) {
626             deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
627             Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
628                     qedeq.getElement2Latex().getLatex(term), 0), result);
629        }
630         return result;
631     }
632 
633     private String getLocationWithinModule() {
634         return moduleContext.getLocationWithinModule();
635     }
636 
637     protected ModuleContext getModuleContext() {
638         return moduleContext;
639     }
640 
641     protected void setModuleContext(final KernelQedeqBo qedeq) {
642         this.qedeq = qedeq;
643         moduleContext = new ModuleContext(qedeq.getModuleAddress());
644     }
645 
646     protected void setLocationWithinModule(final String localContext) {
647         moduleContext.setLocationWithinModule(localContext);
648     }
649 
650     /**
651      * Change to next valuation.
652      *
653      * @return  Is there a next new valuation?
654      */
655     public boolean next() {
656         return subjectVariableInterpreter.next() || predicateVariableInterpreter.next()
657             || functionVariableInterpreter.next();
658     }
659 
660     public String toString() {
661         final StringBuffer buffer = new StringBuffer();
662         buffer.append("Current interpretation:\n");
663         buffer.append("\t" + predicateVariableInterpreter + "\n");
664         buffer.append("\t" + subjectVariableInterpreter + "\n");
665         buffer.append("\t" + functionVariableInterpreter);
666         return buffer.toString();
667     }
668 
669     /**
670      * Strips the reference to external modules.
671      *
672      * @param   operator    Might have reference to an external module.
673      * @return  Operator as local reference.
674      */
675     public String stripReference(final String operator) {
676         final int index = operator.lastIndexOf(".");
677         if (index >= 0 && index + 1 < operator.length()) {
678             return operator.substring(index + 1);
679         }
680         return operator;
681     }
682 
683 
684     /**
685      * Is the given predicate constant already defined?
686      *
687      * @param   constant    Predicate constant to check for.
688      * @return  Is the given predicate constant already defined?
689      */
690     public boolean hasPredicateConstant(final ModelPredicateConstant constant) {
691         return null != model.getPredicateConstant(constant);
692     }
693 
694     /**
695      * Is the given function constant already defined?
696      *
697      * @param   constant    Function constant to check for.
698      * @return  Is the given function constant already defined?
699      */
700     public boolean hasFunctionConstant(final ModelFunctionConstant constant) {
701         return null != model.getFunctionConstant(constant);
702     }
703 
704     /**
705      * Clear all variable settings.
706      */
707     public void clearVariables() {
708         subjectVariableInterpreter.clear();
709         predicateVariableInterpreter.clear();
710         functionVariableInterpreter.clear();
711     }
712 
713     /**
714      * Get model.
715      *
716      * @return  Model we work with.
717      */
718     public DynamicModel getModel() {
719         return model;
720     }
721 
722 
723 }