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