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 | 7 |
1 files changed, 5 insertions, 2 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 | ||