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.SubstPred;
22  
23  
24  /**
25   * Usage of rule for substitute predicate variable.
26   *
27   * @author  Michael Meyling
28   */
29  public class SubstPredVo implements SubstPred {
30  
31      /** Reference to previously proven formula. */
32      private String reference;
33  
34      /** Function variable that will be substituted. */
35      private Element predicateVariable;
36  
37      /** Replacement formula. */
38      private Element substituteFormula;
39  
40      /**
41       * Constructs an reason.
42       *
43       * @param   reference                   Reference to a valid formula.
44       * @param   predicateVariable           Predicate variable that will be substituted.
45       * @param   substituteFormula           Replacement formula.
46       */
47  
48      public SubstPredVo(final String reference, final Element predicateVariable,
49              final Element substituteFormula) {
50          this.reference = reference;
51          this.predicateVariable = predicateVariable;
52          this.substituteFormula = substituteFormula;
53      }
54  
55      /**
56       * Default constructor.
57       */
58      public SubstPredVo() {
59          // nothing to do
60      }
61  
62      public SubstPred getSubstPred() {
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 getPredicateVariable() {
87          return predicateVariable;
88      }
89  
90      /**
91       * Set predicate variable that will be substituted.
92       *
93       * @param   predicateVariable   Function variable that will be replaced.
94       */
95      public void setPredicateVariable(final Element predicateVariable) {
96          this.predicateVariable = predicateVariable;
97      }
98  
99      public Element getSubstituteFormula() {
100         return substituteFormula;
101     }
102 
103     /**
104      * Set substitution formula.
105      *
106      * @param   substituteFormula   New formula.
107      */
108     public void setSubstituteFormula(final Element substituteFormula) {
109         this.substituteFormula = substituteFormula;
110     }
111 
112     public String getName() {
113         return "SubstPred";
114     }
115 
116     public boolean equals(final Object obj) {
117         if (!(obj instanceof SubstPred)) {
118             return false;
119         }
120         final SubstPred other = (SubstPred) obj;
121         return EqualsUtility.equals(getReference(), other.getReference())
122             && EqualsUtility.equals(predicateVariable, other.getPredicateVariable())
123             && EqualsUtility.equals(substituteFormula, other.getSubstituteFormula());
124     }
125 
126     public int hashCode() {
127         return (getReference() != null ? getReference().hashCode() : 0)
128             ^ (getPredicateVariable() != null ? 2 ^ getPredicateVariable().hashCode() : 0)
129             ^ (getSubstituteFormula() != null ? 3 ^ getSubstituteFormula().hashCode() : 0);
130     }
131 
132     public String toString() {
133         StringBuffer result = new StringBuffer();
134         result.append(getName());
135         if (getReference() != null || getPredicateVariable() != null
136                 || getSubstituteFormula() != null) {
137             result.append(" (");
138             boolean w = false;
139             if (getReference() != null) {
140                 result.append(getReference());
141                 w = true;
142             }
143             if (getPredicateVariable() != null) {
144                 if (w) {
145                     result.append(", ");
146                 }
147                 result.append(getPredicateVariable());
148                 w = true;
149             }
150             if (getSubstituteFormula() != null) {
151                 if (w) {
152                     result.append(", ");
153                 }
154                 result.append("by ");
155                 result.append(getSubstituteFormula());
156                 w = true;
157             }
158             result.append(")");
159         }
160         return result.toString();
161     }
162 
163 }