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 | 46 |
1 files changed, 21 insertions, 25 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 81cae109..e1a1ca6e 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 | |||
@@ -6,6 +6,8 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | |||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes; | 8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes; |
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; |
@@ -17,10 +19,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | |||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
19 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 21 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
20 | import java.io.PrintWriter; | ||
21 | import java.util.List; | 22 | import java.util.List; |
22 | import org.eclipse.xtend2.lib.StringConcatenation; | 23 | import org.eclipse.xtend2.lib.StringConcatenation; |
23 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
24 | 24 | ||
25 | @SuppressWarnings("all") | 25 | @SuppressWarnings("all") |
26 | public class VampireSolver extends LogicReasoner { | 26 | public class VampireSolver extends LogicReasoner { |
@@ -32,32 +32,28 @@ public class VampireSolver extends LogicReasoner { | |||
32 | 32 | ||
33 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); | 33 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); |
34 | 34 | ||
35 | private final String fileName = "problem.tptp"; | 35 | private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper(); |
36 | |||
37 | private final VampireHandler handler = new VampireHandler(); | ||
38 | |||
39 | private final String fileName = "vampireProblem.tptp"; | ||
36 | 40 | ||
37 | @Override | 41 | @Override |
38 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration configuration, final ReasonerWorkspace workspace) throws LogicReasonerException { | 42 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { |
39 | try { | 43 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); |
40 | final VampireSolverConfiguration vampireConfig = this.asConfig(configuration); | 44 | final long transformationStart = System.currentTimeMillis(); |
41 | final long transformationStart = System.currentTimeMillis(); | 45 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); |
42 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | 46 | final VampireModel vampireProblem = result.getOutput(); |
43 | final VampireModel vampireProblem = result.getOutput(); | 47 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); |
44 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | 48 | String fileURI = null; |
45 | String fileURI = null; | 49 | String vampireCode = null; |
46 | String vampireCode = null; | 50 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); |
47 | if (vampireConfig.writeToFile) { | 51 | if (vampireConfig.writeToFile) { |
48 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); | 52 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); |
49 | } else { | ||
50 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); | ||
51 | } | ||
52 | long _currentTimeMillis = System.currentTimeMillis(); | ||
53 | final long transformationTime = (_currentTimeMillis - transformationStart); | ||
54 | final PrintWriter out = new PrintWriter("output/files/vampireCode.tptp"); | ||
55 | out.println(vampireCode); | ||
56 | out.close(); | ||
57 | return null; | ||
58 | } catch (Throwable _e) { | ||
59 | throw Exceptions.sneakyThrow(_e); | ||
60 | } | 53 | } |
54 | long _currentTimeMillis = System.currentTimeMillis(); | ||
55 | final long transformationTime = (_currentTimeMillis - transformationStart); | ||
56 | return null; | ||
61 | } | 57 | } |
62 | 58 | ||
63 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | 59 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { |