diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | 162 |
1 files changed, 150 insertions, 12 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index 1f071635..bc0b3e23 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | |||
@@ -1,19 +1,157 @@ | |||
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.VLSFunction | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
12 | import java.util.ArrayList | ||
5 | import java.util.Collection | 13 | import java.util.Collection |
6 | import java.util.List | 14 | import java.util.List |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
8 | 15 | ||
9 | interface Logic2VampireLanguageMapper_TypeMapper { | 16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
10 | def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace); | 17 | |
11 | //samples below 2 lines | 18 | class Logic2VampireLanguageMapper_TypeMapper { |
12 | def List<VLSTerm> transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) | 19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
13 | def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) | 20 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support |
14 | 21 | val Logic2VampireLanguageMapper base | |
15 | def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace) | 22 | |
16 | def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace) | 23 | new(Logic2VampireLanguageMapper base) { |
17 | 24 | LogicproblemPackage.eINSTANCE.class | |
18 | def VampireModelInterpretation_TypeInterpretation getTypeInterpreter() | 25 | this.base = base |
19 | } \ No newline at end of file | 26 | } |
27 | |||
28 | def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { | ||
29 | |||
30 | // val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes | ||
31 | // trace.typeMapperTrace = typeTrace | ||
32 | val VLSVariable variable = createVLSVariable => [it.name = "A"] | ||
33 | |||
34 | // 1. Each type (class) is a predicate with a single variable as input | ||
35 | for (type : types) { | ||
36 | val typePred = createVLSFunction => [ | ||
37 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) | ||
38 | it.terms += support.duplicate(variable) | ||
39 | ] | ||
40 | // typeTrace.type2Predicate.put(type, typePred) | ||
41 | trace.type2Predicate.put(type, typePred) | ||
42 | } | ||
43 | |||
44 | // 2. Map each ENUM type definition to fof formula | ||
45 | for (type : types.filter(TypeDefinition)) { | ||
46 | val List<VLSFunction> orElems = newArrayList | ||
47 | for (e : type.elements) { | ||
48 | val enumElemPred = createVLSFunction => [ | ||
49 | it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2)) | ||
50 | it.terms += support.duplicate(variable) | ||
51 | ] | ||
52 | // typeTrace.element2Predicate.put(e, enumElemPred) | ||
53 | trace.element2Predicate.put(e, enumElemPred) | ||
54 | orElems.add(enumElemPred) | ||
55 | } | ||
56 | |||
57 | val res = createVLSFofFormula => [ | ||
58 | it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) | ||
59 | // below is temporary solution | ||
60 | it.fofRole = "axiom" | ||
61 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
62 | it.variables += support.duplicate(variable) | ||
63 | it.operand = createVLSEquivalent => [ | ||
64 | // it.left = createVLSFunction => [ | ||
65 | // it.constant = type.lookup(typeTrace.type2Predicate).constant | ||
66 | // it.terms += createVLSVariable => [it.name = "A"] | ||
67 | // ] | ||
68 | // it.left = type.lookup(typeTrace.type2Predicate) | ||
69 | it.left = type.lookup(trace.type2Predicate) | ||
70 | |||
71 | it.right = support.unfoldOr(orElems) | ||
72 | |||
73 | // TEMPPPPPPP | ||
74 | // it.right = support.unfoldOr(type.elements.map [e | | ||
75 | // | ||
76 | // createVLSEquality => [ | ||
77 | // it.left = support.duplicate(variable) | ||
78 | // it.right = createVLSDoubleQuote => [ | ||
79 | // it.value = "\"a" + e.name + "\"" | ||
80 | // ] | ||
81 | // ] | ||
82 | // ]) | ||
83 | // END TEMPPPPP | ||
84 | ] | ||
85 | ] | ||
86 | |||
87 | ] | ||
88 | trace.specification.formulas += res | ||
89 | } | ||
90 | |||
91 | //HIERARCHY HANDLER | ||
92 | |||
93 | |||
94 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates | ||
95 | // and store in a map | ||
96 | for (t1 : types.filter[!isIsAbstract]) { | ||
97 | for (t2 : types) { | ||
98 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes | ||
99 | if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { | ||
100 | // typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate))) | ||
101 | trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) | ||
102 | } else { | ||
103 | // typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | ||
104 | trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | ||
105 | it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) | ||
106 | ]) | ||
107 | } | ||
108 | } | ||
109 | // typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values))) | ||
110 | // typeTrace.type2PossibleNot.clear | ||
111 | trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values))) | ||
112 | trace.type2PossibleNot.clear | ||
113 | } | ||
114 | |||
115 | // 5. create fof function that is an or with all the elements in map | ||
116 | val hierarch = createVLSFofFormula => [ | ||
117 | it.name = "hierarchyHandler" | ||
118 | it.fofRole = "axiom" | ||
119 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
120 | it.variables += support.duplicate(variable) | ||
121 | it.operand = createVLSEquivalent => [ | ||
122 | it.left = support.topLevelTypeFunc | ||
123 | // it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values)) | ||
124 | it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values)) | ||
125 | ] | ||
126 | ] | ||
127 | ] | ||
128 | |||
129 | trace.specification.formulas += hierarch | ||
130 | |||
131 | } | ||
132 | |||
133 | //below are from previous interface | ||
134 | def protected transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, | ||
135 | Logic2VampireLanguageMapperTrace trace) { | ||
136 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
137 | } | ||
138 | |||
139 | def protected getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) { | ||
140 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
141 | } | ||
142 | |||
143 | def protected getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) { | ||
144 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
145 | } | ||
146 | |||
147 | def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { | ||
148 | createVLSDoubleQuote => [ | ||
149 | it.value = "\"a" + referred.name + "\"" | ||
150 | ] | ||
151 | } | ||
152 | |||
153 | def protected getTypeInterpreter() { | ||
154 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
155 | } | ||
156 | |||
157 | } | ||