diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend | 102 |
1 files changed, 102 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend new file mode 100644 index 00000000..64484b88 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend | |||
@@ -0,0 +1,102 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage | ||
11 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
12 | import java.io.PrintWriter | ||
13 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | ||
14 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper | ||
15 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes | ||
16 | |||
17 | class VampireSolver extends LogicReasoner{ | ||
18 | |||
19 | new() { | ||
20 | VampireLanguagePackage.eINSTANCE.eClass | ||
21 | val x = new VampireLanguageStandaloneSetupGenerated | ||
22 | VampireLanguageStandaloneSetup::doSetup() | ||
23 | } | ||
24 | |||
25 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) | ||
26 | // //not for now | ||
27 | // val VampireHandler handler = new VampireHandler | ||
28 | // val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | ||
29 | |||
30 | val fileName = "problem.tptp" | ||
31 | |||
32 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | ||
33 | val vampireConfig = configuration.asConfig | ||
34 | |||
35 | // Start: Logic -> Vampire mapping | ||
36 | val transformationStart = System.currentTimeMillis | ||
37 | //TODO | ||
38 | val result = forwardMapper.transformProblem(problem,vampireConfig) | ||
39 | val vampireProblem = result.output | ||
40 | val forwardTrace = result.trace | ||
41 | |||
42 | var String fileURI = null; | ||
43 | var String vampireCode = null; | ||
44 | if(vampireConfig.writeToFile) { | ||
45 | fileURI = workspace.writeModel(vampireProblem,fileName).toFileString | ||
46 | } else { | ||
47 | vampireCode = workspace.writeModelToString(vampireProblem,fileName) | ||
48 | } | ||
49 | val transformationTime = System.currentTimeMillis - transformationStart | ||
50 | // Finish: Logic -> Vampire mapping | ||
51 | |||
52 | //Creates a file containing the tptp code after transformation | ||
53 | val out = new PrintWriter("output/files/vampireCode.tptp") | ||
54 | out.println(vampireCode) | ||
55 | out.close() | ||
56 | |||
57 | |||
58 | /* | ||
59 | * not for now -> Start: Solving Alloy problem | ||
60 | * | ||
61 | // Start: Solving Alloy problem | ||
62 | val solverStart = System.currentTimeMillis | ||
63 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode) | ||
64 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | ||
65 | val solverFinish = System.currentTimeMillis-solverStart | ||
66 | // Finish: Solving Alloy problem | ||
67 | |||
68 | if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) | ||
69 | |||
70 | return logicResult | ||
71 | */ | ||
72 | |||
73 | return null // for now | ||
74 | } | ||
75 | |||
76 | def asConfig(LogicSolverConfiguration configuration){ | ||
77 | if(configuration instanceof VampireSolverConfiguration) { | ||
78 | return configuration | ||
79 | } else { | ||
80 | throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''') | ||
81 | } | ||
82 | } | ||
83 | |||
84 | // /* | ||
85 | // * not for now | ||
86 | // * | ||
87 | override getInterpretations(ModelResult modelResult) { | ||
88 | //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] | ||
89 | // val sols = modelResult.representation// as List<A4Solution> | ||
90 | // //val res = answers.map | ||
91 | // sols.map[ | ||
92 | // new VampireModelInterpretation( | ||
93 | // forwardMapper.typeMapper.typeInterpreter, | ||
94 | // it as A4Solution, | ||
95 | // forwardMapper, | ||
96 | // modelResult.trace as Logic2AlloyLanguageMapperTrace | ||
97 | // ) | ||
98 | // ] | ||
99 | } | ||
100 | // */ | ||
101 | |||
102 | } \ No newline at end of file | ||