diff options
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.java | 51 |
1 files changed, 17 insertions, 34 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 index 4f554956..eb6007ec 100644 --- 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 | |||
@@ -10,11 +10,9 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolut | |||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; |
11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | 11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; |
12 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; | 12 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl; | ||
18 | import com.google.common.base.Objects; | 16 | import com.google.common.base.Objects; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; |
@@ -35,12 +33,10 @@ import java.util.List; | |||
35 | import org.eclipse.emf.common.util.EList; | 33 | import org.eclipse.emf.common.util.EList; |
36 | import org.eclipse.xtend2.lib.StringConcatenation; | 34 | import org.eclipse.xtend2.lib.StringConcatenation; |
37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 35 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
38 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
39 | import org.eclipse.xtext.xbase.lib.Exceptions; | 36 | import org.eclipse.xtext.xbase.lib.Exceptions; |
40 | import org.eclipse.xtext.xbase.lib.Extension; | 37 | import org.eclipse.xtext.xbase.lib.Extension; |
41 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 38 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
42 | import org.eclipse.xtext.xbase.lib.InputOutput; | 39 | import org.eclipse.xtext.xbase.lib.InputOutput; |
43 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
44 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 40 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
45 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 41 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
46 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 42 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
@@ -183,79 +179,66 @@ public class VampireSolver extends LogicReasoner { | |||
183 | } else { | 179 | } else { |
184 | InputOutput.println(); | 180 | InputOutput.println(); |
185 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | 181 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); |
186 | final long backTransformationStart = System.currentTimeMillis(); | ||
187 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, | ||
188 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | ||
189 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
190 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | ||
191 | final Function1<VLSConfirmations, Boolean> _function_1 = (VLSConfirmations it) -> { | ||
192 | Class<? extends VLSConfirmations> _class = it.getClass(); | ||
193 | return Boolean.valueOf(Objects.equal(_class, VLSFiniteModelImpl.class)); | ||
194 | }; | ||
195 | Iterable<VLSConfirmations> model = IterableExtensions.<VLSConfirmations>filter(vampSol.getGeneratedModel().getConfirmations(), _function_1); | ||
196 | String modOut_1 = "no"; | 182 | String modOut_1 = "no"; |
197 | final Iterable<VLSConfirmations> _converted_model = (Iterable<VLSConfirmations>)model; | 183 | boolean _isFiniteModelGenerated = vampSol.isFiniteModelGenerated(); |
198 | int _length = ((Object[])Conversions.unwrapArray(_converted_model, Object.class)).length; | 184 | if (_isFiniteModelGenerated) { |
199 | boolean _greaterThan = (_length > 0); | ||
200 | if (_greaterThan) { | ||
201 | modOut_1 = "FiniteModel"; | 185 | modOut_1 = "FiniteModel"; |
202 | } | 186 | } |
203 | final String realModOut = modOut_1; | 187 | final String realModOut = modOut_1; |
204 | ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); | 188 | ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); |
205 | final Procedure1<ModelResult> _function_2 = (ModelResult it) -> { | 189 | final Procedure1<ModelResult> _function_1 = (ModelResult it) -> { |
206 | it.setProblem(null); | 190 | it.setProblem(null); |
207 | EList<Object> _representation = it.getRepresentation(); | 191 | EList<Object> _representation = it.getRepresentation(); |
208 | VampireModel _createVampireModel = this.factory.createVampireModel(); | 192 | VampireModel _createVampireModel = this.factory.createVampireModel(); |
209 | final Procedure1<VampireModel> _function_3 = (VampireModel it_1) -> { | 193 | final Procedure1<VampireModel> _function_2 = (VampireModel it_1) -> { |
210 | }; | 194 | }; |
211 | VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_3); | 195 | VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_2); |
212 | _representation.add(_doubleArrow); | 196 | _representation.add(_doubleArrow); |
213 | it.setTrace(it.getTrace()); | 197 | it.setTrace(it.getTrace()); |
214 | Statistics _createStatistics = this.resultFactory.createStatistics(); | 198 | Statistics _createStatistics = this.resultFactory.createStatistics(); |
215 | final Procedure1<Statistics> _function_4 = (Statistics it_1) -> { | 199 | final Procedure1<Statistics> _function_3 = (Statistics it_1) -> { |
216 | it_1.setTransformationTime(((int) transformationTime)); | 200 | it_1.setTransformationTime(((int) transformationTime)); |
217 | EList<StatisticEntry> _entries = it_1.getEntries(); | 201 | EList<StatisticEntry> _entries = it_1.getEntries(); |
218 | StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); | 202 | StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); |
219 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { | 203 | final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> { |
220 | it_2.setName("satOut"); | 204 | it_2.setName("satOut"); |
221 | it_2.setValue("-"); | 205 | it_2.setValue("-"); |
222 | }; | 206 | }; |
223 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_5); | 207 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_4); |
224 | _entries.add(_doubleArrow_1); | 208 | _entries.add(_doubleArrow_1); |
225 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); | 209 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); |
226 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); | 210 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); |
227 | final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> { | 211 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { |
228 | it_2.setName("satTime"); | 212 | it_2.setName("satTime"); |
229 | it_2.setValue("-"); | 213 | it_2.setValue("-"); |
230 | }; | 214 | }; |
231 | StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_6); | 215 | StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5); |
232 | _entries_1.add(_doubleArrow_2); | 216 | _entries_1.add(_doubleArrow_2); |
233 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); | 217 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); |
234 | StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); | 218 | StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); |
235 | final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> { | 219 | final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> { |
236 | it_2.setName("modOut"); | 220 | it_2.setName("modOut"); |
237 | it_2.setValue(realModOut); | 221 | it_2.setValue(realModOut); |
238 | }; | 222 | }; |
239 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_7); | 223 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_6); |
240 | _entries_2.add(_doubleArrow_3); | 224 | _entries_2.add(_doubleArrow_3); |
241 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); | 225 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); |
242 | StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); | 226 | StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); |
243 | final Procedure1<StringStatisticEntry> _function_8 = (StringStatisticEntry it_2) -> { | 227 | final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> { |
244 | it_2.setName("modTime"); | 228 | it_2.setName("modTime"); |
245 | long _solverTime = vampSol.getSolverTime(); | 229 | long _solverTime = vampSol.getSolverTime(); |
246 | it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString()); | 230 | it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString()); |
247 | }; | 231 | }; |
248 | StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_8); | 232 | StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_7); |
249 | _entries_3.add(_doubleArrow_4); | 233 | _entries_3.add(_doubleArrow_4); |
250 | }; | 234 | }; |
251 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_4); | 235 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_3); |
252 | it.setStatistics(_doubleArrow_1); | 236 | it.setStatistics(_doubleArrow_1); |
253 | }; | 237 | }; |
254 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_2); | 238 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_1); |
255 | } | 239 | } |
256 | } | 240 | } |
257 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); | 241 | return null; |
258 | return this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); | ||
259 | } catch (Throwable _e) { | 242 | } catch (Throwable _e) { |
260 | throw Exceptions.sneakyThrow(_e); | 243 | throw Exceptions.sneakyThrow(_e); |
261 | } | 244 | } |