View Javadoc

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.Axiom;
20  import org.qedeq.kernel.se.base.module.Formula;
21  import org.qedeq.kernel.se.base.module.FunctionDefinition;
22  import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
23  import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
24  import org.qedeq.kernel.se.base.module.LatexList;
25  import org.qedeq.kernel.se.base.module.PredicateDefinition;
26  import org.qedeq.kernel.se.base.module.Proposition;
27  import org.qedeq.kernel.se.base.module.Rule;
28  
29  
30  /**
31   * Axiom.
32   *
33   * @author  Michael Meyling
34   */
35  public class AxiomVo implements Axiom {
36  
37      /** Axiom formula. */
38      private Formula formula;
39  
40      /** Further proposition description. Normally <code>null</code>. */
41      private LatexList description;
42  
43      /** Defined operator. The axiom defines this operator. Normally <code>null</code>.*/
44      private String definedOperator;
45  
46      /**
47       * Constructs a new axiom.
48       */
49      public AxiomVo() {
50          // nothing to do
51      }
52  
53      public Axiom getAxiom() {
54          return this;
55      }
56  
57      public InitialPredicateDefinition getInitialPredicateDefinition() {
58          return null;
59      }
60  
61      public PredicateDefinition getPredicateDefinition() {
62          return null;
63      }
64  
65      public InitialFunctionDefinition getInitialFunctionDefinition() {
66          return null;
67      }
68  
69      public FunctionDefinition getFunctionDefinition() {
70          return null;
71      }
72  
73      public Proposition getProposition() {
74          return null;
75      }
76  
77      public Rule getRule() {
78          return null;
79      }
80  
81      /**
82       * Set axiom formula.
83       *
84       * @param   formula Set axiom formula.
85       */
86      public final void setFormula(final FormulaVo formula) {
87          this.formula = formula;
88      }
89  
90      public final Formula getFormula() {
91          return formula;
92      }
93  
94      /**
95       * Set description. Only necessary if formula is not self-explanatory.
96       *
97       * @param   description Description.
98       */
99      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 }