diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ | 345 |
1 files changed, 345 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ new file mode 100644 index 00000000..29acd681 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ | |||
@@ -0,0 +1,345 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import java.util.Map | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
6 | import java.util.List | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
11 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant | ||
12 | import edu.mit.csail.sdg.alloy4compiler.ast.Expr | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
33 | import java.util.HashMap | ||
34 | import edu.mit.csail.sdg.alloy4compiler.ast.Decl | ||
35 | import java.util.ArrayList | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
40 | import edu.mit.csail.sdg.alloy4compiler.ast.Attr | ||
41 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
44 | import javax.naming.OperationNotSupportedException | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant | ||
47 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.AlloySpecification | ||
48 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.Multiplicity | ||
49 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.InverseReference | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
52 | |||
53 | class AlloyInput{ | ||
54 | public val List<PrimSig> typeDeclarations=new ArrayList | ||
55 | public val List<Expr> functionDeclarations=new ArrayList | ||
56 | public val List<Expr> assertions=new ArrayList | ||
57 | public val List<Expr> multiplicityConstraints=new ArrayList | ||
58 | public val List<Expr> inverseConstraints=new ArrayList | ||
59 | } | ||
60 | |||
61 | class Logic2AlloyApiMapperTrace { | ||
62 | val Map<Type, PrimSig> typeMap | ||
63 | val Map<DefinedElement, PrimSig> elementMap | ||
64 | //val Map<Function, SMTFunctionDeclaration> functionMap | ||
65 | val Map<Relation,Expr> relationMap | ||
66 | //val Map<Constant,SMTFunctionDeclaration> constantMap | ||
67 | |||
68 | new () { | ||
69 | this.typeMap = new HashMap | ||
70 | this.elementMap = new HashMap | ||
71 | //this.functionMap = new HashMap | ||
72 | this.relationMap = new HashMap | ||
73 | //this.constantMap = new HashMap | ||
74 | } | ||
75 | new (Map<Type, PrimSig> typeMap, | ||
76 | Map<DefinedElement, PrimSig> elementMap, | ||
77 | //Map<Function, SMTFunctionDeclaration> functionMap, | ||
78 | Map<Relation,Expr> relationMap/*, | ||
79 | Map<Constant,SMTFunctionDeclaration> constantMap*/) | ||
80 | { | ||
81 | this.typeMap = typeMap | ||
82 | this.elementMap = elementMap | ||
83 | //this.functionMap = functionMap | ||
84 | this.relationMap = relationMap | ||
85 | //this.constantMap = constantMap | ||
86 | } | ||
87 | |||
88 | def types() { typeMap } | ||
89 | def elements() { elementMap } | ||
90 | //def functions() { functionMap } | ||
91 | def relations() { relationMap } | ||
92 | //def constants() { constantMap } | ||
93 | } | ||
94 | |||
95 | class Logic2AlloyApiMapper{ | ||
96 | //TODO output | ||
97 | public def TracedOutput<List<PrimSig>, Logic2AlloyApiMapperTrace> transformProblem(LogicProblem problem) { | ||
98 | val documentInput = new AlloyInput() | ||
99 | //createSMTInput => [satCommand = createSMTSimpleSatCommand getModelCommand = createSMTGetModelCommand] | ||
100 | //val document = createSMTDocument => [input = documentInput] | ||
101 | val List<PrimSig> document=new ArrayList | ||
102 | val trace = new Logic2AlloyApiMapperTrace | ||
103 | |||
104 | // Trafo | ||
105 | documentInput.typeDeclarations += problem.types.map[transformType(trace)] | ||
106 | //documentInput.functionDeclarations += problem.functions.map[transformFunction(trace)] | ||
107 | documentInput.functionDeclarations += problem.relations.map[transformRelation(trace)] | ||
108 | //documentInput.functionDeclarations += problem.constants.map[transformConstant(trace)] | ||
109 | documentInput.assertions += problem.assertions.map[transformAssertion(trace)] | ||
110 | |||
111 | |||
112 | val alloySpecification = problem.specifications.filter(AlloySpecification).head | ||
113 | |||
114 | for(mult: alloySpecification.multiplicities){ | ||
115 | if(mult.min>0){ | ||
116 | documentInput.multiplicityConstraints+=mult.transformMultiplicityLowerBound(trace) | ||
117 | } | ||
118 | if(mult.max!=-1){ | ||
119 | documentInput.multiplicityConstraints+=mult.transformMultiplicityUpperBound(trace) | ||
120 | } | ||
121 | } | ||
122 | |||
123 | for(inv: alloySpecification.inverses){ | ||
124 | documentInput.inverseConstraints += inv.transformInverse(trace) | ||
125 | } | ||
126 | // End trafo | ||
127 | |||
128 | return new TracedOutput(document,trace) | ||
129 | } | ||
130 | |||
131 | def Expr transformMultiplicityLowerBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){ | ||
132 | |||
133 | val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl | ||
134 | return (forallVariable.get.cardinality.gte(ExprConstant.makeNUMBER(multiplicity.min))).forAll(forallVariable) | ||
135 | |||
136 | } | ||
137 | |||
138 | def Expr transformMultiplicityUpperBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){ | ||
139 | |||
140 | val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl | ||
141 | return (forallVariable.get.cardinality.lte(ExprConstant.makeNUMBER(multiplicity.max))).forAll(forallVariable) | ||
142 | |||
143 | } | ||
144 | |||
145 | def Expr transformInverse(InverseReference inverse, Logic2AlloyApiMapperTrace trace){ | ||
146 | return trace.relations.get(inverse.inverseOf.get(0)).equal(trace.relations.get(inverse.inverseOf.get(1)).transpose) | ||
147 | } | ||
148 | |||
149 | private def toID(List<String> names) {names.join("!") } | ||
150 | |||
151 | def dispatch protected transformType(TypeDefinition declaration, Logic2AlloyApiMapperTrace trace) { | ||
152 | val result = new PrimSig(declaration.name.toID, Attr.ABSTRACT) | ||
153 | trace.types.put(declaration,result) | ||
154 | return result | ||
155 | } | ||
156 | |||
157 | def protected transformDefinedElement(TypeDefinition enumType, DefinedElement element, Logic2AlloyApiMapperTrace trace) { | ||
158 | val result=new PrimSig(element.name.toID, trace.types.get(enumType), Attr.ONE) | ||
159 | trace.elements.put(element,result) | ||
160 | return result | ||
161 | } | ||
162 | |||
163 | def dispatch protected transformType(TypeDeclaration declaration, Logic2AlloyApiMapperTrace trace) { | ||
164 | //TODO �r�kles, absztrakt | ||
165 | val result = new PrimSig(declaration.name.toID) | ||
166 | trace.types.put(declaration,result) | ||
167 | return result | ||
168 | } | ||
169 | |||
170 | def dispatch protected transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyApiMapperTrace trace) { | ||
171 | throw new UnsupportedOperationException("BoolTypeReference is not supported.") | ||
172 | } | ||
173 | def dispatch protected transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyApiMapperTrace trace) { | ||
174 | return PrimSig.SIGINT | ||
175 | } | ||
176 | def dispatch protected transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyApiMapperTrace trace) { | ||
177 | throw new UnsupportedOperationException("RealTypeReference is not supported.") | ||
178 | } | ||
179 | def dispatch protected PrimSig transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyApiMapperTrace trace) { | ||
180 | return trace.types.get(complexTypeReference.referred) | ||
181 | } | ||
182 | |||
183 | /*def protected transformFunction(Function declaration, Logic2AlloyApiMapperTrace trace) { | ||
184 | val functionDeclaration = createSMTFunctionDeclaration => [ | ||
185 | name = declaration.name.toID | ||
186 | range = declaration.range.transformTypeReference(trace) | ||
187 | parameters+= declaration.parameters.map[transformTypeReference(trace)] | ||
188 | ] | ||
189 | trace.functions.put(declaration,functionDeclaration) | ||
190 | return functionDeclaration | ||
191 | }*/ | ||
192 | |||
193 | def transformRelation(Relation relation, Logic2AlloyApiMapperTrace trace) { | ||
194 | if(relation.parameters.size==2){ | ||
195 | trace.relations.put(relation,(relation.parameters.get(0).transformTypeReference(trace) as PrimSig).addField(relation.name.toID, (relation.parameters.get(1).transformTypeReference(trace) as PrimSig).setOf)) | ||
196 | } else{ | ||
197 | throw new OperationNotSupportedException("More parameters are not supported.") | ||
198 | } | ||
199 | } | ||
200 | |||
201 | /*def transformConstant(Constant constant, Logic2AlloyApiMapperTrace trace) { | ||
202 | val smtConstant = createSMTFunctionDeclaration => [ | ||
203 | name = constant.name.toID | ||
204 | range = transformTypeReference(constant.type, trace) | ||
205 | ] | ||
206 | trace.constants.put(constant,smtConstant) | ||
207 | return smtConstant | ||
208 | }*/ | ||
209 | |||
210 | def protected Expr transformAssertion(Assertion assertion, Logic2AlloyApiMapperTrace trace) { | ||
211 | |||
212 | return assertion.value.transformTerm(trace,emptyMap) | ||
213 | } | ||
214 | |||
215 | def dispatch protected Expr transformTerm(BoolLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
216 | throw new UnsupportedOperationException("Bool is not supported") | ||
217 | //open util/boolean, autoPay: Bool | ||
218 | //https://code.google.com/p/valloy2009/source/browse/trunk/src/models/util/boolean.als?r=142 | ||
219 | } | ||
220 | def dispatch protected Expr transformTerm(IntLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
221 | return ExprConstant.makeNUMBER(literal.value) | ||
222 | } | ||
223 | def dispatch protected Expr transformTerm(RealLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
224 | throw new UnsupportedOperationException("Real number is not supported") | ||
225 | } | ||
226 | def dispatch protected Expr transformTerm(Not not, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
227 | return not.operand.transformTerm(trace,variables).not} | ||
228 | def dispatch protected Expr transformTerm(And and, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
229 | val List<Expr> operands= and.operands.map[transformTerm(trace,variables)] | ||
230 | var andTerm=operands.get(0) | ||
231 | for(Integer i: 1..(operands.size-1)){ | ||
232 | andTerm=andTerm.and(operands.get(i)) | ||
233 | } | ||
234 | return andTerm | ||
235 | } | ||
236 | def dispatch protected Expr transformTerm(Or or, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
237 | val List<Expr> operands= or.operands.map[transformTerm(trace,variables)] | ||
238 | var orTerm=operands.get(0) | ||
239 | for(Integer i: 1..(operands.size-1)){ | ||
240 | orTerm=orTerm.or(operands.get(i)) | ||
241 | } | ||
242 | return orTerm | ||
243 | } | ||
244 | def dispatch protected Expr transformTerm(Impl impl, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
245 | return impl.leftOperand.transformTerm(trace,variables).implies(impl.rightOperand.transformTerm(trace,variables)) | ||
246 | } | ||
247 | def dispatch protected Expr transformTerm(Iff ifExpression, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
248 | return ifExpression.leftOperand.transformTerm(trace,variables).iff(ifExpression.rightOperand.transformTerm(trace,variables)) | ||
249 | } | ||
250 | def dispatch protected Expr transformTerm(MoreThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
251 | return moreThan.leftOperand.transformTerm(trace,variables).gt(moreThan.rightOperand.transformTerm(trace,variables)) | ||
252 | } | ||
253 | def dispatch protected Expr transformTerm(LessThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
254 | return lessThan.leftOperand.transformTerm(trace,variables).lt(lessThan.rightOperand.transformTerm(trace,variables)) | ||
255 | } | ||
256 | def dispatch protected Expr transformTerm(MoreOrEqualThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
257 | return moreThan.leftOperand.transformTerm(trace,variables).gte(moreThan.rightOperand.transformTerm(trace,variables)) | ||
258 | } | ||
259 | def dispatch protected Expr transformTerm(LessOrEqualThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
260 | return lessThan.leftOperand.transformTerm(trace,variables).lte(lessThan.rightOperand.transformTerm(trace,variables)) | ||
261 | } | ||
262 | def dispatch protected Expr transformTerm(Equals equals, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
263 | return equals.leftOperand.transformTerm(trace,variables).equal(equals.rightOperand.transformTerm(trace,variables)) | ||
264 | } | ||
265 | /*def dispatch protected Expr transformTerm(Distinct distinct, Logic2AlloyApiMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
266 | createSMTDistinct => [ operands += distinct.operands.map[transformTerm(trace,variables)]]}*/ | ||
267 | def dispatch protected Expr transformTerm(Plus plus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
268 | return plus.leftOperand.transformTerm(trace,variables).plus(plus.rightOperand.transformTerm(trace,variables)) | ||
269 | } | ||
270 | def dispatch protected Expr transformTerm(Minus minus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
271 | return minus.leftOperand.transformTerm(trace,variables).minus(minus.rightOperand.transformTerm(trace,variables)) | ||
272 | } | ||
273 | def dispatch protected Expr transformTerm(Multiply multiply, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
274 | return multiply.leftOperand.transformTerm(trace,variables).mul(multiply.rightOperand.transformTerm(trace,variables)) | ||
275 | } | ||
276 | def dispatch protected Expr transformTerm(Divison div, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
277 | return div.leftOperand.transformTerm(trace,variables).div(div.rightOperand.transformTerm(trace,variables)) | ||
278 | } | ||
279 | def dispatch protected Expr transformTerm(Mod mod, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
280 | throw new UnsupportedOperationException("Modulo is not supported.") | ||
281 | } | ||
282 | def dispatch protected Expr transformTerm(Forall forall, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
283 | return configureForall(forall,trace,variables) | ||
284 | } | ||
285 | def dispatch protected Expr transformTerm(Exists exists, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
286 | return configureExists(exists,trace,variables) | ||
287 | } | ||
288 | def dispatch protected Expr transformTerm(SymbolicValue symbolicValue, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
289 | symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } | ||
290 | |||
291 | def private configureForall( | ||
292 | Forall quantifiedExpression, | ||
293 | Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) | ||
294 | { | ||
295 | val allVariables = new HashMap(variables) | ||
296 | val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size) | ||
297 | |||
298 | for(logicVariable: quantifiedExpression.quantifiedVariables) { | ||
299 | val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl | ||
300 | allVariables.put(logicVariable, newAlloyVariable) | ||
301 | newAlloyVariables += newAlloyVariable | ||
302 | } | ||
303 | val variable0=newAlloyVariables.get(0) | ||
304 | newAlloyVariables.remove(0) | ||
305 | return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forAll(variable0, newAlloyVariables) | ||
306 | } | ||
307 | |||
308 | def private configureExists( | ||
309 | Exists quantifiedExpression, | ||
310 | Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) | ||
311 | { | ||
312 | val allVariables = new HashMap(variables) | ||
313 | val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size) | ||
314 | |||
315 | for(logicVariable: quantifiedExpression.quantifiedVariables) { | ||
316 | val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl | ||
317 | allVariables.put(logicVariable, newAlloyVariable) | ||
318 | newAlloyVariables += newAlloyVariable | ||
319 | } | ||
320 | val variable0=newAlloyVariables.get(0) | ||
321 | newAlloyVariables.remove(0) | ||
322 | return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forSome(variable0, newAlloyVariables) | ||
323 | } | ||
324 | |||
325 | def dispatch protected Expr transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
326 | return trace.elements.get(referred) | ||
327 | } | ||
328 | def dispatch protected Expr transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
329 | return variables.get(variable).get | ||
330 | } | ||
331 | /*def dispatch protected Expr transformSymbolicReference(Function function, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
332 | val result = createSMTSymbolicValue => [sv | sv.symbolicReference = trace.functions.get(function)] | ||
333 | for(paramSubstitution : parameterSubstitutions) { | ||
334 | result.parameterSubstitutions.add(paramSubstitution.transformTerm(trace,variables)) | ||
335 | } | ||
336 | return result | ||
337 | }*/ | ||
338 | def dispatch protected Expr transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
339 | return trace.relations.get(relation) | ||
340 | } | ||
341 | def dispatch protected Expr transformSymbolicReference(Constant constant, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
342 | //createSMTSymbolicValue => [symbolicReference = trace.constants.get(constant)] | ||
343 | throw new UnsupportedOperationException("Constant is not supported") | ||
344 | } | ||
345 | } \ No newline at end of file | ||