From 63d9ea287bd71688b830818007aea462923223c6 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 24 Oct 2016 09:33:15 +0200
Subject: [PATCH] Useful implicit conversion for definition flags
---
src/main/scala/inox/Main.scala | 2 +-
src/main/scala/inox/ast/Definitions.scala | 4 ++++
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/inox/Main.scala b/src/main/scala/inox/Main.scala
index e19602e40..490b78d7a 100644
--- a/src/main/scala/inox/Main.scala
+++ b/src/main/scala/inox/Main.scala
@@ -33,7 +33,7 @@ trait MainHelpers {
protected def getOptions: Map[OptionDef[_], String] = Map(
optTimeout -> "Set a timeout for each proof attempt (in sec.)",
optSelectedSolvers -> {
- "Use solvers s1, s2,...\nAvailable: " +
+ "Use solvers s1,s2,...\nAvailable: " +
solvers.SolverFactory.solverNames.toSeq.sortBy(_._1).map {
case (name, desc) => f"\n $name%-14s : $desc"
}
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index a9491af7c..86ef28e9d 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -178,6 +178,10 @@ trait Definitions { self: Trees =>
case _ => Annotation(name, args)
}
+ implicit class FlagSetWrapper(flags: Set[Flag]) {
+ def contains(str: String): Boolean = flags contains Annotation(str, Seq.empty)
+ }
+
/** Represents an ADT definition (either the ADT sort or a constructor). */
sealed trait ADTDefinition extends Definition {
val id: Identifier
--
GitLab