diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire')
19 files changed, 243 insertions, 32 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 e50e6812..b26c1ded 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 e4925e24..fb8f872d 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 432b14c3..3e3bd688 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 | |||
@@ -5,12 +5,15 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated; | |||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; | 9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; |
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; |
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | 11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; |
11 | 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.VampireLanguageFactory; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
16 | import com.google.common.base.Objects; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; |
@@ -19,13 +22,25 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | |||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 26 | 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.Statistics; | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; | ||
23 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 31 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
32 | import java.util.ArrayList; | ||
24 | import java.util.List; | 33 | import java.util.List; |
25 | import org.eclipse.emf.common.util.EList; | 34 | import org.eclipse.emf.common.util.EList; |
26 | import org.eclipse.xtend2.lib.StringConcatenation; | 35 | import org.eclipse.xtend2.lib.StringConcatenation; |
36 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
37 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
38 | import org.eclipse.xtext.xbase.lib.Extension; | ||
27 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 39 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
40 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
28 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 41 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
42 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
43 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
29 | 44 | ||
30 | @SuppressWarnings("all") | 45 | @SuppressWarnings("all") |
31 | public class VampireSolver extends LogicReasoner { | 46 | public class VampireSolver extends LogicReasoner { |
@@ -41,36 +56,142 @@ public class VampireSolver extends LogicReasoner { | |||
41 | 56 | ||
42 | private final VampireHandler handler = new VampireHandler(); | 57 | private final VampireHandler handler = new VampireHandler(); |
43 | 58 | ||
59 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
60 | |||
61 | @Extension | ||
62 | private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE; | ||
63 | |||
64 | @Extension | ||
65 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
66 | |||
44 | @Override | 67 | @Override |
45 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { | 68 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { |
46 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); | 69 | try { |
47 | String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp"); | 70 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); |
48 | final long transformationStart = System.currentTimeMillis(); | 71 | String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + |
49 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | 72 | Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp"); |
50 | long _currentTimeMillis = System.currentTimeMillis(); | 73 | final long transformationStart = System.currentTimeMillis(); |
51 | final long transformationTime = (_currentTimeMillis - transformationStart); | 74 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); |
52 | final VampireModel vampireProblem = result.getOutput(); | 75 | long _currentTimeMillis = System.currentTimeMillis(); |
53 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | 76 | final long transformationTime = (_currentTimeMillis - transformationStart); |
54 | String fileURI = null; | 77 | final VampireModel vampireProblem = result.getOutput(); |
55 | String vampireCode = null; | 78 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); |
56 | vampireCode = workspace.writeModelToString(vampireProblem, fileName); | 79 | String fileURI = null; |
57 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || | 80 | String vampireCode = null; |
58 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); | 81 | vampireCode = workspace.writeModelToString(vampireProblem, fileName); |
59 | if (writeFile) { | 82 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || |
60 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString(); | 83 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); |
61 | } | 84 | if (writeFile) { |
62 | if (vampireConfig.genModel) { | 85 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString(); |
63 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | 86 | } |
64 | final long backTransformationStart = System.currentTimeMillis(); | 87 | if (vampireConfig.genModel) { |
65 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, | 88 | if (vampireConfig.server) { |
66 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | 89 | final String form = this.support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit); |
67 | long _currentTimeMillis_1 = System.currentTimeMillis(); | 90 | ArrayList<String> response = CollectionLiterals.<String>newArrayList(); |
68 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | 91 | int ind = 0; |
69 | return logicResult; | 92 | boolean done = false; |
93 | InputOutput.<String>print(" "); | ||
94 | while ((!done)) { | ||
95 | { | ||
96 | InputOutput.<String>print("(x)"); | ||
97 | done = false; | ||
98 | response = this.support.sendPost(form); | ||
99 | boolean responseFound = false; | ||
100 | ind = 0; | ||
101 | while ((!responseFound)) { | ||
102 | { | ||
103 | String line = response.get(ind); | ||
104 | if (((line.length() >= 5) && Objects.equal(line.substring(0, 5), "ERROR"))) { | ||
105 | done = false; | ||
106 | responseFound = true; | ||
107 | } else { | ||
108 | boolean _equals = Objects.equal(line, "</PRE>"); | ||
109 | if (_equals) { | ||
110 | done = true; | ||
111 | responseFound = true; | ||
112 | } | ||
113 | } | ||
114 | ind++; | ||
115 | } | ||
116 | } | ||
117 | } | ||
118 | } | ||
119 | final String satRaw = response.get((ind - 3)); | ||
120 | final String modRaw = response.get((ind - 2)); | ||
121 | final ArrayList<String> sat = CollectionLiterals.<String>newArrayList(satRaw.split(" ")); | ||
122 | final ArrayList<String> mod = CollectionLiterals.<String>newArrayList(modRaw.split(" ")); | ||
123 | final String satOut = sat.get(1); | ||
124 | final String modOut = mod.get(1); | ||
125 | final String satTime = sat.get(2); | ||
126 | final String modTime = mod.get(2); | ||
127 | InputOutput.println(); | ||
128 | InputOutput.<ArrayList<String>>println(sat); | ||
129 | InputOutput.<ArrayList<String>>println(mod); | ||
130 | ModelResult _createModelResult = this.resultFactory.createModelResult(); | ||
131 | final Procedure1<ModelResult> _function = (ModelResult it) -> { | ||
132 | it.setProblem(null); | ||
133 | EList<Object> _representation = it.getRepresentation(); | ||
134 | VampireModel _createVampireModel = this.factory.createVampireModel(); | ||
135 | final Procedure1<VampireModel> _function_1 = (VampireModel it_1) -> { | ||
136 | }; | ||
137 | VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1); | ||
138 | _representation.add(_doubleArrow); | ||
139 | it.setTrace(it.getTrace()); | ||
140 | Statistics _createStatistics = this.resultFactory.createStatistics(); | ||
141 | final Procedure1<Statistics> _function_2 = (Statistics it_1) -> { | ||
142 | it_1.setTransformationTime(((int) transformationTime)); | ||
143 | EList<StatisticEntry> _entries = it_1.getEntries(); | ||
144 | StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); | ||
145 | final Procedure1<StringStatisticEntry> _function_3 = (StringStatisticEntry it_2) -> { | ||
146 | it_2.setName("satOut"); | ||
147 | it_2.setValue(satOut); | ||
148 | }; | ||
149 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3); | ||
150 | _entries.add(_doubleArrow_1); | ||
151 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); | ||
152 | RealStatisticEntry _createRealStatisticEntry = this.resultFactory.createRealStatisticEntry(); | ||
153 | final Procedure1<RealStatisticEntry> _function_4 = (RealStatisticEntry it_2) -> { | ||
154 | it_2.setName("satTime"); | ||
155 | it_2.setValue(Double.parseDouble(satTime)); | ||
156 | }; | ||
157 | RealStatisticEntry _doubleArrow_2 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry, _function_4); | ||
158 | _entries_1.add(_doubleArrow_2); | ||
159 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); | ||
160 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); | ||
161 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { | ||
162 | it_2.setName("modOut"); | ||
163 | it_2.setValue(modOut); | ||
164 | }; | ||
165 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5); | ||
166 | _entries_2.add(_doubleArrow_3); | ||
167 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); | ||
168 | RealStatisticEntry _createRealStatisticEntry_1 = this.resultFactory.createRealStatisticEntry(); | ||
169 | final Procedure1<RealStatisticEntry> _function_6 = (RealStatisticEntry it_2) -> { | ||
170 | it_2.setName("modTime"); | ||
171 | it_2.setValue(Double.parseDouble(modTime)); | ||
172 | }; | ||
173 | RealStatisticEntry _doubleArrow_4 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry_1, _function_6); | ||
174 | _entries_3.add(_doubleArrow_4); | ||
175 | }; | ||
176 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2); | ||
177 | it.setStatistics(_doubleArrow_1); | ||
178 | }; | ||
179 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function); | ||
180 | } else { | ||
181 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | ||
182 | final long backTransformationStart = System.currentTimeMillis(); | ||
183 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, | ||
184 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | ||
185 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
186 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | ||
187 | return logicResult; | ||
188 | } | ||
189 | } | ||
190 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); | ||
191 | return this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); | ||
192 | } catch (Throwable _e) { | ||
193 | throw Exceptions.sneakyThrow(_e); | ||
70 | } | 194 | } |
71 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); | ||
72 | return this.backwardMapper.transformOutput(problem, | ||
73 | vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); | ||
74 | } | 195 | } |
75 | 196 | ||
76 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | 197 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java index dd66e910..c094872e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java | |||
@@ -11,7 +11,9 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration { | |||
11 | 11 | ||
12 | public int iteration = (-1); | 12 | public int iteration = (-1); |
13 | 13 | ||
14 | public BackendSolver solver = BackendSolver.VAMP; | 14 | public BackendSolver solver = BackendSolver.VAMPIRE; |
15 | 15 | ||
16 | public boolean genModel = true; | 16 | public boolean genModel = true; |
17 | |||
18 | public boolean server = false; | ||
17 | } | 19 | } |
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 8d2ec6ab..8b7f031e 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 515b4b3c..1b6e8f80 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 46ad8c79..f523f1af 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 169aedc2..30ba1843 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 699ce6e2..174c7362 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 799515d4..affa3754 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 2a112ae7..6c7c7522 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 7f32e055..5be67889 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 a2dd469b..192c9d1a 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 98c355ab..0495ab53 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 246c08c8..c438f1e5 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 9e55bac4..5fb9b455 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 bc39a068..c09d929e 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 | |||
@@ -55,13 +55,13 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
55 | public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 55 | public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
56 | int elemsInIM = trace.definedElement2String.size(); | 56 | int elemsInIM = trace.definedElement2String.size(); |
57 | final int ABSOLUTE_MIN = 0; | 57 | final int ABSOLUTE_MIN = 0; |
58 | final int ABSOLUTE_MAX = ((-1) - elemsInIM); | 58 | final int ABSOLUTE_MAX = (Integer.MAX_VALUE - elemsInIM); |
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/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 index dae0df6e..1255b25c 100644 --- 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 | |||
@@ -1,5 +1,6 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver; | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; |
@@ -29,6 +30,12 @@ import java.util.Collection; | |||
29 | import java.util.HashMap; | 30 | import java.util.HashMap; |
30 | import java.util.List; | 31 | import java.util.List; |
31 | import java.util.Map; | 32 | import java.util.Map; |
33 | import java.util.concurrent.TimeUnit; | ||
34 | import okhttp3.MediaType; | ||
35 | import okhttp3.OkHttpClient; | ||
36 | import okhttp3.Request; | ||
37 | import okhttp3.RequestBody; | ||
38 | import okhttp3.Response; | ||
32 | import org.eclipse.emf.common.util.EList; | 39 | import org.eclipse.emf.common.util.EList; |
33 | import org.eclipse.xtend2.lib.StringConcatenation; | 40 | import org.eclipse.xtend2.lib.StringConcatenation; |
34 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 41 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
@@ -421,4 +428,85 @@ public class Logic2VampireLanguageMapper_Support { | |||
421 | }; | 428 | }; |
422 | return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function); | 429 | return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function); |
423 | } | 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", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s"); | ||
452 | case GEOIII: | ||
453 | return CollectionLiterals.<String>newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s"); | ||
454 | case IPROVER: | ||
455 | return CollectionLiterals.<String>newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s"); | ||
456 | case PARADOX: | ||
457 | return CollectionLiterals.<String>newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s"); | ||
458 | case VAMPIRE: | ||
459 | return CollectionLiterals.<String>newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s"); | ||
460 | case Z3: | ||
461 | return CollectionLiterals.<String>newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s"); | ||
462 | default: | ||
463 | break; | ||
464 | } | ||
465 | } | ||
466 | return null; | ||
467 | } | ||
468 | |||
469 | public String getHeader() { | ||
470 | 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"; | ||
471 | } | ||
472 | |||
473 | public String addSpec(final String spec) { | ||
474 | return spec.replace("\n", "\\r\\n"); | ||
475 | } | ||
476 | |||
477 | public String addOptions() { | ||
478 | 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"; | ||
479 | } | ||
480 | |||
481 | public String addSolver(final BackendSolver solver, final int time) { | ||
482 | final ArrayList<String> solverSpecs = this.getSolverSpecs(solver); | ||
483 | final String ID = solverSpecs.get(0); | ||
484 | final String cmd = solverSpecs.get(1); | ||
485 | String _replace = cmd.replace("%d", Integer.valueOf(time).toString()); | ||
486 | String _plus = ((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID) + | ||
487 | "\"\r\n\r\n") + ID) + | ||
488 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + | ||
489 | "\"\r\n\r\n") + _replace); | ||
490 | return (_plus + "\r\n"); | ||
491 | } | ||
492 | |||
493 | public String addEnd() { | ||
494 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"; | ||
495 | } | ||
496 | |||
497 | public ArrayList<String> sendPost(final String formData) throws Exception { | ||
498 | final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build(); | ||
499 | final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); | ||
500 | final RequestBody body = RequestBody.create(mediaType, formData); | ||
501 | 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", | ||
502 | "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", | ||
503 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", | ||
504 | "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", | ||
505 | "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", | ||
506 | "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", | ||
507 | "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", | ||
508 | "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build(); | ||
509 | final Response response = client.newCall(request).execute(); | ||
510 | return CollectionLiterals.<String>newArrayList(response.body().string().split("\n")); | ||
511 | } | ||
424 | } | 512 | } |
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 fcbdfde7..e32530cb 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 | |||
@@ -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.VAMP); | 44 | boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMPIRE); |
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))) { |