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 | 126 |
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 @@ | |||
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 | } |