diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java | 39 |
1 files changed, 15 insertions, 24 deletions
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 c3e185f5..432b14c3 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 | |||
@@ -24,7 +24,6 @@ import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | |||
24 | import java.util.List; | 24 | import java.util.List; |
25 | import org.eclipse.emf.common.util.EList; | 25 | import org.eclipse.emf.common.util.EList; |
26 | import org.eclipse.xtend2.lib.StringConcatenation; | 26 | import org.eclipse.xtend2.lib.StringConcatenation; |
27 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
28 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 27 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
29 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 28 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
30 | 29 | ||
@@ -42,24 +41,10 @@ public class VampireSolver extends LogicReasoner { | |||
42 | 41 | ||
43 | private final VampireHandler handler = new VampireHandler(); | 42 | private final VampireHandler handler = new VampireHandler(); |
44 | 43 | ||
45 | private String fileName = "problem.tptp"; | ||
46 | |||
47 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace, final String location) { | ||
48 | try { | ||
49 | LogicResult _xblockexpression = null; | ||
50 | { | ||
51 | this.fileName = (location + this.fileName); | ||
52 | _xblockexpression = this.solve(problem, config, workspace); | ||
53 | } | ||
54 | return _xblockexpression; | ||
55 | } catch (Throwable _e) { | ||
56 | throw Exceptions.sneakyThrow(_e); | ||
57 | } | ||
58 | } | ||
59 | |||
60 | @Override | 44 | @Override |
61 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { | 45 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { |
62 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); | 46 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); |
47 | String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp"); | ||
63 | final long transformationStart = System.currentTimeMillis(); | 48 | final long transformationStart = System.currentTimeMillis(); |
64 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | 49 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); |
65 | long _currentTimeMillis = System.currentTimeMillis(); | 50 | long _currentTimeMillis = System.currentTimeMillis(); |
@@ -68,18 +53,24 @@ public class VampireSolver extends LogicReasoner { | |||
68 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | 53 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); |
69 | String fileURI = null; | 54 | String fileURI = null; |
70 | String vampireCode = null; | 55 | String vampireCode = null; |
71 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); | 56 | vampireCode = workspace.writeModelToString(vampireProblem, fileName); |
72 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || | 57 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || |
73 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); | 58 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); |
74 | if (writeFile) { | 59 | if (writeFile) { |
75 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); | 60 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString(); |
61 | } | ||
62 | if (vampireConfig.genModel) { | ||
63 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | ||
64 | final long backTransformationStart = System.currentTimeMillis(); | ||
65 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, | ||
66 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | ||
67 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
68 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | ||
69 | return logicResult; | ||
76 | } | 70 | } |
77 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | 71 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); |
78 | final long backTransformationStart = System.currentTimeMillis(); | 72 | return this.backwardMapper.transformOutput(problem, |
79 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | 73 | vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); |
80 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
81 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | ||
82 | return logicResult; | ||
83 | } | 74 | } |
84 | 75 | ||
85 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | 76 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { |