From 0ff0f3be652cf7aa70f05920782d7cc11916be45 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 4 Jan 2013 17:17:48 +0100
Subject: [PATCH] Define WeightedBranches as default cost model
Improve error output by specifying which one is the default.
---
src/main/scala/leon/synthesis/CostModel.scala | 2 ++
src/main/scala/leon/synthesis/SynthesisPhase.scala | 9 ++++++---
src/main/scala/leon/synthesis/SynthesizerOptions.scala | 2 +-
3 files changed, 9 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index 04892e750..19a975ed2 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -25,6 +25,8 @@ abstract class CostModel(val name: String) {
}
object CostModel {
+ def default: CostModel = WeightedBranchesCostModel
+
def all: Set[CostModel] = Set(
NaiveCostModel,
WeightedBranchesCostModel
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 1cb409d6e..0d2701dbe 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -48,9 +48,12 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
options = options.copy(costModel = model)
case None =>
- val errorMsg = "Unknown cost model: " + cm + "\n" +
- "Defined cost models: \n" +
- (CostModel.all.map(_.name).mkString(" - ", "\n - ", ""))
+ var errorMsg = "Unknown cost model: " + cm + "\n" +
+ "Defined cost models: \n"
+
+ for (cm <- CostModel.all.toSeq.sortBy(_.name)) {
+ errorMsg += " - " + cm.name + (if(cm == CostModel.default) " (default)" else "") + "\n"
+ }
ctx.reporter.fatalError(errorMsg)
}
diff --git a/src/main/scala/leon/synthesis/SynthesizerOptions.scala b/src/main/scala/leon/synthesis/SynthesizerOptions.scala
index a460f03dc..177d21c49 100644
--- a/src/main/scala/leon/synthesis/SynthesizerOptions.scala
+++ b/src/main/scala/leon/synthesis/SynthesizerOptions.scala
@@ -7,5 +7,5 @@ case class SynthesizerOptions(
searchWorkers: Int = 1,
firstOnly: Boolean = false,
timeoutMs: Option[Long] = None,
- costModel: CostModel = NaiveCostModel
+ costModel: CostModel = CostModel.default
)
--
GitLab