From 012e1cbb107110ff0d6381ed186163e399f1dd55 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 21 Oct 2019 17:14:25 -0400 Subject: mid-measurement push --- .../.VampireAnalyzerConfiguration.xtendbin | Bin 3418 -> 3449 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 10151 -> 10862 bytes .../vampire/reasoner/VampireSolver.java | 91 ++++++++++++++++++--- .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 19566 -> 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 -> 10682 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 17151 -> 17151 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11037 -> 11037 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3997 -> 3997 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 7804 -> 7782 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../vampire/reasoner/builder/VampireHandler.java | 4 +- 16 files changed, 81 insertions(+), 14 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse') 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 b26c1ded..5c40d767 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 7fedcc30..2d4d0741 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 3e3bd688..4f554956 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,9 +10,11 @@ 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; @@ -24,7 +26,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; -import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; @@ -34,10 +35,12 @@ 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; @@ -149,28 +152,28 @@ public class VampireSolver extends LogicReasoner { StringStatisticEntry _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry, _function_3); _entries.add(_doubleArrow_1); EList _entries_1 = it_1.getEntries(); - RealStatisticEntry _createRealStatisticEntry = this.resultFactory.createRealStatisticEntry(); - final Procedure1 _function_4 = (RealStatisticEntry it_2) -> { + StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_4 = (StringStatisticEntry it_2) -> { it_2.setName("satTime"); - it_2.setValue(Double.parseDouble(satTime)); + it_2.setValue(satTime); }; - RealStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createRealStatisticEntry, _function_4); + StringStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_1, _function_4); _entries_1.add(_doubleArrow_2); EList _entries_2 = it_1.getEntries(); - StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); + StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); final Procedure1 _function_5 = (StringStatisticEntry it_2) -> { it_2.setName("modOut"); it_2.setValue(modOut); }; - StringStatisticEntry _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_1, _function_5); + StringStatisticEntry _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_2, _function_5); _entries_2.add(_doubleArrow_3); EList _entries_3 = it_1.getEntries(); - RealStatisticEntry _createRealStatisticEntry_1 = this.resultFactory.createRealStatisticEntry(); - final Procedure1 _function_6 = (RealStatisticEntry it_2) -> { + StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_6 = (StringStatisticEntry it_2) -> { it_2.setName("modTime"); - it_2.setValue(Double.parseDouble(modTime)); + it_2.setValue(modTime); }; - RealStatisticEntry _doubleArrow_4 = ObjectExtensions.operator_doubleArrow(_createRealStatisticEntry_1, _function_6); + StringStatisticEntry _doubleArrow_4 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_3, _function_6); _entries_3.add(_doubleArrow_4); }; Statistics _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStatistics, _function_2); @@ -178,13 +181,77 @@ public class VampireSolver extends LogicReasoner { }; return ObjectExtensions.operator_doubleArrow(_createModelResult, _function); } 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); - return logicResult; + 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) { + modOut_1 = "FiniteModel"; + } + final String realModOut = modOut_1; + ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); + final Procedure1 _function_2 = (ModelResult it) -> { + it.setProblem(null); + EList _representation = it.getRepresentation(); + VampireModel _createVampireModel = this.factory.createVampireModel(); + final Procedure1 _function_3 = (VampireModel it_1) -> { + }; + VampireModel _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVampireModel, _function_3); + _representation.add(_doubleArrow); + it.setTrace(it.getTrace()); + Statistics _createStatistics = this.resultFactory.createStatistics(); + final Procedure1 _function_4 = (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) -> { + it_2.setName("satOut"); + it_2.setValue("-"); + }; + StringStatisticEntry _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry, _function_5); + _entries.add(_doubleArrow_1); + EList _entries_1 = it_1.getEntries(); + StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_6 = (StringStatisticEntry it_2) -> { + it_2.setName("satTime"); + it_2.setValue("-"); + }; + StringStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_1, _function_6); + _entries_1.add(_doubleArrow_2); + EList _entries_2 = it_1.getEntries(); + StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_7 = (StringStatisticEntry it_2) -> { + it_2.setName("modOut"); + it_2.setValue(realModOut); + }; + StringStatisticEntry _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_2, _function_7); + _entries_2.add(_doubleArrow_3); + EList _entries_3 = it_1.getEntries(); + StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_8 = (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); + _entries_3.add(_doubleArrow_4); + }; + Statistics _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStatistics, _function_4); + it.setStatistics(_doubleArrow_1); + }; + return ObjectExtensions.operator_doubleArrow(_createModelResult_1, _function_2); } } MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); 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 8b7f031e..887a3a31 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 1b6e8f80..b4943b57 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 f523f1af..e3b29572 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 30ba1843..50ff7011 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 174c7362..337edcba 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 affa3754..c32ba83f 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 9caad4ea..75e60f21 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 5be67889..d69b41ea 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 192c9d1a..6b91ff7b 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 0495ab53..f23063ea 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 c438f1e5..0de59fdb 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 5fb9b455..6176aca5 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/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java index e32530cb..e9073d82 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 @@ -30,7 +30,7 @@ public class VampireHandler { final String CVC4LOC = (CVC4DIR + CVC4NAME); final String CMD = "cmd /c "; final String TEMPNAME = "TEMP.tptp"; - final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + + final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.minNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + ".tptp"); final String PATH = "C:/cygwin64/bin"; final URI wsURI = workspace.getWorkspaceURI(); @@ -41,7 +41,7 @@ public class VampireHandler { long startTime = (-((long) 1)); long solverTime = (-((long) 1)); Process p = null; - boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMPIRE); + boolean _equals = Objects.equal(configuration.solver, BackendSolver.LOCVAMP); if (_equals) { String OPTION = " --mode casc_sat "; if ((configuration.runtimeLimit != (-1))) { -- cgit v1.2.3-54-g00ecf