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.se.dto.module;
017
018 import org.qedeq.base.utility.EqualsUtility;
019 import org.qedeq.kernel.se.base.module.Formula;
020 import org.qedeq.kernel.se.base.module.Hypothesis;
021
022
023 /**
024 * Hypothesis that can be used as an assumption within a proof.
025 *
026 * @author Michael Meyling
027 */
028 public class HypothesisVo implements Hypothesis {
029
030 /** Label for back references. Might be <code>null</code>. */
031 private String label;
032
033 /** Derived formula. */
034 private Formula formula;
035
036 /**
037 * Constructs an proof line.
038 *
039 * @param formula New derived formula.
040 */
041 public HypothesisVo(final Formula formula) {
042 this.label = null;
043 this.formula = formula;
044 }
045
046 /**
047 * Constructs an proof line.
048 *
049 * @param label Label for back references. Might be <code>null</code>.
050 * @param formula New derived formula.
051 */
052 public HypothesisVo(final String label, final Formula formula) {
053 this.label = label;
054 this.formula = formula;
055 }
056
057 /**
058 * Default constructor.
059 */
060 public HypothesisVo() {
061 // nothing to do
062 }
063
064 public Formula getFormula() {
065 return formula;
066 }
067
068 /**
069 * Set proof line formula.
070 *
071 * @param formula Set formula.
072 */
073 public void setFormula(final Formula formula) {
074 this.formula = formula;
075 }
076
077 public String getLabel() {
078 return label;
079 }
080
081 /**
082 * Set label for proof line.
083 *
084 * @param label Set this label.
085 */
086 public void setLabel(final String label) {
087 this.label = label;
088 }
089
090 public boolean equals(final Object obj) {
091 if (!(obj instanceof HypothesisVo)) {
092 return false;
093 }
094 final HypothesisVo other = (HypothesisVo) obj;
095 return EqualsUtility.equals(label, other.label)
096 && EqualsUtility.equals(formula, other.formula);
097 }
098
099 public int hashCode() {
100 return (label != null ? label.hashCode() : 0)
101 ^ (formula != null ? 1 ^ formula.hashCode() : 0);
102 }
103
104 public String toString() {
105 return (label != null ? "[" + label + "] " : " ") + getFormula() + " "
106 + "Hypothesis";
107 }
108
109 }
|