diff options
author | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-03-07 12:48:01 -0500 |
---|---|---|
committer | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-03-07 12:48:01 -0500 |
commit | 5ac36bba74bcf71224d4895cccdae253b07ccbc9 (patch) | |
tree | 85a15ac3d720c24021c9126dc6e00e653135a9b5 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend | |
parent | removed unnecessary println (diff) | |
download | VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.tar.gz VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.tar.zst VIATRA-Generator-5ac36bba74bcf71224d4895cccdae253b07ccbc9.zip |
Rebooting Z3 solver Containment vs Inheritance still has a bug
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend index 38ae1dae..d2c54aaf 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend | |||
@@ -17,9 +17,12 @@ class SmtSolverException extends Exception{ | |||
17 | 17 | ||
18 | class SmtSolverHandler { | 18 | class SmtSolverHandler { |
19 | public def callSolver(URI resourceURI, SmtSolverConfiguration configuration) { | 19 | public def callSolver(URI resourceURI, SmtSolverConfiguration configuration) { |
20 | |||
20 | val URI smtUri = CommonPlugin.resolve(resourceURI) | 21 | val URI smtUri = CommonPlugin.resolve(resourceURI) |
21 | val File smtFile = new File(smtUri.toFileString()) | 22 | val File smtFile = new File(smtUri.toFileString()) |
22 | 23 | ||
24 | val path = configuration.solverPath | ||
25 | if(path===null) {throw new IllegalArgumentException('''Path to solver is not specified!''')} | ||
23 | val params = | 26 | val params = |
24 | '''/smt2 /st« | 27 | '''/smt2 /st« |
25 | IF configuration.runtimeLimit != SmtSolverConfiguration::Unlimited» /T:«configuration.runtimeLimit»«ENDIF»« | 28 | IF configuration.runtimeLimit != SmtSolverConfiguration::Unlimited» /T:«configuration.runtimeLimit»«ENDIF»« |
@@ -28,9 +31,9 @@ class SmtSolverHandler { | |||
28 | » «smtFile.path»''' | 31 | » «smtFile.path»''' |
29 | 32 | ||
30 | val Runtime runTime = Runtime.getRuntime() | 33 | val Runtime runTime = Runtime.getRuntime() |
31 | 34 | ||
32 | try { | 35 | try { |
33 | val process = runTime.exec(configuration.solverPath + " " + params) | 36 | val process = runTime.exec(path + " " + params) |
34 | 37 | ||
35 | val FileWriter writer = new FileWriter(smtFile,true) | 38 | val FileWriter writer = new FileWriter(smtFile,true) |
36 | writer.append("\n--------------\n") | 39 | writer.append("\n--------------\n") |
@@ -44,7 +47,6 @@ class SmtSolverHandler { | |||
44 | 47 | ||
45 | return resourceURI | 48 | return resourceURI |
46 | } | 49 | } |
47 | |||
48 | def private void printStream(InputStream inputStream) throws IOException { | 50 | def private void printStream(InputStream inputStream) throws IOException { |
49 | val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream)) | 51 | val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream)) |
50 | var int line = -1 | 52 | var int line = -1 |