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.bo.logic.proof.finder;
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 SubstPredBo implements SubstPred {
029
030 /** Reference to previously proven formula. */
031 private int n;
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 n Reference to a valid formula.
043 * @param predicateVariable Predicate variable that will be substituted.
044 * @param substituteFormula Replacement formula.
045 */
046
047 public SubstPredBo(final int n, final Element predicateVariable,
048 final Element substituteFormula) {
049 this.n = n;
050 this.predicateVariable = predicateVariable;
051 this.substituteFormula = substituteFormula;
052 }
053
054 public SubstPred getSubstPred() {
055 return this;
056 }
057
058 public String getReference() {
059 return "" + n;
060 }
061
062 /**
063 * Set formula reference.
064 *
065 * @param n Reference to formula.
066 */
067 public void setN(final int n) {
068 this.n = n;
069 }
070
071 /**
072 * Get formula reference.
073 *
074 * @return Reference to formula.
075 */
076 public int getN() {
077 return n;
078 }
079
080 public String[] getReferences() {
081 return new String[] {getReference()};
082 }
083
084 public Element getPredicateVariable() {
085 return predicateVariable;
086 }
087
088 public Element getSubstituteFormula() {
089 return substituteFormula;
090 }
091
092 public String getName() {
093 return "SubstPred";
094 }
095
096 public boolean equals(final Object obj) {
097 if (!(obj instanceof SubstPred)) {
098 return false;
099 }
100 final SubstPred other = (SubstPred) obj;
101 return EqualsUtility.equals(getReference(), other.getReference())
102 && EqualsUtility.equals(predicateVariable, other.getPredicateVariable())
103 && EqualsUtility.equals(substituteFormula, other.getSubstituteFormula());
104 }
105
106 public int hashCode() {
107 return (getReference() != null ? getReference().hashCode() : 0)
108 ^ (getPredicateVariable() != null ? 2 ^ getPredicateVariable().hashCode() : 0)
109 ^ (getSubstituteFormula() != null ? 3 ^ getSubstituteFormula().hashCode() : 0);
110 }
111
112 public String toString() {
113 StringBuffer result = new StringBuffer();
114 result.append("SubstPred");
115 if (getReference() != null || getPredicateVariable() != null
116 || getSubstituteFormula() != null) {
117 result.append(" (");
118 boolean w = false;
119 if (getReference() != null) {
120 result.append(getReference());
121 w = true;
122 }
123 if (getPredicateVariable() != null) {
124 if (w) {
125 result.append(", ");
126 }
127 result.append(getPredicateVariable());
128 w = true;
129 }
130 if (getSubstituteFormula() != null) {
131 if (w) {
132 result.append(", ");
133 }
134 result.append("by ");
135 result.append(getSubstituteFormula());
136 w = true;
137 }
138 result.append(")");
139 }
140 return result.toString();
141 }
142
143 }
|