Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Jan 11 2007 09:03:50 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 656   Methods: 17
NCLOC: 413   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
FormulaChecker.java 94,5% 97,4% 100% 96,6%
coverage coverage
 1    /* $Id: FormulaChecker.java,v 1.4 2006/10/20 20:23:03 m31 Exp $
 2    *
 3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 4    *
 5    * Copyright 2000-2006, Michael Meyling <mime@qedeq.org>.
 6    *
 7    * "Hilbert II" is free software; you can redistribute
 8    * it and/or modify it under the terms of the GNU General Public
 9    * License as published by the Free Software Foundation; either
 10    * version 2 of the License, or (at your option) any later version.
 11    *
 12    * This program is distributed in the hope that it will be useful,
 13    * but WITHOUT ANY WARRANTY; without even the implied warranty of
 14    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 15    * GNU General Public License for more details.
 16    */
 17   
 18    package org.qedeq.kernel.bo.logic;
 19    /* $Id: CheckException.java,v 1.5 2006/10/20 20:23:03 m31 Exp $
 20    *
 21    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 22    *
 23    * Copyright 2000-2006, Michael Meyling <mime@qedeq.org>.
 24    *
 25    * "Hilbert II" is free software; you can redistribute
 26    * it and/or modify it under the terms of the GNU General Public
 27    * License as published by the Free Software Foundation; either
 28    * version 2 of the License, or (at your option) any later version.
 29    *
 30    * This program is distributed in the hope that it will be useful,
 31    * but WITHOUT ANY WARRANTY; without even the implied warranty of
 32    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 33    * GNU General Public License for more details.
 34    */
 35   
 36    import org.qedeq.kernel.base.list.Atom;
 37    import org.qedeq.kernel.base.list.Element;
 38    import org.qedeq.kernel.base.list.ElementList;
 39    import org.qedeq.kernel.context.ModuleContext;
 40    import org.qedeq.kernel.dto.list.ElementSet;
 41    import org.qedeq.kernel.log.Trace;
 42   
 43   
 44    /**
 45    * This class deals with {@link org.qedeq.kernel.base.list.Element}s which represent a
 46    * formula. It has methods to check those elements for certain criteria.
 47    *
 48    * @version $Revision: 1.4 $
 49    * @author Michael Meyling
 50    */
 51    public final class FormulaChecker implements Operators, FormulaBasicErrors {
 52   
 53    /** Current context during creation. */
 54    private final ModuleContext currentContext;
 55   
 56    /** Existence checker for operators. */
 57    private final ExistenceChecker existenceChecker;
 58   
 59   
 60    /**
 61    * Constructor.
 62    *
 63    * @param context For location information. Important for locating errors.
 64    * @param existenceChecker Existence checker for operators.
 65    * @throws IllegalArgumentException The <code>existenceChecker</code> says the equality
 66    * operator exists but the predicate is not found.
 67    */
 68  421 private FormulaChecker(final ModuleContext context,
 69    final ExistenceChecker existenceChecker) {
 70  421 this.existenceChecker = existenceChecker;
 71  421 if (existenceChecker.equalityOperatorExists()
 72    && !existenceChecker.predicateExists(existenceChecker.getEqualityOperator(), 2)) {
 73  0 throw new IllegalArgumentException("equality predicate should exist, but it doesn't");
 74    }
 75  421 currentContext = new ModuleContext(context);
 76    }
 77   
 78    /**
 79    * Is {@link Element} a formula?
 80    *
 81    * @param element Check this element.
 82    * @param context For location information. Important for locating errors.
 83    * @throws CheckException It is no formula.
 84    */
 85  51 public static final void checkFormula(final Element element, final ModuleContext context)
 86    throws CheckException {
 87  51 checkFormula(element, context, EverythingExists.getInstance());
 88    }
 89   
 90    /**
 91    * Is {@link Element} a formula?
 92    *
 93    * @param element Check this element.
 94    * @param context For location information. Important for locating errors.
 95    * @param existenceChecker Existence checker for operators.
 96    * @throws CheckException It is no formula.
 97    */
 98  326 public static final void checkFormula(final Element element, final ModuleContext context,
 99    final ExistenceChecker existenceChecker) throws CheckException {
 100  326 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 101  326 checker.checkFormula(element);
 102    }
 103   
 104    /**
 105    * Is {@link Element} a term?
 106    *
 107    * @param element Check this element.
 108    * @param context For location information. Important for locating errors.
 109    * @throws CheckException It is no term.
 110    */
 111  21 public static final void checkTerm(final Element element, final ModuleContext context)
 112    throws CheckException {
 113  21 checkTerm(element, context, EverythingExists.getInstance());
 114    }
 115   
 116    /**
 117    * Is {@link Element} a term?
 118    *
 119    * @param element Check this element.
 120    * @param context For location information. Important for locating errors.
 121    * @param existenceChecker Existence checker for operators.
 122    * @throws CheckException It is no term.
 123    */
 124  95 public static final void checkTerm(final Element element, final ModuleContext context,
 125    final ExistenceChecker existenceChecker) throws CheckException {
 126  95 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 127  95 checker.checkTerm(element);
 128    }
 129   
 130    /**
 131    * Is {@link Element} a formula?
 132    *
 133    * @param element Check this element.
 134    * @throws CheckException It is no formula.
 135    */
 136  1770 private final void checkFormula(final Element element)
 137    throws CheckException {
 138  1770 final String method = "checkFormula";
 139  1770 Trace.begin(this, method);
 140  1770 Trace.param(this, method, "element", element);
 141  1770 final String context = getCurrentContext().getLocationWithinModule();
 142  1770 Trace.param(this, method, "context", context);
 143  1770 checkList(element);
 144  1763 final ElementList list = element.getList();
 145  1763 final String operator = list.getOperator();
 146  1763 if (operator.equals(CONJUNCTION_OPERATOR)
 147    || operator.equals(DISJUNCTION_OPERATOR)
 148    || operator.equals(IMPLICATION_OPERATOR)
 149    || operator.equals(EQUIVALENCE_OPERATOR)) {
 150  476 Trace.trace(this, method, "one of (and, or, implication, equivalence) operator found");
 151  476 setLocationWithinModule(context + ".getList()");
 152  476 if (list.size() <= 1) {
 153  9 throw new FormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
 154    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\""
 155    + operator + "\"", element, getCurrentContext());
 156    }
 157  467 if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) {
 158  1 throw new FormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
 159    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\""
 160    + operator + "\"", element, getCurrentContext());
 161    }
 162  466 for (int i = 0; i < list.size(); i++) {
 163  1044 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
 164  1044 checkFormula(list.getElement(i));
 165    }
 166  462 setLocationWithinModule(context + ".getList()");
 167  462 checkFreeAndBoundDisjunct(0, list);
 168  1287 } else if (operator.equals(NEGATION_OPERATOR)) {
 169  38 Trace.trace(this, method, "negation operator found");
 170  38 setLocationWithinModule(context + ".getList()");
 171  38 if (list.size() != 1) {
 172  2 throw new FormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
 173    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
 174    element, getCurrentContext());
 175    }
 176  36 setLocationWithinModule(context + ".getList().getElement(0)");
 177  36 checkFormula(list.getElement(0));
 178  1249 } else if (operator.equals(PREDICATE_VARIABLE)
 179    || operator.equals(PREDICATE_CONSTANT)) {
 180  1031 Trace.trace(this, method, "predicate operator found");
 181  1031 setLocationWithinModule(context + ".getList()");
 182  1031 if (list.size() < 1) {
 183  2 throw new FormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
 184    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
 185    element, getCurrentContext());
 186    }
 187    // check if first argument is an atom
 188  1029 setLocationWithinModule(context + ".getList().getElement(0)");
 189  1029 checkAtomFirst(list.getElement(0));
 190   
 191    // check if rest arguments are terms
 192  1021 for (int i = 1; i < list.size(); i++) {
 193  1423 setLocationWithinModule(context + ".getElement(" + i + ")");
 194  1423 checkTerm(list.getElement(i));
 195    }
 196   
 197  1019 setLocationWithinModule(context + ".getList()");
 198  1019 checkFreeAndBoundDisjunct(1, list);
 199   
 200    // check if predicate is known
 201  1015 if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
 202    list.getElement(0).getAtom().getString(), list.size() - 1)) {
 203  2 throw new FormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
 204    UNKNOWN_PREDICATE_CONSTANT_TEXT, element, getCurrentContext());
 205    }
 206   
 207  218 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 208    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 209    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 210  213 Trace.trace(this, method, "quantifier found");
 211  213 setLocationWithinModule(context);
 212  213 checkQuantifier(element);
 213    } else {
 214  5 setLocationWithinModule(context + ".getOperator()");
 215  5 throw new FormulaCheckException(UNKNOWN_LOGICAL_OPERATOR,
 216    UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"",
 217    element, getCurrentContext());
 218    }
 219    // restore context
 220  1677 setLocationWithinModule(context);
 221  1677 Trace.end(this, method);
 222    }
 223   
 224    /**
 225    * Check quantifier element.
 226    *
 227    * @param element Check this element. Must be a quantifier element.
 228    * @throws CheckException Check failed.
 229    * @throws IllegalArgumentException <code>element.getList().getOperator()</code> is no
 230    * quantifier operator.
 231    */
 232  213 private void checkQuantifier(final Element element) throws CheckException {
 233  213 final String method = "checkQuantifier";
 234  213 Trace.begin(this, method);
 235  213 Trace.param(this, method, "element", element);
 236    // save context
 237  213 final String context = getCurrentContext().getLocationWithinModule();
 238  213 Trace.param(this, method, "context", context);
 239  213 setLocationWithinModule(context + ".getList()");
 240  213 checkList(element);
 241  213 final ElementList list = element.getList();
 242  213 final String operator = list.getOperator();
 243  213 if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 244    && operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 245    && operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 246  0 throw new IllegalArgumentException("quantifier element expected but found: "
 247    + element.toString());
 248    }
 249  213 if (list.size() < 2 || list.size() > 3) {
 250  0 throw new FormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
 251    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
 252    }
 253   
 254    // check if unique existential operator could be used
 255  213 setLocationWithinModule(context + ".getOperator()");
 256  213 if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 257    && !existenceChecker.equalityOperatorExists()) {
 258  0 throw new FormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED,
 259    EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext());
 260    }
 261   
 262    // check if first argument is subject variable
 263  213 setLocationWithinModule(context + ".getList().getElement(" + 0 + ")");
 264  213 checkSubjectVariable(list.getElement(0));
 265   
 266    // check if second argument is a formula
 267  210 setLocationWithinModule(context + ".getList().getElement(" + 1 + ")");
 268  210 checkFormula(list.getElement(1));
 269   
 270  204 setLocationWithinModule(context + ".getList()");
 271    // check if subject variable is not already bound in formula
 272  204 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
 273    list.getElement(0))) {
 274  7 throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 275    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
 276    getCurrentContext());
 277    }
 278  197 if (list.size() > 3) {
 279  0 throw new FormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
 280    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list,
 281    getCurrentContext());
 282    }
 283  197 if (list.size() > 2) {
 284    // check if third argument is a formula
 285  41 setLocationWithinModule(context + ".getList().getElement(" + 2 + ")");
 286  41 checkFormula(list.getElement(2));
 287   
 288  41 setLocationWithinModule(context + ".getList()");
 289    // check if subject variable is not bound in formula
 290  41 if (FormulaChecker.getBoundSubjectVariables(list.getElement(2)).contains(
 291    list.getElement(0))) {
 292  3 throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 293    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2),
 294    getCurrentContext());
 295    }
 296    // the following check restricts the restriction formula for quantifiers
 297    // to formulas that contain the subject variable as free variable
 298  38 setLocationWithinModule(context + ".getList()");
 299  38 if (!getFreeSubjectVariables(list.getElement(1)).contains(
 300    list.getElement(0))) {
 301  4 throw new FormulaCheckException(
 302    SUBJECT_VARIABLE_OCCURS_NOT_IN_RESTRICTION_FORMULA,
 303    SUBJECT_VARIABLE_OCCURS_NOT_IN_RESTRICTION_FORMULA_TEXT,
 304    list.getElement(0), getCurrentContext());
 305    }
 306  34 checkFreeAndBoundDisjunct(1, list);
 307    }
 308    // restore context
 309  178 setLocationWithinModule(context);
 310  178 Trace.end(this, method);
 311    }
 312   
 313    /**
 314    * Is {@link Element} a term?
 315    *
 316    * @param element Check this element.
 317    * @throws CheckException It is no term.
 318    */
 319  2118 private void checkTerm(final Element element) throws CheckException {
 320  2118 final String method = "checkTerm";
 321  2118 Trace.begin(this, method);
 322  2118 Trace.param(this, method, "element", element);
 323    // save current context
 324  2118 final String context = getCurrentContext().getLocationWithinModule();
 325  2118 Trace.param(this, method, "context", context);
 326  2118 checkList(element);
 327  2114 final ElementList list = element.getList();
 328  2114 final String operator = list.getOperator();
 329  2114 if (operator.equals(SUBJECT_VARIABLE)) {
 330  1471 checkSubjectVariable(element);
 331  643 } else if (operator.equals(FUNCTION_CONSTANT)
 332    || operator.equals(FUNCTION_VARIABLE)) {
 333   
 334  516 setLocationWithinModule(context + ".getList()");
 335   
 336    // function constants must have at least a function name
 337  516 if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) {
 338  1 throw new TermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
 339    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
 340    }
 341   
 342    // function variables must have at least a function name and at least one argument
 343  515 if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) {
 344  2 throw new TermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
 345    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
 346    }
 347   
 348    // check if first argument is an atom
 349  513 setLocationWithinModule(context + ".getList().getElement(0)");
 350  513 checkAtomFirst(list.getElement(0));
 351   
 352    // check if all arguments are terms
 353  506 setLocationWithinModule(context + ".getList()");
 354  506 for (int i = 1; i < list.size(); i++) {
 355  600 setLocationWithinModule(context + ".getElement(" + i + ")");
 356  600 checkTerm(list.getElement(i));
 357    }
 358   
 359  505 setLocationWithinModule(context + ".getList()");
 360  505 checkFreeAndBoundDisjunct(1, list);
 361   
 362    // check if function is known
 363  501 setLocationWithinModule(context);
 364  501 if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists(
 365    list.getElement(0).getAtom().getString(), list.size() - 1)) {
 366  2 throw new FormulaCheckException(UNKNOWN_FUNCTION_CONSTANT,
 367    UNKNOWN_FUNCTION_CONSTANT_TEXT, element, getCurrentContext());
 368    }
 369   
 370  127 } else if (operator.equals(CLASS)) {
 371   
 372  116 setLocationWithinModule(context + ".getList()");
 373  116 if (list.size() != 2) {
 374  2 throw new TermCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
 375    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
 376    }
 377    // check if first argument is a subject variable
 378  114 setLocationWithinModule(context + ".getList().getElement(" + 0 + ")");
 379  114 if (!isSubjectVariable(list.getElement(0))) {
 380  1 throw new TermCheckException(SUBJECT_VARIABLE_EXPECTED,
 381    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
 382    }
 383   
 384    // check if the second argument is a formula
 385  113 setLocationWithinModule(context + ".getList().getElement(" + 1 + ")");
 386  113 checkFormula(list.getElement(1));
 387   
 388    // check if class operator is allowed
 389  113 if (!existenceChecker.classOperatorExists()) {
 390  2 throw new FormulaCheckException(CLASS_OPERATOR_STILL_UNKNOWN,
 391    CLASS_OPERATOR_STILL_UNKNOWN_TEXT, element, getCurrentContext());
 392    }
 393   
 394    // check if subject variable is not bound in formula
 395  111 setLocationWithinModule(context + ".getList().getElement(" + 0 + ")");
 396  111 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
 397    list.getElement(0))) {
 398  1 throw new TermCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 399    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(0),
 400    getCurrentContext());
 401    }
 402   
 403    } else {
 404  11 setLocationWithinModule(context + ".getOperator()");
 405  11 throw new TermCheckException(UNKNOWN_TERM_OPERATOR,
 406    UNKNOWN_TERM_OPERATOR_TEXT + "\"" + operator + "\"", element, getCurrentContext());
 407    }
 408    // restore context
 409  2077 setLocationWithinModule(context);
 410  2077 Trace.end(this, method);
 411    }
 412   
 413    /**
 414    * Check if no bound variables are free and vice versa.
 415    * The current context must be at the list element.
 416    *
 417    * @param start Start check with this list position. Beginning with 0.
 418    * @param list List element to check.
 419    * @throws CheckException At least one variable occurs free and bound in different
 420    * sub-elements.
 421    */
 422  2020 private void checkFreeAndBoundDisjunct(final int start,
 423    final ElementList list) throws CheckException {
 424    // save current context
 425  2020 final String context = getCurrentContext().getLocationWithinModule();
 426  2020 final ElementSet free = new ElementSet();
 427  2020 final ElementSet bound = new ElementSet();
 428  2020 for (int i = start; i < list.size(); i++) {
 429  3124 setLocationWithinModule(context + ".getElement(" + i + ")");
 430  3124 final ElementSet newFree
 431    = getFreeSubjectVariables(list.getElement(i));
 432  3124 final ElementSet newBound
 433    = FormulaChecker.getBoundSubjectVariables(list.getElement(i));
 434  3124 final ElementSet interBound = newFree.newIntersection(bound);
 435  3124 if (!interBound.isEmpty()) {
 436  17 throw new FormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
 437    FREE_VARIABLE_ALREADY_BOUND_TEXT
 438    + interBound, list.getElement(i), getCurrentContext());
 439    }
 440  3107 final ElementSet interFree = newBound.newIntersection(free);
 441  3107 if (!interFree.isEmpty()) {
 442  15 throw new FormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
 443    BOUND_VARIABLE_ALREADY_FREE_TEXT
 444    + interFree, list.getElement(i), getCurrentContext());
 445    }
 446  3092 bound.union(newBound);
 447  3092 free.union(newFree);
 448    }
 449    // restore context
 450  1988 setLocationWithinModule(context);
 451    }
 452   
 453   
 454    /**
 455    * Is {@link Element} a subject variable?
 456    *
 457    * @param element Element to look onto.
 458    * @return Is it a subject variable?
 459    */
 460  10986 private final boolean isSubjectVariable(final Element element) {
 461  10986 try {
 462  10986 checkSubjectVariable(element);
 463    } catch (CheckException e) {
 464  6418 return false;
 465    }
 466  4568 return true;
 467    }
 468   
 469   
 470    /**
 471    * Check if {@link Element} is a subject variable.
 472    *
 473    * @param element Check this element.
 474    * @throws CheckException It is no subject variable.
 475    */
 476  12670 private final void checkSubjectVariable(final Element element)
 477    throws CheckException {
 478    // save current context
 479  12670 final String context = getCurrentContext().getLocationWithinModule();
 480  12670 checkList(element);
 481  9803 setLocationWithinModule(context + ".getOperator()");
 482  9803 if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) {
 483  6249 setLocationWithinModule(context + ".getList()");
 484  6249 if (element.getList().size() != 1) {
 485  2 throw new FormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
 486    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, element.getList(), getCurrentContext());
 487    }
 488    // check if first argument is an atom
 489  6247 setLocationWithinModule(context + ".getList().getElement(0)");
 490  6247 checkAtomFirst(element.getList().getElement(0));
 491    } else {
 492  3554 throw new FormulaCheckException(SUBJECT_VARIABLE_EXPECTED,
 493    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
 494    }
 495    // restore context
 496  6246 setLocationWithinModule(context);
 497    }
 498   
 499   
 500    /**
 501    * Return all free subject variables of an element.
 502    *
 503    * @param element Work on this element.
 504    * @return All free subject variables.
 505    */
 506  10872 private final ElementSet getFreeSubjectVariables(final Element element) {
 507  10872 final ElementSet free = new ElementSet();
 508  10872 if (isSubjectVariable(element)) {
 509  4455 free.add(element);
 510  6417 } else if (element.isList()) {
 511  3550 final ElementList list = element.getList();
 512  3550 final String operator = list.getOperator();
 513  3550 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 514    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 515    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
 516    || operator.equals(CLASS)) {
 517  302 for (int i = 1; i < list.size(); i++) {
 518  315 free.union(getFreeSubjectVariables(list.getElement(i)));
 519    }
 520  302 free.remove(list.getElement(0));
 521    } else {
 522  3248 for (int i = 0; i < list.size(); i++) {
 523  7395 free.union(getFreeSubjectVariables(list.getElement(i)));
 524    }
 525    }
 526    }
 527  10872 return free;
 528    }
 529   
 530    /**
 531    * Return all bound subject variables of an element.
 532    *
 533    * @param element Work on this element.
 534    * @return All bound subject variables.
 535    */
 536  18382 public static final ElementSet getBoundSubjectVariables(final Element element) {
 537  18382 final ElementSet bound = new ElementSet();
 538  18382 if (element.isList()) {
 539  9668 ElementList list = element.getList();
 540  9668 final String operator = list.getOperator();
 541    // if operator is quantifier or class term
 542  9668 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 543    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 544    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
 545    || operator.equals(CLASS)) {
 546    // add subject variable to bound list
 547  401 bound.add(list.getElement(0));
 548    // add all bound variables of sub-elements
 549  401 for (int i = 1; i < list.size(); i++) {
 550  419 bound.union(FormulaChecker.getBoundSubjectVariables(
 551    list.getElement(i)));
 552    }
 553    } else {
 554    // add all bound variables of sub-elements
 555  9267 for (int i = 0; i < list.size(); i++) {
 556  14483 bound.union(FormulaChecker.getBoundSubjectVariables(list.getElement(i)));
 557    }
 558    }
 559    }
 560  18382 return bound;
 561    }
 562   
 563    /**
 564    * Check common requirements for list elements that are checked for being a term or formula.
 565    *
 566    * @param element List element.
 567    * @throws ElementCheckException Requirements not fulfilled.
 568    */
 569  16771 private void checkList(final Element element) throws ElementCheckException {
 570    // save current context
 571  16771 final String context = getCurrentContext().getLocationWithinModule();
 572  16771 if (element == null) {
 573  2 throw new ElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
 574    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
 575    }
 576  16769 if (!element.isList()) {
 577  2869 throw new ElementCheckException(LIST_EXPECTED,
 578    LIST_EXPECTED_TEXT, element, getCurrentContext());
 579    }
 580  13900 final ElementList list = element.getList();
 581  13900 setLocationWithinModule(context + ".getList()");
 582  13900 if (list == null) {
 583  2 throw new ElementCheckException(LIST_MUST_NOT_BE_NULL,
 584    LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 585    }
 586  13898 final String operator = list.getOperator();
 587  13898 setLocationWithinModule(context + ".getOperator()");
 588  13898 if (operator == null) {
 589  2 throw new ElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_NULL,
 590    OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT + "\""
 591    + operator + "\"", element, getCurrentContext());
 592    }
 593  13896 if (operator.length() == 0) {
 594  3 throw new ElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_EMPTY,
 595    OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT + "\""
 596    + operator + "\"", element, getCurrentContext());
 597    }
 598    // restore context
 599  13893 setLocationWithinModule(context);
 600    }
 601   
 602    /**
 603    * Check if element is an atom and has valid content. It is assumed, that this element is the
 604    * first of a list.
 605    *
 606    * @param element Check this for an atom.
 607    * @throws ElementCheckException No valid content.
 608    */
 609  7789 private void checkAtomFirst(final Element element) throws ElementCheckException {
 610    // save current context
 611  7789 final String context = getCurrentContext().getLocationWithinModule();
 612  7789 if (element == null) {
 613  0 throw new ElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
 614    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
 615    }
 616  7789 if (!element.isAtom()) { // TODO mime 20061126: this is special?
 617  9 throw new ElementCheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM,
 618    FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, element, getCurrentContext());
 619    }
 620  7780 final Atom atom = element.getAtom();
 621  7780 setLocationWithinModule(context + ".getAtom()");
 622  7780 if (atom == null) {
 623  2 throw new ElementCheckException(ATOM_MUST_NOT_BE_NULL,
 624    ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 625    }
 626  7778 if (atom.getString() == null) {
 627  2 throw new ElementCheckException(ATOM_CONTENT_MUST_NOT_BE_NULL,
 628    ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 629    }
 630  7776 if (atom.getString().length() == 0) {
 631  3 throw new ElementCheckException(ATOM_CONTENT_MUST_NOT_BE_EMPTY,
 632    ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, element, getCurrentContext());
 633    }
 634    // restore context
 635  7773 setLocationWithinModule(context);
 636    }
 637   
 638    /**
 639    * Set location information where are we within the original module.
 640    *
 641    * @param locationWithinModule Location within module.
 642    */
 643  106388 protected void setLocationWithinModule(final String locationWithinModule) {
 644  106388 getCurrentContext().setLocationWithinModule(locationWithinModule);
 645    }
 646   
 647    /**
 648    * Get current context within original.
 649    *
 650    * @return Current context.
 651    */
 652  156278 protected final ModuleContext getCurrentContext() {
 653  156278 return currentContext;
 654    }
 655   
 656    }
 
CloverReport generated by Clover Code Coverage v1.3.10
Do Jan 11 2007 09:22:29 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.