diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire')
16 files changed, 81 insertions, 14 deletions
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 b26c1ded..5c40d767 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 7fedcc30..2d4d0741 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 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); |
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 8b7f031e..887a3a31 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 1b6e8f80..b4943b57 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 f523f1af..e3b29572 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 30ba1843..50ff7011 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 174c7362..337edcba 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 affa3754..c32ba83f 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 9caad4ea..75e60f21 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 5be67889..d69b41ea 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 192c9d1a..6b91ff7b 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 0495ab53..f23063ea 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 c438f1e5..0de59fdb 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 5fb9b455..6176aca5 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/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java index e32530cb..e9073d82 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 | |||
@@ -30,7 +30,7 @@ public class VampireHandler { | |||
30 | final String CVC4LOC = (CVC4DIR + CVC4NAME); | 30 | final String CVC4LOC = (CVC4DIR + CVC4NAME); |
31 | final String CMD = "cmd /c "; | 31 | final String CMD = "cmd /c "; |
32 | final String TEMPNAME = "TEMP.tptp"; | 32 | final String TEMPNAME = "TEMP.tptp"; |
33 | final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + | 33 | final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.minNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + |
34 | ".tptp"); | 34 | ".tptp"); |
35 | final String PATH = "C:/cygwin64/bin"; | 35 | final String PATH = "C:/cygwin64/bin"; |
36 | final URI wsURI = workspace.getWorkspaceURI(); | 36 | final URI wsURI = workspace.getWorkspaceURI(); |
@@ -41,7 +41,7 @@ public class VampireHandler { | |||
41 | long startTime = (-((long) 1)); | 41 | long startTime = (-((long) 1)); |
42 | long solverTime = (-((long) 1)); | 42 | long solverTime = (-((long) 1)); |
43 | Process p = null; | 43 | Process p = null; |
44 | boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMPIRE); | 44 | boolean _equals = Objects.equal(configuration.solver, BackendSolver.LOCVAMP); |
45 | if (_equals) { | 45 | if (_equals) { |
46 | String OPTION = " --mode casc_sat "; | 46 | String OPTION = " --mode casc_sat "; |
47 | if ((configuration.runtimeLimit != (-1))) { | 47 | if ((configuration.runtimeLimit != (-1))) { |