1 files changed, 97 insertions, 86 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index 0ae06bc3..2dec281d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -44,9 +44,20 @@ class Logic2VampireLanguageMapper_RelationMapper {
                }
+                //deciding name of relation
+                val nameArray = r.name.split(" ")
+                var relNameVar = ""
+                if (nameArray.length == 3) {
+                        relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
+                }
+                else {
+                        relNameVar = r.name
+                }
+                val relName = relNameVar
+                
                val comply = createVLSFofFormula=> [
-                        val nameArray = r.name.split(" ")
+                        
-                        it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2))
+                        it.name = support.toIDMultiple("compliance", relName)
                        it.fofRole = "axiom"
                        it.fofFormula = createVLSUniversalQuantifier => [
                                for (v : relVar2VLS) {
@@ -54,7 +65,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                                }
                                it.operand = createVLSImplies => [
                                        val rel = createVLSFunction => [
-                                                it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2))
+                                                it.constant = support.toIDMultiple("r", relName)
                                                for (v : relVar2VLS) {
                                                        it.terms += support.duplicate(v)
                                                }
@@ -71,89 +82,89 @@ class Logic2VampireLanguageMapper_RelationMapper {
        def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) {
-                // 1. store all variables in support wrt their name
+//              // 1. store all variables in support wrt their name
-                // 1.1 if variable has type, creating list of type declarations
+//              // 1.1 if variable has type, creating list of type declarations
-//              val VLSVariable variable = createVLSVariable => [it.name = "A"]
+////            val VLSVariable variable = createVLSVariable => [it.name = "A"]
-                val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
+//              val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
-                val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
+//              val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
-                val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
+//              val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
-                val typedefs = new ArrayList<VLSTerm>
+//              val typedefs = new ArrayList<VLSTerm>
+//
-                for (variable : reldef.variables) {
+//              for (variable : reldef.variables) {
-                        val v = createVLSVariable => [
+//                      val v = createVLSVariable => [
-                                it.name = support.toIDMultiple("V", variable.name)
+//                              it.name = support.toIDMultiple("V", variable.name)
-                        ]
+//                      ]
-                        relationVar2VLS.put(variable, v)
+//                      relationVar2VLS.put(variable, v)
+//
-                        val varTypeComply = createVLSFunction => [
+//                      val varTypeComply = createVLSFunction => [
-                                it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
+//                              it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
-                                it.terms += support.duplicate(v)
+//                              it.terms += support.duplicate(v)
-                        ]
+//                      ]
-                        relationVar2TypeDecComply.put(variable, varTypeComply)
+//                      relationVar2TypeDecComply.put(variable, varTypeComply)
-                        relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
+//                      relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
-                }
+//              }
-                val nameArray = reldef.name.split(" ")
+//              val nameArray = reldef.name.split(" ")
-                val comply = createVLSFofFormula => [
+//              val comply = createVLSFofFormula => [
-                        it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
+//                      it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
-                                nameArray.get(nameArray.length - 1))
+//                              nameArray.get(nameArray.length - 1))
-                        it.fofRole = "axiom"
+//                      it.fofRole = "axiom"
-                        it.fofFormula = createVLSUniversalQuantifier => [
+//                      it.fofFormula = createVLSUniversalQuantifier => [
-                                for (variable : reldef.variables) {
+//                              for (variable : reldef.variables) {
-                                        it.variables += support.duplicate(variable.lookup(relationVar2VLS))
+//                                      it.variables += support.duplicate(variable.lookup(relationVar2VLS))
+//
-                                }
+//                              }
-                                it.operand = createVLSImplies => [
+//                              it.operand = createVLSImplies => [
-                                        it.left = createVLSFunction => [
+//                                      it.left = createVLSFunction => [
-                                                it.constant = support.toIDMultiple("rel", reldef.name)
+//                                              it.constant = support.toIDMultiple("rel", reldef.name)
-                                                for (variable : reldef.variables) {
+//                                              for (variable : reldef.variables) {
-                                                        val v = createVLSVariable => [
+//                                                      val v = createVLSVariable => [
-                                                                it.name = variable.lookup(relationVar2VLS).name
+//                                                              it.name = variable.lookup(relationVar2VLS).name
-                                                        ]
+//                                                      ]
-                                                        it.terms += v
+//                                                      it.terms += v
-                                                }
+//                                              }
-                                        ]
+//                                      ]
-                                        it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
+//                                      it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
-                                ]
+//                              ]
-                        ]
+//                      ]
-                ]
+//              ]
+//
-                val res = createVLSFofFormula => [
+//              val res = createVLSFofFormula => [
-                        it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
+//                      it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
-                                nameArray.get(nameArray.length - 1))
+//                              nameArray.get(nameArray.length - 1))
-                        it.fofRole = "axiom"
+//                      it.fofRole = "axiom"
-                        it.fofFormula = createVLSUniversalQuantifier => [
+//                      it.fofFormula = createVLSUniversalQuantifier => [
-                                for (variable : reldef.variables) {
+//                              for (variable : reldef.variables) {
-                                        val v = createVLSVariable => [
+//                                      val v = createVLSVariable => [
-                                                it.name = variable.lookup(relationVar2VLS).name
+//                                              it.name = variable.lookup(relationVar2VLS).name
-                                        ]
+//                                      ]
-                                        it.variables += v
+//                                      it.variables += v
+//
-                                }
+//                              }
-                                it.operand = createVLSImplies => [
+//                              it.operand = createVLSImplies => [
-                                        it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
+//                                      it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
-                                        it.right = createVLSEquivalent => [
+//                                      it.right = createVLSEquivalent => [
-                                                it.left = createVLSFunction => [
+//                                              it.left = createVLSFunction => [
-                                                        it.constant = support.toIDMultiple("rel", reldef.name)
+//                                                      it.constant = support.toIDMultiple("rel", reldef.name)
-                                                        for (variable : reldef.variables) {
+//                                                      for (variable : reldef.variables) {
-                                                                val v = createVLSVariable => [
+//                                                              val v = createVLSVariable => [
-                                                                        it.name = variable.lookup(relationVar2VLS).name
+//                                                                      it.name = variable.lookup(relationVar2VLS).name
-                                                                ]
+//                                                              ]
-                                                                it.terms += v
+//                                                              it.terms += v
+//
-                                                        }
+//                                                      }
-                                                ]
+//                                              ]
-                                                it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
+//                                              it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
-                                        ]
+//                                      ]
+//
-                                ]
+//                              ]
+//
-                        ]
+//                      ]
+//
-                ]
+//              ]
+//
-                // trace.relationDefinition2Predicate.put(r,res)
+//              // trace.relationDefinition2Predicate.put(r,res)
-                trace.specification.formulas += comply;
+//              trace.specification.formulas += comply;
-                trace.specification.formulas += res;
+//              trace.specification.formulas += res;
        }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend index 0ae06bc3..2dec281d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -44,9 +44,20 @@ class Logic2VampireLanguageMapper_RelationMapper {
44		44
45	}	45	}
46		46
		47	//deciding name of relation
		48	val nameArray = r.name.split(" ")
		49	var relNameVar = ""
		50	if (nameArray.length == 3) {
		51	relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
		52	}
		53	else {
		54	relNameVar = r.name
		55	}
		56	val relName = relNameVar
		57
47	val comply = createVLSFofFormula=> [	58	val comply = createVLSFofFormula=> [
48	val nameArray = r.name.split(" ")	59
49	it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2))	60	it.name = support.toIDMultiple("compliance", relName)
50	it.fofRole = "axiom"	61	it.fofRole = "axiom"
51	it.fofFormula = createVLSUniversalQuantifier => [	62	it.fofFormula = createVLSUniversalQuantifier => [
52	for (v : relVar2VLS) {	63	for (v : relVar2VLS) {
@@ -54,7 +65,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
54	}	65	}
55	it.operand = createVLSImplies => [	66	it.operand = createVLSImplies => [
56	val rel = createVLSFunction => [	67	val rel = createVLSFunction => [
57	it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2))	68	it.constant = support.toIDMultiple("r", relName)
58	for (v : relVar2VLS) {	69	for (v : relVar2VLS) {
59	it.terms += support.duplicate(v)	70	it.terms += support.duplicate(v)
60	}	71	}
@@ -71,89 +82,89 @@ class Logic2VampireLanguageMapper_RelationMapper {
71		82
72	def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) {	83	def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) {
73		84
74	// 1. store all variables in support wrt their name	85	// // 1. store all variables in support wrt their name
75	// 1.1 if variable has type, creating list of type declarations	86	// // 1.1 if variable has type, creating list of type declarations
76	// val VLSVariable variable = createVLSVariable => [it.name = "A"]	87	//// val VLSVariable variable = createVLSVariable => [it.name = "A"]
77	val Map<Variable, VLSVariable> relationVar2VLS = new HashMap	88	// val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
78	val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap	89	// val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
79	val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap	90	// val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
80	val typedefs = new ArrayList<VLSTerm>	91	// val typedefs = new ArrayList<VLSTerm>
81		92	//
82	for (variable : reldef.variables) {	93	// for (variable : reldef.variables) {
83	val v = createVLSVariable => [	94	// val v = createVLSVariable => [
84	it.name = support.toIDMultiple("V", variable.name)	95	// it.name = support.toIDMultiple("V", variable.name)
85	]	96	// ]
86	relationVar2VLS.put(variable, v)	97	// relationVar2VLS.put(variable, v)
87		98	//
88	val varTypeComply = createVLSFunction => [	99	// val varTypeComply = createVLSFunction => [
89	it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)	100	// it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
90	it.terms += support.duplicate(v)	101	// it.terms += support.duplicate(v)
91	]	102	// ]
92	relationVar2TypeDecComply.put(variable, varTypeComply)	103	// relationVar2TypeDecComply.put(variable, varTypeComply)
93	relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))	104	// relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
94	}	105	// }
95	val nameArray = reldef.name.split(" ")	106	// val nameArray = reldef.name.split(" ")
96	val comply = createVLSFofFormula => [	107	// val comply = createVLSFofFormula => [
97	it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),	108	// it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
98	nameArray.get(nameArray.length - 1))	109	// nameArray.get(nameArray.length - 1))
99	it.fofRole = "axiom"	110	// it.fofRole = "axiom"
100	it.fofFormula = createVLSUniversalQuantifier => [	111	// it.fofFormula = createVLSUniversalQuantifier => [
101	for (variable : reldef.variables) {	112	// for (variable : reldef.variables) {
102	it.variables += support.duplicate(variable.lookup(relationVar2VLS))	113	// it.variables += support.duplicate(variable.lookup(relationVar2VLS))
103		114	//
104	}	115	// }
105	it.operand = createVLSImplies => [	116	// it.operand = createVLSImplies => [
106	it.left = createVLSFunction => [	117	// it.left = createVLSFunction => [
107	it.constant = support.toIDMultiple("rel", reldef.name)	118	// it.constant = support.toIDMultiple("rel", reldef.name)
108	for (variable : reldef.variables) {	119	// for (variable : reldef.variables) {
109	val v = createVLSVariable => [	120	// val v = createVLSVariable => [
110	it.name = variable.lookup(relationVar2VLS).name	121	// it.name = variable.lookup(relationVar2VLS).name
111	]	122	// ]
112	it.terms += v	123	// it.terms += v
113	}	124	// }
114	]	125	// ]
115	it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))	126	// it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
116	]	127	// ]
117	]	128	// ]
118	]	129	// ]
119		130	//
120	val res = createVLSFofFormula => [	131	// val res = createVLSFofFormula => [
121	it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),	132	// it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
122	nameArray.get(nameArray.length - 1))	133	// nameArray.get(nameArray.length - 1))
123	it.fofRole = "axiom"	134	// it.fofRole = "axiom"
124	it.fofFormula = createVLSUniversalQuantifier => [	135	// it.fofFormula = createVLSUniversalQuantifier => [
125	for (variable : reldef.variables) {	136	// for (variable : reldef.variables) {
126	val v = createVLSVariable => [	137	// val v = createVLSVariable => [
127	it.name = variable.lookup(relationVar2VLS).name	138	// it.name = variable.lookup(relationVar2VLS).name
128	]	139	// ]
129	it.variables += v	140	// it.variables += v
130		141	//
131	}	142	// }
132	it.operand = createVLSImplies => [	143	// it.operand = createVLSImplies => [
133	it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))	144	// it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
134	it.right = createVLSEquivalent => [	145	// it.right = createVLSEquivalent => [
135	it.left = createVLSFunction => [	146	// it.left = createVLSFunction => [
136	it.constant = support.toIDMultiple("rel", reldef.name)	147	// it.constant = support.toIDMultiple("rel", reldef.name)
137	for (variable : reldef.variables) {	148	// for (variable : reldef.variables) {
138	val v = createVLSVariable => [	149	// val v = createVLSVariable => [
139	it.name = variable.lookup(relationVar2VLS).name	150	// it.name = variable.lookup(relationVar2VLS).name
140	]	151	// ]
141	it.terms += v	152	// it.terms += v
142		153	//
143	}	154	// }
144	]	155	// ]
145	it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)	156	// it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
146	]	157	// ]
147		158	//
148	]	159	// ]
149		160	//
150	]	161	// ]
151		162	//
152	]	163	// ]
153		164	//
154	// trace.relationDefinition2Predicate.put(r,res)	165	// // trace.relationDefinition2Predicate.put(r,res)
155	trace.specification.formulas += comply;	166	// trace.specification.formulas += comply;
156	trace.specification.formulas += res;	167	// trace.specification.formulas += res;
157		168
158	}	169	}
159		170