diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/GlobalOptions.scala
similarity index 92%
rename from src/main/scala/leon/SharedOptions.scala
rename to src/main/scala/leon/GlobalOptions.scala
index b68e64c83a6fd42e445dd4b5fa3b3bd42a935de4..4973852c2574413ded9534494a0af9390b0b360a 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/GlobalOptions.scala
@@ -10,7 +10,7 @@ import OptionParsers._
* Options that determine the pipeline of Leon are not stored here,
* but in [[Main.MainComponent]] instead.
*/
-object SharedOptions extends LeonComponent {
+object GlobalOptions extends LeonComponent {
val name = "sharedOptions"
val description = "Options shared by multiple components of Leon"
@@ -66,7 +66,12 @@ object SharedOptions extends LeonComponent {
val parser: String => Set[DebugSection] = setParser[Set[DebugSection]](debugParser)(_).flatten
}
- val optTimeout = LeonLongOptionDef("timeout", "Set a timeout for attempting to prove a verification condition/ repair a function (in sec.)", 0L, "t")
+ val optTimeout = LeonLongOptionDef(
+ "timeout",
+ "Set a timeout for attempting to prove a verification condition/ repair a function (in sec.)",
+ 0L,
+ "t"
+ )
override val definedOptions: Set[LeonOptionDef[Any]] = Set(
optStrictPhases,
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 000e785b0436e290bda692140c33b34e9183860d..2298914183cd45836da8c8ab273c8896a9f62a77 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -40,7 +40,7 @@ object LeonContext {
LeonContext(
reporter,
new InterruptManager(reporter),
- options = Seq(LeonOption[Set[DebugSection]](SharedOptions.optDebug)(Set(DebugSectionTrees)))
+ options = Seq(LeonOption[Set[DebugSection]](GlobalOptions.optDebug)(Set(DebugSectionTrees)))
)
}
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 509a04d38788c922d4fcc3ca9bf5ed4355e2be5c..f8cfa690e8983342d0ea35781f878b4edd3cafe6 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -35,7 +35,7 @@ object Main {
// Add whatever you need here.
lazy val allComponents : Set[LeonComponent] = allPhases.toSet ++ Set(
- solvers.combinators.UnrollingProcedure, MainComponent, SharedOptions, solvers.smtlib.SMTLIBCVC4Component, solvers.isabelle.Component
+ solvers.combinators.UnrollingProcedure, MainComponent, GlobalOptions, solvers.smtlib.SMTLIBCVC4Component, solvers.isabelle.Component
)
/*
@@ -74,14 +74,14 @@ object Main {
reporter.info("")
reporter.title("Additional global options")
- for (opt <- SharedOptions.definedOptions.toSeq.sortBy(_.name)) {
+ for (opt <- GlobalOptions.definedOptions.toSeq.sortBy(_.name)) {
reporter.info(opt.helpString)
}
reporter.info("")
reporter.title("Additional options, by component:")
- for (c <- (allComponents - MainComponent - SharedOptions).toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
+ for (c <- (allComponents - MainComponent - GlobalOptions).toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
reporter.info("")
reporter.info(s"${c.name} (${c.description})")
for (opt <- c.definedOptions.toSeq.sortBy(_.name)) {
@@ -127,8 +127,9 @@ object Main {
val reporter = new DefaultReporter(
leonOptions.collectFirst {
- case LeonOption(SharedOptions.optDebug, sections) => sections.asInstanceOf[Set[DebugSection]]
- }.getOrElse(Set[DebugSection]()))
+ case LeonOption(GlobalOptions.optDebug, sections) => sections.asInstanceOf[Set[DebugSection]]
+ }.getOrElse(Set[DebugSection]())
+ )
reporter.whenDebug(DebugSectionOptions) { debug =>
debug("Options considered by Leon:")
@@ -159,13 +160,13 @@ object Main {
import genc.CFileOutputPhase
import MainComponent._
import invariant.engine.InferInvariantsPhase
- import transformations._
+ import transformations.InstrumentationPhase
import laziness._
val helpF = ctx.findOptionOrDefault(optHelp)
val noopF = ctx.findOptionOrDefault(optNoop)
val synthesisF = ctx.findOptionOrDefault(optSynthesis)
- val xlangF = ctx.findOptionOrDefault(SharedOptions.optXLang)
+ val xlangF = ctx.findOptionOrDefault(GlobalOptions.optXLang)
val repairF = ctx.findOptionOrDefault(optRepair)
val isabelleF = ctx.findOptionOrDefault(optIsabelle)
val terminationF = ctx.findOptionOrDefault(optTermination)
@@ -239,7 +240,7 @@ object Main {
ctx.interruptManager.registerSignalHandler()
- val doWatch = ctx.findOptionOrDefault(SharedOptions.optWatch)
+ val doWatch = ctx.findOptionOrDefault(GlobalOptions.optWatch)
if (doWatch) {
val watcher = new FilesWatcher(ctx, ctx.files ++ Build.libFiles.map { new java.io.File(_) })
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index aa1471cb8b962e4261f116fe98699f5eed94b3ec..24875b4a627c2acc090abdebef442a355cec5794 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): (LeonContext, G) = {
val (ctx2, s) = self.run(ctx, v)
- if(ctx.findOptionOrDefault(SharedOptions.optStrictPhases)) ctx.reporter.terminateIfError()
+ if(ctx.findOptionOrDefault(GlobalOptions.optStrictPhases)) ctx.reporter.terminateIfError()
thenn.run(ctx2, s)
}
}
diff --git a/src/main/scala/leon/evaluators/EvaluationPhase.scala b/src/main/scala/leon/evaluators/EvaluationPhase.scala
index df2f4c42aebc0533fe6fb4b59d263067fa4804a3..79ae30a5b42e372436f5989659b5fd691cbb05b7 100644
--- a/src/main/scala/leon/evaluators/EvaluationPhase.scala
+++ b/src/main/scala/leon/evaluators/EvaluationPhase.scala
@@ -15,7 +15,7 @@ object EvaluationPhase extends UnitPhase[Program] {
implicit val debugSection = utils.DebugSectionEvaluation
def apply(ctx: LeonContext, program: Program): Unit = {
- val evalFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
+ val evalFuns: Option[Seq[String]] = ctx.findOption(GlobalOptions.optFunctions)
val evaluator = ctx.findOptionOrDefault(MainComponent.optEval)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 4b3c577ad8e6c5a0066ac3ac87317abb837c4c87..65ea83c7f9b760dd5d165f17891f4cc7225f1786 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -71,7 +71,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.optDebug) contains utils.DebugSectionTrees) {
+ val debugInfo = if (ctx.findOptionOrDefault(GlobalOptions.optDebug) contains utils.DebugSectionTrees) {
ot.map { t =>
val strWr = new java.io.StringWriter()
new global.TreePrinter(new java.io.PrintWriter(strWr)).printTree(t)
diff --git a/src/main/scala/leon/invariant/engine/InferenceContext.scala b/src/main/scala/leon/invariant/engine/InferenceContext.scala
index 48a45b048a33691f368242b63b45ae5bc062881c..904ae772862b514ea99a19d76a3cff7c9a092e2b 100644
--- a/src/main/scala/leon/invariant/engine/InferenceContext.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceContext.scala
@@ -33,13 +33,13 @@ class InferenceContext(val initProgram: Program, val leonContext: LeonContext) {
val withmult = leonContext.findOption(optWithMult).getOrElse(false)
val usereals = leonContext.findOption(optUseReals).getOrElse(false)
val useCegis: Boolean = leonContext.findOption(optCegis).getOrElse(false)
- val dumpStats = leonContext.findOption(SharedOptions.optBenchmark).getOrElse(false)
+ val dumpStats = leonContext.findOption(GlobalOptions.optBenchmark).getOrElse(false)
// the following options have default values
val vcTimeout = leonContext.findOption(optVCTimeout).getOrElse(15L) // in secs
val nlTimeout = leonContext.findOption(optNLTimeout).getOrElse(15L)
- val totalTimeout = leonContext.findOption(SharedOptions.optTimeout) // in secs
- val functionsToInfer = leonContext.findOption(SharedOptions.optFunctions)
+ val totalTimeout = leonContext.findOption(GlobalOptions.optTimeout) // in secs
+ val functionsToInfer = leonContext.findOption(GlobalOptions.optFunctions)
val reporter = leonContext.reporter
val maxCegisBound = 1000
val statsSuffix = leonContext.findOption(optStatsSuffix).getOrElse("-stats" + FileCountGUID.getID)
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 9c1abab5381882451a3a0769b590301c94d4f81a..60daeb0d3e9e52da177f40c5cab429459899fde9 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -116,7 +116,7 @@ object LazinessEliminationPhase extends TransformationPhase {
checkInstrumentationSpecs(instProg, checkCtx,
checkCtx.findOption(LazinessEliminationPhase.optUseOrb).getOrElse(false))
// dump stats
- if (ctx.findOption(SharedOptions.optBenchmark).getOrElse(false)) {
+ if (ctx.findOption(GlobalOptions.optBenchmark).getOrElse(false)) {
val modid = prog.units.find(_.isMainUnit).get.id
val filename = modid + "-stats.txt"
val pw = new PrintWriter(filename)
diff --git a/src/main/scala/leon/purescala/PrinterOptions.scala b/src/main/scala/leon/purescala/PrinterOptions.scala
index 6a95b265d7871df9c5575a2ea605e457097b4e3f..22c4c02477bb4886df9994eee3f1a24740bfac9b 100644
--- a/src/main/scala/leon/purescala/PrinterOptions.scala
+++ b/src/main/scala/leon/purescala/PrinterOptions.scala
@@ -14,9 +14,9 @@ case class PrinterOptions (
object PrinterOptions {
def fromContext(ctx: LeonContext): PrinterOptions = {
- val debugTrees = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionTrees
- val debugTypes = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionTypes
- val debugPositions = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionPositions
+ val debugTrees = ctx.findOptionOrDefault(GlobalOptions.optDebug) contains DebugSectionTrees
+ val debugTypes = ctx.findOptionOrDefault(GlobalOptions.optDebug) contains DebugSectionTypes
+ val debugPositions = ctx.findOptionOrDefault(GlobalOptions.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 342d41dddb28acf9312e5b5b5388ec2023318529..1481b0e782345eac4267b57b744c1a0c85482113 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -13,8 +13,8 @@ object RepairPhase extends UnitPhase[Program]() {
implicit val debugSection = utils.DebugSectionRepair
def apply(ctx: LeonContext, program: Program) = {
- val repairFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
- val verifTimeoutMs: Option[Long] = ctx.findOption(SharedOptions.optTimeout) map { _ * 1000 }
+ val repairFuns: Option[Seq[String]] = ctx.findOption(GlobalOptions.optFunctions)
+ val verifTimeoutMs: Option[Long] = ctx.findOption(GlobalOptions.optTimeout) map { _ * 1000 }
val reporter = ctx.reporter
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 49f9c0ff2fbe318d303f0c9e2f2719c0da60bf75..65b6aee97bfcea95a7ef242a05ef8f1d5d176c4e 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -29,7 +29,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val reporter = ctx.reporter
- val doBenchmark = ctx.findOptionOrDefault(SharedOptions.optBenchmark)
+ val doBenchmark = ctx.findOptionOrDefault(GlobalOptions.optBenchmark)
var program = initProgram
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 4f8b1f50ae346887c945823ff429761be1a34a78..18b8a72a170fadd83ecdaa71d9aa5c6cd12110dd 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -49,7 +49,7 @@ object SolverFactory {
}.mkString("")
def getFromSettings(implicit ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
- val names = ctx.findOptionOrDefault(SharedOptions.optSelectedSolvers)
+ val names = ctx.findOptionOrDefault(GlobalOptions.optSelectedSolvers)
if (((names contains "fairz3") || (names contains "unrollz3")) && !hasNativeZ3) {
if (hasZ3) {
@@ -138,7 +138,7 @@ object SolverFactory {
// Fast solver used by simplifications, to discharge simple tautologies
def uninterpreted(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
- val names = ctx.findOptionOrDefault(SharedOptions.optSelectedSolvers)
+ val names = ctx.findOptionOrDefault(GlobalOptions.optSelectedSolvers)
if ((names contains "fairz3") && !hasNativeZ3) {
if (hasZ3) {
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 95a8cdd67722660f666a9256a0020fab9d93b5d2..e00faa54c5ccb75cdc0f8730af7fcf89dfe0ec2f 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -4,7 +4,6 @@ package leon
package solvers
package combinators
-import purescala.Printable
import purescala.Common._
import purescala.Definitions._
import purescala.Quantification._
diff --git a/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala b/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
index 2d3218c7b09edfa465618117a66b7f428f755b1c..ace759b4e43c381cce9b4a37348fe84be42aa1b4 100644
--- a/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
+++ b/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
@@ -32,7 +32,7 @@ object AdaptationPhase extends TransformationPhase {
CaseClass(CaseClassType(dummy, List(tree)), Nil)
val enabled =
- context.findOptionOrDefault(SharedOptions.optSelectedSolvers).contains("isabelle") ||
+ context.findOptionOrDefault(GlobalOptions.optSelectedSolvers).contains("isabelle") ||
context.findOptionOrDefault(Main.MainComponent.optIsabelle)
if (!enabled) program
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
index 5856374e289d5f39c9669ec93ba6bef0e91e2693..fa7b3d0345b795d9b757cbcc9e1d0f3dc0db47dc 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
@@ -9,7 +9,7 @@ import scala.concurrent.ExecutionContext.Implicits.global
import leon.LeonContext
import leon.OptionsHelpers._
-import leon.SharedOptions
+import leon.GlobalOptions
import leon.purescala.Definitions._
import leon.purescala.Expressions._
import leon.purescala.Common._
@@ -34,7 +34,7 @@ object IsabelleEnvironment {
val funFilter =
// FIXME duplicated from AnalysisPhase
- filterInclusive[FunDef](context.findOption(SharedOptions.optFunctions).map(fdMatcher(program)), Some(_.annotations contains "library"))
+ filterInclusive[FunDef](context.findOption(GlobalOptions.optFunctions).map(fdMatcher(program)), Some(_.annotations contains "library"))
val funs = program.definedFunctions.filter(funFilter)
diff --git a/src/main/scala/leon/synthesis/SourceInfo.scala b/src/main/scala/leon/synthesis/SourceInfo.scala
index ca689cca02a138c7562c517a1dccad108f2f4a3d..70f116d5f54d0d4bec6c84a2a2c627ef630c6ee1 100644
--- a/src/main/scala/leon/synthesis/SourceInfo.scala
+++ b/src/main/scala/leon/synthesis/SourceInfo.scala
@@ -21,7 +21,7 @@ object SourceInfo {
}
def extractFromProgram(ctx: LeonContext, prog: Program): List[SourceInfo] = {
- val functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet }
+ val functions = ctx.findOption(GlobalOptions.optFunctions) map { _.toSet }
def excludeByDefault(fd: FunDef): Boolean = {
fd.annotations contains "library"
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 7c90d3e3b4495cf8a97c977df1ce4d199df34640..2385f50798b3748f06b63370a4a0bbe2b22f5aa9 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -32,7 +32,7 @@ object SynthesisPhase extends TransformationPhase {
def processOptions(ctx: LeonContext): SynthesisSettings = {
val ms = ctx.findOption(optManual)
- val timeout = ctx.findOption(SharedOptions.optTimeout)
+ val timeout = ctx.findOption(GlobalOptions.optTimeout)
if (ms.isDefined && timeout.isDefined) {
ctx.reporter.warning("Defining timeout with manual search")
}
@@ -58,7 +58,7 @@ object SynthesisPhase extends TransformationPhase {
costModel = costModel,
rules = Rules.all(ctx.findOptionOrDefault(optCEGISNaiveGrammar)),
manualSearch = ms,
- functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet },
+ functions = ctx.findOption(GlobalOptions.optFunctions) map { _.toSet },
cegisUseOptTimeout = ctx.findOptionOrDefault(optCEGISOptTimeout),
cegisUseVanuatoo = ctx.findOptionOrDefault(optCEGISVanuatoo),
cegisMaxSize = ctx.findOptionOrDefault(optCEGISMaxSize).toInt
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index f75d388d4d2f63317f1c90d063a6404bc78e5edb..15f2dbe5ae5e3625252b0bd12c604531335d684f 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -20,7 +20,7 @@ object TerminationPhase extends SimpleLeonPhase[Program, TerminationReport] {
val fdFilter = {
import OptionsHelpers._
- filterInclusive(ctx.findOption(SharedOptions.optFunctions).map(fdMatcher(program)), Some(excludeByDefault _))
+ filterInclusive(ctx.findOption(GlobalOptions.optFunctions).map(fdMatcher(program)), Some(excludeByDefault _))
}
val toVerify = tc.program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
diff --git a/src/main/scala/leon/verification/VerificationPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
index 04c4ecdcce10e724c1fae82b8faff95e7a6a619c..b9da4addb18042bf1f00309d7191f3469776e3f4 100644
--- a/src/main/scala/leon/verification/VerificationPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -22,8 +22,8 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
implicit val debugSection = utils.DebugSectionVerification
def apply(ctx: LeonContext, program: Program): VerificationReport = {
- val filterFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
- val timeout: Option[Long] = ctx.findOption(SharedOptions.optTimeout)
+ val filterFuns: Option[Seq[String]] = ctx.findOption(GlobalOptions.optFunctions)
+ val timeout: Option[Long] = ctx.findOption(GlobalOptions.optTimeout)
val reporter = ctx.reporter
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 5f9861362b3d642f0426131eb39014b962656813..653afe38f37f3eba9d4dfe8029648e752845fe0d 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -38,9 +38,9 @@ class RepairSuite extends LeonRegressionSuite {
reporter = reporter,
interruptManager = new InterruptManager(reporter),
options = Seq(
- LeonOption(SharedOptions.optFunctions)(Seq(fileToFun(name))),
+ LeonOption(GlobalOptions.optFunctions)(Seq(fileToFun(name))),
LeonOption(VerificationPhase.optParallelVCs)(true),
- LeonOption(SharedOptions.optTimeout)(180L)
+ LeonOption(GlobalOptions.optTimeout)(180L)
)
)