diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner')
2 files changed, 81 insertions, 33 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 1d56892e..6bb49080 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 | |||
@@ -27,7 +27,12 @@ class VampireSolver extends LogicReasoner { | |||
27 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | 27 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper |
28 | val VampireHandler handler = new VampireHandler | 28 | val VampireHandler handler = new VampireHandler |
29 | 29 | ||
30 | val fileName = "vampireProblem.tptp" | 30 | var fileName = "problem.tptp" |
31 | |||
32 | def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { | ||
33 | fileName = location + fileName | ||
34 | solve(problem, config, workspace) | ||
35 | } | ||
31 | 36 | ||
32 | override solve(LogicProblem problem, LogicSolverConfiguration config, | 37 | override solve(LogicProblem problem, LogicSolverConfiguration config, |
33 | ReasonerWorkspace workspace) throws LogicReasonerException { | 38 | ReasonerWorkspace workspace) throws LogicReasonerException { |
@@ -54,26 +59,21 @@ class VampireSolver extends LogicReasoner { | |||
54 | // Result as String | 59 | // Result as String |
55 | val transformationTime = System.currentTimeMillis - transformationStart | 60 | val transformationTime = System.currentTimeMillis - transformationStart |
56 | // Finish: Logic -> Vampire mapping | 61 | // Finish: Logic -> Vampire mapping |
57 | /* | 62 | // Start: Solving .tptp problem |
58 | * // Start: Solving Alloy problem | 63 | val solverStart = System.currentTimeMillis |
59 | * val solverStart = System.currentTimeMillis | 64 | // Calling Solver (Currently Manually) |
60 | * //Calling Solver (Currently Manually) | 65 | val result2 = handler.callSolver(vampireProblem, workspace, vampireConfig) |
61 | * val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode) | 66 | // val result2 = null |
62 | * // val result2 = null | 67 | val solvingTime = System.currentTimeMillis - solverStart |
63 | * //TODO | 68 | // TODO |
64 | * //Backwards Mapper | 69 | // val backTransformationStart = System.currentTimeMillis |
65 | * val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | 70 | // // Backwards Mapper |
66 | * | 71 | // val logicResult = backwardMapper.transformOutput(problem, config.solutionScope.numberOfRequiredSolution, |
67 | * val solverFinish = System.currentTimeMillis-solverStart | 72 | // result2, forwardTrace, transformationTime) |
68 | * // Finish: Solving Alloy problem | 73 | // |
69 | * | 74 | // val backTransformationTime = System.currentTimeMillis - backTransformationStart |
70 | * if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) | 75 | // Finish: Solving Alloy problem |
71 | * | 76 | return null |
72 | * return logicResult | ||
73 | * | ||
74 | /*/ | ||
75 | return null // for now | ||
76 | // */ | ||
77 | } | 77 | } |
78 | 78 | ||
79 | def asConfig(LogicSolverConfiguration configuration) { | 79 | def asConfig(LogicSolverConfiguration configuration) { |
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 aefa1a7e..274396ee 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 | |||
@@ -1,21 +1,14 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireBackendSolver | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
6 | import com.google.common.util.concurrent.SimpleTimeLimiter | ||
7 | import com.google.common.util.concurrent.UncheckedTimeoutException | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
9 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 5 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
10 | import java.util.ArrayList | 6 | import java.io.BufferedReader |
11 | import java.util.HashMap | 7 | import java.io.InputStreamReader |
12 | import java.util.LinkedList | ||
13 | import java.util.List | 8 | import java.util.List |
14 | import java.util.Map | 9 | import org.eclipse.emf.ecore.resource.Resource |
15 | import java.util.concurrent.Callable | ||
16 | import java.util.concurrent.TimeUnit | ||
17 | import org.eclipse.emf.common.command.Command | ||
18 | import org.eclipse.xtend.lib.annotations.Data | 10 | import org.eclipse.xtend.lib.annotations.Data |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl | ||
19 | 12 | ||
20 | class VampireSolverException extends Exception{ | 13 | class VampireSolverException extends Exception{ |
21 | new(String s) { super(s) } | 14 | new(String s) { super(s) } |
@@ -39,7 +32,62 @@ class VampireHandler { | |||
39 | 32 | ||
40 | //val fileName = "problem.als" | 33 | //val fileName = "problem.als" |
41 | 34 | ||
42 | public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration,String vampireCode) { | 35 | public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration) { |
36 | |||
37 | val CMD = "cmd /c " | ||
38 | val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" | ||
39 | val VAMPNAME = "vampire.exe" | ||
40 | val TEMPNAME = "TEMP.tptp" | ||
41 | val OPTION = " --mode casc_sat " | ||
42 | val SOLNNAME = "solution.tptp" | ||
43 | val PATH = "C:/cygwin64/bin" | ||
44 | |||
45 | val wsURI = workspace.workspaceURI | ||
46 | val tempLoc = wsURI + TEMPNAME | ||
47 | val solnLoc = wsURI + SOLNNAME + " " | ||
48 | val vampLoc = VAMPDIR + VAMPNAME | ||
49 | |||
50 | |||
51 | //1. create temp file for vampire problem | ||
52 | var tempURI = workspace.writeModel(problem, TEMPNAME).toFileString | ||
53 | |||
54 | //2. run command and save to | ||
55 | //need to have cygwin downloaded | ||
56 | |||
57 | |||
58 | |||
59 | |||
60 | val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) | ||
61 | //2.1 determine time left | ||
62 | p.waitFor | ||
63 | |||
64 | //2.2 store output into local variable | ||
65 | val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); | ||
66 | val List<String> output = newArrayList | ||
67 | |||
68 | var line = ""; | ||
69 | while ((line = reader.readLine())!= null) { | ||
70 | output.add(line + "\n"); | ||
71 | } | ||
72 | |||
73 | // println(output.toString()) | ||
74 | |||
75 | //4. delete temp file | ||
76 | workspace.getFile(TEMPNAME).delete | ||
77 | |||
78 | //5. determine and return whether or not finite model was found | ||
79 | |||
80 | //6. save solution as a .tptp model | ||
81 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new VampireLanguageFactoryImpl) | ||
82 | workspace.readModel(VampireModel, SOLNNAME).eResource.contents | ||
83 | |||
84 | |||
85 | |||
86 | |||
87 | |||
88 | |||
89 | |||
90 | |||
43 | /* | 91 | /* |
44 | //Prepare | 92 | //Prepare |
45 | val warnings = new LinkedList<String> | 93 | val warnings = new LinkedList<String> |