diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-08-29 16:54:53 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:41:41 -0400 |
commit | 5cfe202ab86f117e35b286cfadf7f8301bce3a43 (patch) | |
tree | d3d6bc6b07a841dac02af22523c37327c309a119 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner | |
parent | VAMPIRE: adapt grammar to Vampire solution + get model from text (diff) | |
download | VIATRA-Generator-5cfe202ab86f117e35b286cfadf7f8301bce3a43.tar.gz VIATRA-Generator-5cfe202ab86f117e35b286cfadf7f8301bce3a43.tar.zst VIATRA-Generator-5cfe202ab86f117e35b286cfadf7f8301bce3a43.zip |
VAMPIRE: setup structure of model interpretation
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner')
22 files changed, 154 insertions, 111 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 index 1fd40801..0ec4d0da 100644 --- 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 | |||
@@ -3,11 +3,12 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner | |||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | 3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup |
4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated | 4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper | 8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler | 9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler |
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException |
@@ -15,7 +16,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | |||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
17 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
18 | import org.eclipse.emf.ecore.resource.Resource | 19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
19 | 20 | ||
20 | class VampireSolver extends LogicReasoner { | 21 | class VampireSolver extends LogicReasoner { |
21 | 22 | ||
@@ -71,21 +72,21 @@ class VampireSolver extends LogicReasoner { | |||
71 | // Result as String | 72 | // Result as String |
72 | val transformationTime = System.currentTimeMillis - transformationStart | 73 | val transformationTime = System.currentTimeMillis - transformationStart |
73 | // Finish: Logic -> Vampire mapping | 74 | // Finish: Logic -> Vampire mapping |
75 | |||
74 | // Start: Solving .tptp problem | 76 | // Start: Solving .tptp problem |
75 | val solverStart = System.currentTimeMillis | 77 | val solverStart = System.currentTimeMillis |
76 | // Calling Solver (Currently Manually) | 78 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) |
77 | val result2 = handler.callSolver(vampireProblem, workspace, vampireConfig) | ||
78 | // val result2 = null | ||
79 | val solvingTime = System.currentTimeMillis - solverStart | 79 | val solvingTime = System.currentTimeMillis - solverStart |
80 | // TODO | 80 | // Finish: Solving .tptp problem |
81 | // val backTransformationStart = System.currentTimeMillis | 81 | |
82 | // // Backwards Mapper | 82 | // Start: Vampire -> Logic mapping |
83 | // val logicResult = backwardMapper.transformOutput(problem, config.solutionScope.numberOfRequiredSolution, | 83 | val backTransformationStart = System.currentTimeMillis |
84 | // result2, forwardTrace, transformationTime) | 84 | // Backwards Mapper |
85 | // | 85 | val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime) |
86 | // val backTransformationTime = System.currentTimeMillis - backTransformationStart | 86 | |
87 | // Finish: Solving Alloy problem | 87 | val backTransformationTime = System.currentTimeMillis - backTransformationStart |
88 | return null | 88 | // Finish: Vampire -> Logic Mapping |
89 | return logicResult //currently only a ModelResult | ||
89 | } | 90 | } |
90 | 91 | ||
91 | def asConfig(LogicSolverConfiguration configuration) { | 92 | def asConfig(LogicSolverConfiguration configuration) { |
@@ -100,17 +101,17 @@ class VampireSolver extends LogicReasoner { | |||
100 | // * not for now | 101 | // * not for now |
101 | // * | 102 | // * |
102 | override getInterpretations(ModelResult modelResult) { | 103 | override getInterpretations(ModelResult modelResult) { |
103 | // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] | 104 | // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] |
104 | // val sols = modelResult.representation// as List<A4Solution> | 105 | val sols = modelResult.representation// as List<A4Solution> |
105 | // //val res = answers.map | 106 | //val res = answers.map |
106 | // sols.map[ | 107 | sols.map[ |
107 | // new VampireModelInterpretation( | 108 | new VampireModelInterpretation( |
108 | // forwardMapper.typeMapper.typeInterpreter, | 109 | // forwardMapper.typeMapper.typeInterpreter, |
109 | // it as A4Solution, | 110 | it as VampireModel, |
110 | // forwardMapper, | 111 | // forwardMapper, |
111 | // modelResult.trace as Logic2AlloyLanguageMapperTrace | 112 | modelResult.trace as Logic2VampireLanguageMapperTrace |
112 | // ) | 113 | ) |
113 | // ] | 114 | ] |
114 | } | 115 | } |
115 | // */ | 116 | // */ |
116 | } | 117 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend index 9c9e65b4..a0084204 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend | |||
@@ -4,39 +4,24 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | |||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory |
5 | 5 | ||
6 | class Vampire2LogicMapper { | 6 | class Vampire2LogicMapper { |
7 | } | 7 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE |
8 | // val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | 8 | |
9 | // | ||
10 | // public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) { | ||
11 | // val models = vampireSolution.aswers.map[it.key].toList | ||
12 | // | ||
13 | // if(!monitoredAlloySolution.finishedBeforeTimeout) { | ||
14 | // return createInsuficientResourcesResult => [ | ||
15 | // it.problem = problem | ||
16 | // it.representation += models | ||
17 | // it.trace = trace | ||
18 | // it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
19 | // ] | ||
20 | // } else { | ||
21 | // if(models.last.satisfiable || requiredNumberOfSolution == -1) { | ||
22 | // return createModelResult => [ | ||
23 | // it.problem = problem | ||
24 | // it.representation += models | ||
25 | // it.trace = trace | ||
26 | // it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
27 | // ] | ||
28 | // } else { | ||
29 | // return createInconsistencyResult => [ | ||
30 | // it.problem = problem | ||
31 | // it.representation += models | ||
32 | // it.trace = trace | ||
33 | // it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
34 | // ] | ||
35 | // } | ||
36 | // } | ||
37 | // } | ||
38 | // | 9 | // |
39 | // def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { | 10 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, |
11 | MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace, | ||
12 | long transformationTime) { | ||
13 | |||
14 | // ModelRsult implements LogicResult | ||
15 | return createModelResult => [ | ||
16 | it.problem = problem | ||
17 | it.representation += monitoredVampireSolution.generatedModel | ||
18 | it.trace = trace | ||
19 | it.statistics = transformStatistics(monitoredVampireSolution, transformationTime) | ||
20 | ] | ||
21 | } | ||
22 | |||
23 | def transformStatistics(MonitoredVampireSolution solution, long transformationTime) { | ||
24 | return createStatistics | ||
40 | // createStatistics => [ | 25 | // createStatistics => [ |
41 | // it.transformationTime = transformationTime as int | 26 | // it.transformationTime = transformationTime as int |
42 | // for(solutionIndex : 0..<solution.aswers.size) { | 27 | // for(solutionIndex : 0..<solution.aswers.size) { |
@@ -59,9 +44,6 @@ class Vampire2LogicMapper { | |||
59 | // it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]''' | 44 | // it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]''' |
60 | // ] | 45 | // ] |
61 | // ] | 46 | // ] |
62 | // } | 47 | } |
63 | // | 48 | |
64 | // def sum(Iterable<Long> ints) { | 49 | } |
65 | // ints.reduce[p1, p2|p1+p2] | ||
66 | // } | ||
67 | //} | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend index f0426245..ce672211 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | |||
@@ -25,11 +25,12 @@ class VampireSolverException extends Exception { | |||
25 | } | 25 | } |
26 | } | 26 | } |
27 | 27 | ||
28 | @Data class VampireSolutionModel { | 28 | @Data class MonitoredVampireSolution { |
29 | // List<String> warnings | 29 | // List<String> warnings |
30 | // List<String> debugs | 30 | // List<String> debugs |
31 | // long kodkodTime | 31 | // long kodkodTime |
32 | // val List<Pair<A4Solution, Long>> aswers | 32 | // val List<Pair<A4Solution, Long>> aswers |
33 | val VampireModel generatedModel | ||
33 | // val boolean finishedBeforeTimeout | 34 | // val boolean finishedBeforeTimeout |
34 | } | 35 | } |
35 | 36 | ||
@@ -76,12 +77,10 @@ class VampireHandler { | |||
76 | // 5. determine and return whether or not finite model was found | 77 | // 5. determine and return whether or not finite model was found |
77 | // 6. save solution as a .tptp model | 78 | // 6. save solution as a .tptp model |
78 | val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents | 79 | val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents |
79 | |||
80 | |||
81 | 80 | ||
82 | println((root.get(0) as VampireModelImpl ).comments) | 81 | // println((root.get(0) as VampireModel ).comments) |
83 | 82 | ||
84 | return root | 83 | return new MonitoredVampireSolution(root.get(0) as VampireModel) |
85 | 84 | ||
86 | /* | 85 | /* |
87 | * //Prepare | 86 | * //Prepare |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend new file mode 100644 index 00000000..c2cffa6b --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend | |||
@@ -0,0 +1,49 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
10 | |||
11 | class VampireModelInterpretation implements LogicModelInterpretation { | ||
12 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
13 | |||
14 | protected val Logic2VampireLanguageMapperTrace forwardTrace; | ||
15 | |||
16 | |||
17 | public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) { | ||
18 | this.forwardTrace = trace | ||
19 | } | ||
20 | |||
21 | override getElements(Type type) { | ||
22 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
23 | } | ||
24 | |||
25 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | ||
26 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
27 | } | ||
28 | |||
29 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | ||
30 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
31 | } | ||
32 | |||
33 | override getInterpretation(ConstantDeclaration constant) { | ||
34 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
35 | } | ||
36 | |||
37 | override getAllIntegersInStructure() { | ||
38 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
39 | } | ||
40 | |||
41 | override getAllRealsInStructure() { | ||
42 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
43 | } | ||
44 | |||
45 | override getAllStringsInStructure() { | ||
46 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
47 | } | ||
48 | |||
49 | } \ No newline at end of file | ||
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 b9600616..499504af 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 43992ea0..298a6c08 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 410b47ed..a7780e97 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 | |||
@@ -5,8 +5,10 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated; | |||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 5 | 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.MonitoredVampireSolution; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | 9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; |
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; |
11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
@@ -21,9 +23,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | |||
21 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 23 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
22 | import java.util.List; | 24 | import java.util.List; |
23 | import org.eclipse.emf.common.util.EList; | 25 | import org.eclipse.emf.common.util.EList; |
24 | import org.eclipse.emf.ecore.EObject; | ||
25 | import org.eclipse.xtend2.lib.StringConcatenation; | 26 | import org.eclipse.xtend2.lib.StringConcatenation; |
26 | import org.eclipse.xtext.xbase.lib.Exceptions; | 27 | import org.eclipse.xtext.xbase.lib.Exceptions; |
28 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
29 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
27 | 30 | ||
28 | @SuppressWarnings("all") | 31 | @SuppressWarnings("all") |
29 | public class VampireSolver extends LogicReasoner { | 32 | public class VampireSolver extends LogicReasoner { |
@@ -72,10 +75,14 @@ public class VampireSolver extends LogicReasoner { | |||
72 | long _currentTimeMillis = System.currentTimeMillis(); | 75 | long _currentTimeMillis = System.currentTimeMillis(); |
73 | final long transformationTime = (_currentTimeMillis - transformationStart); | 76 | final long transformationTime = (_currentTimeMillis - transformationStart); |
74 | final long solverStart = System.currentTimeMillis(); | 77 | final long solverStart = System.currentTimeMillis(); |
75 | final EList<EObject> result2 = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | 78 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); |
76 | long _currentTimeMillis_1 = System.currentTimeMillis(); | 79 | long _currentTimeMillis_1 = System.currentTimeMillis(); |
77 | final long solvingTime = (_currentTimeMillis_1 - solverStart); | 80 | final long solvingTime = (_currentTimeMillis_1 - solverStart); |
78 | return null; | 81 | final long backTransformationStart = System.currentTimeMillis(); |
82 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | ||
83 | long _currentTimeMillis_2 = System.currentTimeMillis(); | ||
84 | final long backTransformationTime = (_currentTimeMillis_2 - backTransformationStart); | ||
85 | return logicResult; | ||
79 | } | 86 | } |
80 | 87 | ||
81 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | 88 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { |
@@ -93,6 +100,17 @@ public class VampireSolver extends LogicReasoner { | |||
93 | 100 | ||
94 | @Override | 101 | @Override |
95 | public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) { | 102 | public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) { |
96 | return null; | 103 | List<VampireModelInterpretation> _xblockexpression = null; |
104 | { | ||
105 | final EList<Object> sols = modelResult.getRepresentation(); | ||
106 | final Function1<Object, VampireModelInterpretation> _function = (Object it) -> { | ||
107 | Object _trace = modelResult.getTrace(); | ||
108 | return new VampireModelInterpretation( | ||
109 | ((VampireModel) it), | ||
110 | ((Logic2VampireLanguageMapperTrace) _trace)); | ||
111 | }; | ||
112 | _xblockexpression = ListExtensions.<Object, VampireModelInterpretation>map(sols, _function); | ||
113 | } | ||
114 | return _xblockexpression; | ||
97 | } | 115 | } |
98 | } | 116 | } |
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 19608361..863b572e 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/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index 791a9524..410f2550 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.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 89003c27..b1b39a4f 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 b37d993a..3710e753 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 45afcecc..9dc7abaf 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 0f4dc63a..7029d196 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 ab58fcab..03aead59 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 cf19663e..62960704 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 f8b35528..56a10b3c 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 0b2cb192..319f863c 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/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index ffd37ea3..3b6009bb 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.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/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 9ddc7bd0..d8329084 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.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.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java index f4b5a1d2..29a2ecea 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 | |||
@@ -1,5 +1,36 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; | ||
10 | import org.eclipse.emf.common.util.EList; | ||
11 | import org.eclipse.xtext.xbase.lib.Extension; | ||
12 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
13 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
14 | |||
3 | @SuppressWarnings("all") | 15 | @SuppressWarnings("all") |
4 | public class Vampire2LogicMapper { | 16 | public class Vampire2LogicMapper { |
17 | @Extension | ||
18 | private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE; | ||
19 | |||
20 | public ModelResult transformOutput(final LogicProblem problem, final int requiredNumberOfSolution, final MonitoredVampireSolution monitoredVampireSolution, final Logic2VampireLanguageMapperTrace trace, final long transformationTime) { | ||
21 | ModelResult _createModelResult = this.resultFactory.createModelResult(); | ||
22 | final Procedure1<ModelResult> _function = (ModelResult it) -> { | ||
23 | it.setProblem(problem); | ||
24 | EList<Object> _representation = it.getRepresentation(); | ||
25 | VampireModel _generatedModel = monitoredVampireSolution.getGeneratedModel(); | ||
26 | _representation.add(_generatedModel); | ||
27 | it.setTrace(trace); | ||
28 | it.setStatistics(this.transformStatistics(monitoredVampireSolution, transformationTime)); | ||
29 | }; | ||
30 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function); | ||
31 | } | ||
32 | |||
33 | public Statistics transformStatistics(final MonitoredVampireSolution solution, final long transformationTime) { | ||
34 | return this.resultFactory.createStatistics(); | ||
35 | } | ||
5 | } | 36 | } |
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 7f6ce1c6..4764ae28 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 | |||
@@ -1,9 +1,8 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl; | ||
7 | import com.google.common.base.Objects; | 6 | import com.google.common.base.Objects; |
8 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 7 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
9 | import java.io.BufferedReader; | 8 | import java.io.BufferedReader; |
@@ -16,11 +15,10 @@ import org.eclipse.emf.ecore.EObject; | |||
16 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 15 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
17 | import org.eclipse.xtext.xbase.lib.Conversions; | 16 | import org.eclipse.xtext.xbase.lib.Conversions; |
18 | import org.eclipse.xtext.xbase.lib.Exceptions; | 17 | import org.eclipse.xtext.xbase.lib.Exceptions; |
19 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
20 | 18 | ||
21 | @SuppressWarnings("all") | 19 | @SuppressWarnings("all") |
22 | public class VampireHandler { | 20 | public class VampireHandler { |
23 | public EList<EObject> callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) { | 21 | public MonitoredVampireSolution callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) { |
24 | try { | 22 | try { |
25 | final String CMD = "cmd /c "; | 23 | final String CMD = "cmd /c "; |
26 | final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; | 24 | final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; |
@@ -48,8 +46,7 @@ public class VampireHandler { | |||
48 | workspace.getFile(TEMPNAME).delete(); | 46 | workspace.getFile(TEMPNAME).delete(); |
49 | final EList<EObject> root = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents(); | 47 | final EList<EObject> root = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents(); |
50 | EObject _get = root.get(0); | 48 | EObject _get = root.get(0); |
51 | InputOutput.<EList<VLSComment>>println(((VampireModelImpl) _get).getComments()); | 49 | return new MonitoredVampireSolution(((VampireModel) _get)); |
52 | return root; | ||
53 | } catch (Throwable _e) { | 50 | } catch (Throwable _e) { |
54 | throw Exceptions.sneakyThrow(_e); | 51 | throw Exceptions.sneakyThrow(_e); |
55 | } | 52 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java deleted file mode 100644 index 3c43c4ea..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java +++ /dev/null | |||
@@ -1,34 +0,0 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import org.eclipse.xtend.lib.annotations.Data; | ||
4 | import org.eclipse.xtext.xbase.lib.Pure; | ||
5 | import org.eclipse.xtext.xbase.lib.util.ToStringBuilder; | ||
6 | |||
7 | @Data | ||
8 | @SuppressWarnings("all") | ||
9 | public class VampireSolutionModel { | ||
10 | @Override | ||
11 | @Pure | ||
12 | public int hashCode() { | ||
13 | return 1; | ||
14 | } | ||
15 | |||
16 | @Override | ||
17 | @Pure | ||
18 | public boolean equals(final Object obj) { | ||
19 | if (this == obj) | ||
20 | return true; | ||
21 | if (obj == null) | ||
22 | return false; | ||
23 | if (getClass() != obj.getClass()) | ||
24 | return false; | ||
25 | return true; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | @Pure | ||
30 | public String toString() { | ||
31 | ToStringBuilder b = new ToStringBuilder(this); | ||
32 | return b.toString(); | ||
33 | } | ||
34 | } | ||