diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java | 91 |
1 files changed, 79 insertions, 12 deletions
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 3e3bd688..4f554956 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,9 +10,11 @@ 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; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl; | ||
16 | import com.google.common.base.Objects; | 18 | import com.google.common.base.Objects; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; |
@@ -24,7 +26,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | |||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; | 27 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; |
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 28 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; | 29 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; |
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; | 30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; |
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; | 31 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; |
@@ -34,10 +35,12 @@ import java.util.List; | |||
34 | import org.eclipse.emf.common.util.EList; | 35 | import org.eclipse.emf.common.util.EList; |
35 | import org.eclipse.xtend2.lib.StringConcatenation; | 36 | import org.eclipse.xtend2.lib.StringConcatenation; |
36 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
38 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
37 | import org.eclipse.xtext.xbase.lib.Exceptions; | 39 | import org.eclipse.xtext.xbase.lib.Exceptions; |
38 | import org.eclipse.xtext.xbase.lib.Extension; | 40 | import org.eclipse.xtext.xbase.lib.Extension; |
39 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 41 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
40 | import org.eclipse.xtext.xbase.lib.InputOutput; | 42 | import org.eclipse.xtext.xbase.lib.InputOutput; |
43 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
41 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 44 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
42 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 45 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
43 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 46 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
@@ -149,28 +152,28 @@ public class VampireSolver extends LogicReasoner { | |||
149 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3); | 152 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3); |
150 | _entries.add(_doubleArrow_1); | 153 | _entries.add(_doubleArrow_1); |
151 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); | 154 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); |
152 | RealStatisticEntry _createRealStatisticEntry = this.resultFactory.createRealStatisticEntry(); | 155 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); |
153 | final Procedure1<RealStatisticEntry> _function_4 = (RealStatisticEntry it_2) -> { | 156 | final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> { |
154 | it_2.setName("satTime"); | 157 | it_2.setName("satTime"); |
155 | it_2.setValue(Double.parseDouble(satTime)); | 158 | it_2.setValue(satTime); |
156 | }; | 159 | }; |
157 | RealStatisticEntry _doubleArrow_2 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry, _function_4); | 160 | StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_4); |
158 | _entries_1.add(_doubleArrow_2); | 161 | _entries_1.add(_doubleArrow_2); |
159 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); | 162 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); |
160 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); | 163 | StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); |
161 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { | 164 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { |
162 | it_2.setName("modOut"); | 165 | it_2.setName("modOut"); |
163 | it_2.setValue(modOut); | 166 | it_2.setValue(modOut); |
164 | }; | 167 | }; |
165 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5); | 168 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_5); |
166 | _entries_2.add(_doubleArrow_3); | 169 | _entries_2.add(_doubleArrow_3); |
167 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); | 170 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); |
168 | RealStatisticEntry _createRealStatisticEntry_1 = this.resultFactory.createRealStatisticEntry(); | 171 | StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); |
169 | final Procedure1<RealStatisticEntry> _function_6 = (RealStatisticEntry it_2) -> { | 172 | final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> { |
170 | it_2.setName("modTime"); | 173 | it_2.setName("modTime"); |
171 | it_2.setValue(Double.parseDouble(modTime)); | 174 | it_2.setValue(modTime); |
172 | }; | 175 | }; |
173 | RealStatisticEntry _doubleArrow_4 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry_1, _function_6); | 176 | StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_6); |
174 | _entries_3.add(_doubleArrow_4); | 177 | _entries_3.add(_doubleArrow_4); |
175 | }; | 178 | }; |
176 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2); | 179 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2); |
@@ -178,13 +181,77 @@ public class VampireSolver extends LogicReasoner { | |||
178 | }; | 181 | }; |
179 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function); | 182 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function); |
180 | } else { | 183 | } else { |
184 | InputOutput.println(); | ||
181 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | 185 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); |
182 | final long backTransformationStart = System.currentTimeMillis(); | 186 | final long backTransformationStart = System.currentTimeMillis(); |
183 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, | 187 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, |
184 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | 188 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); |
185 | long _currentTimeMillis_1 = System.currentTimeMillis(); | 189 | long _currentTimeMillis_1 = System.currentTimeMillis(); |
186 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | 190 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); |
187 | return logicResult; | 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"; | ||
197 | final Iterable<VLSConfirmations> _converted_model = (Iterable<VLSConfirmations>)model; | ||
198 | int _length = ((Object[])Conversions.unwrapArray(_converted_model, Object.class)).length; | ||
199 | boolean _greaterThan = (_length > 0); | ||
200 | if (_greaterThan) { | ||
201 | modOut_1 = "FiniteModel"; | ||
202 | } | ||
203 | final String realModOut = modOut_1; | ||
204 | ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); | ||
205 | final Procedure1<ModelResult> _function_2 = (ModelResult it) -> { | ||
206 | it.setProblem(null); | ||
207 | EList<Object> _representation = it.getRepresentation(); | ||
208 | VampireModel _createVampireModel = this.factory.createVampireModel(); | ||
209 | final Procedure1<VampireModel> _function_3 = (VampireModel it_1) -> { | ||
210 | }; | ||
211 | VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_3); | ||
212 | _representation.add(_doubleArrow); | ||
213 | it.setTrace(it.getTrace()); | ||
214 | Statistics _createStatistics = this.resultFactory.createStatistics(); | ||
215 | final Procedure1<Statistics> _function_4 = (Statistics it_1) -> { | ||
216 | it_1.setTransformationTime(((int) transformationTime)); | ||
217 | EList<StatisticEntry> _entries = it_1.getEntries(); | ||
218 | StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); | ||
219 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { | ||
220 | it_2.setName("satOut"); | ||
221 | it_2.setValue("-"); | ||
222 | }; | ||
223 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_5); | ||
224 | _entries.add(_doubleArrow_1); | ||
225 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); | ||
226 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); | ||
227 | final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> { | ||
228 | it_2.setName("satTime"); | ||
229 | it_2.setValue("-"); | ||
230 | }; | ||
231 | StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_6); | ||
232 | _entries_1.add(_doubleArrow_2); | ||
233 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); | ||
234 | StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); | ||
235 | final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> { | ||
236 | it_2.setName("modOut"); | ||
237 | it_2.setValue(realModOut); | ||
238 | }; | ||
239 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_7); | ||
240 | _entries_2.add(_doubleArrow_3); | ||
241 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); | ||
242 | StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); | ||
243 | final Procedure1<StringStatisticEntry> _function_8 = (StringStatisticEntry it_2) -> { | ||
244 | it_2.setName("modTime"); | ||
245 | long _solverTime = vampSol.getSolverTime(); | ||
246 | it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString()); | ||
247 | }; | ||
248 | StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_8); | ||
249 | _entries_3.add(_doubleArrow_4); | ||
250 | }; | ||
251 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_4); | ||
252 | it.setStatistics(_doubleArrow_1); | ||
253 | }; | ||
254 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_2); | ||
188 | } | 255 | } |
189 | } | 256 | } |
190 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); | 257 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); |