diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | 42 |
1 files changed, 38 insertions, 4 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index 06ec585c..090cf916 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | |||
@@ -1,20 +1,21 @@ | |||
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.VLSConstant | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable |
11 | import java.util.ArrayList | 14 | import java.util.ArrayList |
12 | import java.util.HashMap | 15 | import java.util.HashMap |
13 | import java.util.List | 16 | import java.util.List |
14 | import java.util.Map | 17 | import java.util.Map |
15 | import org.eclipse.emf.common.util.EList | 18 | import org.eclipse.emf.common.util.EList |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality | ||
18 | 19 | ||
19 | class Logic2VampireLanguageMapper_Support { | 20 | class Logic2VampireLanguageMapper_Support { |
20 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 21 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -28,10 +29,28 @@ class Logic2VampireLanguageMapper_Support { | |||
28 | ids.split("\\s+").join("_") | 29 | ids.split("\\s+").join("_") |
29 | } | 30 | } |
30 | 31 | ||
32 | //Term Handling | ||
31 | //TODO Make more general | 33 | //TODO Make more general |
32 | def protected VLSVariable duplicate(VLSVariable vrbl) { | 34 | def protected VLSVariable duplicate(VLSVariable term) { |
33 | return createVLSVariable => [it.name = vrbl.name] | 35 | return createVLSVariable => [it.name = term.name] |
36 | } | ||
37 | |||
38 | def protected VLSFunction duplicate(VLSFunction term) { | ||
39 | return createVLSFunction => [ | ||
40 | it.constant = term.constant | ||
41 | for ( v : term.terms){ | ||
42 | it.terms += duplicate(v as VLSVariable) | ||
43 | } | ||
44 | ] | ||
34 | } | 45 | } |
46 | |||
47 | def protected VLSFunction duplicate(VLSFunction term, VLSVariable v) { | ||
48 | return createVLSFunction => [ | ||
49 | it.constant = term.constant | ||
50 | it.terms += duplicate(v) | ||
51 | ] | ||
52 | } | ||
53 | |||
35 | 54 | ||
36 | def protected VLSFunction topLevelTypeFunc() { | 55 | def protected VLSFunction topLevelTypeFunc() { |
37 | return createVLSFunction => [ | 56 | return createVLSFunction => [ |
@@ -175,6 +194,21 @@ class Logic2VampireLanguageMapper_Support { | |||
175 | 194 | ||
176 | ] | 195 | ] |
177 | } | 196 | } |
197 | |||
198 | def protected boolean dfsSupertypeCheck(Type type, Type type2) { | ||
199 | // There is surely a better way to do this | ||
200 | if (type.supertypes.isEmpty) | ||
201 | return false | ||
202 | else { | ||
203 | if (type.supertypes.contains(type2)) | ||
204 | return true | ||
205 | else { | ||
206 | for (supertype : type.supertypes) { | ||
207 | if(dfsSupertypeCheck(supertype, type2)) return true | ||
208 | } | ||
209 | } | ||
210 | } | ||
211 | } | ||
178 | 212 | ||
179 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | 213 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { |
180 | new HashMap(map1) => [putAll(map2)] | 214 | new HashMap(map1) => [putAll(map2)] |