diff --git a/project/Build.scala b/project/Build.scala
index 002494c53806c763a01bbf79fb20525622608b8c..1a03ba0189c16d277c2e722a24c884f6cda5c806 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -80,6 +80,6 @@ object Leon extends Build {
def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
lazy val bonsai = project("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
- lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "24a8b85949c69189f37c5fdfab3265801a084ee8")
+ lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "d13c86eb5a60bd9f64ef6724bc4f53fcf466c922")
}
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 17f431413f77fabeb2ad1ad58fb7b75c06678d16..72e8c3fb9a4e58d60af43a69d1ff1f71729524f6 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -34,17 +34,17 @@ object Main {
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)
+ val optTermination = LeonFlagOptionDef("termination", "Check program termination", false)
+ val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
+ val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
+ val optXLang = LeonFlagOptionDef("xlang", "Support for extra program constructs (imperative,...)", false)
+ val optWatch = LeonFlagOptionDef("watch", "Rerun pipeline when file changes", false)
+ val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
+ val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", true )
+ val optHelp = LeonFlagOptionDef("help", "Show help message", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(Termination, Repair, Synthesis, XLang, Watch, Noop, Help, Verify)
+ Set(optTermination, optRepair, optSynthesis, optXLang, optWatch, optNoop, optHelp, optVerify)
}
@@ -94,7 +94,7 @@ object Main {
val reporter = new DefaultReporter(
leonOptions.collectFirst {
- case LeonOption(SharedOptions.Debug, sections) => sections.asInstanceOf[Set[DebugSection]]
+ case LeonOption(SharedOptions.optDebug, sections) => sections.asInstanceOf[Set[DebugSection]]
}.getOrElse(Set[DebugSection]())
)
@@ -124,13 +124,13 @@ object Main {
import repair.RepairPhase
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)
+ val helpF = ctx.findOptionOrDefault(optHelp)
+ val noopF = ctx.findOptionOrDefault(optNoop)
+ val synthesisF = ctx.findOptionOrDefault(optSynthesis)
+ val xlangF = ctx.findOptionOrDefault(optXLang)
+ val repairF = ctx.findOptionOrDefault(optRepair)
+ val terminationF = ctx.findOptionOrDefault(optTermination)
+ val verifyF = ctx.findOptionOrDefault(optVerify)
if (helpF) {
displayHelp(ctx.reporter, error = false)
@@ -186,7 +186,7 @@ object Main {
ctx.interruptManager.registerSignalHandler()
- val doWatch = ctx.findOptionOrDefault(MainComponent.Watch)
+ val doWatch = ctx.findOptionOrDefault(MainComponent.optWatch)
if (doWatch) {
val watcher = new FilesWatcher(ctx, ctx.files)
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 0838771245f5d279f51b7b5e658225ac88d8da17..e4f93fcfa25809c8d373a54abe6f442b6171ec0f 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.findOptionOrDefault(SharedOptions.StrictPhases)) ctx.reporter.terminateIfError()
+ if(ctx.findOptionOrDefault(SharedOptions.optStrictPhases)) ctx.reporter.terminateIfError()
thenn.run(ctx)(s)
}
}
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
index a5e7e66350ab351003db479bc19214ce9dc02e8a..4541fc0fc21efd28f281a8d3bf9d2da775eb0628 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/SharedOptions.scala
@@ -10,9 +10,9 @@ 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)
+ val optStrictPhases = LeonFlagOptionDef("strict", "Terminate after each phase if there is an error", true)
- case object FunctionsOptionDef extends LeonOptionDef[Seq[String]] {
+ val optFunctions = new LeonOptionDef[Seq[String]] {
val name = "functions"
val description = "Only consider functions f1, f2, ..."
val default = Seq[String]()
@@ -20,7 +20,7 @@ object SharedOptions extends LeonComponent {
val usageRhs = "f1,f2,..."
}
- case object SelectedSolvers extends LeonOptionDef[Set[String]] {
+ val optSelectedSolvers = new LeonOptionDef[Set[String]] {
val name = "solvers"
val description = "Use solvers s1, s2,...\n" + solvers.SolverFactory.availableSolversPretty
val default = Set("fairz3")
@@ -28,7 +28,7 @@ object SharedOptions extends LeonComponent {
val usageRhs = "s1,s2,..."
}
- case object Debug extends LeonOptionDef[Set[DebugSection]] {
+ val optDebug = new LeonOptionDef[Set[DebugSection]] {
import OptionParsers._
val name = "debug"
val description = "Enable detailed messages per component"
@@ -51,7 +51,13 @@ object SharedOptions extends LeonComponent {
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")
+ val optTimeout = 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)
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(
+ optStrictPhases,
+ optFunctions,
+ optSelectedSolvers,
+ optDebug,
+ optTimeout
+ )
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 4d2ab0eeb86f177da3037e5da2eac0ef9c42ea68..e8771c17a00d6a83daa96776fdceebd13b910e53 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.findOptionOrDefault(SharedOptions.Debug) contains utils.DebugSectionTrees) {
+ val debugInfo = if (ctx.findOptionOrDefault(SharedOptions.optDebug) 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.findOptionOrDefault(ExtractionPhase.StrictCompilation)) {
+ if (ctx.findOptionOrDefault(ExtractionPhase.optStrictCompilation)) {
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.findOptionOrDefault(ExtractionPhase.StrictCompilation)) {
+ if (ctx.findOptionOrDefault(ExtractionPhase.optStrictCompilation)) {
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 c0ba4641e7657b75150e350331e8bf24c7a1023c..c4131034a5c215890de58a4042f9dff945f969ec 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -16,9 +16,9 @@ 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)
+ val optStrictCompilation = LeonFlagOptionDef("strictCompilation", "Exit Leon after an error in compilation", true)
- override val definedOptions: Set[LeonOptionDef[Any]] = Set(StrictCompilation)
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(optStrictCompilation)
implicit val debug = DebugSectionTrees
diff --git a/src/main/scala/leon/purescala/PrinterOptions.scala b/src/main/scala/leon/purescala/PrinterOptions.scala
index 3c1d67d745b6d48e4879c4b99d6f96d97d5c11bb..0a9cb6d771f78cf1f4bdc1921972caf1164069ae 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.findOptionOrDefault(SharedOptions.Debug) contains DebugSectionTrees
- val debugPositions = ctx.findOptionOrDefault(SharedOptions.Debug) contains DebugSectionPositions
+ val debugTrees = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionTrees
+ val debugPositions = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionPositions
PrinterOptions(
baseIndent = 0,
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index 0b4c0d4c622ec69aca9b314b43a9149180b78cf2..c79002a2089cbea3f258df179d1a1bd094f87a62 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -13,8 +13,8 @@ object RepairPhase extends LeonPhase[Program, Program] {
implicit val debugSection = utils.DebugSectionRepair
def run(ctx: LeonContext)(program: Program): Program = {
- val repairFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.FunctionsOptionDef)
- val verifTimeoutMs: Option[Long] = ctx.findOption(SharedOptions.Timeout) map { _ * 1000 }
+ val repairFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
+ val verifTimeoutMs: Option[Long] = ctx.findOption(SharedOptions.optTimeout) map { _ * 1000 }
val reporter = ctx.reporter
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 21a56c5b40f31119598488a8fc4df9c4bc04ce31..06a7fb4c4068722cac573395895cd104c9758e05 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -36,7 +36,7 @@ object SolverFactory {
}.mkString("")
def getFromSettings(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
- getFromName(ctx, program)(ctx.findOptionOrDefault(SharedOptions.SelectedSolvers).toSeq : _*)
+ getFromName(ctx, program)(ctx.findOptionOrDefault(SharedOptions.optSelectedSolvers).toSeq : _*)
}
def getFromName(ctx: LeonContext, program: Program)(names: String*): SolverFactory[TimeoutSolver] = {
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 3aea7b2a8fb063d5ab9181f4b4f095e4ca2b9da6..1946d225dc02cc8dc95f2cd19413692020141730 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -10,15 +10,15 @@ import purescala.Constructors._
import purescala.Expressions._
import purescala.ExprOps._
-import z3.FairZ3Component.{FeelingLucky, UseCodeGen}
+import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen}
import templates._
import utils.Interruptible
import evaluators._
class UnrollingSolver(val context: LeonContext, program: Program, underlying: IncrementalSolver with Interruptible) extends Solver with Interruptible {
- val feelingLucky = context.findOptionOrDefault(FeelingLucky)
- val useCodeGen = context.findOptionOrDefault(UseCodeGen)
+ val feelingLucky = context.findOptionOrDefault(optFeelingLucky)
+ val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
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 f97c59b525fae130ab1e4254af33bbc0c95f3e61..43df5a32c0ac3e8d0839220fe69aa163396853e2 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -23,7 +23,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
def targetName = "cvc4"
def userDefinedOps(ctx: LeonContext) = {
- ctx.findOptionOrDefault(SMTLIBCVC4Component.CVC4Options)
+ ctx.findOptionOrDefault(SMTLIBCVC4Component.optCVC4Options)
}
def interpreterOps(ctx: LeonContext) = {
@@ -187,7 +187,7 @@ object SMTLIBCVC4Component extends LeonComponent {
val description = "Solver invoked when --solvers=smt-cvc4"
- case object CVC4Options extends LeonOptionDef[Set[String]] {
+ val optCVC4Options = new LeonOptionDef[Set[String]] {
val name = "solver:cvc4"
val description = "Pass extra arguments to CVC4"
val default = Set("")
@@ -195,5 +195,5 @@ object SMTLIBCVC4Component extends LeonComponent {
val usageRhs = "<cvc4-opt>"
}
- override val definedOptions : Set[LeonOptionDef[Any]] = Set(CVC4Options)
+ override val definedOptions : Set[LeonOptionDef[Any]] = Set(optCVC4Options)
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Component.scala b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
index 5fc6018e7afeec93123e6794a09c90901a6dacb7..add51eb5fd1d1cbbc1cf6faf52fc957175b5a102 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Component.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
@@ -7,14 +7,14 @@ trait FairZ3Component extends LeonComponent {
val name = "Z3-f"
val description = "Fair Z3 Solver"
- 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)
+ val optEvalGround = LeonFlagOptionDef("evalground", "Use evaluator on functions applied to ground arguments", false)
+ val optCheckModels = LeonFlagOptionDef("checkmodels", "Double-check counter-examples with evaluator", false)
+ val optFeelingLucky = LeonFlagOptionDef("feelinglucky","Use evaluator to find counter-examples early", false)
+ val optUseCodeGen = LeonFlagOptionDef("codegen", "Use compiled evaluator instead of interpreter", false)
+ val optUnrollCores = LeonFlagOptionDef("unrollcores", "Use unsat-cores to drive unrolling while remaining fair", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(EvalGround, CheckModels, FeelingLucky, UseCodeGen, UnrollCores)
+ Set(optEvalGround, optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores)
}
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 99c749ef88ea8108fd2dae24fc458fdba4f2923c..b13345ae42bb1abc24180b12514d542f557452ac 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -25,11 +25,11 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
enclosing =>
- 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)
+ val feelingLucky = context.findOptionOrDefault(optFeelingLucky)
+ val checkModels = context.findOptionOrDefault(optCheckModels)
+ val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
+ val evalGroundApps = context.findOptionOrDefault(optEvalGround)
+ val unrollUnsatCores = context.findOptionOrDefault(optUnrollCores)
private val evaluator: Evaluator =
if(useCodeGen) {
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 7a16afed9ad1ac260e8b1c402dc33603cc6f4934..eacb991de1f68f6114e9757fb8451b45dd86b8f4 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -15,31 +15,31 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
val name = "Synthesis"
val description = "Partial synthesis of \"choose\" constructs"
- 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)
+ val optManual = LeonStringOptionDef("manual", "Manual search", default = "", "cmd")
+ val optCostModel = LeonStringOptionDef("costmodel", "Use a specific cost model for this search", "FIXME", "cm")
+ val optDerivTrees = LeonFlagOptionDef( "derivtrees", "Generate derivation trees", false)
// 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)
+ val optCEGISShrink = LeonFlagOptionDef( "cegis:shrink", "Shrink non-det programs when tests pruning works well", true)
+ val optCEGISOptTimeout = LeonFlagOptionDef( "cegis:opttimeout", "Consider a time-out of CE-search as untrusted solution", true)
+ val optCEGISVanuatoo = LeonFlagOptionDef( "cegis:vanuatoo", "Generate inputs using new korat-style generator", false)
override val definedOptions : Set[LeonOptionDef[Any]] =
- Set(Manual, CostModel, DerivTrees, CEGISShrink, CEGISOptTimeout, CEGISVanuatoo)
+ Set(optManual, optCostModel, optDerivTrees, optCEGISShrink, optCEGISOptTimeout, optCEGISVanuatoo)
def processOptions(ctx: LeonContext): SynthesisSettings = {
- val ms = ctx.findOption(Manual)
+ val ms = ctx.findOption(optManual)
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),
+ functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet },
+ timeoutMs = ctx.findOption(SharedOptions.optTimeout) map { _ * 1000 },
+ generateDerivationTrees = ctx.findOptionOrDefault(optDerivTrees),
+ cegisUseOptTimeout = ctx.findOption(optCEGISOptTimeout),
+ cegisUseShrink = ctx.findOption(optCEGISShrink),
+ cegisUseVanuatoo = ctx.findOption(optCEGISVanuatoo),
rules = Rules.all ++ (ms map { _ => rules.AsChoose}),
costModel = {
- ctx.findOption(CostModel) match {
+ ctx.findOption(optCostModel) match {
case None => CostModels.default
case Some(name) => CostModels.all.find(_.name.toLowerCase == name.toLowerCase) match {
case Some(model) => model
diff --git a/src/main/scala/leon/utils/FileOutputPhase.scala b/src/main/scala/leon/utils/FileOutputPhase.scala
index 351e0882a6a26f09a6895f52ba4c5f1b24db8f87..be92b7086b74357e7ce03b880a03f6d7cb6f812b 100644
--- a/src/main/scala/leon/utils/FileOutputPhase.scala
+++ b/src/main/scala/leon/utils/FileOutputPhase.scala
@@ -11,7 +11,7 @@ object FileOutputPhase extends UnitPhase[Program] {
val name = "File output"
val description = "Output parsed/generated program to the specified directory (default: leon.out)"
- val OutputDirectory = new LeonOptionDef[String] {
+ val optOutputDirectory = new LeonOptionDef[String] {
val name = "o"
val description = "Output directory"
val default = "leon.out"
@@ -19,11 +19,11 @@ object FileOutputPhase extends UnitPhase[Program] {
val parser = (x: String) => x
}
- override val definedOptions: Set[LeonOptionDef[Any]] = Set(OutputDirectory)
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(optOutputDirectory)
def apply(ctx:LeonContext, p : Program) {
// Get the output file name from command line, or use default
- val outputFolder = ctx.findOptionOrDefault(OutputDirectory)
+ val outputFolder = ctx.findOptionOrDefault(optOutputDirectory)
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 239637f59ac820a6a7020341355dcacca59f2f69..97def89818d2fa54b3ca0e1a3e132f60bb4210b2 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -19,8 +19,8 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
implicit val debugSection = utils.DebugSectionVerification
def run(ctx: LeonContext)(program: Program): VerificationReport = {
- val filterFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.FunctionsOptionDef)
- val timeout: Option[Long] = ctx.findOption(SharedOptions.Timeout)
+ val filterFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
+ val timeout: Option[Long] = ctx.findOption(SharedOptions.optTimeout)
val reporter = ctx.reporter
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 15e97fcee8946c39e7a7eb46f04e92a073ac7b63..94e94a8580f4540a6efc06452b2e0e13fea34209 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -38,7 +38,7 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
val newOptions = ctx.options map {
- case LeonOption(SharedOptions.FunctionsOptionDef, fs) => {
+ case LeonOption(SharedOptions.optFunctions, fs) => {
var freshToAnalyse: Set[String] = Set()
fs.asInstanceOf[Seq[String]].foreach((toAnalyse: String) => {
pgm.definedFunctions.find(_.id.name == toAnalyse) match {
@@ -51,7 +51,7 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
}
})
- LeonOption(SharedOptions.FunctionsOptionDef)(freshToAnalyse.toList)
+ LeonOption(SharedOptions.optFunctions)(freshToAnalyse.toList)
}
case opt => opt
}
diff --git a/src/test/scala/leon/test/repair/RepairSuite.scala b/src/test/scala/leon/test/repair/RepairSuite.scala
index 797f13abe1027088e28c67731de8daa24384f728..9be4ca160b9df2541a0f61c436a0003b53258e01 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(LeonOption(SharedOptions.FunctionsOptionDef)(Seq(fileToFun(name))))
+ options = Seq(LeonOption(SharedOptions.optFunctions)(Seq(fileToFun(name))))
)
test(name) {