From 25a4b1b53add70e268c3083682f8a3508c618ec2 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 25 Oct 2019 04:15:39 -0400 Subject: VAMPIRE: post-submission push --- .../vampire/reasoner/VampireSolver.java | 51 ++++++++-------------- 1 file changed, 17 insertions(+), 34 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java') 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 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl; import com.google.common.base.Objects; import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; @@ -35,12 +33,10 @@ import java.util.List; import org.eclipse.emf.common.util.EList; import org.eclipse.xtend2.lib.StringConcatenation; import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.Exceptions; import org.eclipse.xtext.xbase.lib.Extension; import org.eclipse.xtext.xbase.lib.Functions.Function1; import org.eclipse.xtext.xbase.lib.InputOutput; -import org.eclipse.xtext.xbase.lib.IterableExtensions; import org.eclipse.xtext.xbase.lib.ListExtensions; import org.eclipse.xtext.xbase.lib.ObjectExtensions; import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @@ -183,79 +179,66 @@ public class VampireSolver extends LogicReasoner { } else { InputOutput.println(); final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); - final long backTransformationStart = System.currentTimeMillis(); - final ModelResult logicResult = this.backwardMapper.transformOutput(problem, - vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); - long _currentTimeMillis_1 = System.currentTimeMillis(); - final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); - final Function1 _function_1 = (VLSConfirmations it) -> { - Class _class = it.getClass(); - return Boolean.valueOf(Objects.equal(_class, VLSFiniteModelImpl.class)); - }; - Iterable model = IterableExtensions.filter(vampSol.getGeneratedModel().getConfirmations(), _function_1); String modOut_1 = "no"; - final Iterable _converted_model = (Iterable)model; - int _length = ((Object[])Conversions.unwrapArray(_converted_model, Object.class)).length; - boolean _greaterThan = (_length > 0); - if (_greaterThan) { + boolean _isFiniteModelGenerated = vampSol.isFiniteModelGenerated(); + if (_isFiniteModelGenerated) { modOut_1 = "FiniteModel"; } final String realModOut = modOut_1; ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); - final Procedure1 _function_2 = (ModelResult it) -> { + final Procedure1 _function_1 = (ModelResult it) -> { it.setProblem(null); EList _representation = it.getRepresentation(); VampireModel _createVampireModel = this.factory.createVampireModel(); - final Procedure1 _function_3 = (VampireModel it_1) -> { + final Procedure1 _function_2 = (VampireModel it_1) -> { }; - VampireModel _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVampireModel, _function_3); + VampireModel _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVampireModel, _function_2); _representation.add(_doubleArrow); it.setTrace(it.getTrace()); Statistics _createStatistics = this.resultFactory.createStatistics(); - final Procedure1 _function_4 = (Statistics it_1) -> { + final Procedure1 _function_3 = (Statistics it_1) -> { it_1.setTransformationTime(((int) transformationTime)); EList _entries = it_1.getEntries(); StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_5 = (StringStatisticEntry it_2) -> { + final Procedure1 _function_4 = (StringStatisticEntry it_2) -> { it_2.setName("satOut"); it_2.setValue("-"); }; - StringStatisticEntry _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry, _function_5); + StringStatisticEntry _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry, _function_4); _entries.add(_doubleArrow_1); EList _entries_1 = it_1.getEntries(); StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_6 = (StringStatisticEntry it_2) -> { + final Procedure1 _function_5 = (StringStatisticEntry it_2) -> { it_2.setName("satTime"); it_2.setValue("-"); }; - StringStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_1, _function_6); + StringStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_1, _function_5); _entries_1.add(_doubleArrow_2); EList _entries_2 = it_1.getEntries(); StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_7 = (StringStatisticEntry it_2) -> { + final Procedure1 _function_6 = (StringStatisticEntry it_2) -> { it_2.setName("modOut"); it_2.setValue(realModOut); }; - StringStatisticEntry _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_2, _function_7); + StringStatisticEntry _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_2, _function_6); _entries_2.add(_doubleArrow_3); EList _entries_3 = it_1.getEntries(); StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_8 = (StringStatisticEntry it_2) -> { + final Procedure1 _function_7 = (StringStatisticEntry it_2) -> { it_2.setName("modTime"); long _solverTime = vampSol.getSolverTime(); it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString()); }; - StringStatisticEntry _doubleArrow_4 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_3, _function_8); + StringStatisticEntry _doubleArrow_4 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_3, _function_7); _entries_3.add(_doubleArrow_4); }; - Statistics _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStatistics, _function_4); + Statistics _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStatistics, _function_3); it.setStatistics(_doubleArrow_1); }; - return ObjectExtensions.operator_doubleArrow(_createModelResult_1, _function_2); + return ObjectExtensions.operator_doubleArrow(_createModelResult_1, _function_1); } } - MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); - return this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); + return null; } catch (Throwable _e) { throw Exceptions.sneakyThrow(_e); } -- cgit v1.2.3-54-g00ecf