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 | |
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')
20 files changed, 63 insertions, 72 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> |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 5c40d767..88e234fc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index 2d4d0741..8f9c0397 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java index 4f554956..eb6007ec 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java | |||
@@ -10,11 +10,9 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolut | |||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; |
11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | 11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; |
12 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; | 12 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl; | ||
18 | import com.google.common.base.Objects; | 16 | import com.google.common.base.Objects; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; |
@@ -35,12 +33,10 @@ import java.util.List; | |||
35 | import org.eclipse.emf.common.util.EList; | 33 | import org.eclipse.emf.common.util.EList; |
36 | import org.eclipse.xtend2.lib.StringConcatenation; | 34 | import org.eclipse.xtend2.lib.StringConcatenation; |
37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 35 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
38 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
39 | import org.eclipse.xtext.xbase.lib.Exceptions; | 36 | import org.eclipse.xtext.xbase.lib.Exceptions; |
40 | import org.eclipse.xtext.xbase.lib.Extension; | 37 | import org.eclipse.xtext.xbase.lib.Extension; |
41 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 38 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
42 | import org.eclipse.xtext.xbase.lib.InputOutput; | 39 | import org.eclipse.xtext.xbase.lib.InputOutput; |
43 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
44 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 40 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
45 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 41 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
46 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 42 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
@@ -183,79 +179,66 @@ public class VampireSolver extends LogicReasoner { | |||
183 | } else { | 179 | } else { |
184 | InputOutput.println(); | 180 | InputOutput.println(); |
185 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | 181 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); |
186 | final long backTransformationStart = System.currentTimeMillis(); | ||
187 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, | ||
188 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | ||
189 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
190 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | ||
191 | final Function1<VLSConfirmations, Boolean> _function_1 = (VLSConfirmations it) -> { | ||
192 | Class<? extends VLSConfirmations> _class = it.getClass(); | ||
193 | return Boolean.valueOf(Objects.equal(_class, VLSFiniteModelImpl.class)); | ||
194 | }; | ||
195 | Iterable<VLSConfirmations> model = IterableExtensions.<VLSConfirmations>filter(vampSol.getGeneratedModel().getConfirmations(), _function_1); | ||
196 | String modOut_1 = "no"; | 182 | String modOut_1 = "no"; |
197 | final Iterable<VLSConfirmations> _converted_model = (Iterable<VLSConfirmations>)model; | 183 | boolean _isFiniteModelGenerated = vampSol.isFiniteModelGenerated(); |
198 | int _length = ((Object[])Conversions.unwrapArray(_converted_model, Object.class)).length; | 184 | if (_isFiniteModelGenerated) { |
199 | boolean _greaterThan = (_length > 0); | ||
200 | if (_greaterThan) { | ||
201 | modOut_1 = "FiniteModel"; | 185 | modOut_1 = "FiniteModel"; |
202 | } | 186 | } |
203 | final String realModOut = modOut_1; | 187 | final String realModOut = modOut_1; |
204 | ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); | 188 | ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); |
205 | final Procedure1<ModelResult> _function_2 = (ModelResult it) -> { | 189 | final Procedure1<ModelResult> _function_1 = (ModelResult it) -> { |
206 | it.setProblem(null); | 190 | it.setProblem(null); |
207 | EList<Object> _representation = it.getRepresentation(); | 191 | EList<Object> _representation = it.getRepresentation(); |
208 | VampireModel _createVampireModel = this.factory.createVampireModel(); | 192 | VampireModel _createVampireModel = this.factory.createVampireModel(); |
209 | final Procedure1<VampireModel> _function_3 = (VampireModel it_1) -> { | 193 | final Procedure1<VampireModel> _function_2 = (VampireModel it_1) -> { |
210 | }; | 194 | }; |
211 | VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_3); | 195 | VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_2); |
212 | _representation.add(_doubleArrow); | 196 | _representation.add(_doubleArrow); |
213 | it.setTrace(it.getTrace()); | 197 | it.setTrace(it.getTrace()); |
214 | Statistics _createStatistics = this.resultFactory.createStatistics(); | 198 | Statistics _createStatistics = this.resultFactory.createStatistics(); |
215 | final Procedure1<Statistics> _function_4 = (Statistics it_1) -> { | 199 | final Procedure1<Statistics> _function_3 = (Statistics it_1) -> { |
216 | it_1.setTransformationTime(((int) transformationTime)); | 200 | it_1.setTransformationTime(((int) transformationTime)); |
217 | EList<StatisticEntry> _entries = it_1.getEntries(); | 201 | EList<StatisticEntry> _entries = it_1.getEntries(); |
218 | StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); | 202 | StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); |
219 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { | 203 | final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> { |
220 | it_2.setName("satOut"); | 204 | it_2.setName("satOut"); |
221 | it_2.setValue("-"); | 205 | it_2.setValue("-"); |
222 | }; | 206 | }; |
223 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_5); | 207 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_4); |
224 | _entries.add(_doubleArrow_1); | 208 | _entries.add(_doubleArrow_1); |
225 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); | 209 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); |
226 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); | 210 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); |
227 | final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> { | 211 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { |
228 | it_2.setName("satTime"); | 212 | it_2.setName("satTime"); |
229 | it_2.setValue("-"); | 213 | it_2.setValue("-"); |
230 | }; | 214 | }; |
231 | StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_6); | 215 | StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5); |
232 | _entries_1.add(_doubleArrow_2); | 216 | _entries_1.add(_doubleArrow_2); |
233 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); | 217 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); |
234 | StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); | 218 | StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); |
235 | final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> { | 219 | final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> { |
236 | it_2.setName("modOut"); | 220 | it_2.setName("modOut"); |
237 | it_2.setValue(realModOut); | 221 | it_2.setValue(realModOut); |
238 | }; | 222 | }; |
239 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_7); | 223 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_6); |
240 | _entries_2.add(_doubleArrow_3); | 224 | _entries_2.add(_doubleArrow_3); |
241 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); | 225 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); |
242 | StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); | 226 | StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); |
243 | final Procedure1<StringStatisticEntry> _function_8 = (StringStatisticEntry it_2) -> { | 227 | final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> { |
244 | it_2.setName("modTime"); | 228 | it_2.setName("modTime"); |
245 | long _solverTime = vampSol.getSolverTime(); | 229 | long _solverTime = vampSol.getSolverTime(); |
246 | it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString()); | 230 | it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString()); |
247 | }; | 231 | }; |
248 | StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_8); | 232 | StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_7); |
249 | _entries_3.add(_doubleArrow_4); | 233 | _entries_3.add(_doubleArrow_4); |
250 | }; | 234 | }; |
251 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_4); | 235 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_3); |
252 | it.setStatistics(_doubleArrow_1); | 236 | it.setStatistics(_doubleArrow_1); |
253 | }; | 237 | }; |
254 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_2); | 238 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_1); |
255 | } | 239 | } |
256 | } | 240 | } |
257 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); | 241 | return null; |
258 | return this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); | ||
259 | } catch (Throwable _e) { | 242 | } catch (Throwable _e) { |
260 | throw Exceptions.sneakyThrow(_e); | 243 | throw Exceptions.sneakyThrow(_e); |
261 | } | 244 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 887a3a31..07b7d4c3 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index b4943b57..04a3303b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index e3b29572..dbd48bbb 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index 50ff7011..4f4710d4 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index 337edcba..19ff819d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index c32ba83f..2774bb57 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 75e60f21..9b636247 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index d69b41ea..739f0cd5 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index 6b91ff7b..96506230 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index f23063ea..b7d9060d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 0de59fdb..d8bc6614 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 6176aca5..512e8a06 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index c09d929e..d6c90484 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |||
@@ -59,9 +59,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
59 | final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); | 59 | final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); |
60 | final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); | 60 | final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); |
61 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); | 61 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); |
62 | final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); | 62 | final boolean consistant = (GLOBAL_MAX >= GLOBAL_MIN); |
63 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { | 63 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { |
64 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant); | 64 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant)); |
65 | if (consistant) { | 65 | if (consistant) { |
66 | for (final VLSConstant i : trace.uniqueInstances) { | 66 | for (final VLSConstant i : trace.uniqueInstances) { |
67 | localInstances.add(this.support.duplicate(i)); | 67 | localInstances.add(this.support.duplicate(i)); |
@@ -72,7 +72,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
72 | } | 72 | } |
73 | } | 73 | } |
74 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { | 74 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { |
75 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, (!consistant)); | 75 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant); |
76 | if (consistant) { | 76 | if (consistant) { |
77 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); | 77 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); |
78 | } else { | 78 | } else { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java index e9073d82..39773357 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java | |||
@@ -7,12 +7,9 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | |||
7 | import com.google.common.base.Objects; | 7 | import com.google.common.base.Objects; |
8 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 8 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
9 | import java.io.BufferedReader; | 9 | import java.io.BufferedReader; |
10 | import java.io.InputStream; | 10 | import java.io.FileReader; |
11 | import java.io.InputStreamReader; | ||
12 | import java.util.List; | 11 | import java.util.List; |
13 | import org.eclipse.emf.common.util.EList; | ||
14 | import org.eclipse.emf.common.util.URI; | 12 | import org.eclipse.emf.common.util.URI; |
15 | import org.eclipse.emf.ecore.EObject; | ||
16 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 13 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
17 | import org.eclipse.xtext.xbase.lib.Conversions; | 14 | import org.eclipse.xtext.xbase.lib.Conversions; |
18 | import org.eclipse.xtext.xbase.lib.Exceptions; | 15 | import org.eclipse.xtext.xbase.lib.Exceptions; |
@@ -67,18 +64,17 @@ public class VampireHandler { | |||
67 | long _minus_1 = (_currentTimeMillis_1 - startTime); | 64 | long _minus_1 = (_currentTimeMillis_1 - startTime); |
68 | solverTime = _minus_1; | 65 | solverTime = _minus_1; |
69 | } | 66 | } |
70 | InputStream _inputStream = p.getInputStream(); | 67 | FileReader _fileReader = new FileReader(solnLoc); |
71 | InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream); | 68 | final BufferedReader reader = new BufferedReader(_fileReader); |
72 | final BufferedReader reader = new BufferedReader(_inputStreamReader); | ||
73 | final List<String> output = CollectionLiterals.<String>newArrayList(); | 69 | final List<String> output = CollectionLiterals.<String>newArrayList(); |
74 | String line = ""; | 70 | String line = ""; |
75 | while ((!Objects.equal((line = reader.readLine()), null))) { | 71 | while ((!Objects.equal((line = reader.readLine()), null))) { |
76 | output.add((line + "\n")); | 72 | boolean _equals_2 = Objects.equal(line, "Finite Model Found!"); |
73 | if (_equals_2) { | ||
74 | return new MonitoredVampireSolution(solverTime, null, true); | ||
75 | } | ||
77 | } | 76 | } |
78 | workspace.getFile(TEMPNAME).delete(); | 77 | return new MonitoredVampireSolution(solverTime, null, false); |
79 | final EList<EObject> root = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents(); | ||
80 | EObject _get = root.get(0); | ||
81 | return new MonitoredVampireSolution(solverTime, ((VampireModel) _get)); | ||
82 | } catch (Throwable _e) { | 78 | } catch (Throwable _e) { |
83 | throw Exceptions.sneakyThrow(_e); | 79 | throw Exceptions.sneakyThrow(_e); |
84 | } | 80 | } |