aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend
blob: 38ae1daee01d4a739bddb5056203029d53313e18 (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
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 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(configuration.solverPath + " " + 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)
		}
	}
}