diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-21 11:47:31 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-21 11:47:31 -0400 |
commit | b1af9114728270d243619bf9498d8cce6e0e0c64 (patch) | |
tree | e8fd1d72eebdf217778ccc1e675d76f41e40d983 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder | |
parent | Add gitignore, commit everything (diff) | |
download | VIATRA-Generator-b1af9114728270d243619bf9498d8cce6e0e0c64.tar.gz VIATRA-Generator-b1af9114728270d243619bf9498d8cce6e0e0c64.tar.zst VIATRA-Generator-b1af9114728270d243619bf9498d8cce6e0e0c64.zip |
Add to containment, add notObject case.
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder')
4 files changed, 154 insertions, 47 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index ff5a192e..820d0db2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend | |||
@@ -1,16 +1,19 @@ | |||
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 | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
7 | import java.util.List | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
12 | import java.util.HashMap | ||
13 | import java.util.List | ||
14 | import java.util.Map | ||
10 | 15 | ||
11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
14 | 17 | ||
15 | class Logic2VampireLanguageMapper_ContainmentMapper { | 18 | class Logic2VampireLanguageMapper_ContainmentMapper { |
16 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -74,54 +77,121 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
74 | // for each edge, if the pointedTo element exists,the edge must exist also | 77 | // for each edge, if the pointedTo element exists,the edge must exist also |
75 | val varA = createVLSVariable => [it.name = "A"] | 78 | val varA = createVLSVariable => [it.name = "A"] |
76 | val varB = createVLSVariable => [it.name = "B"] | 79 | val varB = createVLSVariable => [it.name = "B"] |
80 | val varC = createVLSVariable => [it.name = "C"] | ||
77 | val varList = newArrayList(varB, varA) | 81 | val varList = newArrayList(varB, varA) |
78 | 82 | val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap | |
79 | for (l : relationsList) { | 83 | for (l : relationsList) { |
80 | val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString | 84 | val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList) |
81 | val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type | 85 | // val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type |
82 | val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type | 86 | val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type) |
87 | val toFunc = toType.lookup(trace.type2Predicate) | ||
88 | |||
89 | addToMap(type2cont, toFunc, rel) | ||
83 | 90 | ||
84 | val listForAnd = newArrayList | 91 | for (c : toType.subtypes) { |
85 | // listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) | 92 | addToMap(type2cont, toFunc, rel) |
86 | listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)) | 93 | } |
94 | |||
95 | // val listForAnd = newArrayList | ||
96 | //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) | ||
97 | // listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)) | ||
87 | // listForAnd.add(createVLSInequality => [ | 98 | // listForAnd.add(createVLSInequality => [ |
88 | // it.left = support.duplicate(varA) | 99 | // it.left = support.duplicate(varA) |
89 | // it.right = support.duplicate(varB) | 100 | // it.right = support.duplicate(varB) |
90 | // ]) | 101 | // ]) |
102 | // remove subtypes of elements being pointed to | ||
103 | // var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type | ||
104 | // containmentListCopy.remove(pointingTo) | ||
105 | // for (c : pointingTo.subtypes) { | ||
106 | // containmentListCopy.remove(c) | ||
107 | // } | ||
108 | // STEP 3 | ||
109 | // Ensure that an objct only has 1 parent | ||
110 | val relFormula = createVLSFofFormula => [ | ||
111 | it.name = support.toIDMultiple("noDupCont", rel.constant.toString) | ||
112 | it.fofRole = "axiom" | ||
113 | it.fofFormula = createVLSExistentialQuantifier => [ | ||
114 | it.variables += support.duplicate(varA) | ||
115 | it.variables += support.duplicate(varB) | ||
116 | it.operand = createVLSImplies => [ | ||
117 | it.left = support.duplicate(rel, newArrayList(varA, varB)) | ||
118 | it.right = createVLSUnaryNegation => [ | ||
119 | it.operand = createVLSExistentialQuantifier => [ | ||
120 | it.variables += support.duplicate(varC) | ||
121 | it.variables += support.duplicate(varB) | ||
122 | it.operand = support.duplicate(rel, newArrayList(varC, varB)) | ||
123 | |||
124 | ] | ||
125 | ] | ||
126 | ] | ||
127 | ] | ||
128 | ] | ||
129 | trace.specification.formulas += relFormula | ||
91 | 130 | ||
131 | } | ||
132 | |||
133 | // STEP CONT'D | ||
134 | for (e : type2cont.entrySet) { | ||
92 | val relFormula = createVLSFofFormula => [ | 135 | val relFormula = createVLSFofFormula => [ |
93 | it.name = support.toIDMultiple("containment", relName) | 136 | it.name = support.toIDMultiple("containment", e.key.constant.toString) |
94 | it.fofRole = "axiom" | 137 | it.fofRole = "axiom" |
95 | 138 | ||
96 | it.fofFormula = createVLSUniversalQuantifier => [ | 139 | it.fofFormula = createVLSUniversalQuantifier => [ |
97 | it.variables += support.duplicate(varA) | 140 | it.variables += support.duplicate(varA) |
98 | it.operand = createVLSImplies => [ | 141 | it.operand = createVLSImplies => [ |
99 | it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA) | 142 | it.left = support.duplicate(e.key, varA) |
100 | it.right = createVLSExistentialQuantifier => [ | 143 | it.right = createVLSExistentialQuantifier => [ |
101 | it.variables += support.duplicate(varB) | 144 | it.variables += support.duplicate(varB) |
102 | it.operand = support.unfoldAnd(listForAnd) | 145 | if (e.value.length > 1) { |
103 | ] | 146 | it.operand = makeUnique(e.value) |
147 | } else { | ||
148 | it.operand = e.value.get(0) | ||
149 | } | ||
104 | 150 | ||
105 | createVLSEquality => [ | ||
106 | it.left = support.duplicate(variable) | ||
107 | it.right = createVLSConstant => [ | ||
108 | it.name = "o1" | ||
109 | ] | ||
110 | ] | 151 | ] |
111 | ] | 152 | ] |
112 | ] | 153 | ] |
113 | ] | 154 | ] |
114 | trace.specification.formulas += relFormula | 155 | trace.specification.formulas += relFormula |
115 | var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type | 156 | |
116 | containmentListCopy.remove(pointingTo) | ||
117 | for (c : pointingTo.subtypes) { | ||
118 | containmentListCopy.remove(c) | ||
119 | } | ||
120 | } | 157 | } |
121 | 158 | ||
122 | // STEP 3 | ||
123 | // Ensure that an objct only has 1 parent | ||
124 | // STEP 4 | 159 | // STEP 4 |
125 | // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) | 160 | // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) |
126 | } | 161 | } |
162 | |||
163 | protected def VLSTerm makeUnique(List<VLSFunction> list) { | ||
164 | val List<VLSTerm> possibleNots = newArrayList | ||
165 | val List<VLSTerm> uniqueRels = newArrayList | ||
166 | |||
167 | for (t1 : list) { | ||
168 | for (t2 : list) { | ||
169 | if (t1 == t2) { | ||
170 | val fct = support.duplicate(t2) | ||
171 | possibleNots.add(fct) | ||
172 | } else { | ||
173 | val op = support.duplicate(t2) | ||
174 | val negFct = createVLSUnaryNegation => [ | ||
175 | it.operand = op | ||
176 | ] | ||
177 | possibleNots.add(negFct) | ||
178 | } | ||
179 | } | ||
180 | uniqueRels.add(support.unfoldAnd(possibleNots)) | ||
181 | possibleNots.clear | ||
182 | } | ||
183 | return support.unfoldOr(uniqueRels) | ||
184 | } | ||
185 | |||
186 | protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) { | ||
187 | if (!type2cont.containsKey(toFunc)) { | ||
188 | type2cont.put(toFunc, newArrayList(rel)) | ||
189 | } else { | ||
190 | if (!type2cont.get(toFunc).contains(rel)) { | ||
191 | type2cont.get(toFunc).add(rel) | ||
192 | // type2cont.replace(toFunc, newArrayList(firstRel)) | ||
193 | } | ||
194 | |||
195 | } | ||
196 | } | ||
127 | } | 197 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index 548deda4..bc87d3b7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend | |||
@@ -38,10 +38,10 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
38 | // Handling Minimum_General | 38 | // Handling Minimum_General |
39 | if (GLOBAL_MIN != 0) { | 39 | if (GLOBAL_MIN != 0) { |
40 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) | 40 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) |
41 | for(i : trace.uniqueInstances){ | 41 | for (i : trace.uniqueInstances) { |
42 | localInstances.add(support.duplicate(i)) | 42 | localInstances.add(support.duplicate(i)) |
43 | } | 43 | } |
44 | 44 | ||
45 | makeFofFormula(localInstances, trace, true, null) | 45 | makeFofFormula(localInstances, trace, true, null) |
46 | } | 46 | } |
47 | 47 | ||
@@ -83,14 +83,15 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
83 | 83 | ||
84 | // 3. Specify uniqueness of elements | 84 | // 3. Specify uniqueness of elements |
85 | if (trace.uniqueInstances.length != 0) { | 85 | if (trace.uniqueInstances.length != 0) { |
86 | val uniqueness = createVLSFofFormula => [ | 86 | for (e : trace.uniqueInstances) { |
87 | it.name = "typeUniqueness" | 87 | val uniqueness = createVLSFofFormula => [ |
88 | it.fofRole = "axiom" | 88 | it.name = support.toIDMultiple("t_uniqueness", e.name) |
89 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances) | 89 | it.fofRole = "axiom" |
90 | ] | 90 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) |
91 | trace.specification.formulas += uniqueness | 91 | ] |
92 | trace.specification.formulas += uniqueness | ||
93 | } | ||
92 | } | 94 | } |
93 | |||
94 | } | 95 | } |
95 | 96 | ||
96 | def protected void getInstanceConstants(int endInd, int startInd, ArrayList list, | 97 | def protected void getInstanceConstants(int endInd, int startInd, ArrayList list, |
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 8d00d3e7..d1ea2a15 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 | |||
@@ -92,7 +92,7 @@ class Logic2VampireLanguageMapper_Support { | |||
92 | ] | 92 | ] |
93 | ] | 93 | ] |
94 | } | 94 | } |
95 | 95 | ||
96 | def protected VLSFunction topLevelTypeFunc(VLSVariable v) { | 96 | def protected VLSFunction topLevelTypeFunc(VLSVariable v) { |
97 | return createVLSFunction => [ | 97 | return createVLSFunction => [ |
98 | it.constant = "object" | 98 | it.constant = "object" |
@@ -108,15 +108,26 @@ class Logic2VampireLanguageMapper_Support { | |||
108 | } | 108 | } |
109 | 109 | ||
110 | // TODO Make more general | 110 | // TODO Make more general |
111 | def establishUniqueness(List<VLSConstant> terms) { | 111 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { |
112 | // val List<VLSInequality> eqs = newArrayList | ||
113 | // for (t1 : terms.subList(1, terms.length)) { | ||
114 | // for (t2 : terms.subList(0, terms.indexOf(t1))) { | ||
115 | // val eq = createVLSInequality => [ | ||
116 | // // TEMP | ||
117 | // it.left = createVLSConstant => [it.name = t2.name] | ||
118 | // it.right = createVLSConstant => [it.name = t1.name] | ||
119 | // // TEMP | ||
120 | // ] | ||
121 | // eqs.add(eq) | ||
122 | // } | ||
123 | // } | ||
124 | // return unfoldAnd(eqs) | ||
112 | val List<VLSInequality> eqs = newArrayList | 125 | val List<VLSInequality> eqs = newArrayList |
113 | for (t1 : terms.subList(1, terms.length)) { | 126 | for (t1 : terms) { |
114 | for (t2 : terms.subList(0, terms.indexOf(t1))) { | 127 | if (t1 != t2) { |
115 | val eq = createVLSInequality => [ | 128 | val eq = createVLSInequality => [ |
116 | // TEMP | ||
117 | it.left = createVLSConstant => [it.name = t2.name] | 129 | it.left = createVLSConstant => [it.name = t2.name] |
118 | it.right = createVLSConstant => [it.name = t1.name] | 130 | it.right = createVLSConstant => [it.name = t1.name] |
119 | // TEMP | ||
120 | ] | 131 | ] |
121 | eqs.add(eq) | 132 | eqs.add(eq) |
122 | } | 133 | } |
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 4c4247ce..1719bbcc 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 | |||
@@ -91,13 +91,12 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
91 | it.right = support.unfoldOr(typeDefs) | 91 | it.right = support.unfoldOr(typeDefs) |
92 | ] | 92 | ] |
93 | // it.right = support.unfoldOr((typeDefs)) | 93 | // it.right = support.unfoldOr((typeDefs)) |
94 | |||
95 | ] | 94 | ] |
96 | ] | 95 | ] |
97 | ] | 96 | ] |
98 | trace.specification.formulas += res | 97 | trace.specification.formulas += res |
99 | 98 | ||
100 | for (var i = globalCounter; i < globalCounter+type.elements.length; i++) { | 99 | for (var i = globalCounter; i < globalCounter + type.elements.length; i++) { |
101 | // Create objects for the enum elements | 100 | // Create objects for the enum elements |
102 | val num = i + 1 | 101 | val num = i + 1 |
103 | val cstTerm = createVLSFunctionAsTerm => [ | 102 | val cstTerm = createVLSFunctionAsTerm => [ |
@@ -127,7 +126,7 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
127 | trace.specification.formulas += enumScope | 126 | trace.specification.formulas += enumScope |
128 | 127 | ||
129 | } | 128 | } |
130 | globalCounter+=type.elements.size | 129 | globalCounter += type.elements.size |
131 | } | 130 | } |
132 | 131 | ||
133 | // HIERARCHY HANDLER | 132 | // HIERARCHY HANDLER |
@@ -148,9 +147,35 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
148 | // typeTrace.type2PossibleNot.clear | 147 | // typeTrace.type2PossibleNot.clear |
149 | trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values))) | 148 | trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values))) |
150 | trace.type2PossibleNot.clear | 149 | trace.type2PossibleNot.clear |
150 | |||
151 | } | ||
152 | |||
153 | // 4. case where an object is not an object | ||
154 | val List<VLSTerm> type2Not = newArrayList | ||
155 | |||
156 | for(t : types) { | ||
157 | type2Not.add(createVLSUnaryNegation => [ | ||
158 | it.operand = support.duplicate(t.lookup(trace.type2Predicate)) | ||
159 | ]) | ||
151 | } | 160 | } |
152 | 161 | ||
153 | // 5. create fof function that is an or with all the elements in map | 162 | val notObj = createVLSFofFormula => [ |
163 | it.name = "notObjectHandler" | ||
164 | it.fofRole = "axiom" | ||
165 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
166 | it.variables += support.duplicate(variable) | ||
167 | it.operand = createVLSEquivalent => [ | ||
168 | it.left = createVLSUnaryNegation => [ | ||
169 | it.operand = support.topLevelTypeFunc | ||
170 | ] | ||
171 | it.right = support.unfoldAnd(type2Not) | ||
172 | ] | ||
173 | ] | ||
174 | ] | ||
175 | |||
176 | trace.specification.formulas += notObj | ||
177 | |||
178 | // 4. create fof function that is an or with all the elements in map | ||
154 | val hierarch = createVLSFofFormula => [ | 179 | val hierarch = createVLSFofFormula => [ |
155 | it.name = "inheritanceHierarchyHandler" | 180 | it.name = "inheritanceHierarchyHandler" |
156 | it.fofRole = "axiom" | 181 | it.fofRole = "axiom" |