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.Axiom;
020 import org.qedeq.kernel.se.base.module.Formula;
021 import org.qedeq.kernel.se.base.module.FunctionDefinition;
022 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
023 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
024 import org.qedeq.kernel.se.base.module.LatexList;
025 import org.qedeq.kernel.se.base.module.PredicateDefinition;
026 import org.qedeq.kernel.se.base.module.Proposition;
027 import org.qedeq.kernel.se.base.module.Rule;
028
029
030 /**
031 * Axiom.
032 *
033 * @author Michael Meyling
034 */
035 public class AxiomVo implements Axiom {
036
037 /** Axiom formula. */
038 private Formula formula;
039
040 /** Further proposition description. Normally <code>null</code>. */
041 private LatexList description;
042
043 /** Defined operator. The axiom defines this operator. Normally <code>null</code>.*/
044 private String definedOperator;
045
046 /**
047 * Constructs a new axiom.
048 */
049 public AxiomVo() {
050 // nothing to do
051 }
052
053 public Axiom getAxiom() {
054 return this;
055 }
056
057 public InitialPredicateDefinition getInitialPredicateDefinition() {
058 return null;
059 }
060
061 public PredicateDefinition getPredicateDefinition() {
062 return null;
063 }
064
065 public InitialFunctionDefinition getInitialFunctionDefinition() {
066 return null;
067 }
068
069 public FunctionDefinition getFunctionDefinition() {
070 return null;
071 }
072
073 public Proposition getProposition() {
074 return null;
075 }
076
077 public Rule getRule() {
078 return null;
079 }
080
081 /**
082 * Set axiom formula.
083 *
084 * @param formula Set axiom formula.
085 */
086 public final void setFormula(final FormulaVo formula) {
087 this.formula = formula;
088 }
089
090 public final Formula getFormula() {
091 return formula;
092 }
093
094 /**
095 * Set description. Only necessary if formula is not self-explanatory.
096 *
097 * @param description Description.
098 */
099 public final void setDescription(final LatexListVo description) {
100 this.description = description;
101 }
102
103 public LatexList getDescription() {
104 return description;
105 }
106
107 public String getDefinedOperator() {
108 return definedOperator;
109 }
110
111 /**
112 * Set operator which is defined by this axiom. So the axiom can be eliminated by eliminating
113 * this operator.
114 *
115 * @param definedOperator This operator is defined by this axiom.
116 */
117 public void setDefinedOperator(final String definedOperator) {
118 this.definedOperator = definedOperator;
119 }
120
121 public boolean equals(final Object obj) {
122 if (!(obj instanceof AxiomVo)) {
123 return false;
124 }
125 final AxiomVo other = (AxiomVo) obj;
126 return EqualsUtility.equals(getFormula(), other.getFormula())
127 && EqualsUtility.equals(getDescription(), other.getDescription())
128 && EqualsUtility.equals(getDefinedOperator(), other.getDefinedOperator());
129 }
130
131 public int hashCode() {
132 return (getFormula() != null ? getFormula().hashCode() : 0)
133 ^ (getDefinedOperator() != null ? 1 ^ getDefinedOperator().hashCode() : 0)
134 ^ (getDescription() != null ? 1 ^ getDescription().hashCode() : 0);
135 }
136
137 public String toString() {
138 final StringBuffer buffer = new StringBuffer();
139 buffer.append("Axiom");
140 if (definedOperator != null) {
141 buffer.append(" (defines: " + definedOperator);
142 }
143 buffer.append(":\n");
144 buffer.append(getFormula());
145 buffer.append("\nDescription:\n");
146 buffer.append(getDescription());
147 return buffer.toString();
148 }
149 }
|