From ac385ce59932da0ab4762fe884bcc340fe8568ca Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 1 Jul 2015 17:27:14 +0200
Subject: [PATCH] Make this more readable
---
.../scala/leon/synthesis/SynthesisPhase.scala | 43 +++++++++----------
1 file changed, 21 insertions(+), 22 deletions(-)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 3deeae2f0..31327bf8a 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -33,33 +33,32 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
if (ms.isDefined && timeout.isDefined) {
ctx.reporter.warning("Defining timeout with manual search")
}
+ val costModel = {
+ ctx.findOption(optCostModel) match {
+ case None => CostModels.default
+ case Some(name) => CostModels.all.find(_.name.toLowerCase == name.toLowerCase) getOrElse {
+ var errorMsg = "Unknown cost model: " + name + "\n" +
+ "Defined cost models: \n"
+
+ for (cm <- CostModels.all.toSeq.sortBy(_.name)) {
+ errorMsg += " - " + cm.name + (if (cm == CostModels.default) " (default)" else "") + "\n"
+ }
+
+ ctx.reporter.fatalError(errorMsg)
+ }
+ }
+ }
+
SynthesisSettings(
- manualSearch = ms,
- functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet },
timeoutMs = timeout map { _ * 1000 },
generateDerivationTrees = ctx.findOptionOrDefault(optDerivTrees),
+ costModel = costModel,
+ rules = Rules.all ++ (ms map { _ => rules.AsChoose}),
+ manualSearch = ms,
+ functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet },
cegisUseOptTimeout = ctx.findOption(optCEGISOptTimeout),
cegisUseShrink = ctx.findOption(optCEGISShrink),
- cegisUseVanuatoo = ctx.findOption(optCEGISVanuatoo),
- rules = Rules.all ++ (ms map { _ => rules.AsChoose}),
- costModel = {
- ctx.findOption(optCostModel) match {
- case None => CostModels.default
- case Some(name) => CostModels.all.find(_.name.toLowerCase == name.toLowerCase) match {
- case Some(model) => model
- case None =>
- var errorMsg = "Unknown cost model: " + name + "\n" +
- "Defined cost models: \n"
-
- for (cm <- CostModels.all.toSeq.sortBy(_.name)) {
- errorMsg += " - " + cm.name + (if (cm == CostModels.default) " (default)" else "") + "\n"
- }
-
- ctx.reporter.fatalError(errorMsg)
- }
-
- }
- }
+ cegisUseVanuatoo = ctx.findOption(optCEGISVanuatoo)
)
}
--
GitLab