diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-25 02:50:40 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:37:07 -0400 |
commit | 598daf4605d97466d07c74b1bc76d165be145288 (patch) | |
tree | 3756188257ae023e0cdf22b840ea4ce5dfa95505 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner | |
parent | VAMPIRE : initial model handling almost done. only typeScope remains #40 (diff) | |
download | VIATRA-Generator-598daf4605d97466d07c74b1bc76d165be145288.tar.gz VIATRA-Generator-598daf4605d97466d07c74b1bc76d165be145288.tar.zst VIATRA-Generator-598daf4605d97466d07c74b1bc76d165be145288.zip |
VAMPIRE: fixed MANY bugs in containment and scope. #40 is good for now
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner')
15 files changed, 185 insertions, 95 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 e0089c41..e94584ae 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 | |||
@@ -32,6 +32,7 @@ class Logic2VampireLanguageMapperTrace { | |||
32 | 32 | ||
33 | public var Map<DefinedElement, String> definedElement2String = new HashMap | 33 | public var Map<DefinedElement, String> definedElement2String = new HashMap |
34 | public var topLvlElementIsInInitialModel = null | 34 | public var topLvlElementIsInInitialModel = null |
35 | public var topLevelType = null | ||
35 | 36 | ||
36 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; | 37 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; |
37 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap | 38 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap |
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 9f29ea49..93c28e7c 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 | |||
@@ -70,6 +70,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
70 | 70 | ||
71 | val topName = topTermVar.lookup(trace.type2Predicate).constant.toString | 71 | val topName = topTermVar.lookup(trace.type2Predicate).constant.toString |
72 | val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate)) | 72 | val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate)) |
73 | trace.topLevelType = topTermVar | ||
73 | 74 | ||
74 | var topLvlIsInInitModel = false | 75 | var topLvlIsInInitModel = false |
75 | var topLvlString = "" | 76 | var topLvlString = "" |
@@ -129,16 +130,22 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
129 | val varList = newArrayList(varB, varA) | 130 | val varList = newArrayList(varB, varA) |
130 | val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap | 131 | val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap |
131 | for (l : relationsList) { | 132 | for (l : relationsList) { |
132 | val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList) | 133 | val rel = (l as RelationDeclaration).lookup(trace.rel2Predicate) |
133 | // val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type | 134 | // val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type |
134 | val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type) | 135 | val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type) |
135 | val toFunc = toType.lookup(trace.type2Predicate) | 136 | val toFunc = toType.lookup(trace.type2Predicate) |
136 | 137 | ||
137 | addToMap(type2cont, toFunc, rel) | 138 | addToMap(type2cont, support.duplicate(toFunc), support.duplicate(rel, varList)) |
138 | 139 | ||
139 | for (c : toType.subtypes) { | 140 | var subTypes = newArrayList |
140 | addToMap(type2cont, toFunc, rel) | 141 | support.listSubtypes(toType, subTypes) |
142 | for (c : subTypes) { | ||
143 | addToMap(type2cont, support.duplicate(c.lookup(trace.type2Predicate)), support.duplicate(rel, varList)) | ||
141 | } | 144 | } |
145 | |||
146 | |||
147 | |||
148 | |||
142 | // for (c : support.listSubtypes(toType)) { | 149 | // for (c : support.listSubtypes(toType)) { |
143 | // addToMap(type2cont, toFunc, rel) | 150 | // addToMap(type2cont, toFunc, rel) |
144 | // } | 151 | // } |
@@ -182,6 +189,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
182 | 189 | ||
183 | // STEP 2 CONT'D | 190 | // STEP 2 CONT'D |
184 | for (e : type2cont.entrySet) { | 191 | for (e : type2cont.entrySet) { |
192 | println(e.key + " " + e.value) | ||
185 | val relFormula = createVLSFofFormula => [ | 193 | val relFormula = createVLSFofFormula => [ |
186 | it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) | 194 | it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) |
187 | it.fofRole = "axiom" | 195 | it.fofRole = "axiom" |
@@ -192,6 +200,11 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
192 | it.left = support.duplicate(e.key, varA) | 200 | it.left = support.duplicate(e.key, varA) |
193 | it.right = createVLSExistentialQuantifier => [ | 201 | it.right = createVLSExistentialQuantifier => [ |
194 | it.variables += support.duplicate(varB) | 202 | it.variables += support.duplicate(varB) |
203 | // for ( x : type2cont.entrySet) { | ||
204 | // if (support.dfsSupertypeCheck(e.key, x.key)) { | ||
205 | // e.value.addAll(x.value) | ||
206 | // } | ||
207 | // } | ||
195 | if (e.value.length > 1) { | 208 | if (e.value.length > 1) { |
196 | it.operand = makeUnique(e.value) | 209 | it.operand = makeUnique(e.value) |
197 | } else { | 210 | } else { |
@@ -264,11 +277,20 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
264 | } | 277 | } |
265 | 278 | ||
266 | protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) { | 279 | protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) { |
267 | if (!type2cont.containsKey(toFunc)) { | 280 | var keyInMap = false |
281 | var existingKey = createVLSFunction | ||
282 | for (k : type2cont.keySet) { | ||
283 | if (k.constant.equals(toFunc.constant)) { | ||
284 | keyInMap = true | ||
285 | existingKey = k | ||
286 | } | ||
287 | } | ||
288 | |||
289 | if (!keyInMap) { | ||
268 | type2cont.put(toFunc, newArrayList(rel)) | 290 | type2cont.put(toFunc, newArrayList(rel)) |
269 | } else { | 291 | } else { |
270 | if (!type2cont.get(toFunc).contains(rel)) { | 292 | if (!type2cont.get(existingKey).contains(rel)) { |
271 | type2cont.get(toFunc).add(rel) | 293 | type2cont.get(existingKey).add(rel) |
272 | // type2cont.replace(toFunc, newArrayList(firstRel)) | 294 | // type2cont.replace(toFunc, newArrayList(firstRel)) |
273 | } | 295 | } |
274 | 296 | ||
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 ec841546..df3cfd82 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 | |||
@@ -23,18 +23,22 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
23 | this.base = base | 23 | this.base = base |
24 | } | 24 | } |
25 | 25 | ||
26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { | 26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, |
27 | Logic2VampireLanguageMapperTrace trace) { | ||
27 | val ABSOLUTE_MIN = 0 | 28 | val ABSOLUTE_MIN = 0 |
28 | val ABSOLUTE_MAX = Integer.MAX_VALUE | 29 | val ABSOLUTE_MAX = Integer.MAX_VALUE |
29 | 30 | ||
30 | // TODO HANDLE ERRORS RELATED TO MAX > MIN | 31 | // TODO HANDLE ERRORS RELATED TO MAX > MIN |
31 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS | 32 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS |
32 | // TODO HANDLE | 33 | // TODO HANDLE case where init model does not satisfy for example ine and only one criterion of toplvl elem |
33 | // 1. make a list of constants equaling the min number of specified objects | 34 | // We are currently ignoring all typescope spec related to the topLevel type |
34 | //These numbers do not include enums or initial model elements | 35 | // TODO Case where typeScope spec continas numbers for a type and its subtype |
36 | // We shouldnt waste constants for each one | ||
35 | 37 | ||
36 | //Number of defined non-abstract elements that are not enum elements | 38 | // 1. make a list of constants equaling the min number of specified objects |
37 | //Equals the number of elements in te initial model | 39 | // These numbers do not include enums or initial model elements |
40 | // Number of defined non-abstract elements that are not enum elements | ||
41 | // Equals the number of elements in te initial model | ||
38 | var elemsInIM = trace.definedElement2String.size | 42 | var elemsInIM = trace.definedElement2String.size |
39 | // var elemsInIM = 0 | 43 | // var elemsInIM = 0 |
40 | // | 44 | // |
@@ -45,10 +49,9 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
45 | // elemsInIM += 1 | 49 | // elemsInIM += 1 |
46 | // } | 50 | // } |
47 | // } | 51 | // } |
48 | 52 | // TODO handle errors related to GLOBAL_MIN/MAX < 0 | |
49 | //TODO handle errors related to GLOBAL_MIN/MAX < 0 | 53 | val GLOBAL_MIN = config.typeScopes.minNewElements - elemsInIM |
50 | val GLOBAL_MIN = config.typeScopes.minNewElements-elemsInIM | 54 | val GLOBAL_MAX = config.typeScopes.maxNewElements - elemsInIM |
51 | val GLOBAL_MAX = config.typeScopes.maxNewElements-elemsInIM | ||
52 | 55 | ||
53 | val localInstances = newArrayList | 56 | val localInstances = newArrayList |
54 | 57 | ||
@@ -79,62 +82,60 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
79 | 82 | ||
80 | // Handling Minimum_Specific | 83 | // Handling Minimum_Specific |
81 | var i = 1 | 84 | var i = 1 |
82 | if (trace.topLvlElementIsInInitialModel as Boolean){ | 85 | if (trace.topLvlElementIsInInitialModel as Boolean) { |
83 | i = 0 | 86 | i = 0 |
84 | } | 87 | } |
85 | var minNum = -1 | 88 | var minNum = -1 |
86 | var Map<Type, Integer> startPoints = new HashMap | 89 | var Map<Type, Integer> startPoints = new HashMap |
87 | // var inIM = false | 90 | for (t : config.typeScopes.minNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) { |
88 | for (tConfig : config.typeScopes.minNewElementsByType.keySet) { | 91 | var numIniIntModel = 0 |
89 | // var numIniIntModel = 0 | 92 | for (elem : trace.definedElement2String.keySet) { |
90 | // for (elem : trace.definedElement2String.keySet) { | 93 | for (tDefined : elem.definedInType) { |
91 | // println(elem.definedInType) | 94 | if (support.dfsSubtypeCheck(t, tDefined)) { |
92 | // for (tDefined : elem.definedInType) { | 95 | numIniIntModel += 1 |
93 | // inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined) | 96 | } |
94 | // } | 97 | } |
95 | // if (inIM) { | 98 | } |
96 | // numIniIntModel += 1 | 99 | minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel |
97 | // } | ||
98 | // inIM = false | ||
99 | // } | ||
100 | |||
101 | minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel | ||
102 | if (minNum != 0) { | 100 | if (minNum != 0) { |
103 | getInstanceConstants(i + minNum, i, localInstances, trace, true, false) | 101 | getInstanceConstants(i + minNum, i, localInstances, trace, true, false) |
104 | startPoints.put(tConfig, i) | 102 | startPoints.put(t, i) |
105 | i += minNum | 103 | i += minNum |
106 | makeFofFormula(localInstances, trace, true, tConfig) | 104 | makeFofFormula(localInstances, trace, true, t) |
107 | } | 105 | } |
108 | } | 106 | } |
109 | 107 | ||
110 | // TODO: calc sum of mins, compare to current value of i | 108 | // TODO: calc sum of mins, compare to current value of i |
111 | // Handling Maximum_Specific | 109 | // Handling Maximum_Specific |
112 | for (tConfig : config.typeScopes.maxNewElementsByType.keySet) { | 110 | for (t : config.typeScopes.maxNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) { |
113 | 111 | ||
114 | // var numIniIntModel = 0 | 112 | var numIniIntModel = 0 |
115 | // for (elem : trace.definedElement2String.keySet) { | 113 | for (elem : trace.definedElement2String.keySet) { |
116 | // println(elem.definedInType) | 114 | if (elem.definedInType == t) { |
117 | // for (tDefined : elem.definedInType) { | 115 | numIniIntModel += 1 |
118 | // inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined) | 116 | } |
119 | // } | 117 | } |
120 | // if (inIM) { | 118 | |
121 | // numIniIntModel += 1 | 119 | var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) - numIniIntModel |
122 | // } | 120 | if (config.typeScopes.minNewElementsByType.keySet.contains(t)) { |
123 | // inIM = false | 121 | minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel |
124 | // } | 122 | } else { |
125 | 123 | minNum = 0 | |
126 | var maxNum = tConfig.lookup(config.typeScopes.maxNewElementsByType)//-numIniIntModel | 124 | } |
127 | minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel | 125 | |
128 | var startpoint = tConfig.lookup(startPoints) | ||
129 | if (minNum != 0) { | 126 | if (minNum != 0) { |
127 | var startpoint = t.lookup(startPoints) | ||
130 | getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) | 128 | getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) |
131 | } | 129 | } |
132 | //I do not understand the line below | 130 | else { |
133 | if (maxNum != minNum) { | 131 | localInstances.clear |
134 | var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum) | ||
135 | getInstanceConstants(instEndInd, i, localInstances, trace, false, false) | ||
136 | makeFofFormula(localInstances, trace, false, tConfig) | ||
137 | } | 132 | } |
133 | // I do not understand the line below | ||
134 | // if (maxNum != minNum) { | ||
135 | var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum) | ||
136 | getInstanceConstants(instEndInd, i, localInstances, trace, false, false) | ||
137 | makeFofFormula(localInstances, trace, false, t) | ||
138 | // } | ||
138 | } | 139 | } |
139 | 140 | ||
140 | // 3. Specify uniqueness of elements | 141 | // 3. Specify uniqueness of elements |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index f312e3a8..677cb718 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 88960abc..d071aa8a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index 580eb165..48090814 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index adc1b1cf..154e42a2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index 57f21798..61774e26 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index 355315f8..2798d324 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index 77a5ce95..5f3f349b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 5eef76af..787c44a2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index b042022e..b6e94088 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index f1600087..c2ae099e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java | |||
@@ -33,6 +33,8 @@ public class Logic2VampireLanguageMapperTrace { | |||
33 | 33 | ||
34 | public Object topLvlElementIsInInitialModel = null; | 34 | public Object topLvlElementIsInInitialModel = null; |
35 | 35 | ||
36 | public Object topLevelType = null; | ||
37 | |||
36 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); | 38 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); |
37 | 39 | ||
38 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); | 40 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 07677b7a..dd549c29 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | |||
@@ -37,6 +37,7 @@ import org.eclipse.emf.common.util.EList; | |||
37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
38 | import org.eclipse.xtext.xbase.lib.Conversions; | 38 | import org.eclipse.xtext.xbase.lib.Conversions; |
39 | import org.eclipse.xtext.xbase.lib.Extension; | 39 | import org.eclipse.xtext.xbase.lib.Extension; |
40 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
40 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 41 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
41 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 42 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
42 | 43 | ||
@@ -89,6 +90,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
89 | } | 90 | } |
90 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString(); | 91 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString(); |
91 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); | 92 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); |
93 | trace.topLevelType = topTermVar; | ||
92 | boolean topLvlIsInInitModel = false; | 94 | boolean topLvlIsInInitModel = false; |
93 | String topLvlString = ""; | 95 | String topLvlString = ""; |
94 | ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar); | 96 | ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar); |
@@ -174,15 +176,16 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
174 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); | 176 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); |
175 | for (final Relation l_2 : relationsList) { | 177 | for (final Relation l_2 : relationsList) { |
176 | { | 178 | { |
177 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), varList); | 179 | final VLSFunction rel = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate); |
178 | TypeReference _get = l_2.getParameters().get(1); | 180 | TypeReference _get = l_2.getParameters().get(1); |
179 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | 181 | Type _referred = ((ComplexTypeReference) _get).getReferred(); |
180 | final Type toType = ((Type) _referred); | 182 | final Type toType = ((Type) _referred); |
181 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); | 183 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); |
182 | this.addToMap(type2cont, toFunc, rel); | 184 | this.addToMap(type2cont, this.support.duplicate(toFunc), this.support.duplicate(rel, varList)); |
183 | EList<Type> _subtypes = toType.getSubtypes(); | 185 | ArrayList<Type> subTypes = CollectionLiterals.<Type>newArrayList(); |
184 | for (final Type c_1 : _subtypes) { | 186 | this.support.listSubtypes(toType, subTypes); |
185 | this.addToMap(type2cont, toFunc, rel); | 187 | for (final Type c_1 : subTypes) { |
188 | this.addToMap(type2cont, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(c_1, trace.type2Predicate)), this.support.duplicate(rel, varList)); | ||
186 | } | 189 | } |
187 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 190 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
188 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | 191 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
@@ -231,6 +234,11 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
231 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); | 234 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); |
232 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { | 235 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { |
233 | { | 236 | { |
237 | VLSFunction _key = e.getKey(); | ||
238 | String _plus = (_key + " "); | ||
239 | List<VLSFunction> _value = e.getValue(); | ||
240 | String _plus_1 = (_plus + _value); | ||
241 | InputOutput.<String>println(_plus_1); | ||
234 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 242 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
235 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | 243 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
236 | it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); | 244 | it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); |
@@ -352,20 +360,32 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
352 | } | 360 | } |
353 | 361 | ||
354 | protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) { | 362 | protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) { |
355 | Object _xifexpression = null; | 363 | Object _xblockexpression = null; |
356 | boolean _containsKey = type2cont.containsKey(toFunc); | 364 | { |
357 | boolean _not = (!_containsKey); | 365 | boolean keyInMap = false; |
358 | if (_not) { | 366 | VLSFunction existingKey = this.factory.createVLSFunction(); |
359 | _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel)); | 367 | Set<VLSFunction> _keySet = type2cont.keySet(); |
360 | } else { | 368 | for (final VLSFunction k : _keySet) { |
361 | boolean _xifexpression_1 = false; | 369 | boolean _equals = k.getConstant().equals(toFunc.getConstant()); |
362 | boolean _contains = type2cont.get(toFunc).contains(rel); | 370 | if (_equals) { |
363 | boolean _not_1 = (!_contains); | 371 | keyInMap = true; |
364 | if (_not_1) { | 372 | existingKey = k; |
365 | _xifexpression_1 = type2cont.get(toFunc).add(rel); | 373 | } |
374 | } | ||
375 | Object _xifexpression = null; | ||
376 | if ((!keyInMap)) { | ||
377 | _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel)); | ||
378 | } else { | ||
379 | boolean _xifexpression_1 = false; | ||
380 | boolean _contains = type2cont.get(existingKey).contains(rel); | ||
381 | boolean _not = (!_contains); | ||
382 | if (_not) { | ||
383 | _xifexpression_1 = type2cont.get(existingKey).add(rel); | ||
384 | } | ||
385 | _xifexpression = Boolean.valueOf(_xifexpression_1); | ||
366 | } | 386 | } |
367 | _xifexpression = Boolean.valueOf(_xifexpression_1); | 387 | _xblockexpression = _xifexpression; |
368 | } | 388 | } |
369 | return _xifexpression; | 389 | return _xblockexpression; |
370 | } | 390 | } |
371 | } | 391 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index bf7b70d0..c2e4033b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |||
@@ -14,7 +14,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | |||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
17 | import com.google.common.base.Objects; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
18 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 21 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
19 | import java.util.ArrayList; | 22 | import java.util.ArrayList; |
20 | import java.util.HashMap; | 23 | import java.util.HashMap; |
@@ -26,6 +29,7 @@ import org.eclipse.xtext.xbase.lib.CollectionLiterals; | |||
26 | import org.eclipse.xtext.xbase.lib.Conversions; | 29 | import org.eclipse.xtext.xbase.lib.Conversions; |
27 | import org.eclipse.xtext.xbase.lib.Extension; | 30 | import org.eclipse.xtext.xbase.lib.Extension; |
28 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
29 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 33 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
30 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 34 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
31 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 35 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
@@ -80,33 +84,73 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
80 | } | 84 | } |
81 | int minNum = (-1); | 85 | int minNum = (-1); |
82 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); | 86 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); |
83 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); | 87 | final Function1<Type, Boolean> _function = (Type it) -> { |
84 | for (final Type tConfig : _keySet) { | 88 | boolean _equals = it.equals(trace.topLevelType); |
89 | return Boolean.valueOf((!_equals)); | ||
90 | }; | ||
91 | Iterable<Type> _filter = IterableExtensions.<Type>filter(config.typeScopes.minNewElementsByType.keySet(), _function); | ||
92 | for (final Type t : _filter) { | ||
85 | { | 93 | { |
86 | minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig, config.typeScopes.minNewElementsByType)).intValue(); | 94 | int numIniIntModel = 0; |
95 | Set<DefinedElement> _keySet = trace.definedElement2String.keySet(); | ||
96 | for (final DefinedElement elem : _keySet) { | ||
97 | EList<TypeDefinition> _definedInType = elem.getDefinedInType(); | ||
98 | for (final TypeDefinition tDefined : _definedInType) { | ||
99 | boolean _dfsSubtypeCheck = this.support.dfsSubtypeCheck(t, tDefined); | ||
100 | if (_dfsSubtypeCheck) { | ||
101 | int _numIniIntModel = numIniIntModel; | ||
102 | numIniIntModel = (_numIniIntModel + 1); | ||
103 | } | ||
104 | } | ||
105 | } | ||
106 | Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType); | ||
107 | int _minus = ((_lookup).intValue() - numIniIntModel); | ||
108 | minNum = _minus; | ||
87 | if ((minNum != 0)) { | 109 | if ((minNum != 0)) { |
88 | this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); | 110 | this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); |
89 | startPoints.put(tConfig, Integer.valueOf(i_1)); | 111 | startPoints.put(t, Integer.valueOf(i_1)); |
90 | int _i = i_1; | 112 | int _i = i_1; |
91 | i_1 = (_i + minNum); | 113 | i_1 = (_i + minNum); |
92 | this.makeFofFormula(localInstances, trace, true, tConfig); | 114 | this.makeFofFormula(localInstances, trace, true, t); |
93 | } | 115 | } |
94 | } | 116 | } |
95 | } | 117 | } |
96 | Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); | 118 | final Function1<Type, Boolean> _function_1 = (Type it) -> { |
97 | for (final Type tConfig_1 : _keySet_1) { | 119 | boolean _equals = it.equals(trace.topLevelType); |
120 | return Boolean.valueOf((!_equals)); | ||
121 | }; | ||
122 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(config.typeScopes.maxNewElementsByType.keySet(), _function_1); | ||
123 | for (final Type t_1 : _filter_1) { | ||
98 | { | 124 | { |
99 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.maxNewElementsByType); | 125 | int numIniIntModel = 0; |
100 | minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.minNewElementsByType)).intValue(); | 126 | Set<DefinedElement> _keySet = trace.definedElement2String.keySet(); |
101 | Integer startpoint = CollectionsUtil.<Type, Integer>lookup(tConfig_1, startPoints); | 127 | for (final DefinedElement elem : _keySet) { |
128 | EList<TypeDefinition> _definedInType = elem.getDefinedInType(); | ||
129 | boolean _equals = Objects.equal(_definedInType, t_1); | ||
130 | if (_equals) { | ||
131 | int _numIniIntModel = numIniIntModel; | ||
132 | numIniIntModel = (_numIniIntModel + 1); | ||
133 | } | ||
134 | } | ||
135 | Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); | ||
136 | int maxNum = ((_lookup).intValue() - numIniIntModel); | ||
137 | boolean _contains = config.typeScopes.minNewElementsByType.keySet().contains(t_1); | ||
138 | if (_contains) { | ||
139 | Integer _lookup_1 = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType); | ||
140 | int _minus = ((_lookup_1).intValue() - numIniIntModel); | ||
141 | minNum = _minus; | ||
142 | } else { | ||
143 | minNum = 0; | ||
144 | } | ||
102 | if ((minNum != 0)) { | 145 | if ((minNum != 0)) { |
146 | Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints); | ||
103 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); | 147 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); |
148 | } else { | ||
149 | localInstances.clear(); | ||
104 | } | 150 | } |
105 | if (((maxNum).intValue() != minNum)) { | 151 | int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + maxNum) - minNum)); |
106 | int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); | 152 | this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); |
107 | this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); | 153 | this.makeFofFormula(localInstances, trace, false, t_1); |
108 | this.makeFofFormula(localInstances, trace, false, tConfig_1); | ||
109 | } | ||
110 | } | 154 | } |
111 | } | 155 | } |
112 | final boolean DUPLICATES = config.uniquenessDuplicates; | 156 | final boolean DUPLICATES = config.uniquenessDuplicates; |
@@ -118,12 +162,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
118 | { | 162 | { |
119 | final int x = ind; | 163 | final int x = ind; |
120 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 164 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
121 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 165 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { |
122 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); | 166 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); |
123 | it.setFofRole("axiom"); | 167 | it.setFofRole("axiom"); |
124 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); | 168 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); |
125 | }; | 169 | }; |
126 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 170 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); |
127 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 171 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
128 | _formulas.add(uniqueness); | 172 | _formulas.add(uniqueness); |
129 | ind++; | 173 | ind++; |
@@ -135,12 +179,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
135 | { | 179 | { |
136 | final int x = ind; | 180 | final int x = ind; |
137 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 181 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
138 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 182 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { |
139 | it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName())); | 183 | it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName())); |
140 | it.setFofRole("axiom"); | 184 | it.setFofRole("axiom"); |
141 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1)); | 185 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1)); |
142 | }; | 186 | }; |
143 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 187 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); |
144 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 188 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
145 | _formulas.add(uniqueness); | 189 | _formulas.add(uniqueness); |
146 | ind++; | 190 | ind++; |