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 | 42 |
1 files changed, 21 insertions, 21 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) { |