diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-10 22:25:07 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-10 22:25:07 -0400 |
commit | 16f9cd46474a4934c1afd733d687f3c382fbdf56 (patch) | |
tree | 465a7cc53a489ae81d80f54d45642d84185d5e43 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend | |
parent | VAMPIRE: Further develop testing fo r Vampire solver (diff) | |
download | VIATRA-Generator-16f9cd46474a4934c1afd733d687f3c382fbdf56.tar.gz VIATRA-Generator-16f9cd46474a4934c1afd733d687f3c382fbdf56.tar.zst VIATRA-Generator-16f9cd46474a4934c1afd733d687f3c382fbdf56.zip |
implement http requests for the TPTP server
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 | 59 |
1 files changed, 30 insertions, 29 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 3281a196..85b81a8c 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 | |||
@@ -31,29 +31,32 @@ class VampireSolver extends LogicReasoner { | |||
31 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | 31 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper |
32 | val VampireHandler handler = new VampireHandler | 32 | val VampireHandler handler = new VampireHandler |
33 | 33 | ||
34 | var fileName = "problem.tptp" | 34 | // var fileName = "problem.tptp" |
35 | 35 | ||
36 | def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { | 36 | // def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { |
37 | fileName = location + fileName | 37 | // fileName = location + fileName |
38 | solve(problem, config, workspace) | 38 | // solve(problem, config, workspace) |
39 | } | 39 | // } |
40 | 40 | ||
41 | override solve(LogicProblem problem, LogicSolverConfiguration config, | 41 | override solve(LogicProblem problem, LogicSolverConfiguration config, |
42 | ReasonerWorkspace workspace) throws LogicReasonerException { | 42 | ReasonerWorkspace workspace) throws LogicReasonerException { |
43 | val vampireConfig = config.asConfig | 43 | val vampireConfig = config.asConfig |
44 | var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + vampireConfig.typeScopes.maxNewElements + ".tptp" | ||
44 | 45 | ||
45 | // Start: Logic -> Vampire mapping | 46 | // Start: Logic -> Vampire mapping |
46 | val transformationStart = System.currentTimeMillis | 47 | val transformationStart = System.currentTimeMillis |
47 | // TODO | 48 | // TODO |
48 | val result = forwardMapper.transformProblem(problem, vampireConfig) | 49 | val result = forwardMapper.transformProblem(problem, vampireConfig) |
49 | val transformationTime = System.currentTimeMillis - transformationStart | 50 | val transformationTime = System.currentTimeMillis - transformationStart |
50 | 51 | ||
51 | val vampireProblem = result.output | 52 | val vampireProblem = result.output |
52 | val forwardTrace = result.trace | 53 | val forwardTrace = result.trace |
53 | 54 | ||
54 | var String fileURI = null; | 55 | var String fileURI = null; |
55 | var String vampireCode = null; | 56 | var String vampireCode = null; |
56 | vampireCode = workspace.writeModelToString(vampireProblem, fileName) | 57 | vampireCode = workspace.writeModelToString(vampireProblem, fileName) |
58 | |||
59 | |||
57 | 60 | ||
58 | val writeFile = ( | 61 | val writeFile = ( |
59 | vampireConfig.documentationLevel === DocumentationLevel::NORMAL || | 62 | vampireConfig.documentationLevel === DocumentationLevel::NORMAL || |
@@ -61,35 +64,33 @@ class VampireSolver extends LogicReasoner { | |||
61 | if (writeFile) { | 64 | if (writeFile) { |
62 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString | 65 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString |
63 | } | 66 | } |
64 | 67 | ||
65 | |||
66 | |||
67 | // Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("tptp", new VampireLanguageFactoryImpl) | 68 | // Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("tptp", new VampireLanguageFactoryImpl) |
68 | //// val Resource resource = Resource. | 69 | //// val Resource resource = Resource. |
69 | //// Resource.getResource(wsURI+"problem.tptp") as Resource | 70 | //// Resource.getResource(wsURI+"problem.tptp") as Resource |
70 | //// resource | 71 | //// resource |
71 | // val model = workspace.readModel(VampireModel, "problem.tptp").eResource.contents | 72 | // val model = workspace.readModel(VampireModel, "problem.tptp").eResource.contents |
72 | // println(model) | 73 | // println(model) |
73 | |||
74 | |||
75 | // Result as String | ||
76 | |||
77 | // Finish: Logic -> Vampire mapping | 74 | // Finish: Logic -> Vampire mapping |
78 | 75 | if (vampireConfig.genModel) { | |
79 | // Start: Solving .tptp problem | ||
80 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | ||
81 | // Finish: Solving .tptp problem | ||
82 | |||
83 | // Start: Vampire -> Logic mapping | ||
84 | val backTransformationStart = System.currentTimeMillis | ||
85 | // Backwards Mapper | ||
86 | val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime) | ||
87 | 76 | ||
88 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | 77 | // Start: Solving .tptp problem |
89 | // Finish: Vampire -> Logic Mapping | 78 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) |
90 | 79 | // Finish: Solving .tptp problem | |
80 | // Start: Vampire -> Logic mapping | ||
81 | val backTransformationStart = System.currentTimeMillis | ||
82 | // Backwards Mapper | ||
83 | val logicResult = backwardMapper.transformOutput(problem, | ||
84 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) | ||
85 | |||
86 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | ||
87 | // Finish: Vampire -> Logic Mapping | ||
91 | // print(vampSol.generatedModel.tfformulas.size) | 88 | // print(vampSol.generatedModel.tfformulas.size) |
92 | return logicResult //currently only a ModelResult | 89 | return logicResult // currently only a ModelResult |
90 | } | ||
91 | |||
92 | return backwardMapper.transformOutput(problem, | ||
93 | vampireConfig.solutionScope.numberOfRequiredSolution, new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) | ||
93 | } | 94 | } |
94 | 95 | ||
95 | def asConfig(LogicSolverConfiguration configuration) { | 96 | def asConfig(LogicSolverConfiguration configuration) { |
@@ -105,9 +106,9 @@ class VampireSolver extends LogicReasoner { | |||
105 | // * | 106 | // * |
106 | override getInterpretations(ModelResult modelResult) { | 107 | override getInterpretations(ModelResult modelResult) { |
107 | // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] | 108 | // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] |
108 | val sols = modelResult.representation// as List<A4Solution> | 109 | val sols = modelResult.representation // as List<A4Solution> |
109 | //val res = answers.map | 110 | // val res = answers.map |
110 | sols.map[ | 111 | sols.map [ |
111 | new VampireModelInterpretation( | 112 | new VampireModelInterpretation( |
112 | // forwardMapper.typeMapper.typeInterpreter, | 113 | // forwardMapper.typeMapper.typeInterpreter, |
113 | it as VampireModel, | 114 | it as VampireModel, |