1 files changed, 123 insertions, 0 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
new file mode 100644
index 00000000..0820f47d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
@@ -0,0 +1,123 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+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.Type
+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
+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+        val Logic2VampireLanguageMapper base
+        private val VLSVariable variable = createVLSVariable => [it.name = "A"]
+        public new(Logic2VampireLanguageMapper base) {
+                this.base = base
+        }
+        def public void transformContainment(List<ContainmentHierarchy> hierarchies,
+                Logic2VampireLanguageMapperTrace trace) {
+                // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST
+                // TEMP
+                val hierarchy = hierarchies.get(0)
+                val containmentListCopy = hierarchy.typesOrderedInHierarchy
+                val relationsList = hierarchy.containmentRelations
+                // STEP 1
+                // Find root element
+                for (l : relationsList) {
+                        var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
+                        containmentListCopy.remove(pointingTo)
+                        for (c : pointingTo.subtypes) {
+                                containmentListCopy.remove(c)
+                        }
+                }
+                // State that there must exist 1 and only 1 root element
+                val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString
+                val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))
+                val contTop = createVLSFofFormula => [
+                        it.name = support.toIDMultiple("containment_topLevel", topName)
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                it.variables += support.duplicate(variable)
+                                it.operand = createVLSEquivalent => [
+                                        it.left = topTerm
+                                        it.right = createVLSEquality => [
+                                                it.left = support.duplicate(variable)
+                                                it.right = createVLSConstant => [
+                                                        it.name = "o1"
+                                                ]
+                                        ]
+                                ]
+                        ]
+//                      it.fofFormula = support.duplicate(
+//                              topTerm,
+//                              createVLSFunctionAsTerm => [
+//                                      it.functor = "o1"
+//                              ]
+//                      )
+                ]
+                trace.specification.formulas += contTop
+                // STEP 2
+                // 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 varList = newArrayList(varB, varA)
+                for (l : relationsList) {
+                        val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString
+                        val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type
+                        val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type
+                        val relFormula = createVLSFofFormula => [
+                                it.name = support.toIDMultiple("containment", relName)
+                                it.fofRole = "axiom"
+                                it.fofFormula = createVLSUniversalQuantifier => [
+                                        it.variables += support.duplicate(varA)
+                                        it.operand = createVLSImplies => [
+                                                it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA)
+                                                it.right = createVLSExistentialQuantifier => [
+                                                        it.variables += support.duplicate(varB)
+                                                        it.operand = createVLSAnd => [
+                                                                it.left = support.duplicate(fromType.lookup(trace.type2Predicate), varB)
+                                                                it.right = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate),
+                                                                        varList)
+                                                        ]
+                                                ]
+                                                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?)
+        }
+}

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 new file mode 100644 index 00000000..0820f47d --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
@@ -0,0 +1,123 @@
	1	package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
	2
	3	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
	4	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
	9	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
	10
	11	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
	15	class Logic2VampireLanguageMapper_ContainmentMapper {
	16	private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
	17	private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
	18	val Logic2VampireLanguageMapper base
	19	private val VLSVariable variable = createVLSVariable => [it.name = "A"]
	20
	21	public new(Logic2VampireLanguageMapper base) {
	22	this.base = base
	23	}
	24
	25	def public void transformContainment(List<ContainmentHierarchy> hierarchies,
	26	Logic2VampireLanguageMapperTrace trace) {
	27
	28	// TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST
	29	// TEMP
	30	val hierarchy = hierarchies.get(0)
	31
	32	val containmentListCopy = hierarchy.typesOrderedInHierarchy
	33	val relationsList = hierarchy.containmentRelations
	34	// STEP 1
	35	// Find root element
	36	for (l : relationsList) {
	37	var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
	38	containmentListCopy.remove(pointingTo)
	39	for (c : pointingTo.subtypes) {
	40	containmentListCopy.remove(c)
	41	}
	42	}
	43
	44	// State that there must exist 1 and only 1 root element
	45	val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString
	46	val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))
	47
	48	val contTop = createVLSFofFormula => [
	49	it.name = support.toIDMultiple("containment_topLevel", topName)
	50	it.fofRole = "axiom"
	51
	52	it.fofFormula = createVLSUniversalQuantifier => [
	53	it.variables += support.duplicate(variable)
	54	it.operand = createVLSEquivalent => [
	55	it.left = topTerm
	56	it.right = createVLSEquality => [
	57	it.left = support.duplicate(variable)
	58	it.right = createVLSConstant => [
	59	it.name = "o1"
	60	]
	61	]
	62	]
	63	]
	64	// it.fofFormula = support.duplicate(
	65	// topTerm,
	66	// createVLSFunctionAsTerm => [
	67	// it.functor = "o1"
	68	// ]
	69	// )
	70	]
	71	trace.specification.formulas += contTop
	72
	73	// STEP 2
	74	// for each edge, if the pointedTo element exists,the edge must exist also
	75	val varA = createVLSVariable => [it.name = "A"]
	76	val varB = createVLSVariable => [it.name = "B"]
	77	val varList = newArrayList(varB, varA)
	78
	79	for (l : relationsList) {
	80	val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString
	81	val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type
	82	val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type
	83
	84	val relFormula = createVLSFofFormula => [
	85	it.name = support.toIDMultiple("containment", relName)
	86	it.fofRole = "axiom"
	87
	88	it.fofFormula = createVLSUniversalQuantifier => [
	89	it.variables += support.duplicate(varA)
	90	it.operand = createVLSImplies => [
	91	it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA)
	92	it.right = createVLSExistentialQuantifier => [
	93	it.variables += support.duplicate(varB)
	94	it.operand = createVLSAnd => [
	95	it.left = support.duplicate(fromType.lookup(trace.type2Predicate), varB)
	96	it.right = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate),
	97	varList)
	98	]
	99	]
	100
	101	createVLSEquality => [
	102	it.left = support.duplicate(variable)
	103	it.right = createVLSConstant => [
	104	it.name = "o1"
	105	]
	106	]
	107	]
	108	]
	109	]
	110	trace.specification.formulas += relFormula
	111	var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
	112	containmentListCopy.remove(pointingTo)
	113	for (c : pointingTo.subtypes) {
	114	containmentListCopy.remove(c)
	115	}
	116	}
	117
	118	// STEP 3
	119	// Ensure that an objct only has 1 parent
	120	// STEP 4
	121	// Ensure that there are no cycles in the hierarchy (maybe same as for step3?)
	122	}
	123	}