diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-05 21:33:28 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:22:40 -0400 |
commit | 3d92a0eb813309993892a978482b2858179034f7 (patch) | |
tree | 12203a71c02430b0f8fb93dafbd4aa68be60f8b1 /Solvers | |
parent | Implement type scope handling (diff) | |
download | VIATRA-Generator-3d92a0eb813309993892a978482b2858179034f7.tar.gz VIATRA-Generator-3d92a0eb813309993892a978482b2858179034f7.tar.zst VIATRA-Generator-3d92a0eb813309993892a978482b2858179034f7.zip |
Partially improve coding style (leaving for soccer)
Diffstat (limited to 'Solvers')
23 files changed, 330 insertions, 331 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 135b3f07..3c672f4b 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 | |||
@@ -1,15 +1,17 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula | 3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
13 | import java.util.HashMap | 15 | import java.util.HashMap |
14 | import java.util.Map | 16 | import java.util.Map |
15 | 17 | ||
@@ -22,17 +24,29 @@ class Logic2VampireLanguageMapperTrace { | |||
22 | public var VampireModel specification | 24 | public var VampireModel specification |
23 | public var VLSFofFormula logicLanguageBody | 25 | public var VLSFofFormula logicLanguageBody |
24 | public var VLSTerm formula | 26 | public var VLSTerm formula |
25 | //NOT NEEDED //public var VLSFunction constantDec | ||
26 | 27 | ||
28 | //Necessary containers | ||
27 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace | 29 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace |
28 | 30 | ||
31 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; | ||
32 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap | ||
33 | public val Map<Type, VLSTerm> type2PossibleNot = new HashMap | ||
34 | public val Map<Type, VLSTerm> type2And = new HashMap | ||
35 | |||
36 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | ||
37 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | ||
38 | public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap | ||
39 | |||
40 | |||
41 | //NOT NEEDED //public var VLSFunction constantDec | ||
42 | |||
43 | |||
44 | |||
29 | 45 | ||
30 | //NOT NEEDED //public val Map<ConstantDeclaration, VLSFunctionDeclaration> constantDeclaration2LanguageField = new HashMap | 46 | //NOT NEEDED //public val Map<ConstantDeclaration, VLSFunctionDeclaration> constantDeclaration2LanguageField = new HashMap |
31 | //public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap | 47 | //public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap |
32 | 48 | ||
33 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | ||
34 | 49 | ||
35 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | ||
36 | public val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | 50 | public val Map<Variable, VLSVariable> relationVar2VLS = new HashMap |
37 | public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap | 51 | public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap |
38 | 52 | ||
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 | } |
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 06ec585c..090cf916 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 | |||
@@ -1,20 +1,21 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable |
11 | import java.util.ArrayList | 14 | import java.util.ArrayList |
12 | import java.util.HashMap | 15 | import java.util.HashMap |
13 | import java.util.List | 16 | import java.util.List |
14 | import java.util.Map | 17 | import java.util.Map |
15 | import org.eclipse.emf.common.util.EList | 18 | import org.eclipse.emf.common.util.EList |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality | ||
18 | 19 | ||
19 | class Logic2VampireLanguageMapper_Support { | 20 | class Logic2VampireLanguageMapper_Support { |
20 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 21 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -28,10 +29,28 @@ class Logic2VampireLanguageMapper_Support { | |||
28 | ids.split("\\s+").join("_") | 29 | ids.split("\\s+").join("_") |
29 | } | 30 | } |
30 | 31 | ||
32 | //Term Handling | ||
31 | //TODO Make more general | 33 | //TODO Make more general |
32 | def protected VLSVariable duplicate(VLSVariable vrbl) { | 34 | def protected VLSVariable duplicate(VLSVariable term) { |
33 | return createVLSVariable => [it.name = vrbl.name] | 35 | return createVLSVariable => [it.name = term.name] |
36 | } | ||
37 | |||
38 | def protected VLSFunction duplicate(VLSFunction term) { | ||
39 | return createVLSFunction => [ | ||
40 | it.constant = term.constant | ||
41 | for ( v : term.terms){ | ||
42 | it.terms += duplicate(v as VLSVariable) | ||
43 | } | ||
44 | ] | ||
34 | } | 45 | } |
46 | |||
47 | def protected VLSFunction duplicate(VLSFunction term, VLSVariable v) { | ||
48 | return createVLSFunction => [ | ||
49 | it.constant = term.constant | ||
50 | it.terms += duplicate(v) | ||
51 | ] | ||
52 | } | ||
53 | |||
35 | 54 | ||
36 | def protected VLSFunction topLevelTypeFunc() { | 55 | def protected VLSFunction topLevelTypeFunc() { |
37 | return createVLSFunction => [ | 56 | return createVLSFunction => [ |
@@ -175,6 +194,21 @@ class Logic2VampireLanguageMapper_Support { | |||
175 | 194 | ||
176 | ] | 195 | ] |
177 | } | 196 | } |
197 | |||
198 | def protected boolean dfsSupertypeCheck(Type type, Type type2) { | ||
199 | // There is surely a better way to do this | ||
200 | if (type.supertypes.isEmpty) | ||
201 | return false | ||
202 | else { | ||
203 | if (type.supertypes.contains(type2)) | ||
204 | return true | ||
205 | else { | ||
206 | for (supertype : type.supertypes) { | ||
207 | if(dfsSupertypeCheck(supertype, type2)) return true | ||
208 | } | ||
209 | } | ||
210 | } | ||
211 | } | ||
178 | 212 | ||
179 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | 213 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { |
180 | new HashMap(map1) => [putAll(map2)] | 214 | 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_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend index 88e1e23a..ea72940e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend | |||
@@ -22,21 +22,20 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp | |||
22 | LogicproblemPackage.eINSTANCE.class | 22 | LogicproblemPackage.eINSTANCE.class |
23 | } | 23 | } |
24 | 24 | ||
25 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, | 25 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { |
26 | Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { | 26 | |
27 | val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes | 27 | // val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes |
28 | trace.typeMapperTrace = typeTrace | 28 | // trace.typeMapperTrace = typeTrace |
29 | |||
30 | // The variable | ||
31 | val VLSVariable variable = createVLSVariable => [it.name = "A"] | 29 | val VLSVariable variable = createVLSVariable => [it.name = "A"] |
32 | 30 | ||
33 | // 1. Each type (class) is a predicate with a single variable as input | 31 | // 1. Each type (class) is a predicate with a single variable as input |
34 | for (type : types) { | 32 | for (type : types) { |
35 | val typePred = createVLSFunction => [ | 33 | val typePred = createVLSFunction => [ |
36 | it.constant = support.toIDMultiple("t", type.name) | 34 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) |
37 | it.terms += support.duplicate(variable) | 35 | it.terms += support.duplicate(variable) |
38 | ] | 36 | ] |
39 | typeTrace.type2Predicate.put(type, typePred) | 37 | // typeTrace.type2Predicate.put(type, typePred) |
38 | trace.type2Predicate.put(type, typePred) | ||
40 | } | 39 | } |
41 | 40 | ||
42 | // 2. Map each ENUM type definition to fof formula | 41 | // 2. Map each ENUM type definition to fof formula |
@@ -44,15 +43,16 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp | |||
44 | val List<VLSFunction> orElems = newArrayList | 43 | val List<VLSFunction> orElems = newArrayList |
45 | for (e : type.elements) { | 44 | for (e : type.elements) { |
46 | val enumElemPred = createVLSFunction => [ | 45 | val enumElemPred = createVLSFunction => [ |
47 | it.constant = support.toIDMultiple("e", e.name, type.name) | 46 | it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2)) |
48 | it.terms += support.duplicate(variable) | 47 | it.terms += support.duplicate(variable) |
49 | ] | 48 | ] |
50 | typeTrace.element2Predicate.put(e, enumElemPred) | 49 | // typeTrace.element2Predicate.put(e, enumElemPred) |
50 | trace.element2Predicate.put(e, enumElemPred) | ||
51 | orElems.add(enumElemPred) | 51 | orElems.add(enumElemPred) |
52 | } | 52 | } |
53 | 53 | ||
54 | val res = createVLSFofFormula => [ | 54 | val res = createVLSFofFormula => [ |
55 | it.name = support.toIDMultiple("typeDef", type.name) | 55 | it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) |
56 | // below is temporary solution | 56 | // below is temporary solution |
57 | it.fofRole = "axiom" | 57 | it.fofRole = "axiom" |
58 | it.fofFormula = createVLSUniversalQuantifier => [ | 58 | it.fofFormula = createVLSUniversalQuantifier => [ |
@@ -62,7 +62,8 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp | |||
62 | // it.constant = type.lookup(typeTrace.type2Predicate).constant | 62 | // it.constant = type.lookup(typeTrace.type2Predicate).constant |
63 | // it.terms += createVLSVariable => [it.name = "A"] | 63 | // it.terms += createVLSVariable => [it.name = "A"] |
64 | // ] | 64 | // ] |
65 | it.left = type.lookup(typeTrace.type2Predicate) | 65 | // it.left = type.lookup(typeTrace.type2Predicate) |
66 | it.left = type.lookup(trace.type2Predicate) | ||
66 | 67 | ||
67 | it.right = support.unfoldOr(orElems) | 68 | it.right = support.unfoldOr(orElems) |
68 | 69 | ||
@@ -92,31 +93,23 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp | |||
92 | for (t1 : types.filter[!isIsAbstract]) { | 93 | for (t1 : types.filter[!isIsAbstract]) { |
93 | for (t2 : types) { | 94 | for (t2 : types) { |
94 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes | 95 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes |
95 | if (t1 == t2 || dfsSupertypeCheck(t1, t2)) { | 96 | if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { |
96 | typeTrace.type2PossibleNot.put(t2, createVLSFunction => [ | 97 | // typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate))) |
97 | it.constant = t2.lookup(typeTrace.type2Predicate).constant | 98 | trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) |
98 | it.terms += support.duplicate(variable) | ||
99 | ]) | ||
100 | } else { | 99 | } else { |
101 | typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ | 100 | // typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ |
102 | it.operand = createVLSFunction => [ | 101 | trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ |
103 | it.constant = t2.lookup(typeTrace.type2Predicate).constant | 102 | it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) |
104 | it.terms += support.duplicate(variable) | ||
105 | ] | ||
106 | ]) | 103 | ]) |
107 | } | 104 | } |
108 | // typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate)) | ||
109 | } | 105 | } |
110 | typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values))) | 106 | // typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values))) |
111 | // typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) ) | 107 | // typeTrace.type2PossibleNot.clear |
112 | typeTrace.type2PossibleNot.clear | 108 | trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values))) |
109 | trace.type2PossibleNot.clear | ||
113 | } | 110 | } |
114 | 111 | ||
115 | // 5. create fof function that is an or with all the elements in map | 112 | // 5. create fof function that is an or with all the elements in map |
116 | |||
117 | |||
118 | |||
119 | |||
120 | val hierarch = createVLSFofFormula => [ | 113 | val hierarch = createVLSFofFormula => [ |
121 | it.name = "hierarchyHandler" | 114 | it.name = "hierarchyHandler" |
122 | it.fofRole = "axiom" | 115 | it.fofRole = "axiom" |
@@ -124,7 +117,8 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp | |||
124 | it.variables += support.duplicate(variable) | 117 | it.variables += support.duplicate(variable) |
125 | it.operand = createVLSEquivalent => [ | 118 | it.operand = createVLSEquivalent => [ |
126 | it.left = support.topLevelTypeFunc | 119 | it.left = support.topLevelTypeFunc |
127 | it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values)) | 120 | // it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values)) |
121 | it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values)) | ||
128 | ] | 122 | ] |
129 | ] | 123 | ] |
130 | ] | 124 | ] |
@@ -133,21 +127,6 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp | |||
133 | 127 | ||
134 | } | 128 | } |
135 | 129 | ||
136 | def boolean dfsSupertypeCheck(Type type, Type type2) { | ||
137 | // There is surely a better way to do this | ||
138 | if (type.supertypes.isEmpty) | ||
139 | return false | ||
140 | else { | ||
141 | if (type.supertypes.contains(type2)) | ||
142 | return true | ||
143 | else { | ||
144 | for (supertype : type.supertypes) { | ||
145 | if(dfsSupertypeCheck(supertype, type2)) return true | ||
146 | } | ||
147 | } | ||
148 | } | ||
149 | } | ||
150 | |||
151 | override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, | 130 | override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, |
152 | Logic2VampireLanguageMapperTrace trace) { | 131 | Logic2VampireLanguageMapperTrace trace) { |
153 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 132 | throw new UnsupportedOperationException("TODO: auto-generated method stub") |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 4a4eedf5..bda7463e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin | |||
Binary files differ | |||
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 55f0ac1e..a062fcec 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 e91f89cc..5fc0da27 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 154ff393..562b9bbf 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 5d6ad730..dd7bdf86 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_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 7c787543..496d27b3 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 34f3b285..4a03f2ce 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 f8d6cd3f..511f4a1f 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 7b2b11f8..37e9480c 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/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin index 7e8336e2..f473c4bc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.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_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin index a2229dba..e53791d6 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index d82649ff..1b112c56 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.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/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 030a0be9..c8284658 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.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/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 87203ed8..89d4c657 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.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/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 65689b0c..3c98bd64 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.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 855815f8..2b491209 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 | |||
@@ -8,8 +8,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | |||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
14 | import java.util.HashMap; | 16 | import java.util.HashMap; |
15 | import java.util.Map; | 17 | import java.util.Map; |
@@ -24,10 +26,20 @@ public class Logic2VampireLanguageMapperTrace { | |||
24 | 26 | ||
25 | public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; | 27 | public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; |
26 | 28 | ||
29 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); | ||
30 | |||
31 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); | ||
32 | |||
33 | public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>(); | ||
34 | |||
35 | public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>(); | ||
36 | |||
27 | public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions; | 37 | public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions; |
28 | 38 | ||
29 | public Map<RelationDeclaration, RelationDefinition> relationDefinitions; | 39 | public Map<RelationDeclaration, RelationDefinition> relationDefinitions; |
30 | 40 | ||
41 | public Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap<RelationDeclaration, VLSFunction>(); | ||
42 | |||
31 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | 43 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); |
32 | 44 | ||
33 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); | 45 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java index bce50fcc..4f5c6acc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | |||
@@ -15,6 +15,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | |||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
20 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 21 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
@@ -44,17 +45,84 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
44 | this.base = base; | 45 | this.base = base; |
45 | } | 46 | } |
46 | 47 | ||
47 | public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace) { | 48 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { |
49 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); | ||
50 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
51 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
52 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
53 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
54 | for (final Integer i : _doubleDotLessThan) { | ||
55 | { | ||
56 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
57 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
58 | it.setName(this.support.toIDMultiple("V", i.toString())); | ||
59 | }; | ||
60 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
61 | relVar2VLS.add(v); | ||
62 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
63 | final Type relType = ((ComplexTypeReference) _get).getReferred(); | ||
64 | final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v); | ||
65 | relVar2TypeDecComply.add(varTypeComply); | ||
66 | } | ||
67 | } | ||
68 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
69 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
70 | final String[] nameArray = r.getName().split(" "); | ||
71 | it.setName(this.support.toIDMultiple("compliance", nameArray[0], | ||
72 | nameArray[2])); | ||
73 | it.setFofRole("axiom"); | ||
74 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
75 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
76 | for (final VLSVariable v : relVar2VLS) { | ||
77 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
78 | VLSVariable _duplicate = this.support.duplicate(v); | ||
79 | _variables.add(_duplicate); | ||
80 | } | ||
81 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
82 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
83 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
84 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
85 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | ||
86 | int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
87 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); | ||
88 | for (final Integer i_1 : _doubleDotLessThan_1) { | ||
89 | { | ||
90 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
91 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
92 | it_4.setName(relVar2VLS.get((i_1).intValue()).getName()); | ||
93 | }; | ||
94 | final VLSVariable v_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
95 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
96 | _terms.add(v_1); | ||
97 | } | ||
98 | } | ||
99 | }; | ||
100 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
101 | it_2.setLeft(_doubleArrow); | ||
102 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); | ||
103 | }; | ||
104 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
105 | it_1.setOperand(_doubleArrow); | ||
106 | }; | ||
107 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
108 | it.setFofFormula(_doubleArrow); | ||
109 | }; | ||
110 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
111 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
112 | _formulas.add(comply); | ||
113 | } | ||
114 | |||
115 | public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { | ||
48 | final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | 116 | final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); |
49 | final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>(); | 117 | final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>(); |
50 | final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>(); | 118 | final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>(); |
51 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | 119 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); |
52 | EList<Variable> _variables = r.getVariables(); | 120 | EList<Variable> _variables = reldef.getVariables(); |
53 | for (final Variable variable : _variables) { | 121 | for (final Variable variable : _variables) { |
54 | { | 122 | { |
55 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 123 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
56 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | 124 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { |
57 | it.setName(this.support.toIDMultiple("Var", variable.getName())); | 125 | it.setName(this.support.toIDMultiple("V", variable.getName())); |
58 | }; | 126 | }; |
59 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | 127 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); |
60 | relationVar2VLS.put(variable, v); | 128 | relationVar2VLS.put(variable, v); |
@@ -63,56 +131,39 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
63 | TypeReference _range = variable.getRange(); | 131 | TypeReference _range = variable.getRange(); |
64 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | 132 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); |
65 | EList<VLSTerm> _terms = it.getTerms(); | 133 | EList<VLSTerm> _terms = it.getTerms(); |
66 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 134 | VLSVariable _duplicate = this.support.duplicate(v); |
67 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 135 | _terms.add(_duplicate); |
68 | it_1.setName(this.support.toIDMultiple("Var", variable.getName())); | ||
69 | }; | ||
70 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
71 | _terms.add(_doubleArrow); | ||
72 | }; | 136 | }; |
73 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 137 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); |
74 | relationVar2TypeDecComply.put(variable, varTypeComply); | 138 | relationVar2TypeDecComply.put(variable, varTypeComply); |
75 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); | 139 | relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); |
76 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { | ||
77 | TypeReference _range = variable.getRange(); | ||
78 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | ||
79 | EList<VLSTerm> _terms = it.getTerms(); | ||
80 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
81 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> { | ||
82 | it_1.setName(this.support.toIDMultiple("Var", variable.getName())); | ||
83 | }; | ||
84 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3); | ||
85 | _terms.add(_doubleArrow); | ||
86 | }; | ||
87 | final VLSFunction varTypeRes = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_2); | ||
88 | relationVar2TypeDecRes.put(variable, varTypeRes); | ||
89 | } | 140 | } |
90 | } | 141 | } |
91 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 142 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
92 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 143 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
93 | it.setName(this.support.toIDMultiple("compliance", r.getName())); | 144 | final String[] nameArray = reldef.getName().split(" "); |
145 | int _length = nameArray.length; | ||
146 | int _minus = (_length - 2); | ||
147 | int _length_1 = nameArray.length; | ||
148 | int _minus_1 = (_length_1 - 1); | ||
149 | it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], | ||
150 | nameArray[_minus_1])); | ||
94 | it.setFofRole("axiom"); | 151 | it.setFofRole("axiom"); |
95 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 152 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
96 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | 153 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { |
97 | EList<Variable> _variables_1 = r.getVariables(); | 154 | EList<Variable> _variables_1 = reldef.getVariables(); |
98 | for (final Variable variable_1 : _variables_1) { | 155 | for (final Variable variable_1 : _variables_1) { |
99 | { | 156 | EList<VLSVariable> _variables_2 = it_1.getVariables(); |
100 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 157 | VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS)); |
101 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> { | 158 | _variables_2.add(_duplicate); |
102 | it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName()); | ||
103 | }; | ||
104 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
105 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
106 | _variables_2.add(v); | ||
107 | } | ||
108 | } | 159 | } |
109 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 160 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
110 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | 161 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { |
111 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 162 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
112 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | 163 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { |
113 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | 164 | it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName())); |
114 | EList<Variable> _variables_2 = r.getVariables(); | 165 | EList<Variable> _variables_3 = reldef.getVariables(); |
115 | for (final Variable variable_2 : _variables_2) { | 166 | for (final Variable variable_2 : _variables_3) { |
116 | { | 167 | { |
117 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 168 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
118 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | 169 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { |
@@ -139,11 +190,11 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
139 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 190 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); |
140 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 191 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
141 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 192 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
142 | it.setName(this.support.toIDMultiple("relation", r.getName())); | 193 | it.setName(this.support.toIDMultiple("relation", reldef.getName())); |
143 | it.setFofRole("axiom"); | 194 | it.setFofRole("axiom"); |
144 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 195 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
145 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 196 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
146 | EList<Variable> _variables_1 = r.getVariables(); | 197 | EList<Variable> _variables_1 = reldef.getVariables(); |
147 | for (final Variable variable_1 : _variables_1) { | 198 | for (final Variable variable_1 : _variables_1) { |
148 | { | 199 | { |
149 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 200 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
@@ -164,8 +215,8 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
164 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> { | 215 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> { |
165 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 216 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
166 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> { | 217 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> { |
167 | it_4.setConstant(this.support.toIDMultiple("rel", r.getName())); | 218 | it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName())); |
168 | EList<Variable> _variables_2 = r.getVariables(); | 219 | EList<Variable> _variables_2 = reldef.getVariables(); |
169 | for (final Variable variable_2 : _variables_2) { | 220 | for (final Variable variable_2 : _variables_2) { |
170 | { | 221 | { |
171 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 222 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
@@ -180,7 +231,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
180 | }; | 231 | }; |
181 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | 232 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); |
182 | it_3.setLeft(_doubleArrow); | 233 | it_3.setLeft(_doubleArrow); |
183 | it_3.setRight(this.base.transformTerm(r.getValue(), trace, relationVar2VLS)); | 234 | it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS)); |
184 | }; | 235 | }; |
185 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | 236 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); |
186 | it_2.setRight(_doubleArrow); | 237 | it_2.setRight(_doubleArrow); |
@@ -198,89 +249,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
198 | _formulas_1.add(res); | 249 | _formulas_1.add(res); |
199 | } | 250 | } |
200 | 251 | ||
201 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { | ||
202 | final List<VLSVariable> relationVar2VLS = new ArrayList<VLSVariable>(); | ||
203 | final List<VLSFunction> relationVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
204 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
205 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
206 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
207 | for (final Integer i : _doubleDotLessThan) { | ||
208 | { | ||
209 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
210 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
211 | it.setName(this.support.toIDMultiple("Var", i.toString())); | ||
212 | }; | ||
213 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
214 | relationVar2VLS.add(v); | ||
215 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
216 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
217 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
218 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _get).getReferred().getName())); | ||
219 | EList<VLSTerm> _terms = it.getTerms(); | ||
220 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
221 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
222 | it_1.setName(this.support.toIDMultiple("Var", i.toString())); | ||
223 | }; | ||
224 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
225 | _terms.add(_doubleArrow); | ||
226 | }; | ||
227 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
228 | relationVar2TypeDecComply.add(varTypeComply); | ||
229 | } | ||
230 | } | ||
231 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
232 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
233 | it.setName(this.support.toIDMultiple("compliance", r.getName())); | ||
234 | it.setFofRole("axiom"); | ||
235 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
236 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
237 | int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
238 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); | ||
239 | for (final Integer i_1 : _doubleDotLessThan_1) { | ||
240 | { | ||
241 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
242 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> { | ||
243 | it_2.setName(relationVar2VLS.get((i_1).intValue()).getName()); | ||
244 | }; | ||
245 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
246 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
247 | _variables.add(v); | ||
248 | } | ||
249 | } | ||
250 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
251 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
252 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
253 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
254 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | ||
255 | int _length_2 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
256 | ExclusiveRange _doubleDotLessThan_2 = new ExclusiveRange(0, _length_2, true); | ||
257 | for (final Integer i_2 : _doubleDotLessThan_2) { | ||
258 | { | ||
259 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
260 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
261 | it_4.setName(relationVar2VLS.get((i_2).intValue()).getName()); | ||
262 | }; | ||
263 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
264 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
265 | _terms.add(v); | ||
266 | } | ||
267 | } | ||
268 | }; | ||
269 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
270 | it_2.setLeft(_doubleArrow); | ||
271 | it_2.setRight(this.support.unfoldAnd(relationVar2TypeDecComply)); | ||
272 | }; | ||
273 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
274 | it_1.setOperand(_doubleArrow); | ||
275 | }; | ||
276 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
277 | it.setFofFormula(_doubleArrow); | ||
278 | }; | ||
279 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
280 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
281 | _formulas.add(comply); | ||
282 | } | ||
283 | |||
284 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { | 252 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { |
285 | if (r instanceof RelationDeclaration) { | 253 | if (r instanceof RelationDeclaration) { |
286 | _transformRelation((RelationDeclaration)r, trace); | 254 | _transformRelation((RelationDeclaration)r, trace); |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index dfe624be..35497eab 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |||
@@ -17,6 +17,7 @@ import com.google.common.collect.Iterables; | |||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
22 | import java.util.ArrayList; | 23 | import java.util.ArrayList; |
@@ -52,14 +53,39 @@ public class Logic2VampireLanguageMapper_Support { | |||
52 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_"); | 53 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_"); |
53 | } | 54 | } |
54 | 55 | ||
55 | protected VLSVariable duplicate(final VLSVariable vrbl) { | 56 | protected VLSVariable duplicate(final VLSVariable term) { |
56 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 57 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
57 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | 58 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { |
58 | it.setName(vrbl.getName()); | 59 | it.setName(term.getName()); |
59 | }; | 60 | }; |
60 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | 61 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); |
61 | } | 62 | } |
62 | 63 | ||
64 | protected VLSFunction duplicate(final VLSFunction term) { | ||
65 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
66 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
67 | it.setConstant(term.getConstant()); | ||
68 | EList<VLSTerm> _terms = term.getTerms(); | ||
69 | for (final VLSTerm v : _terms) { | ||
70 | EList<VLSTerm> _terms_1 = it.getTerms(); | ||
71 | VLSVariable _duplicate = this.duplicate(((VLSVariable) v)); | ||
72 | _terms_1.add(_duplicate); | ||
73 | } | ||
74 | }; | ||
75 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
76 | } | ||
77 | |||
78 | protected VLSFunction duplicate(final VLSFunction term, final VLSVariable v) { | ||
79 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
80 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
81 | it.setConstant(term.getConstant()); | ||
82 | EList<VLSTerm> _terms = it.getTerms(); | ||
83 | VLSVariable _duplicate = this.duplicate(v); | ||
84 | _terms.add(_duplicate); | ||
85 | }; | ||
86 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
87 | } | ||
88 | |||
63 | protected VLSFunction topLevelTypeFunc() { | 89 | protected VLSFunction topLevelTypeFunc() { |
64 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 90 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
65 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 91 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
@@ -287,6 +313,30 @@ public class Logic2VampireLanguageMapper_Support { | |||
287 | return _xblockexpression; | 313 | return _xblockexpression; |
288 | } | 314 | } |
289 | 315 | ||
316 | protected boolean dfsSupertypeCheck(final Type type, final Type type2) { | ||
317 | boolean _xifexpression = false; | ||
318 | boolean _isEmpty = type.getSupertypes().isEmpty(); | ||
319 | if (_isEmpty) { | ||
320 | return false; | ||
321 | } else { | ||
322 | boolean _xifexpression_1 = false; | ||
323 | boolean _contains = type.getSupertypes().contains(type2); | ||
324 | if (_contains) { | ||
325 | return true; | ||
326 | } else { | ||
327 | EList<Type> _supertypes = type.getSupertypes(); | ||
328 | for (final Type supertype : _supertypes) { | ||
329 | boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2); | ||
330 | if (_dfsSupertypeCheck) { | ||
331 | return true; | ||
332 | } | ||
333 | } | ||
334 | } | ||
335 | _xifexpression = _xifexpression_1; | ||
336 | } | ||
337 | return _xifexpression; | ||
338 | } | ||
339 | |||
290 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { | 340 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { |
291 | HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1); | 341 | HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1); |
292 | final Procedure1<HashMap<Variable, VLSVariable>> _function = (HashMap<Variable, VLSVariable> it) -> { | 342 | final Procedure1<HashMap<Variable, VLSVariable>> _function = (HashMap<Variable, VLSVariable> it) -> { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java index 1e845d94..b582fb96 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java | |||
@@ -4,7 +4,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage | |||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; | 7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; |
@@ -46,8 +45,6 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
46 | 45 | ||
47 | @Override | 46 | @Override |
48 | public void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | 47 | public void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { |
49 | final Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes(); | ||
50 | trace.typeMapperTrace = typeTrace; | ||
51 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 48 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
52 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | 49 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { |
53 | it.setName("A"); | 50 | it.setName("A"); |
@@ -57,13 +54,13 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
57 | { | 54 | { |
58 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 55 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
59 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 56 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
60 | it.setConstant(this.support.toIDMultiple("t", type.getName())); | 57 | it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); |
61 | EList<VLSTerm> _terms = it.getTerms(); | 58 | EList<VLSTerm> _terms = it.getTerms(); |
62 | VLSVariable _duplicate = this.support.duplicate(variable); | 59 | VLSVariable _duplicate = this.support.duplicate(variable); |
63 | _terms.add(_duplicate); | 60 | _terms.add(_duplicate); |
64 | }; | 61 | }; |
65 | final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 62 | final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); |
66 | typeTrace.type2Predicate.put(type, typePred); | 63 | trace.type2Predicate.put(type, typePred); |
67 | } | 64 | } |
68 | } | 65 | } |
69 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); | 66 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); |
@@ -75,19 +72,19 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
75 | { | 72 | { |
76 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 73 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
77 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 74 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
78 | it.setConstant(this.support.toIDMultiple("e", e.getName(), type_1.getName())); | 75 | it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2])); |
79 | EList<VLSTerm> _terms = it.getTerms(); | 76 | EList<VLSTerm> _terms = it.getTerms(); |
80 | VLSVariable _duplicate = this.support.duplicate(variable); | 77 | VLSVariable _duplicate = this.support.duplicate(variable); |
81 | _terms.add(_duplicate); | 78 | _terms.add(_duplicate); |
82 | }; | 79 | }; |
83 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 80 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); |
84 | typeTrace.element2Predicate.put(e, enumElemPred); | 81 | trace.element2Predicate.put(e, enumElemPred); |
85 | orElems.add(enumElemPred); | 82 | orElems.add(enumElemPred); |
86 | } | 83 | } |
87 | } | 84 | } |
88 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 85 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
89 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 86 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
90 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName())); | 87 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); |
91 | it.setFofRole("axiom"); | 88 | it.setFofRole("axiom"); |
92 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 89 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
93 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 90 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
@@ -96,7 +93,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
96 | _variables.add(_duplicate); | 93 | _variables.add(_duplicate); |
97 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 94 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
98 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | 95 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { |
99 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate)); | 96 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); |
100 | it_2.setRight(this.support.unfoldOr(orElems)); | 97 | it_2.setRight(this.support.unfoldOr(orElems)); |
101 | }; | 98 | }; |
102 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | 99 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); |
@@ -118,37 +115,21 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
118 | for (final Type t1 : _filter_1) { | 115 | for (final Type t1 : _filter_1) { |
119 | { | 116 | { |
120 | for (final Type t2 : types) { | 117 | for (final Type t2 : types) { |
121 | if ((Objects.equal(t1, t2) || this.dfsSupertypeCheck(t1, t2))) { | 118 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { |
122 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 119 | trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); |
123 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { | ||
124 | it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(t2, typeTrace.type2Predicate).getConstant()); | ||
125 | EList<VLSTerm> _terms = it.getTerms(); | ||
126 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
127 | _terms.add(_duplicate); | ||
128 | }; | ||
129 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2); | ||
130 | typeTrace.type2PossibleNot.put(t2, _doubleArrow); | ||
131 | } else { | 120 | } else { |
132 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 121 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); |
133 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { | 122 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { |
134 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); | 123 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); |
135 | final Procedure1<VLSFunction> _function_4 = (VLSFunction it_1) -> { | ||
136 | it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(t2, typeTrace.type2Predicate).getConstant()); | ||
137 | EList<VLSTerm> _terms = it_1.getTerms(); | ||
138 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
139 | _terms.add(_duplicate); | ||
140 | }; | ||
141 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_4); | ||
142 | it.setOperand(_doubleArrow_1); | ||
143 | }; | 124 | }; |
144 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); | 125 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); |
145 | typeTrace.type2PossibleNot.put(t2, _doubleArrow_1); | 126 | trace.type2PossibleNot.put(t2, _doubleArrow); |
146 | } | 127 | } |
147 | } | 128 | } |
148 | Collection<VLSTerm> _values = typeTrace.type2PossibleNot.values(); | 129 | Collection<VLSTerm> _values = trace.type2PossibleNot.values(); |
149 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | 130 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); |
150 | typeTrace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); | 131 | trace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); |
151 | typeTrace.type2PossibleNot.clear(); | 132 | trace.type2PossibleNot.clear(); |
152 | } | 133 | } |
153 | } | 134 | } |
154 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 135 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
@@ -163,7 +144,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
163 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 144 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
164 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | 145 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { |
165 | it_2.setLeft(this.support.topLevelTypeFunc()); | 146 | it_2.setLeft(this.support.topLevelTypeFunc()); |
166 | Collection<VLSTerm> _values = typeTrace.type2And.values(); | 147 | Collection<VLSTerm> _values = trace.type2And.values(); |
167 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | 148 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); |
168 | it_2.setRight(this.support.unfoldOr(_arrayList)); | 149 | it_2.setRight(this.support.unfoldOr(_arrayList)); |
169 | }; | 150 | }; |
@@ -178,30 +159,6 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
178 | _formulas.add(hierarch); | 159 | _formulas.add(hierarch); |
179 | } | 160 | } |
180 | 161 | ||
181 | public boolean dfsSupertypeCheck(final Type type, final Type type2) { | ||
182 | boolean _xifexpression = false; | ||
183 | boolean _isEmpty = type.getSupertypes().isEmpty(); | ||
184 | if (_isEmpty) { | ||
185 | return false; | ||
186 | } else { | ||
187 | boolean _xifexpression_1 = false; | ||
188 | boolean _contains = type.getSupertypes().contains(type2); | ||
189 | if (_contains) { | ||
190 | return true; | ||
191 | } else { | ||
192 | EList<Type> _supertypes = type.getSupertypes(); | ||
193 | for (final Type supertype : _supertypes) { | ||
194 | boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2); | ||
195 | if (_dfsSupertypeCheck) { | ||
196 | return true; | ||
197 | } | ||
198 | } | ||
199 | } | ||
200 | _xifexpression = _xifexpression_1; | ||
201 | } | ||
202 | return _xifexpression; | ||
203 | } | ||
204 | |||
205 | @Override | 162 | @Override |
206 | public List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | 163 | public List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { |
207 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | 164 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); |