blob: d2c54aaf9596a239053ad49e4db9ee4d5a4928e1 (
plain) (
blame)
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
|
package hu.bme.mit.inf.dslreasoner.smt.reasoner.builder
import org.eclipse.emf.common.util.URI
import java.io.InputStream
import java.io.IOException
import java.io.FileWriter
import java.io.File
import java.io.BufferedReader
import java.io.InputStreamReader
import org.eclipse.emf.common.CommonPlugin
import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration
class SmtSolverException extends Exception{
new(String s) { super(s) }
new(String s, Exception e) { super(s,e) }
}
class SmtSolverHandler {
public def callSolver(URI resourceURI, SmtSolverConfiguration configuration) {
val URI smtUri = CommonPlugin.resolve(resourceURI)
val File smtFile = new File(smtUri.toFileString())
val path = configuration.solverPath
if(path===null) {throw new IllegalArgumentException('''Path to solver is not specified!''')}
val params =
'''/smt2 /st«
IF configuration.runtimeLimit != SmtSolverConfiguration::Unlimited» /T:«configuration.runtimeLimit»«ENDIF»«
IF configuration.memoryLimit != SmtSolverConfiguration::Unlimited» /memory:«configuration.memoryLimit»«ENDIF»«
IF configuration.fixRandomSeed» /rs:0«ENDIF
» «smtFile.path»'''
val Runtime runTime = Runtime.getRuntime()
try {
val process = runTime.exec(path + " " + params)
val FileWriter writer = new FileWriter(smtFile,true)
writer.append("\n--------------\n")
appendStream(writer, process.getInputStream())
printStream(process.getErrorStream())
writer.close
} catch (IOException e) {
throw new SmtSolverException(
"Error during the input/output handling of the reasoner.", e)
}
return resourceURI
}
def private void printStream(InputStream inputStream) throws IOException {
val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream))
var int line = -1
while ((line = input.read()) != -1) {
System.out.print(line as char)
}
input.close()
}
def private appendStream(FileWriter writer, InputStream inputStream) throws IOException {
val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream))
var int line = -1
while ((line = input.read()) != -1) {
writer.append(line as char)
}
}
}
|