1 files changed, 98 insertions, 28 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
index ff5a192e..820d0db2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
@@ -1,16 +1,19 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
-import java.util.List
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
+import java.util.HashMap
+import java.util.List
+import java.util.Map
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
 class Logic2VampireLanguageMapper_ContainmentMapper {
        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -74,54 +77,121 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
                // for each edge, if the pointedTo element exists,the edge must exist also
                val varA = createVLSVariable => [it.name = "A"]
                val varB = createVLSVariable => [it.name = "B"]
+                val varC = createVLSVariable => [it.name = "C"]
                val varList = newArrayList(varB, varA)
+                val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap
                for (l : relationsList) {
-                        val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString
+                        val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)
-                        val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type
+//                      val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type
-                        val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type
+                        val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type)
+                        val toFunc = toType.lookup(trace.type2Predicate)
+                        addToMap(type2cont, toFunc, rel)
-                        val listForAnd = newArrayList
+                        for (c : toType.subtypes) {
-//                      listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB))
+                                addToMap(type2cont, toFunc, rel)
-                        listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList))
+                        }
+//                      val listForAnd = newArrayList
+////                    listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB))
+//                      listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList))
 //                      listForAnd.add(createVLSInequality => [
 //                              it.left = support.duplicate(varA)
 //                              it.right = support.duplicate(varB)
 //                      ])
+                        // remove subtypes of elements being pointed to
+//                      var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
+//                      containmentListCopy.remove(pointingTo)
+//                      for (c : pointingTo.subtypes) {
+//                              containmentListCopy.remove(c)
+//                      }
+                        // STEP 3
+                        // Ensure that an objct only has 1 parent
+                        val relFormula = createVLSFofFormula => [
+                                it.name = support.toIDMultiple("noDupCont", rel.constant.toString)
+                                it.fofRole = "axiom"
+                                it.fofFormula = createVLSExistentialQuantifier => [
+                                        it.variables += support.duplicate(varA)
+                                        it.variables += support.duplicate(varB)
+                                        it.operand = createVLSImplies => [
+                                                it.left = support.duplicate(rel, newArrayList(varA, varB))
+                                                it.right = createVLSUnaryNegation => [
+                                                        it.operand = createVLSExistentialQuantifier => [
+                                                                it.variables += support.duplicate(varC)
+                                                                it.variables += support.duplicate(varB)
+                                                                it.operand = support.duplicate(rel, newArrayList(varC, varB))
+                                                        ]
+                                                ]
+                                        ]
+                                ]
+                        ]
+                        trace.specification.formulas += relFormula
+                }
+// STEP  CONT'D
+                for (e : type2cont.entrySet) {
                        val relFormula = createVLSFofFormula => [
-                                it.name = support.toIDMultiple("containment", relName)
+                                it.name = support.toIDMultiple("containment", e.key.constant.toString)
                                it.fofRole = "axiom"
                                it.fofFormula = createVLSUniversalQuantifier => [
                                        it.variables += support.duplicate(varA)
                                        it.operand = createVLSImplies => [
-                                                it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA)
+                                                it.left = support.duplicate(e.key, varA)
                                                it.right = createVLSExistentialQuantifier => [
                                                        it.variables += support.duplicate(varB)
-                                                        it.operand = support.unfoldAnd(listForAnd)
+                                                        if (e.value.length > 1) {
-                                                ]
+                                                                it.operand = makeUnique(e.value)
+                                                        } else {
+                                                                it.operand = e.value.get(0)
+                                                        }
-                                                createVLSEquality => [
-                                                        it.left = support.duplicate(variable)
-                                                        it.right = createVLSConstant => [
-                                                                it.name = "o1"
-                                                        ]
                                                ]
                                        ]
                                ]
                        ]
                        trace.specification.formulas += relFormula
-                        var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
-                        containmentListCopy.remove(pointingTo)
-                        for (c : pointingTo.subtypes) {
-                                containmentListCopy.remove(c)
-                        }
                }
-        // STEP 3
-        // Ensure that an objct only has 1 parent
        // STEP 4
        // Ensure that there are no cycles in the hierarchy (maybe same as for step3?)
        }
+        protected def VLSTerm makeUnique(List<VLSFunction> list) {
+                val List<VLSTerm> possibleNots = newArrayList
+                val List<VLSTerm> uniqueRels = newArrayList
+                for (t1 : list) {
+                        for (t2 : list) {
+                                if (t1 == t2) {
+                                        val fct = support.duplicate(t2)
+                                        possibleNots.add(fct)
+                                } else {
+                                        val op = support.duplicate(t2)
+                                        val negFct = createVLSUnaryNegation => [
+                                                it.operand = op
+                                        ]
+                                        possibleNots.add(negFct)
+                                }
+                        }
+                        uniqueRels.add(support.unfoldAnd(possibleNots))
+                        possibleNots.clear
+                }
+                return support.unfoldOr(uniqueRels)
+        }
+        protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) {
+                if (!type2cont.containsKey(toFunc)) {
+                        type2cont.put(toFunc, newArrayList(rel))
+                } else {
+                        if (!type2cont.get(toFunc).contains(rel)) {
+                                type2cont.get(toFunc).add(rel)
+                        // type2cont.replace(toFunc, newArrayList(firstRel))
+                        }
+                }
+        }
 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index ff5a192e..820d0db2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
@@ -1,16 +1,19 @@
1	package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder	1	package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
2		2
		3	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd
		4	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
		5	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
3	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable	6	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
4	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory	7	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
5	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
6	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
7	import java.util.List
8	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference	8	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
		9	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
9	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type	10	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
		11	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
		12	import java.util.HashMap
		13	import java.util.List
		14	import java.util.Map
10		15
11	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*	16	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
12	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
13	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
14		17
15	class Logic2VampireLanguageMapper_ContainmentMapper {	18	class Logic2VampireLanguageMapper_ContainmentMapper {
16	private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE	19	private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -74,54 +77,121 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
74	// for each edge, if the pointedTo element exists,the edge must exist also	77	// for each edge, if the pointedTo element exists,the edge must exist also
75	val varA = createVLSVariable => [it.name = "A"]	78	val varA = createVLSVariable => [it.name = "A"]
76	val varB = createVLSVariable => [it.name = "B"]	79	val varB = createVLSVariable => [it.name = "B"]
		80	val varC = createVLSVariable => [it.name = "C"]
77	val varList = newArrayList(varB, varA)	81	val varList = newArrayList(varB, varA)
78		82	val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap
79	for (l : relationsList) {	83	for (l : relationsList) {
80	val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString	84	val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)
81	val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type	85	// val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type
82	val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type	86	val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type)
		87	val toFunc = toType.lookup(trace.type2Predicate)
		88
		89	addToMap(type2cont, toFunc, rel)
83		90
84	val listForAnd = newArrayList	91	for (c : toType.subtypes) {
85	// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB))	92	addToMap(type2cont, toFunc, rel)
86	listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList))	93	}
		94
		95	// val listForAnd = newArrayList
		96	//// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB))
		97	// listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList))
87	// listForAnd.add(createVLSInequality => [	98	// listForAnd.add(createVLSInequality => [
88	// it.left = support.duplicate(varA)	99	// it.left = support.duplicate(varA)
89	// it.right = support.duplicate(varB)	100	// it.right = support.duplicate(varB)
90	// ])	101	// ])
		102	// remove subtypes of elements being pointed to
		103	// var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
		104	// containmentListCopy.remove(pointingTo)
		105	// for (c : pointingTo.subtypes) {
		106	// containmentListCopy.remove(c)
		107	// }
		108	// STEP 3
		109	// Ensure that an objct only has 1 parent
		110	val relFormula = createVLSFofFormula => [
		111	it.name = support.toIDMultiple("noDupCont", rel.constant.toString)
		112	it.fofRole = "axiom"
		113	it.fofFormula = createVLSExistentialQuantifier => [
		114	it.variables += support.duplicate(varA)
		115	it.variables += support.duplicate(varB)
		116	it.operand = createVLSImplies => [
		117	it.left = support.duplicate(rel, newArrayList(varA, varB))
		118	it.right = createVLSUnaryNegation => [
		119	it.operand = createVLSExistentialQuantifier => [
		120	it.variables += support.duplicate(varC)
		121	it.variables += support.duplicate(varB)
		122	it.operand = support.duplicate(rel, newArrayList(varC, varB))
		123
		124	]
		125	]
		126	]
		127	]
		128	]
		129	trace.specification.formulas += relFormula
91		130
		131	}
		132
		133	// STEP CONT'D
		134	for (e : type2cont.entrySet) {
92	val relFormula = createVLSFofFormula => [	135	val relFormula = createVLSFofFormula => [
93	it.name = support.toIDMultiple("containment", relName)	136	it.name = support.toIDMultiple("containment", e.key.constant.toString)
94	it.fofRole = "axiom"	137	it.fofRole = "axiom"
95		138
96	it.fofFormula = createVLSUniversalQuantifier => [	139	it.fofFormula = createVLSUniversalQuantifier => [
97	it.variables += support.duplicate(varA)	140	it.variables += support.duplicate(varA)
98	it.operand = createVLSImplies => [	141	it.operand = createVLSImplies => [
99	it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA)	142	it.left = support.duplicate(e.key, varA)
100	it.right = createVLSExistentialQuantifier => [	143	it.right = createVLSExistentialQuantifier => [
101	it.variables += support.duplicate(varB)	144	it.variables += support.duplicate(varB)
102	it.operand = support.unfoldAnd(listForAnd)	145	if (e.value.length > 1) {
103	]	146	it.operand = makeUnique(e.value)
		147	} else {
		148	it.operand = e.value.get(0)
		149	}
104		150
105	createVLSEquality => [
106	it.left = support.duplicate(variable)
107	it.right = createVLSConstant => [
108	it.name = "o1"
109	]
110	]	151	]
111	]	152	]
112	]	153	]
113	]	154	]
114	trace.specification.formulas += relFormula	155	trace.specification.formulas += relFormula
115	var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type	156
116	containmentListCopy.remove(pointingTo)
117	for (c : pointingTo.subtypes) {
118	containmentListCopy.remove(c)
119	}
120	}	157	}
121		158
122	// STEP 3
123	// Ensure that an objct only has 1 parent
124	// STEP 4	159	// STEP 4
125	// Ensure that there are no cycles in the hierarchy (maybe same as for step3?)	160	// Ensure that there are no cycles in the hierarchy (maybe same as for step3?)
126	}	161	}
		162
		163	protected def VLSTerm makeUnique(List<VLSFunction> list) {
		164	val List<VLSTerm> possibleNots = newArrayList
		165	val List<VLSTerm> uniqueRels = newArrayList
		166
		167	for (t1 : list) {
		168	for (t2 : list) {
		169	if (t1 == t2) {
		170	val fct = support.duplicate(t2)
		171	possibleNots.add(fct)
		172	} else {
		173	val op = support.duplicate(t2)
		174	val negFct = createVLSUnaryNegation => [
		175	it.operand = op
		176	]
		177	possibleNots.add(negFct)
		178	}
		179	}
		180	uniqueRels.add(support.unfoldAnd(possibleNots))
		181	possibleNots.clear
		182	}
		183	return support.unfoldOr(uniqueRels)
		184	}
		185
		186	protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) {
		187	if (!type2cont.containsKey(toFunc)) {
		188	type2cont.put(toFunc, newArrayList(rel))
		189	} else {
		190	if (!type2cont.get(toFunc).contains(rel)) {
		191	type2cont.get(toFunc).add(rel)
		192	// type2cont.replace(toFunc, newArrayList(firstRel))
		193	}
		194
		195	}
		196	}
127	}	197	}