testTautology44: unknown term operator: isSet(*)
testTautology44: unknown term operator: isSet(*)
testTautology44: unknown term operator: isSet(*)
testTautology44: unknown term operator: isSet(*)
Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart9.png 45% of files have more coverage
209   430   63   16.08
96   310   0.3   13
13     4.85  
1    
 
  Interpreter       Line # 34 209 63 89% 0.8899371
 
  (145)
 
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.Operators;
23    import org.qedeq.kernel.bo.logic.common.SubjectVariable;
24    import org.qedeq.kernel.se.base.list.Element;
25    import org.qedeq.kernel.se.base.list.ElementList;
26    import org.qedeq.kernel.se.common.ModuleContext;
27   
28   
29    /**
30    * This class calculates a new truth value for a given formula for a given interpretation.
31    *
32    * @author Michael Meyling
33    */
 
34    public final class Interpreter {
35   
36    /** This class. */
37    private static final Class CLASS = Interpreter.class;
38   
39    /** Model contains entities, functions, predicates. */
40    private final Model model;
41   
42    /** Interpret subject variables. */
43    private final SubjectVariableInterpreter subjectVariableInterpreter;
44   
45    /** Interpret predicate variables. */
46    private final PredicateVariableInterpreter predicateVariableInterpreter;
47   
48    /** Interpret function variables. */
49    private final FunctionVariableInterpreter functionVariableInterpreter;
50   
51    /** Module context. Here were are currently. */
52    private ModuleContext moduleContext;
53   
54    /** For formatting debug trace output. */
55    private final StringBuffer deepness = new StringBuffer();
56   
57    /**
58    * Constructor.
59    *
60    * @param model We work with this model.
61    */
 
62  349 toggle public Interpreter(final Model model) {
63  349 this.model = model;
64  349 subjectVariableInterpreter = new SubjectVariableInterpreter(model);
65  349 predicateVariableInterpreter = new PredicateVariableInterpreter(model);
66  349 functionVariableInterpreter = new FunctionVariableInterpreter(model);
67    }
68   
69    /**
70    * Calculate the truth value of a given formula is a tautology. This is done by checking with
71    * a model and certain variable values.
72    *
73    * @param moduleContext Where we are within an module.
74    * @param formula Formula.
75    * @return Truth value of formula.
76    * @throws HeuristicException We couldn't calculate the value.
77    */
 
78  5950 toggle public boolean calculateValue(final ModuleContext moduleContext, final Element formula)
79    throws HeuristicException {
80  5950 this.moduleContext = moduleContext;
81  5950 Test failure here return calculateValue(formula);
82    }
83   
84    /**
85    * Calculate the truth value of a given formula is a tautology. This is done by checking with
86    * a model and certain variable values.
87    *
88    * @param formula Formula.
89    * @return Truth value of formula.
90    * @throws HeuristicException We couldn't calculate the value.
91    */
 
92  312153 toggle private boolean calculateValue(final Element formula) throws HeuristicException {
93  312153 final String method = "calculateValue(Element)";
94  312153 if (Trace.isDebugEnabled(CLASS)) {
95  0 Trace.param(CLASS, this, method, deepness.toString() + "formula", formula);
96  0 deepness.append("-");
97    }
98  312153 if (formula.isAtom()) {
99  0 throw new HeuristicException(HeuristicErrorCodes.WRONG_CALLING_CONVENTION_CODE,
100    HeuristicErrorCodes.WRONG_CALLING_CONVENTION_TEXT, moduleContext);
101    }
102  312153 String context = getLocationWithinModule();
103  312153 if (!context.endsWith(".getList()")) {
104  306552 context += ".getList()";
105  306552 setLocationWithinModule(context);
106    }
107  312153 final ElementList list = formula.getList();
108  312153 final String op = list.getOperator();
109  312153 boolean result;
110  312153 if (Operators.CONJUNCTION_OPERATOR.equals(op)) {
111  13664 result = true;
112  58491 for (int i = 0; i < list.size(); i++) {
113  44837 setLocationWithinModule(context + ".getElement(" + i + ")");
114  44837 result &= calculateValue(list.getElement(i));
115    }
116  298489 } else if (Operators.DISJUNCTION_OPERATOR.equals(op)) {
117  14706 result = false;
118  68694 for (int i = 0; i < list.size(); i++) {
119  53988 setLocationWithinModule(context + ".getElement(" + i + ")");
120  53988 result |= calculateValue(list.getElement(i));
121    }
122  283783 } else if (Operators.EQUIVALENCE_OPERATOR.equals(op)) {
123  20487 result = true;
124  20487 boolean value = false;
125  61438 for (int i = 0; i < list.size(); i++) {
126  40963 if (i > 0) {
127  20476 setLocationWithinModule(context + ".getElement(" + i + ")");
128  20475 if (value != calculateValue(list.getElement(i))) {
129  4131 result = false;
130    }
131    } else {
132  20487 setLocationWithinModule(context + ".getElement(" + i + ")");
133  20487 Test failure here value = calculateValue(list.getElement(i));
134    }
135    }
136  263296 } else if (Operators.IMPLICATION_OPERATOR.equals(op)) {
137  31468 result = false;
138  94386 for (int i = 0; i < list.size(); i++) {
139  62933 setLocationWithinModule(context + ".getElement(" + i + ")");
140  62933 if (i < list.size() - 1) {
141  31468 result |= !calculateValue(list.getElement(i));
142    } else {
143  31465 result |= calculateValue(list.getElement(i));
144    }
145    }
146  231828 } else if (Operators.NEGATION_OPERATOR.equals(op)) {
147  898 result = true;
148  1796 for (int i = 0; i < list.size(); i++) {
149  898 setLocationWithinModule(context + ".getElement(" + i + ")");
150  898 result &= !calculateValue(list.getElement(i));
151    }
152  230930 } else if (Operators.PREDICATE_VARIABLE.equals(op)) {
153  170603 final PredicateVariable var = new PredicateVariable(list.getElement(0).getAtom().getString(),
154    list.size() - 1);
155  170603 setLocationWithinModule(context);
156  170603 result = predicateVariableInterpreter.getPredicate(var)
157    .calculate(getEntities(list));
158  60327 } else if (Operators.UNIVERSAL_QUANTIFIER_OPERATOR.equals(op)) {
159  36721 result = handleUniversalQuantifier(list);
160  23606 } else if (Operators.EXISTENTIAL_QUANTIFIER_OPERATOR.equals(op)) {
161  16573 result = handleExistentialQuantifier(list);
162  7033 } else if (Operators.UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR.equals(op)) {
163  64 result = handleUniqueExistentialQuantifier(list);
164  6969 } else if (Operators.PREDICATE_CONSTANT.equals(op)) {
165  6969 final String text = stripReference(list.getElement(0).getAtom().getString());
166  6969 final ModelPredicateConstant var = new ModelPredicateConstant(text,
167    list.size() - 1);
168  6969 Predicate predicate = model.getPredicateConstant(var);
169  6969 if (predicate == null) {
170  6 setLocationWithinModule(context + ".getOperator()");
171  6 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE,
172    HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT + var, moduleContext);
173    }
174  6963 setLocationWithinModule(context);
175  6963 Test failure here result = predicate.calculate(getEntities(list));
176    } else {
177  0 setLocationWithinModule(context + ".getOperator()");
178  0 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_OPERATOR_CODE,
179    HeuristicErrorCodes.UNKNOWN_OPERATOR_TEXT + op, moduleContext);
180    }
181  312083 setLocationWithinModule(context);
182  312083 if (Trace.isDebugEnabled(CLASS)) {
183  0 deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
184  0 Trace.param(CLASS, this, method, deepness.toString() + "result ", result);
185    }
186  312083 return result;
187    }
188   
189    /**
190    * Handle universal quantifier operator.
191    *
192    * @param list Work on this formula.
193    * @return result Calculated truth value.
194    * @throws HeuristicException Calculation not possible.
195    */
 
196  36721 toggle private boolean handleUniversalQuantifier(final ElementList list) throws HeuristicException {
197  36721 final String context = getLocationWithinModule();
198  36721 boolean result = true;
199  36721 final ElementList variable = list.getElement(0).getList();
200  36721 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
201  36721 subjectVariableInterpreter.addSubjectVariable(var);
202  73707 for (int i = 0; i < model.getEntitiesSize(); i++) {
203  63937 if (list.size() == 2) {
204  63449 setLocationWithinModule(context + ".getElement(1)");
205  63449 result &= calculateValue(list.getElement(1));
206    } else { // must be 3
207  488 setLocationWithinModule(context + ".getElement(1)");
208  488 final boolean result1 = calculateValue(list.getElement(1));
209  488 setLocationWithinModule(context + ".getElement(2)");
210  488 final boolean result2 = calculateValue(list.getElement(2));
211  488 result &= !result1 || result2;
212    }
213  63935 if (!result) {
214  26949 break;
215    }
216  36986 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
217    }
218  36719 subjectVariableInterpreter.removeSubjectVariable(var);
219  36719 return result;
220    }
221   
222    /**
223    * Handle existential quantifier operator.
224    *
225    * @param list Work on this formula.
226    * @return result Calculated truth value.
227    * @throws HeuristicException Calculation not possible.
228    */
 
229  16573 toggle private boolean handleExistentialQuantifier(final ElementList list) throws HeuristicException {
230  16573 final String context = getLocationWithinModule();
231  16573 boolean result = false;
232  16573 final ElementList variable = list.getElement(0).getList();
233  16573 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
234  16573 subjectVariableInterpreter.addSubjectVariable(var);
235  35433 for (int i = 0; i < model.getEntitiesSize(); i++) {
236  30915 if (list.size() == 2) {
237  30725 setLocationWithinModule(context + ".getElement(1)");
238  30725 result |= calculateValue(list.getElement(1));
239    } else { // must be 3
240  190 setLocationWithinModule(context + ".getElement(1)");
241  190 final boolean result1 = calculateValue(list.getElement(1));
242  190 setLocationWithinModule(context + ".getElement(2)");
243  190 final boolean result2 = calculateValue(list.getElement(2));
244  190 result |= result1 && result2;
245    }
246  30914 if (result) {
247  12054 break;
248    }
249  18860 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
250    }
251  16572 subjectVariableInterpreter.removeSubjectVariable(var);
252  16572 return result;
253    }
254   
255    /**
256    * Handle unique existential quantifier operator.
257    *
258    * @param list Work on this formula.
259    * @return result Calculated truth value.
260    * @throws HeuristicException Calculation not possible.
261    */
 
262  64 toggle private boolean handleUniqueExistentialQuantifier(final ElementList list) throws HeuristicException {
263  64 final String context = getLocationWithinModule();
264  64 boolean result = false;
265  64 final ElementList variable = list.getElement(0).getList();
266  64 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
267  64 subjectVariableInterpreter.addSubjectVariable(var);
268  223 for (int i = 0; i < model.getEntitiesSize(); i++) {
269  164 boolean val;
270  164 if (list.size() == 2) {
271  53 setLocationWithinModule(context + ".getElement(1)");
272  53 val = calculateValue(list.getElement(1));
273    } else { // must be 3
274  111 setLocationWithinModule(context + ".getElement(1)");
275  111 final boolean result1 = calculateValue(list.getElement(1));
276  111 setLocationWithinModule(context + ".getElement(2)");
277  111 final boolean result2 = calculateValue(list.getElement(2));
278  111 val = result1 && result2;
279    }
280  164 if (val) {
281  45 if (result) {
282  5 result = false;
283  5 break;
284    }
285  40 result = true;
286    }
287  159 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
288    }
289  64 subjectVariableInterpreter.removeSubjectVariable(var);
290  64 return result;
291    }
292   
293    /**
294    * Interpret terms.
295    *
296    * @param terms Interpret these terms. The first entry is stripped.
297    * @return Values.
298    * @throws HeuristicException evaluation failed.
299    */
 
300  179482 toggle private Entity[] getEntities(final ElementList terms)
301    throws HeuristicException {
302  179482 final String context = getLocationWithinModule();
303  179482 final Entity[] result = new Entity[terms.size() - 1]; // strip first argument
304  321350 for (int i = 0; i < result.length; i++) {
305  141892 setLocationWithinModule(context + ".getElement(" + (i + 1) + ")");
306  141892 Test failure here result[i] = calculateTerm(terms.getElement(i + 1));
307    }
308  179458 setLocationWithinModule(context);
309  179458 return result;
310    }
311   
312    /**
313    * Interpret term.
314    *
315    * @param term Interpret this term.
316    * @return Value.
317    * @throws HeuristicException evaluation failed.
318    */
 
319  141892 toggle private Entity calculateTerm(final Element term)
320    throws HeuristicException {
321  141892 final String method = "calculateTerm(Element) ";
322  141892 if (Trace.isDebugEnabled(CLASS)) {
323  0 Trace.param(CLASS, this, method, deepness.toString() + "term ", term);
324  0 deepness.append("-");
325    }
326  141892 if (!term.isList()) {
327  0 throw new RuntimeException("a term should be a list: " + term);
328    }
329  141892 final String context = getLocationWithinModule();
330  141892 final ElementList termList = term.getList();
331  141892 final String op = termList.getOperator();
332  141892 Entity result = null;
333  141892 if (Operators.SUBJECT_VARIABLE.equals(op)) {
334  137637 final String text = stripReference(termList.getElement(0).getAtom().getString());
335  137637 final SubjectVariable var = new SubjectVariable(text);
336  137637 result = subjectVariableInterpreter.getEntity(var);
337  4255 } else if (Operators.FUNCTION_VARIABLE.equals(op)) {
338  186 final FunctionVariable var = new FunctionVariable(termList.getElement(0).getAtom().getString(),
339    termList.size() - 1);
340  186 Function function = functionVariableInterpreter.getFunction(var);
341  186 setLocationWithinModule(context + ".getList()");
342  186 result = function.map(getEntities(termList));
343  4069 } else if (Operators.FUNCTION_CONSTANT.equals(op)) {
344  1750 final String text = stripReference(termList.getElement(0).getAtom().getString());
345  1750 final ModelFunctionConstant var = new ModelFunctionConstant(text,
346    termList.size() - 1);
347  1750 Function function = model.getFunctionConstant(var);
348  1750 if (function == null) {
349  20 setLocationWithinModule(context + ".getList().getOperator()");
350  20 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE,
351    HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT + var, moduleContext);
352    }
353  1730 setLocationWithinModule(context + ".getList()");
354  1730 result = function.map(getEntities(termList));
355  2319 } else if (Operators.CLASS_OP.equals(op)) {
356  2319 List fullfillers = new ArrayList();
357  2319 ElementList variable = termList.getElement(0).getList();
358  2319 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
359  2319 subjectVariableInterpreter.addSubjectVariable(var);
360  2319 final ModelPredicateConstant isSetPredicate = new ModelPredicateConstant("isSet", 1);
361  2319 Predicate isSet = model.getPredicateConstant(isSetPredicate);
362  2315 if (isSet == null) {
363  0 Test failure here throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
364    HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + "isSet(*)", moduleContext);
365    }
366  9094 for (int i = 0; i < model.getEntitiesSize(); i++) {
367  6779 setLocationWithinModule(context + ".getList().getElement(1)");
368  6779 if (calculateValue(termList.getElement(1))
369    && isSet.calculate(new Entity[] {model.getEntity(i)})) {
370  2247 fullfillers.add(model.getEntity(i));
371    }
372  6779 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
373    }
374  2315 result = model.comprehension((Entity[]) fullfillers.toArray(new Entity[] {}));
375  2315 subjectVariableInterpreter.removeSubjectVariable(var);
376    } else {
377  0 setLocationWithinModule(context + ".getList().getOperator()");
378  0 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
379    HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + op, moduleContext);
380    }
381  141868 setLocationWithinModule(context);
382  141868 if (Trace.isDebugEnabled(CLASS)) {
383  0 deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
384  0 Trace.param(CLASS, this, method, deepness.toString() + "result ", result);
385    }
386  141868 return result;
387    }
388   
 
389  686885 toggle private String getLocationWithinModule() {
390  686885 return moduleContext.getLocationWithinModule();
391    }
392   
 
393  1567564 toggle private void setLocationWithinModule(final String localContext) {
394  1567564 moduleContext.setLocationWithinModule(localContext);
395    }
396   
397    /**
398    * Change to next valuation.
399    *
400    * @return Is there a next new valuation?
401    */
 
402  5862 toggle public boolean next() {
403  5862 return subjectVariableInterpreter.next() || predicateVariableInterpreter.next()
404    || functionVariableInterpreter.next();
405    }
406   
 
407  0 toggle public String toString() {
408  0 final StringBuffer buffer = new StringBuffer();
409  0 buffer.append("Current interpretation:\n");
410  0 buffer.append("\t" + predicateVariableInterpreter + "\n");
411  0 buffer.append("\t" + subjectVariableInterpreter + "\n");
412  0 buffer.append("\t" + functionVariableInterpreter);
413  0 return buffer.toString();
414    }
415   
416    /**
417    * Strips the reference to external modules.
418    *
419    * @param operator Might have reference to an external module.
420    * @return Operator as local reference.
421    */
 
422  146356 toggle public String stripReference(final String operator) {
423  146356 final int index = operator.lastIndexOf(".");
424  146356 if (index >= 0 && index + 1 < operator.length()) {
425  2102 return operator.substring(index + 1);
426    }
427  144254 return operator;
428    }
429   
430    }
 
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 .