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 // nothing to do here
041 }
042
043 /**
044 * Is {@link Element} a subject variable?
045 *
046 * @param element Element to look onto.
047 * @return Is it a subject variable?
048 */
049 public static final boolean isSubjectVariable(final Element element) {
050 if (element == null || !element.isList() || element.getList() == null) {
051 return false;
052 }
053 final ElementList list = element.getList();
054 if (list.getOperator().equals(SUBJECT_VARIABLE)) {
055 if (list.size() != 1) {
056 return false;
057 }
058 final Element first = element.getList().getElement(0);
059 if (first == null || !first.isAtom() || first.getAtom() == null) {
060 return false;
061 }
062 final Atom atom = first.getAtom();
063 if (atom.getString() == null || atom.getAtom().getString() == null
064 || atom.getString().length() == 0) {
065 return false;
066 }
067 } else {
068 return false;
069 }
070 return true;
071 }
072
073 /**
074 * Is {@link Element} a predicate variable?
075 *
076 * @param element Element to look onto.
077 * @return Is it a predicate variable?
078 */
079 public static final boolean isPredicateVariable(final Element element) {
080 return isOperator(PREDICATE_VARIABLE, element);
081 }
082
083 /**
084 * Is {@link Element} a proposition variable?
085 *
086 * @param element Element to look onto.
087 * @return Is it a proposition variable?
088 */
089 public static final boolean isPropositionVariable(final Element element) {
090 return isOperator(PREDICATE_VARIABLE, element) && element.getList().size() <= 1;
091 }
092
093 /**
094 * Is {@link Element} a function variable?
095 *
096 * @param element Element to look onto.
097 * @return Is it a function variable?
098 */
099 public static final boolean isFunctionVariable(final Element element) {
100 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 public static final boolean isPredicateConstant(final Element element) {
110 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 public static final boolean isFunctionConstant(final Element element) {
120 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 public static boolean isOperator(final String operator,
132 final Element element) {
133 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 private static boolean isOperator(final String operator,
146 final Element element, final int minArguments) {
147 if (element == null || !element.isList() || element.getList() == null) {
148 return false;
149 }
150 final ElementList list = element.getList();
151 if (list.getOperator().equals(operator)) {
152 if (list.size() < 1 + minArguments) {
153 return false;
154 }
155 final Element first = element.getList().getElement(0);
156 if (first == null || !first.isAtom() || first.getAtom() == null) {
157 return false;
158 }
159 final Atom atom = first.getAtom();
160 if (atom.getString() == null || atom.getAtom().getString() == null
161 || atom.getString().length() == 0) {
162 return false;
163 }
164 } else {
165 return false;
166 }
167 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 public static final ElementSet getFreeSubjectVariables(final Element element) {
177 final ElementSet free = new ElementSet();
178 if (isSubjectVariable(element)) {
179 free.add(element);
180 } else if (element.isList()) {
181 final ElementList list = element.getList();
182 if (isBindingOperator(list)) {
183 for (int i = 1; i < list.size(); i++) {
184 free.union(getFreeSubjectVariables(list.getElement(i)));
185 }
186 free.remove(list.getElement(0));
187 } else {
188 for (int i = 0; i < list.size(); i++) {
189 free.union(getFreeSubjectVariables(list.getElement(i)));
190 }
191 }
192 }
193 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 public static final ElementSet getBoundSubjectVariables(final Element element) {
203 final ElementSet bound = new ElementSet();
204 if (element.isList()) {
205 ElementList list = element.getList();
206 // if operator is quantifier or class term
207 if (isBindingOperator(list)) {
208 // add subject variable to bound list
209 bound.add(list.getElement(0));
210 // add all bound variables of sub-elements
211 for (int i = 1; i < list.size(); i++) {
212 bound.union(getBoundSubjectVariables(
213 list.getElement(i)));
214 }
215 } else {
216 // add all bound variables of sub-elements
217 for (int i = 0; i < list.size(); i++) {
218 bound.union(getBoundSubjectVariables(list.getElement(i)));
219 }
220 }
221 }
222 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 public static final ElementSet getSubjectVariables(final Element element) {
232 final ElementSet all = new ElementSet();
233 if (isSubjectVariable(element)) {
234 all.add(element);
235 } else if (element.isList()) {
236 final ElementList list = element.getList();
237 for (int i = 1; i < list.size(); i++) {
238 all.union(getSubjectVariables(list.getElement(i)));
239 }
240 }
241 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 public static final ElementSet getPredicateVariables(final Element element) {
252 final ElementSet all = new ElementSet();
253 if (isPredicateVariable(element)) {
254 final ElementList pred = element.getList();
255 final DefaultElementList normalized = new DefaultElementList(pred.getOperator());
256 normalized.add(pred.getElement(0));
257 for (int i = 1; i < pred.size(); i++) {
258 normalized.add(createSubjectVariable("x_" + i));
259 }
260 all.add(normalized);
261 } else if (element.isList()) {
262 final ElementList list = element.getList();
263 for (int i = 0; i < list.size(); i++) {
264 all.union(getPredicateVariables(list.getElement(i)));
265 }
266 }
267 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 public static final ElementSet getPropositionVariables(final Element element) {
278 final ElementSet all = new ElementSet();
279 if (isPropositionVariable(element)) {
280 all.add(element);
281 } else if (element.isList()) {
282 final ElementList list = element.getList();
283 for (int i = 0; i < list.size(); i++) {
284 all.union(getPropositionVariables(list.getElement(i)));
285 }
286 }
287 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 public static final ElementSet getPartFormulas(final Element element) {
297 final ElementSet all = new ElementSet();
298 if (element == null || element.isAtom()) {
299 return all;
300 }
301 final ElementList list = element.getList();
302 if (isPredicateVariable(list)) {
303 all.add(element);
304 } else if (isPredicateConstant(list)) {
305 all.add(list);
306 } 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 all.add(list);
313 for (int i = 0; i < list.size(); i++) {
314 all.union(getPartFormulas(list.getElement(i)));
315 }
316 } else if (isBindingOperator(list)) {
317 all.add(list);
318 for (int i = 0; i < list.size(); i++) {
319 all.union(getPartFormulas(list.getElement(i)));
320 }
321 } else if (isSubjectVariable(list)) {
322 // this is no formula
323 } else if (isFunctionVariable(list)) {
324 // this is no formula
325 } else if (isFunctionConstant(list)) {
326 // this is no formula
327 } else {
328 for (int i = 0; i < list.size(); i++) {
329 all.union(getPartFormulas(list.getElement(i)));
330 }
331 }
332 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 public static boolean isBindingOperator(final ElementList list) {
342 final String operator = list.getOperator();
343 if (operator == null || list.size() <= 0 || !isSubjectVariable(list.getElement(0))) {
344 return false;
345 }
346 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 public static String getDifferenceLocation(final Element first, final Element second) {
360 final StringBuffer diff = new StringBuffer();
361 equal(diff, first, second);
362 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 private static boolean equal(final StringBuffer firstContext,
375 final Element first, final Element second) {
376 if (first == null) {
377 return second == null;
378 }
379 if (second == null) {
380 return false;
381 }
382 if (first.isAtom()) {
383 if (!second.isAtom()) {
384 return false;
385 }
386 return EqualsUtility.equals(first.getAtom().getString(), second.getAtom().getString());
387 }
388 if (second.isAtom()) {
389 return false;
390 }
391 if (!EqualsUtility.equals(first.getList().getOperator(), second.getList().getOperator())) {
392 return false;
393 }
394 if (first.getList().size() != second.getList().size()) {
395 return false;
396 }
397 for (int i = 0; i < first.getList().size(); i++) {
398 final int length = firstContext.length();
399 firstContext.append(".getList().getElement(" + i + ")");
400 if (!equal(firstContext, first.getList().getElement(i),
401 second.getList().getElement(i))) {
402 return false;
403 }
404 firstContext.setLength(length);
405 }
406 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 public static Element replaceSubjectVariableQuantifier(final Element originalSubjectVariable,
422 final Element replacementSubjectVariable, final Element formulaElement,
423 final int occurrenceGoal, final Enumerator occurreneCurrent) {
424 if (formulaElement.isAtom()) {
425 return formulaElement;
426 }
427 final ElementList formula = formulaElement.getList();
428 if (occurreneCurrent.getNumber() > occurrenceGoal) {
429 return formula.copy();
430 }
431 final ElementList result = new DefaultElementList(formula.getOperator());
432 if (isBindingOperator(formula)
433 && formula.getElement(0).equals(originalSubjectVariable)) {
434 occurreneCurrent.increaseNumber();
435 // System.out.println("found: " + occurreneCurrent);
436 if (occurrenceGoal == occurreneCurrent.getNumber()) {
437 // System.out.println("match: " + occurrenceGoal);
438 return formula.replace(originalSubjectVariable,
439 replacementSubjectVariable);
440 }
441 }
442 for (int i = 0; i < formula.size(); i++) {
443 result.add(replaceSubjectVariableQuantifier(originalSubjectVariable,
444 replacementSubjectVariable, formula.getElement(i), occurrenceGoal,
445 occurreneCurrent));
446 }
447 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 public static Element replaceOperatorVariable(final Element formula,
463 final Element operatorVariable, final Element replacement) {
464 if (formula == null || operatorVariable == null || replacement == null
465 || formula.isAtom() || operatorVariable.isAtom() || replacement.isAtom()) {
466 return formula;
467 }
468 final ElementList f = formula.getList();
469 final ElementList ov = operatorVariable.getList();
470 final ElementList r = replacement.getList();
471 // check elementary preconditions
472 // System.out.println("ov.size=" + ov.size());
473 if (f.size() < 1 || ov.size() < 1) {
474 // System.out.println("failed elementary conditions");
475 return formula;
476 }
477 // construct replacement formula with meta variables
478 Element rn = r;
479 for (int i = 1; i < ov.size(); i++) {
480 rn = rn.replace(ov.getElement(i), createMeta(ov.getElement(i)));
481 }
482 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 private static Element replaceOperatorVariableMeta(final Element formula,
498 final Element operatorVariable, final Element replacement) {
499 if (formula.isAtom() || operatorVariable.isAtom() || replacement.isAtom()) {
500 return formula;
501 }
502 final ElementList f = formula.getList();
503 final ElementList ov = operatorVariable.getList();
504 final ElementList r = replacement.getList();
505 if (f.size() < 1 || ov.size() < 1) {
506 return formula.copy();
507 }
508 ElementList result;
509 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 result = r;
513 for (int i = 1; i < ov.size(); i++) {
514 result = (ElementList) result.replace(createMeta(ov.getElement(i)),
515 replaceOperatorVariableMeta(f.getElement(i), operatorVariable, replacement));
516 }
517 } else {
518 result = new DefaultElementList(f.getOperator());
519 for (int i = 0; i < f.size(); i++) {
520 result.add(replaceOperatorVariableMeta(f.getElement(i), operatorVariable,
521 replacement));
522 }
523 }
524 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 public static boolean containsOperatorVariable(final Element formula,
537 final Element operatorVariable) {
538 if (formula == null || formula.isAtom() || operatorVariable == null
539 || operatorVariable.isAtom()) {
540 return false;
541 }
542 final ElementList f = formula.getList();
543 final ElementList ov = operatorVariable.getList();
544 if (f.size() < 1 || ov.size() < 1) {
545 return f.equals(ov);
546 }
547 if (EqualsUtility.equals(f.getOperator(), ov.getOperator()) && f.size() == ov.size()
548 && f.getElement(0).equals(ov.getElement(0))) {
549 return true;
550 }
551 for (int i = 0; i < f.size(); i++) {
552 if (containsOperatorVariable(f.getElement(i), operatorVariable)) {
553 return true;
554 }
555 }
556 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 public static boolean testOperatorVariable(final Element formula,
570 final Element operatorVariable, final ElementSet bound) {
571 if (formula.isAtom() || operatorVariable.isAtom()) {
572 return true;
573 }
574 final ElementList f = formula.getList();
575 final ElementList ov = operatorVariable.getList();
576 if (f.size() < 1 || ov.size() < 1) {
577 return true;
578 }
579 boolean ok = true;
580 if (EqualsUtility.equals(f.getOperator(), ov.getOperator()) && f.size() == ov.size()
581 && f.getElement(0).equals(ov.getElement(0))) {
582 if (!getSubjectVariables(f).intersection(bound).isEmpty()) {
583 return false;
584 }
585 } else {
586 for (int i = 0; ok && i < f.size(); i++) {
587 ok = testOperatorVariable(f.getElement(i), operatorVariable, bound);
588 }
589 }
590 return ok;
591 }
592
593 /**
594 * Is the given formula a simple implication like A => B.
595 *
596 * @param formula Check this formula.
597 * @return Is the formula a simple implication?
598 */
599 public static boolean isImplication(final Element formula) {
600 if (formula.isAtom()) {
601 return false;
602 }
603 final ElementList f = formula.getList();
604 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 public static Element createMeta(final Element subjectVariable) {
616 if (!isSubjectVariable(subjectVariable)) {
617 return subjectVariable;
618 }
619 final DefaultElementList result = new DefaultElementList(META_VARIABLE);
620 result.add(subjectVariable.getList().getElement(0));
621 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 public static Element createSubjectVariable(final String subjectVariableName) {
631 final DefaultElementList result = new DefaultElementList(SUBJECT_VARIABLE);
632 result.add(new DefaultAtom(subjectVariableName));
633 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 public static Element createPredicateVariable(final String predicateVariableName) {
643 final DefaultElementList result = new DefaultElementList(PREDICATE_VARIABLE);
644 result.add(new DefaultAtom(predicateVariableName));
645 return result;
646 }
647
648 }
|