Skip to content
Snippets Groups Projects
Commit 13af0f46 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

SynthesisPhase is now an object

parent dba1a853
No related branches found
No related tags found
No related merge requests found
......@@ -52,7 +52,7 @@ class AnalysisComponent(val global: Global, val leonReporter: Reporter, val plug
,
if (Settings.synthesis)
List(
new SynthesisPhase(leonReporter)
SynthesisPhase
)
else
Nil
......@@ -71,7 +71,8 @@ class AnalysisComponent(val global: Global, val leonReporter: Reporter, val plug
//global ref to freshName creator
fresh = unit.fresh
var ac = LeonContext(program = extractCode(unit))
var ac = LeonContext(program = extractCode(unit),
reporter = leonReporter)
if(Settings.stopAfterExtraction) {
leonReporter.info("Extracted program for " + unit + ": ")
......
......@@ -4,6 +4,7 @@ package plugin
import purescala.Definitions.Program
case class LeonContext(
val program: Program
val program: Program,
val reporter: Reporter
)
package leon
package synthesis
import plugin.LeonContext
import purescala.Definitions.Program
class SynthesisPhase(reporter: Reporter) extends plugin.TransformationPhase {
object SynthesisPhase extends plugin.LeonPhase {
val name = "Synthesis"
val description = "Synthesis"
def apply(program: Program): Program = {
def run(ctx: LeonContext): LeonContext = {
val quietReporter = new QuietReporter
val solvers = List(
new TrivialSolver(quietReporter),
new FairZ3Solver(quietReporter)
)
new Synthesizer(reporter, solvers).synthesizeAll(program)
val newProgram = new Synthesizer(ctx.reporter, solvers).synthesizeAll(ctx.program)
ctx.copy(program = newProgram)
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment