Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart8.png 62% of files have more coverage
326   726   97   14.17
130   527   0.3   23
23     4.22  
1    
 
  DynamicDirectInterpreter       Line # 41 326 97 76.6% 0.76617956
 
  (52)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, 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.control.DefaultKernelQedeqBo;
30    import org.qedeq.kernel.bo.service.unicode.Latex2UnicodeParser;
31    import org.qedeq.kernel.se.base.list.Element;
32    import org.qedeq.kernel.se.base.list.ElementList;
33    import org.qedeq.kernel.se.common.ModuleContext;
34   
35   
36    /**
37    * This class calculates a new truth value for a given formula for a given interpretation.
38    *
39    * @author Michael Meyling
40    */
 
41    public class DynamicDirectInterpreter {
42   
43    /** This class. */
44    private static final Class CLASS = DynamicDirectInterpreter.class;
45   
46    /** We work with this module. */
47    private KernelQedeqBo qedeq;
48   
49    /** Module context. Here were are currently. */
50    private ModuleContext moduleContext;
51   
52    /** For formatting debug trace output. */
53    private final StringBuffer deepness = new StringBuffer();
54   
55    /** Model contains entities, functions, predicates. */
56    private final DynamicModel model;
57   
58    /** Interpret subject variables. */
59    private final SubjectVariableInterpreter subjectVariableInterpreter;
60   
61    /** Interpret predicate variables. */
62    private final PredicateVariableInterpreter predicateVariableInterpreter;
63   
64    /** Interpret function variables. */
65    private final FunctionVariableInterpreter functionVariableInterpreter;
66   
67    /**
68    * Constructor.
69    *
70    * @param qedeq We work with this module.
71    * @param model We work with this model.
72    */
 
73  52 toggle public DynamicDirectInterpreter(final KernelQedeqBo qedeq, final DynamicModel model) {
74  52 this(qedeq, model, new SubjectVariableInterpreter(model), new PredicateVariableInterpreter(
75    model), new FunctionVariableInterpreter(model));
76    }
77   
78    /**
79    * Constructor.
80    *
81    * @param qedeq We work with this module.
82    * @param model We work with this model.
83    * @param subjectVariableInterpreter Subject variable interpreter.
84    * @param predicateVariableInterpreter Predicate variable interpreter.
85    * @param functionVariableInterpreter Function variable interpreter.
86    */
 
87  52 toggle public DynamicDirectInterpreter(final KernelQedeqBo qedeq, final DynamicModel model,
88    final SubjectVariableInterpreter subjectVariableInterpreter,
89    final PredicateVariableInterpreter predicateVariableInterpreter,
90    final FunctionVariableInterpreter functionVariableInterpreter) {
91  52 this.qedeq = qedeq;
92  52 this.model = model;
93  52 this.subjectVariableInterpreter = subjectVariableInterpreter;
94  52 this.predicateVariableInterpreter = predicateVariableInterpreter;
95  52 this.functionVariableInterpreter = functionVariableInterpreter;
96    }
97   
98    /**
99    * 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  6504 toggle public Entity calculateFunctionValue(final FunctionConstant constant,
107    final Entity[] entities) throws HeuristicException {
108  6504 final List params = constant.getSubjectVariables();
109  17404 for (int i = 0; i < entities.length; i++) {
110  10900 final SubjectVariable var = (SubjectVariable) params.get(i);
111  10900 subjectVariableInterpreter.forceAddSubjectVariable(var, entities[i].getValue());
112    }
113  6504 Entity result;
114  6504 try {
115  6504 result = calculateTerm(constant.getDefiningTerm());
116    } finally {
117  17404 for (int i = entities.length - 1; i >= 0; i--) {
118  10900 final SubjectVariable var = (SubjectVariable) params.get(i);
119  10900 subjectVariableInterpreter.forceRemoveSubjectVariable(var);
120    }
121    }
122  6504 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  12842 toggle public boolean calculatePredicateValue(final PredicateConstant constant,
134    final Entity[] entities) throws HeuristicException {
135  12842 final List params = constant.getSubjectVariables();
136  31646 for (int i = 0; i < entities.length; i++) {
137  18804 final SubjectVariable var = (SubjectVariable) params.get(i);
138  18804 subjectVariableInterpreter.forceAddSubjectVariable(var, entities[i].getValue());
139    }
140  12842 boolean result;
141  12842 try {
142  12842 result = calculateValue(constant.getDefiningFormula());
143    } finally {
144  31646 for (int i = entities.length - 1; i >= 0; i--) {
145  18804 final SubjectVariable var = (SubjectVariable) params.get(i);
146  18804 subjectVariableInterpreter.forceRemoveSubjectVariable(var);
147    }
148    }
149  12842 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  1583 toggle public boolean calculateValue(final ModuleContext moduleContext, final Element formula)
162    throws HeuristicException {
163    // this.startElement = formula;
164  1583 this.moduleContext = new ModuleContext(moduleContext);
165    // this.startContext = new ModuleContext(moduleContext);
166  1583 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  236342 toggle private boolean calculateValue(final Element formula) throws HeuristicException {
178  236342 final String method = "calculateValue(Element)";
179  236342 if (Trace.isDebugEnabled(CLASS)) {
180  0 Trace.param(CLASS, this, method, deepness.toString() + "formula",
181    Latex2UnicodeParser.transform(null, qedeq.getElement2Latex().getLatex(formula), 0));
182  0 deepness.append("-");
183    }
184  236342 if (formula.isAtom()) {
185  0 throw new HeuristicException(HeuristicErrorCodes.WRONG_CALLING_CONVENTION_CODE,
186    HeuristicErrorCodes.WRONG_CALLING_CONVENTION_TEXT, moduleContext);
187    }
188  236342 final KernelQedeqBo qedeqOld = qedeq;
189  236342 final ModuleContext moduleContextOld = new ModuleContext(moduleContext);
190  236342 final String context = getLocationWithinModule();
191  236342 boolean result;
192  236342 try {
193  236342 final ElementList list = formula.getList();
194  236342 setLocationWithinModule(context + ".getList()");
195  236342 final String op = list.getOperator();
196  236342 if (Operators.CONJUNCTION_OPERATOR.equals(op)) {
197  28721 result = true;
198  77925 for (int i = 0; i < list.size() && result; i++) {
199  49204 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
200  49204 result &= calculateValue(list.getElement(i));
201    }
202  207621 } else if (Operators.DISJUNCTION_OPERATOR.equals(op)) {
203  8254 result = false;
204  21658 for (int i = 0; i < list.size() && !result; i++) {
205  13404 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
206  13404 result |= calculateValue(list.getElement(i));
207    }
208  199367 } else if (Operators.EQUIVALENCE_OPERATOR.equals(op)) {
209  11079 result = true;
210  11079 boolean value = false;
211  33237 for (int i = 0; i < list.size() && result; i++) {
212  22158 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
213  22158 if (i > 0) {
214  11079 if (value != calculateValue(list.getElement(i))) {
215  1601 result = false;
216    }
217    } else {
218  11079 value = calculateValue(list.getElement(i));
219    }
220    }
221  188288 } else if (Operators.IMPLICATION_OPERATOR.equals(op)) {
222  19572 result = false;
223  45950 for (int i = 0; i < list.size() && !result; i++) {
224  26378 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
225  26378 if (i < list.size() - 1) {
226  19572 result |= !calculateValue(list.getElement(i));
227    } else {
228  6806 result |= calculateValue(list.getElement(i));
229    }
230    }
231  168716 } else if (Operators.NEGATION_OPERATOR.equals(op)) {
232  1847 result = true;
233  3694 for (int i = 0; i < list.size() && result; i++) {
234  1847 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
235  1847 result &= !calculateValue(list.getElement(i));
236    }
237  166869 } else if (Operators.PREDICATE_VARIABLE.equals(op)) {
238  70997 setLocationWithinModule(context + ".getList()");
239  70997 final Entity[] arguments = getEntities(list);
240  70997 final PredicateVariable var = new PredicateVariable(
241    list.getElement(0).getAtom().getString(), list.size() - 1);
242  70997 result = predicateVariableInterpreter.getPredicate(var)
243    .calculate(arguments);
244  95872 } else if (Operators.UNIVERSAL_QUANTIFIER_OPERATOR.equals(op)) {
245  18502 result = handleUniversalQuantifier(list);
246  77370 } else if (Operators.EXISTENTIAL_QUANTIFIER_OPERATOR.equals(op)) {
247  16913 result = handleExistentialQuantifier(list);
248  60457 } else if (Operators.UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR.equals(op)) {
249  5 result = handleUniqueExistentialQuantifier(list);
250  60452 } else if (Operators.PREDICATE_CONSTANT.equals(op)) {
251  60452 final String label = list.getElement(0).getAtom().getString();
252  60452 String name = label;
253    // System.out.println(label);
254  60452 KernelQedeqBo newProp = qedeq;
255  66944 while (name.indexOf(".") >= 0) {
256  6492 name = name.substring(label.indexOf(".") + 1);
257  6492 final String external = label.substring(0, label.indexOf("."));
258  6492 newProp = null;
259  6492 if (qedeq.getKernelRequiredModules() != null) {
260  6492 newProp = (DefaultKernelQedeqBo)
261    qedeq.getKernelRequiredModules().getQedeqBo(external);
262    }
263  6492 if (newProp == null) {
264  0 setLocationWithinModule(context + ".getList().getOperator()");
265  0 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  60452 final PredicateKey predicateKey = new PredicateKey(name, "" + (list.size() - 1));
273  60452 final PredicateConstant constant = (newProp.getExistenceChecker() != null
274    ? newProp.getExistenceChecker().get(predicateKey) : null);
275  60452 if (constant != null) {
276  6478 setLocationWithinModule(context + ".getList()");
277  6478 final Entity[] arguments = getEntities(list);
278  6478 setModuleContext(newProp);
279  6478 moduleContext = new ModuleContext(constant.getContext());
280    // we must get the second argument of equivalence
281  6478 moduleContext.setLocationWithinModule(moduleContext.getLocationWithinModule()
282    + ".getElement(1)");
283  6478 try {
284  6478 result = calculatePredicateValue(constant, arguments);
285    } catch (HeuristicException e) {
286  0 setModuleContext(qedeqOld);
287  0 moduleContext = moduleContextOld;
288  0 setLocationWithinModule(context + ".getList().getElement(1)");
289  0 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  53974 final ModelPredicateConstant var = new ModelPredicateConstant(name, list.size()
296    - 1);
297  53974 final Predicate predicate = model.getPredicateConstant(var);
298  53974 if (predicate == null) {
299  0 setLocationWithinModule(context + ".getList().getOperator()");
300  0 throw new HeuristicException(
301    HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE,
302    HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT + var,
303    moduleContext);
304    }
305  53974 setLocationWithinModule(context + ".getList()");
306  53974 final Entity[] arguments = getEntities(list);
307  53974 result = predicate.calculate(arguments);
308    }
309    } else {
310  0 setLocationWithinModule(context + ".getList().getOperator()");
311  0 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_OPERATOR_CODE,
312    HeuristicErrorCodes.UNKNOWN_OPERATOR_TEXT + op, moduleContext);
313    }
314    } finally {
315    // qedeq = qedeqOld;
316  236342 setModuleContext(qedeqOld);
317  236342 moduleContext = moduleContextOld;
318  236342 setLocationWithinModule(context);
319    }
320  236342 if (Trace.isDebugEnabled(CLASS)) {
321  0 deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
322  0 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(
323    null, qedeq.getElement2Latex().getLatex(formula), 0), result);
324    }
325  236342 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  18502 toggle private boolean handleUniversalQuantifier(final ElementList list)
336    throws HeuristicException {
337  18502 final String method = "handleUniversalQuantifier(ElementList)";
338  18502 final String context = getLocationWithinModule();
339  18502 boolean result = true;
340  18502 final ElementList variable = list.getElement(0).getList();
341  18502 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
342  18502 subjectVariableInterpreter.addSubjectVariable(var);
343  42311 for (int i = 0; i < model.getEntitiesSize(); i++) {
344  37704 if (Trace.isDebugEnabled(CLASS)) {
345  0 Trace.param(CLASS, this, method, deepness.toString()
346    + Latex2UnicodeParser.transform(null, qedeq.getElement2Latex()
347    .getLatex(variable), 0), model.getEntity(i));
348    }
349  37704 if (list.size() == 2) {
350  37478 setLocationWithinModule(context + ".getElement(1)");
351  37478 result &= calculateValue(list.getElement(1));
352    } else { // must be 3
353  226 setLocationWithinModule(context + ".getElement(1)");
354  226 final boolean result1 = calculateValue(list.getElement(1));
355  226 setLocationWithinModule(context + ".getElement(2)");
356  226 final boolean result2 = calculateValue(list.getElement(2));
357  226 result &= !result1 || result2;
358    }
359  37704 if (!result) {
360  13895 break;
361    }
362  23809 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
363    }
364  18502 subjectVariableInterpreter.removeSubjectVariable(var);
365  18502 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  16913 toggle private boolean handleExistentialQuantifier(final ElementList list)
376    throws HeuristicException {
377  16913 final String method = "handleExistentialQuantifier(ElementList)";
378  16913 final String context = getLocationWithinModule();
379  16913 boolean result = false;
380  16913 final ElementList variable = list.getElement(0).getList();
381  16913 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
382  16913 subjectVariableInterpreter.addSubjectVariable(var);
383  49952 for (int i = 0; i < model.getEntitiesSize(); i++) {
384  44834 if (Trace.isDebugEnabled(CLASS)) {
385  0 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser
386    .transform(null, qedeq.getElement2Latex().getLatex(variable), 0),
387    model.getEntity(i));
388    }
389  44834 if (list.size() == 2) {
390  44834 setLocationWithinModule(context + ".getElement(1)");
391  44834 result |= calculateValue(list.getElement(1));
392    } else { // must be 3
393  0 setLocationWithinModule(context + ".getElement(1)");
394  0 final boolean result1 = calculateValue(list.getElement(1));
395  0 setLocationWithinModule(context + ".getElement(2)");
396  0 final boolean result2 = calculateValue(list.getElement(2));
397  0 result |= result1 && result2;
398    }
399  44834 if (result) {
400  11795 break;
401    }
402  33039 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
403    }
404  16913 subjectVariableInterpreter.removeSubjectVariable(var);
405  16913 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  5 toggle private boolean handleUniqueExistentialQuantifier(final ElementList list)
416    throws HeuristicException {
417  5 final String method = "handleUniqueExistentialQuantifier(ElementList)";
418  5 final String context = getLocationWithinModule();
419  5 boolean result = false;
420  5 final ElementList variable = list.getElement(0).getList();
421  5 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
422  5 subjectVariableInterpreter.addSubjectVariable(var);
423  22 for (int i = 0; i < model.getEntitiesSize(); i++) {
424  18 if (Trace.isDebugEnabled(CLASS)) {
425  0 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
426    qedeq.getElement2Latex().getLatex(variable), 0), model.getEntity(i));
427    }
428  18 boolean val;
429  18 if (list.size() == 2) {
430  18 setLocationWithinModule(context + ".getList().getElement(1)");
431  18 val = calculateValue(list.getElement(1));
432    } else { // must be 3
433  0 setLocationWithinModule(context + ".getList().getElement(1)");
434  0 final boolean result1 = calculateValue(list.getElement(1));
435  0 setLocationWithinModule(context + ".getList().getElement(2)");
436  0 final boolean result2 = calculateValue(list.getElement(2));
437  0 val = result1 && result2;
438    }
439  18 if (val) {
440  6 if (result) {
441  1 result = false;
442  1 break;
443    }
444  5 result = true;
445    }
446  17 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
447    }
448  5 subjectVariableInterpreter.removeSubjectVariable(var);
449  5 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  138097 toggle private Entity[] getEntities(final ElementList terms)
460    throws HeuristicException {
461    // System.out.println(terms);
462  138097 final String context = getLocationWithinModule();
463  138097 final Entity[] result = new Entity[terms.size() - 1]; // strip first argument
464  347464 for (int i = 0; i < result.length; i++) {
465    // System.out.println(i + " " + terms.getElement(i + 1));
466  209367 setLocationWithinModule(context + ".getElement(" + (i + 1) + ")");
467  209367 result[i] = calculateTerm(terms.getElement(i + 1));
468    }
469  138097 setLocationWithinModule(context);
470  138097 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  0 toggle public Entity calculateTerm(final ModuleContext moduleContext, final Element term)
483    throws HeuristicException {
484  0 this.moduleContext = moduleContext;
485  0 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  215871 toggle private Entity calculateTerm(final Element term)
496    throws HeuristicException {
497  215871 final String method = "calculateTerm(Element) ";
498  215871 if (Trace.isDebugEnabled(CLASS)) {
499  0 Trace.param(CLASS, this, method, deepness.toString() + "term ", Latex2UnicodeParser.transform(null,
500    qedeq.getElement2Latex().getLatex(term), 0));
501  0 deepness.append("-");
502    }
503  215871 if (!term.isList()) {
504  0 throw new RuntimeException("a term should be a list: " + term);
505    }
506  215871 final KernelQedeqBo qedeqOld = qedeq;
507  215871 final ModuleContext moduleContextOld = new ModuleContext(moduleContext);
508  215871 final String context = getLocationWithinModule();
509  215871 Entity result = null;
510  215871 try {
511  215871 final ElementList termList = term.getList();
512  215871 final String op = termList.getOperator();
513  215871 if (Operators.SUBJECT_VARIABLE.equals(op)) {
514  202687 final String text = termList.getElement(0).getAtom().getString();
515  202687 final SubjectVariable var = new SubjectVariable(text);
516  202687 result = subjectVariableInterpreter.getEntity(var);
517  13184 } else if (Operators.FUNCTION_VARIABLE.equals(op)) {
518  144 final FunctionVariable var = new FunctionVariable(termList.getElement(0).getAtom().getString(),
519    termList.size() - 1);
520  144 Function function = functionVariableInterpreter.getFunction(var);
521  144 setLocationWithinModule(context + ".getList()");
522  144 result = function.map(getEntities(termList));
523  13040 } else if (Operators.FUNCTION_CONSTANT.equals(op)) {
524  6504 final String label = termList.getElement(0).getAtom().getString();
525  6504 String name = label;
526  6504 KernelQedeqBo newProp = qedeq;
527  6504 if (label.indexOf(".") >= 0) {
528  0 name = label.substring(label.indexOf(".") + 1);
529  0 final String external = label.substring(0, label.indexOf("."));
530  0 newProp = null;
531  0 if (qedeq.getKernelRequiredModules() != null) {
532  0 newProp = (DefaultKernelQedeqBo)
533    qedeq.getKernelRequiredModules().getQedeqBo(external);
534    }
535  0 if (newProp == null) {
536  0 setLocationWithinModule(context + ".getList().getOperator()");
537  0 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  6504 final FunctionKey functionKey = new FunctionKey(name, "" + (termList.size() - 1));
544  6504 FunctionConstant constant
545    = newProp.getExistenceChecker().get(functionKey);
546  6504 if (constant != null) {
547  6504 setLocationWithinModule(context + ".getList()");
548  6504 final Entity[] arguments = getEntities(termList);
549  6504 setModuleContext(newProp);
550  6504 moduleContext = new ModuleContext(constant.getContext());
551    // we must get the second argument of equal relation
552  6504 moduleContext.setLocationWithinModule(moduleContext.getLocationWithinModule() + ".getElement(2)");
553  6504 try {
554  6504 result = calculateFunctionValue(constant, arguments);
555    } catch (HeuristicException e) {
556  0 setModuleContext(qedeqOld);
557  0 moduleContext = moduleContextOld;
558  0 setLocationWithinModule(context + ".getList().getElement(1)");
559  0 throw new HeuristicException(HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
560    HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + functionKey,
561    moduleContext, e.getContext());
562    }
563    } else {
564  0 final ModelFunctionConstant var = new ModelFunctionConstant(name,
565    termList.size() - 1);
566  0 Function function = model.getFunctionConstant(var);
567  0 if (function == null) {
568  0 setLocationWithinModule(context + ".getList().getOperator()");
569  0 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE,
570    HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT + var, moduleContext);
571    }
572  0 setLocationWithinModule(context + ".getList()");
573  0 final Entity[] arguments = getEntities(termList);
574  0 result = function.map(arguments);
575    }
576  6536 } else if (Operators.CLASS_OP.equals(op)) {
577  6536 List fullfillers = new ArrayList();
578  6536 ElementList variable = termList.getElement(0).getList();
579  6536 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
580  6536 subjectVariableInterpreter.addSubjectVariable(var);
581  6536 KernelQedeqBo newProp = qedeq;
582  6536 if (qedeq.getExistenceChecker() != null) {
583  6536 newProp = qedeq.getExistenceChecker().getClassOperatorModule();
584    }
585  6536 final PredicateConstant isSet = newProp.getExistenceChecker().getPredicate("isSet", 1);
586  6536 if (isSet == null) {
587  0 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
588    HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + "isSet(*)", moduleContext);
589    }
590  32680 for (int i = 0; i < model.getEntitiesSize(); i++) {
591  26144 setModuleContext(qedeqOld);
592  26144 moduleContext = moduleContextOld;
593  26144 setLocationWithinModule(context + ".getList().getElement(1)");
594  26144 if (calculateValue(termList.getElement(1))) {
595  6364 setModuleContext(newProp);
596  6364 moduleContext = newProp.getLabels().getPredicateContext("isSet", 1);
597  6364 setLocationWithinModule(moduleContext.getLocationWithinModule()
598    + ".getFormula().getElement().getList().getElement(1)");
599  6364 try {
600  6364 if (calculatePredicateValue(isSet, new Entity[] {model.getEntity(i)})) {
601  4880 fullfillers.add(model.getEntity(i));
602    }
603    } catch (HeuristicException e) {
604  0 setModuleContext(qedeqOld);
605  0 moduleContext = moduleContextOld;
606  0 setLocationWithinModule(context + ".getList().getElement(1)");
607  0 throw new HeuristicException(HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
608    HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + isSet,
609    moduleContext, e.getContext());
610    }
611    }
612  26144 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
613    }
614  6536 result = model.comprehension((Entity[]) fullfillers.toArray(new Entity[] {}));
615  6536 subjectVariableInterpreter.removeSubjectVariable(var);
616    } else {
617  0 setLocationWithinModule(context + ".getList().getOperator()");
618  0 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
619    HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + op, moduleContext);
620    }
621    } finally {
622    // qedeq = qedeqOld;
623  215871 setModuleContext(qedeqOld);
624  215871 moduleContext = moduleContextOld;
625    // System.out.println("module context old: " + moduleContextOld);
626  215871 setLocationWithinModule(context);
627    }
628  215871 if (Trace.isDebugEnabled(CLASS)) {
629  0 deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
630  0 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
631    qedeq.getElement2Latex().getLatex(term), 0), result);
632    }
633  215871 return result;
634    }
635   
 
636  625730 toggle private String getLocationWithinModule() {
637  625730 return moduleContext.getLocationWithinModule();
638    }
639   
 
640  1397904 toggle protected ModuleContext getModuleContext() {
641  1397904 return moduleContext;
642    }
643   
 
644  497703 toggle protected void setModuleContext(final KernelQedeqBo qedeq) {
645  497703 this.qedeq = qedeq;
646  497703 moduleContext = new ModuleContext(qedeq.getModuleAddress());
647    }
648   
 
649  1402397 toggle protected void setLocationWithinModule(final String localContext) {
650  1402397 moduleContext.setLocationWithinModule(localContext);
651    }
652   
653    /**
654    * Change to next valuation.
655    *
656    * @return Is there a next new valuation?
657    */
 
658  1564 toggle public boolean next() {
659  1564 return subjectVariableInterpreter.next() || predicateVariableInterpreter.next()
660    || functionVariableInterpreter.next();
661    }
662   
 
663  0 toggle public String toString() {
664  0 final StringBuffer buffer = new StringBuffer();
665  0 buffer.append("Current interpretation:\n");
666  0 buffer.append("\t" + predicateVariableInterpreter + "\n");
667  0 buffer.append("\t" + subjectVariableInterpreter + "\n");
668  0 buffer.append("\t" + functionVariableInterpreter);
669  0 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  0 toggle public String stripReference(final String operator) {
679  0 final int index = operator.lastIndexOf(".");
680  0 if (index >= 0 && index + 1 < operator.length()) {
681  0 return operator.substring(index + 1);
682    }
683  0 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  1 toggle public boolean hasPredicateConstant(final ModelPredicateConstant constant) {
694  1 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  0 toggle public boolean hasFunctionConstant(final ModelFunctionConstant constant) {
704  0 return null != model.getFunctionConstant(constant);
705    }
706   
707    /**
708    * Clear all variable settings.
709    */
 
710  3 toggle public void clearVariables() {
711  3 subjectVariableInterpreter.clear();
712  3 predicateVariableInterpreter.clear();
713  3 functionVariableInterpreter.clear();
714    }
715   
716    /**
717    * Get model.
718    *
719    * @return Model we work with.
720    */
 
721  0 toggle public DynamicModel getModel() {
722  0 return model;
723    }
724   
725   
726    }
 
CloverReport generated by Clover Code Coverage v3.1.10
Fri May 24 2013 13:47:32 UTC.		   Clover: Open Source License registered to qedeq.org .