diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2023-09-14 19:29:36 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2023-09-14 19:29:36 +0200 |
commit | 98ed3b6db5f4e51961a161050cc31c66015116e8 (patch) | |
tree | 8bfd6d9bc8d6ed23b9eb0f889dd40b6c24fe8f92 /subprojects/viatra-runtime/src/main/java/tools/refinery/viatra/runtime/matchers/psystem/PVariable.java | |
parent | Merge pull request #38 from nagilooh/design-space-exploration (diff) | |
parent | Merge remote-tracking branch 'upstream/main' into partial-interpretation (diff) | |
download | refinery-98ed3b6db5f4e51961a161050cc31c66015116e8.tar.gz refinery-98ed3b6db5f4e51961a161050cc31c66015116e8.tar.zst refinery-98ed3b6db5f4e51961a161050cc31c66015116e8.zip |
Merge pull request #39 from kris7t/partial-interpretation
Implement partial interpretation based model generation
Diffstat (limited to 'subprojects/viatra-runtime/src/main/java/tools/refinery/viatra/runtime/matchers/psystem/PVariable.java')
-rw-r--r-- | subprojects/viatra-runtime/src/main/java/tools/refinery/viatra/runtime/matchers/psystem/PVariable.java | 203 |
1 files changed, 203 insertions, 0 deletions
diff --git a/subprojects/viatra-runtime/src/main/java/tools/refinery/viatra/runtime/matchers/psystem/PVariable.java b/subprojects/viatra-runtime/src/main/java/tools/refinery/viatra/runtime/matchers/psystem/PVariable.java new file mode 100644 index 00000000..b6ea4861 --- /dev/null +++ b/subprojects/viatra-runtime/src/main/java/tools/refinery/viatra/runtime/matchers/psystem/PVariable.java | |||
@@ -0,0 +1,203 @@ | |||
1 | /******************************************************************************* | ||
2 | * Copyright (c) 2004-2010 Gabor Bergmann and Daniel Varro | ||
3 | * This program and the accompanying materials are made available under the | ||
4 | * terms of the Eclipse Public License v. 2.0 which is available at | ||
5 | * http://www.eclipse.org/legal/epl-v20.html. | ||
6 | * | ||
7 | * SPDX-License-Identifier: EPL-2.0 | ||
8 | *******************************************************************************/ | ||
9 | |||
10 | package tools.refinery.viatra.runtime.matchers.psystem; | ||
11 | |||
12 | import java.util.HashSet; | ||
13 | import java.util.Set; | ||
14 | |||
15 | /** | ||
16 | * @author Gabor Bergmann | ||
17 | * | ||
18 | */ | ||
19 | public class PVariable { | ||
20 | private PBody pBody; | ||
21 | /** | ||
22 | * The name of the pattern variable. This is the unique key of the pattern node. | ||
23 | */ | ||
24 | private String name; | ||
25 | /** | ||
26 | * virtual pVariables are nodes that do not correspond to actual pattern variables; they represent constants or Term | ||
27 | * substitutes | ||
28 | */ | ||
29 | private boolean virtual; | ||
30 | |||
31 | /** | ||
32 | * Set of constraints that mention this variable | ||
33 | */ | ||
34 | private Set<PConstraint> referringConstraints; | ||
35 | |||
36 | /** | ||
37 | * Determines whether there are any constraints that can deduce this variable | ||
38 | */ | ||
39 | private Boolean deducable; | ||
40 | |||
41 | /** | ||
42 | * Another PVariable this variable has been unified into. Please use the other variable instead of this. Null iff | ||
43 | * this is still a first-class variable. | ||
44 | */ | ||
45 | private PVariable unifiedInto; | ||
46 | |||
47 | PVariable(PBody pBody, String name) { | ||
48 | this(pBody, name, false); | ||
49 | } | ||
50 | |||
51 | PVariable(PBody pBody, String name, boolean virtual) { | ||
52 | super(); | ||
53 | this.pBody = pBody; | ||
54 | this.name = name; | ||
55 | this.virtual = virtual; | ||
56 | // this.exportedParameter = false; | ||
57 | this.referringConstraints = new HashSet<PConstraint>(); | ||
58 | this.unifiedInto = null; | ||
59 | this.deducable = false; | ||
60 | } | ||
61 | |||
62 | /** | ||
63 | * Replaces this variable with a given other, resulting in their unification. This variable will no longer be | ||
64 | * unique. | ||
65 | * | ||
66 | * @param replacement | ||
67 | */ | ||
68 | public void unifyInto(PVariable replacement) { | ||
69 | pBody.checkMutability(); | ||
70 | replacementCheck(); | ||
71 | replacement = replacement.getUnifiedIntoRoot(); | ||
72 | |||
73 | if (this.equals(replacement)) | ||
74 | return; | ||
75 | |||
76 | if (!this.isVirtual() && replacement.isVirtual()) { | ||
77 | replacement.unifyInto(this); | ||
78 | } else { | ||
79 | // replacement.referringConstraints.addAll(this.referringConstraints); | ||
80 | // replacement.exportedParameter |= this.exportedParameter; | ||
81 | replacement.virtual &= this.virtual; | ||
82 | if (replacement.deducable != null && this.deducable != null) | ||
83 | replacement.deducable |= this.deducable; | ||
84 | else | ||
85 | replacement.deducable = null; | ||
86 | Set<PConstraint> snapshotConstraints = // avoid ConcurrentModificationX | ||
87 | new HashSet<PConstraint>(this.referringConstraints); | ||
88 | for (PConstraint constraint : snapshotConstraints) { | ||
89 | constraint.replaceVariable(this, replacement); | ||
90 | } | ||
91 | // replacementCheck() will fail from this point | ||
92 | this.unifiedInto = replacement; | ||
93 | pBody.noLongerUnique(this); | ||
94 | } | ||
95 | } | ||
96 | |||
97 | /** | ||
98 | * Determines whether there are any constraints that can deduce this variable | ||
99 | */ | ||
100 | public boolean isDeducable() { | ||
101 | replacementCheck(); | ||
102 | if (deducable == null) { | ||
103 | deducable = false; | ||
104 | for (PConstraint pConstraint : getReferringConstraints()) { | ||
105 | if (pConstraint.getDeducedVariables().contains(this)) { | ||
106 | deducable = true; | ||
107 | break; | ||
108 | } | ||
109 | } | ||
110 | } | ||
111 | return deducable; | ||
112 | } | ||
113 | |||
114 | /** | ||
115 | * Register that this variable is referred by the given constraint. | ||
116 | * | ||
117 | * @param constraint | ||
118 | */ | ||
119 | public void refer(PConstraint constraint) { | ||
120 | pBody.checkMutability(); | ||
121 | replacementCheck(); | ||
122 | deducable = null; | ||
123 | referringConstraints.add(constraint); | ||
124 | } | ||
125 | |||
126 | /** | ||
127 | * Register that this variable is no longer referred by the given constraint. | ||
128 | * | ||
129 | * @param constraint | ||
130 | */ | ||
131 | public void unrefer(PConstraint constraint) { | ||
132 | pBody.checkMutability(); | ||
133 | replacementCheck(); | ||
134 | deducable = null; | ||
135 | referringConstraints.remove(constraint); | ||
136 | } | ||
137 | |||
138 | /** | ||
139 | * @return the name of the pattern variable. This is the unique key of the pattern node. | ||
140 | */ | ||
141 | public String getName() { | ||
142 | replacementCheck(); | ||
143 | return name; | ||
144 | } | ||
145 | |||
146 | /** | ||
147 | * @return the virtual | ||
148 | */ | ||
149 | public boolean isVirtual() { | ||
150 | replacementCheck(); | ||
151 | return virtual; | ||
152 | } | ||
153 | |||
154 | /** | ||
155 | * @return the referringConstraints | ||
156 | */ | ||
157 | public Set<PConstraint> getReferringConstraints() { | ||
158 | replacementCheck(); | ||
159 | return referringConstraints; | ||
160 | } | ||
161 | |||
162 | @SuppressWarnings("unchecked") | ||
163 | public <ConstraintType> Set<ConstraintType> getReferringConstraintsOfType(Class<ConstraintType> constraintClass) { | ||
164 | replacementCheck(); | ||
165 | Set<ConstraintType> result = new HashSet<ConstraintType>(); | ||
166 | for (PConstraint pConstraint : referringConstraints) { | ||
167 | if (constraintClass.isInstance(pConstraint)) | ||
168 | result.add((ConstraintType) pConstraint); | ||
169 | } | ||
170 | return result; | ||
171 | } | ||
172 | |||
173 | @Override | ||
174 | public String toString() { | ||
175 | // replacementCheck(); | ||
176 | return name;// + ":PatternNode"; | ||
177 | } | ||
178 | |||
179 | public PVariable getDirectUnifiedInto() { | ||
180 | return unifiedInto; | ||
181 | } | ||
182 | |||
183 | public PVariable getUnifiedIntoRoot() { | ||
184 | PVariable nextUnified = unifiedInto; | ||
185 | PVariable oldUnifiedInto = this; | ||
186 | while (nextUnified != null) { | ||
187 | oldUnifiedInto = nextUnified; | ||
188 | nextUnified = oldUnifiedInto.getDirectUnifiedInto(); | ||
189 | } | ||
190 | return oldUnifiedInto; // unifiedInto; | ||
191 | } | ||
192 | |||
193 | public boolean isUnique() { | ||
194 | return unifiedInto == null; | ||
195 | } | ||
196 | |||
197 | private void replacementCheck() { | ||
198 | if (unifiedInto != null) | ||
199 | throw new IllegalStateException("Illegal usage of variable " + name + " which has been replaced with " | ||
200 | + unifiedInto.name); | ||
201 | } | ||
202 | |||
203 | } | ||