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.se.dto.module;
017
018 import org.qedeq.base.utility.EqualsUtility;
019 import org.qedeq.kernel.se.base.list.Element;
020 import org.qedeq.kernel.se.base.module.Existential;
021
022
023 /**
024 * Usage of rule for existential generalization.
025 *
026 * @author Michael Meyling
027 */
028 public class ExistentialVo implements Existential {
029
030 /** Reference to previously proven formula. Usually like A -> B. */
031 private String reference;
032
033 /** Subject variable that we will quantify about. */
034 private Element subjectVariable;
035
036 /**
037 * Constructs an reason.
038 *
039 * @param reference Reference to a valid formula.
040 * @param subjectVariable Subject variable that we will quantify about.
041 */
042
043 public ExistentialVo(final String reference, final Element subjectVariable) {
044 this.reference = reference;
045 this.subjectVariable = subjectVariable;
046 }
047
048 /**
049 * Default constructor.
050 */
051 public ExistentialVo() {
052 // nothing to do
053 }
054
055 public String getReference() {
056 return reference;
057 }
058
059 /**
060 * Set formula reference.
061 *
062 * @param reference Reference to formula.
063 */
064 public void setReference(final String reference) {
065 this.reference = reference;
066 }
067
068 public String[] getReferences() {
069 if (reference == null || reference.length() == 0) {
070 return new String[] {};
071 } else {
072 return new String[] {reference };
073 }
074 }
075
076 public Element getSubjectVariable() {
077 return subjectVariable;
078 }
079
080 /**
081 * Set quantification subject variable.
082 *
083 * @param subjectVariable Set free subject variable.
084 */
085 public void setSubjectVariable(final Element subjectVariable) {
086 this.subjectVariable = subjectVariable;
087 }
088
089 public String getName() {
090 return "Existential";
091 }
092
093 public boolean equals(final Object obj) {
094 if (!(obj instanceof ExistentialVo)) {
095 return false;
096 }
097 final ExistentialVo other = (ExistentialVo) obj;
098 return EqualsUtility.equals(reference, other.reference)
099 && EqualsUtility.equals(subjectVariable, other.subjectVariable);
100 }
101
102 public int hashCode() {
103 return (reference != null ? reference.hashCode() : 0)
104 ^ (subjectVariable != null ? 2 ^ subjectVariable.hashCode() : 0);
105 }
106
107 public String toString() {
108 StringBuffer result = new StringBuffer();
109 result.append("SubstFree");
110 if (reference != null || subjectVariable != null) {
111 result.append(" (");
112 boolean w = false;
113 if (reference != null) {
114 result.append(reference);
115 w = true;
116 }
117 if (subjectVariable != null) {
118 if (w) {
119 result.append(", ");
120 }
121 result.append(subjectVariable);
122 w = true;
123 }
124 result.append(")");
125 }
126 return result.toString();
127 }
128
129 }
|