diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca')
3 files changed, 109 insertions, 4 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend index 7ab15fba..6b383b12 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend | |||
@@ -46,6 +46,7 @@ class Logic2VampireLanguageMapperTrace { | |||
46 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | 46 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions |
47 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | 47 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions |
48 | public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap | 48 | public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap |
49 | public var Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap | ||
49 | 50 | ||
50 | 51 | ||
51 | //NOT NEEDED //public var VLSFunction constantDec | 52 | //NOT NEEDED //public var VLSFunction constantDec |
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 2dec281d..18e97020 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 | |||
@@ -71,6 +71,7 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
71 | } | 71 | } |
72 | ] | 72 | ] |
73 | trace.rel2Predicate.put(r, rel) | 73 | trace.rel2Predicate.put(r, rel) |
74 | trace.predicate2Relation.put(rel, r) | ||
74 | it.left = support.duplicate(rel) | 75 | it.left = support.duplicate(rel) |
75 | it.right = support.unfoldAnd(relVar2TypeDecComply) | 76 | it.right = support.unfoldAnd(relVar2TypeDecComply) |
76 | ] | 77 | ] |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend index 0c93e3fe..5df47bbc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend | |||
@@ -22,22 +22,27 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | |||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl |
27 | import java.util.Arrays | ||
26 | import java.util.HashMap | 28 | import java.util.HashMap |
27 | import java.util.List | 29 | import java.util.List |
28 | import java.util.Map | 30 | import java.util.Map |
31 | import java.util.Set | ||
29 | 32 | ||
30 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 33 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl | ||
31 | 35 | ||
32 | class VampireModelInterpretation implements LogicModelInterpretation { | 36 | class VampireModelInterpretation implements LogicModelInterpretation { |
33 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | 37 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE |
34 | 38 | ||
35 | protected val Logic2VampireLanguageMapperTrace forwardTrace; | 39 | protected val Logic2VampireLanguageMapperTrace forwardTrace; |
36 | 40 | ||
41 | //These three maps capture all the information found in the Vampire output | ||
37 | private val Map<String, DefinedElement> name2DefinedElement = new HashMap | 42 | private val Map<String, DefinedElement> name2DefinedElement = new HashMap |
38 | private val Map<TypeDeclaration, List<DefinedElement>> type2DefinedElement = new HashMap | 43 | private val Map<TypeDeclaration, List<DefinedElement>> type2DefinedElement = new HashMap |
39 | 44 | private val Map<RelationDeclaration, List<String[]>> rel2Inst = new HashMap | |
40 | var num = -1 | 45 | //end |
41 | 46 | ||
42 | public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) { | 47 | public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) { |
43 | this.forwardTrace = trace | 48 | this.forwardTrace = trace |
@@ -74,6 +79,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
74 | // Fill keys of map | 79 | // Fill keys of map |
75 | val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] | 80 | val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] |
76 | val allTypeFunctions = trace.predicate2Type | 81 | val allTypeFunctions = trace.predicate2Type |
82 | println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl]) | ||
77 | 83 | ||
78 | for (type : allTypeDecls) { | 84 | for (type : allTypeDecls) { |
79 | type2DefinedElement.put(type as TypeDeclaration, newArrayList) | 85 | type2DefinedElement.put(type as TypeDeclaration, newArrayList) |
@@ -116,12 +122,56 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
116 | } | 122 | } |
117 | } | 123 | } |
118 | } | 124 | } |
119 | 125 | ||
120 | printMap() | 126 | printMap() |
127 | |||
128 | // 3. get relations | ||
129 | // Fill keys of map | ||
130 | val allRelDecls = trace.rel2Predicate.keySet.filter[class == RelationDeclarationImpl] | ||
131 | val allRelFunctions = trace.predicate2Relation | ||
132 | |||
133 | for (rel : allRelDecls) { | ||
134 | rel2Inst.put(rel as RelationDeclaration, newArrayList) | ||
135 | } | ||
136 | |||
137 | // USE THE DECLARE_<RELATION_NAME> FORMULAS TO SEE WHAT THE RELATIONS ARE | ||
138 | val relFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_r_"] | ||
139 | |||
140 | for (formula : relFormulas) { | ||
141 | // get associated type | ||
142 | val associatedRelName = (formula as VLSTffFormula).name.substring(10) | ||
143 | val associatedRelFunction = allRelFunctions.keySet.filter[constant == associatedRelName]. | ||
144 | get(0) as VLSFunction | ||
145 | val associatedRel = associatedRelFunction.lookup(allRelFunctions) as RelationDeclaration | ||
146 | |||
147 | // get definedElements | ||
148 | var andFormulaTerm = formula.fofFormula | ||
149 | end = false | ||
150 | val List<String[]> instances = newArrayList | ||
151 | while (!end) { | ||
152 | if (andFormulaTerm.class == VLSAndImpl) { | ||
153 | val andFormula = andFormulaTerm as VLSAnd | ||
154 | val andRight = andFormula.right | ||
155 | addRelIfNotNeg(andRight, instances) | ||
156 | andFormulaTerm = andFormula.left | ||
157 | } else { | ||
158 | addRelIfNotNeg(andFormulaTerm as VLSTerm, instances) | ||
159 | end = true | ||
160 | } | ||
161 | |||
162 | } | ||
163 | for (elem : instances) { | ||
164 | associatedRel.lookup(rel2Inst).add(elem) | ||
165 | } | ||
166 | |||
167 | } | ||
168 | |||
169 | // printMap2() | ||
121 | 170 | ||
122 | } | 171 | } |
123 | 172 | ||
124 | def printMap() { | 173 | def printMap() { |
174 | println("------------------") | ||
125 | for (key : type2DefinedElement.keySet) { | 175 | for (key : type2DefinedElement.keySet) { |
126 | println(key.name + "==>") | 176 | println(key.name + "==>") |
127 | for (elem : key.lookup(type2DefinedElement)) { | 177 | for (elem : key.lookup(type2DefinedElement)) { |
@@ -132,6 +182,19 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
132 | } | 182 | } |
133 | println() | 183 | println() |
134 | } | 184 | } |
185 | |||
186 | def printMap2() { | ||
187 | println("------------------") | ||
188 | for (key : rel2Inst.keySet) { | ||
189 | println(key.name + "==>") | ||
190 | for (elem : key.lookup(rel2Inst)) { | ||
191 | print("[" + elem.get(0) + "-" + elem.get(1) + "], ") | ||
192 | } | ||
193 | println() | ||
194 | |||
195 | } | ||
196 | println() | ||
197 | } | ||
135 | 198 | ||
136 | def private addIfNotNeg(VLSTerm term, List<DefinedElement> list) { | 199 | def private addIfNotNeg(VLSTerm term, List<DefinedElement> list) { |
137 | if (term.class != VLSUnaryNegationImpl) { | 200 | if (term.class != VLSUnaryNegationImpl) { |
@@ -140,6 +203,15 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
140 | list.add(defnElem) | 203 | list.add(defnElem) |
141 | } | 204 | } |
142 | } | 205 | } |
206 | |||
207 | def private addRelIfNotNeg(VLSTerm term, List<String[]> list) { | ||
208 | if (term.class != VLSUnaryNegationImpl) { | ||
209 | val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor | ||
210 | val nodeName2 = ((term as VLSFunction).terms.get(1) as VLSFunctionAsTerm).functor | ||
211 | val strArr = newArrayList(nodeName1, nodeName2) | ||
212 | list.add(strArr) | ||
213 | } | ||
214 | } | ||
143 | 215 | ||
144 | def private add2ConstDefMap(VLSEquality eq) { | 216 | def private add2ConstDefMap(VLSEquality eq) { |
145 | val defElemConst = (eq.right as VLSConstant) | 217 | val defElemConst = (eq.right as VLSConstant) |
@@ -160,7 +232,15 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
160 | } | 232 | } |
161 | 233 | ||
162 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | 234 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { |
163 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 235 | val node1 = (parameterSubstitution.get(0) as DefinedElement).name |
236 | val node2 = (parameterSubstitution.get(1) as DefinedElement).name | ||
237 | val realRelations = relation.lookup(rel2Inst) | ||
238 | for (real : realRelations){ | ||
239 | if(real.contains(node1) && real.contains(node2)){ | ||
240 | return true | ||
241 | } | ||
242 | } | ||
243 | return false | ||
164 | } | 244 | } |
165 | 245 | ||
166 | override getInterpretation(ConstantDeclaration constant) { | 246 | override getInterpretation(ConstantDeclaration constant) { |
@@ -180,3 +260,26 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
180 | } | 260 | } |
181 | 261 | ||
182 | } | 262 | } |
263 | |||
264 | /** | ||
265 | * Helper class for efficiently matching parameter substitutions for functions and relations. | ||
266 | */ | ||
267 | class ParameterSubstitution { | ||
268 | val Object[] data; | ||
269 | |||
270 | new(Object[] data) { | ||
271 | this.data = data | ||
272 | } | ||
273 | |||
274 | override equals(Object obj) { | ||
275 | if(obj === this) return true else if(obj == null) return false | ||
276 | if (obj instanceof ParameterSubstitution) { | ||
277 | return Arrays.equals(this.data, obj.data) | ||
278 | } | ||
279 | return false | ||
280 | } | ||
281 | |||
282 | override hashCode() { | ||
283 | Arrays.hashCode(data) | ||
284 | } | ||
285 | } | ||