001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, 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 private 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 normalized 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 normalized predicate 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 * Has the given list an operator that binds a subject variable?
291 *
292 * @param list Check for this operator.
293 * @return Has it an binding operator with subject variable?
294 */
295 public static boolean isBindingOperator(final ElementList list) {
296 final String operator = list.getOperator();
297 if (operator == null || list.size() <= 0 || !isSubjectVariable(list.getElement(0))) {
298 return false;
299 }
300 return operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
301 || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
302 || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
303 || operator.equals(CLASS_OP);
304 }
305
306 /**
307 * Get relative context of the first difference between the given elements.
308 *
309 * @param first First element.
310 * @param second Second element.
311 * @return Relative path (beginning with ".") of first difference.
312 */
313 public static String getDifferenceLocation(final Element first, final Element second) {
314 final StringBuffer diff = new StringBuffer();
315 equal(diff, first, second);
316 return diff.toString();
317 }
318
319 /**
320 * Is there any difference between the two elements? If so, the context has the difference
321 * position.
322 *
323 * @param firstContext Context (might be relative) for first element.
324 * @param first First element.
325 * @param second Second element.
326 * @return Are both elements equal?
327 */
328 private static boolean equal(final StringBuffer firstContext,
329 final Element first, final Element second) {
330 if (first == null) {
331 return second == null;
332 }
333 if (first.isAtom()) {
334 if (!second.isAtom()) {
335 return false;
336 }
337 return EqualsUtility.equals(first.getAtom().getString(), second.getAtom().getString());
338 }
339 if (second.isAtom()) {
340 return false;
341 }
342 if (!EqualsUtility.equals(first.getList().getOperator(), second.getList().getOperator())) {
343 return false;
344 }
345 if (first.getList().size() != second.getList().size()) {
346 return false;
347 }
348 for (int i = 0; i < first.getList().size(); i++) {
349 final int length = firstContext.length();
350 firstContext.append(".getList().getElement(" + i + ")");
351 if (!equal(firstContext, first.getList().getElement(i),
352 second.getList().getElement(i))) {
353 return false;
354 }
355 firstContext.setLength(length);
356 }
357 return true;
358 }
359
360 /**
361 * Replace bound subject variables at given occurrence by another one.
362 * If goal occurrence number is below number of occurrences within the formula nothing is
363 * changed. Original parts are used, so don't modify the formulas directly.
364 *
365 * @param originalSubjectVariable Replace this subject variable.
366 * @param replacementSubjectVariable By this subject variable.
367 * @param formulaElement This is the formula we work on.
368 * @param occurrenceGoal This is the binding occurrence number.
369 * @param occurreneCurrent Counter how much occurrences we already had.
370 * @return Formula with replaced subject variables.
371 */
372 public static Element replaceSubjectVariableQuantifier(final Element originalSubjectVariable,
373 final Element replacementSubjectVariable, final Element formulaElement,
374 final int occurrenceGoal, final Enumerator occurreneCurrent) {
375 if (formulaElement.isAtom()) {
376 return formulaElement;
377 }
378 final ElementList formula = formulaElement.getList();
379 if (occurreneCurrent.getNumber() > occurrenceGoal) {
380 return formula.copy();
381 }
382 final ElementList result = new DefaultElementList(formula.getOperator());
383 if (isBindingOperator(formula)
384 && formula.getElement(0).equals(originalSubjectVariable)) {
385 occurreneCurrent.increaseNumber();
386 // System.out.println("found: " + occurreneCurrent);
387 if (occurrenceGoal == occurreneCurrent.getNumber()) {
388 // System.out.println("match: " + occurrenceGoal);
389 return formula.replace(originalSubjectVariable,
390 replacementSubjectVariable);
391 }
392 }
393 for (int i = 0; i < formula.size(); i++) {
394 result.add(replaceSubjectVariableQuantifier(originalSubjectVariable,
395 replacementSubjectVariable, formula.getElement(i), occurrenceGoal,
396 occurreneCurrent));
397 }
398 return result;
399 }
400
401 /**
402 * Replace function or predicate variable by given term or formula. Old parts are not copied
403 * but taken directly - so don't modify the formulas!
404 *
405 * @param formula Formula we want the replacement take place.
406 * @param operatorVariable Predicate variable or function variable with only subject
407 * variables as arguments.
408 * @param replacement Replacement formula or term with matching subject variables.
409 * <code>operatorVariable</code> might have some subject variables
410 * that are not in <code>replacement</code> and vice versa.
411 * @return Formula where operatorVariable was replaced.
412 */
413 public static Element replaceOperatorVariable(final Element formula,
414 final Element operatorVariable, final Element replacement) {
415 if (formula == null || operatorVariable == null || replacement == null
416 || formula.isAtom() || operatorVariable.isAtom() || replacement.isAtom()) {
417 return formula;
418 }
419 final ElementList f = formula.getList();
420 final ElementList ov = operatorVariable.getList();
421 final ElementList r = replacement.getList();
422 // check elementary preconditions
423 // System.out.println("ov.size=" + ov.size());
424 if (f.size() < 1 || ov.size() < 1) {
425 // System.out.println("failed elementary conditions");
426 return formula;
427 }
428 // construct replacement formula with meta variables
429 Element rn = r;
430 for (int i = 1; i < ov.size(); i++) {
431 rn = rn.replace(ov.getElement(i), createMeta(ov.getElement(i)));
432 }
433 return replaceOperatorVariableMeta(formula, operatorVariable, rn);
434 }
435
436 /**
437 * Replace function or predicate variable by given term or formula. Original parts are used -
438 * so don't modify them!
439 *
440 * @param formula Formula we want the replacement take place.
441 * @param operatorVariable Predicate variable or function variable with only subject
442 * variables as arguments.
443 * @param replacement Replacement formula or term with meta variables instead of
444 * subject variables to replace (matching
445 * <code>operatorVariable</code>).
446 * @return Formula where operatorVariable was replaced.
447 */
448 private static Element replaceOperatorVariableMeta(final Element formula,
449 final Element operatorVariable, final Element replacement) {
450 if (formula.isAtom() || operatorVariable.isAtom() || replacement.isAtom()) {
451 return formula;
452 }
453 final ElementList f = formula.getList();
454 final ElementList ov = operatorVariable.getList();
455 final ElementList r = replacement.getList();
456 if (f.size() < 1 || ov.size() < 1) {
457 return formula.copy();
458 }
459 ElementList result;
460 if (f.getOperator() == ov.getOperator() && f.size() == ov.size()
461 && f.getElement(0).equals(ov.getElement(0))) {
462 // replace meta variables by matching entries
463 result = r;
464 for (int i = 1; i < ov.size(); i++) {
465 result = (ElementList) result.replace(createMeta(ov.getElement(i)),
466 replaceOperatorVariableMeta(f.getElement(i), operatorVariable, replacement));
467 }
468 } else {
469 result = new DefaultElementList(f.getOperator());
470 for (int i = 0; i < f.size(); i++) {
471 result.add(replaceOperatorVariableMeta(f.getElement(i), operatorVariable,
472 replacement));
473 }
474 }
475 return result;
476 }
477
478 /**
479 * Test if operator occurrence in formula matches always to a formula that contains no subject
480 * variable that is in the given ElementSet of bound subject variables..
481 *
482 * @param formula Formula we want to test the condition.
483 * @param operatorVariable Predicate variable or function variable with only subject
484 * variables as arguments.
485 * @param bound Set of subject variables that are tabu.
486 * @return Formula test was successful.
487 */
488 public static boolean testOperatorVariable(final Element formula,
489 final Element operatorVariable, final ElementSet bound) {
490 if (formula.isAtom() || operatorVariable.isAtom()) {
491 return true;
492 }
493 final ElementList f = formula.getList();
494 final ElementList ov = operatorVariable.getList();
495 if (f.size() < 1 || ov.size() < 1) {
496 return true;
497 }
498 boolean ok = true;
499 if (f.getOperator() == ov.getOperator() && f.size() == ov.size()
500 && f.getElement(0).equals(ov.getElement(0))) {
501 if (!getSubjectVariables(f).intersection(bound).isEmpty()) {
502 return false;
503 }
504 } else {
505 for (int i = 0; ok && i < f.size(); i++) {
506 ok = testOperatorVariable(f.getElement(i), operatorVariable, bound);
507 }
508 }
509 return ok;
510 }
511
512 /**
513 * Is the given formula a simple implication like A => B.
514 *
515 * @param formula Check this formula.
516 * @return Is the formula a simple implication?
517 */
518 public static boolean isImplication(final Element formula) {
519 if (formula.isAtom()) {
520 return false;
521 }
522 final ElementList f = formula.getList();
523 return Operators.IMPLICATION_OPERATOR.equals(f.getList().getOperator())
524 && f.getList().size() == 2;
525 }
526
527 /**
528 * Create meta variable for subject variable.
529 *
530 * @param subjectVariable Subject variable, we want to have a meta variable for.
531 * @return Resulting meta variable. If we didn't got a subject variable we just
532 * return the original.
533 */
534 public static Element createMeta(final Element subjectVariable) {
535 if (!isSubjectVariable(subjectVariable)) {
536 return subjectVariable;
537 }
538 final DefaultElementList result = new DefaultElementList(META_VARIABLE);
539 result.add(subjectVariable.getList().getElement(0));
540 return result;
541 }
542
543 /**
544 * Create subject variable out of variable name.
545 *
546 * @param subjectVariableName Subject variable name.
547 * @return Resulting subject variable.
548 */
549 public static Element createSubjectVariable(final String subjectVariableName) {
550 final DefaultElementList result = new DefaultElementList(SUBJECT_VARIABLE);
551 result.add(new DefaultAtom(subjectVariableName));
552 return result;
553 }
554
555 /**
556 * Create predicate variable out of variable name with no further arguments.
557 *
558 * @param predicateVariableName Predicate variable name.
559 * @return Resulting predicate variable.
560 */
561 public static Element createPredicateVariable(final String predicateVariableName) {
562 final DefaultElementList result = new DefaultElementList(PREDICATE_VARIABLE);
563 result.add(new DefaultAtom(predicateVariableName));
564 return result;
565 }
566
567 }
|