diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-08 03:00:08 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:10 -0400 |
commit | d0e4ffcc9dfc85367ccc73bf070404416081a477 (patch) | |
tree | 0db0134207f473f6a12d7c362512b008bd6449eb /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner | |
parent | VAMPIRE: Implement Vampire measurement code (diff) | |
download | VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.tar.gz VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.tar.zst VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.zip |
VAMPIRE: fix bug in transformation, further implement measurement code
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner')
17 files changed, 66 insertions, 16 deletions
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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 { | |||
62 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); | 62 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); |
63 | final long transformationStart = System.currentTimeMillis(); | 63 | final long transformationStart = System.currentTimeMillis(); |
64 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | 64 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); |
65 | long _currentTimeMillis = System.currentTimeMillis(); | ||
66 | final long transformationTime = (_currentTimeMillis - transformationStart); | ||
65 | final VampireModel vampireProblem = result.getOutput(); | 67 | final VampireModel vampireProblem = result.getOutput(); |
66 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | 68 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); |
67 | String fileURI = null; | 69 | String fileURI = null; |
@@ -72,16 +74,11 @@ public class VampireSolver extends LogicReasoner { | |||
72 | if (writeFile) { | 74 | if (writeFile) { |
73 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); | 75 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); |
74 | } | 76 | } |
75 | long _currentTimeMillis = System.currentTimeMillis(); | ||
76 | final long transformationTime = (_currentTimeMillis - transformationStart); | ||
77 | final long solverStart = System.currentTimeMillis(); | ||
78 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | 77 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); |
79 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
80 | final long solvingTime = (_currentTimeMillis_1 - solverStart); | ||
81 | final long backTransformationStart = System.currentTimeMillis(); | 78 | final long backTransformationStart = System.currentTimeMillis(); |
82 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, solvingTime); | 79 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); |
83 | long _currentTimeMillis_2 = System.currentTimeMillis(); | 80 | long _currentTimeMillis_1 = System.currentTimeMillis(); |
84 | final long backTransformationTime = (_currentTimeMillis_2 - backTransformationStart); | 81 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); |
85 | return logicResult; | 82 | return logicResult; |
86 | } | 83 | } |
87 | 84 | ||
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 { | |||
7 | public int contCycleLevel = 0; | 7 | public int contCycleLevel = 0; |
8 | 8 | ||
9 | public boolean uniquenessDuplicates = false; | 9 | public boolean uniquenessDuplicates = false; |
10 | |||
11 | public int iteration = (-1); | ||
10 | } | 12 | } |
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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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; | |||
54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
55 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 55 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
56 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl; | 56 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl; |
57 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl; | ||
57 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 58 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
58 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 59 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
59 | import java.util.Arrays; | 60 | import java.util.Arrays; |
@@ -65,6 +66,9 @@ import java.util.function.Consumer; | |||
65 | import org.eclipse.emf.common.util.EList; | 66 | import org.eclipse.emf.common.util.EList; |
66 | import org.eclipse.xtend.lib.annotations.AccessorType; | 67 | import org.eclipse.xtend.lib.annotations.AccessorType; |
67 | import org.eclipse.xtend.lib.annotations.Accessors; | 68 | import org.eclipse.xtend.lib.annotations.Accessors; |
69 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
70 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
71 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
68 | import org.eclipse.xtext.xbase.lib.Extension; | 72 | import org.eclipse.xtext.xbase.lib.Extension; |
69 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 73 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
70 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | 74 | import org.eclipse.xtext.xbase.lib.IterableExtensions; |
@@ -118,18 +122,23 @@ public class Logic2VampireLanguageMapper { | |||
118 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); | 122 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); |
119 | } | 123 | } |
120 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | 124 | trace.relationDefinitions = this.collectRelationDefinitions(problem); |
121 | final Consumer<Relation> _function_3 = (Relation it) -> { | 125 | final Function1<Relation, Boolean> _function_3 = (Relation it) -> { |
126 | Class<? extends Relation> _class = it.getClass(); | ||
127 | return Boolean.valueOf(Objects.equal(_class, RelationDefinitionImpl.class)); | ||
128 | }; | ||
129 | this.toTrace(IterableExtensions.<Relation>filter(problem.getRelations(), _function_3), trace); | ||
130 | final Consumer<Relation> _function_4 = (Relation it) -> { | ||
122 | Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper(); | 131 | Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper(); |
123 | this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper); | 132 | this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper); |
124 | }; | 133 | }; |
125 | problem.getRelations().forEach(_function_3); | 134 | problem.getRelations().forEach(_function_4); |
126 | this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); | 135 | this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); |
127 | this.scopeMapper.transformScope(problem.getTypes(), config, trace); | 136 | this.scopeMapper.transformScope(problem.getTypes(), config, trace); |
128 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | 137 | trace.constantDefinitions = this.collectConstantDefinitions(problem); |
129 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { | 138 | final Consumer<ConstantDefinition> _function_5 = (ConstantDefinition it) -> { |
130 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); | 139 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); |
131 | }; | 140 | }; |
132 | Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_4); | 141 | Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_5); |
133 | EList<Assertion> _assertions = problem.getAssertions(); | 142 | EList<Assertion> _assertions = problem.getAssertions(); |
134 | for (final Assertion assertion : _assertions) { | 143 | for (final Assertion assertion : _assertions) { |
135 | this.transformAssertion(assertion, trace); | 144 | this.transformAssertion(assertion, trace); |
@@ -137,6 +146,49 @@ public class Logic2VampireLanguageMapper { | |||
137 | return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace); | 146 | return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace); |
138 | } | 147 | } |
139 | 148 | ||
149 | public void toTrace(final Iterable<Relation> relations, final Logic2VampireLanguageMapperTrace trace) { | ||
150 | final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList(); | ||
151 | for (final Relation rel : relations) { | ||
152 | { | ||
153 | final String[] nameArray = rel.getName().split(" "); | ||
154 | String relNameVar = ""; | ||
155 | int _length = nameArray.length; | ||
156 | boolean _equals = (_length == 3); | ||
157 | if (_equals) { | ||
158 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
159 | } else { | ||
160 | relNameVar = rel.getName(); | ||
161 | } | ||
162 | final String relName = relNameVar; | ||
163 | final RelationDefinition relDef = ((RelationDefinition) rel); | ||
164 | int _length_1 = ((Object[])Conversions.unwrapArray(rel.getParameters(), Object.class)).length; | ||
165 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length_1, true); | ||
166 | for (final Integer i : _doubleDotLessThan) { | ||
167 | { | ||
168 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
169 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
170 | it.setName(this.support.toIDMultiple("V", i.toString())); | ||
171 | }; | ||
172 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
173 | vars.add(v); | ||
174 | } | ||
175 | } | ||
176 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
177 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
178 | it.setConstant(this.support.toIDMultiple("r", relName)); | ||
179 | for (final VLSVariable v : vars) { | ||
180 | EList<VLSTerm> _terms = it.getTerms(); | ||
181 | VLSVariable _duplicate = this.support.duplicate(v); | ||
182 | _terms.add(_duplicate); | ||
183 | } | ||
184 | }; | ||
185 | final VLSFunction relFunc = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
186 | trace.relDef2Predicate.put(relDef, relFunc); | ||
187 | trace.predicate2RelDef.put(relFunc, relDef); | ||
188 | } | ||
189 | } | ||
190 | } | ||
191 | |||
140 | protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { | 192 | protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { |
141 | return null; | 193 | return null; |
142 | } | 194 | } |
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 { | |||
176 | } | 176 | } |
177 | }; | 177 | }; |
178 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_4); | 178 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_4); |
179 | trace.relDef2Predicate.put(r, rel); | ||
180 | trace.predicate2RelDef.put(rel, r); | ||
181 | it_2.setLeft(this.support.duplicate(rel)); | 179 | it_2.setLeft(this.support.duplicate(rel)); |
182 | it_2.setRight(compDefn); | 180 | it_2.setRight(compDefn); |
183 | }; | 181 | }; |
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 { | |||
34 | Statistics _createStatistics = this.resultFactory.createStatistics(); | 34 | Statistics _createStatistics = this.resultFactory.createStatistics(); |
35 | final Procedure1<Statistics> _function = (Statistics it) -> { | 35 | final Procedure1<Statistics> _function = (Statistics it) -> { |
36 | long _solverTime = solution.getSolverTime(); | 36 | long _solverTime = solution.getSolverTime(); |
37 | it.setTransformationTime(((int) _solverTime)); | 37 | it.setSolverTime(((int) _solverTime)); |
38 | it.setTransformationTime(((int) transformationTime)); | ||
38 | }; | 39 | }; |
39 | return ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function); | 40 | return ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function); |
40 | } | 41 | } |
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 { | |||
25 | final String VAMPNAME = "vampire.exe"; | 25 | final String VAMPNAME = "vampire.exe"; |
26 | final String TEMPNAME = "TEMP.tptp"; | 26 | final String TEMPNAME = "TEMP.tptp"; |
27 | final String OPTION = " --mode casc_sat -t 300 "; | 27 | final String OPTION = " --mode casc_sat -t 300 "; |
28 | final String SOLNNAME = (("_solution" + Integer.valueOf(configuration.typeScopes.maxNewElements)) + ".tptp"); | 28 | final String SOLNNAME = (((("solution" + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + ".tptp"); |
29 | final String PATH = "C:/cygwin64/bin"; | 29 | final String PATH = "C:/cygwin64/bin"; |
30 | final URI wsURI = workspace.getWorkspaceURI(); | 30 | final URI wsURI = workspace.getWorkspaceURI(); |
31 | final String tempLoc = (wsURI + TEMPNAME); | 31 | final String tempLoc = (wsURI + TEMPNAME); |