From 2e7b523fa5eb2863a0d43f1e8faba534ab9d4ef5 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 25 Oct 2012 17:27:09 +0200
Subject: [PATCH] Process management, try #2
---
.../scala/leon/synthesis/SynthesisPhase.scala | 31 +++++++++++++++++--
.../scala/leon/synthesis/Synthesizer.scala | 20 +++++++++---
2 files changed, 44 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index bf7a62e7e..b21f87ae3 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -14,7 +14,8 @@ object SynthesisPhase extends LeonPhase[Program, PipelineControl] {
new FairZ3Solver(quietReporter)
)
- val newProgram = new Synthesizer(ctx.reporter, solvers).synthesizeAll(p)
+ val synth = new Synthesizer(ctx.reporter, solvers)
+ val solutions = synth.synthesizeAll(p)
detectEditor match {
case Some(program) =>
@@ -31,7 +32,31 @@ object SynthesisPhase extends LeonPhase[Program, PipelineControl] {
}
def openEditor(program: String, path: String) {
- val p = sys.process.Process(program+" "+path)
- p !<
+ val proc = Runtime.getRuntime().exec(program+" "+path)
+
+ val errGobbler = new StreamGobbler(proc.getErrorStream(), System.err)
+ val outGobbler = new StreamGobbler(proc.getInputStream(), System.out)
+ val inGobbler = new StreamGobbler(System.in, proc.getOutputStream())
+
+ errGobbler.start()
+ outGobbler.start()
+ inGobbler.start()
+
+ proc.waitFor()
+ errGobbler.join()
+ outGobbler.join()
+ }
+
+ import java.io.{InputStream, OutputStream}
+ class StreamGobbler(is: InputStream, os: OutputStream) extends Thread {
+ override def run() {
+ var c: Int = is.read()
+ while(c != 1) {
+ os.write(c);
+ os.flush();
+
+ c = is.read()
+ }
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 9e02f8025..7e53e3812 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -86,8 +86,8 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
(None, Map())
}
- def synthesizeAll(program: Program) = {
- import purescala.Trees._
+ import purescala.Trees._
+ def synthesizeAll(program: Program): List[(Choose, Solution)] = {
solvers.foreach(_.setProgram(program))
@@ -95,8 +95,10 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
def noop(u:Expr, u2: Expr) = u
+ var solutions = List[(Choose, Solution)]()
+
def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
- case Choose(vars, pred) =>
+ case ch @ Choose(vars, pred) =>
val xs = vars
val as = (variablesOf(pred)--xs).toList
val phi = pred
@@ -105,8 +107,11 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
info("")
info("In Function "+f.id+":")
info("-"*80)
+
val sol = synthesize(Problem(as, phi, xs), rules)
+ solutions = (ch, sol) :: solutions
+
info("Scala code:")
info(ScalaPrinter(simplifyLets(sol.toExpr)))
@@ -120,6 +125,13 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
treeCatamorphism(x => x, noop, actOnChoose(f), f.body.get)
}
- program
+ solutions
+ }
+
+ def substitueChooses(file: String, sols: List[(Choose, Solution)]) = {
+ import scala.io.Source
+
+ val src = Source.fromFile(file)
+
}
}
--
GitLab