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
215   648   144   7.96
150   385   0.67   27
27     5.33  
1    
 
  FormulaUtility       Line # 33 215 144 72.7% 0.7270408
 
  (74)
 
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.common;
17   
18    import org.qedeq.base.utility.Enumerator;
19    import org.qedeq.base.utility.EqualsUtility;
20    import org.qedeq.kernel.se.base.list.Atom;
21    import org.qedeq.kernel.se.base.list.Element;
22    import org.qedeq.kernel.se.base.list.ElementList;
23    import org.qedeq.kernel.se.dto.list.DefaultAtom;
24    import org.qedeq.kernel.se.dto.list.DefaultElementList;
25    import org.qedeq.kernel.se.dto.list.ElementSet;
26   
27   
28    /**
29    * Some useful static methods for formulas and terms.
30    *
31    * @author Michael Meyling
32    */
 
33    public final class FormulaUtility implements Operators {
34   
35    /**
36    * Constructor.
37    *
38    */
 
39  0 toggle private FormulaUtility() {
40    // nothing to do here
41    }
42   
43    /**
44    * Is {@link Element} a subject variable?
45    *
46    * @param element Element to look onto.
47    * @return Is it a subject variable?
48    */
 
49  1560011 toggle public static final boolean isSubjectVariable(final Element element) {
50  1560011 if (element == null || !element.isList() || element.getList() == null) {
51  878927 return false;
52    }
53  681084 final ElementList list = element.getList();
54  681084 if (list.getOperator().equals(SUBJECT_VARIABLE)) {
55  240054 if (list.size() != 1) {
56  0 return false;
57    }
58  240054 final Element first = element.getList().getElement(0);
59  240054 if (first == null || !first.isAtom() || first.getAtom() == null) {
60  0 return false;
61    }
62  240054 final Atom atom = first.getAtom();
63  240054 if (atom.getString() == null || atom.getAtom().getString() == null
64    || atom.getString().length() == 0) {
65  0 return false;
66    }
67    } else {
68  441030 return false;
69    }
70  240054 return true;
71    }
72   
73    /**
74    * Is {@link Element} a predicate variable?
75    *
76    * @param element Element to look onto.
77    * @return Is it a predicate variable?
78    */
 
79  35 toggle public static final boolean isPredicateVariable(final Element element) {
80  35 return isOperator(PREDICATE_VARIABLE, element);
81    }
82   
83    /**
84    * Is {@link Element} a proposition variable?
85    *
86    * @param element Element to look onto.
87    * @return Is it a proposition variable?
88    */
 
89  109415 toggle public static final boolean isPropositionVariable(final Element element) {
90  109415 return isOperator(PREDICATE_VARIABLE, element) && element.getList().size() <= 1;
91    }
92   
93    /**
94    * Is {@link Element} a function variable?
95    *
96    * @param element Element to look onto.
97    * @return Is it a function variable?
98    */
 
99  0 toggle public static final boolean isFunctionVariable(final Element element) {
100  0 return isOperator(FUNCTION_VARIABLE, element);
101    }
102   
103    /**
104    * Is {@link Element} a predicate constant?
105    *
106    * @param element Element to look onto.
107    * @return Is it a predicate constant?
108    */
 
109  15902 toggle public static final boolean isPredicateConstant(final Element element) {
110  15902 return isOperator(PREDICATE_CONSTANT, element);
111    }
112   
113    /**
114    * Is {@link Element} a function constant?
115    *
116    * @param element Element to look onto.
117    * @return Is it a function constant?
118    */
 
119  15889 toggle public static final boolean isFunctionConstant(final Element element) {
120  15889 return isOperator(FUNCTION_CONSTANT, element);
121    }
122   
123    /**
124    * Is the given element an list with given operator and has as first element an non empty
125    * string atom?
126    *
127    * @param operator Operator.
128    * @param element Check this element.
129    * @return Check successful?
130    */
 
131  141241 toggle public static boolean isOperator(final String operator,
132    final Element element) {
133  141241 return isOperator(operator, element, 0);
134    }
135   
136    /**
137    * Is the given element an list with given operator and has as first element an non empty
138    * string atom?
139    *
140    * @param operator Operator.
141    * @param element Check this element.
142    * @param minArguments Minimum number of arguments (beside the first string atom).
143    * @return Check successful?
144    */
 
145  141241 toggle private static boolean isOperator(final String operator,
146    final Element element, final int minArguments) {
147  141241 if (element == null || !element.isList() || element.getList() == null) {
148  60 return false;
149    }
150  141181 final ElementList list = element.getList();
151  141181 if (list.getOperator().equals(operator)) {
152  58544 if (list.size() < 1 + minArguments) {
153  0 return false;
154    }
155  58544 final Element first = element.getList().getElement(0);
156  58544 if (first == null || !first.isAtom() || first.getAtom() == null) {
157  0 return false;
158    }
159  58544 final Atom atom = first.getAtom();
160  58544 if (atom.getString() == null || atom.getAtom().getString() == null
161    || atom.getString().length() == 0) {
162  0 return false;
163    }
164    } else {
165  82637 return false;
166    }
167  58544 return true;
168    }
169   
170    /**
171    * Return all free subject variables of an element.
172    *
173    * @param element Work on this element.
174    * @return All free subject variables.
175    */
 
176  701848 toggle public static final ElementSet getFreeSubjectVariables(final Element element) {
177  701848 final ElementSet free = new ElementSet();
178  701848 if (isSubjectVariable(element)) {
179  184280 free.add(element);
180  517568 } else if (element.isList()) {
181  303699 final ElementList list = element.getList();
182  303699 if (isBindingOperator(list)) {
183  49304 for (int i = 1; i < list.size(); i++) {
184  24970 free.union(getFreeSubjectVariables(list.getElement(i)));
185    }
186  24334 free.remove(list.getElement(0));
187    } else {
188  768986 for (int i = 0; i < list.size(); i++) {
189  489621 free.union(getFreeSubjectVariables(list.getElement(i)));
190    }
191    }
192    }
193  701848 return free;
194    }
195   
196    /**
197    * Return all bound subject variables of an element.
198    *
199    * @param element Work on this element.
200    * @return All bound subject variables.
201    */
 
202  999248 toggle public static final ElementSet getBoundSubjectVariables(final Element element) {
203  999248 final ElementSet bound = new ElementSet();
204  999248 if (element.isList()) {
205  548306 ElementList list = element.getList();
206    // if operator is quantifier or class term
207  548306 if (isBindingOperator(list)) {
208    // add subject variable to bound list
209  26162 bound.add(list.getElement(0));
210    // add all bound variables of sub-elements
211  53043 for (int i = 1; i < list.size(); i++) {
212  26881 bound.union(getBoundSubjectVariables(
213    list.getElement(i)));
214    }
215    } else {
216    // add all bound variables of sub-elements
217  1293525 for (int i = 0; i < list.size(); i++) {
218  771381 bound.union(getBoundSubjectVariables(list.getElement(i)));
219    }
220    }
221    }
222  999248 return bound;
223    }
224   
225    /**
226    * Return all subject variables of an element.
227    *
228    * @param element Work on this element.
229    * @return All subject variables.
230    */
 
231  632 toggle public static final ElementSet getSubjectVariables(final Element element) {
232  632 final ElementSet all = new ElementSet();
233  632 if (isSubjectVariable(element)) {
234  54 all.add(element);
235  578 } else if (element.isList()) {
236  578 final ElementList list = element.getList();
237  632 for (int i = 1; i < list.size(); i++) {
238  54 all.union(getSubjectVariables(list.getElement(i)));
239    }
240    }
241  632 return all;
242    }
243   
244    /**
245    * Return all predicate variables of an element. The arguments are normalized to subject
246    * variables "x_1", "x_2" and so on.
247    *
248    * @param element Work on this element.
249    * @return All predicate variables of that formula.
250    */
 
251  0 toggle public static final ElementSet getPredicateVariables(final Element element) {
252  0 final ElementSet all = new ElementSet();
253  0 if (isPredicateVariable(element)) {
254  0 final ElementList pred = element.getList();
255  0 final DefaultElementList normalized = new DefaultElementList(pred.getOperator());
256  0 normalized.add(pred.getElement(0));
257  0 for (int i = 1; i < pred.size(); i++) {
258  0 normalized.add(createSubjectVariable("x_" + i));
259    }
260  0 all.add(normalized);
261  0 } else if (element.isList()) {
262  0 final ElementList list = element.getList();
263  0 for (int i = 0; i < list.size(); i++) {
264  0 all.union(getPredicateVariables(list.getElement(i)));
265    }
266    }
267  0 return all;
268    }
269   
270    /**
271    * Return all proposition variables of an element. That are predicate variables with
272    * arity zero.
273    *
274    * @param element Work on this element.
275    * @return All proposition variables of that formula.
276    */
 
277  109415 toggle public static final ElementSet getPropositionVariables(final Element element) {
278  109415 final ElementSet all = new ElementSet();
279  109415 if (isPropositionVariable(element)) {
280  58498 all.add(element);
281  50917 } else if (element.isList()) {
282  50857 final ElementList list = element.getList();
283  152535 for (int i = 0; i < list.size(); i++) {
284  101678 all.union(getPropositionVariables(list.getElement(i)));
285    }
286    }
287  109415 return all;
288    }
289   
290    /**
291    * Return all part formulas of an element.
292    *
293    * @param element Work on this element.
294    * @return All part formulas of that element.
295    */
 
296  35 toggle public static final ElementSet getPartFormulas(final Element element) {
297  35 final ElementSet all = new ElementSet();
298  35 if (element == null || element.isAtom()) {
299  0 return all;
300    }
301  35 final ElementList list = element.getList();
302  35 if (isPredicateVariable(list)) {
303  22 all.add(element);
304  13 } else if (isPredicateConstant(list)) {
305  0 all.add(list);
306  13 } else if (Operators.CONJUNCTION_OPERATOR.equals(list.getOperator())
307    || Operators.DISJUNCTION_OPERATOR.equals(list.getOperator())
308    || Operators.NEGATION_OPERATOR.equals(list.getOperator())
309    || Operators.IMPLICATION_OPERATOR.equals(list.getOperator())
310    || Operators.EQUIVALENCE_OPERATOR.equals(list.getOperator())
311    ) {
312  13 all.add(list);
313  39 for (int i = 0; i < list.size(); i++) {
314  26 all.union(getPartFormulas(list.getElement(i)));
315    }
316  0 } else if (isBindingOperator(list)) {
317  0 all.add(list);
318  0 for (int i = 0; i < list.size(); i++) {
319  0 all.union(getPartFormulas(list.getElement(i)));
320    }
321  0 } else if (isSubjectVariable(list)) {
322    // this is no formula
323  0 } else if (isFunctionVariable(list)) {
324    // this is no formula
325  0 } else if (isFunctionConstant(list)) {
326    // this is no formula
327    } else {
328  0 for (int i = 0; i < list.size(); i++) {
329  0 all.union(getPartFormulas(list.getElement(i)));
330    }
331    }
332  35 return all;
333    }
334   
335    /**
336    * Has the given list an operator that binds a subject variable?
337    *
338    * @param list Check for this operator.
339    * @return Has it an binding operator with subject variable?
340    */
 
341  852428 toggle public static boolean isBindingOperator(final ElementList list) {
342  852428 final String operator = list.getOperator();
343  852428 if (operator == null || list.size() <= 0 || !isSubjectVariable(list.getElement(0))) {
344  801806 return false;
345    }
346  50622 return operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
347    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
348    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
349    || operator.equals(CLASS_OP);
350    }
351   
352    /**
353    * Get relative context of the first difference between the given elements.
354    *
355    * @param first First element.
356    * @param second Second element.
357    * @return Relative path (beginning with ".") of first difference.
358    */
 
359  18 toggle public static String getDifferenceLocation(final Element first, final Element second) {
360  18 final StringBuffer diff = new StringBuffer();
361  18 equal(diff, first, second);
362  18 return diff.toString();
363    }
364   
365    /**
366    * Is there any difference between the two elements? If so, the context has the difference
367    * position.
368    *
369    * @param firstContext Context (might be relative) for first element.
370    * @param first First element.
371    * @param second Second element.
372    * @return Are both elements equal?
373    */
 
374  185 toggle private static boolean equal(final StringBuffer firstContext,
375    final Element first, final Element second) {
376  185 if (first == null) {
377  0 return second == null;
378    }
379  185 if (second == null) {
380  0 return false;
381    }
382  185 if (first.isAtom()) {
383  66 if (!second.isAtom()) {
384  0 return false;
385    }
386  66 return EqualsUtility.equals(first.getAtom().getString(), second.getAtom().getString());
387    }
388  119 if (second.isAtom()) {
389  0 return false;
390    }
391  119 if (!EqualsUtility.equals(first.getList().getOperator(), second.getList().getOperator())) {
392  6 return false;
393    }
394  113 if (first.getList().size() != second.getList().size()) {
395  2 return false;
396    }
397  230 for (int i = 0; i < first.getList().size(); i++) {
398  167 final int length = firstContext.length();
399  167 firstContext.append(".getList().getElement(" + i + ")");
400  167 if (!equal(firstContext, first.getList().getElement(i),
401    second.getList().getElement(i))) {
402  48 return false;
403    }
404  119 firstContext.setLength(length);
405    }
406  63 return true;
407    }
408   
409    /**
410    * Replace bound subject variables at given occurrence by another one.
411    * If goal occurrence number is below number of occurrences within the formula nothing is
412    * changed. Original parts are used, so don't modify the formulas directly.
413    *
414    * @param originalSubjectVariable Replace this subject variable.
415    * @param replacementSubjectVariable By this subject variable.
416    * @param formulaElement This is the formula we work on.
417    * @param occurrenceGoal This is the binding occurrence number.
418    * @param occurreneCurrent Counter how much occurrences we already had.
419    * @return Formula with replaced subject variables.
420    */
 
421  681 toggle public static Element replaceSubjectVariableQuantifier(final Element originalSubjectVariable,
422    final Element replacementSubjectVariable, final Element formulaElement,
423    final int occurrenceGoal, final Enumerator occurreneCurrent) {
424  681 if (formulaElement.isAtom()) {
425  243 return formulaElement;
426    }
427  438 final ElementList formula = formulaElement.getList();
428  438 if (occurreneCurrent.getNumber() > occurrenceGoal) {
429  15 return formula.copy();
430    }
431  423 final ElementList result = new DefaultElementList(formula.getOperator());
432  423 if (isBindingOperator(formula)
433    && formula.getElement(0).equals(originalSubjectVariable)) {
434  56 occurreneCurrent.increaseNumber();
435    // System.out.println("found: " + occurreneCurrent);
436  56 if (occurrenceGoal == occurreneCurrent.getNumber()) {
437    // System.out.println("match: " + occurrenceGoal);
438  43 return formula.replace(originalSubjectVariable,
439    replacementSubjectVariable);
440    }
441    }
442  1007 for (int i = 0; i < formula.size(); i++) {
443  627 result.add(replaceSubjectVariableQuantifier(originalSubjectVariable,
444    replacementSubjectVariable, formula.getElement(i), occurrenceGoal,
445    occurreneCurrent));
446    }
447  380 return result;
448    }
449   
450    /**
451    * Replace function or predicate variable by given term or formula. Old parts are not copied
452    * but taken directly - so don't modify the formulas!
453    *
454    * @param formula Formula we want the replacement take place.
455    * @param operatorVariable Predicate variable or function variable with only subject
456    * variables as arguments.
457    * @param replacement Replacement formula or term with matching subject variables.
458    * <code>operatorVariable</code> might have some subject variables
459    * that are not in <code>replacement</code> and vice versa.
460    * @return Formula where operatorVariable was replaced.
461    */
 
462  75877 toggle public static Element replaceOperatorVariable(final Element formula,
463    final Element operatorVariable, final Element replacement) {
464  75877 if (formula == null || operatorVariable == null || replacement == null
465    || formula.isAtom() || operatorVariable.isAtom() || replacement.isAtom()) {
466  3 return formula;
467    }
468  75874 final ElementList f = formula.getList();
469  75874 final ElementList ov = operatorVariable.getList();
470  75874 final ElementList r = replacement.getList();
471    // check elementary preconditions
472    // System.out.println("ov.size=" + ov.size());
473  75874 if (f.size() < 1 || ov.size() < 1) {
474    // System.out.println("failed elementary conditions");
475  0 return formula;
476    }
477    // construct replacement formula with meta variables
478  75874 Element rn = r;
479  75907 for (int i = 1; i < ov.size(); i++) {
480  33 rn = rn.replace(ov.getElement(i), createMeta(ov.getElement(i)));
481    }
482  75874 return replaceOperatorVariableMeta(formula, operatorVariable, rn);
483    }
484   
485    /**
486    * Replace function or predicate variable by given term or formula. Original parts are used -
487    * so don't modify them!
488    *
489    * @param formula Formula we want the replacement take place.
490    * @param operatorVariable Predicate variable or function variable with only subject
491    * variables as arguments.
492    * @param replacement Replacement formula or term with meta variables instead of
493    * subject variables to replace (matching
494    * <code>operatorVariable</code>).
495    * @return Formula where operatorVariable was replaced.
496    */
 
497  1460058 toggle private static Element replaceOperatorVariableMeta(final Element formula,
498    final Element operatorVariable, final Element replacement) {
499  1460058 if (formula.isAtom() || operatorVariable.isAtom() || replacement.isAtom()) {
500  358440 return formula;
501    }
502  1101618 final ElementList f = formula.getList();
503  1101618 final ElementList ov = operatorVariable.getList();
504  1101618 final ElementList r = replacement.getList();
505  1101618 if (f.size() < 1 || ov.size() < 1) {
506  0 return formula.copy();
507    }
508  1101618 ElementList result;
509  1101618 if (EqualsUtility.equals(f.getOperator(), ov.getOperator()) && f.size() == ov.size()
510    && f.getElement(0).equals(ov.getElement(0))) {
511    // replace meta variables by matching entries
512  230419 result = r;
513  230481 for (int i = 1; i < ov.size(); i++) {
514  62 result = (ElementList) result.replace(createMeta(ov.getElement(i)),
515    replaceOperatorVariableMeta(f.getElement(i), operatorVariable, replacement));
516    }
517    } else {
518  871199 result = new DefaultElementList(f.getOperator());
519  2255321 for (int i = 0; i < f.size(); i++) {
520  1384122 result.add(replaceOperatorVariableMeta(f.getElement(i), operatorVariable,
521    replacement));
522    }
523    }
524  1101618 return result;
525    }
526   
527    /**
528    * Checks if a given term or formula contains a given function or predicate variable with same
529    * size.
530    *
531    * @param formula Formula we want the replacement take place.
532    * @param operatorVariable Predicate variable or function variable with only subject
533    * variables as arguments.
534    * @return Do we have any occurrence?
535    */
 
536  164 toggle public static boolean containsOperatorVariable(final Element formula,
537    final Element operatorVariable) {
538  164 if (formula == null || formula.isAtom() || operatorVariable == null
539    || operatorVariable.isAtom()) {
540  0 return false;
541    }
542  164 final ElementList f = formula.getList();
543  164 final ElementList ov = operatorVariable.getList();
544  164 if (f.size() < 1 || ov.size() < 1) {
545  164 return f.equals(ov);
546    }
547  0 if (EqualsUtility.equals(f.getOperator(), ov.getOperator()) && f.size() == ov.size()
548    && f.getElement(0).equals(ov.getElement(0))) {
549  0 return true;
550    }
551  0 for (int i = 0; i < f.size(); i++) {
552  0 if (containsOperatorVariable(f.getElement(i), operatorVariable)) {
553  0 return true;
554    }
555    }
556  0 return false;
557    }
558   
559    /**
560    * Test if operator occurrence in formula matches always to a formula that contains no subject
561    * variable that is in the given ElementSet of bound subject variables..
562    *
563    * @param formula Formula we want to test the condition.
564    * @param operatorVariable Predicate variable or function variable with only subject
565    * variables as arguments.
566    * @param bound Set of subject variables that are tabu.
567    * @return Formula test was successful.
568    */
 
569  4123 toggle public static boolean testOperatorVariable(final Element formula,
570    final Element operatorVariable, final ElementSet bound) {
571  4123 if (formula.isAtom() || operatorVariable.isAtom()) {
572  1140 return true;
573    }
574  2983 final ElementList f = formula.getList();
575  2983 final ElementList ov = operatorVariable.getList();
576  2983 if (f.size() < 1 || ov.size() < 1) {
577  0 return true;
578    }
579  2983 boolean ok = true;
580  2983 if (EqualsUtility.equals(f.getOperator(), ov.getOperator()) && f.size() == ov.size()
581    && f.getElement(0).equals(ov.getElement(0))) {
582  578 if (!getSubjectVariables(f).intersection(bound).isEmpty()) {
583  0 return false;
584    }
585    } else {
586  6238 for (int i = 0; ok && i < f.size(); i++) {
587  3833 ok = testOperatorVariable(f.getElement(i), operatorVariable, bound);
588    }
589    }
590  2983 return ok;
591    }
592   
593    /**
594    * Is the given formula a simple implication like A =&gt; B.
595    *
596    * @param formula Check this formula.
597    * @return Is the formula a simple implication?
598    */
 
599  25552187 toggle public static boolean isImplication(final Element formula) {
600  25552187 if (formula.isAtom()) {
601  0 return false;
602    }
603  25552187 final ElementList f = formula.getList();
604  25552187 return Operators.IMPLICATION_OPERATOR.equals(f.getList().getOperator())
605    && f.getList().size() == 2;
606    }
607   
608    /**
609    * Create meta variable for subject variable.
610    *
611    * @param subjectVariable Subject variable, we want to have a meta variable for.
612    * @return Resulting meta variable. If we didn't got a subject variable we just
613    * return the original.
614    */
 
615  95 toggle public static Element createMeta(final Element subjectVariable) {
616  95 if (!isSubjectVariable(subjectVariable)) {
617  0 return subjectVariable;
618    }
619  95 final DefaultElementList result = new DefaultElementList(META_VARIABLE);
620  95 result.add(subjectVariable.getList().getElement(0));
621  95 return result;
622    }
623   
624    /**
625    * Create subject variable out of variable name.
626    *
627    * @param subjectVariableName Subject variable name.
628    * @return Resulting subject variable.
629    */
 
630  0 toggle public static Element createSubjectVariable(final String subjectVariableName) {
631  0 final DefaultElementList result = new DefaultElementList(SUBJECT_VARIABLE);
632  0 result.add(new DefaultAtom(subjectVariableName));
633  0 return result;
634    }
635   
636    /**
637    * Create predicate variable out of variable name with no further arguments.
638    *
639    * @param predicateVariableName Predicate variable name.
640    * @return Resulting predicate variable.
641    */
 
642  0 toggle public static Element createPredicateVariable(final String predicateVariableName) {
643  0 final DefaultElementList result = new DefaultElementList(PREDICATE_VARIABLE);
644  0 result.add(new DefaultAtom(predicateVariableName));
645  0 return result;
646    }
647   
648    }
 
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 .