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