Fix problems with options

Move optEval to MainComponent
Add helpful comments
Beautify how debugSections are printed
Termination and analysis should happen iff --verify and --termination

src/main/scala/leon/Main.scala

@@ -31,20 +31,25 @@ object Main {
     solvers.z3.FairZ3Component, MainComponent, SharedOptions, solvers.smtlib.SMTLIBCVC4Component
   )
 
+  /*
+   * This object holds the options that determine the selected pipeline of Leon.
+   * Please put any further such options here to have them print nicely in --help message.
+   */
   object MainComponent extends LeonComponent {
     val name = "main"
     val description = "Options that determine the feature of Leon to be used (mutually exclusive). Default: verify"
 
-    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 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)
+    val optEval        = LeonStringOptionDef("eval", "Evaluate ground functions with selected evaluator", "default", "[code|default]")
+    val optXLang       = LeonFlagOptionDef("xlang",       "Verification with support for extra program constructs (imperative,...)", 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 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(optTermination, optRepair, optSynthesis, optXLang, optNoop, optHelp, optVerify)
+      Set(optTermination, optRepair, optSynthesis, optXLang, optNoop, optHelp, optEval, optVerify)
 
   }
 
@@ -149,10 +154,10 @@ object Main {
     val synthesisF   = ctx.findOptionOrDefault(optSynthesis)
     val xlangF       = ctx.findOptionOrDefault(optXLang)
     val repairF      = ctx.findOptionOrDefault(optRepair)
-    val analysisF    = ctx.findOption(optVerify).isDefined && ctx.findOption(optTermination).isDefined
     val terminationF = ctx.findOptionOrDefault(optTermination)
     val verifyF      = ctx.findOptionOrDefault(optVerify)
-    val evalF        = ctx.findOption(SharedOptions.optEval)
+    val evalF        = ctx.findOption(optEval)
+    val analysisF    = verifyF && terminationF
 
     def debugTrees(title: String): LeonPhase[Program, Program] = {
       if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {

src/main/scala/leon/SharedOptions.scala

@@ -5,6 +5,12 @@ package leon
 import leon.utils.{DebugSections, DebugSection}
 import OptionParsers._
 
+/*
+ * This object contains options that are shared among different modules of Leon.
+ *
+ * Options that determine the pipeline of Leon are not stored here,
+ * but in MainComponent in Main.scala.
+ */
 object SharedOptions extends LeonComponent {
 
   val name = "sharedOptions"
@@ -22,8 +28,6 @@ object SharedOptions extends LeonComponent {
     val usageRhs = "f1,f2,..."
   }
 
-  val optEval = LeonStringOptionDef("eval", "Evaluate ground functions", "default", "[code|default]")
-
   val optSelectedSolvers = new LeonOptionDef[Set[String]] {
     val name = "solvers"
     val description = "Use solvers s1, s2,...\n" + solvers.SolverFactory.availableSolversPretty
@@ -35,10 +39,13 @@ object SharedOptions extends LeonComponent {
   val optDebug = new LeonOptionDef[Set[DebugSection]] {
     import OptionParsers._
     val name = "debug"
-    val description = (
-      "Enable detailed messages per component.\nAvailable:" +:
-      DebugSections.all.toSeq.map(_.name).sorted
-    ).mkString("\n  ")
+    val description = {
+      val sects = DebugSections.all.toSeq.map(_.name).sorted
+      val (first, second) = sects.splitAt(sects.length/2)
+      "Enable detailed messages per component.\nAvailable:\n" +
+        "  " + first.mkString(", ") + ",\n" +
+        "  " + second.mkString(", ")
+    }
     val default = Set[DebugSection]()
     val usageRhs = "d1,d2,..."
     val debugParser: OptionParser[Set[DebugSection]] = s => {
@@ -66,7 +73,6 @@ object SharedOptions extends LeonComponent {
     optSelectedSolvers,
     optDebug,
     optWatch,
-    optEval,
     optTimeout
   )
 }

src/main/scala/leon/evaluators/EvaluationPhase.scala

@@ -3,6 +3,7 @@
 package leon
 package evaluators
 
+import leon.Main.MainComponent
 import purescala.Definitions._
 import purescala.DefOps._
 import purescala.Expressions._
@@ -16,7 +17,7 @@ object EvaluationPhase extends LeonPhase[Program, Unit] {
   def run(ctx: LeonContext)(program: Program): Unit = {
     val evalFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
 
-    val evaluator = ctx.findOptionOrDefault(SharedOptions.optEval)
+    val evaluator = ctx.findOptionOrDefault(MainComponent.optEval)
 
     val reporter = ctx.reporter
 

src/main/scala/leon/synthesis/SynthesisPhase.scala

@@ -15,7 +15,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
   val name        = "Synthesis"
   val description = "Partial synthesis of \"choose\" constructs. Also used by repair during the synthesis stage."
 
-  val optManual      = LeonStringOptionDef("manual", "Manual search", default = "", "cmd")
+  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)