Evaluator option --eval takes evaluator as argument

src/main/scala/leon/Main.scala

@@ -42,10 +42,9 @@ object Main {
     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        = LeonFlagOptionDef("eval",        "Evaluate ground functions",                             false)
 
     override val definedOptions: Set[LeonOptionDef[Any]] =
-      Set(optTermination, optRepair, optSynthesis, optXLang, optNoop, optHelp, optVerify, optEval)
+      Set(optTermination, optRepair, optSynthesis, optXLang, optNoop, optHelp, optVerify)
 
   }
 
@@ -151,7 +150,7 @@ object Main {
     val repairF      = ctx.findOptionOrDefault(optRepair)
     val terminationF = ctx.findOptionOrDefault(optTermination)
     val verifyF      = ctx.findOptionOrDefault(optVerify)
-    val evalF        = ctx.findOptionOrDefault(optEval)
+    val evalF        = ctx.findOption(SharedOptions.optEval)
 
     def debugTrees(title: String): LeonPhase[Program, Program] = {
       if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {
@@ -184,7 +183,7 @@ object Main {
         else if (repairF) RepairPhase
         else if (terminationF) TerminationPhase
         else if (xlangF) XLangAnalysisPhase
-        else if (evalF) EvaluationPhase
+        else if (evalF.isDefined) EvaluationPhase
         else if (verifyF) FunctionClosure andThen AnalysisPhase
         else    NoopPhase()
       }

src/main/scala/leon/SharedOptions.scala

@@ -22,6 +22,8 @@ object SharedOptions extends LeonComponent {
     val usageRhs = "f1,f2,..."
   }
 
+  val optEval = LeonStringOptionDef("eval", "Evaluate ground functions", "default", "--eval[=code|default]")
+
   val optSelectedSolvers = new LeonOptionDef[Set[String]] {
     val name = "solvers"
     val description = "Use solvers s1, s2,...\n" + solvers.SolverFactory.availableSolversPretty
@@ -64,6 +66,7 @@ object SharedOptions extends LeonComponent {
     optSelectedSolvers,
     optDebug,
     optWatch,
+    optEval,
     optTimeout
   )
 }

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

@@ -16,6 +16,8 @@ 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 reporter = ctx.reporter
 
     val fdFilter = {
@@ -27,9 +29,15 @@ object EvaluationPhase extends LeonPhase[Program, Unit] {
     val toEvaluate = funDefsFromMain(program).toList.filter(_.params.size == 0).filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
 
     if (toEvaluate.isEmpty) reporter.warning("No ground functions found with the given names")
-    
-    val eval = new CodeGenEvaluator(ctx, program)
-    //val eval = new DefaultEvaluator(ctx, program)
+
+    val eval = if (evaluator == "codegen") {
+      new CodeGenEvaluator(ctx, program)
+    } else if (evaluator == "default" || evaluator == "") {
+      new DefaultEvaluator(ctx, program)
+    } else {
+      reporter.fatalError(s"Unknown evaluator '$evaluator'. Available: default, codegen")
+    }
+
     for (fd <- toEvaluate) {
       reporter.info(s" - Evaluating ${fd.id}")
       val call = FunctionInvocation(fd.typedWithDef, Seq())