aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.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_RelationMapper.java')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java205
1 files changed, 0 insertions, 205 deletions
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
deleted file mode 100644
index 4c14e93e..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
+++ /dev/null
@@ -1,205 +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.vampireLanguage.VLSAnd;
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition;
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
22import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
23import java.util.ArrayList;
24import java.util.Arrays;
25import java.util.HashMap;
26import java.util.List;
27import java.util.Map;
28import org.eclipse.emf.common.util.EList;
29import org.eclipse.xtext.xbase.lib.CollectionLiterals;
30import org.eclipse.xtext.xbase.lib.Conversions;
31import org.eclipse.xtext.xbase.lib.ExclusiveRange;
32import org.eclipse.xtext.xbase.lib.Extension;
33import org.eclipse.xtext.xbase.lib.ObjectExtensions;
34import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
35
36@SuppressWarnings("all")
37public class Logic2VampireLanguageMapper_RelationMapper {
38 @Extension
39 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
40
41 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
42
43 private final Logic2VampireLanguageMapper base;
44
45 public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) {
46 this.base = base;
47 }
48
49 public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) {
50 final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>();
51 final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>();
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 final String[] nameArray = r.getName().split(" ");
69 String relNameVar = "";
70 int _length_1 = nameArray.length;
71 boolean _equals = (_length_1 == 3);
72 if (_equals) {
73 relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);
74 } else {
75 relNameVar = r.getName();
76 }
77 final String relName = relNameVar;
78 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
79 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
80 it.setName(this.support.toIDMultiple("compliance", relName));
81 it.setFofRole("axiom");
82 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
83 final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
84 for (final VLSVariable v : relVar2VLS) {
85 EList<VLSTffTerm> _variables = it_1.getVariables();
86 VLSVariable _duplicate = this.support.duplicate(v);
87 _variables.add(_duplicate);
88 }
89 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
90 final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {
91 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
92 final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {
93 it_3.setConstant(this.support.toIDMultiple("r", relName));
94 for (final VLSVariable v_1 : relVar2VLS) {
95 EList<VLSTerm> _terms = it_3.getTerms();
96 VLSVariable _duplicate_1 = this.support.duplicate(v_1);
97 _terms.add(_duplicate_1);
98 }
99 };
100 final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);
101 trace.rel2Predicate.put(r, rel);
102 trace.predicate2Relation.put(rel, r);
103 it_2.setLeft(this.support.duplicate(rel));
104 it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply));
105 };
106 VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
107 it_1.setOperand(_doubleArrow);
108 };
109 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
110 it.setFofFormula(_doubleArrow);
111 };
112 final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
113 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
114 _formulas.add(comply);
115 }
116
117 public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) {
118 final Map<Variable, VLSVariable> relVar2VLS = new HashMap<Variable, VLSVariable>();
119 final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList();
120 final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>();
121 int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
122 ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true);
123 for (final Integer i : _doubleDotLessThan) {
124 {
125 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
126 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
127 it.setName(this.support.toIDMultiple("V", i.toString()));
128 };
129 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
130 relVar2VLS.put(r.getVariables().get((i).intValue()), v);
131 vars.add(v);
132 TypeReference _get = r.getParameters().get((i).intValue());
133 final Type relType = ((ComplexTypeReference) _get).getReferred();
134 final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v);
135 relVar2TypeDecComply.add(varTypeComply);
136 }
137 }
138 final String[] nameArray = r.getName().split(" ");
139 String relNameVar = "";
140 int _length_1 = nameArray.length;
141 boolean _equals = (_length_1 == 3);
142 if (_equals) {
143 relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);
144 } else {
145 relNameVar = r.getName();
146 }
147 final String relName = relNameVar;
148 final VLSTerm definition = mapper.transformTerm(r.getValue(), trace, relVar2VLS);
149 final VLSTerm compliance = this.support.unfoldAnd(relVar2TypeDecComply);
150 VLSAnd _createVLSAnd = this.factory.createVLSAnd();
151 final Procedure1<VLSAnd> _function = (VLSAnd it) -> {
152 it.setLeft(compliance);
153 it.setRight(definition);
154 };
155 final VLSAnd compDefn = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function);
156 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
157 final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
158 it.setName(this.support.toID(relName));
159 it.setFofRole("axiom");
160 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
161 final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
162 for (final VLSVariable v : vars) {
163 EList<VLSTffTerm> _variables = it_1.getVariables();
164 VLSVariable _duplicate = this.support.duplicate(v);
165 _variables.add(_duplicate);
166 }
167 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
168 final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {
169 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
170 final Procedure1<VLSFunction> _function_4 = (VLSFunction it_3) -> {
171 it_3.setConstant(this.support.toIDMultiple("r", relName));
172 for (final VLSVariable v_1 : vars) {
173 EList<VLSTerm> _terms = it_3.getTerms();
174 VLSVariable _duplicate_1 = this.support.duplicate(v_1);
175 _terms.add(_duplicate_1);
176 }
177 };
178 final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_4);
179 it_2.setLeft(this.support.duplicate(rel));
180 it_2.setRight(compDefn);
181 };
182 VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);
183 it_1.setOperand(_doubleArrow);
184 };
185 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);
186 it.setFofFormula(_doubleArrow);
187 };
188 final VLSFofFormula relDef = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);
189 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
190 _formulas.add(relDef);
191 }
192
193 public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) {
194 if (r instanceof RelationDeclaration) {
195 _transformRelation((RelationDeclaration)r, trace, mapper);
196 return;
197 } else if (r instanceof RelationDefinition) {
198 _transformRelation((RelationDefinition)r, trace, mapper);
199 return;
200 } else {
201 throw new IllegalArgumentException("Unhandled parameter types: " +
202 Arrays.<Object>asList(r, trace, mapper).toString());
203 }
204 }
205}
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-05 12:54:41 +0000