diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill')
4 files changed, 38 insertions, 33 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend index b223dbe5..4e9737cb 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend | |||
@@ -8,6 +8,7 @@ class VampireSolverConfiguration extends LogicSolverConfiguration { | |||
8 | public var boolean uniquenessDuplicates = false | 8 | public var boolean uniquenessDuplicates = false |
9 | public var int iteration = -1 | 9 | public var int iteration = -1 |
10 | public var BackendSolver solver = BackendSolver::VAMP | 10 | public var BackendSolver solver = BackendSolver::VAMP |
11 | public var genModel = true | ||
11 | //choose needed backend solver | 12 | //choose needed backend solver |
12 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J | 13 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J |
13 | } | 14 | } |
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, |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index df3cfd82..39862c65 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend | |||
@@ -25,8 +25,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
25 | 25 | ||
26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, | 26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, |
27 | Logic2VampireLanguageMapperTrace trace) { | 27 | Logic2VampireLanguageMapperTrace trace) { |
28 | val ABSOLUTE_MIN = 0 | 28 | |
29 | val ABSOLUTE_MAX = Integer.MAX_VALUE | ||
30 | 29 | ||
31 | // TODO HANDLE ERRORS RELATED TO MAX > MIN | 30 | // TODO HANDLE ERRORS RELATED TO MAX > MIN |
32 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS | 31 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS |
@@ -40,6 +39,8 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
40 | // Number of defined non-abstract elements that are not enum elements | 39 | // Number of defined non-abstract elements that are not enum elements |
41 | // Equals the number of elements in te initial model | 40 | // Equals the number of elements in te initial model |
42 | var elemsInIM = trace.definedElement2String.size | 41 | var elemsInIM = trace.definedElement2String.size |
42 | val ABSOLUTE_MIN = 0 | ||
43 | val ABSOLUTE_MAX = -1-elemsInIM | ||
43 | // var elemsInIM = 0 | 44 | // var elemsInIM = 0 |
44 | // | 45 | // |
45 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { | 46 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { |
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 c1eb3382..47eae807 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 | |||
@@ -52,8 +52,10 @@ class VampireHandler { | |||
52 | 52 | ||
53 | val CMD = "cmd /c " | 53 | val CMD = "cmd /c " |
54 | val TEMPNAME = "TEMP.tptp" | 54 | val TEMPNAME = "TEMP.tptp" |
55 | val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + | 55 | // val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + |
56 | "_" + configuration.iteration + ".tptp" | 56 | // "_" + configuration.iteration + ".tptp" |
57 | val SOLNNAME = "solution" + "_" + configuration.typeScopes.maxNewElements + "_" + configuration.iteration + | ||
58 | ".tptp" | ||
57 | val PATH = "C:/cygwin64/bin" | 59 | val PATH = "C:/cygwin64/bin" |
58 | 60 | ||
59 | val wsURI = workspace.workspaceURI | 61 | val wsURI = workspace.workspaceURI |