diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-04 14:43:17 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:36:03 -0400 |
commit | 844c46e8a3620c7fae26f87e148643b32480dced (patch) | |
tree | 9252d89ef05bd9f4e5aafc9575155ebb3ee59211 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill | |
parent | Add to containment, add notObject case. (diff) | |
download | VIATRA-Generator-844c46e8a3620c7fae26f87e148643b32480dced.tar.gz VIATRA-Generator-844c46e8a3620c7fae26f87e148643b32480dced.tar.zst VIATRA-Generator-844c46e8a3620c7fae26f87e148643b32480dced.zip |
Closes #34, adds code to test cases where minScope>maxScope.
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill')
4 files changed, 60 insertions, 19 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 820d0db2..48ee8789 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 | |||
@@ -27,7 +27,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
27 | 27 | ||
28 | def public void transformContainment(List<ContainmentHierarchy> hierarchies, | 28 | def public void transformContainment(List<ContainmentHierarchy> hierarchies, |
29 | Logic2VampireLanguageMapperTrace trace) { | 29 | Logic2VampireLanguageMapperTrace trace) { |
30 | 30 | //TODO throw error is there exists a circular containment that does not involve hierarchy | |
31 | // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST | 31 | // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST |
32 | // TEMP | 32 | // TEMP |
33 | val hierarchy = hierarchies.get(0) | 33 | val hierarchy = hierarchies.get(0) |
@@ -91,6 +91,9 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
91 | for (c : toType.subtypes) { | 91 | for (c : toType.subtypes) { |
92 | addToMap(type2cont, toFunc, rel) | 92 | addToMap(type2cont, toFunc, rel) |
93 | } | 93 | } |
94 | // for (c : support.listSubtypes(toType)) { | ||
95 | // addToMap(type2cont, toFunc, rel) | ||
96 | // } | ||
94 | 97 | ||
95 | // val listForAnd = newArrayList | 98 | // val listForAnd = newArrayList |
96 | //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) | 99 | //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) |
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 bc87d3b7..54fcdc86 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 | |||
@@ -24,11 +24,12 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
24 | } | 24 | } |
25 | 25 | ||
26 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { | 26 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { |
27 | val ABSOLUTE_MIN = 0 | ||
28 | val ABSOLUTE_MAX = Integer.MAX_VALUE | ||
27 | 29 | ||
28 | // TODO HANDLE ERRORS RELATED TO MAX > MIN | 30 | // TODO HANDLE ERRORS RELATED TO MAX > MIN |
29 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS | 31 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS |
30 | // TODO HANDLE | 32 | // TODO HANDLE |
31 | // TODO NOT SPECIFIED MEANS =0 ? | ||
32 | // 1. make a list of constants equaling the min number of specified objects | 33 | // 1. make a list of constants equaling the min number of specified objects |
33 | val GLOBAL_MIN = config.typeScopes.minNewElements | 34 | val GLOBAL_MIN = config.typeScopes.minNewElements |
34 | val GLOBAL_MAX = config.typeScopes.maxNewElements | 35 | val GLOBAL_MAX = config.typeScopes.maxNewElements |
@@ -36,19 +37,30 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
36 | val localInstances = newArrayList | 37 | val localInstances = newArrayList |
37 | 38 | ||
38 | // Handling Minimum_General | 39 | // Handling Minimum_General |
39 | if (GLOBAL_MIN != 0) { | 40 | if (GLOBAL_MIN != ABSOLUTE_MIN) { |
40 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) | 41 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) |
41 | for (i : trace.uniqueInstances) { | 42 | for (i : trace.uniqueInstances) { |
42 | localInstances.add(support.duplicate(i)) | 43 | localInstances.add(support.duplicate(i)) |
43 | } | 44 | } |
44 | 45 | ||
45 | makeFofFormula(localInstances, trace, true, null) | 46 | makeFofFormula(localInstances, trace, true, null) |
47 | |||
48 | // //For testing Min>Max scope | ||
49 | // getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, true) | ||
50 | // makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null) | ||
51 | // //end for testing | ||
52 | |||
46 | } | 53 | } |
47 | 54 | ||
48 | // Handling Maximum_General | 55 | // Handling Maximum_General |
49 | if (GLOBAL_MAX != 0) { | 56 | if (GLOBAL_MAX != ABSOLUTE_MAX) { |
50 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) | 57 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) |
51 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) | 58 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) |
59 | |||
60 | // //For testing Min>Max scope | ||
61 | // getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, false) | ||
62 | // makeFofFormula(localInstances, trace, false, null) | ||
63 | // //end for testing | ||
52 | } | 64 | } |
53 | 65 | ||
54 | // Handling Minimum_Specific | 66 | // Handling Minimum_Specific |
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 d1ea2a15..b00dad42 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 | |||
@@ -23,7 +23,7 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
23 | class Logic2VampireLanguageMapper_Support { | 23 | class Logic2VampireLanguageMapper_Support { |
24 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 24 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
25 | 25 | ||
26 | // ID Handler | 26 | // ID Handler |
27 | def protected String toIDMultiple(String... ids) { | 27 | def protected String toIDMultiple(String... ids) { |
28 | ids.map[it.split("\\s+").join("_")].join("_") | 28 | ids.map[it.split("\\s+").join("_")].join("_") |
29 | } | 29 | } |
@@ -32,8 +32,8 @@ class Logic2VampireLanguageMapper_Support { | |||
32 | ids.split("\\s+").join("_") | 32 | ids.split("\\s+").join("_") |
33 | } | 33 | } |
34 | 34 | ||
35 | // Term Handling | 35 | // Term Handling |
36 | // TODO Make more general | 36 | // TODO Make more general |
37 | def protected VLSVariable duplicate(VLSVariable term) { | 37 | def protected VLSVariable duplicate(VLSVariable term) { |
38 | return createVLSVariable => [it.name = term.name] | 38 | return createVLSVariable => [it.name = term.name] |
39 | } | 39 | } |
@@ -107,7 +107,7 @@ class Logic2VampireLanguageMapper_Support { | |||
107 | ] | 107 | ] |
108 | } | 108 | } |
109 | 109 | ||
110 | // TODO Make more general | 110 | // TODO Make more general |
111 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { | 111 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { |
112 | // val List<VLSInequality> eqs = newArrayList | 112 | // val List<VLSInequality> eqs = newArrayList |
113 | // for (t1 : terms.subList(1, terms.length)) { | 113 | // for (t1 : terms.subList(1, terms.length)) { |
@@ -135,9 +135,9 @@ class Logic2VampireLanguageMapper_Support { | |||
135 | return unfoldAnd(eqs) | 135 | return unfoldAnd(eqs) |
136 | } | 136 | } |
137 | 137 | ||
138 | // Support Functions | 138 | // Support Functions |
139 | // booleans | 139 | // booleans |
140 | // AND and OR | 140 | // AND and OR |
141 | def protected VLSTerm unfoldAnd(List<? extends VLSTerm> operands) { | 141 | def protected VLSTerm unfoldAnd(List<? extends VLSTerm> operands) { |
142 | if (operands.size == 1) { | 142 | if (operands.size == 1) { |
143 | return operands.head | 143 | return operands.head |
@@ -163,7 +163,7 @@ class Logic2VampireLanguageMapper_Support { | |||
163 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP | 163 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP |
164 | } | 164 | } |
165 | 165 | ||
166 | // can delete below | 166 | // can delete below |
167 | def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands, | 167 | def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands, |
168 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | 168 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { |
169 | if (operands.size == 1) { | 169 | if (operands.size == 1) { |
@@ -183,8 +183,8 @@ class Logic2VampireLanguageMapper_Support { | |||
183 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') | 183 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') |
184 | } | 184 | } |
185 | 185 | ||
186 | // Symbolic | 186 | // Symbolic |
187 | // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) { | 187 | // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) { |
188 | // if(type instanceof BoolTypeReference) { | 188 | // if(type instanceof BoolTypeReference) { |
189 | // return booleanToLogicValue(term ,trace) | 189 | // return booleanToLogicValue(term ,trace) |
190 | // } | 190 | // } |
@@ -198,7 +198,7 @@ class Logic2VampireLanguageMapper_Support { | |||
198 | * ids.map[it.split("\\s+").join("'")].join("'") | 198 | * ids.map[it.split("\\s+").join("'")].join("'") |
199 | * } | 199 | * } |
200 | */ | 200 | */ |
201 | // QUANTIFIERS + VARIABLES | 201 | // QUANTIFIERS + VARIABLES |
202 | def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, | 202 | def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, |
203 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables, | 203 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables, |
204 | boolean isUniversal) { | 204 | boolean isUniversal) { |
@@ -245,6 +245,32 @@ class Logic2VampireLanguageMapper_Support { | |||
245 | } | 245 | } |
246 | } | 246 | } |
247 | } | 247 | } |
248 | //TODO rewrite such that it uses "listSubTypes" | ||
249 | def protected boolean dfsSubtypeCheck(Type type, Type type2) { | ||
250 | // There is surely a better way to do this | ||
251 | if (type.subtypes.isEmpty) | ||
252 | return false | ||
253 | else { | ||
254 | if (type.subtypes.contains(type2)) | ||
255 | return true | ||
256 | else { | ||
257 | for (subtype : type.subtypes) { | ||
258 | if(dfsSubtypeCheck(subtype, type2)) return true | ||
259 | } | ||
260 | } | ||
261 | } | ||
262 | } | ||
263 | |||
264 | def protected List<Type> listSubtypes(Type t) { | ||
265 | var List<Type> allSubtypes = newArrayList | ||
266 | if (!t.subtypes.isEmpty) { | ||
267 | for (subt : t.subtypes) { | ||
268 | allSubtypes.add(subt) | ||
269 | allSubtypes = listSubtypes(subt) | ||
270 | } | ||
271 | } | ||
272 | return allSubtypes | ||
273 | } | ||
248 | 274 | ||
249 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | 275 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { |
250 | new HashMap(map1) => [putAll(map2)] | 276 | new HashMap(map1) => [putAll(map2)] |
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 1719bbcc..3bc945df 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 | |||
@@ -150,10 +150,10 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
150 | 150 | ||
151 | } | 151 | } |
152 | 152 | ||
153 | // 4. case where an object is not an object | 153 | // 3.5: case where an object is not an object |
154 | val List<VLSTerm> type2Not = newArrayList | 154 | val List<VLSTerm> type2Not = newArrayList |
155 | 155 | ||
156 | for(t : types) { | 156 | for (t : types) { |
157 | type2Not.add(createVLSUnaryNegation => [ | 157 | type2Not.add(createVLSUnaryNegation => [ |
158 | it.operand = support.duplicate(t.lookup(trace.type2Predicate)) | 158 | it.operand = support.duplicate(t.lookup(trace.type2Predicate)) |
159 | ]) | 159 | ]) |
@@ -174,7 +174,7 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
174 | ] | 174 | ] |
175 | 175 | ||
176 | trace.specification.formulas += notObj | 176 | trace.specification.formulas += notObj |
177 | 177 | // End 3.5 | |
178 | // 4. create fof function that is an or with all the elements in map | 178 | // 4. create fof function that is an or with all the elements in map |
179 | val hierarch = createVLSFofFormula => [ | 179 | val hierarch = createVLSFofFormula => [ |
180 | it.name = "inheritanceHierarchyHandler" | 180 | it.name = "inheritanceHierarchyHandler" |