1 files changed, 104 insertions, 99 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index cd48a032..e2c15b75 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -48,6 +48,8 @@ class Logic2VampireLanguageMapper {
                this)
        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(
                this)
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(
+                this)
        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper
        public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) {
@@ -72,11 +74,15 @@ class Logic2VampireLanguageMapper {
 //                      it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem))
                ]
-                // call mappers
+                // TYPE MAPPER
                if (!problem.types.isEmpty) {
                        typeMapper.transformTypes(problem.types, problem.elements, this, trace)
                }
+                // SCOPE MAPPER
+                scopeMapper.transformScope(config, trace)
+                
+                
                trace.constantDefinitions = problem.collectConstantDefinitions
                trace.relationDefinitions = problem.collectRelationDefinitions
@@ -204,8 +210,9 @@ class Logic2VampireLanguageMapper {
                ]
        }
-        def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+        def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace,
-                support.unfoldDistinctTerms(this,distinct.operands,trace,variables) }
+                Map<Variable, VLSVariable> variables) { support.unfoldDistinctTerms(this, distinct.operands, trace, variables) }
 //      
 //              def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
 //              createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] }
@@ -228,12 +235,14 @@ class Logic2VampireLanguageMapper {
                support.createExistentiallyQuantifiedExpression(this, exists, trace, variables)
        }
-        def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+        def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
                return createVLSFunction => [
-                        it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name )
+                        it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name)
                        it.terms += instanceOf.value.transformTerm(trace, variables)
                ]
        }
 //      
 //      def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
 //              return this.relationMapper.transformTransitiveRelationReference(
@@ -253,50 +262,49 @@ class Logic2VampireLanguageMapper {
        def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,
                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
                Map<Variable, VLSVariable> variables) {
-                        typeMapper.transformReference(referred, trace)
+                typeMapper.transformReference(referred, trace)
-                }
+        }
-                def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant,
+        def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant,
-                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                        Map<Variable, VLSVariable> variables) {
+                Map<Variable, VLSVariable> variables) {
-                                // might need to make sure that only declared csts get transformed. see for Alloy
+                // might need to make sure that only declared csts get transformed. see for Alloy
-                                val res = createVLSConstant => [
+                val res = createVLSConstant => [
-                                        // ask if necessary VLSConstantDeclaration and not just directly strng
+                        // ask if necessary VLSConstantDeclaration and not just directly strng
-                                        it.name = support.toID(constant.name)
+                        it.name = support.toID(constant.name)
-                                ]
+                ]
-                                // no postprocessing cuz booleans are accepted
+                // no postprocessing cuz booleans are accepted
-                                return res
+                return res
-                        }
+        }
-                        // NOT NEEDED FOR NOW
+        // NOT NEEDED FOR NOW
-                        // TODO
+        // TODO
-                        def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant,
+        def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant,
-                                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                Map<Variable, VLSVariable> variables) {
+                Map<Variable, VLSVariable> variables) {
 //              val res = createVLSFunctionCall => [
 //                      it.referredDefinition = constant.lookup(trace.constantDefinition2Function)
 //              ]
 //              return support.postprocessResultOfSymbolicReference(constant.type,res,trace)
-                                }
+        }
-                                def dispatch protected VLSTerm transformSymbolicReference(Variable variable,
+        def dispatch protected VLSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions,
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
-                                        Map<Variable, VLSVariable> variables) {
-                                        // cannot treat variable as function (constant) because of name ID not being the same
+                // cannot treat variable as function (constant) because of name ID not being the same
-                                        // below does not work
+                // below does not work
-                                        val res = createVLSVariable => [
+                val res = createVLSVariable => [
 //                                              it.name = support.toIDMultiple("Var", variable.lookup(variables).name)
-                                                it.name = support.toID(variable.lookup(variables).name)
+                        it.name = support.toID(variable.lookup(variables).name)
-                                        ]
+                ]
-                                        // no need for potprocessing cuz booleans are supported
+                // no need for potprocessing cuz booleans are supported
-                                        return res
+                return res
-                                }
+        }
-                                // TODO
+        // TODO
-                                def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function,
+        def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function,
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                        Map<Variable, VLSVariable> variables) {
+                Map<Variable, VLSVariable> variables) {
 //              if(trace.functionDefinitions.containsKey(function)) {
 //                      return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables)
 //              } else {
@@ -316,71 +324,68 @@ class Logic2VampireLanguageMapper {
 //                              return support.postprocessResultOfSymbolicReference(function.range,res,trace)
 //                      }
 //              }
-                                }
+        }
-                                // TODO
+        // TODO
-                                def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function,
+        def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function,
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                        Map<Variable, VLSVariable> variables) {
+                Map<Variable, VLSVariable> variables) {
 //              val result = createVLSFunctionCall => [
 //                      it.referredDefinition = function.lookup(trace.functionDefinition2Function)
 //                      it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)]
 //              ]
 //              return support.postprocessResultOfSymbolicReference(function.range,result,trace)
-                                }
+        }
-                                // TODO
+        // TODO
-                                /*
+        /*
-                                def dispatch protected VLSTerm transformSymbolicReference(Relation relation,
+         * def dispatch protected VLSTerm transformSymbolicReference(Relation relation,
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+         *      List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                        Map<Variable, VLSVariable> variables) {
+         *      Map<Variable, VLSVariable> variables) {
-                                        if (trace.relationDefinitions.containsKey(relation)) {
+         *      if (trace.relationDefinitions.containsKey(relation)) {
-                                                this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),
+         *              this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),
-                                                        parameterSubstitutions, trace, variables)
+         *                      parameterSubstitutions, trace, variables)
-                                        }
+         *      }
-                                        else {
+         *      else {
-//                                              if (relationMapper.transformToHostedField(relation, trace)) {
+         * //                                           if (relationMapper.transformToHostedField(relation, trace)) {
-//                                                      val VLSRelation = relation.lookup(trace.relationDeclaration2Field)
+         * //                                                   val VLSRelation = relation.lookup(trace.relationDeclaration2Field)
-//                                                      // R(a,b) =>
+         * //                                                   // R(a,b) =>
-//                                                      // b in a.R
+         * //                                                   // b in a.R
-//                                                      return createVLSSubset => [
+         * //                                                   return createVLSSubset => [
-//                                                              it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables)
+         * //                                                           it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables)
-//                                                              it.rightOperand = createVLSJoin => [
+         * //                                                           it.rightOperand = createVLSJoin => [
-//                                                                      it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables)
+         * //                                                                   it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables)
-//                                                                      it.rightOperand = createVLSReference => [it.referred = VLSRelation]
+         * //                                                                   it.rightOperand = createVLSReference => [it.referred = VLSRelation]
-//                                                              ]
+         * //                                                           ]
-//                                                      ]
+         * //                                                   ]
-//                                              } else {
+         * //                                           } else {
-//                                                      val target = createVLSJoin => [
+         * //                                                   val target = createVLSJoin => [
-//                                                              leftOperand = createVLSReference => [referred = trace.logicLanguage]
+         * //                                                           leftOperand = createVLSReference => [referred = trace.logicLanguage]
-//                                                              rightOperand = createVLSReference => [
+         * //                                                           rightOperand = createVLSReference => [
-//                                                                      referred = relation.lookup(trace.relationDeclaration2Global)
+         * //                                                                   referred = relation.lookup(trace.relationDeclaration2Global)
-//                                                              ]
+         * //                                                           ]
-//                                                      ]
+         * //                                                   ]
-//                                                      val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables)
+         * //                                                   val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables)
-//
+         * //
-//                                                      return createVLSSubset => [
+         * //                                                   return createVLSSubset => [
-//                                                              leftOperand = source
+         * //                                                           leftOperand = source
-//                                                              rightOperand = target
+         * //                                                           rightOperand = target
-//                                                      ]
+         * //                                                   ]
-//                                              }
+         * //                                           }
-                                        }
+         *      }
-                                }
+         * }
-                                */
+         */
+        // TODO
-                                // TODO
+        def dispatch protected VLSTerm transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions,
-                                def dispatch protected VLSTerm transformSymbolicReference(Relation relation,
+                Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                        Map<Variable, VLSVariable> variables) {
 //                                       createVLSFunction => [
 //                                              it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)
 //                                              it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
 //                                      ]
-                                        return createVLSFunction => [
+                return createVLSFunction => [
-                                                it.constant = support.toIDMultiple("rel", relation.name)
+                        it.constant = support.toIDMultiple("rel", relation.name)
-                                                it.terms += parameterSubstitutions.map[p | p.transformTerm(trace,variables)]
+                        it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
-                                        ]
+                ]
-                                }
+        }
-                        }
+}
-                        
-\ No newline at end of file

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index cd48a032..e2c15b75 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -48,6 +48,8 @@ class Logic2VampireLanguageMapper {
48	this)	48	this)
49	@Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(	49	@Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(
50	this)	50	this)
		51	@Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(
		52	this)
51	@Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper	53	@Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper
52		54
53	public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) {	55	public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) {
@@ -72,11 +74,15 @@ class Logic2VampireLanguageMapper {
72	// it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem))	74	// it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem))
73	]	75	]
74		76
75	// call mappers	77	// TYPE MAPPER
76	if (!problem.types.isEmpty) {	78	if (!problem.types.isEmpty) {
77	typeMapper.transformTypes(problem.types, problem.elements, this, trace)	79	typeMapper.transformTypes(problem.types, problem.elements, this, trace)
78	}	80	}
79		81
		82	// SCOPE MAPPER
		83	scopeMapper.transformScope(config, trace)
		84
		85
80	trace.constantDefinitions = problem.collectConstantDefinitions	86	trace.constantDefinitions = problem.collectConstantDefinitions
81	trace.relationDefinitions = problem.collectRelationDefinitions	87	trace.relationDefinitions = problem.collectRelationDefinitions
82		88
@@ -204,8 +210,9 @@ class Logic2VampireLanguageMapper {
204	]	210	]
205	}	211	}
206		212
207	def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {	213	def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace,
208	support.unfoldDistinctTerms(this,distinct.operands,trace,variables) }	214	Map<Variable, VLSVariable> variables) { support.unfoldDistinctTerms(this, distinct.operands, trace, variables) }
		215
209	//	216	//
210	// def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {	217	// def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
211	// createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] }	218	// createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] }
@@ -228,12 +235,14 @@ class Logic2VampireLanguageMapper {
228	support.createExistentiallyQuantifiedExpression(this, exists, trace, variables)	235	support.createExistentiallyQuantifiedExpression(this, exists, trace, variables)
229	}	236	}
230		237
231	def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {	238	def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace,
		239	Map<Variable, VLSVariable> variables) {
232	return createVLSFunction => [	240	return createVLSFunction => [
233	it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name )	241	it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name)
234	it.terms += instanceOf.value.transformTerm(trace, variables)	242	it.terms += instanceOf.value.transformTerm(trace, variables)
235	]	243	]
236	}	244	}
		245
237	//	246	//
238	// def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {	247	// def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
239	// return this.relationMapper.transformTransitiveRelationReference(	248	// return this.relationMapper.transformTransitiveRelationReference(
@@ -253,50 +262,49 @@ class Logic2VampireLanguageMapper {
253	def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,	262	def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,
254	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,	263	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
255	Map<Variable, VLSVariable> variables) {	264	Map<Variable, VLSVariable> variables) {
256	typeMapper.transformReference(referred, trace)	265	typeMapper.transformReference(referred, trace)
257	}	266	}
258		267
259	def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant,	268	def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant,
260	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,	269	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
261	Map<Variable, VLSVariable> variables) {	270	Map<Variable, VLSVariable> variables) {
262	// might need to make sure that only declared csts get transformed. see for Alloy	271	// might need to make sure that only declared csts get transformed. see for Alloy
263	val res = createVLSConstant => [	272	val res = createVLSConstant => [
264	// ask if necessary VLSConstantDeclaration and not just directly strng	273	// ask if necessary VLSConstantDeclaration and not just directly strng
265	it.name = support.toID(constant.name)	274	it.name = support.toID(constant.name)
266	]	275	]
267	// no postprocessing cuz booleans are accepted	276	// no postprocessing cuz booleans are accepted
268	return res	277	return res
269	}	278	}
270		279
271	// NOT NEEDED FOR NOW	280	// NOT NEEDED FOR NOW
272	// TODO	281	// TODO
273	def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant,	282	def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant,
274	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,	283	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
275	Map<Variable, VLSVariable> variables) {	284	Map<Variable, VLSVariable> variables) {
276	// val res = createVLSFunctionCall => [	285	// val res = createVLSFunctionCall => [
277	// it.referredDefinition = constant.lookup(trace.constantDefinition2Function)	286	// it.referredDefinition = constant.lookup(trace.constantDefinition2Function)
278	// ]	287	// ]
279	// return support.postprocessResultOfSymbolicReference(constant.type,res,trace)	288	// return support.postprocessResultOfSymbolicReference(constant.type,res,trace)
280	}	289	}
281		290
282	def dispatch protected VLSTerm transformSymbolicReference(Variable variable,	291	def dispatch protected VLSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions,
283	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,	292	Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
284	Map<Variable, VLSVariable> variables) {
285		293
286	// cannot treat variable as function (constant) because of name ID not being the same	294	// cannot treat variable as function (constant) because of name ID not being the same
287	// below does not work	295	// below does not work
288	val res = createVLSVariable => [	296	val res = createVLSVariable => [
289	// it.name = support.toIDMultiple("Var", variable.lookup(variables).name)	297	// it.name = support.toIDMultiple("Var", variable.lookup(variables).name)
290	it.name = support.toID(variable.lookup(variables).name)	298	it.name = support.toID(variable.lookup(variables).name)
291	]	299	]
292	// no need for potprocessing cuz booleans are supported	300	// no need for potprocessing cuz booleans are supported
293	return res	301	return res
294	}	302	}
295		303
296	// TODO	304	// TODO
297	def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function,	305	def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function,
298	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,	306	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
299	Map<Variable, VLSVariable> variables) {	307	Map<Variable, VLSVariable> variables) {
300	// if(trace.functionDefinitions.containsKey(function)) {	308	// if(trace.functionDefinitions.containsKey(function)) {
301	// return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables)	309	// return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables)
302	// } else {	310	// } else {
@@ -316,71 +324,68 @@ class Logic2VampireLanguageMapper {
316	// return support.postprocessResultOfSymbolicReference(function.range,res,trace)	324	// return support.postprocessResultOfSymbolicReference(function.range,res,trace)
317	// }	325	// }
318	// }	326	// }
319	}	327	}
320		328
321	// TODO	329	// TODO
322	def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function,	330	def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function,
323	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,	331	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
324	Map<Variable, VLSVariable> variables) {	332	Map<Variable, VLSVariable> variables) {
325	// val result = createVLSFunctionCall => [	333	// val result = createVLSFunctionCall => [
326	// it.referredDefinition = function.lookup(trace.functionDefinition2Function)	334	// it.referredDefinition = function.lookup(trace.functionDefinition2Function)
327	// it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)]	335	// it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)]
328	// ]	336	// ]
329	// return support.postprocessResultOfSymbolicReference(function.range,result,trace)	337	// return support.postprocessResultOfSymbolicReference(function.range,result,trace)
330	}	338	}
331		339
332	// TODO	340	// TODO
333	/*	341	/*
334	def dispatch protected VLSTerm transformSymbolicReference(Relation relation,	342	* def dispatch protected VLSTerm transformSymbolicReference(Relation relation,
335	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,	343	* List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
336	Map<Variable, VLSVariable> variables) {	344	* Map<Variable, VLSVariable> variables) {
337	if (trace.relationDefinitions.containsKey(relation)) {	345	* if (trace.relationDefinitions.containsKey(relation)) {
338	this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),	346	* this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),
339	parameterSubstitutions, trace, variables)	347	* parameterSubstitutions, trace, variables)
340	}	348	* }
341	else {	349	* else {
342	// if (relationMapper.transformToHostedField(relation, trace)) {	350	* // if (relationMapper.transformToHostedField(relation, trace)) {
343	// val VLSRelation = relation.lookup(trace.relationDeclaration2Field)	351	* // val VLSRelation = relation.lookup(trace.relationDeclaration2Field)
344	// // R(a,b) =>	352	* // // R(a,b) =>
345	// // b in a.R	353	* // // b in a.R
346	// return createVLSSubset => [	354	* // return createVLSSubset => [
347	// it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables)	355	* // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables)
348	// it.rightOperand = createVLSJoin => [	356	* // it.rightOperand = createVLSJoin => [
349	// it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables)	357	* // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables)
350	// it.rightOperand = createVLSReference => [it.referred = VLSRelation]	358	* // it.rightOperand = createVLSReference => [it.referred = VLSRelation]
351	// ]	359	* // ]
352	// ]	360	* // ]
353	// } else {	361	* // } else {
354	// val target = createVLSJoin => [	362	* // val target = createVLSJoin => [
355	// leftOperand = createVLSReference => [referred = trace.logicLanguage]	363	* // leftOperand = createVLSReference => [referred = trace.logicLanguage]
356	// rightOperand = createVLSReference => [	364	* // rightOperand = createVLSReference => [
357	// referred = relation.lookup(trace.relationDeclaration2Global)	365	* // referred = relation.lookup(trace.relationDeclaration2Global)
358	// ]	366	* // ]
359	// ]	367	* // ]
360	// val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables)	368	* // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables)
361	//	369	* //
362	// return createVLSSubset => [	370	* // return createVLSSubset => [
363	// leftOperand = source	371	* // leftOperand = source
364	// rightOperand = target	372	* // rightOperand = target
365	// ]	373	* // ]
366	// }	374	* // }
367	}	375	* }
368	}	376	* }
369	*/	377	*/
370		378	// TODO
371	// TODO	379	def dispatch protected VLSTerm transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions,
372	def dispatch protected VLSTerm transformSymbolicReference(Relation relation,	380	Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
373	List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
374	Map<Variable, VLSVariable> variables) {
375	// createVLSFunction => [	381	// createVLSFunction => [
376	// it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)	382	// it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)
377	// it.params += parameterSubstitutions.map[p\|p.transformTerm(trace, variables)]	383	// it.params += parameterSubstitutions.map[p\|p.transformTerm(trace, variables)]
378	// ]	384	// ]
379	return createVLSFunction => [	385	return createVLSFunction => [
380	it.constant = support.toIDMultiple("rel", relation.name)	386	it.constant = support.toIDMultiple("rel", relation.name)
381	it.terms += parameterSubstitutions.map[p \| p.transformTerm(trace,variables)]	387	it.terms += parameterSubstitutions.map[p\|p.transformTerm(trace, variables)]
382	]	388	]
383	}	389	}
384		390
385	}	391	}
386	\ No newline at end of file