diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire')
4 files changed, 30 insertions, 19 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 0ec4d0da..3b5cec0a 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 | |||
@@ -9,6 +9,8 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper | |||
9 | 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 | 10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException |
@@ -16,7 +18,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | |||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 20 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
20 | 21 | ||
21 | class VampireSolver extends LogicReasoner { | 22 | class VampireSolver extends LogicReasoner { |
22 | 23 | ||
@@ -82,10 +83,12 @@ class VampireSolver extends LogicReasoner { | |||
82 | // Start: Vampire -> Logic mapping | 83 | // Start: Vampire -> Logic mapping |
83 | val backTransformationStart = System.currentTimeMillis | 84 | val backTransformationStart = System.currentTimeMillis |
84 | // Backwards Mapper | 85 | // Backwards Mapper |
85 | val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime) | 86 | val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,solvingTime) |
86 | 87 | ||
87 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | 88 | val backTransformationTime = System.currentTimeMillis - backTransformationStart |
88 | // Finish: Vampire -> Logic Mapping | 89 | // Finish: Vampire -> Logic Mapping |
90 | |||
91 | // print(vampSol.generatedModel.tfformulas.size) | ||
89 | return logicResult //currently only a ModelResult | 92 | return logicResult //currently only a ModelResult |
90 | } | 93 | } |
91 | 94 | ||
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 a0084204..489bf423 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 | |||
@@ -21,7 +21,9 @@ class Vampire2LogicMapper { | |||
21 | } | 21 | } |
22 | 22 | ||
23 | def transformStatistics(MonitoredVampireSolution solution, long transformationTime) { | 23 | def transformStatistics(MonitoredVampireSolution solution, long transformationTime) { |
24 | return createStatistics | 24 | return createStatistics => [ |
25 | it.transformationTime = solution.solverTime as int | ||
26 | ] | ||
25 | // createStatistics => [ | 27 | // createStatistics => [ |
26 | // it.transformationTime = transformationTime as int | 28 | // it.transformationTime = transformationTime as int |
27 | // for(solutionIndex : 0..<solution.aswers.size) { | 29 | // for(solutionIndex : 0..<solution.aswers.size) { |
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 ce672211..74532ee5 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 | |||
@@ -28,7 +28,7 @@ class VampireSolverException extends Exception { | |||
28 | @Data class MonitoredVampireSolution { | 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 solverTime |
32 | // val List<Pair<A4Solution, Long>> aswers | 32 | // val List<Pair<A4Solution, Long>> aswers |
33 | val VampireModel generatedModel | 33 | val VampireModel generatedModel |
34 | // val boolean finishedBeforeTimeout | 34 | // val boolean finishedBeforeTimeout |
@@ -43,8 +43,8 @@ class VampireHandler { | |||
43 | val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" | 43 | val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" |
44 | val VAMPNAME = "vampire.exe" | 44 | val VAMPNAME = "vampire.exe" |
45 | val TEMPNAME = "TEMP.tptp" | 45 | val TEMPNAME = "TEMP.tptp" |
46 | val OPTION = " --mode casc_sat " | 46 | val OPTION = " --mode casc_sat -t 300 " |
47 | val SOLNNAME = "solution.tptp" | 47 | val SOLNNAME = "_solution" + configuration.typeScopes.maxNewElements + ".tptp" |
48 | val PATH = "C:/cygwin64/bin" | 48 | val PATH = "C:/cygwin64/bin" |
49 | 49 | ||
50 | val wsURI = workspace.workspaceURI | 50 | val wsURI = workspace.workspaceURI |
@@ -57,9 +57,11 @@ class VampireHandler { | |||
57 | 57 | ||
58 | // 2. run command and save to | 58 | // 2. run command and save to |
59 | // need to have cygwin downloaded | 59 | // need to have cygwin downloaded |
60 | var startTime = System.currentTimeMillis | ||
60 | val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) | 61 | val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) |
61 | // 2.1 determine time left | 62 | // 2.1 determine time left |
62 | p.waitFor | 63 | p.waitFor |
64 | val solverTime = System.currentTimeMillis - startTime | ||
63 | 65 | ||
64 | // 2.2 store output into local variable | 66 | // 2.2 store output into local variable |
65 | val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); | 67 | val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); |
@@ -80,7 +82,7 @@ class VampireHandler { | |||
80 | 82 | ||
81 | // println((root.get(0) as VampireModel ).comments) | 83 | // println((root.get(0) as VampireModel ).comments) |
82 | 84 | ||
83 | return new MonitoredVampireSolution(root.get(0) as VampireModel) | 85 | return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel) |
84 | 86 | ||
85 | /* | 87 | /* |
86 | * //Prepare | 88 | * //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 index 9eb47f41..063dcf2a 100644 --- 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 | |||
@@ -33,6 +33,7 @@ import java.util.Map | |||
33 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 33 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
35 | import java.util.concurrent.TimeUnit | 35 | import java.util.concurrent.TimeUnit |
36 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTermImpl | ||
36 | 37 | ||
37 | class VampireModelInterpretation implements LogicModelInterpretation { | 38 | class VampireModelInterpretation implements LogicModelInterpretation { |
38 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | 39 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE |
@@ -79,10 +80,10 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
79 | // println() | 80 | // println() |
80 | // println(trace.type2Predicate) | 81 | // println(trace.type2Predicate) |
81 | // Fill keys of map | 82 | // Fill keys of map |
82 | println(trace.type2Predicate.keySet) | 83 | // println(trace.type2Predicate.keySet) |
83 | val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] | 84 | val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] |
84 | val allTypeFunctions = trace.predicate2Type | 85 | val allTypeFunctions = trace.predicate2Type |
85 | println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl]) | 86 | // println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl]) |
86 | 87 | ||
87 | for (type : allTypeDecls) { | 88 | for (type : allTypeDecls) { |
88 | type2DefinedElement.put(type as TypeDeclaration, newArrayList) | 89 | type2DefinedElement.put(type as TypeDeclaration, newArrayList) |
@@ -97,7 +98,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
97 | for (formula : typeFormulas) { | 98 | for (formula : typeFormulas) { |
98 | // get associated type | 99 | // get associated type |
99 | val associatedTypeName = (formula as VLSTffFormula).name.substring(10) | 100 | val associatedTypeName = (formula as VLSTffFormula).name.substring(10) |
100 | print(associatedTypeName) | 101 | // print(associatedTypeName) |
101 | val associatedFunctions = allTypeFunctions.keySet.filter[constant == associatedTypeName] | 102 | val associatedFunctions = allTypeFunctions.keySet.filter[constant == associatedTypeName] |
102 | if (associatedFunctions.length > 0) { | 103 | if (associatedFunctions.length > 0) { |
103 | val associatedFunction = associatedFunctions.get(0) as VLSFunction | 104 | val associatedFunction = associatedFunctions.get(0) as VLSFunction |
@@ -132,7 +133,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
132 | 133 | ||
133 | } | 134 | } |
134 | 135 | ||
135 | printMap() | 136 | // printMap() |
136 | 137 | ||
137 | // 3. get relations | 138 | // 3. get relations |
138 | // Fill keys of map | 139 | // Fill keys of map |
@@ -153,6 +154,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
153 | val relFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_r_"] | 154 | val relFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_r_"] |
154 | 155 | ||
155 | for (formula : relFormulas) { | 156 | for (formula : relFormulas) { |
157 | // println(formula) | ||
156 | // get associated type | 158 | // get associated type |
157 | val associatedRelName = (formula as VLSTffFormula).name.substring(10) | 159 | val associatedRelName = (formula as VLSTffFormula).name.substring(10) |
158 | 160 | ||
@@ -169,7 +171,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
169 | end = false | 171 | end = false |
170 | val List<String[]> instances = newArrayList | 172 | val List<String[]> instances = newArrayList |
171 | while (!end) { | 173 | while (!end) { |
172 | if (andFormulaTerm.class == VLSAndImpl) { | 174 | if (andFormulaTerm.class != null && andFormulaTerm.class == VLSAndImpl) { |
173 | val andFormula = andFormulaTerm as VLSAnd | 175 | val andFormula = andFormulaTerm as VLSAnd |
174 | val andRight = andFormula.right | 176 | val andRight = andFormula.right |
175 | addRelIfNotNeg(andRight, instances) | 177 | addRelIfNotNeg(andRight, instances) |
@@ -202,6 +204,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
202 | 204 | ||
203 | } | 205 | } |
204 | println() | 206 | println() |
207 | println("--------END ELEMENTS MAP----------") | ||
205 | } | 208 | } |
206 | 209 | ||
207 | def printMap2() { | 210 | def printMap2() { |
@@ -226,7 +229,8 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
226 | } | 229 | } |
227 | 230 | ||
228 | def private addRelIfNotNeg(VLSTerm term, List<String[]> list) { | 231 | def private addRelIfNotNeg(VLSTerm term, List<String[]> list) { |
229 | if (term.class != VLSUnaryNegationImpl) { | 232 | // println("xxx " + term.class) |
233 | if (term.class != VLSUnaryNegationImpl && term.class != VLSTermImpl) { | ||
230 | val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor | 234 | val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor |
231 | val nodeName2 = ((term as VLSFunction).terms.get(1) as VLSFunctionAsTerm).functor | 235 | val nodeName2 = ((term as VLSFunction).terms.get(1) as VLSFunctionAsTerm).functor |
232 | val strArr = newArrayList(nodeName1, nodeName2) | 236 | val strArr = newArrayList(nodeName1, nodeName2) |
@@ -247,9 +251,9 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
247 | } | 251 | } |
248 | 252 | ||
249 | def private dispatch getElementsDispatch(TypeDefinition declaration) { | 253 | def private dispatch getElementsDispatch(TypeDefinition declaration) { |
250 | println("~~" + declaration) | 254 | // println("~~" + declaration) |
251 | println(declaration.elements) | 255 | // println(declaration.elements) |
252 | println() | 256 | // println() |
253 | return declaration.elements | 257 | return declaration.elements |
254 | } | 258 | } |
255 | 259 | ||
@@ -258,18 +262,18 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
258 | } | 262 | } |
259 | 263 | ||
260 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | 264 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { |
261 | print("-- " + relation.name) | 265 | // print("-- " + relation.name) |
262 | val node1 = (parameterSubstitution.get(0) as DefinedElement).name | 266 | val node1 = (parameterSubstitution.get(0) as DefinedElement).name |
263 | val node2 = (parameterSubstitution.get(1) as DefinedElement).name | 267 | val node2 = (parameterSubstitution.get(1) as DefinedElement).name |
264 | val realRelations = relation.lookup(relDec2Inst) | 268 | val realRelations = relation.lookup(relDec2Inst) |
265 | for (real : realRelations) { | 269 | for (real : realRelations) { |
266 | if (real.contains(node1) && real.contains(node2)) { | 270 | if (real.contains(node1) && real.contains(node2)) { |
267 | println(" true") | 271 | // println(" true") |
268 | TimeUnit.MILLISECONDS.sleep(10) | 272 | TimeUnit.MILLISECONDS.sleep(10) |
269 | return true | 273 | return true |
270 | } | 274 | } |
271 | } | 275 | } |
272 | println(" false") | 276 | // println(" false") |
273 | TimeUnit.MILLISECONDS.sleep(10) | 277 | TimeUnit.MILLISECONDS.sleep(10) |
274 | return false | 278 | return false |
275 | } | 279 | } |