From f63a94c06268b5233264436cc538062f1f7b01bc Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 8 Oct 2019 03:00:08 -0400 Subject: VAMPIRE: fix bug in transformation, further implement measurement code --- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2691 -> 2845 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 7020 -> 6973 bytes .../vampire/reasoner/VampireSolver.java | 13 ++--- .../reasoner/VampireSolverConfiguration.java | 2 + .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18099 -> 19565 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3165 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11807 -> 11807 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 7934 -> 7880 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10676 -> 10676 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13060 -> 13059 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11037 -> 11038 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3950 -> 3997 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 6882 -> 6937 bytes .../builder/Logic2VampireLanguageMapper.java | 60 +++++++++++++++++++-- ...Logic2VampireLanguageMapper_RelationMapper.java | 2 - .../reasoner/builder/Vampire2LogicMapper.java | 3 +- .../vampire/reasoner/builder/VampireHandler.java | 2 +- 17 files changed, 66 insertions(+), 16 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 600187ca..2c203d6e 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 9517185f..f2461efc 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 1241dcb2..c3e185f5 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 @@ -62,6 +62,8 @@ public class VampireSolver extends LogicReasoner { final VampireSolverConfiguration vampireConfig = this.asConfig(config); final long transformationStart = System.currentTimeMillis(); final TracedOutput result = this.forwardMapper.transformProblem(problem, vampireConfig); + long _currentTimeMillis = System.currentTimeMillis(); + final long transformationTime = (_currentTimeMillis - transformationStart); final VampireModel vampireProblem = result.getOutput(); final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); String fileURI = null; @@ -72,16 +74,11 @@ public class VampireSolver extends LogicReasoner { if (writeFile) { fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); } - long _currentTimeMillis = System.currentTimeMillis(); - final long transformationTime = (_currentTimeMillis - transformationStart); - final long solverStart = System.currentTimeMillis(); final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); - long _currentTimeMillis_1 = System.currentTimeMillis(); - final long solvingTime = (_currentTimeMillis_1 - solverStart); final long backTransformationStart = System.currentTimeMillis(); - final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, solvingTime); - long _currentTimeMillis_2 = System.currentTimeMillis(); - final long backTransformationTime = (_currentTimeMillis_2 - backTransformationStart); + 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; } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java index ac55ebd7..5086d15a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java @@ -7,4 +7,6 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration { public int contCycleLevel = 0; public boolean uniquenessDuplicates = false; + + public int iteration = (-1); } 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 3ebc907b..f537b830 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/.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 c9ae6c62..14a639ad 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 ec8fae35..ba5dbd89 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 5e770b94..f5e4ca8c 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 1d3cd01c..6c06a366 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 72067608..1ee73cd6 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 a9228720..edda9f05 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 3697ed87..8edf2fe9 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 c489bf07..18c788c6 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/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index c8961c6e..dc5ec788 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java @@ -54,6 +54,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.Arrays; @@ -65,6 +66,9 @@ import java.util.function.Consumer; import org.eclipse.emf.common.util.EList; import org.eclipse.xtend.lib.annotations.AccessorType; import org.eclipse.xtend.lib.annotations.Accessors; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; +import org.eclipse.xtext.xbase.lib.Conversions; +import org.eclipse.xtext.xbase.lib.ExclusiveRange; import org.eclipse.xtext.xbase.lib.Extension; import org.eclipse.xtext.xbase.lib.Functions.Function1; import org.eclipse.xtext.xbase.lib.IterableExtensions; @@ -118,18 +122,23 @@ public class Logic2VampireLanguageMapper { this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); } trace.relationDefinitions = this.collectRelationDefinitions(problem); - final Consumer _function_3 = (Relation it) -> { + final Function1 _function_3 = (Relation it) -> { + Class _class = it.getClass(); + return Boolean.valueOf(Objects.equal(_class, RelationDefinitionImpl.class)); + }; + this.toTrace(IterableExtensions.filter(problem.getRelations(), _function_3), trace); + final Consumer _function_4 = (Relation it) -> { Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper(); this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper); }; - problem.getRelations().forEach(_function_3); + problem.getRelations().forEach(_function_4); this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); this.scopeMapper.transformScope(problem.getTypes(), config, trace); trace.constantDefinitions = this.collectConstantDefinitions(problem); - final Consumer _function_4 = (ConstantDefinition it) -> { + final Consumer _function_5 = (ConstantDefinition it) -> { this.constantMapper.transformConstantDefinitionSpecification(it, trace); }; - Iterables.filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_4); + Iterables.filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_5); EList _assertions = problem.getAssertions(); for (final Assertion assertion : _assertions) { this.transformAssertion(assertion, trace); @@ -137,6 +146,49 @@ public class Logic2VampireLanguageMapper { return new TracedOutput(specification, trace); } + public void toTrace(final Iterable relations, final Logic2VampireLanguageMapperTrace trace) { + final List vars = CollectionLiterals.newArrayList(); + for (final Relation rel : relations) { + { + final String[] nameArray = rel.getName().split(" "); + String relNameVar = ""; + int _length = nameArray.length; + boolean _equals = (_length == 3); + if (_equals) { + relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); + } else { + relNameVar = rel.getName(); + } + final String relName = relNameVar; + final RelationDefinition relDef = ((RelationDefinition) rel); + int _length_1 = ((Object[])Conversions.unwrapArray(rel.getParameters(), Object.class)).length; + ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length_1, true); + for (final Integer i : _doubleDotLessThan) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function = (VLSVariable it) -> { + it.setName(this.support.toIDMultiple("V", i.toString())); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + vars.add(v); + } + } + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant(this.support.toIDMultiple("r", relName)); + for (final VLSVariable v : vars) { + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.support.duplicate(v); + _terms.add(_duplicate); + } + }; + final VLSFunction relFunc = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); + trace.relDef2Predicate.put(relDef, relFunc); + trace.predicate2RelDef.put(relFunc, relDef); + } + } + } + protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { return null; } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java index c175c72a..4c14e93e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java @@ -176,8 +176,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { } }; final VLSFunction rel = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_4); - trace.relDef2Predicate.put(r, rel); - trace.predicate2RelDef.put(rel, r); it_2.setLeft(this.support.duplicate(rel)); it_2.setRight(compDefn); }; diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java index 4fbf7291..9fb23c71 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java @@ -34,7 +34,8 @@ public class Vampire2LogicMapper { Statistics _createStatistics = this.resultFactory.createStatistics(); final Procedure1 _function = (Statistics it) -> { long _solverTime = solution.getSolverTime(); - it.setTransformationTime(((int) _solverTime)); + it.setSolverTime(((int) _solverTime)); + it.setTransformationTime(((int) transformationTime)); }; return ObjectExtensions.operator_doubleArrow(_createStatistics, _function); } 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 0c8b0013..a1f19410 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 @@ -25,7 +25,7 @@ public class VampireHandler { final String VAMPNAME = "vampire.exe"; final String TEMPNAME = "TEMP.tptp"; final String OPTION = " --mode casc_sat -t 300 "; - final String SOLNNAME = (("_solution" + Integer.valueOf(configuration.typeScopes.maxNewElements)) + ".tptp"); + final String SOLNNAME = (((("solution" + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + ".tptp"); final String PATH = "C:/cygwin64/bin"; final URI wsURI = workspace.getWorkspaceURI(); final String tempLoc = (wsURI + TEMPNAME); -- cgit v1.2.3-54-g00ecf