diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 176cb96b1f9fe411be0553afca3a31895d7e962a..2ba7a69ad7aa69be4b49d0cdd7b395dfa2bf6c34 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -327,3 +327,12 @@ object Analysis {
liftLets(Implies(And(trueThings.reverse), result))
}
}
+
+object AnalysisPhase extends plugin.UnitPhase {
+ val name = "Analysis"
+ val description = "Leon Analyses"
+
+ def apply(program: Program) {
+ new Analysis(program).analyse
+ }
+}
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 7d0d94458291b71381d8719a25e13751ca3cdd9f..0dab758176b2b3381eaed88c67415d95d5cd8df3 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -5,8 +5,9 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object ArrayTransformation extends Pass {
+object ArrayTransformation extends plugin.TransformationPhase {
+ val name = "Array Transformation"
val description = "Add bound checking for array access and remove array update with side effect"
def apply(pgm: Program): Program = {
diff --git a/src/main/scala/leon/EpsilonElimination.scala b/src/main/scala/leon/EpsilonElimination.scala
index 585888f4c771ea6354df64f8792d0becd90dea52..5cc7645d54e99c6480f09dcfd16b46e01e4a0713 100644
--- a/src/main/scala/leon/EpsilonElimination.scala
+++ b/src/main/scala/leon/EpsilonElimination.scala
@@ -5,8 +5,9 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object EpsilonElimination extends Pass {
+object EpsilonElimination extends plugin.TransformationPhase {
+ val name = "Epsilon Elimination"
val description = "Remove all epsilons from the program"
def apply(pgm: Program): Program = {
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index 8a6fd5bffd1a7c6a9a6a9b6fdde5e8bd3598f940..64c0c123f7d1c289e6b59a0bbe13ddd6390f5ae4 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -5,8 +5,9 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object FunctionClosure extends Pass {
+object FunctionClosure extends plugin.TransformationPhase{
+ val name = "Function Closure"
val description = "Closing function with its scoping variables"
private var pathConstraints: List[Expr] = Nil
diff --git a/src/main/scala/leon/FunctionHoisting.scala b/src/main/scala/leon/FunctionHoisting.scala
index 37bc69c41fa12e41c94b3c8d876631f8e3f47220..e467f3f20eb0c414936a3584001285fdc24d9eba 100644
--- a/src/main/scala/leon/FunctionHoisting.scala
+++ b/src/main/scala/leon/FunctionHoisting.scala
@@ -5,8 +5,9 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object FunctionHoisting extends Pass {
+object FunctionHoisting extends plugin.TransformationPhase {
+ val name = "Function Hoisting"
val description = "Hoist function at the top level"
def apply(program: Program): Program = {
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index d3cd29907c5cd8c30fb574d06ddd1682e5bfa59a..bb770ba8e15eede296321707f58bcf4460404a98 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -5,8 +5,9 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object ImperativeCodeElimination extends Pass {
+object ImperativeCodeElimination extends plugin.TransformationPhase {
+ val name = "Imperative Code Elimination"
val description = "Transform imperative constructs into purely functional code"
private var varInScope = Set[Identifier]()
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 9af1b41e731e32ff4b25942c4ec4f6ac63f91b0a..760e5c5de0a994f450c2d6190e9ce89624d79fac 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -27,19 +27,7 @@ object Main {
def run(args: Array[String], reporter: Reporter = new DefaultReporter, classPath : Option[Seq[String]] = None) : Unit = {
val settings = new NSCSettings
classPath.foreach(s => settings.classpath.tryToSet(s.toList))
- runWithSettings(args, settings, s => reporter.info(s), Some(p => defaultAction(p, reporter)))
- }
-
- private def defaultAction(program: Program, reporter: Reporter) : Unit = {
- Logger.debug("Default action on program: " + program, 3, "main")
- val passManager = new PassManager(Seq(ArrayTransformation, EpsilonElimination, ImperativeCodeElimination, /*UnitElimination,*/ FunctionClosure, /*FunctionHoisting,*/ Simplificator))
- val program2 = passManager.run(program)
- assert(program2.isPure)
- val analysis = new Analysis(program2, reporter)
- analysis.analyse
- }
- private def runWithSettings(args : Array[String], settings : NSCSettings, printerFunction : String=>Unit, actionOnProgram : Option[Program=>Unit] = None) : Unit = {
val (leonOptions, nonLeonOptions) = args.toList.partition(_.startsWith("--"))
val command = new CompilerCommand(nonLeonOptions, settings) {
override val cmdName = "leon"
@@ -49,9 +37,9 @@ object Main {
if(settings.version.value) {
println(command.cmdName + " beta.")
} else {
- val runner = new PluginRunner(settings, printerFunction, actionOnProgram)
- runner.leonPlugin.processOptions(leonOptions.map(_.substring(2)), Console.err.println(_))
- runner.leonPlugin.stopAfterAnalysis = false
+ val runner = new PluginRunner(settings, reporter)
+ runner.leonPlugin.processOptions(leonOptions.map(_.substring(2)), reporter.error(_))
+
val run = new runner.Run
run.compile(command.files)
}
@@ -61,8 +49,8 @@ object Main {
/** This class is a compiler that will be used for running the plugin in
* standalone mode. Original version courtesy of D. Zufferey. */
-class PluginRunner(settings : NSCSettings, reportingFunction : String => Unit, actionOnProgram : Option[Program=>Unit]) extends Global(settings, new plugin.SimpleReporter(settings, reportingFunction)) {
- val leonPlugin = new plugin.LeonPlugin(this, actionOnProgram)
+class PluginRunner(settings : NSCSettings, reporter : Reporter) extends Global(settings, new plugin.SimpleReporter(settings, reporter)) {
+ val leonPlugin = new plugin.LeonPlugin(this, reporter)
protected def myAddToPhasesSet(sub : SubComponent, descr : String) : Unit = {
phasesSet += sub
diff --git a/src/main/scala/leon/Pass.scala b/src/main/scala/leon/Pass.scala
deleted file mode 100644
index 4bbc88856c20b96bd5c9c3fd9e1815b57b85d976..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/Pass.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-package leon
-
-import purescala.Definitions._
-
-abstract class Pass {
-
- def apply(pgm: Program): Program
-
- val description: String
-
-
- //Maybe adding some dependency declaration and tree checking methods
-
-}
diff --git a/src/main/scala/leon/PassManager.scala b/src/main/scala/leon/PassManager.scala
deleted file mode 100644
index 307a227ffb0ce0decb39624b1dde34bc6a589a39..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/PassManager.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-package leon
-
-import purescala.Definitions._
-
-class PassManager(passes: Seq[Pass]) {
-
- def run(program: Program): Program = {
- passes.foldLeft(program)((pgm, pass) => {
- Logger.debug("Running Pass: " + pass.description, 1, "passman")
- val newPgm = pass(pgm)
- TypeChecking(newPgm)
- Logger.debug("Resulting program: " + newPgm, 3, "passman")
- newPgm
- })
- }
-
-}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index dc88a7cb365f1942aa5bfa5ebdf6841057cb30bd..4c15d2cbea3ad72442aca4a42b12c39eebaa285d 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -27,4 +27,10 @@ object Settings {
var debugLevel: Int = 0
var debugTags: Set[String] = Set.empty
var simpleOutput: Boolean = false
+ var synthesis: Boolean = false
+ var transformProgram: Boolean = true
+ var stopAfterExtraction: Boolean = false
+ var stopAfterTransformation: Boolean = false
+ var stopAfterAnalysis: Boolean = true
+ var silentlyTolerateNonPureBodies: Boolean = false
}
diff --git a/src/main/scala/leon/Simplificator.scala b/src/main/scala/leon/Simplificator.scala
index d52d6fe0d380b90424c239f3d302fb3620d502c4..c9de13922b3a93ee8e9055046dfcf020bd64c74e 100644
--- a/src/main/scala/leon/Simplificator.scala
+++ b/src/main/scala/leon/Simplificator.scala
@@ -5,8 +5,9 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object Simplificator extends Pass {
+object Simplificator extends plugin.TransformationPhase {
+ val name = "Simplificator"
val description = "Some safe and minimal simplification"
def apply(pgm: Program): Program = {
diff --git a/src/main/scala/leon/TypeChecking.scala b/src/main/scala/leon/TypeChecking.scala
index f6d4b259f19ab5e19e462cd4ba137d39bba16917..67a2e1bafb7e9d2e9f7f4c169ee77918b45d73d1 100644
--- a/src/main/scala/leon/TypeChecking.scala
+++ b/src/main/scala/leon/TypeChecking.scala
@@ -5,11 +5,12 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object TypeChecking extends Pass {
+object TypeChecking extends plugin.UnitPhase {
+ val name = "Type Checking"
val description = "Type check the AST"
- def apply(pgm: Program): Program = {
+ def apply(pgm: Program): Unit = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => {
@@ -17,8 +18,6 @@ object TypeChecking extends Pass {
fd.postcondition.foreach(typeCheck)
fd.body.foreach(typeCheck)
})
-
- pgm
}
private def typeCheck(expr: Expr): Unit = { //expr match {
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index 2c5d4d5a532614873b9b6786481e82f0ebd4a3de..f653b8b7c8d9cd75e1dc60b400410316d1dcb6b3 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -5,8 +5,9 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object UnitElimination extends Pass {
+object UnitElimination extends plugin.TransformationPhase {
+ val name = "Unit Elimination"
val description = "Remove all usage of the Unit type and value"
private var fun2FreshFun: Map[FunDef, FunDef] = Map()
diff --git a/src/main/scala/leon/plugin/AnalysisComponent.scala b/src/main/scala/leon/plugin/AnalysisComponent.scala
index 08b94f8304030fedd3cc8b19c6fbff5ae255c8b1..0578055c5d0486bcaa544dba6b7d090685fe2d91 100644
--- a/src/main/scala/leon/plugin/AnalysisComponent.scala
+++ b/src/main/scala/leon/plugin/AnalysisComponent.scala
@@ -4,7 +4,10 @@ package plugin
import scala.tools.nsc._
import scala.tools.nsc.plugins._
-class AnalysisComponent(val global: Global, val pluginInstance: LeonPlugin)
+import purescala.Definitions.Program
+import synthesis.SynthesisPhase
+
+class AnalysisComponent(val global: Global, val leonReporter: Reporter, val pluginInstance: LeonPlugin)
extends PluginComponent
with CodeExtraction
{
@@ -22,7 +25,7 @@ class AnalysisComponent(val global: Global, val pluginInstance: LeonPlugin)
protected def stopIfErrors: Unit = {
if(reporter.hasErrors) {
if(Settings.simpleOutput)
- println("error")
+ leonReporter.fatalError("errrr")
sys.exit(1)
//throw new Exception("There were errors.")
}
@@ -31,34 +34,58 @@ class AnalysisComponent(val global: Global, val pluginInstance: LeonPlugin)
def newPhase(prev: Phase) = new AnalysisPhase(prev)
class AnalysisPhase(prev: Phase) extends StdPhase(prev) {
+ def computeLeonPhases: List[LeonPhase] = {
+ List(
+ if (Settings.transformProgram) {
+ List(
+ ArrayTransformation,
+ EpsilonElimination,
+ ImperativeCodeElimination,
+ /*UnitElimination,*/
+ FunctionClosure,
+ /*FunctionHoisting,*/
+ Simplificator
+ )
+ } else {
+ Nil
+ }
+ ,
+ if (Settings.synthesis)
+ List(
+ new SynthesisPhase(leonReporter)
+ )
+ else
+ Nil
+ ,
+ if (!Settings.stopAfterTransformation) {
+ List(
+ AnalysisPhase
+ )
+ } else {
+ Nil
+ }
+ ).flatten
+ }
+
def apply(unit: CompilationUnit): Unit = {
//global ref to freshName creator
fresh = unit.fresh
- val prog: purescala.Definitions.Program = extractCode(unit)
- if(pluginInstance.stopAfterExtraction) {
- println("Extracted program for " + unit + ": ")
- println(prog)
- println("Extraction complete. Now terminating the compiler process.")
+ var ac = LeonContext(program = extractCode(unit))
+
+ if(Settings.stopAfterExtraction) {
+ leonReporter.info("Extracted program for " + unit + ": ")
+ leonReporter.info(ac.program)
sys.exit(0)
- } else {
- if(!pluginInstance.actionAfterExtraction.isDefined) {
- println("Extracted program for " + unit + ". Re-run with -P:leon:parse to see the output.")
- }
- //println(prog)
}
- if(!pluginInstance.actionAfterExtraction.isDefined) {
- println("Starting analysis.")
- val analysis = new Analysis(prog)
- analysis.analyse
- if(pluginInstance.stopAfterAnalysis) {
- println("Analysis complete. Now terminating the compiler process.")
- sys.exit(0)
- }
- } else {
- pluginInstance.actionAfterExtraction.get(prog)
+ val phases = computeLeonPhases
+
+ for ((phase, i) <- phases.zipWithIndex) {
+ leonReporter.info("%2d".format(i)+": "+phase.name)
+ ac = phase.run(ac)
}
+
}
}
}
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 24f49dfab090b3b7735671faaa98a4b1b252b3ed..9c2d4fbf80afe77e878ec4fb1892365a69fad44e 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -289,7 +289,7 @@ trait CodeExtraction extends Extractors {
}
val bodyAttempt = try {
- Some(flattenBlocks(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies)(realBody)))
+ Some(flattenBlocks(scala2PureScala(unit, Settings.silentlyTolerateNonPureBodies)(realBody)))
} catch {
case e: ImpureCodeEncounteredException => None
}
@@ -441,7 +441,7 @@ trait CodeExtraction extends Extractors {
realBody match {
case ExEnsuredExpression(body2, resSym, contract) => {
varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType))
- val c1 = scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies) (contract)
+ val c1 = scala2PureScala(unit, Settings.silentlyTolerateNonPureBodies) (contract)
// varSubsts.remove(resSym)
realBody = body2
ensCont = Some(c1)
@@ -456,13 +456,13 @@ trait CodeExtraction extends Extractors {
realBody match {
case ExRequiredExpression(body3, contract) => {
realBody = body3
- reqCont = Some(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies) (contract))
+ reqCont = Some(scala2PureScala(unit, Settings.silentlyTolerateNonPureBodies) (contract))
}
case _ => ;
}
val bodyAttempt = try {
- Some(flattenBlocks(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies)(realBody)))
+ Some(flattenBlocks(scala2PureScala(unit, Settings.silentlyTolerateNonPureBodies)(realBody)))
} catch {
case e: ImpureCodeEncounteredException => None
}
diff --git a/src/main/scala/leon/plugin/LeonContext.scala b/src/main/scala/leon/plugin/LeonContext.scala
new file mode 100644
index 0000000000000000000000000000000000000000..29274a5fdd6d602007ce2be7956b79566f37dd2c
--- /dev/null
+++ b/src/main/scala/leon/plugin/LeonContext.scala
@@ -0,0 +1,9 @@
+package leon
+package plugin
+
+import purescala.Definitions.Program
+
+case class LeonContext(
+ val program: Program
+)
+
diff --git a/src/main/scala/leon/plugin/LeonPhase.scala b/src/main/scala/leon/plugin/LeonPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..13f437ea4b0f1e9eb0846cb6921980320723f62d
--- /dev/null
+++ b/src/main/scala/leon/plugin/LeonPhase.scala
@@ -0,0 +1,23 @@
+package leon
+package plugin
+
+import purescala.Definitions.Program
+
+abstract class LeonPhase {
+ val name: String
+ val description: String
+
+ def run(ac: LeonContext): LeonContext
+}
+
+abstract class TransformationPhase extends LeonPhase {
+ def apply(p: Program): Program
+
+ override def run(ac: LeonContext) = ac.copy(program = apply(ac.program))
+}
+
+abstract class UnitPhase extends LeonPhase {
+ def apply(p: Program): Unit
+
+ override def run(ac: LeonContext) = { apply(ac.program); ac }
+}
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index e37b5b1a8c047cc5b7af6ab26d5cdabb03731287..b2efd9d536d779036ebd8fa8665c0369969af00b 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -7,16 +7,12 @@ import scala.tools.nsc.plugins.{Plugin,PluginComponent}
import purescala.Definitions.Program
/** This class is the entry point for the plugin. */
-class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=>Unit] = None) extends Plugin {
+class LeonPlugin(val global: Global, val reporter: Reporter) extends Plugin {
import global._
val name = "leon"
val description = "The Leon static analyzer"
- var stopAfterAnalysis: Boolean = true
- var stopAfterExtraction: Boolean = false
- var silentlyTolerateNonPureBodies: Boolean = false
-
/** The help message displaying the options for that plugin. */
override val optionsHelp: Option[String] = Some(
" --uniqid When pretty-printing purescala trees, show identifiers IDs" + "\n" +
@@ -43,7 +39,8 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
" --noverifymodel Do not verify the correctness of models returned by Z3" + "\n" +
" --debug=[1-5] Debug level" + "\n" +
" --tags=t1:... Filter out debug information that are not of one of the given tags" + "\n" +
- " --oneline Reduce the output to a single line: valid if all properties were valid, invalid if at least one is invalid, unknown else"
+ " --oneline Reduce the output to a single line: valid if all properties were valid, invalid if at least one is invalid, unknown else" + "\n" +
+ " --synthesis Magic!"
)
/** Processes the command-line options. */
@@ -51,10 +48,10 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
override def processOptions(options: List[String], error: String => Unit) {
for(option <- options) {
option match {
- case "with-code" => stopAfterAnalysis = false
+ case "with-code" => leon.Settings.stopAfterAnalysis = false
case "uniqid" => leon.Settings.showIDs = true
- case "parse" => stopAfterExtraction = true
- case "tolerant" => silentlyTolerateNonPureBodies = true
+ case "parse" => leon.Settings.stopAfterExtraction = true
+ case "tolerant" => leon.Settings.silentlyTolerateNonPureBodies = true
case "nodefaults" => leon.Settings.runDefaultExtensions = false
case "axioms" => leon.Settings.noForallAxioms = false
case "bapa" => leon.Settings.useBAPA = true
@@ -68,6 +65,9 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
case "oneline" => leon.Settings.simpleOutput = true
case "noLuckyTests" => leon.Settings.luckyTest = false
case "noverifymodel" => leon.Settings.verifyModel = false
+ case "synthesis" => leon.Settings.synthesis = true;
+ leon.Settings.transformProgram = false;
+ leon.Settings.stopAfterTransformation = true;
case s if s.startsWith("debug=") => leon.Settings.debugLevel = try { s.substring("debug=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("tags=") => leon.Settings.debugTags = Set(splitList(s.substring("tags=".length, s.length)): _*)
@@ -82,6 +82,6 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
}
}
- val components = List[PluginComponent](new AnalysisComponent(global, this))
+ val components = List(new AnalysisComponent(global, reporter, this))
val descriptions = List[String]("leon analyses")
}
diff --git a/src/main/scala/leon/plugin/SimpleReporter.scala b/src/main/scala/leon/plugin/SimpleReporter.scala
index 0d8e4b0adf6d93d355c5bfaf57f49916b630851b..31cc4d7b132be2dafb1b712bc5355eadba35c46b 100644
--- a/src/main/scala/leon/plugin/SimpleReporter.scala
+++ b/src/main/scala/leon/plugin/SimpleReporter.scala
@@ -4,10 +4,11 @@ package plugin
import scala.tools.nsc.Settings
import scala.tools.nsc.reporters.AbstractReporter
import scala.tools.nsc.util._
+import scala.tools.util.StringOps
/** This implements a reporter that calls the callback with every line that a
regular ConsoleReporter would display. */
-class SimpleReporter(val settings: Settings, callback: String => Unit) extends AbstractReporter {
+class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends AbstractReporter {
final val ERROR_LIMIT = 5
private def label(severity: Severity): String = severity match {
@@ -22,10 +23,10 @@ class SimpleReporter(val settings: Settings, callback: String => Unit) extends A
}
private def getCountString(severity: Severity): String =
- countElementsAsString((severity).count, label(severity))
+ StringOps.countElementsAsString((severity).count, label(severity))
/** Prints the message. */
- def printMessage(msg: String) { callback(msg) }
+ def printMessage(msg: String) { reporter.info(msg) }
/** Prints the message with the given position indication. */
def printMessage(posIn: Position, msg: String) {
diff --git a/src/main/scala/leon/synthesis/Main.scala b/src/main/scala/leon/synthesis/Main.scala
index 10520ef26cd2f4b0d67c7bc437b941f2c2f96d53..a3704d349db726b52bcd657fbecb94d31a67f404 100644
--- a/src/main/scala/leon/synthesis/Main.scala
+++ b/src/main/scala/leon/synthesis/Main.scala
@@ -2,11 +2,4 @@ package leon
package synthesis
object Main {
- def main(args : Array[String]) {
- val reporter = new DefaultReporter
- val solvers = List(new TrivialSolver(reporter))
-
- new Synthesizer(reporter, solvers).test()
- }
-
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 0472c87ecedc0942805991b3253adceb02da8cca..5d7af0d5f1e4659335c6f24e8471e4f5c805418c 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -64,6 +64,25 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
def isApplicable(p: Problem, parent: Task): List[Task] = {
- Nil
+ if (p.as.isEmpty) {
+ synth.solveSAT(p.phi) match {
+ case (Some(true), model) =>
+ val onSuccess: List[Solution] => Solution = {
+ case Nil => Solution(BooleanLiteral(true), replaceFromIDs(model, p.phi))
+ }
+
+ List(new Task(synth, parent, this, p, Nil, onSuccess, 200))
+ case (Some(false), model) =>
+ val onSuccess: List[Solution] => Solution = {
+ case Nil => Solution(BooleanLiteral(false), BooleanLiteral(false))
+ }
+
+ List(new Task(synth, parent, this, p, Nil, onSuccess, 200))
+ case _ =>
+ Nil
+ }
+ } else {
+ Nil
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..da729fe3c23143f87ad3ff0cdb0f0243e6d6eeaf
--- /dev/null
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -0,0 +1,18 @@
+package leon
+package synthesis
+
+import purescala.Definitions.Program
+
+class SynthesisPhase(reporter: Reporter) extends plugin.TransformationPhase {
+ val name = "Synthesis"
+ val description = "Synthesis"
+
+ def apply(program: Program): Program = {
+ val solvers = List(
+ new TrivialSolver(reporter),
+ new FairZ3Solver(reporter)
+ )
+
+ new Synthesizer(reporter, solvers).synthesizeAll(program)
+ }
+}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 3f7ba6a85355b9cb7ccf6249cb1dfce890b34b8d..c8dccc8ba481d013fd073419d6cc4a3c725869d8 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -1,7 +1,10 @@
package leon
package synthesis
+import purescala.Common._
import purescala.Definitions.Program
+import purescala.Trees.{Expr, Not}
+
import Extensions.Solver
import collection.mutable.PriorityQueue
@@ -61,6 +64,19 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
solution
}
+ def solveSAT(phi: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
+ for (s <- solvers) {
+ s.solveOrGetCounterexample(Not(phi)) match {
+ case (Some(true), _) =>
+ return (Some(false), Map())
+ case (Some(false), model) =>
+ return (Some(true), model)
+ case _ =>
+ }
+ }
+ (None, Map())
+ }
+
def onTaskSucceeded(task: Task, solution: Solution) {
info(" => Solved "+task.problem+" ⊢ "+solution)
task match {
@@ -83,5 +99,9 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
synthesize(p, Rules.all(this))
}
-}
+ def synthesizeAll(program: Program) = {
+ solvers.foreach(_.setProgram(program))
+ program
+ }
+}