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.se.dto.module;
17
18 import org.qedeq.base.utility.EqualsUtility;
19 import org.qedeq.kernel.se.base.module.FormalProofLine;
20 import org.qedeq.kernel.se.base.module.Formula;
21 import org.qedeq.kernel.se.base.module.Reason;
22
23
24 /**
25 * Contains a formal proof for a proposition.
26 *
27 * @author Michael Meyling
28 */
29 public class FormalProofLineVo implements FormalProofLine {
30
31 /** Label for back references. Might be <code>null</code>. */
32 private String label;
33
34 /** Rule that is used for deriving. */
35 private Reason reason;
36
37 /** Derived formula. */
38 private Formula formula;
39
40 /**
41 * Constructs an proof line.
42 *
43 * @param formula New derived formula.
44 * @param reason Rule that was used to derive the formula.
45 */
46 public FormalProofLineVo(final Formula formula, final Reason reason) {
47 this.label = null;
48 this.reason = reason;
49 this.formula = formula;
50 }
51
52 /**
53 * Constructs an proof line.
54 *
55 * @param label Label for back references. Might be <code>null</code>.
56 * @param formula New derived formula.
57 * @param reason Rule that was used to derive the formula.
58 */
59 public FormalProofLineVo(final String label, final Formula formula, final Reason reason) {
60 this.label = label;
61 this.reason = reason;
62 this.formula = formula;
63 }
64
65 /**
66 * Default constructor.
67 */
68 public FormalProofLineVo() {
69 // nothing to do
70 }
71
72 public Formula getFormula() {
73 return formula;
74 }
75
76 /**
77 * Set proof line formula.
78 *
79 * @param formula Set formula.
80 */
81 public void setFormula(final Formula formula) {
82 this.formula = formula;
83 }
84
85 public String getLabel() {
86 return label;
87 }
88
89 /**
90 * Set label for proof line.
91 *
92 * @param label Set this label.
93 */
94 public void setLabel(final String label) {
95 this.label = label;
96 }
97
98 public Reason getReason() {
99 return reason;
100 }
101
102 /**
103 * Set reason type for proof line.
104 *
105 * @param reason Set this reason type.
106 */
107 public void setReason(final Reason reason) {
108 this.reason = reason;
109 }
110
111 public boolean equals(final Object obj) {
112 if (!(obj instanceof FormalProofLineVo)) {
113 return false;
114 }
115 final FormalProofLineVo other = (FormalProofLineVo) obj;
116 return EqualsUtility.equals(label, other.label)
117 && EqualsUtility.equals(formula, other.formula)
118 && EqualsUtility.equals(reason, other.reason);
119 }
120
121 public int hashCode() {
122 return (label != null ? label.hashCode() : 0)
123 ^ (formula != null ? 1 ^ formula.hashCode() : 0)
124 ^ (reason != null ? 2 ^ reason.hashCode() : 0);
125 }
126
127 public String toString() {
128 return (label != null ? "[" + label + "] " : " ") + getFormula() + " "
129 + getReason();
130 }
131
132 }