1 /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">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.bo.logic.common;
17
18 import java.util.ArrayList;
19 import java.util.List;
20
21 import org.qedeq.base.utility.EqualsUtility;
22 import org.qedeq.kernel.se.base.list.ElementList;
23 import org.qedeq.kernel.se.common.ModuleContext;
24
25 /**
26 * Predicate constant.
27 *
28 * @author Michael Meyling
29 */
30 public final class PredicateConstant {
31
32 /** Predicate key. */
33 private final PredicateKey key;
34
35 /** Complete formula. */
36 private final ElementList completeFormula;
37
38 /** In this context the predicate was defined. */
39 private final ModuleContext context;
40
41 /** Predicate with subject variables. */
42 private final ElementList predicate;
43
44 /** Defining formula. */
45 private final ElementList definingFormula;
46
47 /** Subject variable strings. */
48 private final List subjectVariables;
49
50 /**
51 * Constructor.
52 *
53 * @param key Predicate name.
54 * @param completeFormula Complete formula defining predicate. Includes predicate.
55 * Must be like: A(x, y) <-> \forall z (z \in x <-> z \in y)
56 * @param context Module context we are in.
57 */
58 public PredicateConstant(final PredicateKey key, final ElementList completeFormula,
59 final ModuleContext context) {
60 this.key = key;
61 this.completeFormula = completeFormula;
62 this.context = new ModuleContext(context); // using copy constructor to fix context
63 final ElementList list = completeFormula.getList();
64 predicate = list.getElement(0).getList();
65 definingFormula = list.getElement(1).getList();
66 subjectVariables = new ArrayList(predicate.size() - 1);
67 for (int i = 0; i < predicate.size() - 1; i++) {
68 subjectVariables.add(new SubjectVariable(
69 predicate.getElement(i + 1).getList().getElement(0).getAtom().getString()));
70 }
71 }
72
73 /**
74 * Get predicate key.
75 *
76 * @return Predicate key.
77 */
78 public PredicateKey getKey() {
79 return key;
80 }
81
82 /**
83 * Get predicate name.
84 *
85 * @return Predicate name.
86 */
87 public String getName() {
88 return key.getName();
89 }
90
91 /**
92 * Get predicate argument number.
93 *
94 * @return Number of arguments.
95 */
96 public String getArguments() {
97 return key.getArguments();
98 }
99
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 }