aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.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/VampireSolver.java')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java275
1 files changed, 0 insertions, 275 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
deleted file mode 100644
index eb6007ec..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ /dev/null
@@ -1,275 +0,0 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner;
2
3import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup;
4import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
8import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
9import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;
10import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;
11import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;
12import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
16import com.google.common.base.Objects;
17import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
18import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation;
19import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
20import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException;
21import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
22import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
23import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
24import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
25import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory;
26import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
27import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry;
28import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics;
29import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry;
30import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
31import java.util.ArrayList;
32import java.util.List;
33import org.eclipse.emf.common.util.EList;
34import org.eclipse.xtend2.lib.StringConcatenation;
35import org.eclipse.xtext.xbase.lib.CollectionLiterals;
36import org.eclipse.xtext.xbase.lib.Exceptions;
37import org.eclipse.xtext.xbase.lib.Extension;
38import org.eclipse.xtext.xbase.lib.Functions.Function1;
39import org.eclipse.xtext.xbase.lib.InputOutput;
40import org.eclipse.xtext.xbase.lib.ListExtensions;
41import org.eclipse.xtext.xbase.lib.ObjectExtensions;
42import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
43
44@SuppressWarnings("all")
45public class VampireSolver extends LogicReasoner {
46 public VampireSolver() {
47 VampireLanguagePackage.eINSTANCE.eClass();
48 final VampireLanguageStandaloneSetupGenerated x = new VampireLanguageStandaloneSetupGenerated();
49 VampireLanguageStandaloneSetup.doSetup();
50 }
51
52 private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper();
53
54 private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper();
55
56 private final VampireHandler handler = new VampireHandler();
57
58 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
59
60 @Extension
61 private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;
62
63 @Extension
64 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
65
66 @Override
67 public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException {
68 try {
69 final VampireSolverConfiguration vampireConfig = this.asConfig(config);
70 String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") +
71 Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp");
72 final long transformationStart = System.currentTimeMillis();
73 final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig);
74 long _currentTimeMillis = System.currentTimeMillis();
75 final long transformationTime = (_currentTimeMillis - transformationStart);
76 final VampireModel vampireProblem = result.getOutput();
77 final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();
78 String fileURI = null;
79 String vampireCode = null;
80 vampireCode = workspace.writeModelToString(vampireProblem, fileName);
81 final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) ||
82 (vampireConfig.documentationLevel == DocumentationLevel.FULL));
83 if (writeFile) {
84 fileURI = workspace.writeModel(vampireProblem, fileName).toFileString();
85 }
86 if (vampireConfig.genModel) {
87 if (vampireConfig.server) {
88 final String form = this.support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit);
89 ArrayList<String> response = CollectionLiterals.<String>newArrayList();
90 int ind = 0;
91 boolean done = false;
92 InputOutput.<String>print(" ");
93 while ((!done)) {
94 {
95 InputOutput.<String>print("(x)");
96 done = false;
97 response = this.support.sendPost(form);
98 boolean responseFound = false;
99 ind = 0;
100 while ((!responseFound)) {
101 {
102 String line = response.get(ind);
103 if (((line.length() >= 5) && Objects.equal(line.substring(0, 5), "ERROR"))) {
104 done = false;
105 responseFound = true;
106 } else {
107 boolean _equals = Objects.equal(line, "</PRE>");
108 if (_equals) {
109 done = true;
110 responseFound = true;
111 }
112 }
113 ind++;
114 }
115 }
116 }
117 }
118 final String satRaw = response.get((ind - 3));
119 final String modRaw = response.get((ind - 2));
120 final ArrayList<String> sat = CollectionLiterals.<String>newArrayList(satRaw.split(" "));
121 final ArrayList<String> mod = CollectionLiterals.<String>newArrayList(modRaw.split(" "));
122 final String satOut = sat.get(1);
123 final String modOut = mod.get(1);
124 final String satTime = sat.get(2);
125 final String modTime = mod.get(2);
126 InputOutput.println();
127 InputOutput.<ArrayList<String>>println(sat);
128 InputOutput.<ArrayList<String>>println(mod);
129 ModelResult _createModelResult = this.resultFactory.createModelResult();
130 final Procedure1<ModelResult> _function = (ModelResult it) -> {
131 it.setProblem(null);
132 EList<Object> _representation = it.getRepresentation();
133 VampireModel _createVampireModel = this.factory.createVampireModel();
134 final Procedure1<VampireModel> _function_1 = (VampireModel it_1) -> {
135 };
136 VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1);
137 _representation.add(_doubleArrow);
138 it.setTrace(it.getTrace());
139 Statistics _createStatistics = this.resultFactory.createStatistics();
140 final Procedure1<Statistics> _function_2 = (Statistics it_1) -> {
141 it_1.setTransformationTime(((int) transformationTime));
142 EList<StatisticEntry> _entries = it_1.getEntries();
143 StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry();
144 final Procedure1<StringStatisticEntry> _function_3 = (StringStatisticEntry it_2) -> {
145 it_2.setName("satOut");
146 it_2.setValue(satOut);
147 };
148 StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3);
149 _entries.add(_doubleArrow_1);
150 EList<StatisticEntry> _entries_1 = it_1.getEntries();
151 StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry();
152 final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> {
153 it_2.setName("satTime");
154 it_2.setValue(satTime);
155 };
156 StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_4);
157 _entries_1.add(_doubleArrow_2);
158 EList<StatisticEntry> _entries_2 = it_1.getEntries();
159 StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry();
160 final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> {
161 it_2.setName("modOut");
162 it_2.setValue(modOut);
163 };
164 StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_5);
165 _entries_2.add(_doubleArrow_3);
166 EList<StatisticEntry> _entries_3 = it_1.getEntries();
167 StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry();
168 final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> {
169 it_2.setName("modTime");
170 it_2.setValue(modTime);
171 };
172 StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_6);
173 _entries_3.add(_doubleArrow_4);
174 };
175 Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2);
176 it.setStatistics(_doubleArrow_1);
177 };
178 return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function);
179 } else {
180 InputOutput.println();
181 final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);
182 String modOut_1 = "no";
183 boolean _isFiniteModelGenerated = vampSol.isFiniteModelGenerated();
184 if (_isFiniteModelGenerated) {
185 modOut_1 = "FiniteModel";
186 }
187 final String realModOut = modOut_1;
188 ModelResult _createModelResult_1 = this.resultFactory.createModelResult();
189 final Procedure1<ModelResult> _function_1 = (ModelResult it) -> {
190 it.setProblem(null);
191 EList<Object> _representation = it.getRepresentation();
192 VampireModel _createVampireModel = this.factory.createVampireModel();
193 final Procedure1<VampireModel> _function_2 = (VampireModel it_1) -> {
194 };
195 VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_2);
196 _representation.add(_doubleArrow);
197 it.setTrace(it.getTrace());
198 Statistics _createStatistics = this.resultFactory.createStatistics();
199 final Procedure1<Statistics> _function_3 = (Statistics it_1) -> {
200 it_1.setTransformationTime(((int) transformationTime));
201 EList<StatisticEntry> _entries = it_1.getEntries();
202 StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry();
203 final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> {
204 it_2.setName("satOut");
205 it_2.setValue("-");
206 };
207 StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_4);
208 _entries.add(_doubleArrow_1);
209 EList<StatisticEntry> _entries_1 = it_1.getEntries();
210 StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry();
211 final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> {
212 it_2.setName("satTime");
213 it_2.setValue("-");
214 };
215 StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5);
216 _entries_1.add(_doubleArrow_2);
217 EList<StatisticEntry> _entries_2 = it_1.getEntries();
218 StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry();
219 final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> {
220 it_2.setName("modOut");
221 it_2.setValue(realModOut);
222 };
223 StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_6);
224 _entries_2.add(_doubleArrow_3);
225 EList<StatisticEntry> _entries_3 = it_1.getEntries();
226 StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry();
227 final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> {
228 it_2.setName("modTime");
229 long _solverTime = vampSol.getSolverTime();
230 it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString());
231 };
232 StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_7);
233 _entries_3.add(_doubleArrow_4);
234 };
235 Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_3);
236 it.setStatistics(_doubleArrow_1);
237 };
238 return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_1);
239 }
240 }
241 return null;
242 } catch (Throwable _e) {
243 throw Exceptions.sneakyThrow(_e);
244 }
245 }
246
247 public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) {
248 if ((configuration instanceof VampireSolverConfiguration)) {
249 return ((VampireSolverConfiguration)configuration);
250 } else {
251 StringConcatenation _builder = new StringConcatenation();
252 _builder.append("The configuration have to be an ");
253 String _simpleName = VampireSolverConfiguration.class.getSimpleName();
254 _builder.append(_simpleName);
255 _builder.append("!");
256 throw new IllegalArgumentException(_builder.toString());
257 }
258 }
259
260 @Override
261 public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) {
262 List<VampireModelInterpretation> _xblockexpression = null;
263 {
264 final EList<Object> sols = modelResult.getRepresentation();
265 final Function1<Object, VampireModelInterpretation> _function = (Object it) -> {
266 Object _trace = modelResult.getTrace();
267 return new VampireModelInterpretation(
268 ((VampireModel) it),
269 ((Logic2VampireLanguageMapperTrace) _trace));
270 };
271 _xblockexpression = ListExtensions.<Object, VampireModelInterpretation>map(sols, _function);
272 }
273 return _xblockexpression;
274 }
275}
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-05 10:47:44 +0000