diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-14 03:45:46 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:22:51 -0400 |
commit | d7730cb0d684d6324622021a310d9b4a53e7531c (patch) | |
tree | b631b8c666448b948bdf670fbf5ad7c2277496dd /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | |
parent | Implement type scope for specific types (diff) | |
download | VIATRA-Generator-d7730cb0d684d6324622021a310d9b4a53e7531c.tar.gz VIATRA-Generator-d7730cb0d684d6324622021a310d9b4a53e7531c.tar.zst VIATRA-Generator-d7730cb0d684d6324622021a310d9b4a53e7531c.zip |
Implement Containment mapping (partially) and revisit enum mapping
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 | 104 |
1 files changed, 58 insertions, 46 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 e12180fa..4c4247ce 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,12 +1,12 @@ | |||
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 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 9 | 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 | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
12 | import java.util.ArrayList | 12 | import java.util.ArrayList |
@@ -14,7 +14,6 @@ import java.util.Collection | |||
14 | import java.util.List | 14 | import java.util.List |
15 | 15 | ||
16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
17 | import java.util.Collections | ||
18 | 17 | ||
19 | class Logic2VampireLanguageMapper_TypeMapper { | 18 | class Logic2VampireLanguageMapper_TypeMapper { |
20 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -28,10 +27,8 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
28 | 27 | ||
29 | def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, | 28 | def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, |
30 | Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { | 29 | Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { |
31 | |||
32 | // val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes | ||
33 | // trace.typeMapperTrace = typeTrace | ||
34 | val VLSVariable variable = createVLSVariable => [it.name = "A"] | 30 | val VLSVariable variable = createVLSVariable => [it.name = "A"] |
31 | var globalCounter = 0 | ||
35 | 32 | ||
36 | // 1. Each type (class) is a predicate with a single variable as input | 33 | // 1. Each type (class) is a predicate with a single variable as input |
37 | for (type : types) { | 34 | for (type : types) { |
@@ -39,94 +36,109 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
39 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) | 36 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) |
40 | it.terms += support.duplicate(variable) | 37 | it.terms += support.duplicate(variable) |
41 | ] | 38 | ] |
42 | // typeTrace.type2Predicate.put(type, typePred) | ||
43 | trace.type2Predicate.put(type, typePred) | 39 | trace.type2Predicate.put(type, typePred) |
44 | } | 40 | } |
45 | 41 | ||
46 | // 2. Map each ENUM type definition to fof formula | 42 | // 2. Map each ENUM type definition to fof formula |
47 | for (type : types.filter(TypeDefinition)) { | 43 | for (type : types.filter(TypeDefinition)) { |
44 | |||
45 | // Create a VLSFunction for each Enum Element | ||
48 | val List<VLSFunction> orElems = newArrayList | 46 | val List<VLSFunction> orElems = newArrayList |
49 | for (e : type.elements) { | 47 | for (e : type.elements) { |
50 | val enumElemPred = createVLSFunction => [ | 48 | val enumElemPred = createVLSFunction => [ |
51 | val splitName = e.name.split(" ") | 49 | val splitName = e.name.split(" ") |
52 | if( splitName.length > 2) { | 50 | if (splitName.length > 2) { |
53 | it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) | 51 | it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) |
54 | } | 52 | } else { |
55 | else { | ||
56 | it.constant = support.toIDMultiple("e", splitName.get(0)) | 53 | it.constant = support.toIDMultiple("e", splitName.get(0)) |
57 | } | 54 | } |
58 | it.terms += support.duplicate(variable) | 55 | it.terms += support.duplicate(variable) |
59 | ] | 56 | ] |
60 | // typeTrace.element2Predicate.put(e, enumElemPred) | ||
61 | trace.element2Predicate.put(e, enumElemPred) | 57 | trace.element2Predicate.put(e, enumElemPred) |
62 | orElems.add(enumElemPred) | ||
63 | } | 58 | } |
64 | 59 | ||
60 | // Similar to InheritanceHierarchy for the Enum | ||
61 | val List<VLSTerm> possibleNots = newArrayList | ||
62 | val List<VLSTerm> typeDefs = newArrayList | ||
63 | |||
64 | for (t1 : type.elements) { | ||
65 | for (t2 : type.elements) { | ||
66 | if (t1 == t2) { | ||
67 | val fct = support.duplicate(t2.lookup(trace.element2Predicate), variable) | ||
68 | possibleNots.add(fct) | ||
69 | } else { | ||
70 | val op = support.duplicate(t2.lookup(trace.element2Predicate), variable) | ||
71 | val negFct = createVLSUnaryNegation => [ | ||
72 | it.operand = op | ||
73 | ] | ||
74 | possibleNots.add(negFct) | ||
75 | } | ||
76 | } | ||
77 | typeDefs.add(support.unfoldAnd(possibleNots)) | ||
78 | possibleNots.clear | ||
79 | } | ||
80 | |||
81 | // Implement Enum Inheritence Hierarchy | ||
65 | val res = createVLSFofFormula => [ | 82 | val res = createVLSFofFormula => [ |
66 | it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) | 83 | it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) |
67 | // below is temporary solution | ||
68 | it.fofRole = "axiom" | 84 | it.fofRole = "axiom" |
69 | it.fofFormula = createVLSUniversalQuantifier => [ | 85 | it.fofFormula = createVLSUniversalQuantifier => [ |
70 | it.variables += support.duplicate(variable) | 86 | it.variables += support.duplicate(variable) |
71 | it.operand = createVLSEquivalent => [ | 87 | it.operand = createVLSEquivalent => [ |
72 | it.left = type.lookup(trace.type2Predicate) | 88 | it.left = type.lookup(trace.type2Predicate) |
73 | it.right = support.unfoldOr(orElems) | 89 | it.right = createVLSAnd => [ |
90 | it.left = support.topLevelTypeFunc(variable) | ||
91 | it.right = support.unfoldOr(typeDefs) | ||
92 | ] | ||
93 | // it.right = support.unfoldOr((typeDefs)) | ||
94 | |||
74 | ] | 95 | ] |
75 | ] | 96 | ] |
76 | |||
77 | ] | 97 | ] |
78 | trace.specification.formulas += res | 98 | trace.specification.formulas += res |
79 | 99 | ||
80 | // Create objects for the enum elements | 100 | for (var i = globalCounter; i < globalCounter+type.elements.length; i++) { |
81 | val List<VLSTerm> enumScopeElems = newArrayList | 101 | // Create objects for the enum elements |
82 | for (var i = 0; i < type.elements.length; i++) { | ||
83 | val num = i + 1 | 102 | val num = i + 1 |
84 | val cstTerm = createVLSFunctionAsTerm => [ | 103 | val cstTerm = createVLSFunctionAsTerm => [ |
85 | it.functor = "eo" + num | 104 | it.functor = "eo" + num |
86 | ] | 105 | ] |
87 | val cst = support.toConstant(cstTerm) | 106 | val cst = support.toConstant(cstTerm) |
88 | trace.uniqueInstances.add(cst) | 107 | trace.uniqueInstances.add(cst) |
89 | val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm) | 108 | |
90 | enumScopeElems.add(fct) | 109 | val index = i |
91 | 110 | val enumScope = createVLSFofFormula => [ | |
92 | //For paradox Only | 111 | it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0), |
93 | for (var j = 0; j < type.elements.length; j++) { | 112 | type.elements.get(index).name.split(" ").get(0)) |
94 | if(j != i) { | 113 | it.fofRole = "axiom" |
95 | val op = support.duplicate(type.elements.get(j).lookup(trace.element2Predicate), cstTerm) | 114 | it.fofFormula = createVLSUniversalQuantifier => [ |
96 | val negFct = createVLSUnaryNegation => [ | 115 | it.variables += support.duplicate(variable) |
97 | it.operand = op | 116 | it.operand = createVLSEquivalent => [ |
117 | it.left = createVLSEquality => [ | ||
118 | it.left = support.duplicate(variable) | ||
119 | it.right = support.duplicate(support.toConstant(cstTerm)) | ||
120 | ] | ||
121 | it.right = support.duplicate(type.elements.get(index).lookup(trace.element2Predicate), | ||
122 | variable) | ||
98 | ] | 123 | ] |
99 | enumScopeElems.add(negFct) | 124 | ] |
100 | } | 125 | ] |
101 | } | 126 | |
102 | //End Paradox | 127 | trace.specification.formulas += enumScope |
103 | // enumScopeElems.add(support.topLevelTypeFunc(cstTerm)) | 128 | |
104 | } | 129 | } |
105 | 130 | globalCounter+=type.elements.size | |
106 | |||
107 | |||
108 | val enumScope = createVLSFofFormula => [ | ||
109 | it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0)) | ||
110 | // below is temporary solution | ||
111 | it.fofRole = "axiom" | ||
112 | it.fofFormula = support.unfoldAnd(enumScopeElems) | ||
113 | ] | ||
114 | |||
115 | trace.specification.formulas += enumScope | ||
116 | } | 131 | } |
117 | 132 | ||
118 | // HIERARCHY HANDLER | 133 | // HIERARCHY HANDLER |
119 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates | 134 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates |
120 | // and store in a map | 135 | // and store in a map |
121 | // println(types.filter[!isIsAbstract]) | 136 | for (t1 : types.filter[!isIsAbstract]) { |
122 | for (t1 : types.filter[!isIsAbstract].filter(TypeDeclaration)) { | ||
123 | for (t2 : types) { | 137 | for (t2 : types) { |
124 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes | 138 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes |
125 | if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { | 139 | if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { |
126 | // typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate))) | ||
127 | trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) | 140 | trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) |
128 | } else { | 141 | } else { |
129 | // typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | ||
130 | trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | 142 | trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ |
131 | it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) | 143 | it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) |
132 | ]) | 144 | ]) |