aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend159
1 files changed, 72 insertions, 87 deletions
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 6f3b13ef..23b57701 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
@@ -24,52 +24,97 @@ class Logic2VampireLanguageMapper_RelationMapper {
24 this.base = base 24 this.base = base
25 } 25 }
26 26
27 def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace) { 27 def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) {
28 28
29 // 1. store all variables in support wrt their name 29 // 1. store all variables in support wrt their name
30 // 1.1 if variable has type, creating list of type declarations 30 // 1.1 if variable has type, creating list of type declarations
31 val List<VLSVariable> relVar2VLS = new ArrayList
32 val List<VLSFunction> relVar2TypeDecComply = new ArrayList
33 val typedefs = new ArrayList<VLSTerm>
34
35 for (i : 0 ..< r.parameters.length) {
36
37 val v = createVLSVariable => [
38 it.name = support.toIDMultiple("V", i.toString)
39 ]
40 relVar2VLS.add(v)
41
42 val relType = (r.parameters.get(i) as ComplexTypeReference).referred
43 val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v)
44 relVar2TypeDecComply.add(varTypeComply)
45
46 }
47
48 val comply = createVLSFofFormula => [
49 val nameArray = r.name.split(" ")
50 it.name = support.toIDMultiple("compliance", nameArray.get(0),
51 nameArray.get(2))
52 it.fofRole = "axiom"
53 it.fofFormula = createVLSUniversalQuantifier => [
54
55 for (v : relVar2VLS) {
56 it.variables += support.duplicate(v)
57 }
58
59 it.operand = createVLSImplies => [
60 it.left = createVLSFunction => [
61 it.constant = support.toIDMultiple("rel", r.name)
62
63 for (i : 0 ..< r.parameters.length) {
64 val v = createVLSVariable => [
65 it.name = relVar2VLS.get(i).name
66 ]
67 it.terms += v
68 }
69
70 ]
71 it.right = support.unfoldAnd(relVar2TypeDecComply)
72 ]
73 ]
74 ]
75
76 // trace.relationDefinition2Predicate.put(r,res)
77 trace.specification.formulas += comply
78 }
79
80 def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) {
81
82 // 1. store all variables in support wrt their name
83 // 1.1 if variable has type, creating list of type declarations
84// val VLSVariable variable = createVLSVariable => [it.name = "A"]
31 val Map<Variable, VLSVariable> relationVar2VLS = new HashMap 85 val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
32 val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap 86 val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
33 val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap 87 val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
34 val typedefs = new ArrayList<VLSTerm> 88 val typedefs = new ArrayList<VLSTerm>
35 for (variable : r.variables) { 89
90 for (variable : reldef.variables) {
36 val v = createVLSVariable => [ 91 val v = createVLSVariable => [
37 it.name = support.toIDMultiple("Var", variable.name) 92 it.name = support.toIDMultiple("V", variable.name)
38 ] 93 ]
39 relationVar2VLS.put(variable, v) 94 relationVar2VLS.put(variable, v)
40 95
41 val varTypeComply = createVLSFunction => [ 96 val varTypeComply = createVLSFunction => [
42 it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) 97 it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
43 it.terms += createVLSVariable => [ 98 it.terms += support.duplicate(v)
44 it.name = support.toIDMultiple("Var", variable.name)
45 ]
46 ] 99 ]
47 relationVar2TypeDecComply.put(variable, varTypeComply) 100 relationVar2TypeDecComply.put(variable, varTypeComply)
48 101 relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
49 val varTypeRes = createVLSFunction => [
50 it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
51 it.terms += createVLSVariable => [
52 it.name = support.toIDMultiple("Var", variable.name)
53 ]
54 ]
55 relationVar2TypeDecRes.put(variable, varTypeRes)
56 } 102 }
57 103
58 val comply = createVLSFofFormula => [ 104 val comply = createVLSFofFormula => [
59 it.name = support.toIDMultiple("compliance", r.name) 105 val nameArray = reldef.name.split(" ")
106 it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
107 nameArray.get(nameArray.length - 1))
60 it.fofRole = "axiom" 108 it.fofRole = "axiom"
61 it.fofFormula = createVLSUniversalQuantifier => [ 109 it.fofFormula = createVLSUniversalQuantifier => [
62 for (variable : r.variables) { 110 for (variable : reldef.variables) {
63 val v = createVLSVariable => [ 111 it.variables += support.duplicate(variable.lookup(relationVar2VLS))
64 it.name = variable.lookup(relationVar2VLS).name
65 ]
66 it.variables += v
67 112
68 } 113 }
69 it.operand = createVLSImplies => [ 114 it.operand = createVLSImplies => [
70 it.left = createVLSFunction => [ 115 it.left = createVLSFunction => [
71 it.constant = support.toIDMultiple("rel", r.name) 116 it.constant = support.toIDMultiple("rel", reldef.name)
72 for (variable : r.variables) { 117 for (variable : reldef.variables) {
73 val v = createVLSVariable => [ 118 val v = createVLSVariable => [
74 it.name = variable.lookup(relationVar2VLS).name 119 it.name = variable.lookup(relationVar2VLS).name
75 ] 120 ]
@@ -82,10 +127,10 @@ class Logic2VampireLanguageMapper_RelationMapper {
82 ] 127 ]
83 128
84 val res = createVLSFofFormula => [ 129 val res = createVLSFofFormula => [
85 it.name = support.toIDMultiple("relation", r.name) 130 it.name = support.toIDMultiple("relation", reldef.name)
86 it.fofRole = "axiom" 131 it.fofRole = "axiom"
87 it.fofFormula = createVLSUniversalQuantifier => [ 132 it.fofFormula = createVLSUniversalQuantifier => [
88 for (variable : r.variables) { 133 for (variable : reldef.variables) {
89 val v = createVLSVariable => [ 134 val v = createVLSVariable => [
90 it.name = variable.lookup(relationVar2VLS).name 135 it.name = variable.lookup(relationVar2VLS).name
91 ] 136 ]
@@ -96,8 +141,8 @@ class Logic2VampireLanguageMapper_RelationMapper {
96 it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) 141 it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
97 it.right = createVLSEquivalent => [ 142 it.right = createVLSEquivalent => [
98 it.left = createVLSFunction => [ 143 it.left = createVLSFunction => [
99 it.constant = support.toIDMultiple("rel", r.name) 144 it.constant = support.toIDMultiple("rel", reldef.name)
100 for (variable : r.variables) { 145 for (variable : reldef.variables) {
101 val v = createVLSVariable => [ 146 val v = createVLSVariable => [
102 it.name = variable.lookup(relationVar2VLS).name 147 it.name = variable.lookup(relationVar2VLS).name
103 ] 148 ]
@@ -105,7 +150,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
105 150
106 } 151 }
107 ] 152 ]
108 it.right = base.transformTerm(r.value, trace, relationVar2VLS) 153 it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
109 ] 154 ]
110 155
111 ] 156 ]
@@ -119,65 +164,5 @@ class Logic2VampireLanguageMapper_RelationMapper {
119 trace.specification.formulas += res; 164 trace.specification.formulas += res;
120 165
121 } 166 }
122
123 def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) {
124
125 // 1. store all variables in support wrt their name
126 // 1.1 if variable has type, creating list of type declarations
127 val List<VLSVariable> relationVar2VLS = new ArrayList
128 val List<VLSFunction> relationVar2TypeDecComply = new ArrayList
129 val typedefs = new ArrayList<VLSTerm>
130
131 for (i : 0..<r.parameters.length) {
132
133 val v = createVLSVariable => [
134 it.name = support.toIDMultiple("Var", i.toString)
135 ]
136 relationVar2VLS.add(v)
137
138 val varTypeComply = createVLSFunction => [
139 it.constant = support.toIDMultiple("t", (r.parameters.get(i) as ComplexTypeReference).referred.name)
140 it.terms += createVLSVariable => [
141 it.name = support.toIDMultiple("Var", i.toString)
142 ]
143 ]
144 relationVar2TypeDecComply.add(varTypeComply)
145
146 }
147
148
149 val comply = createVLSFofFormula => [
150 it.name = support.toIDMultiple("compliance", r.name)
151 it.fofRole = "axiom"
152 it.fofFormula = createVLSUniversalQuantifier => [
153
154 for (i : 0..<r.parameters.length) {
155 val v = createVLSVariable => [
156 it.name = relationVar2VLS.get(i).name
157 ]
158 it.variables += v
159
160 }
161
162 it.operand = createVLSImplies => [
163 it.left = createVLSFunction => [
164 it.constant = support.toIDMultiple("rel", r.name)
165
166 for (i : 0..<r.parameters.length) {
167 val v = createVLSVariable => [
168 it.name = relationVar2VLS.get(i).name
169 ]
170 it.terms += v
171 }
172
173 ]
174 it.right = support.unfoldAnd(relationVar2TypeDecComply)
175 ]
176 ]
177 ]
178
179 // trace.relationDefinition2Predicate.put(r,res)
180 trace.specification.formulas += comply
181 }
182 167
183} 168}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-17 18:08:13 +0000