diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend | 30 |
1 files changed, 22 insertions, 8 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 135b3f07..3c672f4b 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 | |||
@@ -1,15 +1,17 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula | 3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
13 | import java.util.HashMap | 15 | import java.util.HashMap |
14 | import java.util.Map | 16 | import java.util.Map |
15 | 17 | ||
@@ -22,17 +24,29 @@ class Logic2VampireLanguageMapperTrace { | |||
22 | public var VampireModel specification | 24 | public var VampireModel specification |
23 | public var VLSFofFormula logicLanguageBody | 25 | public var VLSFofFormula logicLanguageBody |
24 | public var VLSTerm formula | 26 | public var VLSTerm formula |
25 | //NOT NEEDED //public var VLSFunction constantDec | ||
26 | 27 | ||
28 | //Necessary containers | ||
27 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace | 29 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace |
28 | 30 | ||
31 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; | ||
32 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap | ||
33 | public val Map<Type, VLSTerm> type2PossibleNot = new HashMap | ||
34 | public val Map<Type, VLSTerm> type2And = new HashMap | ||
35 | |||
36 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | ||
37 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | ||
38 | public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap | ||
39 | |||
40 | |||
41 | //NOT NEEDED //public var VLSFunction constantDec | ||
42 | |||
43 | |||
44 | |||
29 | 45 | ||
30 | //NOT NEEDED //public val Map<ConstantDeclaration, VLSFunctionDeclaration> constantDeclaration2LanguageField = new HashMap | 46 | //NOT NEEDED //public val Map<ConstantDeclaration, VLSFunctionDeclaration> constantDeclaration2LanguageField = new HashMap |
31 | //public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap | 47 | //public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap |
32 | 48 | ||
33 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | ||
34 | 49 | ||
35 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | ||
36 | public val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | 50 | public val Map<Variable, VLSVariable> relationVar2VLS = new HashMap |
37 | public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap | 51 | public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap |
38 | 52 | ||