From 32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 25 Oct 2019 04:15:39 -0400 Subject: VAMPIRE: post-submission push --- .../.VampireAnalyzerConfiguration.xtendbin | Bin 3449 -> 3449 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 10862 -> 10104 bytes .../vampire/reasoner/VampireSolver.java | 51 +++++++-------------- .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 19565 -> 19565 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 5080 -> 5080 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11807 -> 11807 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 7880 -> 7880 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10682 -> 10684 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 17151 -> 17151 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11037 -> 11037 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3997 -> 3998 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 7782 -> 7743 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../Logic2VampireLanguageMapper_ScopeMapper.java | 6 +-- .../vampire/reasoner/builder/VampireHandler.java | 20 ++++---- 17 files changed, 28 insertions(+), 49 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 5c40d767..88e234fc 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index 2d4d0741..8f9c0397 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin differ 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); } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 887a3a31..07b7d4c3 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index b4943b57..04a3303b 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index e3b29572..dbd48bbb 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index 50ff7011..4f4710d4 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index 337edcba..19ff819d 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index c32ba83f..2774bb57 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 75e60f21..9b636247 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index d69b41ea..739f0cd5 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index 6b91ff7b..96506230 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index f23063ea..b7d9060d 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 0de59fdb..d8bc6614 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 6176aca5..512e8a06 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index c09d929e..d6c90484 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java @@ -59,9 +59,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper { final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); final ArrayList localInstances = CollectionLiterals.newArrayList(); - final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); + final boolean consistant = (GLOBAL_MAX >= GLOBAL_MIN); if ((GLOBAL_MIN != ABSOLUTE_MIN)) { - this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant); + this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant)); if (consistant) { for (final VLSConstant i : trace.uniqueInstances) { localInstances.add(this.support.duplicate(i)); @@ -72,7 +72,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { } } if ((GLOBAL_MAX != ABSOLUTE_MAX)) { - this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, (!consistant)); + this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant); if (consistant) { this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); } else { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java index e9073d82..39773357 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java @@ -7,12 +7,9 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; import com.google.common.base.Objects; import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; import java.io.BufferedReader; -import java.io.InputStream; -import java.io.InputStreamReader; +import java.io.FileReader; import java.util.List; -import org.eclipse.emf.common.util.EList; import org.eclipse.emf.common.util.URI; -import org.eclipse.emf.ecore.EObject; import org.eclipse.xtext.xbase.lib.CollectionLiterals; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.Exceptions; @@ -67,18 +64,17 @@ public class VampireHandler { long _minus_1 = (_currentTimeMillis_1 - startTime); solverTime = _minus_1; } - InputStream _inputStream = p.getInputStream(); - InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream); - final BufferedReader reader = new BufferedReader(_inputStreamReader); + FileReader _fileReader = new FileReader(solnLoc); + final BufferedReader reader = new BufferedReader(_fileReader); final List output = CollectionLiterals.newArrayList(); String line = ""; while ((!Objects.equal((line = reader.readLine()), null))) { - output.add((line + "\n")); + boolean _equals_2 = Objects.equal(line, "Finite Model Found!"); + if (_equals_2) { + return new MonitoredVampireSolution(solverTime, null, true); + } } - workspace.getFile(TEMPNAME).delete(); - final EList root = workspace.readModel(VampireModel.class, SOLNNAME).eResource().getContents(); - EObject _get = root.get(0); - return new MonitoredVampireSolution(solverTime, ((VampireModel) _get)); + return new MonitoredVampireSolution(solverTime, null, false); } catch (Throwable _e) { throw Exceptions.sneakyThrow(_e); } -- cgit v1.2.3-54-g00ecf