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.apache.commons.lang.ArrayUtils;
019 import org.qedeq.base.utility.EqualsUtility;
020 import org.qedeq.kernel.se.base.list.Element;
021 import org.qedeq.kernel.se.base.module.Existential;
022
023
024 /**
025 * Usage of rule for existential generalization.
026 *
027 * @author Michael Meyling
028 */
029 public class ExistentialVo implements Existential {
030
031 /** Reference to previously proven formula. Usually like A -> B. */
032 private String reference;
033
034 /** Subject variable that we will quantify about. */
035 private Element subjectVariable;
036
037 /**
038 * Constructs an reason.
039 *
040 * @param reference Reference to a valid formula.
041 * @param subjectVariable Subject variable that we will quantify about.
042 */
043
044 public ExistentialVo(final String reference, final Element subjectVariable) {
045 this.reference = reference;
046 this.subjectVariable = subjectVariable;
047 }
048
049 /**
050 * Default constructor.
051 */
052 public ExistentialVo() {
053 // nothing to do
054 }
055
056 public Existential getExistential() {
057 return this;
058 }
059
060 public String getReference() {
061 return reference;
062 }
063
064 /**
065 * Set formula reference.
066 *
067 * @param reference Reference to formula.
068 */
069 public void setReference(final String reference) {
070 this.reference = reference;
071 }
072
073 public String[] getReferences() {
074 if (reference == null) {
075 return ArrayUtils.EMPTY_STRING_ARRAY;
076 } else {
077 return new String[] {reference };
078 }
079 }
080
081 public Element getSubjectVariable() {
082 return subjectVariable;
083 }
084
085 /**
086 * Set quantification subject variable.
087 *
088 * @param subjectVariable Set free subject variable.
089 */
090 public void setSubjectVariable(final Element subjectVariable) {
091 this.subjectVariable = subjectVariable;
092 }
093
094 public String getName() {
095 return "Existential";
096 }
097
098 public boolean equals(final Object obj) {
099 if (!(obj instanceof ExistentialVo)) {
100 return false;
101 }
102 final ExistentialVo other = (ExistentialVo) obj;
103 return EqualsUtility.equals(reference, other.reference)
104 && EqualsUtility.equals(subjectVariable, other.subjectVariable);
105 }
106
107 public int hashCode() {
108 return (reference != null ? reference.hashCode() : 0)
109 ^ (subjectVariable != null ? 2 ^ subjectVariable.hashCode() : 0);
110 }
111
112 public String toString() {
113 StringBuffer result = new StringBuffer();
114 result.append(getName());
115 if (reference != null || subjectVariable != null) {
116 result.append(" (");
117 boolean w = false;
118 if (reference != null) {
119 result.append(reference);
120 w = true;
121 }
122 if (subjectVariable != null) {
123 if (w) {
124 result.append(", ");
125 }
126 result.append(subjectVariable);
127 w = true;
128 }
129 result.append(")");
130 }
131 return result.toString();
132 }
133
134 }
|