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