diff --git a/src/main/scala/leon/LeonComponent.scala b/src/main/scala/leon/LeonComponent.scala
index 114103d2ad447ee354de0b7947465176ad7adaf3..74a8865a85cb283d544a66c18533e59ab26bb4e6 100644
--- a/src/main/scala/leon/LeonComponent.scala
+++ b/src/main/scala/leon/LeonComponent.scala
@@ -9,5 +9,5 @@ trait LeonComponent {
val name : String
val description : String
- val definedOptions : Set[LeonOptionDef] = Set()
+ val definedOptions : Set[LeonOptionDef[Any]] = Set()
}
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index c7aca5cea0361a43e924227f1c69ce40fd6316d7..0fa623e1a64342a11939000aeed4ed48100d74da 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -12,8 +12,18 @@ import java.io.File
case class LeonContext(
reporter: Reporter,
interruptManager: InterruptManager,
- settings: Settings = Settings(),
- options: Seq[LeonOption] = Seq(),
+ options: Seq[LeonOption[Any]] = Seq(),
files: Seq[File] = Seq(),
timers: TimerStorage = new TimerStorage
-)
+) {
+
+ // @mk: This is not typesafe, because equality for options is implemented as name equality.
+ // It will fail if an LeonOptionDef is passed that has the same name
+ // with one in Main,allOptions, but is different
+ def findOption[A](optDef: LeonOptionDef[A]): Option[A] = options.collectFirst {
+ case LeonOption(`optDef`, value) => value.asInstanceOf[A]
+ }
+
+ def findOptionOrDefault[A](optDef: LeonOptionDef[A]): A =
+ findOption(optDef).getOrElse(optDef.default)
+}
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index f481904558a7eba94e349814e6edd36de69770f9..a62abbfff70efbb37ff9aa4716bda3906694ae55 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -2,76 +2,107 @@
package leon
-/** Describes a command-line option. */
-sealed abstract class LeonOption {
- val name: String
-}
+import OptionParsers._
-/** Boolean (on/off) options. Present means "on". */
-case class LeonFlagOption(name: String, value: Boolean) extends LeonOption {
- override def toString: String = {
- if (value) {
- "--" + name
- } else {
- "--" + name + "=off"
+abstract class LeonOptionDef[+A] {
+ val name: String
+ val description: String
+ val default: A
+ val parser: OptionParser[A]
+ val usageRhs: String
+ def usageDesc = {
+ if (usageRhs.isEmpty) s"--$name"
+ else s"--$name=$usageRhs"
+ }
+ def usageDescs = usageDesc.split("\n").toList
+ def helpString = f"${usageDesc}%-21s ${description}"
+
+ private def parseValue(s: String)(implicit reporter: Reporter): A = {
+ try { parser(s) }
+ catch {
+ case _ : IllegalArgumentException =>
+ reporter.error(s"Invalid option usage: $usageDesc")
+ Main.displayHelp(reporter, error = true)
}
}
-}
-/** Options of the form --option=value. */
-case class LeonValueOption(name: String, value: String) extends LeonOption {
- def splitList : Seq[String] = value.split(':').map(_.trim).filter(!_.isEmpty)
+ def parse(s: String)(implicit reporter: Reporter): LeonOption[A] =
+ LeonOption(this)(parseValue(s))
- def asInt(ctx : LeonContext) : Option[Int] = try {
- Some(value.toInt)
- } catch {
- case _ : Throwable =>
- ctx.reporter.error(s"Option --$name takes an integer as value.")
- None
- }
+ def withDefaultValue: LeonOption[A] =
+ LeonOption(this)(default)
- def asLong(ctx : LeonContext) : Option[Long] = try {
- Some(value.toLong)
- } catch {
- case _ : Throwable =>
- ctx.reporter.error(s"Option --$name takes a long as value.")
- None
+ // @mk: FIXME: Is this cool?
+ override def equals(other: Any) = other match {
+ case that: LeonOptionDef[_] => this.name == that.name
+ case _ => false
}
+ override def hashCode = name.hashCode
+}
- override def toString: String = s"--$name=$value"
+case class LeonFlagOptionDef(name: String, description: String, default: Boolean) extends LeonOptionDef[Boolean] {
+ val parser = booleanParser(default)
+ val usageRhs = ""
}
-sealed abstract class LeonOptionDef {
- val name: String
- val usageOption: String
- val usageDesc: String
- def usageDescs = usageDesc.split("\n").toList
+case class LeonStringOptionDef(name: String, description: String, default: String, usageRhs: String) extends LeonOptionDef[String] {
+ val parser = stringParser
}
-case class LeonFlagOptionDef(name: String,
- usageOption: String,
- usageDesc: String,
- default: Boolean = false) extends LeonOptionDef
-
-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]] = {
- if (value == "off") {
- None
- } else {
- Some(value.split("[:,]").map(_.trim).filter(!_.isEmpty))
- }
+case class LeonLongOptionDef(name: String, description: String, default: Long, usageRhs: String) extends LeonOptionDef[Long] {
+ val parser = longParser
+}
+
+
+class LeonOption[+A] private (val optionDef: LeonOptionDef[A], val value: A) {
+ override def toString = s"--${optionDef.name}=$value"
+ override def equals(other: Any) = other match {
+ case LeonOption(optionDef, value) =>
+ optionDef.name == this.optionDef.name && value == this.value
+ case _ => false
}
+ override def hashCode = optionDef.hashCode
}
+object LeonOption {
+ def apply[A](optionDef: LeonOptionDef[A])(value: A) = {
+ new LeonOption(optionDef, value)
+ }
+ def unapply[A](opt: LeonOption[A]) = Some((opt.optionDef, opt.value))
+}
+
+object OptionParsers {
+ type OptionParser[A] = String => A
+
+ val longParser: OptionParser[Long] = _.toLong
+ val stringParser: OptionParser[String] = x => x
+ def booleanParser(default: Boolean): OptionParser[Boolean] = {
+ case "on" | "true" | "yes" | "" => true
+ case "off" | "false" | "no" => false
+ case _ => throw new IllegalArgumentException
+ }
+ def seqParser[A](base: OptionParser[A]): OptionParser[Seq[A]] = s => {
+ s.split(",").map(base)
+ }
+ def setParser[A](base: OptionParser[A]): OptionParser[Set[A]] = s => {
+ s.split(",").map(base).toSet
+ }
+
+}
+
+
object OptionsHelpers {
+
+ private val matcher = s"--(.*)=(.*)".r
+ private val matcherWithout = s"--(.*)".r
+
+ def nameValue(s: String) = s match {
+ case matcher(name, value) => (name, value)
+ case matcherWithout(name) => (name, "")
+ case _ => sys.error("") // FIXME
+ }
+
// helper for options that include patterns
def matcher(patterns: Traversable[String]): String => Boolean = {
@@ -79,7 +110,7 @@ object OptionsHelpers {
import java.util.regex.Pattern
val p0 = scala.reflect.NameTransformer.encode(s)
- val p = p0.replaceAll("\\$","\\\\\\$").replaceAll("\\.", "\\\\.").replaceAll("_", ".+")
+ val p = p0.replaceAll("\\$","\\\\\\$").replaceAll("\\.", "\\\\.").replaceAll("_", ".+")
Pattern.compile(p)
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index daff9774815c2718a4d8c51256705f3ae69616c9..153a28a763fc0f5c99db021afefb5339134a36ec 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -3,7 +3,6 @@
package leon
import leon.utils._
-import solvers.SolverFactory
object Main {
@@ -28,33 +27,35 @@ object Main {
// Add whatever you need here.
lazy val allComponents : Set[LeonComponent] = allPhases.toSet ++ Set(
- new solvers.z3.FairZ3Component{},
- solvers.smtlib.SMTLIBCVC4Component
+ solvers.z3.FairZ3Component, MainComponent, SharedOptions, solvers.smtlib.SMTLIBCVC4Component
)
- lazy val topLevelOptions : Set[LeonOptionDef] = Set(
- LeonFlagOptionDef ("termination", "--termination", "Check program termination"),
- LeonFlagOptionDef ("repair", "--repair", "Repair selected functions"),
- LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
- LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
- LeonFlagOptionDef ("watch", "--watch", "Rerun pipeline when file changes"),
- LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 \nAvailable:"+
- SolverFactory.definedSolvers.toSeq.sortBy(_._1).map {
- case (name, desc) => f"\n $name%-14s : $desc"
- }.mkString("")),
- LeonValueOptionDef("debug", "--debug=<sections..>", "Enables specific messages"),
- LeonFlagOptionDef ("noop", "--noop", "No operation performed, just output program"),
- LeonFlagOptionDef ("help", "--help", "Show help")
- )
+ object MainComponent extends LeonComponent {
+ val name = "main"
+ val description = "The main Leon component, handling the top-level options"
+
+ val Termination = LeonFlagOptionDef("termination", "Check program termination", false)
+ val Repair = LeonFlagOptionDef("repair", "Repair selected functions", false)
+ val Synthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
+ val XLang = LeonFlagOptionDef("xlang", "Support for extra program constructs (imperative,...)", false)
+ val Watch = LeonFlagOptionDef("watch", "Rerun pipeline when file changes", false)
+ val Noop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
+ val Verify = LeonFlagOptionDef("verify", "Verify function contracts", true )
+ val Help = LeonFlagOptionDef("help", "Show help message", false)
+
+ override val definedOptions: Set[LeonOptionDef[Any]] =
+ Set(Termination, Repair, Synthesis, XLang, Watch, Noop, Help, Verify)
+
+ }
- lazy val allOptions = allComponents.flatMap(_.definedOptions) ++ topLevelOptions
+ lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
- def displayHelp(reporter: Reporter, error: Boolean) {
- reporter.info("usage: leon [--xlang] [--termination] [--synthesis] [--help] [--debug=<N>] [..] <files>")
+ def displayHelp(reporter: Reporter, error: Boolean) = {
reporter.info("")
- for (opt <- topLevelOptions.toSeq.sortBy(_.name)) {
+
+ for (opt <- (MainComponent.definedOptions ++ SharedOptions.definedOptions).toSeq.sortBy(_.name)) {
val (uhead :: utail) = opt.usageDescs
- reporter.info(f"${opt.usageOption}%-20s ${uhead}")
+ reporter.info(f"${opt.usageDesc}%-20s ${uhead}")
for(u <- utail) {
reporter.info(f"${""}%-20s ${u}")
}
@@ -63,12 +64,12 @@ object Main {
reporter.info("")
reporter.info("Additional options, by component:")
- for (c <- allComponents.toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
+ for (c <- (allComponents - MainComponent - SharedOptions).toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
reporter.info("")
reporter.info(s"${c.name} (${c.description})")
for(opt <- c.definedOptions.toSeq.sortBy(_.name)) {
// there is a non-breaking space at the beginning of the string :)
- reporter.info(f"${opt.usageOption}%-20s ${opt.usageDesc}")
+ reporter.info(opt.helpString)
}
}
exit(error)
@@ -78,141 +79,45 @@ object Main {
def processOptions(args: Seq[String]): LeonContext = {
- val initReporter = new DefaultReporter(Settings())
-
- val allOptions = this.allOptions
+ val initReporter = new DefaultReporter(Set())
- val allOptionsMap = allOptions.map(o => o.name -> o).toMap
+ val allOptions: Set[LeonOptionDef[Any]] = this.allOptions
- // Detect unknown options:
- val options = args.filter(_.startsWith("--"))
+ val options = args.filter(_.startsWith("--")).toSet
val files = args.filterNot(_.startsWith("-")).map(new java.io.File(_))
- 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) =>
- (name, Some(value))
- case List(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 _ =>
- None
- }
-
- if (allOptionsMap contains name) {
- optV.foreach { v =>
- optionsValues += allOptionsMap(name) -> v
- }
- } else {
- initReporter.fatalError("'"+name+"' is not a valid option. See 'leon --help'")
+ val leonOptions: Set[LeonOption[Any]] = options.map { opt =>
+ val (name, value) = OptionsHelpers.nameValue(opt)
+ // Find respective LeonOptionDef, or report an unknown option
+ val df = allOptions.find(_. name == name).getOrElse{
+ initReporter.error(s"Unknown option: $name")
+ displayHelp(initReporter, error = true)
}
+ df.parse(value)(initReporter)
}
- 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, error=true)
- 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", value) =>
- settings = settings.copy(termination = value)
- case LeonFlagOption("repair", value) =>
- settings = settings.copy(repair = value)
- case LeonFlagOption("synthesis", value) =>
- settings = settings.copy(synthesis = value)
- case LeonFlagOption("xlang", value) =>
- settings = settings.copy(xlang = value)
- case LeonValueOption("solvers", ListValue(ss)) =>
- val available = SolverFactory.definedSolvers.keySet
- val unknown = ss.toSet -- available
- if (unknown.nonEmpty) {
- initReporter.error("Unknown solver(s): "+unknown.mkString(", ")+" (Available: "+available.mkString(", ")+")")
- }
- settings = settings.copy(selectedSolvers = ss.toSet)
-
- case LeonValueOption("debug", ListValue(sections)) =>
- val debugSections = sections.flatMap { s =>
- if (s == "all") {
- DebugSections.all
- } else {
- DebugSections.all.find(_.name == s) match {
- case Some(rs) =>
- Some(rs)
- case None =>
- initReporter.error("Section "+s+" not found, available: "+DebugSections.all.map(_.name).mkString(", "))
- None
- }
- }
- }
- settings = settings.copy(debugSections = debugSections.toSet)
- case LeonFlagOption("noop", true) =>
- settings = settings.copy(verify = false)
- case LeonFlagOption("help", true) =>
- displayHelp(initReporter, error = false)
- case _ =>
- }
-
- // Create a new reporter taking settings into account
- val reporter = new DefaultReporter(settings)
+ val reporter = new DefaultReporter(
+ leonOptions.collectFirst {
+ case LeonOption(SharedOptions.Debug, sections) => sections.asInstanceOf[Set[DebugSection]]
+ }.getOrElse(Set[DebugSection]())
+ )
reporter.whenDebug(DebugSectionOptions) { debug =>
-
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)
-
- }
+ for (lo <- leonOptions) debug(lo.toString)
}
- val intManager = new InterruptManager(reporter)
-
- LeonContext(settings = settings,
- reporter = reporter,
- files = files,
- options = leonOptions,
- interruptManager = intManager)
+ LeonContext(
+ reporter = reporter,
+ files = files,
+ options = leonOptions.toSeq,
+ interruptManager = new InterruptManager(reporter)
+ )
}
- def computePipeline(settings: Settings): Pipeline[List[String], Any] = {
+ def computePipeline(ctx: LeonContext): Pipeline[List[String], Any] = {
+
import purescala.Definitions.Program
import purescala.{FunctionClosure, RestoreMethods}
import utils.FileOutputPhase
@@ -222,36 +127,41 @@ object Main {
import xlang.XLangAnalysisPhase
import verification.AnalysisPhase
import repair.RepairPhase
-
- val pipeSanityCheck : Pipeline[Program, Program] =
- if(!settings.xlang)
- xlang.NoXLangFeaturesChecking
- else
- NoopPhase()
-
- val pipeBegin : Pipeline[List[String],Program] =
- ExtractionPhase andThen
- PreprocessingPhase andThen
- pipeSanityCheck
-
- val pipeProcess: Pipeline[Program, Any] = {
- if (settings.synthesis) {
- SynthesisPhase
- } else if (settings.repair) {
- RepairPhase
- } else if (settings.termination) {
- TerminationPhase
- } else if (settings.xlang) {
- XLangAnalysisPhase
- } else if (settings.verify) {
- FunctionClosure andThen AnalysisPhase
- } else {
- RestoreMethods andThen FileOutputPhase
+ import MainComponent._
+
+ val helpF = ctx.findOptionOrDefault(Help)
+ val noopF = ctx.findOptionOrDefault(Noop)
+ val synthesisF = ctx.findOptionOrDefault(Synthesis)
+ val xlangF = ctx.findOptionOrDefault(XLang)
+ val repairF = ctx.findOptionOrDefault(Repair)
+ val terminationF = ctx.findOptionOrDefault(Termination)
+ val verifyF = ctx.findOptionOrDefault(Verify)
+
+ if (helpF) {
+ displayHelp(ctx.reporter, error = false)
+ } else {
+ val pipeBegin: Pipeline[List[String], Program] =
+ if (xlangF)
+ ExtractionPhase andThen
+ PreprocessingPhase andThen
+ xlang.NoXLangFeaturesChecking
+ else
+ ExtractionPhase andThen
+ PreprocessingPhase
+
+ val pipeProcess: Pipeline[Program, Any] = {
+ if (noopF) RestoreMethods andThen FileOutputPhase
+ else if (synthesisF) SynthesisPhase
+ else if (repairF) RepairPhase
+ else if (terminationF) TerminationPhase
+ else if (xlangF) XLangAnalysisPhase
+ else if (verifyF) FunctionClosure andThen AnalysisPhase
+ else NoopPhase()
}
- }
- pipeBegin andThen
- pipeProcess
+ pipeBegin andThen
+ pipeProcess
+ }
}
private var hasFatal = false
@@ -271,7 +181,7 @@ object Main {
// For the special case of fatal errors not sent though Reporter, we
// send them through reporter one time
try {
- new DefaultReporter(Settings()).fatalError(msg)
+ new DefaultReporter(Set()).fatalError(msg)
} catch {
case _: LeonFatalError =>
}
@@ -281,10 +191,7 @@ object Main {
ctx.interruptManager.registerSignalHandler()
- val doWatch = ctx.options.exists {
- case LeonFlagOption("watch", value) => value
- case _ => false
- }
+ val doWatch = ctx.findOptionOrDefault(MainComponent.Watch)
if (doWatch) {
val watcher = new FilesWatcher(ctx, ctx.files)
@@ -299,11 +206,11 @@ object Main {
}
def execute(args: Seq[String], ctx0: LeonContext): Unit = {
- val ctx = ctx0.copy(reporter = new DefaultReporter(ctx0.settings))
+ val ctx = ctx0.copy(reporter = new DefaultReporter(ctx0.reporter.debugSections))
try {
// Compute leon pipeline
- val pipeline = computePipeline(ctx.settings)
+ val pipeline = computePipeline(ctx)
val timer = ctx.timers.total.start()
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 9e9d44f3375d6b813915233e6dc599c601d6aec0..0838771245f5d279f51b7b5e658225ac88d8da17 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -8,7 +8,7 @@ abstract class Pipeline[-F, +T] {
def andThen[G](thenn: Pipeline[T, G]): Pipeline[F, G] = new Pipeline[F,G] {
def run(ctx : LeonContext)(v : F) : G = {
val s = self.run(ctx)(v)
- if(ctx.settings.terminateAfterEachPhase) ctx.reporter.terminateIfError()
+ if(ctx.findOptionOrDefault(SharedOptions.StrictPhases)) ctx.reporter.terminateIfError()
thenn.run(ctx)(s)
}
}
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 2827c04699a8a3f64d764a868c09e204e2b1ac39..f9df384188225d08bf2569c724a15e035549407a 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -4,7 +4,7 @@ package leon
import utils._
-abstract class Reporter(settings: Settings) {
+abstract class Reporter(val debugSections: Set[DebugSection]) {
abstract class Severity
case object INFO extends Severity
@@ -67,7 +67,7 @@ abstract class Reporter(settings: Settings) {
}
// Debugging
- private val debugMask = settings.debugSections.foldLeft(0){ _ | _.mask }
+ private val debugMask = debugSections.foldLeft(0){ _ | _.mask }
def ifDebug(body: (Any => Unit) => Any)(implicit section: DebugSection) = {
if ((debugMask & section.mask) == section.mask) {
@@ -99,7 +99,7 @@ abstract class Reporter(settings: Settings) {
final def debug(msg: => Any)(implicit section: DebugSection): Unit = debug(NoPosition, msg)
}
-class DefaultReporter(settings: Settings) extends Reporter(settings) {
+class DefaultReporter(debugSections: Set[DebugSection]) extends Reporter(debugSections) {
protected def severityToPrefix(sev: Severity): String = sev match {
case ERROR => "["+Console.RED +" Error "+Console.RESET+"]"
case WARNING => "["+Console.YELLOW +"Warning "+Console.RESET+"]"
@@ -176,7 +176,7 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
}
-class PlainTextReporter(settings: Settings) extends DefaultReporter(settings) {
+class PlainTextReporter(debugSections: Set[DebugSection]) extends DefaultReporter(debugSections) {
override protected def severityToPrefix(sev: Severity): String = sev match {
case ERROR => "[ Error ]"
case WARNING => "[Warning ]"
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
deleted file mode 100644
index e6975481b8af1a4727c806b549e453d44427d59d..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/Settings.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-
-import utils.DebugSection
-
-case class Settings(
- strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
- terminateAfterEachPhase: Boolean = true, // Terminates Leon after each phase if an error occured
- debugSections: Set[DebugSection] = Set(), // Enables debug message for the following sections
- termination: Boolean = false,
- repair: Boolean = false,
- synthesis: Boolean = false,
- xlang: Boolean = false,
- verify: Boolean = true,
- selectedSolvers: Set[String] = Set("fairz3")
-)
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..41dfe68dfe6b2a9d9834d474547a63a3a1ced7f6
--- /dev/null
+++ b/src/main/scala/leon/SharedOptions.scala
@@ -0,0 +1,57 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import leon.utils.{DebugSections, DebugSection}
+import OptionParsers._
+
+object SharedOptions extends LeonComponent {
+
+ val name = "sharedOptions"
+ val description = "Options shared by multiple components of Leon"
+
+ val StrictPhases = LeonFlagOptionDef("strict", "Terminate after each phase if there is an error", true)
+
+ case object FunctionsOptionDef extends LeonOptionDef[Seq[String]] {
+ val name = "functions"
+ val description = "Only consider functions f1, f2, ..."
+ val default = Seq[String]()
+ val parser = seqParser(stringParser)
+ val usageRhs = "f1,f2,..."
+ }
+
+ case object SelectedSolvers extends LeonOptionDef[Set[String]] {
+ val name = "solvers"
+ val description = "Use solvers s1, s2, ... in parallel (default: fairz3)"
+ val default = Set("fairz3")
+ val parser = setParser(stringParser)
+ val usageRhs = "s1,s2,..."
+ }
+
+ case object Debug extends LeonOptionDef[Set[DebugSection]] {
+ import OptionParsers._
+ val name = "debug"
+ val description = "Enable detailed messages per component"
+ val default = Set[DebugSection]()
+ val usageRhs = "d1,d2,..."
+ val debugParser: OptionParser[Set[DebugSection]] = s => {
+ if (s == "all") {
+ DebugSections.all
+ } else {
+ DebugSections.all.find(_.name == s) match {
+ case Some(rs) =>
+ Set(rs)
+ case None =>
+ throw new IllegalArgumentException
+ //initReporter.error("Section "+s+" not found, available: "+DebugSections.all.map(_.name).mkString(", "))
+ //Set()
+ }
+ }
+ }
+ val parser: String => Set[DebugSection] = setParser[Set[DebugSection]](debugParser)(_).flatten
+ }
+
+ val Timeout = LeonLongOptionDef("timeout", "Set a timeout for each verification/repair (in sec.)", 0L, "t")
+
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(StrictPhases, FunctionsOptionDef, SelectedSolvers, Debug, Timeout)
+}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index fd148e997af49663a7b728029e44578fe9d4e0d6..4d2ab0eeb86f177da3037e5da2eac0ef9c42ea68 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -87,7 +87,7 @@ trait CodeExtraction extends ASTExtractors {
/** An exception thrown when non-purescala compatible code is encountered. */
sealed class ImpureCodeEncounteredException(pos: Position, msg: String, ot: Option[Tree]) extends Exception(msg) {
def emit() {
- val debugInfo = if (ctx.settings.debugSections contains utils.DebugSectionTrees) {
+ val debugInfo = if (ctx.findOptionOrDefault(SharedOptions.Debug) contains utils.DebugSectionTrees) {
ot.map { t =>
val strWr = new java.io.StringWriter()
new global.TreePrinter(new java.io.PrintWriter(strWr)).printTree(t)
@@ -97,7 +97,7 @@ trait CodeExtraction extends ASTExtractors {
""
}
- if (ctx.settings.strictCompilation) {
+ if (ctx.findOptionOrDefault(ExtractionPhase.StrictCompilation)) {
reporter.error(pos, msg + debugInfo)
} else {
reporter.warning(pos, msg + debugInfo)
@@ -919,7 +919,7 @@ trait CodeExtraction extends ASTExtractors {
if (!dctx.isExtern) {
e.emit()
//val pos = if (body0.pos == NoPosition) NoPosition else leonPosToScalaPos(body0.pos.source, funDef.getPos)
- if (ctx.settings.strictCompilation) {
+ if (ctx.findOptionOrDefault(ExtractionPhase.StrictCompilation)) {
reporter.error(funDef.getPos, "Function "+funDef.id.name+" could not be extracted. (Forgot @extern ?)")
} else {
reporter.warning(funDef.getPos, "Function "+funDef.id.name+" is not fully unavailable to Leon.")
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index a08f55c6c272fabecad5969db11850b85c7f3138..c0ba4641e7657b75150e350331e8bf24c7a1023c 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -8,7 +8,7 @@ import purescala.Common.FreshIdentifier
import utils._
-import scala.tools.nsc.{Settings=>NSCSettings,CompilerCommand}
+import scala.tools.nsc.{Settings,CompilerCommand}
import java.io.File
object ExtractionPhase extends LeonPhase[List[String], Program] {
@@ -16,12 +16,16 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
val name = "Scalac Extraction"
val description = "Extraction of trees from the Scala Compiler"
+ val StrictCompilation = LeonFlagOptionDef("strictCompilation", "Exit Leon after an error in compilation", true)
+
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(StrictCompilation)
+
implicit val debug = DebugSectionTrees
def run(ctx: LeonContext)(args: List[String]): Program = {
val timer = ctx.timers.frontend.start()
- val settings = new NSCSettings
+ val settings = new Settings
val scalaLib = Option(scala.Predef.getClass.getProtectionDomain.getCodeSource).map{
_.getLocation.getPath
diff --git a/src/main/scala/leon/purescala/PrinterOptions.scala b/src/main/scala/leon/purescala/PrinterOptions.scala
index 86c48653e189c70bcc0771437853869ca538d2cc..3c1d67d745b6d48e4879c4b99d6f96d97d5c11bb 100644
--- a/src/main/scala/leon/purescala/PrinterOptions.scala
+++ b/src/main/scala/leon/purescala/PrinterOptions.scala
@@ -14,8 +14,8 @@ case class PrinterOptions (
object PrinterOptions {
def fromContext(ctx: LeonContext): PrinterOptions = {
- val debugTrees = ctx.settings.debugSections contains DebugSectionTrees
- val debugPositions = ctx.settings.debugSections contains DebugSectionPositions
+ val debugTrees = ctx.findOptionOrDefault(SharedOptions.Debug) contains DebugSectionTrees
+ val debugPositions = ctx.findOptionOrDefault(SharedOptions.Debug) contains DebugSectionPositions
PrinterOptions(
baseIndent = 0,
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index 996c5b5cb8c56b7cdb422d022423d8ba1fb1da90..913e722c9ff067c10f87c51f7bb3b35a76f9ac3c 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -12,25 +12,12 @@ object RepairPhase extends LeonPhase[Program, Program] {
implicit val debugSection = utils.DebugSectionRepair
- override val definedOptions : Set[LeonOptionDef] = Set(
- LeonValueOptionDef("functions", "--functions=f1:f2", "Repair functions f1,f2,...")
- )
-
def run(ctx: LeonContext)(program: Program): Program = {
- var repairFuns: Option[Seq[String]] = None
- var verifTimeoutMs: Option[Long] = None
+ var repairFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.FunctionsOptionDef)
+ var verifTimeoutMs: Option[Long] = ctx.findOption(SharedOptions.Timeout) map { _ * 1000 }
val reporter = ctx.reporter
- for(opt <- ctx.options) opt match {
- case v @ LeonValueOption("timeout", _) =>
- verifTimeoutMs = v.asLong(ctx) map { _ * 1000L }
- case LeonValueOption("functions", ListValue(fs)) =>
- repairFuns = Some(fs)
- case _ =>
- }
-
-
val fdFilter = {
import OptionsHelpers._
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 0163d4ceeec92ff50acaec0c6e3f8930b5b2c349..bb7c2ef9acd8e366e95a5fcaa6bba0e0954aa14d 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -372,7 +372,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val timeoutMs = verifTimeoutMs.getOrElse(3000L)
val solver = SolverFactory.getFromSettings(ctx, prog).withTimeout(timeoutMs)
val vctx = VerificationContext(ctx, prog, solver, reporter)
- val vcs = AnalysisPhase.generateVCs(vctx, Some(List(fd.id.name)))
+ val vcs = AnalysisPhase.generateVCs(vctx, Some(Seq(fd.id.name)))
val report = AnalysisPhase.checkVCs(
vctx,
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index b326199b2bd85029dfa27f2b4e19c42582962fcc..c897fc259fcace479f005957934323eceb60f0f7 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -31,7 +31,7 @@ object SolverFactory {
)
def getFromSettings(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
- getFromName(ctx, program)(ctx.settings.selectedSolvers.toSeq : _*)
+ getFromName(ctx, program)(ctx.findOptionOrDefault(SharedOptions.SelectedSolvers).toSeq : _*)
}
def getFromName(ctx: LeonContext, program: Program)(names: String*): SolverFactory[TimeoutSolver] = {
@@ -66,15 +66,20 @@ object SolverFactory {
SolverFactory(() => new SMTLIBSolver(ctx, program) with SMTLIBCVC4CounterExampleTarget with TimeoutSolver)
case _ =>
- ctx.reporter.fatalError("Unknown solver "+name)
+ ctx.reporter.error(s"Unknown solver $name")
+ showSolvers()
}
- val solvers = names.toSeq.toSet
+ def showSolvers() = {
+ ctx.reporter.error("Available:\n" + definedSolvers.map {" - " + _}.mkString("\n"))
+ ctx.reporter.fatalError("Aborting Leon...")
+ }
- val selectedSolvers = solvers.map(getSolver)
+ val selectedSolvers = names.map(getSolver)
if (selectedSolvers.isEmpty) {
- ctx.reporter.fatalError("No solver selected. Aborting")
+ ctx.reporter.error(s"No solver selected.")
+ showSolvers()
} else if (selectedSolvers.size == 1) {
selectedSolvers.head
} else {
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 0d1232b712a7493ff36869e4cee329c91f2c873f..3aea7b2a8fb063d5ab9181f4b4f095e4ca2b9da6 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -10,24 +10,15 @@ import purescala.Constructors._
import purescala.Expressions._
import purescala.ExprOps._
-import solvers.templates._
+import z3.FairZ3Component.{FeelingLucky, UseCodeGen}
+import templates._
import utils.Interruptible
import evaluators._
class UnrollingSolver(val context: LeonContext, program: Program, underlying: IncrementalSolver with Interruptible) extends Solver with Interruptible {
- val (feelingLucky, useCodeGen) = locally {
- var lucky = false
- var codegen = false
-
- for(opt <- context.options) opt match {
- case LeonFlagOption("feelinglucky", v) => lucky = v
- case LeonFlagOption("codegen", v) => codegen = v
- case _ =>
- }
-
- (lucky, codegen)
- }
+ val feelingLucky = context.findOptionOrDefault(FeelingLucky)
+ val useCodeGen = context.findOptionOrDefault(UseCodeGen)
private val evaluator : Evaluator = {
if(useCodeGen) {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index e1c8c1d2662d098cd1bedc1a017267b5edc92aaa..f97c59b525fae130ab1e4254af33bbc0c95f3e61 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -4,6 +4,7 @@ package leon
package solvers
package smtlib
+import leon.OptionParsers._
import purescala._
import Common._
import Expressions.{Assert => _, _}
@@ -22,9 +23,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
def targetName = "cvc4"
def userDefinedOps(ctx: LeonContext) = {
- ctx.options.collect {
- case LeonValueOption("solver:cvc4", value) => value
- }
+ ctx.findOptionOrDefault(SMTLIBCVC4Component.CVC4Options)
}
def interpreterOps(ctx: LeonContext) = {
@@ -36,7 +35,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
"--dt-rewrite-error-sel",
"--print-success",
"--lang", "smt"
- ) ++ userDefinedOps(ctx)
+ ) ++ userDefinedOps(ctx).toSeq
}
def getNewInterpreter(ctx: LeonContext) = {
@@ -188,7 +187,13 @@ object SMTLIBCVC4Component extends LeonComponent {
val description = "Solver invoked when --solvers=smt-cvc4"
- override val definedOptions : Set[LeonOptionDef] = Set(
- LeonValueOptionDef("solver:cvc4", "--solver:cvc4=<cvc4-opt>", "Pass extra arguments to CVC4")
- )
+ case object CVC4Options extends LeonOptionDef[Set[String]] {
+ val name = "solver:cvc4"
+ val description = "Pass extra arguments to CVC4"
+ val default = Set("")
+ val parser = setParser(stringParser)
+ val usageRhs = "<cvc4-opt>"
+ }
+
+ override val definedOptions : Set[LeonOptionDef[Any]] = Set(CVC4Options)
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Component.scala b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
index 8246903cc83e5d72a4b29b647dc50fb7a8a09cf2..5fc6018e7afeec93123e6794a09c90901a6dacb7 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Component.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
@@ -7,11 +7,14 @@ 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")
- )
+ val EvalGround = LeonFlagOptionDef("evalground", "Use evaluator on functions applied to ground arguments", false)
+ val CheckModels = LeonFlagOptionDef("checkmodels", "Double-check counter-examples with evaluator", false)
+ val FeelingLucky = LeonFlagOptionDef("feelinglucky","Use evaluator to find counter-examples early", false)
+ val UseCodeGen = LeonFlagOptionDef("codegen", "Use compiled evaluator instead of interpreter", false)
+ val UnrollCores = LeonFlagOptionDef("unrollcores", "Use unsat-cores to drive unrolling while remaining fair", false)
+
+ override val definedOptions: Set[LeonOptionDef[Any]] =
+ Set(EvalGround, CheckModels, FeelingLucky, UseCodeGen, UnrollCores)
}
+
+object FairZ3Component extends FairZ3Component
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index d29cdcd7858ba46f817e7b55811ed95f1b05149c..99c749ef88ea8108fd2dae24fc458fdba4f2923c 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -25,26 +25,14 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
enclosing =>
- val (feelingLucky, checkModels, useCodeGen, evalGroundApps, unrollUnsatCores) = locally {
- var lucky = false
- var check = false
- var codegen = false
- var evalground = false
- var unrollUnsatCores = false
-
- for(opt <- context.options) opt match {
- 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 _ =>
- }
-
- (lucky, check, codegen, evalground, unrollUnsatCores)
- }
-
- private val evaluator : Evaluator = if(useCodeGen) {
+ val feelingLucky = context.findOptionOrDefault(FeelingLucky)
+ val checkModels = context.findOptionOrDefault(CheckModels)
+ val useCodeGen = context.findOptionOrDefault(UseCodeGen)
+ val evalGroundApps = context.findOptionOrDefault(EvalGround)
+ val unrollUnsatCores = context.findOptionOrDefault(UnrollCores)
+
+ private val evaluator: Evaluator =
+ if(useCodeGen) {
// TODO If somehow we could not recompile each time we create a solver,
// that would be good?
new CodeGenEvaluator(context, program)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 4208740007ed7d4138e60f0caab2a5b70303198b..5a8063d5b43aedf7e36f3e614bdcdf852a726eea 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -48,7 +48,6 @@ object Rules {
DetupleOutput,
DetupleInput,
ADTSplit,
- InlineHoles,
//IntegerEquation,
//IntegerInequalities,
IntInduction,
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 4f71836d24603311f4a47c382e4088f065b5a83c..d0419f81ad5d6a4d9549b8f2ab58d32e2ac711fe 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -8,7 +8,6 @@ import solvers.combinators.PortfolioSolverSynth
import solvers.z3._
import purescala.Definitions.{Program, FunDef}
-
/**
* This is global information per entire search, contains necessary information
*/
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 9fe9d7b48e120f8fdf18932a4472b42736680d1f..7a16afed9ad1ac260e8b1c402dc33603cc6f4934 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-
package leon
package synthesis
@@ -14,99 +13,52 @@ import graph._
object SynthesisPhase extends LeonPhase[Program, Program] {
val name = "Synthesis"
- val description = "Synthesis"
-
- override val definedOptions : Set[LeonOptionDef] = Set(
- LeonFlagOptionDef( "inplace", "--inplace", "Debug level"),
- LeonFlagOptionDef( "allseeing", "--allseeing", "Also synthesize functions using holes"),
- LeonValueOptionDef("parallel", "--parallel[=N]", "Parallel synthesis search using N workers", Some("5")),
- LeonValueOptionDef( "manual", "--manual[=cmd]", "Manual search", Some("")),
- 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:shrink", "--cegis:shrink", "Shrink non-det programs when tests pruning works well", 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),
- LeonFlagOptionDef( "holes:discrete", "--holes:discrete", "Oracles get split", false)
- )
-
- def processOptions(ctx: LeonContext): SynthesisSettings = {
- var options = SynthesisSettings()
-
- for(opt <- ctx.options) opt match {
- case LeonValueOption("manual", cmd) =>
- options = options.copy(manualSearch = Some(cmd))
-
- case LeonFlagOption("allseeing", v) =>
- options = options.copy(allSeeing = v)
-
- case LeonFlagOption("inplace", v) =>
- options = options.copy(inPlace = v)
+ val description = "Partial synthesis of \"choose\" constructs"
- case LeonValueOption("functions", ListValue(fs)) =>
- options = options.copy(filterFuns = Some(fs.toSet))
+ val Manual = LeonStringOptionDef("manual", "Manual search", default = "", "cmd")
+ val CostModel = LeonStringOptionDef("costmodel", "Use a specific cost model for this search", "FIXME", "cm")
+ val DerivTrees = LeonFlagOptionDef( "derivtrees", "Generate derivation trees", false)
- case LeonValueOption("costmodel", cm) =>
- CostModels.all.find(_.name.toLowerCase == cm.toLowerCase) match {
- case Some(model) =>
- options = options.copy(costModel = model)
- case None =>
+ // CEGIS options
+ val CEGISShrink = LeonFlagOptionDef( "cegis:shrink", "Shrink non-det programs when tests pruning works well", true)
+ val CEGISOptTimeout = LeonFlagOptionDef( "cegis:opttimeout", "Consider a time-out of CE-search as untrusted solution", true)
+ val CEGISVanuatoo = LeonFlagOptionDef( "cegis:vanuatoo", "Generate inputs using new korat-style generator", false)
- var errorMsg = "Unknown cost model: " + cm + "\n" +
- "Defined cost models: \n"
+ override val definedOptions : Set[LeonOptionDef[Any]] =
+ Set(Manual, CostModel, DerivTrees, CEGISShrink, CEGISOptTimeout, CEGISVanuatoo)
- for (cm <- CostModels.all.toSeq.sortBy(_.name)) {
- errorMsg += " - " + cm.name + (if(cm == CostModels.default) " (default)" else "") + "\n"
- }
-
- ctx.reporter.fatalError(errorMsg)
- }
-
- case v @ LeonValueOption("timeout", _) =>
- v.asInt(ctx).foreach { t =>
- options = options.copy(timeoutMs = Some(t.toLong))
- }
-
- case LeonFlagOption("firstonly", v) =>
- options = options.copy(firstOnly = v)
+ def processOptions(ctx: LeonContext): SynthesisSettings = {
+ val ms = ctx.findOption(Manual)
+ SynthesisSettings(
+ manualSearch = ms,
+ functions = ctx.findOption(SharedOptions.FunctionsOptionDef) map { _.toSet },
+ timeoutMs = ctx.findOption(SharedOptions.Timeout) map { _ * 1000 },
+ generateDerivationTrees = ctx.findOptionOrDefault(DerivTrees),
+ cegisUseOptTimeout = ctx.findOption(CEGISOptTimeout),
+ cegisUseShrink = ctx.findOption(CEGISShrink),
+ cegisUseVanuatoo = ctx.findOption(CEGISVanuatoo),
+ rules = Rules.all ++ (ms map { _ => rules.AsChoose}),
+ costModel = {
+ ctx.findOption(CostModel) match {
+ case None => CostModels.default
+ case Some(name) => CostModels.all.find(_.name.toLowerCase == name.toLowerCase) match {
+ case Some(model) => model
+ case None =>
+ var errorMsg = "Unknown cost model: " + name + "\n" +
+ "Defined cost models: \n"
+
+ for (cm <- CostModels.all.toSeq.sortBy(_.name)) {
+ errorMsg += " - " + cm.name + (if (cm == CostModels.default) " (default)" else "") + "\n"
+ }
+
+ ctx.reporter.fatalError(errorMsg)
+ }
- case o @ LeonValueOption("parallel", nWorkers) =>
- o.asInt(ctx).foreach { nWorkers =>
- options = options.copy(searchWorkers = nWorkers)
}
-
- case LeonFlagOption("derivtrees", v) =>
- options = options.copy(generateDerivationTrees = v)
-
- case LeonFlagOption("cegis:bssfilter", v) =>
- options = options.copy(cegisUseShrink = Some(v))
-
- case LeonFlagOption("cegis:opttimeout", v) =>
- options = options.copy(cegisUseOptTimeout = Some(v))
-
- case LeonFlagOption("cegis:vanuatoo", v) =>
- options = options.copy(cegisUseVanuatoo = Some(v))
-
-// case LeonFlagOption("holes:discrete", v) =>
-// options = options.copy(distreteHoles = v)
-
- case _ =>
- }
-
- if (options.manualSearch.isDefined) {
- options = options.copy(
- rules = rules.AsChoose +:
- options.rules
- )
- }
-
- options
+ }
+ )
}
-
def run(ctx: LeonContext)(p: Program): Program = {
val options = processOptions(ctx)
@@ -116,7 +68,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
import OptionsHelpers._
val ciTofd = { (ci: ChooseInfo) => ci.fd }
- filterInclusive(options.filterFuns.map(fdMatcher), Some(excludeByDefault _)) compose ciTofd
+ filterInclusive(options.functions.map(fdMatcher), Some(excludeByDefault _)) compose ciTofd
}
val chooses = ChooseInfo.extractFromProgram(p).filter(fdFilter)
diff --git a/src/main/scala/leon/synthesis/SynthesisSettings.scala b/src/main/scala/leon/synthesis/SynthesisSettings.scala
index 9b772870ad5363881f4073fb1073d83feb79d78c..caacfea8ecc5a31ddd24b5c87ac73a10a5413ccc 100644
--- a/src/main/scala/leon/synthesis/SynthesisSettings.scala
+++ b/src/main/scala/leon/synthesis/SynthesisSettings.scala
@@ -7,25 +7,19 @@ import scala.language.existentials
import leon.purescala.Definitions.FunDef
case class SynthesisSettings(
- inPlace: Boolean = false,
- allSeeing: Boolean = false,
- generateDerivationTrees: Boolean = false,
- filterFuns: Option[Set[String]] = None,
- searchWorkers: Int = 1,
- firstOnly: Boolean = false,
timeoutMs: Option[Long] = None,
+ generateDerivationTrees: Boolean = false,
costModel: CostModel = CostModels.default,
rules: Seq[Rule] = Rules.all,
manualSearch: Option[String] = None,
searchBound: Option[Int] = None,
selectedSolvers: Set[String] = Set("fairz3"),
+ functions: Option[Set[String]] = None,
functionsToIgnore: Set[FunDef] = Set(),
// Cegis related options
cegisUseOptTimeout: Option[Boolean] = None,
cegisUseShrink: Option[Boolean] = None,
- cegisUseVanuatoo: Option[Boolean] = None,
+ cegisUseVanuatoo: Option[Boolean] = None
- // Oracles and holes
- distreteHoles: Boolean = false
)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index acce32ff10747b3217b831fc1a04f65614da7545..a482a471de050e1a17145a7ac7409dbbef8b5b0d 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -30,9 +30,6 @@ class Synthesizer(val context : LeonContext,
def getSearch: Search = {
if (settings.manualSearch.isDefined) {
new ManualSearch(context, ci, problem, settings.costModel, settings.manualSearch)
- } else if (settings.searchWorkers > 1) {
- ???
- //new ParallelSearch(this, problem, options.searchWorkers)
} else {
new SimpleSearch(context, ci, problem, settings.costModel, settings.searchBound)
}
@@ -79,7 +76,7 @@ class Synthesizer(val context : LeonContext,
val solverf = SolverFactory.getFromName(context, npr)("fairz3").withTimeout(timeout)
val vctx = VerificationContext(context, npr, solverf, context.reporter)
- val vcs = generateVCs(vctx, Some(fds.map(_.id.name).toSeq))
+ val vcs = generateVCs(vctx, Some(fds.map(_.id.name)))
val vcreport = checkVCs(vctx, vcs)
if (vcreport.totalValid == vcreport.totalConditions) {
diff --git a/src/main/scala/leon/synthesis/rules/InlineHoles.scala b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
deleted file mode 100644
index 2ad8a822b566cdff4a33e2efe1550b721b6f2961..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/synthesis/rules/InlineHoles.scala
+++ /dev/null
@@ -1,152 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package synthesis
-package rules
-
-import scala.annotation.tailrec
-import scala.concurrent.duration._
-
-import solvers._
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Constructors._
-
-case object InlineHoles extends Rule("Inline-Holes") {
- override val priority = RulePriorityHoles
-
- def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- // When true: withOracle gets converted into a big choose() on result.
- val sctx = hctx.sctx
- val discreteHoles = sctx.settings.distreteHoles
-
- if (!discreteHoles) {
- return Nil
- }
-
- val Some(oracleHead) = sctx.program.definedFunctions.find(_.id.name == "Oracle.head")
-
- def containsHoles(e: Expr): Boolean = {
- preTraversal{
- case FunctionInvocation(TypedFunDef(`oracleHead`, _), _) => return true
- case _ =>
- }(e)
- false
- }
-
- /**
- * Returns true if the expression directly or indirectly relies on a Hole
- */
- def usesHoles(e: Expr): Boolean = {
- var cache = Map[FunDef, Boolean]()
-
- def callsHolesExpr(e: Expr): Boolean = {
- containsHoles(e) || functionCallsOf(e).exists(fi => callsHoles(fi.tfd.fd))
- }
-
- def callsHoles(fd: FunDef): Boolean = cache.get(fd) match {
- case Some(r) => r
- case None =>
- cache += fd -> false
-
- val res = fd.body.exists(callsHolesExpr)
-
- cache += fd -> res
- res
- }
-
- callsHolesExpr(e)
- }
-
- @tailrec
- def inlineUntilHoles(e: Expr): Expr = {
- if (containsHoles(e)) {
- // Holes are exposed, no need to inline (yet)
- e
- } else {
- // Inline all functions "once" that contain holes
- val newE = postMap {
- case fi @ FunctionInvocation(tfd, args) if usesHoles(fi) && tfd.hasBody =>
- val inlined = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, tfd.body.get)
- Some(inlined)
-
- case _ => None
- }(e)
-
- inlineUntilHoles(newE)
- }
- }
-
- def inlineHoles(phi: Expr): (List[Identifier], Expr) = {
-
- var newXs = List[Identifier]()
-
- val res = preMap {
- case h @ FunctionInvocation(TypedFunDef(`oracleHead`, Seq(tpe)), Seq(o)) =>
- val x = FreshIdentifier("h", tpe, true)
- newXs ::= x
-
- Some(x.toVariable)
- case _ => None
- }(phi)
-
- (newXs.reverse, res)
- }
-
- if (usesHoles(p.phi)) {
- val pathsToCalls = CollectorWithPaths({
- case fi: FunctionInvocation if usesHoles(fi) => fi
- }).traverse(p.phi).map(_._2)
-
- val pc = if (pathsToCalls.nonEmpty) {
- not(orJoin(pathsToCalls))
- } else {
- BooleanLiteral(false)
- }
-
- // Creates two alternative branches:
- // 1) a version with holes unreachable, on which this rule won't re-apply
- val sfact = sctx.solverFactory.withTimeout(500.millis)
- val solver = SimpleSolverAPI(sctx.solverFactory.withTimeout(2.seconds))
-
- val(holesAvoidable, _) = solver.solveSAT(and(p.pc, pc))
-
- val avoid = if (holesAvoidable != Some(false)) {
- val newPhi = simplifyPaths(sfact)(and(pc, p.phi))
- val newProblem1 = p.copy(phi = newPhi)
-
- Some(decomp(List(newProblem1), {
- case List(s) if s.pre != BooleanLiteral(false) => Some(s)
- case _ => None
- }, "Avoid Holes"))
- } else {
- None
- }
-
- // 2) a version with holes reachable to continue applying itself
- val newPhi = inlineUntilHoles(p.phi)
- val (newXs, newPhiInlined) = inlineHoles(newPhi)
-
- val newProblem2 = p.copy(phi = newPhiInlined, xs = p.xs ::: newXs)
- val rec = Some(decomp(List(newProblem2), project(p.xs.size), "Inline Holes"))
-
- List(rec, avoid).flatten
- } else {
- Nil
- }
- }
-
- def project(firstN: Int): List[Solution] => Option[Solution] = {
- project(0 until firstN)
- }
-
- def project(ids: Seq[Int]): List[Solution] => Option[Solution] = {
- case List(s) =>
- Some(s.project(ids))
- case _ =>
- None
- }
-}
diff --git a/src/main/scala/leon/utils/FileOutputPhase.scala b/src/main/scala/leon/utils/FileOutputPhase.scala
index 76341dd1cd28279dbf412fae4233120a1ddde079..351e0882a6a26f09a6895f52ba4c5f1b24db8f87 100644
--- a/src/main/scala/leon/utils/FileOutputPhase.scala
+++ b/src/main/scala/leon/utils/FileOutputPhase.scala
@@ -9,15 +9,21 @@ import java.io.File
object FileOutputPhase extends UnitPhase[Program] {
val name = "File output"
- val description = "Output parsed/generated program into files under the specified directory (default: leon.out)"
-
- override val definedOptions : Set[LeonOptionDef] = Set(
- LeonValueOptionDef("o", "--o=<file>", "Output file")
- )
+ val description = "Output parsed/generated program to the specified directory (default: leon.out)"
+
+ val OutputDirectory = new LeonOptionDef[String] {
+ val name = "o"
+ val description = "Output directory"
+ val default = "leon.out"
+ val usageRhs = "dir"
+ val parser = (x: String) => x
+ }
+
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(OutputDirectory)
def apply(ctx:LeonContext, p : Program) {
// Get the output file name from command line, or use default
- val outputFolder = ( for (LeonValueOption("o", file) <- ctx.options) yield file ).lastOption.getOrElse("leon.out")
+ val outputFolder = ctx.findOptionOrDefault(OutputDirectory)
try {
new File(outputFolder).mkdir()
} catch {
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 865f3b484ccad97f77410974d6937d7b2e60ec14..239637f59ac820a6a7020341355dcacca59f2f69 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -18,28 +18,12 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
implicit val debugSection = utils.DebugSectionVerification
- override val definedOptions : Set[LeonOptionDef] = Set(
- LeonValueOptionDef("functions", "--functions=f1:f2", "Limit verification to f1,f2,..."),
- LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when trying to prove a verification condition.")
- )
-
def run(ctx: LeonContext)(program: Program): VerificationReport = {
- var filterFuns: Option[Seq[String]] = None
- var timeout: Option[Int] = None
+ val filterFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.FunctionsOptionDef)
+ val timeout: Option[Long] = ctx.findOption(SharedOptions.Timeout)
val reporter = ctx.reporter
- for(opt <- ctx.options) opt match {
- case LeonValueOption("functions", ListValue(fs)) =>
- filterFuns = Some(fs)
-
-
- case v @ LeonValueOption("timeout", _) =>
- timeout = v.asInt(ctx)
-
- case _ =>
- }
-
// Solvers selection and validation
var baseSolverF = SolverFactory.getFromSettings(ctx, program)
@@ -119,14 +103,14 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
for (vc <- vcs.par if !stop) yield {
val r = checkVC(vctx, vc)
if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
- stop = stopAfter.map(f => f(vc, r)).getOrElse(false)
+ stop = stopAfter.exists(_(vc, r))
vc -> Some(r)
}
} else {
for (vc <- vcs.toSeq.sortWith((a,b) => a.fd.getPos < b.fd.getPos) if !interruptManager.isInterrupted && !stop) yield {
val r = checkVC(vctx, vc)
if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
- stop = stopAfter.map(f => f(vc, r)).getOrElse(false)
+ stop = stopAfter.exists(_(vc, r))
vc -> Some(r)
}
}
@@ -142,7 +126,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val vcCond = vc.condition
- val s = solverFactory.getNewSolver
+ val s = solverFactory.getNewSolver()
try {
reporter.synchronized {
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 7d49e07658f414be6f4ee9aff5e09b98fe4a1c5b..15e97fcee8946c39e7a7eb46f04e92a073ac7b63 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -38,9 +38,9 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
val newOptions = ctx.options map {
- case LeonValueOption("functions", ListValue(fs)) => {
+ case LeonOption(SharedOptions.FunctionsOptionDef, fs) => {
var freshToAnalyse: Set[String] = Set()
- fs.foreach((toAnalyse: String) => {
+ fs.asInstanceOf[Seq[String]].foreach((toAnalyse: String) => {
pgm.definedFunctions.find(_.id.name == toAnalyse) match {
case Some(fd) => {
val children = subFunctionsOf(fd)
@@ -51,7 +51,7 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
}
})
- LeonValueOption("functions", ListValue(freshToAnalyse.toList))
+ LeonOption(SharedOptions.FunctionsOptionDef)(freshToAnalyse.toList)
}
case opt => opt
}
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index c5e3c7f4087e9f32e25904c542861799285c2da9..9b2822faf9ec4c84e8dd4352d5355d737ae99487 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -113,11 +113,11 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
body
} catch {
case fe: LeonFatalError =>
- testContext.reporter match {
- case sr: TestSilentReporter =>
- sr.lastErrors ++= fe.msg
- throw new TestFailedException(sr.lastErrors.mkString("\n"), fe, 5)
- }
+ testContext.reporter match {
+ case sr: TestSilentReporter =>
+ sr.lastErrors ++= fe.msg
+ throw new TestFailedException(sr.lastErrors.mkString("\n"), fe, 5)
+ }
}
}
diff --git a/src/test/scala/leon/test/TestSilentReporter.scala b/src/test/scala/leon/test/TestSilentReporter.scala
index a0bb40495cc55d2f085485409d480028bf7f181a..a303d35a99ed6a76d2068a9a279fb5ec664e5d38 100644
--- a/src/test/scala/leon/test/TestSilentReporter.scala
+++ b/src/test/scala/leon/test/TestSilentReporter.scala
@@ -1,9 +1,9 @@
/* Copyright 2009-2015 EPFL, Lausanne */
package leon.test
-import leon.{DefaultReporter,Settings}
+import leon.DefaultReporter
-class TestSilentReporter extends DefaultReporter(Settings()) {
+class TestSilentReporter extends DefaultReporter(Set()) {
var lastErrors: List[String] = Nil
override def emit(msg: Message): Unit = msg match {
diff --git a/src/test/scala/leon/test/frontends/ImportsTests.scala b/src/test/scala/leon/test/frontends/ImportsTests.scala
index d0d6e719fb38b7074b220cb49dd44ed7c508e188..e01c786abef801f03c873d18b71a413578703e5f 100644
--- a/src/test/scala/leon/test/frontends/ImportsTests.scala
+++ b/src/test/scala/leon/test/frontends/ImportsTests.scala
@@ -9,17 +9,13 @@ import purescala.ScalaPrinter
import frontends.scalac._
import utils._
-
class ImportsTests extends LeonTestSuite {
private def parseStrings(strs : List[String]) : Program = {
- val settings : Settings = Settings(
- verify = false
- )
- val reporter = new DefaultReporter(settings)
+
+ val reporter = new DefaultReporter(Set())
val context : LeonContext = LeonContext(
reporter,
new InterruptManager(reporter),
- settings,
Seq()
)
diff --git a/src/test/scala/leon/test/purescala/DefOpsTests.scala b/src/test/scala/leon/test/purescala/DefOpsTests.scala
index 27c192e61b392d338e88bd2ed09cfeb902a1bd62..0f6d2465cb4b7531e3465d7c73d8b8368e050bd3 100644
--- a/src/test/scala/leon/test/purescala/DefOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/DefOpsTests.scala
@@ -11,11 +11,8 @@ import leon.test.LeonTestSuite
private [purescala] object DefOpsHelper extends LeonTestSuite {
private def parseStrings(strs : List[String]) : Program = {
- val c = createLeonContext()
- val context : LeonContext = c.copy(settings =
- c.settings.copy(verify = false)
- )
-
+ val context = createLeonContext()
+
val pipeline =
ExtractionPhase andThen
PreprocessingPhase
diff --git a/src/test/scala/leon/test/repair/RepairSuite.scala b/src/test/scala/leon/test/repair/RepairSuite.scala
index 54fdd551ed0e7b433f8277c00bd3deae9c437154..797f13abe1027088e28c67731de8daa24384f728 100644
--- a/src/test/scala/leon/test/repair/RepairSuite.scala
+++ b/src/test/scala/leon/test/repair/RepairSuite.scala
@@ -30,7 +30,7 @@ class RepairSuite extends LeonTestSuite {
val ctx = LeonContext(
reporter = reporter,
interruptManager = new InterruptManager(reporter),
- options = Seq(LeonValueOption("functions", fileToFun(name)))
+ options = Seq(LeonOption(SharedOptions.FunctionsOptionDef)(Seq(fileToFun(name))))
)
test(name) {
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 6dc11e732af485125bdc08323dfe2fe6f0e5213b..6c9fee9be112fee40eee5d4da1ef1a3ebad2a877 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -28,7 +28,7 @@ class SynthesisRegressionSuite extends LeonTestSuite {
test(cat+": "+f.getName+" Compilation") {
ctx = createLeonContext("--synthesis")
- opts = SynthesisSettings(searchBound = Some(bound), allSeeing = true)
+ opts = SynthesisSettings(searchBound = Some(bound))
val pipeline = leon.frontends.scalac.ExtractionPhase andThen leon.utils.PreprocessingPhase
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index aea7b5c550c37b867df1603a1a130dedb1f24dd4..d2aa2d412f0215f18e9325afdc5f2ed506435447 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -83,11 +83,7 @@ class SynthesisSuite extends LeonTestSuite {
def forProgram(title: String, opts: SynthesisSettings = SynthesisSettings())(content: String)(strats: PartialFunction[String, SynStrat]) {
test(f"Synthesizing ${nextInt()}%3d: [$title]") {
- val ctx = testContext.copy(settings = Settings(
- synthesis = true,
- xlang = false,
- verify = false
- ))
+ val ctx = testContext
val pipeline = leon.utils.TemporaryInputPhase andThen leon.frontends.scalac.ExtractionPhase andThen PreprocessingPhase andThen SynthesisProblemExtractionPhase
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
index 0ed517ecbddf483e026255d0e207faf7adeb765e..15b6bc3c434994b0b4fde1d1c420ee5d984c62fb 100644
--- a/src/test/scala/leon/test/termination/TerminationRegression.scala
+++ b/src/test/scala/leon/test/termination/TerminationRegression.scala
@@ -20,7 +20,7 @@ class TerminationRegression extends LeonTestSuite {
private def mkPipeline : Pipeline[List[String],TerminationReport] =
leon.frontends.scalac.ExtractionPhase andThen leon.utils.PreprocessingPhase andThen leon.termination.TerminationPhase
- private def mkTest(file : File, leonOptions: Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
+ private def mkTest(file : File, leonOptions: Seq[LeonOption[Any]], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath
val start = fullName.indexOf("regression")
@@ -35,13 +35,7 @@ class TerminationRegression extends LeonTestSuite {
s"Benchmark $displayName is not a readable file")
val ctx = testContext.copy(
- settings = Settings(
- synthesis = false,
- xlang = false,
- verify = false,
- termination = true
- ),
- options = leonOptions.toList,
+ options = leonOptions,
files = List(file)
)