1 /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org
2 *
3 * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>.
4 *
5 * "Hilbert II" is free software; you can redistribute
6 * it and/or modify it under the terms of the GNU General Public
7 * License as published by the Free Software Foundation; either
8 * version 2 of the License, or (at your option) any later version.
9 *
10 * This program is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 */
15
16 package org.qedeq.kernel.bo.logic.proof.finder;
17
18 import org.qedeq.base.utility.EqualsUtility;
19 import org.qedeq.kernel.se.base.module.ModusPonens;
20
21
22 /**
23 * Modes Ponens usage.
24 *
25 * @author Michael Meyling
26 */
27 public class ModusPonensBo implements ModusPonens {
28
29 /** Reference to a formula like A -> B. */
30 private int n1;
31
32 /** Usually reference to a formula like A. */
33 private int n2;
34
35 /**
36 * Constructs a Modus Ponens argument.
37 *
38 * @param n1 Usually reference to a formula like A -> B.
39 * @param n2 Usually reference to a formula like A.
40 */
41 public ModusPonensBo(final int n1, final int n2) {
42 this.n1 = n1;
43 this.n2 = n2;
44 }
45
46 public ModusPonens getModusPonens() {
47 return this;
48 }
49
50 public String getReference1() {
51 return "" + n1;
52 }
53
54 /**
55 * Set first formula reference.
56 *
57 * @param n1 Reference to formula.
58 */
59 public void setN1(final int n1) {
60 this.n1 = n1;
61 }
62
63 /**
64 * Get first formula reference.
65 *
66 * @return Reference to formula.
67 */
68 public int getN1() {
69 return n1;
70 }
71
72 public String getReference2() {
73 return "" + n2;
74 }
75
76 /**
77 * Set second formula reference.
78 *
79 * @param n2 Reference to formula.
80 */
81 public void setN2(final int n2) {
82 this.n2 = n2;
83 }
84
85 /**
86 * Get second formula reference.
87 *
88 * @return Reference to formula.
89 */
90 public int getN2() {
91 return n2;
92 }
93
94 public String[] getReferences() {
95 return new String[] {getReference1(), getReference2()};
96 }
97
98 /**
99 * 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().hashCode() ^ getReference2().hashCode();
118 }
119
120 public String toString() {
121 StringBuffer result = new StringBuffer();
122 result.append("MP");
123 result.append(" (");
124 if (getReference1() != null) {
125 result.append(getReference1());
126 }
127 if (getReference2() != null) {
128 if (getReference1() != null) {
129 result.append(", ");
130 }
131 result.append(getReference2());
132 }
133 result.append(")");
134 return result.toString();
135 }
136
137 public String getName() {
138 return "MP";
139 }
140
141 }