diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | 167 |
1 files changed, 130 insertions, 37 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 8c0ae38d..7bc70e9d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | |||
@@ -10,9 +10,12 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | |||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
18 | import com.google.common.base.Objects; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; |
@@ -21,9 +24,13 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | |||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; |
22 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 25 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
23 | import java.util.ArrayList; | 26 | import java.util.ArrayList; |
27 | import java.util.HashMap; | ||
24 | import java.util.List; | 28 | import java.util.List; |
29 | import java.util.Map; | ||
30 | import java.util.Set; | ||
25 | import org.eclipse.emf.common.util.EList; | 31 | import org.eclipse.emf.common.util.EList; |
26 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 32 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
33 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
27 | import org.eclipse.xtext.xbase.lib.Extension; | 34 | import org.eclipse.xtext.xbase.lib.Extension; |
28 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 35 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
29 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 36 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
@@ -107,69 +114,155 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
107 | it.setName("B"); | 114 | it.setName("B"); |
108 | }; | 115 | }; |
109 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | 116 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); |
117 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
118 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it) -> { | ||
119 | it.setName("C"); | ||
120 | }; | ||
121 | final VLSVariable varC = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_3); | ||
110 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); | 122 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); |
123 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); | ||
111 | for (final Relation l_1 : relationsList) { | 124 | for (final Relation l_1 : relationsList) { |
112 | { | 125 | { |
113 | final String relName = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString(); | 126 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList); |
114 | TypeReference _get = l_1.getParameters().get(0); | 127 | TypeReference _get = l_1.getParameters().get(1); |
115 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | 128 | Type _referred = ((ComplexTypeReference) _get).getReferred(); |
116 | final Type fromType = ((Type) _referred); | 129 | final Type toType = ((Type) _referred); |
117 | TypeReference _get_1 = l_1.getParameters().get(1); | 130 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); |
118 | Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred(); | 131 | this.addToMap(type2cont, toFunc, rel); |
119 | final Type toType = ((Type) _referred_1); | 132 | EList<Type> _subtypes = toType.getSubtypes(); |
120 | final ArrayList<VLSFunction> listForAnd = CollectionLiterals.<VLSFunction>newArrayList(); | 133 | for (final Type c : _subtypes) { |
121 | listForAnd.add(this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList)); | 134 | this.addToMap(type2cont, toFunc, rel); |
135 | } | ||
136 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
137 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
138 | it.setName(this.support.toIDMultiple("noDupCont", rel.getConstant().toString())); | ||
139 | it.setFofRole("axiom"); | ||
140 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
141 | final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> { | ||
142 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
143 | VLSVariable _duplicate = this.support.duplicate(varA); | ||
144 | _variables.add(_duplicate); | ||
145 | EList<VLSVariable> _variables_1 = it_1.getVariables(); | ||
146 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | ||
147 | _variables_1.add(_duplicate_1); | ||
148 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
149 | final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> { | ||
150 | it_2.setLeft(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varA, varB))); | ||
151 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
152 | final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> { | ||
153 | VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier(); | ||
154 | final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> { | ||
155 | EList<VLSVariable> _variables_2 = it_4.getVariables(); | ||
156 | VLSVariable _duplicate_2 = this.support.duplicate(varC); | ||
157 | _variables_2.add(_duplicate_2); | ||
158 | EList<VLSVariable> _variables_3 = it_4.getVariables(); | ||
159 | VLSVariable _duplicate_3 = this.support.duplicate(varB); | ||
160 | _variables_3.add(_duplicate_3); | ||
161 | it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB))); | ||
162 | }; | ||
163 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier_1, _function_8); | ||
164 | it_3.setOperand(_doubleArrow); | ||
165 | }; | ||
166 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_7); | ||
167 | it_2.setRight(_doubleArrow); | ||
168 | }; | ||
169 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6); | ||
170 | it_1.setOperand(_doubleArrow); | ||
171 | }; | ||
172 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_5); | ||
173 | it.setFofFormula(_doubleArrow); | ||
174 | }; | ||
175 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); | ||
176 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
177 | _formulas_1.add(relFormula); | ||
178 | } | ||
179 | } | ||
180 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); | ||
181 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { | ||
182 | { | ||
122 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 183 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
123 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 184 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
124 | it.setName(this.support.toIDMultiple("containment", relName)); | 185 | it.setName(this.support.toIDMultiple("containment", e.getKey().getConstant().toString())); |
125 | it.setFofRole("axiom"); | 186 | it.setFofRole("axiom"); |
126 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 187 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
127 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | 188 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
128 | EList<VLSVariable> _variables = it_1.getVariables(); | 189 | EList<VLSVariable> _variables = it_1.getVariables(); |
129 | VLSVariable _duplicate = this.support.duplicate(varA); | 190 | VLSVariable _duplicate = this.support.duplicate(varA); |
130 | _variables.add(_duplicate); | 191 | _variables.add(_duplicate); |
131 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 192 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
132 | final Procedure1<VLSImplies> _function_5 = (VLSImplies it_2) -> { | 193 | final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> { |
133 | it_2.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate), varA)); | 194 | it_2.setLeft(this.support.duplicate(e.getKey(), varA)); |
134 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | 195 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); |
135 | final Procedure1<VLSExistentialQuantifier> _function_6 = (VLSExistentialQuantifier it_3) -> { | 196 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> { |
136 | EList<VLSVariable> _variables_1 = it_3.getVariables(); | 197 | EList<VLSVariable> _variables_1 = it_3.getVariables(); |
137 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | 198 | VLSVariable _duplicate_1 = this.support.duplicate(varB); |
138 | _variables_1.add(_duplicate_1); | 199 | _variables_1.add(_duplicate_1); |
139 | it_3.setOperand(this.support.unfoldAnd(listForAnd)); | 200 | int _length = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; |
201 | boolean _greaterThan = (_length > 1); | ||
202 | if (_greaterThan) { | ||
203 | it_3.setOperand(this.makeUnique(e.getValue())); | ||
204 | } else { | ||
205 | it_3.setOperand(e.getValue().get(0)); | ||
206 | } | ||
140 | }; | 207 | }; |
141 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_6); | 208 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); |
142 | it_2.setRight(_doubleArrow); | 209 | it_2.setRight(_doubleArrow); |
143 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
144 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { | ||
145 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
146 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
147 | final Procedure1<VLSConstant> _function_8 = (VLSConstant it_4) -> { | ||
148 | it_4.setName("o1"); | ||
149 | }; | ||
150 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_8); | ||
151 | it_3.setRight(_doubleArrow_1); | ||
152 | }; | ||
153 | ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); | ||
154 | }; | 210 | }; |
155 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_5); | 211 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6); |
156 | it_1.setOperand(_doubleArrow); | 212 | it_1.setOperand(_doubleArrow); |
157 | }; | 213 | }; |
158 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | 214 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); |
159 | it.setFofFormula(_doubleArrow); | 215 | it.setFofFormula(_doubleArrow); |
160 | }; | 216 | }; |
161 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | 217 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); |
162 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | 218 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
163 | _formulas_1.add(relFormula); | 219 | _formulas_1.add(relFormula); |
164 | TypeReference _get_2 = l_1.getParameters().get(1); | 220 | } |
165 | Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred(); | 221 | } |
166 | Type pointingTo = ((Type) _referred_2); | 222 | } |
167 | containmentListCopy.remove(pointingTo); | 223 | |
168 | EList<Type> _subtypes = pointingTo.getSubtypes(); | 224 | protected VLSTerm makeUnique(final List<VLSFunction> list) { |
169 | for (final Type c : _subtypes) { | 225 | final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList(); |
170 | containmentListCopy.remove(c); | 226 | final List<VLSTerm> uniqueRels = CollectionLiterals.<VLSTerm>newArrayList(); |
227 | for (final VLSFunction t1 : list) { | ||
228 | { | ||
229 | for (final VLSFunction t2 : list) { | ||
230 | boolean _equals = Objects.equal(t1, t2); | ||
231 | if (_equals) { | ||
232 | final VLSFunction fct = this.support.duplicate(t2); | ||
233 | possibleNots.add(fct); | ||
234 | } else { | ||
235 | final VLSFunction op = this.support.duplicate(t2); | ||
236 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
237 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { | ||
238 | it.setOperand(op); | ||
239 | }; | ||
240 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function); | ||
241 | possibleNots.add(negFct); | ||
242 | } | ||
171 | } | 243 | } |
244 | uniqueRels.add(this.support.unfoldAnd(possibleNots)); | ||
245 | possibleNots.clear(); | ||
246 | } | ||
247 | } | ||
248 | return this.support.unfoldOr(uniqueRels); | ||
249 | } | ||
250 | |||
251 | protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) { | ||
252 | Object _xifexpression = null; | ||
253 | boolean _containsKey = type2cont.containsKey(toFunc); | ||
254 | boolean _not = (!_containsKey); | ||
255 | if (_not) { | ||
256 | _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel)); | ||
257 | } else { | ||
258 | boolean _xifexpression_1 = false; | ||
259 | boolean _contains = type2cont.get(toFunc).contains(rel); | ||
260 | boolean _not_1 = (!_contains); | ||
261 | if (_not_1) { | ||
262 | _xifexpression_1 = type2cont.get(toFunc).add(rel); | ||
172 | } | 263 | } |
264 | _xifexpression = Boolean.valueOf(_xifexpression_1); | ||
173 | } | 265 | } |
266 | return _xifexpression; | ||
174 | } | 267 | } |
175 | } | 268 | } |