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 | 116 |
1 files changed, 94 insertions, 22 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 85b81a8c..31aa091c 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 | |||
@@ -4,18 +4,20 @@ 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 | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution | 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 |
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation | 11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
20 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 22 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
21 | 23 | ||
@@ -30,18 +32,20 @@ class VampireSolver extends LogicReasoner { | |||
30 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper | 32 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper |
31 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | 33 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper |
32 | val VampireHandler handler = new VampireHandler | 34 | val VampireHandler handler = new VampireHandler |
35 | val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
36 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | ||
37 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
33 | 38 | ||
34 | // var fileName = "problem.tptp" | 39 | // var fileName = "problem.tptp" |
35 | |||
36 | // def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { | 40 | // def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { |
37 | // fileName = location + fileName | 41 | // fileName = location + fileName |
38 | // solve(problem, config, workspace) | 42 | // solve(problem, config, workspace) |
39 | // } | 43 | // } |
40 | |||
41 | override solve(LogicProblem problem, LogicSolverConfiguration config, | 44 | override solve(LogicProblem problem, LogicSolverConfiguration config, |
42 | ReasonerWorkspace workspace) throws LogicReasonerException { | 45 | ReasonerWorkspace workspace) throws LogicReasonerException { |
43 | val vampireConfig = config.asConfig | 46 | val vampireConfig = config.asConfig |
44 | var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + vampireConfig.typeScopes.maxNewElements + ".tptp" | 47 | var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + |
48 | vampireConfig.typeScopes.maxNewElements + ".tptp" | ||
45 | 49 | ||
46 | // Start: Logic -> Vampire mapping | 50 | // Start: Logic -> Vampire mapping |
47 | val transformationStart = System.currentTimeMillis | 51 | val transformationStart = System.currentTimeMillis |
@@ -55,8 +59,6 @@ class VampireSolver extends LogicReasoner { | |||
55 | var String fileURI = null; | 59 | var String fileURI = null; |
56 | var String vampireCode = null; | 60 | var String vampireCode = null; |
57 | vampireCode = workspace.writeModelToString(vampireProblem, fileName) | 61 | vampireCode = workspace.writeModelToString(vampireProblem, fileName) |
58 | |||
59 | |||
60 | 62 | ||
61 | val writeFile = ( | 63 | val writeFile = ( |
62 | vampireConfig.documentationLevel === DocumentationLevel::NORMAL || | 64 | vampireConfig.documentationLevel === DocumentationLevel::NORMAL || |
@@ -73,24 +75,94 @@ class VampireSolver extends LogicReasoner { | |||
73 | // println(model) | 75 | // println(model) |
74 | // Finish: Logic -> Vampire mapping | 76 | // Finish: Logic -> Vampire mapping |
75 | if (vampireConfig.genModel) { | 77 | if (vampireConfig.genModel) { |
76 | 78 | if (vampireConfig.server) { | |
77 | // Start: Solving .tptp problem | 79 | val form = support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit) |
78 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | 80 | var response = newArrayList |
79 | // Finish: Solving .tptp problem | 81 | var ind = 0 |
80 | // Start: Vampire -> Logic mapping | 82 | var done = false |
81 | val backTransformationStart = System.currentTimeMillis | 83 | print(" ") |
82 | // Backwards Mapper | 84 | while (!done) { |
83 | val logicResult = backwardMapper.transformOutput(problem, | 85 | print("(x)") |
84 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) | 86 | done = false |
85 | 87 | response = support.sendPost(form) | |
86 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | 88 | |
87 | // Finish: Vampire -> Logic Mapping | 89 | var responseFound = false |
90 | ind = 0 | ||
91 | while (!responseFound) { | ||
92 | var line = response.get(ind) | ||
93 | if (line.length >= 5 && line.substring(0, 5) == "ERROR") { | ||
94 | done = false | ||
95 | responseFound = true | ||
96 | } else { | ||
97 | if (line == "</PRE>") { | ||
98 | done = true | ||
99 | responseFound = true | ||
100 | } | ||
101 | } | ||
102 | ind++ | ||
103 | } | ||
104 | } | ||
105 | val satRaw = response.get(ind - 3) | ||
106 | val modRaw = response.get(ind - 2) | ||
107 | |||
108 | val sat = newArrayList(satRaw.split(" ")) | ||
109 | val mod = newArrayList(modRaw.split(" ")) | ||
110 | |||
111 | val satOut = sat.get(1) | ||
112 | val modOut = mod.get(1) | ||
113 | val satTime = sat.get(2) | ||
114 | val modTime = mod.get(2) | ||
115 | |||
116 | println() | ||
117 | println(sat) | ||
118 | println(mod) | ||
119 | |||
120 | return createModelResult => [ | ||
121 | it.problem = null | ||
122 | it.representation += createVampireModel => [] | ||
123 | it.trace = trace | ||
124 | it.statistics = createStatistics => [ | ||
125 | it.transformationTime = transformationTime as int | ||
126 | it.entries += createStringStatisticEntry => [ | ||
127 | it.name = "satOut" | ||
128 | it.value = satOut | ||
129 | ] | ||
130 | it.entries += createRealStatisticEntry => [ | ||
131 | it.name = "satTime" | ||
132 | it.value = Double.parseDouble(satTime) | ||
133 | ] | ||
134 | it.entries += createStringStatisticEntry => [ | ||
135 | it.name = "modOut" | ||
136 | it.value = modOut | ||
137 | ] | ||
138 | it.entries += createRealStatisticEntry => [ | ||
139 | it.name = "modTime" | ||
140 | it.value = Double.parseDouble(modTime) | ||
141 | ] | ||
142 | |||
143 | ] | ||
144 | ] | ||
145 | |||
146 | // return newArrayList(line1, line2) | ||
147 | } else { | ||
148 | |||
149 | // Start: Solving .tptp problem | ||
150 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | ||
151 | // Finish: Solving .tptp problem | ||
152 | // Start: Vampire -> Logic mapping | ||
153 | val backTransformationStart = System.currentTimeMillis | ||
154 | // Backwards Mapper | ||
155 | val logicResult = backwardMapper.transformOutput(problem, | ||
156 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) | ||
157 | |||
158 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | ||
159 | // Finish: Vampire -> Logic Mapping | ||
88 | // print(vampSol.generatedModel.tfformulas.size) | 160 | // print(vampSol.generatedModel.tfformulas.size) |
89 | return logicResult // currently only a ModelResult | 161 | return logicResult // currently only a ModelResult |
162 | } | ||
90 | } | 163 | } |
91 | 164 | return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, | |
92 | return backwardMapper.transformOutput(problem, | 165 | new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) |
93 | vampireConfig.solutionScope.numberOfRequiredSolution, new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) | ||
94 | } | 166 | } |
95 | 167 | ||
96 | def asConfig(LogicSolverConfiguration configuration) { | 168 | def asConfig(LogicSolverConfiguration configuration) { |