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.bo.service.logic;
017
018 import java.util.HashMap;
019 import java.util.Map;
020
021 import org.qedeq.base.trace.Trace;
022 import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
023 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
024 import org.qedeq.kernel.bo.logic.common.FunctionKey;
025 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
026 import org.qedeq.kernel.bo.logic.common.PredicateKey;
027 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
028 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
029 import org.qedeq.kernel.se.base.module.Rule;
030 import org.qedeq.kernel.se.common.RuleKey;
031
032
033 /**
034 * Checks if all predicate and function constants exist already.
035 *
036 * @author Michael Meyling
037 */
038 public class DefaultExistenceChecker implements ExistenceChecker {
039
040 /** This class. */
041 private static final Class CLASS = DefaultExistenceChecker.class;
042
043 /** Maps {@link PredicateKey} identifiers to {@link InitialPredicateDefinitions}s. */
044 private final Map initialPredicateDefinitions = new HashMap();
045
046 /** Maps {@link PredicateKey} identifiers to {@link PredicateConstant}s. */
047 private final Map predicateDefinitions = new HashMap();
048
049 /** Maps {@link FunctionKey} identifiers to {@link InitialFunctionDefinition}s. */
050 private final Map initialFunctionDefinitions = new HashMap();
051
052 /** Maps {@link FunctionKey} identifiers to {@link FunctionConstant}s. */
053 private final Map functionDefinitions = new HashMap();
054
055 /** Maps {@link RuleKey}s to {@link Rules}s. */
056 private final Map ruleDefinitions = new HashMap();
057
058 /** Is the class operator already defined? */
059 private boolean setDefinitionByFormula;
060
061 /** Identity operator. */
062 private String identityOperator;
063
064
065 /**
066 * Constructor.
067 */
068 public DefaultExistenceChecker() {
069 clear();
070 }
071
072 /**
073 * Empty all definitions.
074 */
075 public void clear() {
076 Trace.trace(CLASS, this, "setClassOperatorExists", "clear");
077 initialPredicateDefinitions.clear();
078 predicateDefinitions.clear();
079 initialFunctionDefinitions.clear();
080 ruleDefinitions.clear();
081 functionDefinitions.clear();
082 identityOperator = null;
083 setDefinitionByFormula = false;
084 }
085
086 public boolean predicateExists(final PredicateKey predicate) {
087 final InitialPredicateDefinition initialDefinition
088 = (InitialPredicateDefinition) initialPredicateDefinitions.get(predicate);
089 if (initialDefinition != null) {
090 return true;
091 }
092 return null != predicateDefinitions.get(predicate);
093 }
094
095 public boolean predicateExists(final String name, final int arguments) {
096 final PredicateKey predicate = new PredicateKey(name, "" + arguments);
097 return predicateExists(predicate);
098 }
099
100 public boolean isInitialPredicate(final PredicateKey predicate) {
101 final InitialPredicateDefinition initialDefinition
102 = (InitialPredicateDefinition) initialPredicateDefinitions.get(predicate);
103 return initialDefinition != null;
104 }
105
106 /**
107 * Add unknown predicate constant definition. If the predicate constant is already known a
108 * runtime exception is thrown.
109 *
110 * @param initialDefinition Predicate constant definition that is not already known. Must not be
111 * <code>null</code>.
112 * @throws IllegalArgumentException Predicate constant is already defined.
113 */
114 public void add(final InitialPredicateDefinition initialDefinition) {
115 final PredicateKey predicate = new PredicateKey(initialDefinition.getName(),
116 initialDefinition.getArgumentNumber());
117 if (predicateExists(predicate)) {
118 throw new IllegalArgumentException(LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
119 + predicate);
120 }
121 initialPredicateDefinitions.put(predicate, initialDefinition);
122 }
123
124 /**
125 * Add unknown predicate constant definition. If the predicate constant is already known a
126 * runtime exception is thrown.
127 *
128 * @param constant Predicate constant definition that is not already known. Must not be
129 * <code>null</code>.
130 * @throws IllegalArgumentException Predicate constant is already defined.
131 */
132 public void add(final PredicateConstant constant) {
133 final PredicateKey predicate = constant.getKey();
134 if (predicateExists(predicate)) {
135 throw new IllegalArgumentException(LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
136 + predicate);
137 }
138 predicateDefinitions.put(predicate, constant);
139 }
140
141 /**
142 * Get predicate constant definition.
143 *
144 * @param predicate Get definition of this predicate.
145 * @return Definition.
146 */
147 public PredicateConstant get(final PredicateKey predicate) {
148 return (PredicateConstant) predicateDefinitions.get(predicate);
149 }
150
151 /**
152 * Get predicate constant definition.
153 *
154 * @param name Name of predicate.
155 * @param arguments Arguments of predicate.
156 * @return Definition. Might be <code>null</code>.
157 */
158 public PredicateConstant getPredicate(final String name, final int arguments) {
159 final PredicateKey predicate = new PredicateKey(name, "" + arguments);
160 return get(predicate);
161 }
162
163 public boolean functionExists(final FunctionKey function) {
164 final InitialFunctionDefinition initialDefinition
165 = (InitialFunctionDefinition) initialFunctionDefinitions.get(function);
166 if (initialDefinition != null) {
167 return true;
168 }
169 return null != functionDefinitions.get(function);
170 }
171
172 public boolean functionExists(final String name, final int arguments) {
173 final FunctionKey function = new FunctionKey(name, "" + arguments);
174 return functionExists(function);
175 }
176
177 /**
178 * Add unknown function constant definition. If the function constant is already known a
179 * runtime exception is thrown.
180 *
181 * @param definition Function constant definition that is not already known. Must not be
182 * <code>null</code>.
183 * @throws IllegalArgumentException Function constant is already defined.
184 */
185 public void add(final FunctionConstant definition) {
186 final FunctionKey function = definition.getKey();
187 if (functionDefinitions.get(function) != null) {
188 throw new IllegalArgumentException(LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT
189 + function);
190 }
191 functionDefinitions.put(function, definition);
192 }
193
194 /**
195 * Add unknown function constant definition. If the function constant is already known a
196 * runtime exception is thrown.
197 *
198 * @param initialDefinition Function constant definition that is not already known. Must not be
199 * <code>null</code>.
200 * @throws IllegalArgumentException Function constant is already defined.
201 */
202 public void add(final InitialFunctionDefinition initialDefinition) {
203 final FunctionKey predicate = new FunctionKey(initialDefinition.getName(),
204 initialDefinition.getArgumentNumber());
205 if (functionExists(predicate)) {
206 throw new IllegalArgumentException(LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT
207 + predicate);
208 }
209 initialFunctionDefinitions.put(predicate, initialDefinition);
210 }
211
212 /**
213 * Get function constant definition.
214 *
215 * @param function Get definition of this predicate.
216 * @return Definition. Might be <code>null</code>.
217 */
218 public FunctionConstant get(final FunctionKey function) {
219 return (FunctionConstant) functionDefinitions.get(function);
220 }
221
222 /**
223 * Get function constant definition.
224 *
225 * @param name Name of function.
226 * @param arguments Arguments of function.
227 * @return Definition. Might be <code>null</code>.
228 */
229 public FunctionConstant getFunction(final String name, final int arguments) {
230 final FunctionKey function = new FunctionKey(name, "" + arguments);
231 return get(function);
232 }
233
234 public boolean isInitialFunction(final FunctionKey function) {
235 final InitialFunctionDefinition initialDefinition
236 = (InitialFunctionDefinition) initialFunctionDefinitions.get(function);
237 return initialDefinition != null;
238 }
239
240
241 public boolean ruleExists(final RuleKey ruleKey) {
242 return null != get(ruleKey);
243 }
244
245 /**
246 * Add unknown rule definition. If the rule is already known a runtime exception is thrown.
247 *
248 * @param ruleKey Key for rule.
249 * @param definition Rule definition that is not already known. Must not be
250 * <code>null</code>. Rule key might be different!
251 * @throws IllegalArgumentException Rule is already defined (for given version).
252 */
253 public void add(final RuleKey ruleKey, final Rule definition) {
254 if (ruleDefinitions.get(ruleKey) != null) {
255 throw new IllegalArgumentException(LogicErrors.RULE_ALREADY_DEFINED_TEXT
256 + ruleKey);
257 }
258 ruleDefinitions.put(ruleKey, definition);
259 }
260
261 /**
262 * Get rule definition.
263 *
264 * @param ruleKey Get definition of this key.
265 * @return Definition. Might be <code>null</code>.
266 */
267 public Rule get(final RuleKey ruleKey) {
268 return (Rule) ruleDefinitions.get(ruleKey);
269 }
270
271 public boolean classOperatorExists() {
272 return setDefinitionByFormula;
273 }
274
275 // /**
276 // * Set if the class operator is already defined.
277 // *
278 // * @param existence Class operator is defined.
279 // */
280 // TODO m31 20100820: write some tests that use this feature
281 // public void setClassOperatorExists(final boolean existence) {
282 // Trace.param(CLASS, this, "setClassOperatorExists", "existence", existence);
283 // setDefinitionByFormula = existence;
284 // }
285
286 public boolean identityOperatorExists() {
287 return this.identityOperator != null;
288 }
289
290 public String getIdentityOperator() {
291 return this.identityOperator;
292 }
293
294 /**
295 * Set the identity operator.
296 *
297 * @param identityOperator Operator name. Might be <code>null</code>.
298 */
299 public void setIdentityOperatorDefined(final String identityOperator) {
300 Trace.param(CLASS, this, "setIdentityOperatorDefined", "identityOperator", identityOperator);
301 this.identityOperator = identityOperator;
302 }
303
304 }
|