aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-04-25 02:50:40 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2020-06-07 19:37:07 -0400
commit598daf4605d97466d07c74b1bc76d165be145288 (patch)
tree3756188257ae023e0cdf22b840ea4ce5dfa95505 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner
parentVAMPIRE : initial model handling almost done. only typeScope remains #40 (diff)
downloadVIATRA-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/src/ca/mcgill/ecse/dslreasoner')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend1
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend38
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend101
3 files changed, 82 insertions, 58 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-26 08:46:45 +0000