From 51f3e6a46bae5eeff576848579ac467d2fa1d6a3 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 7 Aug 2013 18:38:00 +0200
Subject: [PATCH] Reshape options, add debug sections, simplify reporters
- Debug sections can be toggled to enable detailled information
- Options can be explicitly turned off, --debug:options lists all
- Switch from multiple reporters to a single one to rule them all
- Turn cegis:gencalls on by default
---
src/main/scala/leon/LeonContext.scala | 8 +-
src/main/scala/leon/LeonOption.scala | 38 +++--
src/main/scala/leon/Main.scala | 148 ++++++++++++------
src/main/scala/leon/Reporter.scala | 50 ++++--
src/main/scala/leon/Settings.scala | 32 ++--
src/main/scala/leon/purescala/Common.scala | 5 +-
src/main/scala/leon/purescala/TreeOps.scala | 10 +-
.../leon/solvers/z3/FairZ3Component.scala | 15 ++
.../scala/leon/solvers/z3/FairZ3Solver.scala | 71 ++++-----
.../leon/synthesis/LinearEquations.scala | 3 +-
.../scala/leon/synthesis/ParallelSearch.scala | 5 +-
src/main/scala/leon/synthesis/Solution.scala | 2 +-
.../leon/synthesis/SynthesisOptions.scala | 6 +-
.../scala/leon/synthesis/SynthesisPhase.scala | 64 +++++---
.../scala/leon/synthesis/Synthesizer.scala | 12 +-
.../scala/leon/synthesis/rules/Cegis.scala | 28 +---
.../leon/synthesis/utils/Benchmarks.scala | 9 +-
.../scala/leon/test/TestSilentReporter.scala | 6 +
src/test/scala/leon/test/TestUtils.scala | 1 +
.../test/evaluators/EvaluatorsTests.scala | 2 +-
.../scala/leon/test/purescala/DataGen.scala | 2 +-
.../scala/leon/test/purescala/LikelyEq.scala | 5 +-
.../purescala/TreeNormalizationsTests.scala | 4 +-
.../leon/test/purescala/TreeOpsTests.scala | 6 +-
.../test/solvers/z3/FairZ3SolverTests.scala | 6 +-
.../solvers/z3/FairZ3SolverTestsNewAPI.scala | 6 +-
.../z3/UninterpretedZ3SolverTests.scala | 6 +-
.../leon/test/synthesis/SynthesisSuite.scala | 5 +-
.../PureScalaVerificationRegression.scala | 6 +-
.../XLangVerificationRegression.scala | 2 +-
30 files changed, 324 insertions(+), 239 deletions(-)
create mode 100644 src/main/scala/leon/solvers/z3/FairZ3Component.scala
create mode 100644 src/test/scala/leon/test/TestSilentReporter.scala
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index b271db3a4..8be9ae0b3 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -9,8 +9,8 @@ import java.io.File
* Contexts are immutable, and so should all there fields (with the possible
* exception of the reporter). */
case class LeonContext(
- val settings: Settings = Settings(),
- val options: Seq[LeonOption] = Seq.empty,
- val files: Seq[File] = Seq.empty,
- val reporter: Reporter = new DefaultReporter
+ settings: Settings = Settings(),
+ options: Seq[LeonOption] = Seq(),
+ files: Seq[File] = Seq(),
+ reporter: Reporter = new DefaultReporter()
)
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 08ebbbb2c..d1379cf38 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -8,8 +8,14 @@ sealed abstract class LeonOption {
}
/** Boolean (on/off) options. Present means "on". */
-case class LeonFlagOption(name: String) extends LeonOption {
- override def toString() : String = "--" + name
+case class LeonFlagOption(name: String, value: Boolean) extends LeonOption {
+ override def toString() : String = {
+ if (value) {
+ "--" + name
+ } else {
+ "--" + name + "=off"
+ }
+ }
}
/** Options of the form --option=value. */
@@ -31,22 +37,26 @@ sealed abstract class LeonOptionDef {
val name: String
val usageOption: String
val usageDesc: String
- val isFlag: Boolean
}
-case class LeonFlagOptionDef(name: String, usageOption: String, usageDesc: String) extends LeonOptionDef {
- val isFlag = true
-}
+case class LeonFlagOptionDef(name: String,
+ usageOption: String,
+ usageDesc: String,
+ default: Boolean = false) extends LeonOptionDef
-case class LeonValueOptionDef(name: String, usageOption: String, usageDesc: String) extends LeonOptionDef {
- val isFlag = false
-}
-
-case class LeonOptValueOptionDef(name: String, usageOption: String, usageDesc: String) extends LeonOptionDef {
- val isFlag = false
-}
+case class LeonValueOptionDef(name: String,
+ usageOption: String,
+ usageDesc: String,
+ flagValue: Option[String] = None,
+ default: Option[String] = None) extends LeonOptionDef
object ListValue {
def apply(values: Seq[String]) = values.mkString(":")
- def unapply(value: String): Option[Seq[String]] = Some(value.split(':').map(_.trim).filter(!_.isEmpty))
+ def unapply(value: String): Option[Seq[String]] = {
+ if (value == "off") {
+ None
+ } else {
+ Some(value.split(':').map(_.trim).filter(!_.isEmpty))
+ }
+ }
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 88c072dcf..bd9ee762e 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -21,22 +21,15 @@ object Main {
// Add whatever you need here.
lazy val allComponents : Set[LeonComponent] = allPhases.toSet ++ Set(
- // It's a little unfortunate that we need to build one...
- new solvers.z3.FairZ3Solver(LeonContext())
+ new solvers.z3.FairZ3Component{}
)
lazy val topLevelOptions : Set[LeonOptionDef] = Set(
- LeonFlagOptionDef ("termination", "--termination", "Check program termination"),
- LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
- LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
- LeonFlagOptionDef ("parse", "--parse", "Checks only whether the program is valid PureScala"),
- LeonValueOptionDef("debug", "--debug=[1-5]", "Debug level"),
- LeonFlagOptionDef ("help", "--help", "Show help")
-
- // Unimplemented Options:
- //
- // LeonFlagOptionDef("uniqid", "--uniqid", "When pretty-printing purescala trees, show identifiers IDs"),
- // LeonFlagOptionDef("tolerant", "--tolerant", "Silently extracts non-pure function bodies as ''unknown''"),
+ LeonFlagOptionDef ("termination", "--termination", "Check program termination"),
+ LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
+ LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
+ LeonValueOptionDef("debug", "--debug=<sections..>", "Enables specific messages"),
+ LeonFlagOptionDef ("help", "--help", "Show help")
)
lazy val allOptions = allComponents.flatMap(_.definedOptions) ++ topLevelOptions
@@ -62,9 +55,11 @@ object Main {
sys.exit(1)
}
- def processOptions(reporter: Reporter, args: Seq[String]): LeonContext = {
+ def processOptions(args: Seq[String]): LeonContext = {
val phases = allPhases
+ val initReporter = new DefaultReporter()
+
val allOptions = this.allOptions
val allOptionsMap = allOptions.map(o => o.name -> o).toMap
@@ -74,50 +69,108 @@ object Main {
val files = args.filterNot(_.startsWith("-")).map(new java.io.File(_))
- val leonOptions = options.flatMap { opt =>
- val leonOpt: LeonOption = opt.substring(2, opt.length).split("=", 2).toList match {
+ def valueToFlag(s: String) = s match {
+ case "on" | "true" | "yes" => Some(true)
+ case "off" | "false" | "no" => Some(false)
+ case _ => None
+ }
+
+ var optionsValues: Map[LeonOptionDef, String] = allOptions.flatMap{
+ case fod: LeonFlagOptionDef =>
+ Some((fod, if (fod.default) "on" else "off"))
+ case vod: LeonValueOptionDef =>
+ vod.default.map(d =>
+ (vod, d)
+ )
+ }.toMap
+
+ for (opt <- options) {
+ val (name, value) = opt.substring(2, opt.length).split("=", 2).toList match {
case List(name, value) =>
- LeonValueOption(name, value)
+ (name, Some(value))
case List(name) =>
- LeonFlagOption(name)
+ (name, None)
+ }
+
+ val optV = allOptionsMap.get(name) match {
+ case Some(fod: LeonFlagOptionDef) =>
+ value.orElse(Some("on"))
+
+ case Some(vod: LeonValueOptionDef) =>
+ value.orElse(vod.flagValue)
+
case _ =>
- reporter.fatalError("Woot?")
+ None
}
- if (allOptionsMap contains leonOpt.name) {
- (allOptionsMap(leonOpt.name), leonOpt) match {
- case (_: LeonFlagOptionDef | _: LeonOptValueOptionDef, LeonFlagOption(name)) =>
- Some(leonOpt)
- case (_: LeonValueOptionDef | _: LeonOptValueOptionDef, LeonValueOption(name, value)) =>
- Some(leonOpt)
- case _ =>
- reporter.error("Invalid option usage: " + opt)
- displayHelp(reporter)
- None
+ if (allOptionsMap contains name) {
+ optV.foreach { v =>
+ optionsValues += allOptionsMap(name) -> v
}
} else {
- reporter.error("leon: '"+opt+"' is not a valid option. See 'leon --help'")
+ initReporter.error("'"+name+"' is not a valid option. See 'leon --help'")
None
}
}
+ val leonOptions = optionsValues.flatMap {
+ case (fod: LeonFlagOptionDef, value) =>
+ valueToFlag(value) match {
+ case Some(v) =>
+ Some(LeonFlagOption(fod.name, v))
+ case None =>
+ initReporter.error("Invalid option usage: --"+fod.name+"="+value)
+ displayHelp(initReporter)
+ None
+ }
+ case (vod: LeonValueOptionDef, value) =>
+ Some(LeonValueOption(vod.name, value))
+ }.toSeq
+
+
+
var settings = Settings()
// Process options we understand:
for(opt <- leonOptions) opt match {
- case LeonFlagOption("termination") =>
- settings = settings.copy(termination = true, xlang = false, verify = false, synthesis = false)
- case LeonFlagOption("synthesis") =>
- settings = settings.copy(synthesis = true, xlang = false, verify = false)
- case LeonFlagOption("xlang") =>
- settings = settings.copy(synthesis = false, xlang = true)
- case LeonFlagOption("parse") =>
- settings = settings.copy(synthesis = false, xlang = false, verify = false)
- case LeonFlagOption("help") =>
- displayHelp(reporter)
+ case LeonFlagOption("termination", value) =>
+ settings = settings.copy(termination = value)
+ case LeonFlagOption("synthesis", value) =>
+ settings = settings.copy(synthesis = value)
+ case LeonFlagOption("xlang", value) =>
+ settings = settings.copy(xlang = value)
+ case LeonValueOption("debug", ListValue(sections)) =>
+ val debugSections = sections.flatMap { s =>
+ ReportingSections.all.find(_.name == s) match {
+ case Some(rs) =>
+ Some(rs)
+ case None =>
+ initReporter.error("Section "+s+" not found, available: "+ReportingSections.all.map(_.name).mkString(", "))
+ None
+ }
+ }
+ settings = settings.copy(debugSections = debugSections.toSet)
+ case LeonFlagOption("help", true) =>
+ displayHelp(initReporter)
case _ =>
}
+ // Create a new reporter taking debugSections into account
+ val reporter = new DefaultReporter(settings.debugSections)
+
+ reporter.ifDebug(ReportingOptions) {
+ val debug = reporter.debug(ReportingOptions)_
+
+ debug("Options considered by Leon:")
+ for (lo <- leonOptions) lo match {
+ case LeonFlagOption(name, v) =>
+ debug(" --"+name+"="+(if(v) "on" else "off"))
+ case LeonValueOption(name, v) =>
+ debug(" --"+name+"="+v)
+
+ }
+ }
+
LeonContext(settings = settings, reporter = reporter, files = files, options = leonOptions)
}
@@ -126,16 +179,10 @@ object Main {
val pipeBegin : Pipeline[List[String],Program] = plugin.ExtractionPhase andThen SubtypingPhase
- val pipeSynthesis: Pipeline[Program, Program] =
+ val pipeProcess: Pipeline[Program, Any] =
if (settings.synthesis) {
synthesis.SynthesisPhase
- } else {
- NoopPhase()
- }
-
- val pipeVerify: Pipeline[Program, Any] =
- if (settings.termination) {
- // OK, OK, that's not really verification...
+ } else if (settings.termination) {
termination.TerminationPhase
} else if (settings.xlang) {
xlang.XlangAnalysisPhase
@@ -146,15 +193,14 @@ object Main {
}
pipeBegin andThen
- pipeSynthesis andThen
- pipeVerify
+ pipeProcess
}
def main(args : Array[String]) {
val reporter = new DefaultReporter()
// Process options
- val ctx = processOptions(reporter, args.toList)
+ val ctx = processOptions(args.toList)
// Compute leon pipeline
val pipeline = computePipeline(ctx.settings)
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 8db2e5acf..028408583 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -6,11 +6,12 @@ import purescala.Definitions.Definition
import purescala.Trees.Expr
import purescala.PrettyPrinter
-abstract class Reporter {
- def infoFunction(msg: Any) : Unit
- def warningFunction(msg: Any) : Unit
+abstract class Reporter(enabledSections: Set[ReportingSection]) {
+ def infoFunction(msg: Any) : Unit
+ def warningFunction(msg: Any) : Unit
def errorFunction(msg: Any) : Unit
def fatalErrorFunction(msg: Any) : Nothing
+ def debugFunction(msg: Any) : Unit
// This part of the implementation is non-negociable.
private var _errorCount : Int = 0
@@ -32,19 +33,37 @@ abstract class Reporter {
_errorCount += 1
fatalErrorFunction(msg)
}
+
+ val debugMask = enabledSections.foldLeft(0){ _ | _.mask }
+
+ final def debug(section: ReportingSection)(msg: => Any) = {
+ ifDebug(section) { debugFunction(msg) }
+ }
+
+ final def ifDebug(section: ReportingSection)(body: => Unit) = {
+ if ((debugMask & section.mask) == section.mask) {
+ body
+ }
+ }
}
-class DefaultReporter extends Reporter {
+
+class DefaultReporter(enabledSections: Set[ReportingSection] = Set()) extends Reporter(enabledSections) {
protected val errorPfx = "[ Error ] "
protected val warningPfx = "[Warning] "
protected val infoPfx = "[ Info ] "
protected val fatalPfx = "[ Fatal ] "
+ protected val debugPfx = "[ Debug ] "
def output(msg: String) : Unit = println(msg)
protected def reline(pfx: String, msg: String) : String = {
- val color = if(pfx == errorPfx || pfx == warningPfx || pfx == fatalPfx) {
+ val color = if(pfx == errorPfx || pfx == fatalPfx) {
Console.RED
+ } else if(pfx == warningPfx) {
+ Console.YELLOW
+ } else if(pfx == debugPfx) {
+ Console.MAGENTA
} else {
Console.BLUE
}
@@ -56,14 +75,21 @@ class DefaultReporter extends Reporter {
def warningFunction(msg: Any) = output(reline(warningPfx, msg.toString))
def infoFunction(msg: Any) = output(reline(infoPfx, msg.toString))
def fatalErrorFunction(msg: Any) = { output(reline(fatalPfx, msg.toString)); throw LeonFatalError() }
+ def debugFunction(msg: Any) = output(reline(debugPfx, msg.toString))
}
-class QuietReporter extends DefaultReporter {
- override def warningFunction(msg : Any) = {}
- override def infoFunction(msg : Any) = {}
-}
+sealed abstract class ReportingSection(val name: String, val mask: Int)
+
+case object ReportingSolver extends ReportingSection("solver", 1 << 0)
+case object ReportingSynthesis extends ReportingSection("synthesis", 1 << 1)
+case object ReportingTimers extends ReportingSection("timers", 1 << 2)
+case object ReportingOptions extends ReportingSection("options", 1 << 3)
-class SilentReporter extends QuietReporter {
- override def errorFunction(msg : Any) = {}
- override def fatalErrorFunction(msg: Any) = throw LeonFatalError()
+object ReportingSections {
+ val all = Set[ReportingSection](
+ ReportingSolver,
+ ReportingSynthesis,
+ ReportingTimers,
+ ReportingOptions
+ )
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index a9605e620..a121d69ca 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -2,14 +2,22 @@
package leon
-// typically these settings can be changed through some command-line switch.
-// TODO this global object needs to die (or at least clean out of its var's)
-object Settings {
- lazy val reporter: Reporter = new DefaultReporter
+case class Settings(
+ val strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
+ val debugSections: Set[ReportingSection] = Set(), // Enables debug message for the following sections
+ val termination: Boolean = false,
+ val synthesis: Boolean = false,
+ val xlang: Boolean = false,
+ val verify: Boolean = true,
+ val classPath: List[String] = Settings.defaultClassPath()
+)
- var showIDs: Boolean = false
+object Settings {
+ // This is a list of directories that is passed as class-path of the inner-compiler.
+ // It needs to contain at least a directory containing scala-library.jar, and
+ // one for the leon runtime library.
- def defaultClassPath() = {
+ private def defaultClassPath() = {
val leonLib = System.getenv("LEON_LIBRARY_PATH")
if (leonLib == "" || leonLib == null) {
sys.error("LEON_LIBRARY_PATH env variable is undefined")
@@ -32,15 +40,3 @@ object Settings {
leonCPs :: scalaCPs
}
}
-
-case class Settings(
- val strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
- val termination: Boolean = false,
- val synthesis: Boolean = false,
- val xlang: Boolean = false,
- val verify: Boolean = true,
- // This is a list of directories that is passed as class-path of the inner-compiler.
- // It needs to contain at least a directory containing scala-library.jar, and
- // one for the leon runtime library.
- val classPath: List[String] = Settings.defaultClassPath()
-)
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 45142714e..6ca933b74 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -21,10 +21,7 @@ object Common {
override def hashCode: Int = globalId
override def toString: String = {
- if(Settings.showIDs) {
- // angle brackets: name + "\u3008" + id + "\u3009"
- name + "[" + id + "]"
- } else if(alwaysShowUniqueID) {
+ if(alwaysShowUniqueID) {
name + (if(id > 0) id else "")
} else {
name
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 405055e44..77ded68f1 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -46,7 +46,7 @@ object TreeOps {
def rec(ex: Expr, skip: Expr = null) : Expr = (if (ex == skip) None else subst(ex)) match {
case Some(newExpr) => {
if(newExpr.getType == Untyped) {
- Settings.reporter.error("REPLACING IN EXPRESSION WITH AN UNTYPED TREE ! " + ex + " --to--> " + newExpr)
+ sys.error("REPLACING IN EXPRESSION WITH AN UNTYPED TREE ! " + ex + " --to--> " + newExpr)
}
if(ex == newExpr)
if(recursive) rec(ex, ex) else ex
@@ -155,8 +155,8 @@ object TreeOps {
case Some(newEx) => {
somethingChanged = true
if(newEx.getType == Untyped) {
- Settings.reporter.warning("REPLACING [" + ex + "] WITH AN UNTYPED EXPRESSION !")
- Settings.reporter.warning("Here's the new expression: " + newEx)
+ sys.error("REPLACING [" + ex + "] WITH AN UNTYPED EXPRESSION !")
+ sys.error("Here's the new expression: " + newEx)
}
newEx
}
@@ -606,12 +606,12 @@ object TreeOps {
val intersection = vars intersect definitions
if(!intersection.isEmpty) {
intersection.foreach(id => {
- Settings.reporter.error("Variable with identifier '" + id + "' has escaped its let-definition !")
+ sys.error("Variable with identifier '" + id + "' has escaped its let-definition !")
})
false
} else {
vars.forall(id => if(id.isLetBinder) {
- Settings.reporter.error("Variable with identifier '" + id + "' has lost its let-definition (it disappeared??)")
+ sys.error("Variable with identifier '" + id + "' has lost its let-definition (it disappeared??)")
false
} else {
true
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Component.scala b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
new file mode 100644
index 000000000..14e3e4d55
--- /dev/null
+++ b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
@@ -0,0 +1,15 @@
+package leon
+package solvers.z3
+
+trait FairZ3Component extends LeonComponent {
+ val name = "Z3-f"
+ val description = "Fair Z3 Solver"
+
+ override val definedOptions : Set[LeonOptionDef] = Set(
+ LeonFlagOptionDef("evalground", "--evalground", "Use evaluator on functions applied to ground arguments"),
+ LeonFlagOptionDef("checkmodels", "--checkmodels", "Double-check counter-examples with evaluator"),
+ LeonFlagOptionDef("feelinglucky", "--feelinglucky", "Use evaluator to find counter-examples early"),
+ LeonFlagOptionDef("codegen", "--codegen", "Use compiled evaluator instead of interpreter"),
+ LeonFlagOptionDef("fairz3:unrollcores", "--fairz3:unrollcores", "Use unsat-cores to drive unrolling while remaining fair")
+ )
+}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 1a601470f..78d2e1d2b 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -24,21 +24,12 @@ import scala.collection.mutable.{Set => MutableSet}
class FairZ3Solver(context : LeonContext)
extends Solver(context)
with AbstractZ3Solver
- with Z3ModelReconstruction
- with LeonComponent {
+ with Z3ModelReconstruction
+ with FairZ3Component {
enclosing =>
- val name = "Z3-f"
- val description = "Fair Z3 Solver"
-
- override val definedOptions : Set[LeonOptionDef] = Set(
- LeonFlagOptionDef("evalground", "--evalground", "Use evaluator on functions applied to ground arguments"),
- LeonFlagOptionDef("checkmodels", "--checkmodels", "Double-check counter-examples with evaluator"),
- LeonFlagOptionDef("feelinglucky", "--feelinglucky", "Use evaluator to find counter-examples early"),
- LeonFlagOptionDef("codegen", "--codegen", "Use compiled evaluator instead of interpreter"),
- LeonFlagOptionDef("fairz3:unrollcores", "--fairz3:unrollcores", "Use unsat-cores to drive unrolling while remaining fair")
- )
+ def debug(s: String) = context.reporter.debug(ReportingSolver)(s)
// What wouldn't we do to avoid defining vars?
val (feelingLucky, checkModels, useCodeGen, evalGroundApps, unrollUnsatCores) = locally {
@@ -49,11 +40,11 @@ class FairZ3Solver(context : LeonContext)
var unrollUnsatCores = false
for(opt <- context.options) opt match {
- case LeonFlagOption("checkmodels") => check = true
- case LeonFlagOption("feelinglucky") => lucky = true
- case LeonFlagOption("codegen") => codegen = true
- case LeonFlagOption("evalground") => evalground = true
- case LeonFlagOption("fairz3:unrollcores") => unrollUnsatCores = true
+ case LeonFlagOption("checkmodels", v) => check = v
+ case LeonFlagOption("feelinglucky", v) => lucky = v
+ case LeonFlagOption("codegen", v) => codegen = v
+ case LeonFlagOption("evalground", v) => evalground = v
+ case LeonFlagOption("fairz3:unrollcores", v) => unrollUnsatCores = v
case _ =>
}
@@ -175,20 +166,20 @@ class FairZ3Solver(context : LeonContext)
evalResult match {
case EvaluationResults.Successful(BooleanLiteral(true)) =>
- reporter.info("- Model validated.")
+ debug("- Model validated.")
(true, asMap)
case EvaluationResults.Successful(BooleanLiteral(false)) =>
- reporter.info("- Invalid model.")
+ debug("- Invalid model.")
(false, asMap)
case EvaluationResults.RuntimeError(msg) =>
- reporter.info("- Model leads to runtime error.")
+ debug("- Model leads to runtime error.")
(false, asMap)
case EvaluationResults.EvaluatorError(msg) =>
if (silenceErrors) {
- reporter.info("- Model leads to evaluator error: " + msg)
+ debug("- Model leads to evaluator error: " + msg)
} else {
reporter.warning("Something went wrong. While evaluating the model, we got this : " + msg)
}
@@ -249,10 +240,10 @@ class FairZ3Solver(context : LeonContext)
def dumpBlockers = {
blockersInfo.groupBy(_._2._1).toSeq.sortBy(_._1).foreach { case (gen, entries) =>
- reporter.info("--- "+gen)
+ debug("--- "+gen)
for (((bast), (gen, origGen, ast, fis)) <- entries) {
- reporter.info(". "+bast +" ~> "+fis.map(_.funDef.id))
+ debug(". "+bast +" ~> "+fis.map(_.funDef.id))
}
}
}
@@ -483,11 +474,11 @@ class FairZ3Solver(context : LeonContext)
//val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.toSeq.map(toZ3Formula(_).get)
// println("Blocking set : " + blockingSet)
- reporter.info(" - Running Z3 search...")
+ debug(" - Running Z3 search...")
- // reporter.info("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
- // reporter.info("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
- // reporter.info("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
+ // debug("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
+ // debug("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
+ // debug("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
z3Time.start
solver.push() // FIXME: remove when z3 bug is fixed
@@ -495,7 +486,7 @@ class FairZ3Solver(context : LeonContext)
solver.pop() // FIXME: remove when z3 bug is fixed
z3Time.stop
- reporter.info(" - Finished search with blocked literals")
+ debug(" - Finished search with blocked literals")
res match {
case None =>
@@ -523,8 +514,8 @@ class FairZ3Solver(context : LeonContext)
scalaTime.stop
//lazy val modelAsString = model.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
- //reporter.info("- Found a model:")
- //reporter.info(modelAsString)
+ //debug("- Found a model:")
+ //debug(modelAsString)
foundAnswer(Some(true), model)
}
@@ -568,15 +559,15 @@ class FairZ3Solver(context : LeonContext)
}
- //reporter.info("UNSAT BECAUSE: "+solver.getUnsatCore.mkString("\n AND \n"))
- //reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
+ //debug("UNSAT BECAUSE: "+solver.getUnsatCore.mkString("\n AND \n"))
+ //debug("UNSAT BECAUSE: "+core.mkString(" AND "))
if (!forceStop) {
if (this.feelingLucky) {
// we need the model to perform the additional test
- reporter.info(" - Running search without blocked literals (w/ lucky test)")
+ debug(" - Running search without blocked literals (w/ lucky test)")
} else {
- reporter.info(" - Running search without blocked literals (w/o lucky test)")
+ debug(" - Running search without blocked literals (w/o lucky test)")
}
z3Time.start
@@ -587,10 +578,10 @@ class FairZ3Solver(context : LeonContext)
res2 match {
case Some(false) =>
- //reporter.info("UNSAT WITHOUT Blockers")
+ //debug("UNSAT WITHOUT Blockers")
foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
case Some(true) =>
- //reporter.info("SAT WITHOUT Blockers")
+ //debug("SAT WITHOUT Blockers")
if (this.feelingLucky && !forceStop) {
// we might have been lucky :D
luckyTime.start
@@ -612,11 +603,11 @@ class FairZ3Solver(context : LeonContext)
}
if(!foundDefinitiveAnswer) {
- reporter.info("- We need to keep going.")
+ debug("- We need to keep going.")
val toRelease = unrollingBank.getZ3BlockersToUnlock
- reporter.info(" - more unrollings")
+ debug(" - more unrollings")
for(id <- toRelease) {
unlockingTime.start
@@ -630,7 +621,7 @@ class FairZ3Solver(context : LeonContext)
unrollingTime.stop
}
- reporter.info(" - finished unrolling")
+ debug(" - finished unrolling")
}
}
}
@@ -643,7 +634,7 @@ class FairZ3Solver(context : LeonContext)
StopwatchCollections.get("FairZ3 Unlocking") += unlockingTime
StopwatchCollections.get("FairZ3 ScalaTime") += scalaTime
- //reporter.info(" !! DONE !! ")
+ //debug(" !! DONE !! ")
if(forceStop) {
None
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index 428c9ac69..713fcdd0b 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -14,7 +14,8 @@ import synthesis.Algebra._
object LinearEquations {
// This is a hack, but the use of an evaluator in this file is itself beyond that.
import evaluators._
- private lazy val evaluator = new DefaultEvaluator(LeonContext(), Program.empty)
+ // TODO: Kill with fire
+ private lazy val evaluator = new DefaultEvaluator(LeonContext(Settings(), Seq(), Seq(), new DefaultReporter()), Program.empty)
//eliminate one variable from normalizedEquation t + a1*x1 + ... + an*xn = 0
//return a mapping for each of the n variables in (pre, map, freshVars)
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index d9982a12d..ae02170fd 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -24,12 +24,11 @@ class ParallelSearch(synth: Synthesizer,
private[this] var contexts = List[SynthesisContext]()
def initWorkerContext(wr: ActorRef) = {
- val reporter = new SilentReporter
- val solver = new FairZ3Solver(synth.context.copy(reporter = reporter))
+ val solver = new FairZ3Solver(synth.context)
solver.setProgram(synth.program)
solver.initZ3
- val simpleSolver = new UninterpretedZ3Solver(synth.context.copy(reporter = reporter))
+ val simpleSolver = new UninterpretedZ3Solver(synth.context)
simpleSolver.setProgram(synth.program)
simpleSolver.initZ3
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 53c25e93b..61a60a2d8 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -32,7 +32,7 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
defs.foldLeft(term){ case (t, fd) => LetDef(fd, t) }
def toSimplifiedExpr(ctx: LeonContext, p: Program): Expr = {
- val uninterpretedZ3 = new UninterpretedZ3Solver(ctx.copy(reporter = new SilentReporter))
+ val uninterpretedZ3 = new UninterpretedZ3Solver(ctx)
uninterpretedZ3.setProgram(p)
val simplifiers = List[Expr => Expr](
diff --git a/src/main/scala/leon/synthesis/SynthesisOptions.scala b/src/main/scala/leon/synthesis/SynthesisOptions.scala
index 0e7294f72..c776ab044 100644
--- a/src/main/scala/leon/synthesis/SynthesisOptions.scala
+++ b/src/main/scala/leon/synthesis/SynthesisOptions.scala
@@ -15,7 +15,11 @@ case class SynthesisOptions(
manualSearch: Boolean = false,
// Cegis related options
- cegisGenerateFunCalls: Boolean = false,
+ cegisUseUninterpretedProbe: Boolean = false,
+ cegisUseUnsatCores: Boolean = true,
+ cegisUseOptTimeout: Boolean = true,
+ cegisUseBssFiltering: Boolean = true,
+ cegisGenerateFunCalls: Boolean = true,
cegisUseCETests: Boolean = true,
cegisUseCEPruning: Boolean = true,
cegisUseBPaths: Boolean = true,
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index fd210b24b..57dca4236 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -16,27 +16,32 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
val description = "Synthesis"
override val definedOptions : Set[LeonOptionDef] = Set(
- LeonFlagOptionDef( "inplace", "--inplace", "Debug level"),
- LeonOptValueOptionDef("parallel", "--parallel[=N]", "Parallel synthesis search using N workers"),
- LeonFlagOptionDef( "manual", "--manual", "Manual search"),
- LeonFlagOptionDef( "derivtrees", "--derivtrees", "Generate derivation trees"),
- LeonFlagOptionDef( "firstonly", "--firstonly", "Stop as soon as one synthesis solution is found"),
- LeonValueOptionDef( "timeout", "--timeout=T", "Timeout after T seconds when searching for synthesis solutions .."),
- LeonValueOptionDef( "costmodel", "--costmodel=cm", "Use a specific cost model for this search"),
- LeonValueOptionDef( "functions", "--functions=f1:f2", "Limit synthesis of choose found within f1,f2,.."),
- LeonFlagOptionDef( "cegis:gencalls", "--cegis:gencalls", "Include function calls in CEGIS generators"),
- LeonFlagOptionDef( "cegis:vanuatoo", "--cegis:vanuatoo", "Generate inputs using new korat-style generator")
+ LeonFlagOptionDef( "inplace", "--inplace", "Debug level"),
+ LeonValueOptionDef("parallel", "--parallel[=N]", "Parallel synthesis search using N workers", Some("5")),
+ LeonFlagOptionDef( "manual", "--manual", "Manual search"),
+ LeonFlagOptionDef( "derivtrees", "--derivtrees", "Generate derivation trees"),
+ LeonFlagOptionDef( "firstonly", "--firstonly", "Stop as soon as one synthesis solution is found", true),
+ LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when searching for synthesis solutions .."),
+ LeonValueOptionDef("costmodel", "--costmodel=cm", "Use a specific cost model for this search"),
+ LeonValueOptionDef("functions", "--functions=f1:f2", "Limit synthesis of choose found within f1,f2,.."),
+ // CEGIS options
+ LeonFlagOptionDef( "cegis:gencalls", "--cegis:gencalls", "Include function calls in CEGIS generators", true),
+ LeonFlagOptionDef( "cegis:unintprobe", "--cegis:unintprobe", "Check for UNSAT without bloecks and with uninterpreted functions", false),
+ LeonFlagOptionDef( "cegis:bssfilter", "--cegis:bssfilter", "Filter non-det programs when tests pruning works well", true),
+ LeonFlagOptionDef( "cegis:unsatcores", "--cegis:unsatcores", "Use UNSAT-cores in pruning", true),
+ LeonFlagOptionDef( "cegis:opttimeout", "--cegis:opttimeout", "Consider a time-out of CE-search as untrusted solution", true),
+ LeonFlagOptionDef( "cegis:vanuatoo", "--cegis:vanuatoo", "Generate inputs using new korat-style generator", false)
)
def processOptions(ctx: LeonContext): SynthesisOptions = {
var options = SynthesisOptions()
for(opt <- ctx.options) opt match {
- case LeonFlagOption("manual") =>
- options = options.copy(manualSearch = true)
+ case LeonFlagOption("manual", v) =>
+ options = options.copy(manualSearch = v)
- case LeonFlagOption("inplace") =>
- options = options.copy(inPlace = true)
+ case LeonFlagOption("inplace", v) =>
+ options = options.copy(inPlace = v)
case LeonValueOption("functions", ListValue(fs)) =>
options = options.copy(filterFuns = Some(fs.toSet))
@@ -62,25 +67,34 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
options = options.copy(timeoutMs = Some(t.toLong))
}
- case LeonFlagOption("firstonly") =>
- options = options.copy(firstOnly = true)
-
- case LeonFlagOption("parallel") =>
- options = options.copy(searchWorkers = 5)
+ case LeonFlagOption("firstonly", v) =>
+ options = options.copy(firstOnly = v)
case o @ LeonValueOption("parallel", nWorkers) =>
o.asInt(ctx).foreach { nWorkers =>
options = options.copy(searchWorkers = nWorkers)
}
- case LeonFlagOption("cegis:gencalls") =>
- options = options.copy(cegisGenerateFunCalls = true)
+ case LeonFlagOption("derivtrees", v) =>
+ options = options.copy(generateDerivationTrees = v)
+
+ case LeonFlagOption("cegis:unintprobe", v) =>
+ options = options.copy(cegisUseUninterpretedProbe = v)
+
+ case LeonFlagOption("cegis:unsatcores", v) =>
+ options = options.copy(cegisUseUnsatCores = v)
+
+ case LeonFlagOption("cegis:bssfilter", v) =>
+ options = options.copy(cegisUseBssFiltering = v)
+
+ case LeonFlagOption("cegis:opttimeout", v) =>
+ options = options.copy(cegisUseOptTimeout = v)
- case LeonFlagOption("cegis:vanuatoo") =>
- options = options.copy(cegisUseVanuatoo = true)
+ case LeonFlagOption("cegis:gencalls", v) =>
+ options = options.copy(cegisGenerateFunCalls = v)
- case LeonFlagOption("derivtrees") =>
- options = options.copy(generateDerivationTrees = true)
+ case LeonFlagOption("cegis:vanuatoo", v) =>
+ options = options.copy(cegisUseVanuatoo = v)
case _ =>
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 20116d24b..42032b3e6 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -27,15 +27,12 @@ class Synthesizer(val context : LeonContext,
val problem: Problem,
val options: SynthesisOptions) {
- val silentReporter = new SilentReporter
- val silentContext = context.copy(reporter = silentReporter)
-
val rules: Seq[Rule] = options.rules
- val solver: FairZ3Solver = new FairZ3Solver(silentContext)
+ val solver: FairZ3Solver = new FairZ3Solver(context)
solver.setProgram(program)
- val simpleSolver: Solver = new UninterpretedZ3Solver(silentContext)
+ val simpleSolver: Solver = new UninterpretedZ3Solver(context)
simpleSolver.setProgram(program)
val reporter = context.reporter
@@ -97,11 +94,10 @@ class Synthesizer(val context : LeonContext,
val (npr, fds) = solutionToProgram(sol)
- val tsolver = new TimeoutSolver(new FairZ3Solver(silentContext), timeoutMs)
- tsolver.setProgram(npr)
+ val tsolver = new TimeoutSolver(solver, timeoutMs)
val vcs = generateVerificationConditions(reporter, npr, fds.map(_.id.name))
- val vctx = VerificationContext(context, Seq(tsolver), silentReporter)
+ val vctx = VerificationContext(context, Seq(tsolver), context.reporter)
val vcreport = checkVerificationConditions(vctx, vcs)
if (vcreport.totalValid == vcreport.totalConditions) {
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index bed95ffd8..0905e4173 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -24,10 +24,9 @@ case object CEGIS extends Rule("CEGIS") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
// CEGIS Flags to actiave or de-activate features
- val useCEAsserts = false
- val useUninterpretedProbe = false
- val useUnsatCores = true
- val useOptTimeout = true
+ val useUninterpretedProbe = sctx.options.cegisUseUninterpretedProbe
+ val useUnsatCores = sctx.options.cegisUseUnsatCores
+ val useOptTimeout = sctx.options.cegisUseOptTimeout
val useFunGenerators = sctx.options.cegisGenerateFunCalls
val useBPaths = sctx.options.cegisUseBPaths
val useVanuatoo = sctx.options.cegisUseVanuatoo
@@ -35,7 +34,7 @@ case object CEGIS extends Rule("CEGIS") {
val useCEPruning = sctx.options.cegisUseCEPruning
// Limits the number of programs CEGIS will specifically test for instead of reasonning symbolically
val testUpTo = 5
- val useBssFiltering = true
+ val useBssFiltering = sctx.options.cegisUseBssFiltering
val filterThreshold = 1.0/2
val evaluator = new CodeGenEvaluator(sctx.context, sctx.program)
@@ -718,25 +717,6 @@ case object CEGIS extends Rule("CEGIS") {
if (unsatCore.isEmpty) {
needMoreUnrolling = true
} else {
- //if (useCEAsserts) {
- // val freshCss = ndProgram.css.map(c => c -> Variable(FreshIdentifier(c.name, true).setType(c.getType))).toMap
- // val ceIn = ass.collect {
- // case id if invalidModel contains id => id -> invalidModel(id)
- // }
-
- // val ceMap = (freshCss ++ ceIn)
-
- // val counterexample = substAll(ceMap, And(Seq(ndProgram.program, p.phi)))
-
- // //val And(ands) = counterexample
- // //println("CE:")
- // //for (a <- ands) {
- // // println(" - "+a)
- // //}
-
- // solver1.assertCnstr(counterexample)
- //}
-
solver1.assertCnstr(Not(And(unsatCore.toSeq)))
}
diff --git a/src/main/scala/leon/synthesis/utils/Benchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
index 08226d925..6350e19b2 100644
--- a/src/main/scala/leon/synthesis/utils/Benchmarks.scala
+++ b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
@@ -73,7 +73,8 @@ object Benchmarks extends App {
var nSuccessTotal, nInnapTotal, nDecompTotal, nAltTotal = 0
var tTotal: Long = 0
- val ctx = leon.Main.processOptions(new DefaultReporter, others ++ newOptions)
+ val reporter = new DefaultReporter()
+ val ctx = leon.Main.processOptions(others ++ newOptions)
for (file <- ctx.files) {
val innerCtx = ctx.copy(files = List(file))
@@ -84,10 +85,10 @@ object Benchmarks extends App {
val (program, results) = pipeline.run(innerCtx)(file.getPath :: Nil)
- val solver = new FairZ3Solver(ctx.copy(reporter = new SilentReporter))
+ val solver = new FairZ3Solver(ctx)
solver.setProgram(program)
- val simpleSolver = new UninterpretedZ3Solver(ctx.copy(reporter = new SilentReporter))
+ val simpleSolver = new UninterpretedZ3Solver(ctx)
simpleSolver.setProgram(program)
for ((f, ps) <- results.toSeq.sortBy(_._1.id.toString); p <- ps) {
@@ -98,7 +99,7 @@ object Benchmarks extends App {
program = program,
solver = solver,
simpleSolver = simpleSolver,
- reporter = new DefaultReporter,
+ reporter = reporter,
shouldStop = new java.util.concurrent.atomic.AtomicBoolean
)
diff --git a/src/test/scala/leon/test/TestSilentReporter.scala b/src/test/scala/leon/test/TestSilentReporter.scala
new file mode 100644
index 000000000..c396bded5
--- /dev/null
+++ b/src/test/scala/leon/test/TestSilentReporter.scala
@@ -0,0 +1,6 @@
+package leon
+package test
+
+class TestSilentReporter extends DefaultReporter() {
+ override def output(msg: String) : Unit = {}
+}
diff --git a/src/test/scala/leon/test/TestUtils.scala b/src/test/scala/leon/test/TestUtils.scala
index 2f8b789ae..376d6e402 100644
--- a/src/test/scala/leon/test/TestUtils.scala
+++ b/src/test/scala/leon/test/TestUtils.scala
@@ -21,4 +21,5 @@ object TestUtils {
asFile.listFiles().filter(f => filter(f.getPath()))
}
+
}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index cda418e96..9fd88e13b 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -24,7 +24,7 @@ class EvaluatorsTests extends FunSuite {
verify = false
),
files = List(),
- reporter = new SilentReporter
+ reporter = new TestSilentReporter
)
private val evaluatorConstructors : List[(LeonContext,Program)=>Evaluator] = List(
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index 65b20298c..b188291bb 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -24,7 +24,7 @@ class DataGen extends FunSuite {
verify = false
),
files = List(),
- reporter = new SilentReporter
+ reporter = new TestSilentReporter
)
private def parseString(str : String) : Program = {
diff --git a/src/test/scala/leon/test/purescala/LikelyEq.scala b/src/test/scala/leon/test/purescala/LikelyEq.scala
index 77bac7555..1267b794a 100644
--- a/src/test/scala/leon/test/purescala/LikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEq.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.purescala
+package leon.test
+package purescala
import leon._
import leon.evaluators._
@@ -16,7 +17,7 @@ import leon.purescala.Trees._
* only prove the non equality of two expressions.
*/
object LikelyEq {
- private lazy val evaluator : Evaluator = new DefaultEvaluator(LeonContext(reporter = new SilentReporter), Program.empty)
+ private lazy val evaluator : Evaluator = new DefaultEvaluator(LeonContext(reporter = new TestSilentReporter), Program.empty)
private val min = -5
private val max = 5
diff --git a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
index 9199b38e7..42ac12758 100644
--- a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.purescala
+package leon.test
+package purescala
import leon.purescala.Common._
import leon.purescala.Definitions._
@@ -8,7 +9,6 @@ import leon.purescala.TypeTrees._
import leon.purescala.Trees._
import leon.purescala.TreeOps._
import leon.purescala.TreeNormalizations._
-import leon.SilentReporter
import org.scalatest.FunSuite
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 44c9f6a37..42ccca719 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -1,9 +1,9 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.purescala
+package leon.test
+package purescala
import leon.LeonContext
-import leon.SilentReporter
import leon.purescala.Common._
import leon.purescala.Definitions._
@@ -14,7 +14,7 @@ import leon.purescala.TreeOps._
import org.scalatest.FunSuite
class TreeOpsTests extends FunSuite {
- private val silentContext = LeonContext(reporter = new SilentReporter)
+ private val silentContext = LeonContext(reporter = new TestSilentReporter)
test("Path-aware simplifications") {
import leon.solvers.z3.UninterpretedZ3Solver
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 6cd6480cb..4e479a835 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -1,9 +1,9 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.solvers.z3
+package leon.test
+package solvers.z3
import leon.LeonContext
-import leon.SilentReporter
import leon.purescala.Common._
import leon.purescala.Definitions._
@@ -41,7 +41,7 @@ class FairZ3SolverTests extends FunSuite {
"Solver should not be able to decide the formula " + expr + "."
)
- private val silentContext = LeonContext(reporter = new SilentReporter)
+ private val silentContext = LeonContext(reporter = new TestSilentReporter)
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 9bc961371..53bac4d7c 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -1,9 +1,9 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.solvers.z3
+package leon.test
+package solvers.z3
import leon.LeonContext
-import leon.SilentReporter
import leon.purescala.Common._
import leon.purescala.Definitions._
@@ -45,7 +45,7 @@ class FairZ3SolverTestsNewAPI extends FunSuite {
"Solver should not be able to decide the formula " + expr + "."
)
- private val silentContext = LeonContext(reporter = new SilentReporter)
+ private val silentContext = LeonContext(reporter = new TestSilentReporter)
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index db492d3d3..e9d87d641 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -1,9 +1,9 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.solvers.z3
+package leon.test
+package solvers.z3
import leon.LeonContext
-import leon.SilentReporter
import leon.purescala.Common._
import leon.purescala.Definitions._
@@ -41,7 +41,7 @@ class UninterpretedZ3SolverTests extends FunSuite {
"Solver should not be able to decide the formula " + expr + "."
)
- private val silentContext = LeonContext(reporter = new SilentReporter)
+ private val silentContext = LeonContext(reporter = new TestSilentReporter)
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 123310ac8..610ceb3d6 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.synthesis
+package leon.test
+package synthesis
import leon._
import leon.purescala.Definitions._
@@ -32,7 +33,7 @@ class SynthesisSuite extends FunSuite {
verify = false
),
files = List(),
- reporter = new SilentReporter
+ reporter = new TestSilentReporter
)
val opts = SynthesisOptions()
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 4d73eb949..5dd93cbed 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -45,7 +45,7 @@ class PureScalaVerificationRegression extends FunSuite {
),
options = leonOptions.toList,
files = List(file),
- reporter = new SilentReporter
+ reporter = new TestSilentReporter
)
val pipeline = mkPipeline
@@ -69,8 +69,8 @@ class PureScalaVerificationRegression extends FunSuite {
_.endsWith(".scala"))
for(f <- fs) {
- mkTest(f, List(LeonFlagOption("feelinglucky")), forError)(block)
- mkTest(f, List(LeonFlagOption("codegen"), LeonFlagOption("evalground"), LeonFlagOption("feelinglucky")), forError)(block)
+ mkTest(f, List(LeonFlagOption("feelinglucky", true)), forError)(block)
+ mkTest(f, List(LeonFlagOption("codegen", true), LeonFlagOption("evalground", true), LeonFlagOption("feelinglucky", true)), forError)(block)
}
}
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index bd169c167..d85a5dd6f 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -47,7 +47,7 @@ class XLangVerificationRegression extends FunSuite {
),
//options = List(LeonFlagOption("feelinglucky")),
files = List(file),
- reporter = new SilentReporter
+ reporter = new TestSilentReporter
)
val pipeline = mkPipeline
--
GitLab