aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-04-15 00:06:29 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2020-06-07 19:36:48 -0400
commit85e6d0b8590f5aa22cd7065cb850b0f460da25dd (patch)
treefcc945827435f113aa9099d0be63d68551f7f5a3 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill
parentVAMPIRE: #39 Reorganise tests, working yakindu test, need debugging (diff)
downloadVIATRA-Generator-85e6d0b8590f5aa22cd7065cb850b0f460da25dd.tar.gz
VIATRA-Generator-85e6d0b8590f5aa22cd7065cb850b0f460da25dd.tar.zst
VIATRA-Generator-85e6d0b8590f5aa22cd7065cb850b0f460da25dd.zip
VAMPIRE: close #22, improve test structure for #39, .vql file trouble
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend12
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend183
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend1
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend12
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend23
5 files changed, 126 insertions, 105 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 395b4305..8e0e0b11 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
@@ -39,7 +39,15 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
39 for (l : relationsList) { 39 for (l : relationsList) {
40 var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type 40 var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
41 containmentListCopy.remove(pointingTo) 41 containmentListCopy.remove(pointingTo)
42 for (c : pointingTo.subtypes) { 42 var List<Type> allSubtypes = newArrayList
43 support.listSubtypes(pointingTo, allSubtypes)
44 for (c : allSubtypes) {
45 containmentListCopy.remove(c)
46 }
47 }
48
49 for (c : containmentListCopy) {
50 if(c.isIsAbstract) {
43 containmentListCopy.remove(c) 51 containmentListCopy.remove(c)
44 } 52 }
45 } 53 }
@@ -135,7 +143,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
135// STEP 2 CONT'D 143// STEP 2 CONT'D
136 for (e : type2cont.entrySet) { 144 for (e : type2cont.entrySet) {
137 val relFormula = createVLSFofFormula => [ 145 val relFormula = createVLSFofFormula => [
138 it.name = support.toIDMultiple("containment", e.key.constant.toString) 146 it.name = support.toIDMultiple("containment_contained", e.key.constant.toString)
139 it.fofRole = "axiom" 147 it.fofRole = "axiom"
140 148
141 it.fofFormula = createVLSUniversalQuantifier => [ 149 it.fofFormula = createVLSUniversalQuantifier => [
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index 0ae06bc3..2dec281d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -44,9 +44,20 @@ class Logic2VampireLanguageMapper_RelationMapper {
44 44
45 } 45 }
46 46
47 //deciding name of relation
48 val nameArray = r.name.split(" ")
49 var relNameVar = ""
50 if (nameArray.length == 3) {
51 relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
52 }
53 else {
54 relNameVar = r.name
55 }
56 val relName = relNameVar
57
47 val comply = createVLSFofFormula=> [ 58 val comply = createVLSFofFormula=> [
48 val nameArray = r.name.split(" ") 59
49 it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2)) 60 it.name = support.toIDMultiple("compliance", relName)
50 it.fofRole = "axiom" 61 it.fofRole = "axiom"
51 it.fofFormula = createVLSUniversalQuantifier => [ 62 it.fofFormula = createVLSUniversalQuantifier => [
52 for (v : relVar2VLS) { 63 for (v : relVar2VLS) {
@@ -54,7 +65,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
54 } 65 }
55 it.operand = createVLSImplies => [ 66 it.operand = createVLSImplies => [
56 val rel = createVLSFunction => [ 67 val rel = createVLSFunction => [
57 it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2)) 68 it.constant = support.toIDMultiple("r", relName)
58 for (v : relVar2VLS) { 69 for (v : relVar2VLS) {
59 it.terms += support.duplicate(v) 70 it.terms += support.duplicate(v)
60 } 71 }
@@ -71,89 +82,89 @@ class Logic2VampireLanguageMapper_RelationMapper {
71 82
72 def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { 83 def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) {
73 84
74 // 1. store all variables in support wrt their name 85// // 1. store all variables in support wrt their name
75 // 1.1 if variable has type, creating list of type declarations 86// // 1.1 if variable has type, creating list of type declarations
76// val VLSVariable variable = createVLSVariable => [it.name = "A"] 87//// val VLSVariable variable = createVLSVariable => [it.name = "A"]
77 val Map<Variable, VLSVariable> relationVar2VLS = new HashMap 88// val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
78 val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap 89// val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
79 val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap 90// val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
80 val typedefs = new ArrayList<VLSTerm> 91// val typedefs = new ArrayList<VLSTerm>
81 92//
82 for (variable : reldef.variables) { 93// for (variable : reldef.variables) {
83 val v = createVLSVariable => [ 94// val v = createVLSVariable => [
84 it.name = support.toIDMultiple("V", variable.name) 95// it.name = support.toIDMultiple("V", variable.name)
85 ] 96// ]
86 relationVar2VLS.put(variable, v) 97// relationVar2VLS.put(variable, v)
87 98//
88 val varTypeComply = createVLSFunction => [ 99// val varTypeComply = createVLSFunction => [
89 it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) 100// it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
90 it.terms += support.duplicate(v) 101// it.terms += support.duplicate(v)
91 ] 102// ]
92 relationVar2TypeDecComply.put(variable, varTypeComply) 103// relationVar2TypeDecComply.put(variable, varTypeComply)
93 relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) 104// relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
94 } 105// }
95 val nameArray = reldef.name.split(" ") 106// val nameArray = reldef.name.split(" ")
96 val comply = createVLSFofFormula => [ 107// val comply = createVLSFofFormula => [
97 it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), 108// it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
98 nameArray.get(nameArray.length - 1)) 109// nameArray.get(nameArray.length - 1))
99 it.fofRole = "axiom" 110// it.fofRole = "axiom"
100 it.fofFormula = createVLSUniversalQuantifier => [ 111// it.fofFormula = createVLSUniversalQuantifier => [
101 for (variable : reldef.variables) { 112// for (variable : reldef.variables) {
102 it.variables += support.duplicate(variable.lookup(relationVar2VLS)) 113// it.variables += support.duplicate(variable.lookup(relationVar2VLS))
103 114//
104 } 115// }
105 it.operand = createVLSImplies => [ 116// it.operand = createVLSImplies => [
106 it.left = createVLSFunction => [ 117// it.left = createVLSFunction => [
107 it.constant = support.toIDMultiple("rel", reldef.name) 118// it.constant = support.toIDMultiple("rel", reldef.name)
108 for (variable : reldef.variables) { 119// for (variable : reldef.variables) {
109 val v = createVLSVariable => [ 120// val v = createVLSVariable => [
110 it.name = variable.lookup(relationVar2VLS).name 121// it.name = variable.lookup(relationVar2VLS).name
111 ] 122// ]
112 it.terms += v 123// it.terms += v
113 } 124// }
114 ] 125// ]
115 it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values)) 126// it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
116 ] 127// ]
117 ] 128// ]
118 ] 129// ]
119 130//
120 val res = createVLSFofFormula => [ 131// val res = createVLSFofFormula => [
121 it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), 132// it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
122 nameArray.get(nameArray.length - 1)) 133// nameArray.get(nameArray.length - 1))
123 it.fofRole = "axiom" 134// it.fofRole = "axiom"
124 it.fofFormula = createVLSUniversalQuantifier => [ 135// it.fofFormula = createVLSUniversalQuantifier => [
125 for (variable : reldef.variables) { 136// for (variable : reldef.variables) {
126 val v = createVLSVariable => [ 137// val v = createVLSVariable => [
127 it.name = variable.lookup(relationVar2VLS).name 138// it.name = variable.lookup(relationVar2VLS).name
128 ] 139// ]
129 it.variables += v 140// it.variables += v
130 141//
131 } 142// }
132 it.operand = createVLSImplies => [ 143// it.operand = createVLSImplies => [
133 it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) 144// it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
134 it.right = createVLSEquivalent => [ 145// it.right = createVLSEquivalent => [
135 it.left = createVLSFunction => [ 146// it.left = createVLSFunction => [
136 it.constant = support.toIDMultiple("rel", reldef.name) 147// it.constant = support.toIDMultiple("rel", reldef.name)
137 for (variable : reldef.variables) { 148// for (variable : reldef.variables) {
138 val v = createVLSVariable => [ 149// val v = createVLSVariable => [
139 it.name = variable.lookup(relationVar2VLS).name 150// it.name = variable.lookup(relationVar2VLS).name
140 ] 151// ]
141 it.terms += v 152// it.terms += v
142 153//
143 } 154// }
144 ] 155// ]
145 it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) 156// it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
146 ] 157// ]
147 158//
148 ] 159// ]
149 160//
150 ] 161// ]
151 162//
152 ] 163// ]
153 164//
154 // trace.relationDefinition2Predicate.put(r,res) 165// // trace.relationDefinition2Predicate.put(r,res)
155 trace.specification.formulas += comply; 166// trace.specification.formulas += comply;
156 trace.specification.formulas += res; 167// trace.specification.formulas += res;
157 168
158 } 169 }
159 170
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 0a8812e4..4a8d2827 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
@@ -29,6 +29,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
29// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS 29// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS
30// TODO HANDLE 30// TODO HANDLE
31 // 1. make a list of constants equaling the min number of specified objects 31 // 1. make a list of constants equaling the min number of specified objects
32 //These numbers do not include enums or initial model elements
32 val GLOBAL_MIN = config.typeScopes.minNewElements 33 val GLOBAL_MIN = config.typeScopes.minNewElements
33 val GLOBAL_MAX = config.typeScopes.maxNewElements 34 val GLOBAL_MAX = config.typeScopes.maxNewElements
34 35
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 195b89bb..680213ab 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
@@ -273,15 +273,11 @@ class Logic2VampireLanguageMapper_Support {
273 } 273 }
274 } 274 }
275 275
276 def protected List<Type> listSubtypes(Type t) { 276 def protected void listSubtypes(Type t, List<Type> allSubtypes) {
277 var List<Type> allSubtypes = newArrayList 277 for (subt : t.subtypes) {
278 if (!t.subtypes.isEmpty) { 278 allSubtypes.add(subt)
279 for (subt : t.subtypes) { 279 listSubtypes(subt, allSubtypes)
280 allSubtypes.add(subt)
281 allSubtypes = listSubtypes(subt)
282 }
283 } 280 }
284 return allSubtypes
285 } 281 }
286 282
287 def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { 283 def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> 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 3bc945df..2f3af593 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
@@ -44,14 +44,19 @@ class Logic2VampireLanguageMapper_TypeMapper {
44 44
45 // Create a VLSFunction for each Enum Element 45 // Create a VLSFunction for each Enum Element
46 val List<VLSFunction> orElems = newArrayList 46 val List<VLSFunction> orElems = newArrayList
47
47 for (e : type.elements) { 48 for (e : type.elements) {
49 val nameArray = e.name.split(" ")
50 var relNameVar = ""
51 if (nameArray.length == 3) {
52 relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
53 } else {
54 relNameVar = e.name
55 }
56 val relName = relNameVar
57
48 val enumElemPred = createVLSFunction => [ 58 val enumElemPred = createVLSFunction => [
49 val splitName = e.name.split(" ") 59 it.constant = support.toIDMultiple("e", relName)
50 if (splitName.length > 2) {
51 it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2))
52 } else {
53 it.constant = support.toIDMultiple("e", splitName.get(0))
54 }
55 it.terms += support.duplicate(variable) 60 it.terms += support.duplicate(variable)
56 ] 61 ]
57 trace.element2Predicate.put(e, enumElemPred) 62 trace.element2Predicate.put(e, enumElemPred)
@@ -80,7 +85,7 @@ class Logic2VampireLanguageMapper_TypeMapper {
80 85
81 // Implement Enum Inheritence Hierarchy 86 // Implement Enum Inheritence Hierarchy
82 val res = createVLSFofFormula => [ 87 val res = createVLSFofFormula => [
83 it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) 88 it.name = support.toIDMultiple("typeDef", type.lookup(trace.type2Predicate).constant.toString)
84 it.fofRole = "axiom" 89 it.fofRole = "axiom"
85 it.fofFormula = createVLSUniversalQuantifier => [ 90 it.fofFormula = createVLSUniversalQuantifier => [
86 it.variables += support.duplicate(variable) 91 it.variables += support.duplicate(variable)
@@ -105,9 +110,9 @@ class Logic2VampireLanguageMapper_TypeMapper {
105 val cst = support.toConstant(cstTerm) 110 val cst = support.toConstant(cstTerm)
106 trace.uniqueInstances.add(cst) 111 trace.uniqueInstances.add(cst)
107 112
108 val index = i 113 val index = i-globalCounter
109 val enumScope = createVLSFofFormula => [ 114 val enumScope = createVLSFofFormula => [
110 it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0), 115 it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString,
111 type.elements.get(index).name.split(" ").get(0)) 116 type.elements.get(index).name.split(" ").get(0))
112 it.fofRole = "axiom" 117 it.fofRole = "axiom"
113 it.fofFormula = createVLSUniversalQuantifier => [ 118 it.fofFormula = createVLSUniversalQuantifier => [
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-28 06:39:42 +0000