aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.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_TypeMapper_FilteredTypes.java')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java193
1 files changed, 0 insertions, 193 deletions
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
deleted file mode 100644
index b582fb96..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
+++ /dev/null
@@ -1,193 +0,0 @@
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.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper;
7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation;
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
16import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
17import com.google.common.base.Objects;
18import com.google.common.collect.Iterables;
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
22import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;
23import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
24import java.util.ArrayList;
25import java.util.Collection;
26import java.util.List;
27import org.eclipse.emf.common.util.EList;
28import org.eclipse.xtext.xbase.lib.CollectionLiterals;
29import org.eclipse.xtext.xbase.lib.Extension;
30import org.eclipse.xtext.xbase.lib.Functions.Function1;
31import org.eclipse.xtext.xbase.lib.IterableExtensions;
32import org.eclipse.xtext.xbase.lib.ObjectExtensions;
33import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
34
35@SuppressWarnings("all")
36public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {
37 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
38
39 @Extension
40 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
41
42 public Logic2VampireLanguageMapper_TypeMapper_FilteredTypes() {
43 LogicproblemPackage.eINSTANCE.getClass();
44 }
45
46 @Override
47 public void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {
48 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
49 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
50 it.setName("A");
51 };
52 final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
53 for (final Type type : types) {
54 {
55 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
56 final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
57 it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0]));
58 EList<VLSTerm> _terms = it.getTerms();
59 VLSVariable _duplicate = this.support.duplicate(variable);
60 _terms.add(_duplicate);
61 };
62 final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
63 trace.type2Predicate.put(type, typePred);
64 }
65 }
66 Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);
67 for (final TypeDefinition type_1 : _filter) {
68 {
69 final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();
70 EList<DefinedElement> _elements = type_1.getElements();
71 for (final DefinedElement e : _elements) {
72 {
73 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
74 final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
75 it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2]));
76 EList<VLSTerm> _terms = it.getTerms();
77 VLSVariable _duplicate = this.support.duplicate(variable);
78 _terms.add(_duplicate);
79 };
80 final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
81 trace.element2Predicate.put(e, enumElemPred);
82 orElems.add(enumElemPred);
83 }
84 }
85 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
86 final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
87 it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0]));
88 it.setFofRole("axiom");
89 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
90 final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
91 EList<VLSVariable> _variables = it_1.getVariables();
92 VLSVariable _duplicate = this.support.duplicate(variable);
93 _variables.add(_duplicate);
94 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
95 final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> {
96 it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate));
97 it_2.setRight(this.support.unfoldOr(orElems));
98 };
99 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);
100 it_1.setOperand(_doubleArrow);
101 };
102 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);
103 it.setFofFormula(_doubleArrow);
104 };
105 final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);
106 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
107 _formulas.add(res);
108 }
109 }
110 final Function1<Type, Boolean> _function_1 = (Type it) -> {
111 boolean _isIsAbstract = it.isIsAbstract();
112 return Boolean.valueOf((!_isIsAbstract));
113 };
114 Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);
115 for (final Type t1 : _filter_1) {
116 {
117 for (final Type t2 : types) {
118 if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) {
119 trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
120 } else {
121 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
122 final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> {
123 it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
124 };
125 VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);
126 trace.type2PossibleNot.put(t2, _doubleArrow);
127 }
128 }
129 Collection<VLSTerm> _values = trace.type2PossibleNot.values();
130 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
131 trace.type2And.put(t1, this.support.unfoldAnd(_arrayList));
132 trace.type2PossibleNot.clear();
133 }
134 }
135 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
136 final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
137 it.setName("hierarchyHandler");
138 it.setFofRole("axiom");
139 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
140 final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> {
141 EList<VLSVariable> _variables = it_1.getVariables();
142 VLSVariable _duplicate = this.support.duplicate(variable);
143 _variables.add(_duplicate);
144 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
145 final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> {
146 it_2.setLeft(this.support.topLevelTypeFunc());
147 Collection<VLSTerm> _values = trace.type2And.values();
148 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
149 it_2.setRight(this.support.unfoldOr(_arrayList));
150 };
151 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);
152 it_1.setOperand(_doubleArrow);
153 };
154 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3);
155 it.setFofFormula(_doubleArrow);
156 };
157 final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
158 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
159 _formulas.add(hierarch);
160 }
161
162 @Override
163 public List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {
164 throw new UnsupportedOperationException("TODO: auto-generated method stub");
165 }
166
167 @Override
168 public VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) {
169 throw new UnsupportedOperationException("TODO: auto-generated method stub");
170 }
171
172 @Override
173 public int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) {
174 throw new UnsupportedOperationException("TODO: auto-generated method stub");
175 }
176
177 @Override
178 public VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) {
179 VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote();
180 final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> {
181 String _name = referred.getName();
182 String _plus = ("\"a" + _name);
183 String _plus_1 = (_plus + "\"");
184 it.setValue(_plus_1);
185 };
186 return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function);
187 }
188
189 @Override
190 public VampireModelInterpretation_TypeInterpretation getTypeInterpreter() {
191 throw new UnsupportedOperationException("TODO: auto-generated method stub");
192 }
193}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 10:17:37 +0000