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.Existential;
22  
23  
24  /**
25   * Usage of rule for existential generalization.
26   *
27   * @author  Michael Meyling
28   */
29  public class ExistentialVo implements Existential {
30  
31      /** Reference to previously proven formula. Usually like A -&gt; B. */
32      private String reference;
33  
34      /** Subject variable that we will quantify about. */
35      private Element subjectVariable;
36  
37      /**
38       * Constructs an reason.
39       *
40       * @param   reference                   Reference to a valid formula.
41       * @param   subjectVariable             Subject variable that we will quantify about.
42       */
43  
44      public ExistentialVo(final String reference, final Element subjectVariable) {
45          this.reference = reference;
46          this.subjectVariable = subjectVariable;
47      }
48  
49      /**
50       * Default constructor.
51       */
52      public ExistentialVo() {
53          // nothing to do
54      }
55  
56      public Existential getExistential() {
57          return this;
58      }
59  
60      public String getReference() {
61          return reference;
62      }
63  
64      /**
65       * Set formula reference.
66       *
67       * @param   reference   Reference to formula.
68       */
69      public void setReference(final String reference) {
70          this.reference = reference;
71      }
72  
73      public String[] getReferences() {
74          if (reference == null) {
75              return ArrayUtils.EMPTY_STRING_ARRAY;
76          }
77          return new String[] {reference };
78      }
79  
80      public Element getSubjectVariable() {
81          return subjectVariable;
82      }
83  
84      /**
85       * Set quantification subject variable.
86       *
87       * @param   subjectVariable Set free subject variable.
88       */
89      public void setSubjectVariable(final Element subjectVariable) {
90          this.subjectVariable = subjectVariable;
91      }
92  
93      public String getName() {
94          return "Existential";
95      }
96  
97      public boolean equals(final Object obj) {
98          if (!(obj instanceof ExistentialVo)) {
99              return false;
100         }
101         final ExistentialVo other = (ExistentialVo) obj;
102         return EqualsUtility.equals(reference, other.reference)
103             && EqualsUtility.equals(subjectVariable, other.subjectVariable);
104     }
105 
106     public int hashCode() {
107         return (reference != null ? reference.hashCode() : 0)
108             ^ (subjectVariable != null ? 2 ^ subjectVariable.hashCode() : 0);
109     }
110 
111     public String toString() {
112         StringBuffer result = new StringBuffer();
113         result.append(getName());
114         if (reference != null || subjectVariable != null) {
115             result.append(" (");
116             boolean w = false;
117             if (reference != null) {
118                 result.append(reference);
119                 w = true;
120             }
121             if (subjectVariable != null) {
122                 if (w) {
123                     result.append(", ");
124                 }
125                 result.append(subjectVariable);
126                 w = true;
127             }
128             result.append(")");
129         }
130         return result.toString();
131     }
132 
133 }