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.SubstPred;
022
023
024 /**
025 * Usage of rule for substitute predicate variable.
026 *
027 * @author Michael Meyling
028 */
029 public class SubstPredVo implements SubstPred {
030
031 /** Reference to previously proven formula. */
032 private String reference;
033
034 /** Function variable that will be substituted. */
035 private Element predicateVariable;
036
037 /** Replacement formula. */
038 private Element substituteFormula;
039
040 /**
041 * Constructs an reason.
042 *
043 * @param reference Reference to a valid formula.
044 * @param predicateVariable Predicate variable that will be substituted.
045 * @param substituteFormula Replacement formula.
046 */
047
048 public SubstPredVo(final String reference, final Element predicateVariable,
049 final Element substituteFormula) {
050 this.reference = reference;
051 this.predicateVariable = predicateVariable;
052 this.substituteFormula = substituteFormula;
053 }
054
055 /**
056 * Default constructor.
057 */
058 public SubstPredVo() {
059 // nothing to do
060 }
061
062 public SubstPred getSubstPred() {
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 } else {
083 return new String[] {reference };
084 }
085 }
086
087 public Element getPredicateVariable() {
088 return predicateVariable;
089 }
090
091 /**
092 * Set predicate variable that will be substituted.
093 *
094 * @param predicateVariable Function variable that will be replaced.
095 */
096 public void setPredicateVariable(final Element predicateVariable) {
097 this.predicateVariable = predicateVariable;
098 }
099
100 public Element getSubstituteFormula() {
101 return substituteFormula;
102 }
103
104 /**
105 * Set substitution formula.
106 *
107 * @param substituteFormula New formula.
108 */
109 public void setSubstituteFormula(final Element substituteFormula) {
110 this.substituteFormula = substituteFormula;
111 }
112
113 public String getName() {
114 return "SubstPred";
115 }
116
117 public boolean equals(final Object obj) {
118 if (!(obj instanceof SubstPred)) {
119 return false;
120 }
121 final SubstPred other = (SubstPred) obj;
122 return EqualsUtility.equals(getReference(), other.getReference())
123 && EqualsUtility.equals(predicateVariable, other.getPredicateVariable())
124 && EqualsUtility.equals(substituteFormula, other.getSubstituteFormula());
125 }
126
127 public int hashCode() {
128 return (getReference() != null ? getReference().hashCode() : 0)
129 ^ (getPredicateVariable() != null ? 2 ^ getPredicateVariable().hashCode() : 0)
130 ^ (getSubstituteFormula() != null ? 3 ^ getSubstituteFormula().hashCode() : 0);
131 }
132
133 public String toString() {
134 StringBuffer result = new StringBuffer();
135 result.append(getName());
136 if (getReference() != null || getPredicateVariable() != null
137 || getSubstituteFormula() != null) {
138 result.append(" (");
139 boolean w = false;
140 if (getReference() != null) {
141 result.append(getReference());
142 w = true;
143 }
144 if (getPredicateVariable() != null) {
145 if (w) {
146 result.append(", ");
147 }
148 result.append(getPredicateVariable());
149 w = true;
150 }
151 if (getSubstituteFormula() != null) {
152 if (w) {
153 result.append(", ");
154 }
155 result.append("by ");
156 result.append(getSubstituteFormula());
157 w = true;
158 }
159 result.append(")");
160 }
161 return result.toString();
162 }
163
164 }
|