aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
diff options
context:
space:
mode:
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.java180
1 files changed, 180 insertions, 0 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
new file mode 100644
index 00000000..da0e5615
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
@@ -0,0 +1,180 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
16import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
22import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy;
23import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
24import java.util.ArrayList;
25import java.util.List;
26import org.eclipse.emf.common.util.EList;
27import org.eclipse.xtext.xbase.lib.CollectionLiterals;
28import org.eclipse.xtext.xbase.lib.Extension;
29import org.eclipse.xtext.xbase.lib.ObjectExtensions;
30import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
31
32@SuppressWarnings("all")
33public class Logic2VampireLanguageMapper_ContainmentMapper {
34 @Extension
35 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
36
37 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
38
39 private final Logic2VampireLanguageMapper base;
40
41 private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> {
42 it.setName("A");
43 }));
44
45 public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) {
46 this.base = base;
47 }
48
49 public void transformContainment(final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) {
50 final ContainmentHierarchy hierarchy = hierarchies.get(0);
51 final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy();
52 final EList<Relation> relationsList = hierarchy.getContainmentRelations();
53 for (final Relation l : relationsList) {
54 {
55 TypeReference _get = l.getParameters().get(1);
56 Type _referred = ((ComplexTypeReference) _get).getReferred();
57 Type pointingTo = ((Type) _referred);
58 containmentListCopy.remove(pointingTo);
59 EList<Type> _subtypes = pointingTo.getSubtypes();
60 for (final Type c : _subtypes) {
61 containmentListCopy.remove(c);
62 }
63 }
64 }
65 final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString();
66 final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate));
67 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
68 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
69 it.setName(this.support.toIDMultiple("containment_topLevel", topName));
70 it.setFofRole("axiom");
71 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
72 final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
73 EList<VLSVariable> _variables = it_1.getVariables();
74 VLSVariable _duplicate = this.support.duplicate(this.variable);
75 _variables.add(_duplicate);
76 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
77 final Procedure1<VLSEquivalent> _function_2 = (VLSEquivalent it_2) -> {
78 it_2.setLeft(topTerm);
79 VLSEquality _createVLSEquality = this.factory.createVLSEquality();
80 final Procedure1<VLSEquality> _function_3 = (VLSEquality it_3) -> {
81 it_3.setLeft(this.support.duplicate(this.variable));
82 VLSConstant _createVLSConstant = this.factory.createVLSConstant();
83 final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> {
84 it_4.setName("o1");
85 };
86 VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4);
87 it_3.setRight(_doubleArrow);
88 };
89 VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_3);
90 it_2.setRight(_doubleArrow);
91 };
92 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_2);
93 it_1.setOperand(_doubleArrow);
94 };
95 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
96 it.setFofFormula(_doubleArrow);
97 };
98 final VLSFofFormula contTop = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
99 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
100 _formulas.add(contTop);
101 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
102 final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> {
103 it.setName("A");
104 };
105 final VLSVariable varA = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);
106 VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
107 final Procedure1<VLSVariable> _function_2 = (VLSVariable it) -> {
108 it.setName("B");
109 };
110 final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);
111 final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA);
112 for (final Relation l_1 : relationsList) {
113 {
114 final String relName = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString();
115 TypeReference _get = l_1.getParameters().get(0);
116 Type _referred = ((ComplexTypeReference) _get).getReferred();
117 final Type fromType = ((Type) _referred);
118 TypeReference _get_1 = l_1.getParameters().get(1);
119 Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred();
120 final Type toType = ((Type) _referred_1);
121 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
122 final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> {
123 it.setName(this.support.toIDMultiple("containment", relName));
124 it.setFofRole("axiom");
125 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
126 final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> {
127 EList<VLSVariable> _variables = it_1.getVariables();
128 VLSVariable _duplicate = this.support.duplicate(varA);
129 _variables.add(_duplicate);
130 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
131 final Procedure1<VLSImplies> _function_5 = (VLSImplies it_2) -> {
132 it_2.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate), varA));
133 VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();
134 final Procedure1<VLSExistentialQuantifier> _function_6 = (VLSExistentialQuantifier it_3) -> {
135 EList<VLSVariable> _variables_1 = it_3.getVariables();
136 VLSVariable _duplicate_1 = this.support.duplicate(varB);
137 _variables_1.add(_duplicate_1);
138 VLSAnd _createVLSAnd = this.factory.createVLSAnd();
139 final Procedure1<VLSAnd> _function_7 = (VLSAnd it_4) -> {
140 it_4.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(fromType, trace.type2Predicate), varB));
141 it_4.setRight(this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList));
142 };
143 VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_7);
144 it_3.setOperand(_doubleArrow);
145 };
146 VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_6);
147 it_2.setRight(_doubleArrow);
148 VLSEquality _createVLSEquality = this.factory.createVLSEquality();
149 final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> {
150 it_3.setLeft(this.support.duplicate(this.variable));
151 VLSConstant _createVLSConstant = this.factory.createVLSConstant();
152 final Procedure1<VLSConstant> _function_8 = (VLSConstant it_4) -> {
153 it_4.setName("o1");
154 };
155 VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_8);
156 it_3.setRight(_doubleArrow_1);
157 };
158 ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7);
159 };
160 VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_5);
161 it_1.setOperand(_doubleArrow);
162 };
163 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4);
164 it.setFofFormula(_doubleArrow);
165 };
166 final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3);
167 EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
168 _formulas_1.add(relFormula);
169 TypeReference _get_2 = l_1.getParameters().get(1);
170 Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred();
171 Type pointingTo = ((Type) _referred_2);
172 containmentListCopy.remove(pointingTo);
173 EList<Type> _subtypes = pointingTo.getSubtypes();
174 for (final Type c : _subtypes) {
175 containmentListCopy.remove(c);
176 }
177 }
178 }
179 }
180}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 10:42:33 +0000