diff options
author | 2019-08-29 16:54:53 -0400 | |
---|---|---|
committer | 2019-08-29 16:54:53 -0400 | |
commit | 9c1450f069049a5f3e62c6eaa14cf3f5832eeadd (patch) | |
tree | c793d23b3234a7d60ef85bf99df61810354e28aa /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner | |
parent | VAMPIRE: adapt grammar to Vampire solution + get model from text (diff) | |
download | VIATRA-Generator-9c1450f069049a5f3e62c6eaa14cf3f5832eeadd.tar.gz VIATRA-Generator-9c1450f069049a5f3e62c6eaa14cf3f5832eeadd.tar.zst VIATRA-Generator-9c1450f069049a5f3e62c6eaa14cf3f5832eeadd.zip |
VAMPIRE: setup structure of model interpretation
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner')
4 files changed, 98 insertions, 67 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 | ||