1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
import com.google.common.base.Objects;
import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
import java.io.BufferedReader;
import java.io.FileReader;
import java.util.List;
import org.eclipse.emf.common.util.URI;
import org.eclipse.xtext.xbase.lib.CollectionLiterals;
import org.eclipse.xtext.xbase.lib.Conversions;
import org.eclipse.xtext.xbase.lib.Exceptions;
import org.eclipse.xtext.xbase.lib.InputOutput;
@SuppressWarnings("all")
public class VampireHandler {
public MonitoredVampireSolution callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) {
try {
final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\";
final String VAMPNAME = "vampire.exe";
final String VAMPLOC = (VAMPDIR + VAMPNAME);
final String CVC4DIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\";
final String CVC4NAME = "vampire.exe";
final String CVC4LOC = (CVC4DIR + CVC4NAME);
final String CMD = "cmd /c ";
final String TEMPNAME = "TEMP.tptp";
final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.minNewElements)) + "_") + Integer.valueOf(configuration.iteration)) +
".tptp");
final String PATH = "C:/cygwin64/bin";
final URI wsURI = workspace.getWorkspaceURI();
final String tempLoc = (wsURI + TEMPNAME);
String _plus = (wsURI + SOLNNAME);
final String solnLoc = (_plus + " ");
String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString();
long startTime = (-((long) 1));
long solverTime = (-((long) 1));
Process p = null;
boolean _equals = Objects.equal(configuration.solver, BackendSolver.LOCVAMP);
if (_equals) {
String OPTION = " --mode casc_sat ";
if ((configuration.runtimeLimit != (-1))) {
OPTION = (((OPTION + "-t ") + Integer.valueOf(configuration.runtimeLimit)) + " ");
}
startTime = System.currentTimeMillis();
p = Runtime.getRuntime().exec((((((CMD + VAMPLOC) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class)));
p.waitFor();
long _currentTimeMillis = System.currentTimeMillis();
long _minus = (_currentTimeMillis - startTime);
solverTime = _minus;
}
boolean _equals_1 = Objects.equal(configuration.solver, BackendSolver.CVC4);
if (_equals_1) {
String OPTION_1 = " SAT ";
if ((configuration.runtimeLimit != (-1))) {
OPTION_1 = ((" " + Integer.valueOf(configuration.runtimeLimit)) + OPTION_1);
}
InputOutput.<String>println((((((CMD + CVC4LOC) + tempLoc) + OPTION_1) + " > ") + solnLoc));
p = Runtime.getRuntime().exec((((((CMD + CVC4LOC) + tempLoc) + OPTION_1) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class)));
p.waitFor();
long _currentTimeMillis_1 = System.currentTimeMillis();
long _minus_1 = (_currentTimeMillis_1 - startTime);
solverTime = _minus_1;
}
FileReader _fileReader = new FileReader(solnLoc);
final BufferedReader reader = new BufferedReader(_fileReader);
final List<String> output = CollectionLiterals.<String>newArrayList();
String line = "";
while ((!Objects.equal((line = reader.readLine()), null))) {
boolean _equals_2 = Objects.equal(line, "Finite Model Found!");
if (_equals_2) {
return new MonitoredVampireSolution(solverTime, null, true);
}
}
return new MonitoredVampireSolution(solverTime, null, false);
} catch (Throwable _e) {
throw Exceptions.sneakyThrow(_e);
}
}
}
|
