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.module.ModusPonens;
020
021
022 /**
023 * Modes Ponens usage.
024 *
025 * @author Michael Meyling
026 */
027 public class ModusPonensBo implements ModusPonens {
028
029 /** Reference to a formula like A -> B. */
030 private int n1;
031
032 /** Usually reference to a formula like A. */
033 private int n2;
034
035 /**
036 * Constructs a Modus Ponens argument.
037 *
038 * @param n1 Usually reference to a formula like A -> B.
039 * @param n2 Usually reference to a formula like A.
040 */
041 public ModusPonensBo(final int n1, final int n2) {
042 this.n1 = n1;
043 this.n2 = n2;
044 }
045
046 public ModusPonens getModusPonens() {
047 return this;
048 }
049
050 public String getReference1() {
051 return "" + n1;
052 }
053
054 /**
055 * Set first formula reference.
056 *
057 * @param n1 Reference to formula.
058 */
059 public void setN1(final int n1) {
060 this.n1 = n1;
061 }
062
063 /**
064 * Get first formula reference.
065 *
066 * @return Reference to formula.
067 */
068 public int getN1() {
069 return n1;
070 }
071
072 public String getReference2() {
073 return "" + n2;
074 }
075
076 /**
077 * Set second formula reference.
078 *
079 * @param n2 Reference to formula.
080 */
081 public void setN2(final int n2) {
082 this.n2 = n2;
083 }
084
085 /**
086 * Get second formula reference.
087 *
088 * @return Reference to formula.
089 */
090 public int getN2() {
091 return n2;
092 }
093
094 public String[] getReferences() {
095 return new String[] {getReference1(), getReference2()};
096 }
097
098 /**
099 * Get references to previous lines.
100 *
101 * @return List of references.
102 */
103 public int[] getLines() {
104 return new int[] {getN1(), getN2()};
105 }
106
107 public boolean equals(final Object obj) {
108 if (!(obj instanceof ModusPonens)) {
109 return false;
110 }
111 final ModusPonens other = (ModusPonens) obj;
112 return EqualsUtility.equals(getReference1(), other.getReference1())
113 && EqualsUtility.equals(getReference2(), other.getReference2());
114 }
115
116 public int hashCode() {
117 return (getReference1() != null ? getReference1().hashCode() : 0)
118 + (getReference2() != null ? 1 ^ getReference2().hashCode() : 0);
119 }
120
121 public String toString() {
122 StringBuffer result = new StringBuffer();
123 result.append("MP");
124 if (getReference1() != null || getReference2() != null) {
125 result.append(" (");
126 if (getReference1() != null) {
127 result.append(getReference1());
128 }
129 if (getReference2() != null) {
130 if (getReference1() != null) {
131 result.append(", ");
132 }
133 result.append(getReference2());
134 }
135 result.append(")");
136 }
137 return result.toString();
138 }
139
140 public String getName() {
141 return "MP";
142 }
143
144 }
|