diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala index 04892e750e63afc33b5a7a3ba193f1b93797cae6..19a975ed266b2edc069403d7310a66a9fc1c9e4d 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 1cb409d6e992d186aab86c5e9cea7ef35607c653..0d2701dbe20dec1a84c0cfe5e61ff01958653094 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 a460f03dc453ea750d3c7b86099bef60d901acb2..177d21c49bbfcb6fd4d8e804aaf1647e1405d17a 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 )