diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend | 60 |
1 files changed, 49 insertions, 11 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 8e0e0b11..c56b54be 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 | |||
@@ -14,10 +14,11 @@ import java.util.List | |||
14 | import java.util.Map | 14 | import java.util.Map |
15 | 15 | ||
16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
17 | 18 | ||
18 | class Logic2VampireLanguageMapper_ContainmentMapper { | 19 | class Logic2VampireLanguageMapper_ContainmentMapper { |
19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 20 | val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
20 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | 21 | val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support |
21 | val Logic2VampireLanguageMapper base | 22 | val Logic2VampireLanguageMapper base |
22 | private val VLSVariable variable = createVLSVariable => [it.name = "A"] | 23 | private val VLSVariable variable = createVLSVariable => [it.name = "A"] |
23 | 24 | ||
@@ -34,6 +35,8 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
34 | 35 | ||
35 | val containmentListCopy = hierarchy.typesOrderedInHierarchy | 36 | val containmentListCopy = hierarchy.typesOrderedInHierarchy |
36 | val relationsList = hierarchy.containmentRelations | 37 | val relationsList = hierarchy.containmentRelations |
38 | val toRemove = newArrayList | ||
39 | |||
37 | // STEP 1 | 40 | // STEP 1 |
38 | // Find root element | 41 | // Find root element |
39 | for (l : relationsList) { | 42 | for (l : relationsList) { |
@@ -46,16 +49,51 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
46 | } | 49 | } |
47 | } | 50 | } |
48 | 51 | ||
49 | for (c : containmentListCopy) { | 52 | // OLD |
50 | if(c.isIsAbstract) { | 53 | // for (c : containmentListCopy) { |
51 | containmentListCopy.remove(c) | 54 | // if(c.isIsAbstract) { |
52 | } | 55 | // toRemove.add(c) |
53 | } | 56 | // } |
54 | 57 | // } | |
55 | // State that there must exist 1 and only 1 root element | 58 | // State that there must exist 1 and only 1 root element |
56 | val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString | 59 | // val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString |
57 | val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) | 60 | // val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) |
58 | 61 | ||
62 | var topTermVar = containmentListCopy.get(0) | ||
63 | for (l : relationsList) { | ||
64 | var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type | ||
65 | if(containmentListCopy.contains(pointingFrom)) { | ||
66 | //The correct topTerm will be identified | ||
67 | topTermVar = pointingFrom | ||
68 | } | ||
69 | } | ||
70 | |||
71 | val topName = topTermVar.lookup(trace.type2Predicate).constant.toString | ||
72 | val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate)) | ||
73 | |||
74 | |||
75 | |||
76 | var topLvlIsInInitModel = false | ||
77 | var topLvlString = "" | ||
78 | for ( c : topTermVar.subtypes) { | ||
79 | if (c.class.simpleName.equals("TypeDefinitionImpl") ) { | ||
80 | |||
81 | for (d : (c as TypeDefinition).elements) { | ||
82 | if (trace.definedElement2String.containsKey(d)) { | ||
83 | topLvlIsInInitModel = true | ||
84 | topLvlString = d.lookup(trace.definedElement2String) | ||
85 | } | ||
86 | } | ||
87 | |||
88 | } | ||
89 | |||
90 | |||
91 | } | ||
92 | val topInIM = topLvlIsInInitModel | ||
93 | val topStr = topLvlString | ||
94 | print(topInIM) | ||
95 | print(topStr) | ||
96 | |||
59 | val contTop = createVLSFofFormula => [ | 97 | val contTop = createVLSFofFormula => [ |
60 | it.name = support.toIDMultiple("containment_topLevel", topName) | 98 | it.name = support.toIDMultiple("containment_topLevel", topName) |
61 | it.fofRole = "axiom" | 99 | it.fofRole = "axiom" |
@@ -67,7 +105,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
67 | it.right = createVLSEquality => [ | 105 | it.right = createVLSEquality => [ |
68 | it.left = support.duplicate(variable) | 106 | it.left = support.duplicate(variable) |
69 | it.right = createVLSConstant => [ | 107 | it.right = createVLSConstant => [ |
70 | it.name = "o1" | 108 | it.name = if (topInIM) topStr else "o1" |
71 | ] | 109 | ] |
72 | ] | 110 | ] |
73 | ] | 111 | ] |