1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
package ca.mcgill.ecse.dslreasoner.vampire.reasoner
import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
class VampireSolver extends LogicReasoner {
new() {
VampireLanguagePackage.eINSTANCE.eClass
val x = new VampireLanguageStandaloneSetupGenerated
VampireLanguageStandaloneSetup::doSetup()
}
val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper
val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
val VampireHandler handler = new VampireHandler
var fileName = "problem.tptp"
def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) {
fileName = location + fileName
solve(problem, config, workspace)
}
override solve(LogicProblem problem, LogicSolverConfiguration config,
ReasonerWorkspace workspace) throws LogicReasonerException {
val vampireConfig = config.asConfig
// Start: Logic -> Vampire mapping
val transformationStart = System.currentTimeMillis
// TODO
val result = forwardMapper.transformProblem(problem, vampireConfig)
val vampireProblem = result.output
val forwardTrace = result.trace
var String fileURI = null;
var String vampireCode = null;
vampireCode = workspace.writeModelToString(vampireProblem, fileName)
val writeFile = (
vampireConfig.documentationLevel === DocumentationLevel::NORMAL ||
vampireConfig.documentationLevel === DocumentationLevel::FULL)
if (writeFile) {
fileURI = workspace.writeModel(vampireProblem, fileName).toFileString
}
// Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("tptp", new VampireLanguageFactoryImpl)
//// val Resource resource = Resource.
//// Resource.getResource(wsURI+"problem.tptp") as Resource
//// resource
// val model = workspace.readModel(VampireModel, "problem.tptp").eResource.contents
// println(model)
// Result as String
val transformationTime = System.currentTimeMillis - transformationStart
// Finish: Logic -> Vampire mapping
// Start: Solving .tptp problem
val solverStart = System.currentTimeMillis
val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
val solvingTime = System.currentTimeMillis - solverStart
// Finish: Solving .tptp problem
// Start: Vampire -> Logic mapping
val backTransformationStart = System.currentTimeMillis
// Backwards Mapper
val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime)
val backTransformationTime = System.currentTimeMillis - backTransformationStart
// Finish: Vampire -> Logic Mapping
return logicResult //currently only a ModelResult
}
def asConfig(LogicSolverConfiguration configuration) {
if (configuration instanceof VampireSolverConfiguration) {
return configuration
} else {
throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''')
}
}
// /*
// * not for now
// *
override getInterpretations(ModelResult modelResult) {
// val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
val sols = modelResult.representation// as List<A4Solution>
//val res = answers.map
sols.map[
new VampireModelInterpretation(
// forwardMapper.typeMapper.typeInterpreter,
it as VampireModel,
// forwardMapper,
modelResult.trace as Logic2VampireLanguageMapperTrace
)
]
}
// */
}
|
