aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java515
1 files changed, 0 insertions, 515 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
deleted file mode 100644
index d757212a..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ /dev/null
@@ -1,515 +0,0 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier;
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;
16import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
17import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
18import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
19import com.google.common.base.Objects;
20import com.google.common.collect.Iterables;
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;
22import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression;
23import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term;
24import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
25import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
26import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
27import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
28import java.util.ArrayList;
29import java.util.Collection;
30import java.util.HashMap;
31import java.util.List;
32import java.util.Map;
33import java.util.concurrent.TimeUnit;
34import okhttp3.MediaType;
35import okhttp3.OkHttpClient;
36import okhttp3.Request;
37import okhttp3.RequestBody;
38import okhttp3.Response;
39import org.eclipse.emf.common.util.EList;
40import org.eclipse.xtend2.lib.StringConcatenation;
41import org.eclipse.xtext.xbase.lib.CollectionLiterals;
42import org.eclipse.xtext.xbase.lib.Conversions;
43import org.eclipse.xtext.xbase.lib.ExclusiveRange;
44import org.eclipse.xtext.xbase.lib.Extension;
45import org.eclipse.xtext.xbase.lib.Functions.Function1;
46import org.eclipse.xtext.xbase.lib.IterableExtensions;
47import org.eclipse.xtext.xbase.lib.ListExtensions;
48import org.eclipse.xtext.xbase.lib.ObjectExtensions;
49import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
50
51@SuppressWarnings("all")
52public class Logic2VampireLanguageMapper_Support {
53 @Extension
54 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
55
56 protected String toIDMultiple(final String... ids) {
57 final Function1<String, String> _function = (String it) -> {
58 return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(it.split("\\s+"))), "_");
59 };
60 return IterableExtensions.join(ListExtensions.<String, String>map(((List<String>)Conversions.doWrapArray(ids)), _function), "_");
61 }
62
63 protected String toID(final String ids) {
64 return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_");
65 }
66
67 protected VLSVariable duplicate(final VLSVariable term) {
68 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
69 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
70 it.setName(term.getName());
71 };
72 return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
73 }
74
75 protected VLSFunctionAsTerm duplicate(final VLSFunctionAsTerm term) {
76 VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();
77 final Procedure1<VLSFunctionAsTerm> _function = (VLSFunctionAsTerm it) -> {
78 it.setFunctor(term.getFunctor());
79 };
80 return ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function);
81 }
82
83 protected VLSConstant duplicate(final VLSConstant term) {
84 VLSConstant _createVLSConstant = this.factory.createVLSConstant();
85 final Procedure1<VLSConstant> _function = (VLSConstant it) -> {
86 it.setName(term.getName());
87 };
88 return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);
89 }
90
91 protected VLSFunction duplicate(final VLSFunction term) {
92 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
93 final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
94 it.setConstant(term.getConstant());
95 EList<VLSTerm> _terms = term.getTerms();
96 for (final VLSTerm v : _terms) {
97 EList<VLSTerm> _terms_1 = it.getTerms();
98 VLSVariable _duplicate = this.duplicate(((VLSVariable) v));
99 _terms_1.add(_duplicate);
100 }
101 };
102 return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
103 }
104
105 protected VLSFunction duplicate(final VLSFunction term, final VLSVariable v) {
106 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
107 final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
108 it.setConstant(term.getConstant());
109 EList<VLSTerm> _terms = it.getTerms();
110 VLSVariable _duplicate = this.duplicate(v);
111 _terms.add(_duplicate);
112 };
113 return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
114 }
115
116 protected VLSFunction duplicate(final VLSFunction term, final List<VLSVariable> vars) {
117 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
118 final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
119 it.setConstant(term.getConstant());
120 for (final VLSVariable v : vars) {
121 EList<VLSTerm> _terms = it.getTerms();
122 VLSVariable _duplicate = this.duplicate(v);
123 _terms.add(_duplicate);
124 }
125 };
126 return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
127 }
128
129 protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) {
130 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
131 final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
132 it.setConstant(term.getConstant());
133 EList<VLSTerm> _terms = it.getTerms();
134 VLSFunctionAsTerm _duplicate = this.duplicate(v);
135 _terms.add(_duplicate);
136 };
137 return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
138 }
139
140 protected List<VLSVariable> duplicate(final List<VLSVariable> vars) {
141 ArrayList<VLSVariable> newList = CollectionLiterals.<VLSVariable>newArrayList();
142 for (final VLSVariable v : vars) {
143 newList.add(this.duplicate(v));
144 }
145 return newList;
146 }
147
148 protected VLSConstant toConstant(final VLSFunctionAsTerm term) {
149 VLSConstant _createVLSConstant = this.factory.createVLSConstant();
150 final Procedure1<VLSConstant> _function = (VLSConstant it) -> {
151 it.setName(term.getFunctor());
152 };
153 return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);
154 }
155
156 protected VLSFunction topLevelTypeFunc() {
157 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
158 final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
159 it.setConstant("object");
160 EList<VLSTerm> _terms = it.getTerms();
161 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
162 final Procedure1<VLSVariable> _function_1 = (VLSVariable it_1) -> {
163 it_1.setName("A");
164 };
165 VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);
166 _terms.add(_doubleArrow);
167 };
168 return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
169 }
170
171 protected VLSFunction topLevelTypeFunc(final VLSVariable v) {
172 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
173 final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
174 it.setConstant("object");
175 EList<VLSTerm> _terms = it.getTerms();
176 VLSVariable _duplicate = this.duplicate(v);
177 _terms.add(_duplicate);
178 };
179 return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
180 }
181
182 protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) {
183 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
184 final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
185 it.setConstant("object");
186 EList<VLSTerm> _terms = it.getTerms();
187 VLSFunctionAsTerm _duplicate = this.duplicate(v);
188 _terms.add(_duplicate);
189 };
190 return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
191 }
192
193 public VLSTerm establishUniqueness(final List<VLSConstant> terms, final VLSConstant t2) {
194 final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList();
195 for (final VLSConstant t1 : terms) {
196 boolean _notEquals = (!Objects.equal(t1, t2));
197 if (_notEquals) {
198 VLSInequality _createVLSInequality = this.factory.createVLSInequality();
199 final Procedure1<VLSInequality> _function = (VLSInequality it) -> {
200 VLSConstant _createVLSConstant = this.factory.createVLSConstant();
201 final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> {
202 it_1.setName(t2.getName());
203 };
204 VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1);
205 it.setLeft(_doubleArrow);
206 VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant();
207 final Procedure1<VLSConstant> _function_2 = (VLSConstant it_1) -> {
208 it_1.setName(t1.getName());
209 };
210 VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2);
211 it.setRight(_doubleArrow_1);
212 };
213 final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function);
214 eqs.add(eq);
215 }
216 }
217 return this.unfoldAnd(eqs);
218 }
219
220 protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) {
221 int _size = operands.size();
222 boolean _equals = (_size == 1);
223 if (_equals) {
224 return IterableExtensions.head(operands);
225 } else {
226 int _size_1 = operands.size();
227 boolean _greaterThan = (_size_1 > 1);
228 if (_greaterThan) {
229 VLSAnd _createVLSAnd = this.factory.createVLSAnd();
230 final Procedure1<VLSAnd> _function = (VLSAnd it) -> {
231 it.setLeft(IterableExtensions.head(operands));
232 it.setRight(this.unfoldAnd(operands.subList(1, operands.size())));
233 };
234 return ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function);
235 } else {
236 StringConcatenation _builder = new StringConcatenation();
237 _builder.append("Logic operator with 0 operands!");
238 throw new UnsupportedOperationException(_builder.toString());
239 }
240 }
241 }
242
243 protected VLSTerm unfoldOr(final List<? extends VLSTerm> operands) {
244 int _size = operands.size();
245 boolean _equals = (_size == 1);
246 if (_equals) {
247 return IterableExtensions.head(operands);
248 } else {
249 int _size_1 = operands.size();
250 boolean _greaterThan = (_size_1 > 1);
251 if (_greaterThan) {
252 VLSOr _createVLSOr = this.factory.createVLSOr();
253 final Procedure1<VLSOr> _function = (VLSOr it) -> {
254 it.setLeft(IterableExtensions.head(operands));
255 it.setRight(this.unfoldOr(operands.subList(1, operands.size())));
256 };
257 return ObjectExtensions.<VLSOr>operator_doubleArrow(_createVLSOr, _function);
258 } else {
259 StringConcatenation _builder = new StringConcatenation();
260 _builder.append("Logic operator with 0 operands!");
261 throw new UnsupportedOperationException(_builder.toString());
262 }
263 }
264 }
265
266 protected VLSTerm unfoldDistinctTerms(final Logic2VampireLanguageMapper m, final EList<Term> operands, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
267 int _size = operands.size();
268 boolean _equals = (_size == 1);
269 if (_equals) {
270 return m.transformTerm(IterableExtensions.<Term>head(operands), trace, variables);
271 } else {
272 int _size_1 = operands.size();
273 boolean _greaterThan = (_size_1 > 1);
274 if (_greaterThan) {
275 int _size_2 = operands.size();
276 int _size_3 = operands.size();
277 int _multiply = (_size_2 * _size_3);
278 int _divide = (_multiply / 2);
279 final ArrayList<VLSTerm> notEquals = new ArrayList<VLSTerm>(_divide);
280 int _size_4 = operands.size();
281 ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _size_4, true);
282 for (final Integer i : _doubleDotLessThan) {
283 int _size_5 = operands.size();
284 ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(((i).intValue() + 1), _size_5, true);
285 for (final Integer j : _doubleDotLessThan_1) {
286 VLSInequality _createVLSInequality = this.factory.createVLSInequality();
287 final Procedure1<VLSInequality> _function = (VLSInequality it) -> {
288 it.setLeft(m.transformTerm(operands.get((i).intValue()), trace, variables));
289 it.setRight(m.transformTerm(operands.get((j).intValue()), trace, variables));
290 };
291 VLSInequality _doubleArrow = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function);
292 notEquals.add(_doubleArrow);
293 }
294 }
295 return this.unfoldAnd(notEquals);
296 } else {
297 StringConcatenation _builder = new StringConcatenation();
298 _builder.append("Logic operator with 0 operands!");
299 throw new UnsupportedOperationException(_builder.toString());
300 }
301 }
302 }
303
304 /**
305 * def protected String toID(List<String> ids) {
306 * ids.map[it.split("\\s+").join("'")].join("'")
307 * }
308 */
309 protected VLSTerm createQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables, final boolean isUniversal) {
310 VLSTerm _xblockexpression = null;
311 {
312 final Function1<Variable, VLSVariable> _function = (Variable v) -> {
313 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
314 final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> {
315 it.setName(this.toIDMultiple("V", v.getName()));
316 };
317 return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);
318 };
319 final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function);
320 final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();
321 EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables();
322 for (final Variable variable : _quantifiedVariables) {
323 {
324 TypeReference _range = variable.getRange();
325 final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate),
326 CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap));
327 typedefs.add(eq);
328 }
329 }
330 VLSTerm _xifexpression = null;
331 if (isUniversal) {
332 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
333 final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> {
334 EList<VLSTffTerm> _variables = it.getVariables();
335 Collection<VLSVariable> _values = variableMap.values();
336 Iterables.<VLSTffTerm>addAll(_variables, _values);
337 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
338 final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> {
339 it_1.setLeft(this.unfoldAnd(typedefs));
340 it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));
341 };
342 VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
343 it.setOperand(_doubleArrow);
344 };
345 _xifexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
346 } else {
347 VLSExistentialQuantifier _xblockexpression_1 = null;
348 {
349 typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));
350 VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();
351 final Procedure1<VLSExistentialQuantifier> _function_2 = (VLSExistentialQuantifier it) -> {
352 EList<VLSTffTerm> _variables = it.getVariables();
353 Collection<VLSVariable> _values = variableMap.values();
354 Iterables.<VLSTffTerm>addAll(_variables, _values);
355 it.setOperand(this.unfoldAnd(typedefs));
356 };
357 _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2);
358 }
359 _xifexpression = _xblockexpression_1;
360 }
361 _xblockexpression = _xifexpression;
362 }
363 return _xblockexpression;
364 }
365
366 protected boolean dfsSupertypeCheck(final Type type, final Type type2) {
367 boolean _xifexpression = false;
368 boolean _isEmpty = type.getSupertypes().isEmpty();
369 if (_isEmpty) {
370 return false;
371 } else {
372 boolean _xifexpression_1 = false;
373 boolean _contains = type.getSupertypes().contains(type2);
374 if (_contains) {
375 return true;
376 } else {
377 EList<Type> _supertypes = type.getSupertypes();
378 for (final Type supertype : _supertypes) {
379 boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2);
380 if (_dfsSupertypeCheck) {
381 return true;
382 }
383 }
384 }
385 _xifexpression = _xifexpression_1;
386 }
387 return _xifexpression;
388 }
389
390 protected boolean dfsSubtypeCheck(final Type type, final Type type2) {
391 boolean _xifexpression = false;
392 boolean _isEmpty = type.getSubtypes().isEmpty();
393 if (_isEmpty) {
394 return false;
395 } else {
396 boolean _xifexpression_1 = false;
397 boolean _contains = type.getSubtypes().contains(type2);
398 if (_contains) {
399 return true;
400 } else {
401 EList<Type> _subtypes = type.getSubtypes();
402 for (final Type subtype : _subtypes) {
403 boolean _dfsSubtypeCheck = this.dfsSubtypeCheck(subtype, type2);
404 if (_dfsSubtypeCheck) {
405 return true;
406 }
407 }
408 }
409 _xifexpression = _xifexpression_1;
410 }
411 return _xifexpression;
412 }
413
414 protected void listSubtypes(final Type t, final List<Type> allSubtypes) {
415 EList<Type> _subtypes = t.getSubtypes();
416 for (final Type subt : _subtypes) {
417 {
418 allSubtypes.add(subt);
419 this.listSubtypes(subt, allSubtypes);
420 }
421 }
422 }
423
424 protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) {
425 HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1);
426 final Procedure1<HashMap<Variable, VLSVariable>> _function = (HashMap<Variable, VLSVariable> it) -> {
427 it.putAll(map2);
428 };
429 return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function);
430 }
431
432 public String makeForm(final String formula, final BackendSolver solver, final int time) {
433 String _header = this.getHeader();
434 String _plus = (_header + formula);
435 String _addOptions = this.addOptions();
436 String _plus_1 = (_plus + _addOptions);
437 String _addSolver = this.addSolver(solver, time);
438 String _plus_2 = (_plus_1 + _addSolver);
439 String _addEnd = this.addEnd();
440 return (_plus_2 + _addEnd);
441 }
442
443 public ArrayList<String> getSolverSpecs(final BackendSolver solver) {
444 if (solver != null) {
445 switch (solver) {
446 case CVC4:
447 return CollectionLiterals.<String>newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT");
448 case DARWINFM:
449 return CollectionLiterals.<String>newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s");
450 case EDARWIN:
451 return CollectionLiterals.<String>newArrayList("E-Darwin---1.5",
452 "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s");
453 case GEOIII:
454 return CollectionLiterals.<String>newArrayList("Geo-III---2018C",
455 "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s");
456 case IPROVER:
457 return CollectionLiterals.<String>newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s");
458 case PARADOX:
459 return CollectionLiterals.<String>newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s");
460 case VAMPIRE:
461 return CollectionLiterals.<String>newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s");
462 case Z3:
463 return CollectionLiterals.<String>newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s");
464 default:
465 break;
466 }
467 }
468 return null;
469 }
470
471 public String getHeader() {
472 return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n";
473 }
474
475 public String addSpec(final String spec) {
476 return spec.replace("\n", "\\r\\n");
477 }
478
479 public String addOptions() {
480 return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n";
481 }
482
483 public String addSolver(final BackendSolver solver, final int time) {
484 final ArrayList<String> solverSpecs = this.getSolverSpecs(solver);
485 final String ID = solverSpecs.get(0);
486 final String cmd = solverSpecs.get(1);
487 return (((((((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"TimeLimit___" + ID) +
488 "\"\r\n\r\n") + Integer.valueOf(time)) +
489 "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___") + ID) +
490 "\"\r\n\r\n") + ID) +
491 "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) +
492 "\"\r\n\r\n") + cmd) + "\r\n");
493 }
494
495 public String addEnd() {
496 return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--";
497 }
498
499 public ArrayList<String> sendPost(final String formData) throws Exception {
500 final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(600, TimeUnit.SECONDS).readTimeout(350,
501 TimeUnit.SECONDS).build();
502 final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA");
503 final RequestBody body = RequestBody.create(mediaType, formData);
504 final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin",
505 "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type",
506 "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent",
507 "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").addHeader("Accept",
508 "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding",
509 "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token",
510 "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host",
511 "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build();
512 final Response response = client.newCall(request).execute();
513 return CollectionLiterals.<String>newArrayList(response.body().string().split("\n"));
514 }
515}
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-05 12:26:37 +0000