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.logic.common;
017
018 import java.util.ArrayList;
019 import java.util.List;
020
021 import org.qedeq.base.utility.EqualsUtility;
022 import org.qedeq.kernel.se.base.list.ElementList;
023 import org.qedeq.kernel.se.common.ModuleContext;
024
025 /**
026 * Predicate constant.
027 *
028 * @author Michael Meyling
029 */
030 public final class PredicateConstant {
031
032 /** Predicate key. */
033 private final PredicateKey key;
034
035 /** Complete formula. */
036 private final ElementList completeFormula;
037
038 /** In this context the predicate was defined. */
039 private final ModuleContext context;
040
041 /** Predicate with subject variables. */
042 private final ElementList predicate;
043
044 /** Defining formula. */
045 private final ElementList definingFormula;
046
047 /** Subject variable strings. */
048 private final List subjectVariables;
049
050 /**
051 * Constructor.
052 *
053 * @param key Predicate name.
054 * @param completeFormula Complete formula defining predicate. Includes predicate.
055 * Must be like: A(x, y) <-> \forall z (z \in x <-> z \in y)
056 * @param context Module context we are in.
057 */
058 public PredicateConstant(final PredicateKey key, final ElementList completeFormula,
059 final ModuleContext context) {
060 this.key = key;
061 this.completeFormula = completeFormula;
062 this.context = new ModuleContext(context); // using copy constructor to fix context
063 final ElementList list = completeFormula.getList();
064 predicate = list.getElement(0).getList();
065 definingFormula = list.getElement(1).getList();
066 subjectVariables = new ArrayList(predicate.size() - 1);
067 for (int i = 0; i < predicate.size() - 1; i++) {
068 subjectVariables.add(new SubjectVariable(
069 predicate.getElement(i + 1).getList().getElement(0).getAtom().getString()));
070 }
071 }
072
073 /**
074 * Get predicate key.
075 *
076 * @return Predicate key.
077 */
078 public PredicateKey getKey() {
079 return key;
080 }
081
082 /**
083 * Get predicate name.
084 *
085 * @return Predicate name.
086 */
087 public String getName() {
088 return key.getName();
089 }
090
091 /**
092 * Get predicate argument number.
093 *
094 * @return Number of arguments.
095 */
096 public String getArguments() {
097 return key.getArguments();
098 }
099
100 /**
101 * Get complete defining formula. Includes predicate itself.
102 *
103 * @return Complete defining formula.
104 */
105 public ElementList getCompleteFormula() {
106 return completeFormula;
107 }
108
109 /**
110 * Get context where the complete formula is.
111 *
112 * @return Module context for complete formula.
113 */
114 public ModuleContext getContext() {
115 return context;
116 }
117
118 /**
119 * Get predicate with parameters.
120 *
121 * @return Predicate part of definition formula.
122 */
123 public ElementList getPredicate() {
124 return predicate;
125 }
126
127 /**
128 * Get parameter subject variables.
129 *
130 * @return Parameter subject variables as within a list.
131 */
132 public List getSubjectVariables() {
133 return subjectVariables;
134 }
135
136 /**
137 * Get defining formula. Predicate itself is not included.
138 *
139 * @return Defining formula only.
140 */
141 public ElementList getDefiningFormula() {
142 return definingFormula;
143 }
144
145 public int hashCode() {
146 return (getKey() != null ? getKey().hashCode() : 0)
147 ^ (getCompleteFormula() != null ? getCompleteFormula().hashCode() : 0);
148 }
149
150 public boolean equals(final Object obj) {
151 if (!(obj instanceof PredicateConstant)) {
152 return false;
153 }
154 final PredicateConstant other = (PredicateConstant) obj;
155 return EqualsUtility.equals(getKey(), other.getKey())
156 && EqualsUtility.equals(getCompleteFormula(), other.getCompleteFormula());
157 }
158
159 public String toString() {
160 return getName() + "[" + getArguments() + "]";
161 }
162
163
164 }
|