From 4f601d017f11a7001e042884b058b9f8ad1beb0f Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 4 Apr 2016 15:19:18 +0200
Subject: [PATCH] DepthBound aspect
---
.../leon/grammars/aspects/DepthBound.scala | 23 +++++++++++++++++++
1 file changed, 23 insertions(+)
create mode 100644 src/main/scala/leon/grammars/aspects/DepthBound.scala
diff --git a/src/main/scala/leon/grammars/aspects/DepthBound.scala b/src/main/scala/leon/grammars/aspects/DepthBound.scala
new file mode 100644
index 000000000..b694b5403
--- /dev/null
+++ b/src/main/scala/leon/grammars/aspects/DepthBound.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package grammars
+package aspects
+
+/** Limits a grammar by depth */
+case class DepthBound(depth: Int) extends Aspect {
+ require(depth >= 0)
+
+ def asString(implicit ctx: LeonContext): String = s"D$depth"
+
+ def applyTo(l: Label, ps: Seq[Production])(implicit ctx: LeonContext) = {
+ if (depth == 0) Nil
+ else if (depth == 1) ps.filter(_.isTerminal)
+ else {
+ ps map { prod =>
+ prod.copy(subTrees = prod.subTrees.map(_.withAspect(DepthBound(depth - 1))))
+ }
+ }
+ }
+
+}
--
GitLab