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.apache.commons.lang.ArrayUtils;
19  import org.qedeq.base.utility.EqualsUtility;
20  import org.qedeq.kernel.se.base.list.Element;
21  import org.qedeq.kernel.se.base.module.SubstFree;
22  
23  
24  /**
25   * Usage of rule for substitute free subject variable.
26   *
27   * @author  Michael Meyling
28   */
29  public class SubstFreeVo implements SubstFree {
30  
31      /** Reference to previously proven formula. */
32      private String reference;
33  
34      /** Free subject variable that will be replaced. */
35      private Element subjectVariable;
36  
37      /** Replacement term. */
38      private Element substituteTerm;
39  
40      /**
41       * Constructs an reason.
42       *
43       * @param   reference                   Reference to a valid formula.
44       * @param   subjectVariable             Bound subject variable that will be substituted.
45       * @param   substituteTerm              Replacement term.
46       */
47  
48      public SubstFreeVo(final String reference, final Element subjectVariable,
49              final Element substituteTerm) {
50          this.reference = reference;
51          this.subjectVariable = subjectVariable;
52          this.substituteTerm = substituteTerm;
53      }
54  
55      /**
56       * Default constructor.
57       */
58      public SubstFreeVo() {
59          // nothing to do
60      }
61  
62      public SubstFree getSubstFree() {
63          return this;
64      }
65  
66      public String getReference() {
67          return reference;
68      }
69  
70      /**
71       * Set formula reference.
72       *
73       * @param   reference   Reference to formula.
74       */
75      public void setReference(final String reference) {
76          this.reference = reference;
77      }
78  
79      public String[] getReferences() {
80          if (reference == null) {
81              return ArrayUtils.EMPTY_STRING_ARRAY;
82          }
83          return new String[] {reference };
84      }
85  
86      public Element getSubjectVariable() {
87          return subjectVariable;
88      }
89  
90      /**
91       * Get subject variable that will be substituted.
92       *
93       * @param   subjectVariable Subject variable that will be replaced.
94       */
95      public void setSubjectVariable(final Element subjectVariable) {
96          this.subjectVariable = subjectVariable;
97      }
98  
99      public Element getSubstituteTerm() {
100         return substituteTerm;
101     }
102 
103     /**
104      * Set substitution term.
105      *
106      * @param   substituteTerm  New term.
107      */
108     public void setSubstituteTerm(final Element substituteTerm) {
109         this.substituteTerm = substituteTerm;
110     }
111 
112     public String getName() {
113         return "SubstFree";
114     }
115 
116     public boolean equals(final Object obj) {
117         if (!(obj instanceof SubstFreeVo)) {
118             return false;
119         }
120         final SubstFreeVo other = (SubstFreeVo) obj;
121         return EqualsUtility.equals(reference, other.reference)
122             && EqualsUtility.equals(subjectVariable, other.subjectVariable)
123             && EqualsUtility.equals(substituteTerm, other.substituteTerm);
124     }
125 
126     public int hashCode() {
127         return (reference != null ? reference.hashCode() : 0)
128             ^ (subjectVariable != null ? 2 ^ subjectVariable.hashCode() : 0)
129             ^ (substituteTerm != null ? 3 ^ substituteTerm.hashCode() : 0);
130     }
131 
132     public String toString() {
133         StringBuffer result = new StringBuffer();
134         result.append(getName());
135         if (reference != null || subjectVariable != null
136                 || substituteTerm != null) {
137             result.append(" (");
138             boolean w = false;
139             if (reference != null) {
140                 result.append(reference);
141                 w = true;
142             }
143             if (subjectVariable != null) {
144                 if (w) {
145                     result.append(", ");
146                 }
147                 result.append(subjectVariable);
148                 w = true;
149             }
150             if (substituteTerm != null) {
151                 if (w) {
152                     result.append(", ");
153                 }
154                 result.append("by ");
155                 result.append(substituteTerm);
156                 w = true;
157             }
158             result.append(")");
159         }
160         return result.toString();
161     }
162 
163 }