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.se.dto.module;
017
018 import org.apache.commons.lang.ArrayUtils;
019 import org.qedeq.base.utility.EqualsUtility;
020 import org.qedeq.kernel.se.base.list.Element;
021 import org.qedeq.kernel.se.base.module.SubstFree;
022
023
024 /**
025 * Usage of rule for substitute free subject variable.
026 *
027 * @author Michael Meyling
028 */
029 public class SubstFreeVo implements SubstFree {
030
031 /** Reference to previously proven formula. */
032 private String reference;
033
034 /** Free subject variable that will be replaced. */
035 private Element subjectVariable;
036
037 /** Replacement term. */
038 private Element substituteTerm;
039
040 /**
041 * Constructs an reason.
042 *
043 * @param reference Reference to a valid formula.
044 * @param subjectVariable Bound subject variable that will be substituted.
045 * @param substituteTerm Replacement term.
046 */
047
048 public SubstFreeVo(final String reference, final Element subjectVariable,
049 final Element substituteTerm) {
050 this.reference = reference;
051 this.subjectVariable = subjectVariable;
052 this.substituteTerm = substituteTerm;
053 }
054
055 /**
056 * Default constructor.
057 */
058 public SubstFreeVo() {
059 // nothing to do
060 }
061
062 public SubstFree getSubstFree() {
063 return this;
064 }
065
066 public String getReference() {
067 return reference;
068 }
069
070 /**
071 * Set formula reference.
072 *
073 * @param reference Reference to formula.
074 */
075 public void setReference(final String reference) {
076 this.reference = reference;
077 }
078
079 public String[] getReferences() {
080 if (reference == null) {
081 return ArrayUtils.EMPTY_STRING_ARRAY;
082 }
083 return new String[] {reference };
084 }
085
086 public Element getSubjectVariable() {
087 return subjectVariable;
088 }
089
090 /**
091 * Get subject variable that will be substituted.
092 *
093 * @param subjectVariable Subject variable that will be replaced.
094 */
095 public void setSubjectVariable(final Element subjectVariable) {
096 this.subjectVariable = subjectVariable;
097 }
098
099 public Element getSubstituteTerm() {
100 return substituteTerm;
101 }
102
103 /**
104 * Set substitution term.
105 *
106 * @param substituteTerm New term.
107 */
108 public void setSubstituteTerm(final Element substituteTerm) {
109 this.substituteTerm = substituteTerm;
110 }
111
112 public String getName() {
113 return "SubstFree";
114 }
115
116 public boolean equals(final Object obj) {
117 if (!(obj instanceof SubstFreeVo)) {
118 return false;
119 }
120 final SubstFreeVo other = (SubstFreeVo) obj;
121 return EqualsUtility.equals(reference, other.reference)
122 && EqualsUtility.equals(subjectVariable, other.subjectVariable)
123 && EqualsUtility.equals(substituteTerm, other.substituteTerm);
124 }
125
126 public int hashCode() {
127 return (reference != null ? reference.hashCode() : 0)
128 ^ (subjectVariable != null ? 2 ^ subjectVariable.hashCode() : 0)
129 ^ (substituteTerm != null ? 3 ^ substituteTerm.hashCode() : 0);
130 }
131
132 public String toString() {
133 StringBuffer result = new StringBuffer();
134 result.append(getName());
135 if (reference != null || subjectVariable != null
136 || substituteTerm != null) {
137 result.append(" (");
138 boolean w = false;
139 if (reference != null) {
140 result.append(reference);
141 w = true;
142 }
143 if (subjectVariable != null) {
144 if (w) {
145 result.append(", ");
146 }
147 result.append(subjectVariable);
148 w = true;
149 }
150 if (substituteTerm != null) {
151 if (w) {
152 result.append(", ");
153 }
154 result.append("by ");
155 result.append(substituteTerm);
156 w = true;
157 }
158 result.append(")");
159 }
160 return result.toString();
161 }
162
163 }
|