From 4150a2a946184b183da0114b32ee4acfe6be73eb Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 27 May 2015 12:44:31 +0200
Subject: [PATCH] Evaluator option --eval takes evaluator as argument
---
src/main/scala/leon/Main.scala | 7 +++----
src/main/scala/leon/SharedOptions.scala | 3 +++
.../scala/leon/evaluators/EvaluationPhase.scala | 14 +++++++++++---
3 files changed, 17 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index b7a734523..4d525fbcb 100644
--- a/src/main/scala/leon/Main.scala
+++ b/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()
}
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
index 49f480985..5c2cce35e 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/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
)
}
diff --git a/src/main/scala/leon/evaluators/EvaluationPhase.scala b/src/main/scala/leon/evaluators/EvaluationPhase.scala
index 7f163a747..13c5418ae 100644
--- a/src/main/scala/leon/evaluators/EvaluationPhase.scala
+++ b/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())
--
GitLab