001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.logic.common;
017
018 import org.qedeq.base.utility.Enumerator;
019 import org.qedeq.base.utility.EqualsUtility;
020 import org.qedeq.kernel.se.base.list.Atom;
021 import org.qedeq.kernel.se.base.list.Element;
022 import org.qedeq.kernel.se.base.list.ElementList;
023 import org.qedeq.kernel.se.dto.list.DefaultAtom;
024 import org.qedeq.kernel.se.dto.list.DefaultElementList;
025 import org.qedeq.kernel.se.dto.list.ElementSet;
026
027
028 /**
029 * Some useful static methods for formulas and terms.
030 *
031 * @author Michael Meyling
032 */
033 public final class FormulaUtility implements Operators {
034
035 /**
036 * Constructor.
037 *
038 */
039 private FormulaUtility() {
040 }
041
042 /**
043 * Is {@link Element} a subject variable?
044 *
045 * @param element Element to look onto.
046 * @return Is it a subject variable?
047 */
048 public static final boolean isSubjectVariable(final Element element) {
049 if (element == null || !element.isList() || element.getList() == null) {
050 return false;
051 }
052 final ElementList list = element.getList();
053 if (list.getOperator().equals(SUBJECT_VARIABLE)) {
054 if (list.size() != 1) {
055 return false;
056 }
057 final Element first = element.getList().getElement(0);
058 if (first == null || !first.isAtom() || first.getAtom() == null) {
059 return false;
060 }
061 final Atom atom = first.getAtom();
062 if (atom.getString() == null || atom.getAtom().getString() == null
063 || atom.getString().length() == 0) {
064 return false;
065 }
066 } else {
067 return false;
068 }
069 return true;
070 }
071
072 /**
073 * Is {@link Element} a predicate variable?
074 *
075 * @param element Element to look onto.
076 * @return Is it a predicate variable?
077 */
078 public static final boolean isPredicateVariable(final Element element) {
079 return isOperator(PREDICATE_VARIABLE, element);
080 }
081
082 /**
083 * Is {@link Element} a proposition variable?
084 *
085 * @param element Element to look onto.
086 * @return Is it a proposition variable?
087 */
088 public static final boolean isPropositionVariable(final Element element) {
089 return isOperator(PREDICATE_VARIABLE, element) && element.getList().size() <= 1;
090 }
091
092 /**
093 * Is {@link Element} a function variable?
094 *
095 * @param element Element to look onto.
096 * @return Is it a function variable?
097 */
098 public static final boolean isFunctionVariable(final Element element) {
099 return isOperator(FUNCTION_VARIABLE, element);
100 }
101
102 /**
103 * Is {@link Element} a predicate constant?
104 *
105 * @param element Element to look onto.
106 * @return Is it a predicate constant?
107 */
108 public static final boolean isPredicateConstant(final Element element) {
109 return isOperator(PREDICATE_CONSTANT, element);
110 }
111
112 /**
113 * Is {@link Element} a function constant?
114 *
115 * @param element Element to look onto.
116 * @return Is it a function constant?
117 */
118 public static final boolean isFunctionConstant(final Element element) {
119 return isOperator(FUNCTION_CONSTANT, element);
120 }
121
122 /**
123 * Is the given element an list with given operator and has as first element an non empty
124 * string atom?
125 *
126 * @param operator Operator.
127 * @param element Check this element.
128 * @return Check successful?
129 */
130 public static boolean isOperator(final String operator,
131 final Element element) {
132 return isOperator(operator, element, 0);
133 }
134
135 /**
136 * Is the given element an list with given operator and has as first element an non empty
137 * string atom?
138 *
139 * @param operator Operator.
140 * @param element Check this element.
141 * @param minArguments Minimum number of arguments (beside the first string atom).
142 * @return Check successful?
143 */
144 private static boolean isOperator(final String operator,
145 final Element element, final int minArguments) {
146 if (element == null || !element.isList() || element.getList() == null) {
147 return false;
148 }
149 final ElementList list = element.getList();
150 if (list.getOperator().equals(operator)) {
151 if (list.size() < 1 + minArguments) {
152 return false;
153 }
154 final Element first = element.getList().getElement(0);
155 if (first == null || !first.isAtom() || first.getAtom() == null) {
156 return false;
157 }
158 final Atom atom = first.getAtom();
159 if (atom.getString() == null || atom.getAtom().getString() == null
160 || atom.getString().length() == 0) {
161 return false;
162 }
163 } else {
164 return false;
165 }
166 return true;
167 }
168
169 /**
170 * Return all free subject variables of an element.
171 *
172 * @param element Work on this element.
173 * @return All free subject variables.
174 */
175 public static final ElementSet getFreeSubjectVariables(final Element element) {
176 final ElementSet free = new ElementSet();
177 if (isSubjectVariable(element)) {
178 free.add(element);
179 } else if (element.isList()) {
180 final ElementList list = element.getList();
181 if (isBindingOperator(list)) {
182 for (int i = 1; i < list.size(); i++) {
183 free.union(getFreeSubjectVariables(list.getElement(i)));
184 }
185 free.remove(list.getElement(0));
186 } else {
187 for (int i = 0; i < list.size(); i++) {
188 free.union(getFreeSubjectVariables(list.getElement(i)));
189 }
190 }
191 }
192 return free;
193 }
194
195 /**
196 * Return all bound subject variables of an element.
197 *
198 * @param element Work on this element.
199 * @return All bound subject variables.
200 */
201 public static final ElementSet getBoundSubjectVariables(final Element element) {
202 final ElementSet bound = new ElementSet();
203 if (element.isList()) {
204 ElementList list = element.getList();
205 // if operator is quantifier or class term
206 if (isBindingOperator(list)) {
207 // add subject variable to bound list
208 bound.add(list.getElement(0));
209 // add all bound variables of sub-elements
210 for (int i = 1; i < list.size(); i++) {
211 bound.union(getBoundSubjectVariables(
212 list.getElement(i)));
213 }
214 } else {
215 // add all bound variables of sub-elements
216 for (int i = 0; i < list.size(); i++) {
217 bound.union(getBoundSubjectVariables(list.getElement(i)));
218 }
219 }
220 }
221 return bound;
222 }
223
224 /**
225 * Return all subject variables of an element.
226 *
227 * @param element Work on this element.
228 * @return All subject variables.
229 */
230 public static final ElementSet getSubjectVariables(final Element element) {
231 final ElementSet all = new ElementSet();
232 if (isSubjectVariable(element)) {
233 all.add(element);
234 } else if (element.isList()) {
235 final ElementList list = element.getList();
236 for (int i = 1; i < list.size(); i++) {
237 all.union(getSubjectVariables(list.getElement(i)));
238 }
239 }
240 return all;
241 }
242
243 /**
244 * Return all predicate variables of an element. The arguments are normalized to subject
245 * variables "x_1", "x_2" and so on.
246 *
247 * @param element Work on this element.
248 * @return All predicate variables of that formula.
249 */
250 public static final ElementSet getPredicateVariables(final Element element) {
251 final ElementSet all = new ElementSet();
252 if (isPredicateVariable(element)) {
253 final ElementList pred = element.getList();
254 final DefaultElementList normalized = new DefaultElementList(pred.getOperator());
255 normalized.add(pred.getElement(0));
256 for (int i = 1; i < pred.size(); i++) {
257 normalized.add(createSubjectVariable("x_" + i));
258 }
259 all.add(normalized);
260 } else if (element.isList()) {
261 final ElementList list = element.getList();
262 for (int i = 0; i < list.size(); i++) {
263 all.union(getPredicateVariables(list.getElement(i)));
264 }
265 }
266 return all;
267 }
268
269 /**
270 * Return all proposition variables of an element. That are predicate variables with
271 * arity zero.
272 *
273 * @param element Work on this element.
274 * @return All proposition variables of that formula.
275 */
276 public static final ElementSet getPropositionVariables(final Element element) {
277 final ElementSet all = new ElementSet();
278 if (isPropositionVariable(element)) {
279 all.add(element);
280 } else if (element.isList()) {
281 final ElementList list = element.getList();
282 for (int i = 0; i < list.size(); i++) {
283 all.union(getPropositionVariables(list.getElement(i)));
284 }
285 }
286 return all;
287 }
288
289 /**
290 * Return all part formulas of an element.
291 *
292 * @param element Work on this element.
293 * @return All part formulas of that element.
294 */
295 public static final ElementSet getPartFormulas(final Element element) {
296 final ElementSet all = new ElementSet();
297 if (element == null || element.isAtom()) {
298 return all;
299 }
300 final ElementList list = element.getList();
301 if (isPredicateVariable(list)) {
302 all.add(element);
303 } else if (isPredicateConstant(list)) {
304 all.add(list);
305 } else if (Operators.CONJUNCTION_OPERATOR.equals(list.getOperator())
306 || Operators.DISJUNCTION_OPERATOR.equals(list.getOperator())
307 || Operators.NEGATION_OPERATOR.equals(list.getOperator())
308 || Operators.IMPLICATION_OPERATOR.equals(list.getOperator())
309 || Operators.EQUIVALENCE_OPERATOR.equals(list.getOperator())
310 ) {
311 all.add(list);
312 for (int i = 0; i < list.size(); i++) {
313 all.union(getPartFormulas(list.getElement(i)));
314 }
315 } else if (isBindingOperator(list)) {
316 all.add(list);
317 for (int i = 0; i < list.size(); i++) {
318 all.union(getPartFormulas(list.getElement(i)));
319 }
320 } else if (isSubjectVariable(list)) {
321 } else if (isFunctionVariable(list)) {
322 } else if (isFunctionConstant(list)) {
323 } else {
324 for (int i = 0; i < list.size(); i++) {
325 all.union(getPartFormulas(list.getElement(i)));
326 }
327 }
328 return all;
329 }
330
331 /**
332 * Has the given list an operator that binds a subject variable?
333 *
334 * @param list Check for this operator.
335 * @return Has it an binding operator with subject variable?
336 */
337 public static boolean isBindingOperator(final ElementList list) {
338 final String operator = list.getOperator();
339 if (operator == null || list.size() <= 0 || !isSubjectVariable(list.getElement(0))) {
340 return false;
341 }
342 return operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
343 || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
344 || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
345 || operator.equals(CLASS_OP);
346 }
347
348 /**
349 * Get relative context of the first difference between the given elements.
350 *
351 * @param first First element.
352 * @param second Second element.
353 * @return Relative path (beginning with ".") of first difference.
354 */
355 public static String getDifferenceLocation(final Element first, final Element second) {
356 final StringBuffer diff = new StringBuffer();
357 equal(diff, first, second);
358 return diff.toString();
359 }
360
361 /**
362 * Is there any difference between the two elements? If so, the context has the difference
363 * position.
364 *
365 * @param firstContext Context (might be relative) for first element.
366 * @param first First element.
367 * @param second Second element.
368 * @return Are both elements equal?
369 */
370 private static boolean equal(final StringBuffer firstContext,
371 final Element first, final Element second) {
372 if (first == null) {
373 return second == null;
374 }
375 if (second == null) {
376 return false;
377 }
378 if (first.isAtom()) {
379 if (!second.isAtom()) {
380 return false;
381 }
382 return EqualsUtility.equals(first.getAtom().getString(), second.getAtom().getString());
383 }
384 if (second.isAtom()) {
385 return false;
386 }
387 if (!EqualsUtility.equals(first.getList().getOperator(), second.getList().getOperator())) {
388 return false;
389 }
390 if (first.getList().size() != second.getList().size()) {
391 return false;
392 }
393 for (int i = 0; i < first.getList().size(); i++) {
394 final int length = firstContext.length();
395 firstContext.append(".getList().getElement(" + i + ")");
396 if (!equal(firstContext, first.getList().getElement(i),
397 second.getList().getElement(i))) {
398 return false;
399 }
400 firstContext.setLength(length);
401 }
402 return true;
403 }
404
405 /**
406 * Replace bound subject variables at given occurrence by another one.
407 * If goal occurrence number is below number of occurrences within the formula nothing is
408 * changed. Original parts are used, so don't modify the formulas directly.
409 *
410 * @param originalSubjectVariable Replace this subject variable.
411 * @param replacementSubjectVariable By this subject variable.
412 * @param formulaElement This is the formula we work on.
413 * @param occurrenceGoal This is the binding occurrence number.
414 * @param occurreneCurrent Counter how much occurrences we already had.
415 * @return Formula with replaced subject variables.
416 */
417 public static Element replaceSubjectVariableQuantifier(final Element originalSubjectVariable,
418 final Element replacementSubjectVariable, final Element formulaElement,
419 final int occurrenceGoal, final Enumerator occurreneCurrent) {
420 if (formulaElement.isAtom()) {
421 return formulaElement;
422 }
423 final ElementList formula = formulaElement.getList();
424 if (occurreneCurrent.getNumber() > occurrenceGoal) {
425 return formula.copy();
426 }
427 final ElementList result = new DefaultElementList(formula.getOperator());
428 if (isBindingOperator(formula)
429 && formula.getElement(0).equals(originalSubjectVariable)) {
430 occurreneCurrent.increaseNumber();
431 // System.out.println("found: " + occurreneCurrent);
432 if (occurrenceGoal == occurreneCurrent.getNumber()) {
433 // System.out.println("match: " + occurrenceGoal);
434 return formula.replace(originalSubjectVariable,
435 replacementSubjectVariable);
436 }
437 }
438 for (int i = 0; i < formula.size(); i++) {
439 result.add(replaceSubjectVariableQuantifier(originalSubjectVariable,
440 replacementSubjectVariable, formula.getElement(i), occurrenceGoal,
441 occurreneCurrent));
442 }
443 return result;
444 }
445
446 /**
447 * Replace function or predicate variable by given term or formula. Old parts are not copied
448 * but taken directly - so don't modify the formulas!
449 *
450 * @param formula Formula we want the replacement take place.
451 * @param operatorVariable Predicate variable or function variable with only subject
452 * variables as arguments.
453 * @param replacement Replacement formula or term with matching subject variables.
454 * <code>operatorVariable</code> might have some subject variables
455 * that are not in <code>replacement</code> and vice versa.
456 * @return Formula where operatorVariable was replaced.
457 */
458 public static Element replaceOperatorVariable(final Element formula,
459 final Element operatorVariable, final Element replacement) {
460 if (formula == null || operatorVariable == null || replacement == null
461 || formula.isAtom() || operatorVariable.isAtom() || replacement.isAtom()) {
462 return formula;
463 }
464 final ElementList f = formula.getList();
465 final ElementList ov = operatorVariable.getList();
466 final ElementList r = replacement.getList();
467 // check elementary preconditions
468 // System.out.println("ov.size=" + ov.size());
469 if (f.size() < 1 || ov.size() < 1) {
470 // System.out.println("failed elementary conditions");
471 return formula;
472 }
473 // construct replacement formula with meta variables
474 Element rn = r;
475 for (int i = 1; i < ov.size(); i++) {
476 rn = rn.replace(ov.getElement(i), createMeta(ov.getElement(i)));
477 }
478 return replaceOperatorVariableMeta(formula, operatorVariable, rn);
479 }
480
481 /**
482 * Replace function or predicate variable by given term or formula. Original parts are used -
483 * so don't modify them!
484 *
485 * @param formula Formula we want the replacement take place.
486 * @param operatorVariable Predicate variable or function variable with only subject
487 * variables as arguments.
488 * @param replacement Replacement formula or term with meta variables instead of
489 * subject variables to replace (matching
490 * <code>operatorVariable</code>).
491 * @return Formula where operatorVariable was replaced.
492 */
493 private static Element replaceOperatorVariableMeta(final Element formula,
494 final Element operatorVariable, final Element replacement) {
495 if (formula.isAtom() || operatorVariable.isAtom() || replacement.isAtom()) {
496 return formula;
497 }
498 final ElementList f = formula.getList();
499 final ElementList ov = operatorVariable.getList();
500 final ElementList r = replacement.getList();
501 if (f.size() < 1 || ov.size() < 1) {
502 return formula.copy();
503 }
504 ElementList result;
505 if (f.getOperator() == ov.getOperator() && f.size() == ov.size()
506 && f.getElement(0).equals(ov.getElement(0))) {
507 // replace meta variables by matching entries
508 result = r;
509 for (int i = 1; i < ov.size(); i++) {
510 result = (ElementList) result.replace(createMeta(ov.getElement(i)),
511 replaceOperatorVariableMeta(f.getElement(i), operatorVariable, replacement));
512 }
513 } else {
514 result = new DefaultElementList(f.getOperator());
515 for (int i = 0; i < f.size(); i++) {
516 result.add(replaceOperatorVariableMeta(f.getElement(i), operatorVariable,
517 replacement));
518 }
519 }
520 return result;
521 }
522
523 /**
524 * Checks if a given term or formula contains a given function or predicate variable with same
525 * size.
526 *
527 * @param formula Formula we want the replacement take place.
528 * @param operatorVariable Predicate variable or function variable with only subject
529 * variables as arguments.
530 * @return Do we have any occurrence?
531 */
532 public static boolean containsOperatorVariable(final Element formula,
533 final Element operatorVariable) {
534 if (formula == null || formula.isAtom() || operatorVariable == null
535 || operatorVariable.isAtom()) {
536 return false;
537 }
538 final ElementList f = formula.getList();
539 final ElementList ov = operatorVariable.getList();
540 if (f.size() < 1 || ov.size() < 1) {
541 return f.equals(ov);
542 }
543 if (f.getOperator() == ov.getOperator() && f.size() == ov.size()
544 && f.getElement(0).equals(ov.getElement(0))) {
545 return true;
546 }
547 for (int i = 0; i < f.size(); i++) {
548 if (containsOperatorVariable(f.getElement(i), operatorVariable)) {
549 return true;
550 }
551 }
552 return false;
553 }
554
555 /**
556 * Test if operator occurrence in formula matches always to a formula that contains no subject
557 * variable that is in the given ElementSet of bound subject variables..
558 *
559 * @param formula Formula we want to test the condition.
560 * @param operatorVariable Predicate variable or function variable with only subject
561 * variables as arguments.
562 * @param bound Set of subject variables that are tabu.
563 * @return Formula test was successful.
564 */
565 public static boolean testOperatorVariable(final Element formula,
566 final Element operatorVariable, final ElementSet bound) {
567 if (formula.isAtom() || operatorVariable.isAtom()) {
568 return true;
569 }
570 final ElementList f = formula.getList();
571 final ElementList ov = operatorVariable.getList();
572 if (f.size() < 1 || ov.size() < 1) {
573 return true;
574 }
575 boolean ok = true;
576 if (f.getOperator() == ov.getOperator() && f.size() == ov.size()
577 && f.getElement(0).equals(ov.getElement(0))) {
578 if (!getSubjectVariables(f).intersection(bound).isEmpty()) {
579 return false;
580 }
581 } else {
582 for (int i = 0; ok && i < f.size(); i++) {
583 ok = testOperatorVariable(f.getElement(i), operatorVariable, bound);
584 }
585 }
586 return ok;
587 }
588
589 /**
590 * Is the given formula a simple implication like A => B.
591 *
592 * @param formula Check this formula.
593 * @return Is the formula a simple implication?
594 */
595 public static boolean isImplication(final Element formula) {
596 if (formula.isAtom()) {
597 return false;
598 }
599 final ElementList f = formula.getList();
600 return Operators.IMPLICATION_OPERATOR.equals(f.getList().getOperator())
601 && f.getList().size() == 2;
602 }
603
604 /**
605 * Create meta variable for subject variable.
606 *
607 * @param subjectVariable Subject variable, we want to have a meta variable for.
608 * @return Resulting meta variable. If we didn't got a subject variable we just
609 * return the original.
610 */
611 public static Element createMeta(final Element subjectVariable) {
612 if (!isSubjectVariable(subjectVariable)) {
613 return subjectVariable;
614 }
615 final DefaultElementList result = new DefaultElementList(META_VARIABLE);
616 result.add(subjectVariable.getList().getElement(0));
617 return result;
618 }
619
620 /**
621 * Create subject variable out of variable name.
622 *
623 * @param subjectVariableName Subject variable name.
624 * @return Resulting subject variable.
625 */
626 public static Element createSubjectVariable(final String subjectVariableName) {
627 final DefaultElementList result = new DefaultElementList(SUBJECT_VARIABLE);
628 result.add(new DefaultAtom(subjectVariableName));
629 return result;
630 }
631
632 /**
633 * Create predicate variable out of variable name with no further arguments.
634 *
635 * @param predicateVariableName Predicate variable name.
636 * @return Resulting predicate variable.
637 */
638 public static Element createPredicateVariable(final String predicateVariableName) {
639 final DefaultElementList result = new DefaultElementList(PREDICATE_VARIABLE);
640 result.add(new DefaultAtom(predicateVariableName));
641 return result;
642 }
643
644 }
|