diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-25 04:15:39 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:49 -0400 |
commit | 32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f (patch) | |
tree | 0e67f50df5b4d9a42f0075e1e19be988eae59bf9 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill | |
parent | mid-measurement push (diff) | |
download | VIATRA-Generator-32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f.tar.gz VIATRA-Generator-32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f.tar.zst VIATRA-Generator-32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f.zip |
VAMPIRE: post-submission push
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill')
3 files changed, 35 insertions, 23 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 042caa86..59084843 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 | |||
@@ -153,21 +153,21 @@ class VampireSolver extends LogicReasoner { | |||
153 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | 153 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) |
154 | // Finish: Solving .tptp problem | 154 | // Finish: Solving .tptp problem |
155 | // Start: Vampire -> Logic mapping | 155 | // Start: Vampire -> Logic mapping |
156 | val backTransformationStart = System.currentTimeMillis | 156 | // val backTransformationStart = System.currentTimeMillis |
157 | // Backwards Mapper | 157 | // // Backwards Mapper |
158 | val logicResult = backwardMapper.transformOutput(problem, | 158 | // val logicResult = backwardMapper.transformOutput(problem, |
159 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) | 159 | // vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) |
160 | 160 | // | |
161 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | 161 | // val backTransformationTime = System.currentTimeMillis - backTransformationStart |
162 | // Finish: Vampire -> Logic Mapping | 162 | // Finish: Vampire -> Logic Mapping |
163 | // print(vampSol.generatedModel.tfformulas.size) | 163 | // print(vampSol.generatedModel.tfformulas.size) |
164 | 164 | ||
165 | // return logicResult // currently only a ModelResult | 165 | // return logicResult // currently only a ModelResult |
166 | 166 | ||
167 | var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl] | 167 | // var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl] |
168 | // | 168 | // |
169 | var modOut = "no" | 169 | var modOut = "no" |
170 | if(model.length >0){ | 170 | if(vampSol.finiteModelGenerated){ |
171 | modOut = "FiniteModel" | 171 | modOut = "FiniteModel" |
172 | } | 172 | } |
173 | 173 | ||
@@ -201,8 +201,8 @@ class VampireSolver extends LogicReasoner { | |||
201 | ] | 201 | ] |
202 | } | 202 | } |
203 | } | 203 | } |
204 | return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, | 204 | // return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, |
205 | new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) | 205 | // new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) |
206 | } | 206 | } |
207 | 207 | ||
208 | def asConfig(LogicSolverConfiguration configuration) { | 208 | def asConfig(LogicSolverConfiguration configuration) { |
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 a9516cc4..96c2da48 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 | |||
@@ -56,11 +56,11 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
56 | 56 | ||
57 | val localInstances = newArrayList | 57 | val localInstances = newArrayList |
58 | 58 | ||
59 | val consistant = GLOBAL_MAX > GLOBAL_MIN | 59 | val consistant = GLOBAL_MAX >= GLOBAL_MIN |
60 | 60 | ||
61 | // Handling Minimum_General | 61 | // Handling Minimum_General |
62 | if (GLOBAL_MIN != ABSOLUTE_MIN) { | 62 | if (GLOBAL_MIN != ABSOLUTE_MIN) { |
63 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant)//may make not consistent here | 63 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant)//may make not consistent here |
64 | if (consistant) { | 64 | if (consistant) { |
65 | for (i : trace.uniqueInstances) { | 65 | for (i : trace.uniqueInstances) { |
66 | localInstances.add(support.duplicate(i)) | 66 | localInstances.add(support.duplicate(i)) |
@@ -73,7 +73,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
73 | 73 | ||
74 | // Handling Maximum_General | 74 | // Handling Maximum_General |
75 | if (GLOBAL_MAX != ABSOLUTE_MAX) { | 75 | if (GLOBAL_MAX != ABSOLUTE_MAX) { |
76 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, !consistant) | 76 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant) |
77 | if (consistant) { | 77 | if (consistant) { |
78 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) | 78 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) |
79 | } else { | 79 | } else { |
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 c277759a..d7dd53f0 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 | |||
@@ -11,6 +11,7 @@ import org.eclipse.xtend.lib.annotations.Data | |||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl |
13 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver | 13 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver |
14 | import java.io.FileReader | ||
14 | 15 | ||
15 | class VampireSolverException extends Exception { | 16 | class VampireSolverException extends Exception { |
16 | new(String s) { | 17 | new(String s) { |
@@ -33,6 +34,7 @@ class VampireSolverException extends Exception { | |||
33 | // val List<Pair<A4Solution, Long>> aswers | 34 | // val List<Pair<A4Solution, Long>> aswers |
34 | val VampireModel generatedModel | 35 | val VampireModel generatedModel |
35 | // val boolean finishedBeforeTimeout | 36 | // val boolean finishedBeforeTimeout |
37 | val boolean finiteModelGenerated | ||
36 | } | 38 | } |
37 | 39 | ||
38 | class VampireHandler { | 40 | class VampireHandler { |
@@ -92,28 +94,38 @@ class VampireHandler { | |||
92 | p.waitFor | 94 | p.waitFor |
93 | solverTime = System.currentTimeMillis - startTime | 95 | solverTime = System.currentTimeMillis - startTime |
94 | } | 96 | } |
97 | |||
95 | 98 | ||
96 | // 2.1 determine time left | 99 | // 2.1 determine time left |
97 | // 2.2 store output into local variable | 100 | // 2.2 store output into local variable |
98 | val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); | 101 | val BufferedReader reader = new BufferedReader(new FileReader(solnLoc)); |
99 | val List<String> output = newArrayList | 102 | val List<String> output = newArrayList |
100 | 103 | ||
101 | var line = ""; | 104 | var line = ""; |
102 | while ((line = reader.readLine()) != null) { | 105 | while ((line = reader.readLine()) != null) { |
103 | output.add(line + "\n"); | 106 | if (line == "Finite Model Found!") { |
107 | return new MonitoredVampireSolution(solverTime, null, true) | ||
108 | } | ||
104 | } | 109 | } |
110 | return new MonitoredVampireSolution(solverTime, null, false) | ||
105 | 111 | ||
106 | // println(output.toString()) | 112 | /* var line = ""; |
107 | // 4. delete temp file | 113 | * while ((line = reader.readLine()) != null) { |
108 | workspace.getFile(TEMPNAME).delete | 114 | * output.add(line + "\n"); |
115 | * } | ||
109 | 116 | ||
110 | // 5. determine and return whether or not finite model was found | 117 | * // println(output.toString()) |
111 | // 6. save solution as a .tptp model | 118 | * // 4. delete temp file |
112 | val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents | 119 | * workspace.getFile(TEMPNAME).delete |
113 | 120 | ||
114 | // println((root.get(0) as VampireModel ).comments) | 121 | * // 5. determine and return whether or not finite model was found |
115 | return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel) | 122 | * // 6. save solution as a .tptp model |
123 | * val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents | ||
116 | 124 | ||
125 | * // println((root.get(0) as VampireModel ).comments) | ||
126 | * return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel) | ||
127 | * | ||
128 | */ | ||
117 | /* | 129 | /* |
118 | * //Prepare | 130 | * //Prepare |
119 | * val warnings = new LinkedList<String> | 131 | * val warnings = new LinkedList<String> |