Clover Coverage Report
Coverage timestamp: Sat Sep 18 2010 04:09:52 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../img/srcFileCovDistChart10.png 0% of files have more coverage
279   766   114   13.95
130   492   0.41   20
20     5.7  
1    
 
  FormulaChecker       Line # 44 279 114 94.4% 0.9440559
 
  (31)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2010, 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;
17   
18    import org.qedeq.base.trace.Trace;
19    import org.qedeq.kernel.base.list.Atom;
20    import org.qedeq.kernel.base.list.Element;
21    import org.qedeq.kernel.base.list.ElementList;
22    import org.qedeq.kernel.bo.logic.wf.ElementCheckException;
23    import org.qedeq.kernel.bo.logic.wf.EverythingExists;
24    import org.qedeq.kernel.bo.logic.wf.ExistenceChecker;
25    import org.qedeq.kernel.bo.logic.wf.FormulaBasicErrors;
26    import org.qedeq.kernel.bo.logic.wf.FormulaCheckException;
27    import org.qedeq.kernel.bo.logic.wf.LogicalCheckExceptionList;
28    import org.qedeq.kernel.bo.logic.wf.Operators;
29    import org.qedeq.kernel.bo.logic.wf.TermCheckException;
30    import org.qedeq.kernel.common.ModuleContext;
31    import org.qedeq.kernel.dto.list.ElementSet;
32   
33   
34    /**
35    * This class deals with {@link org.qedeq.kernel.base.list.Element}s which represent a
36    * formula. It has methods to check those elements for being well-formed.
37    *
38    * LATER mime 20070307: here are sometimes error messages that get concatenated with
39    * an {@link org.qedeq.kernel.base.list.ElementList#getOperator()} string. Perhaps these
40    * strings must be translated into the original input format and a mapping must be done.
41    *
42    * @author Michael Meyling
43    */
 
44    public final class FormulaChecker implements Operators, FormulaBasicErrors {
45   
46    // FIXME mime 20080404: we should do that within a JUnit test!
47    // If you want to check if the context information within this class is correct you have to
48    // do the following:
49    // 1. add "private Qedeq qedeq;" as a new field of this class
50    // 2. add DynamicGetter from test project into this package
51    // 3. modify {@link #setLocationWithinModule(String) by calling
52    // DynamicGetter.get(qedeq, getCurrentContext().getLocationWithinModule());
53    // 4. modify the {@link #checkFormula(Element, ModuleContext, ExistenceChecker} by adding
54    // a Qedeq parameter;
55    // 5. modify {@link #checkTerm(Element, ModuleContext, ExistenceChecker) analogous
56   
57    /** This class. */
58    private static final Class CLASS = FormulaChecker.class;
59   
60    /** Current context during creation. */
61    private final ModuleContext currentContext;
62   
63    /** Existence checker for operators. */
64    private final ExistenceChecker existenceChecker;
65   
66    /** All exceptions that occurred during checking. */
67    private final LogicalCheckExceptionList exceptions;
68   
69   
70    /**
71    * Constructor.
72    *
73    * @param context For location information. Important for locating errors.
74    * @param existenceChecker Existence checker for operators.
75    * @throws IllegalArgumentException The <code>existenceChecker</code> says the equality
76    * operator exists but the predicate is not found. This should be a programming
77    * error.
78    */
 
79  1107 toggle private FormulaChecker(final ModuleContext context,
80    final ExistenceChecker existenceChecker) {
81  1107 this.existenceChecker = existenceChecker;
82  1107 if (existenceChecker.identityOperatorExists()
83    && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
84  0 throw new IllegalArgumentException("identy predicate should exist, but it doesn't");
85    }
86  1107 currentContext = new ModuleContext(context);
87  1107 exceptions = new LogicalCheckExceptionList();
88    }
89   
90    /**
91    * Checks if an {@link Element} is a formula. If there are any errors the returned list
92    * (which is always not <code>null</code>) has a size greater zero.
93    *
94    * @param element Check this element.
95    * @param context For location information. Important for locating errors.
96    * @param existenceChecker Existence checker for operators.
97    * @return Collected errors if there are any. Not <code>null</code>.
98    */
 
99  943 toggle public static final LogicalCheckExceptionList checkFormula(final Element element,
100    final ModuleContext context, final ExistenceChecker existenceChecker) {
101  943 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
102  943 checker.checkFormula(element);
103  943 return checker.exceptions;
104    }
105   
106    /**
107    * Checks if an {@link Element} is a formula. All predicates and functions are assumed to exit.
108    * If there are any errors the returned list (which is always not <code>null</code>) has a size
109    * greater zero.
110    * If the existence context is known you should use
111    * {@link #checkFormula(Element, ModuleContext, ExistenceChecker)}.
112    *
113    * @param element Check this element.
114    * @param context For location information. Important for locating errors.
115    * @return Collected errors if there are any. Not <code>null</code>.
116    */
 
117  51 toggle public static final LogicalCheckExceptionList checkFormula(final Element element,
118    final ModuleContext context) {
119  51 return checkFormula(element, context, EverythingExists.getInstance());
120    }
121   
122    /**
123    * Check if {@link Element} is a term. If there are any errors the returned list
124    * (which is always not <code>null</code>) has a size greater zero.
125    *
126    * @param element Check this element.
127    * @param context For location information. Important for locating errors.
128    * @param existenceChecker Existence checker for operators.
129    * @return Collected errors if there are any. Not <code>null</code>.
130    */
 
131  164 toggle public static final LogicalCheckExceptionList checkTerm(final Element element,
132    final ModuleContext context, final ExistenceChecker existenceChecker) {
133  164 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
134  164 checker.checkTerm(element);
135  164 return checker.exceptions;
136    }
137   
138    /**
139    * Check if {@link Element} is a term. If there are any errors the returned list
140    * (which is always not <code>null</code>) has a size greater zero.
141    * If the existence context is known you should use
142    * {@link #checkTerm(Element, ModuleContext, ExistenceChecker)}.
143    *
144    * @param element Check this element.
145    * @param context For location information. Important for locating errors.
146    * @return Collected errors if there are any. Not <code>null</code>.
147    */
 
148  21 toggle public static final LogicalCheckExceptionList checkTerm(final Element element,
149    final ModuleContext context) {
150  21 return checkTerm(element, context, EverythingExists.getInstance());
151    }
152   
153    /**
154    * Is {@link Element} a formula?
155    *
156    * @param element Check this element.
157    */
 
158  9422 toggle private final void checkFormula(final Element element) {
159  9422 final String method = "checkFormula";
160  9422 Trace.begin(CLASS, this, method);
161  9422 Trace.param(CLASS, this, method, "element", element);
162  9422 final String context = getCurrentContext().getLocationWithinModule();
163  9422 Trace.param(CLASS, this, method, "context", context);
164  9422 if (!checkList(element)) {
165  7 return;
166    }
167  9415 final ElementList list = element.getList();
168  9415 final String listContext = context + ".getList()";
169  9415 setLocationWithinModule(listContext);
170  9415 final String operator = list.getOperator();
171  9415 if (operator.equals(CONJUNCTION_OPERATOR)
172    || operator.equals(DISJUNCTION_OPERATOR)
173    || operator.equals(IMPLICATION_OPERATOR)
174    || operator.equals(EQUIVALENCE_OPERATOR)) {
175  3065 Trace.trace(CLASS, this, method,
176    "one of (and, or, implication, equivalence) operator found");
177  3065 if (list.size() <= 1) {
178  9 handleFormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
179    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\""
180    + operator + "\"", element, getCurrentContext());
181  9 return;
182    }
183  3056 if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) {
184  1 handleFormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
185    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\""
186    + operator + "\"", element, getCurrentContext());
187  1 return;
188    }
189  9924 for (int i = 0; i < list.size(); i++) {
190  6869 setLocationWithinModule(listContext + ".getElement(" + i + ")");
191  6869 checkFormula(list.getElement(i));
192    }
193  3055 setLocationWithinModule(listContext);
194  3055 checkFreeAndBoundDisjunct(0, list);
195  6350 } else if (operator.equals(NEGATION_OPERATOR)) {
196  312 Trace.trace(CLASS, this, method, "negation operator found");
197  312 setLocationWithinModule(listContext);
198  312 if (list.size() != 1) {
199  2 handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
200    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
201    element, getCurrentContext());
202  2 return;
203    }
204  310 setLocationWithinModule(listContext + ".getElement(0)");
205  310 checkFormula(list.getElement(0));
206  6038 } else if (operator.equals(PREDICATE_VARIABLE)
207    || operator.equals(PREDICATE_CONSTANT)) {
208  5060 Trace.trace(CLASS, this, method, "predicate operator found");
209  5060 setLocationWithinModule(listContext);
210  5060 if (list.size() < 1) {
211  2 handleFormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
212    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
213    element, getCurrentContext());
214  2 return;
215    }
216    // check if first argument is an atom
217  5058 setLocationWithinModule(listContext + ".getElement(0)");
218  5058 if (!checkAtomFirst(list.getElement(0))) {
219  8 return;
220    }
221   
222    // check if rest arguments are terms
223  10067 for (int i = 1; i < list.size(); i++) {
224  5017 setLocationWithinModule(listContext + ".getElement(" + i + ")");
225  5017 checkTerm(list.getElement(i));
226    }
227   
228  5050 setLocationWithinModule(listContext);
229  5050 checkFreeAndBoundDisjunct(1, list);
230   
231    // check if predicate is known
232  5050 if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
233    list.getElement(0).getAtom().getString(), list.size() - 1)) {
234  9 handleFormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
235    UNKNOWN_PREDICATE_CONSTANT_TEXT + "\""
236    + list.getElement(0).getAtom().getString() + "\" [" + (list.size() - 1) + "]",
237    element, getCurrentContext());
238    }
239   
240  978 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
241    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
242    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
243  972 Trace.trace(CLASS, this, method, "quantifier found");
244  972 setLocationWithinModule(context);
245  972 checkQuantifier(element);
246    } else {
247  6 setLocationWithinModule(listContext + ".getOperator()");
248  6 handleFormulaCheckException(UNKNOWN_LOGICAL_OPERATOR,
249    UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"",
250    element, getCurrentContext());
251    }
252    // restore context
253  9393 setLocationWithinModule(context);
254  9393 Trace.end(CLASS, this, method);
255    }
256   
257    /**
258    * Check quantifier element.
259    *
260    * @param element Check this element. Must be a quantifier element.
261    * @throws IllegalArgumentException <code>element.getList().getOperator()</code> is no
262    * quantifier operator.
263    */
 
264  972 toggle private void checkQuantifier(final Element element) {
265  972 final String method = "checkQuantifier";
266  972 Trace.begin(CLASS, this, method);
267  972 Trace.param(CLASS, this, method, "element", element);
268    // save context
269  972 final String context = getCurrentContext().getLocationWithinModule();
270  972 Trace.param(CLASS, this, method, "context", context);
271  972 checkList(element);
272  972 final ElementList list = element.getList();
273  972 final String listContext = context + ".getList()";
274  972 setLocationWithinModule(listContext);
275  972 final String operator = list.getOperator();
276  972 if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
277    && operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
278    && operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
279  0 throw new IllegalArgumentException("quantifier element expected but found: "
280    + element.toString());
281    }
282  972 if (list.size() < 2 || list.size() > 3) {
283  0 handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
284    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
285  0 return;
286    }
287   
288    // check if unique existential operator could be used
289  972 if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
290    && !existenceChecker.identityOperatorExists()) {
291  0 setLocationWithinModule(listContext + ".getOperator()");
292  0 handleFormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED,
293    EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext());
294    }
295   
296    // check if first argument is subject variable
297  972 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
298  972 checkSubjectVariable(list.getElement(0));
299   
300    // check if second argument is a formula
301  972 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
302  972 checkFormula(list.getElement(1));
303   
304  972 setLocationWithinModule(listContext);
305    // check if subject variable is not already bound in formula
306  972 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
307    list.getElement(0))) {
308  10 handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
309    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
310    getCurrentContext());
311    }
312  972 if (list.size() > 3) {
313  0 handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
314    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list,
315    getCurrentContext());
316  0 return;
317    }
318  972 if (list.size() > 2) {
319    // check if third argument is a formula
320  75 setLocationWithinModule(listContext + ".getElement(" + 2 + ")");
321  75 checkFormula(list.getElement(2));
322   
323    // check if subject variable is not bound in formula
324  75 setLocationWithinModule(listContext);
325  75 if (FormulaChecker.getBoundSubjectVariables(list.getElement(2)).contains(
326    list.getElement(0))) {
327  3 handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
328    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2),
329    getCurrentContext());
330  3 return;
331    }
332  72 setLocationWithinModule(listContext);
333  72 checkFreeAndBoundDisjunct(1, list);
334    }
335    // restore context
336  969 setLocationWithinModule(context);
337  969 Trace.end(CLASS, this, method);
338    }
339   
340    /**
341    * Is {@link Element} a term?
342    *
343    * @param element Check this element.
344    */
 
345  6931 toggle private void checkTerm(final Element element) {
346  6931 final String method = "checkTerm";
347  6931 Trace.begin(CLASS, this, method);
348  6931 Trace.param(CLASS, this, method, "element", element);
349    // save current context
350  6931 final String context = getCurrentContext().getLocationWithinModule();
351  6931 Trace.param(CLASS, this, method, "context", context);
352  6931 if (!checkList(element)) {
353  4 return;
354    }
355  6927 final ElementList list = element.getList();
356  6927 final String listContext = context + ".getList()";
357  6927 setLocationWithinModule(listContext);
358  6927 final String operator = list.getOperator();
359  6927 if (operator.equals(SUBJECT_VARIABLE)) {
360  5167 checkSubjectVariable(element);
361  1760 } else if (operator.equals(FUNCTION_CONSTANT)
362    || operator.equals(FUNCTION_VARIABLE)) {
363   
364    // function constants must have at least a function name
365  1494 if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) {
366  1 handleTermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
367    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
368  1 return;
369    }
370   
371    // function variables must have at least a function name and at least one argument
372  1493 if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) {
373  2 handleTermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
374    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
375  2 return;
376    }
377   
378    // check if first argument is an atom
379  1491 setLocationWithinModule(listContext + ".getElement(0)");
380  1491 if (!checkAtomFirst(list.getElement(0))) {
381  7 return;
382    }
383   
384    // check if all arguments are terms
385  1484 setLocationWithinModule(listContext);
386  3234 for (int i = 1; i < list.size(); i++) {
387  1750 setLocationWithinModule(listContext + ".getElement(" + i + ")");
388  1750 checkTerm(list.getElement(i));
389    }
390   
391  1484 setLocationWithinModule(listContext);
392  1484 checkFreeAndBoundDisjunct(1, list);
393   
394    // check if function is known
395  1484 setLocationWithinModule(listContext);
396  1484 if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists(
397    list.getElement(0).getAtom().getString(), list.size() - 1)) {
398  2 handleFormulaCheckException(UNKNOWN_FUNCTION_CONSTANT,
399    UNKNOWN_FUNCTION_CONSTANT_TEXT + "\""
400    + list.getElement(0).getAtom().getString() + "\"", element,
401    getCurrentContext());
402    }
403   
404  266 } else if (operator.equals(CLASS_OP)) {
405   
406  255 if (list.size() != 2) {
407  2 handleTermCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
408    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
409  2 return;
410    }
411    // check if first argument is a subject variable
412  253 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
413  253 if (!isSubjectVariable(list.getElement(0))) {
414  1 handleTermCheckException(SUBJECT_VARIABLE_EXPECTED,
415    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
416    }
417   
418    // check if the second argument is a formula
419  253 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
420  253 checkFormula(list.getElement(1));
421   
422    // check if class operator is allowed
423  253 setLocationWithinModule(listContext);
424  253 if (!existenceChecker.classOperatorExists()) {
425  2 handleFormulaCheckException(CLASS_OPERATOR_STILL_UNKNOWN,
426    CLASS_OPERATOR_STILL_UNKNOWN_TEXT, element, getCurrentContext());
427    }
428   
429    // check if subject variable is not bound in formula
430  253 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
431  253 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
432    list.getElement(0))) {
433  1 handleTermCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
434    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(0),
435    getCurrentContext());
436    }
437   
438    } else {
439  11 setLocationWithinModule(listContext + ".getOperator()");
440  11 handleTermCheckException(UNKNOWN_TERM_OPERATOR,
441    UNKNOWN_TERM_OPERATOR_TEXT + "\"" + operator + "\"", element, getCurrentContext());
442    }
443    // restore context
444  6915 setLocationWithinModule(context);
445  6915 Trace.end(CLASS, this, method);
446    }
447   
448    /**
449    * Check if no bound variables are free and vice versa.
450    * The current context must be at the list element.
451    *
452    * @param start Start check with this list position. Beginning with 0.
453    * @param list List element to check.
454    */
 
455  9661 toggle private void checkFreeAndBoundDisjunct(final int start,
456    final ElementList list) {
457    // save current context
458  9661 final String context = getCurrentContext().getLocationWithinModule();
459  9661 final ElementSet free = new ElementSet();
460  9661 final ElementSet bound = new ElementSet();
461  23441 for (int i = start; i < list.size(); i++) {
462  13780 setLocationWithinModule(context + ".getElement(" + i + ")");
463  13780 final ElementSet newFree
464    = getFreeSubjectVariables(list.getElement(i));
465  13780 final ElementSet newBound
466    = FormulaChecker.getBoundSubjectVariables(list.getElement(i));
467  13780 final ElementSet interBound = newFree.newIntersection(bound);
468  13780 if (!interBound.isEmpty()) {
469  20 handleFormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
470    FREE_VARIABLE_ALREADY_BOUND_TEXT
471    + interBound, list.getElement(i), getCurrentContext());
472    }
473  13780 final ElementSet interFree = newBound.newIntersection(free);
474  13780 if (!interFree.isEmpty()) {
475  16 handleFormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
476    BOUND_VARIABLE_ALREADY_FREE_TEXT
477    + interFree, list.getElement(i), getCurrentContext());
478    }
479  13780 bound.union(newBound);
480  13780 free.union(newFree);
481    }
482    // restore context
483  9661 setLocationWithinModule(context);
484    }
485   
486   
487    /**
488    * Is {@link Element} a subject variable?
489    *
490    * @param element Element to look onto.
491    * @return Is it a subject variable?
492    */
 
493  52308 toggle private final boolean isSubjectVariable(final Element element) {
494  52308 if (element == null || !element.isList() || element.getList() == null) {
495  14876 return false;
496    }
497  37432 final ElementList list = element.getList();
498  37432 if (list.getOperator().equals(SUBJECT_VARIABLE)) {
499  16217 if (list.size() != 1) {
500  0 return false;
501    }
502  16217 final Element first = element.getList().getElement(0);
503  16217 if (first == null || !first.isAtom() || first.getAtom() == null) {
504  0 return false;
505    }
506  16217 final Atom atom = first.getAtom();
507  16217 if (atom.getString() == null || atom.getAtom().getString() == null
508    || atom.getString().length() == 0) {
509  0 return false;
510    }
511    } else {
512  21215 return false;
513    }
514  16217 return true;
515    }
516   
517   
518    /**
519    * Check if {@link Element} is a subject variable.
520    *
521    * @param element Check this element.
522    * @return Is it a subject variable?
523    */
 
524  6139 toggle private boolean checkSubjectVariable(final Element element) {
525    // throws LogicalCheckException {
526    // save current context
527  6139 final String context = getCurrentContext().getLocationWithinModule();
528  6139 if (!checkList(element)) {
529  0 return false;
530    }
531  6139 setLocationWithinModule(context + ".getList()");
532  6139 if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) {
533  6136 if (element.getList().size() != 1) {
534  2 handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
535    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, element.getList(), getCurrentContext());
536  2 return false;
537    }
538    // check if first argument is an atom
539  6134 setLocationWithinModule(context + ".getList().getElement(0)");
540  6134 if (checkAtomFirst(element.getList().getElement(0))) {
541  6133 return false;
542    }
543    } else {
544  3 setLocationWithinModule(context + ".getList().getOperator()");
545  3 handleFormulaCheckException(SUBJECT_VARIABLE_EXPECTED,
546    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
547  3 return false;
548    }
549    // restore context
550  1 setLocationWithinModule(context);
551  1 return true;
552    }
553   
554   
555    /**
556    * Return all free subject variables of an element.
557    *
558    * @param element Work on this element.
559    * @return All free subject variables.
560    */
 
561  52055 toggle private final ElementSet getFreeSubjectVariables(final Element element) {
562  52055 final ElementSet free = new ElementSet();
563  52055 if (isSubjectVariable(element)) {
564  15965 free.add(element);
565  36090 } else if (element.isList()) {
566  21214 final ElementList list = element.getList();
567  21214 final String operator = list.getOperator();
568  21214 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
569    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
570    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
571    || operator.equals(CLASS_OP)) {
572  3947 for (int i = 1; i < list.size(); i++) {
573  1999 free.union(getFreeSubjectVariables(list.getElement(i)));
574    }
575  1948 free.remove(list.getElement(0));
576    } else {
577  55542 for (int i = 0; i < list.size(); i++) {
578  36276 free.union(getFreeSubjectVariables(list.getElement(i)));
579    }
580    }
581    }
582  52055 return free;
583    }
584   
585    /**
586    * Return all bound subject variables of an element.
587    *
588    * @param element Work on this element.
589    * @return All bound subject variables.
590    */
 
591  79120 toggle public static final ElementSet getBoundSubjectVariables(final Element element) {
592  79120 final ElementSet bound = new ElementSet();
593  79120 if (element.isList()) {
594  43187 ElementList list = element.getList();
595  43187 final String operator = list.getOperator();
596    // if operator is quantifier or class term
597  43187 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
598    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
599    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
600    || operator.equals(CLASS_OP)) {
601    // add subject variable to bound list
602  2221 bound.add(list.getElement(0));
603    // add all bound variables of sub-elements
604  4509 for (int i = 1; i < list.size(); i++) {
605  2288 bound.union(FormulaChecker.getBoundSubjectVariables(
606    list.getElement(i)));
607    }
608    } else {
609    // add all bound variables of sub-elements
610  102718 for (int i = 0; i < list.size(); i++) {
611  61752 bound.union(FormulaChecker.getBoundSubjectVariables(list.getElement(i)));
612    }
613    }
614    }
615  79120 return bound;
616    }
617   
618    /**
619    * Check common requirements for list elements that are checked for being a term or formula.
620    * That includes: is the element a true list, has the operator a non zero size.
621    *
622    * @param element List element.
623    * @return Are the requirements fulfilled?
624    */
 
625  23464 toggle private boolean checkList(final Element element) {
626    // save current context
627  23464 final String context = getCurrentContext().getLocationWithinModule();
628  23464 if (element == null) {
629  2 handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
630    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
631  2 return false;
632    }
633  23462 if (!element.isList()) {
634  2 handleElementCheckException(LIST_EXPECTED,
635    LIST_EXPECTED_TEXT, element, getCurrentContext());
636  2 return false;
637    }
638  23460 final ElementList list = element.getList();
639  23460 setLocationWithinModule(context + ".getList()");
640  23460 if (list == null) {
641  2 handleElementCheckException(LIST_MUST_NOT_BE_NULL,
642    LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
643  2 return false;
644    }
645  23458 final String operator = list.getOperator();
646  23458 setLocationWithinModule(context + ".getList().getOperator()");
647  23458 if (operator == null) {
648  2 handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_NULL,
649    OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT , element,
650    getCurrentContext());
651  2 return false;
652    }
653  23456 if (operator.length() == 0) {
654  3 handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_EMPTY,
655    OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT + "\""
656    + operator + "\"", element, getCurrentContext());
657  3 return false;
658    }
659    // restore context
660  23453 setLocationWithinModule(context);
661  23453 return true;
662    }
663   
664    /**
665    * Check if element is an atom and has valid content. It is assumed, that this element is the
666    * first of a list.
667    *
668    * @param element Check this for an atom.
669    * @return Is the content valid?
670    */
 
671  12683 toggle private boolean checkAtomFirst(final Element element) {
672    // save current context
673  12683 final String context = getCurrentContext().getLocationWithinModule();
674  12683 if (element == null) {
675  0 handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
676    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
677  0 return false;
678    }
679  12683 if (!element.isAtom()) { // TODO mime 20061126: this is special?
680  9 handleElementCheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM,
681    FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, element, getCurrentContext());
682  9 return false;
683    }
684  12674 final Atom atom = element.getAtom();
685  12674 setLocationWithinModule(context + ".getAtom()");
686  12674 if (atom == null) {
687  2 handleElementCheckException(ATOM_MUST_NOT_BE_NULL,
688    ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
689  2 return false;
690    }
691  12672 if (atom.getString() == null) {
692  2 handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_NULL,
693    ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
694  2 return false;
695    }
696  12670 if (atom.getString().length() == 0) {
697  3 handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_EMPTY,
698    ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, element, getCurrentContext());
699  3 return false;
700    }
701    // restore context
702  12667 setLocationWithinModule(context);
703  12667 return true;
704    }
705   
706    /**
707    * Add new {@link FormulaCheckException} to exception list.
708    *
709    * @param code Error code.
710    * @param msg Error message.
711    * @param element Element with error.
712    * @param context Error context.
713    */
 
714  87 toggle private void handleFormulaCheckException(final int code, final String msg,
715    final Element element, final ModuleContext context) {
716  87 final FormulaCheckException ex = new FormulaCheckException(code, msg, element, context);
717  87 exceptions.add(ex);
718    }
719   
720    /**
721    * Add new {@link TermCheckException} to exception list.
722    *
723    * @param code Error code.
724    * @param msg Error message.
725    * @param element Element with error.
726    * @param context Error context.
727    */
 
728  18 toggle private void handleTermCheckException(final int code, final String msg,
729    final Element element, final ModuleContext context) {
730  18 final TermCheckException ex = new TermCheckException(code, msg, element, context);
731  18 exceptions.add(ex);
732    }
733   
734    /**
735    * Add new {@link ElementCheckException} to exception list.
736    *
737    * @param code Error code.
738    * @param msg Error message.
739    * @param element Element with error.
740    * @param context Error context.
741    */
 
742  27 toggle private void handleElementCheckException(final int code, final String msg,
743    final Element element, final ModuleContext context) {
744  27 final ElementCheckException ex = new ElementCheckException(code, msg, element, context);
745  27 exceptions.add(ex);
746    }
747   
748    /**
749    * Set location information where are we within the original module.
750    *
751    * @param locationWithinModule Location within module.
752    */
 
753  209584 toggle protected void setLocationWithinModule(final String locationWithinModule) {
754  209584 getCurrentContext().setLocationWithinModule(locationWithinModule);
755    }
756   
757    /**
758    * Get current context within original.
759    *
760    * @return Current context.
761    */
 
762  278988 toggle protected final ModuleContext getCurrentContext() {
763  278988 return currentContext;
764    }
765   
766    }
 
CloverReport generated by Clover Code Coverage v2.3.1
Sat Sep 18 2010 04:09:52 UTC.		   Clover: Open Source License registered to qedeq.org .