diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse')
3 files changed, 48 insertions, 8 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend index 4c2f1952..1fda24d9 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend | |||
@@ -24,7 +24,8 @@ enum BackendSolver { | |||
24 | IPROVER, | 24 | IPROVER, |
25 | PARADOX, | 25 | PARADOX, |
26 | VAMPIRE, | 26 | VAMPIRE, |
27 | Z3 | 27 | Z3, |
28 | LOCVAMP | ||
28 | //add needed things | 29 | //add needed things |
29 | } | 30 | } |
30 | 31 | ||
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 9ec08163..042caa86 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 | |||
@@ -20,6 +20,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | |||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
22 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 22 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl | ||
23 | 24 | ||
24 | class VampireSolver extends LogicReasoner { | 25 | class VampireSolver extends LogicReasoner { |
25 | 26 | ||
@@ -128,17 +129,17 @@ class VampireSolver extends LogicReasoner { | |||
128 | it.name = "satOut" | 129 | it.name = "satOut" |
129 | it.value = satOut | 130 | it.value = satOut |
130 | ] | 131 | ] |
131 | it.entries += createRealStatisticEntry => [ | 132 | it.entries += createStringStatisticEntry => [ |
132 | it.name = "satTime" | 133 | it.name = "satTime" |
133 | it.value = Double.parseDouble(satTime) | 134 | it.value = satTime |
134 | ] | 135 | ] |
135 | it.entries += createStringStatisticEntry => [ | 136 | it.entries += createStringStatisticEntry => [ |
136 | it.name = "modOut" | 137 | it.name = "modOut" |
137 | it.value = modOut | 138 | it.value = modOut |
138 | ] | 139 | ] |
139 | it.entries += createRealStatisticEntry => [ | 140 | it.entries += createStringStatisticEntry => [ |
140 | it.name = "modTime" | 141 | it.name = "modTime" |
141 | it.value = Double.parseDouble(modTime) | 142 | it.value = modTime |
142 | ] | 143 | ] |
143 | 144 | ||
144 | ] | 145 | ] |
@@ -148,6 +149,7 @@ class VampireSolver extends LogicReasoner { | |||
148 | } else { | 149 | } else { |
149 | 150 | ||
150 | // Start: Solving .tptp problem | 151 | // Start: Solving .tptp problem |
152 | println() | ||
151 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | 153 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) |
152 | // Finish: Solving .tptp problem | 154 | // Finish: Solving .tptp problem |
153 | // Start: Vampire -> Logic mapping | 155 | // Start: Vampire -> Logic mapping |
@@ -159,7 +161,44 @@ class VampireSolver extends LogicReasoner { | |||
159 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | 161 | val backTransformationTime = System.currentTimeMillis - backTransformationStart |
160 | // Finish: Vampire -> Logic Mapping | 162 | // Finish: Vampire -> Logic Mapping |
161 | // print(vampSol.generatedModel.tfformulas.size) | 163 | // print(vampSol.generatedModel.tfformulas.size) |
162 | return logicResult // currently only a ModelResult | 164 | |
165 | // return logicResult // currently only a ModelResult | ||
166 | |||
167 | var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl] | ||
168 | // | ||
169 | var modOut = "no" | ||
170 | if(model.length >0){ | ||
171 | modOut = "FiniteModel" | ||
172 | } | ||
173 | |||
174 | val realModOut=modOut | ||
175 | |||
176 | |||
177 | return createModelResult => [ | ||
178 | it.problem = null | ||
179 | it.representation += createVampireModel => [] | ||
180 | it.trace = trace | ||
181 | it.statistics = createStatistics => [ | ||
182 | it.transformationTime = transformationTime as int | ||
183 | it.entries += createStringStatisticEntry => [ | ||
184 | it.name = "satOut" | ||
185 | it.value = "-" | ||
186 | ] | ||
187 | it.entries += createStringStatisticEntry => [ | ||
188 | it.name = "satTime" | ||
189 | it.value = "-" | ||
190 | ] | ||
191 | it.entries += createStringStatisticEntry => [ | ||
192 | it.name = "modOut" | ||
193 | it.value = realModOut | ||
194 | ] | ||
195 | it.entries += createStringStatisticEntry => [ | ||
196 | it.name = "modTime" | ||
197 | it.value = (vampSol.solverTime/1000.0).toString | ||
198 | ] | ||
199 | |||
200 | ] | ||
201 | ] | ||
163 | } | 202 | } |
164 | } | 203 | } |
165 | return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, | 204 | return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, |
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 6d301442..c277759a 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 | |||
@@ -54,7 +54,7 @@ class VampireHandler { | |||
54 | val TEMPNAME = "TEMP.tptp" | 54 | val TEMPNAME = "TEMP.tptp" |
55 | // val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + | 55 | // val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + |
56 | // "_" + configuration.iteration + ".tptp" | 56 | // "_" + configuration.iteration + ".tptp" |
57 | val SOLNNAME = "solution" + "_" + configuration.typeScopes.maxNewElements + "_" + configuration.iteration + | 57 | val SOLNNAME = "solution" + "_" + configuration.typeScopes.minNewElements + "_" + configuration.iteration + |
58 | ".tptp" | 58 | ".tptp" |
59 | val PATH = "C:/cygwin64/bin" | 59 | val PATH = "C:/cygwin64/bin" |
60 | 60 | ||
@@ -70,7 +70,7 @@ class VampireHandler { | |||
70 | var long startTime = -1 as long | 70 | var long startTime = -1 as long |
71 | var long solverTime = -1 as long | 71 | var long solverTime = -1 as long |
72 | var Process p = null | 72 | var Process p = null |
73 | if (configuration.solver == BackendSolver::VAMPIRE) { | 73 | if (configuration.solver == BackendSolver::LOCVAMP) { |
74 | 74 | ||
75 | var OPTION = " --mode casc_sat " | 75 | var OPTION = " --mode casc_sat " |
76 | if (configuration.runtimeLimit != -1) { | 76 | if (configuration.runtimeLimit != -1) { |