From ca2a7b6b6ef0565e61d15e0c6a9372cfc0c91ffd Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 8 Jan 2016 16:19:12 +0100
Subject: [PATCH] Label -> NonTerminal. Remove view bounds from Grammars
---
.../scala/leon/grammars/DepthBoundedGrammar.scala | 4 ++--
src/main/scala/leon/grammars/EmbeddedGrammar.scala | 2 +-
src/main/scala/leon/grammars/Empty.scala | 4 ++--
src/main/scala/leon/grammars/ExpressionGrammar.scala | 2 +-
src/main/scala/leon/grammars/Grammars.scala | 2 +-
.../leon/grammars/{Label.scala => NonTerminal.scala} | 2 +-
src/main/scala/leon/grammars/Or.scala | 2 +-
src/main/scala/leon/grammars/SimilarTo.scala | 12 ++++++------
.../scala/leon/grammars/SizeBoundedGrammar.scala | 4 ++--
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 2 ++
.../scala/leon/synthesis/rules/BottomUpTegis.scala | 2 +-
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 2 +-
src/main/scala/leon/synthesis/rules/CEGLESS.scala | 6 +++---
src/main/scala/leon/synthesis/rules/TEGISLike.scala | 2 +-
src/main/scala/leon/synthesis/rules/TEGLESS.scala | 6 +++---
15 files changed, 28 insertions(+), 26 deletions(-)
rename src/main/scala/leon/grammars/{Label.scala => NonTerminal.scala} (71%)
diff --git a/src/main/scala/leon/grammars/DepthBoundedGrammar.scala b/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
index 7ec864e03..fc999be64 100644
--- a/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
+++ b/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
@@ -3,8 +3,8 @@
package leon
package grammars
-case class DepthBoundedGrammar[T](g: ExpressionGrammar[Label[T]], bound: Int) extends ExpressionGrammar[Label[T]] {
- def computeProductions(l: Label[T])(implicit ctx: LeonContext): Seq[Gen] = g.computeProductions(l).flatMap {
+case class DepthBoundedGrammar[T](g: ExpressionGrammar[NonTerminal[T]], bound: Int) extends ExpressionGrammar[NonTerminal[T]] {
+ def computeProductions(l: NonTerminal[T])(implicit ctx: LeonContext): Seq[Gen] = g.computeProductions(l).flatMap {
case gen =>
if (l.depth == Some(bound) && gen.subTrees.nonEmpty) {
Nil
diff --git a/src/main/scala/leon/grammars/EmbeddedGrammar.scala b/src/main/scala/leon/grammars/EmbeddedGrammar.scala
index bcee19b01..8dcbc6ec1 100644
--- a/src/main/scala/leon/grammars/EmbeddedGrammar.scala
+++ b/src/main/scala/leon/grammars/EmbeddedGrammar.scala
@@ -12,7 +12,7 @@ import purescala.Constructors._
*
* We rely on a bijection between Li and Lo labels
*/
-case class EmbeddedGrammar[Ti <% Typed, To <% Typed](innerGrammar: ExpressionGrammar[Ti], iToo: Ti => To, oToi: To => Ti) extends ExpressionGrammar[To] {
+case class EmbeddedGrammar[Ti <: Typed, To <: Typed](innerGrammar: ExpressionGrammar[Ti], iToo: Ti => To, oToi: To => Ti) extends ExpressionGrammar[To] {
def computeProductions(t: To)(implicit ctx: LeonContext): Seq[Gen] = {
innerGrammar.computeProductions(oToi(t)).map { innerGen =>
nonTerminal(innerGen.subTrees.map(iToo), innerGen.builder)
diff --git a/src/main/scala/leon/grammars/Empty.scala b/src/main/scala/leon/grammars/Empty.scala
index 56b332309..70ebddc98 100644
--- a/src/main/scala/leon/grammars/Empty.scala
+++ b/src/main/scala/leon/grammars/Empty.scala
@@ -3,8 +3,8 @@
package leon
package grammars
-import purescala.Types._
+import purescala.Types.Typed
-case class Empty[T <% Typed]() extends ExpressionGrammar[T] {
+case class Empty[T <: Typed]() extends ExpressionGrammar[T] {
def computeProductions(t: T)(implicit ctx: LeonContext): Seq[Gen] = Nil
}
diff --git a/src/main/scala/leon/grammars/ExpressionGrammar.scala b/src/main/scala/leon/grammars/ExpressionGrammar.scala
index 465904f5d..01a3524d1 100644
--- a/src/main/scala/leon/grammars/ExpressionGrammar.scala
+++ b/src/main/scala/leon/grammars/ExpressionGrammar.scala
@@ -11,7 +11,7 @@ import purescala.Common._
import scala.collection.mutable.{HashMap => MutableMap}
-abstract class ExpressionGrammar[T <% Typed] {
+abstract class ExpressionGrammar[T <: Typed] {
type Gen = Generator[T, Expr]
private[this] val cache = new MutableMap[T, Seq[Gen]]()
diff --git a/src/main/scala/leon/grammars/Grammars.scala b/src/main/scala/leon/grammars/Grammars.scala
index 2194aa539..23b1dd5a1 100644
--- a/src/main/scala/leon/grammars/Grammars.scala
+++ b/src/main/scala/leon/grammars/Grammars.scala
@@ -24,7 +24,7 @@ object Grammars {
default(sctx.program, p.as.map(_.toVariable), sctx.functionContext, sctx.settings.functionsToIgnore, p.ws, p.pc)
}
- def typeDepthBound[T <% Typed](g: ExpressionGrammar[T], b: Int) = {
+ def typeDepthBound[T <: Typed](g: ExpressionGrammar[T], b: Int) = {
g.filter(g => g.subTrees.forall(t => typeDepth(t.getType) <= b))
}
}
diff --git a/src/main/scala/leon/grammars/Label.scala b/src/main/scala/leon/grammars/NonTerminal.scala
similarity index 71%
rename from src/main/scala/leon/grammars/Label.scala
rename to src/main/scala/leon/grammars/NonTerminal.scala
index aaaaccf30..7492ffac5 100644
--- a/src/main/scala/leon/grammars/Label.scala
+++ b/src/main/scala/leon/grammars/NonTerminal.scala
@@ -5,7 +5,7 @@ package grammars
import purescala.Types._
-case class Label[T](t: TypeTree, l: T, depth: Option[Int] = None) extends Typed {
+case class NonTerminal[T](t: TypeTree, l: T, depth: Option[Int] = None) extends Typed {
val getType = t
override def asString(implicit ctx: LeonContext) = t.asString+"#"+l+depth.map(d => "@"+d).getOrElse("")
diff --git a/src/main/scala/leon/grammars/Or.scala b/src/main/scala/leon/grammars/Or.scala
index ae0bc9697..e691a2459 100644
--- a/src/main/scala/leon/grammars/Or.scala
+++ b/src/main/scala/leon/grammars/Or.scala
@@ -5,7 +5,7 @@ package grammars
import purescala.Types._
-case class Union[T <% Typed](gs: Seq[ExpressionGrammar[T]]) extends ExpressionGrammar[T] {
+case class Union[T <: Typed](gs: Seq[ExpressionGrammar[T]]) extends ExpressionGrammar[T] {
val subGrammars: Seq[ExpressionGrammar[T]] = gs.flatMap {
case u: Union[T] => u.subGrammars
case g => Seq(g)
diff --git a/src/main/scala/leon/grammars/SimilarTo.scala b/src/main/scala/leon/grammars/SimilarTo.scala
index c134546d2..77e912792 100644
--- a/src/main/scala/leon/grammars/SimilarTo.scala
+++ b/src/main/scala/leon/grammars/SimilarTo.scala
@@ -13,7 +13,7 @@ import purescala.Expressions._
import synthesis._
-case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[Label[String]] {
+case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[NonTerminal[String]] {
val excludeFCalls = sctx.settings.functionsToIgnore
@@ -23,11 +23,11 @@ case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisConte
OneOf(terminals.toSeq :+ e) ||
FunctionCalls(sctx.program, sctx.functionContext, p.as.map(_.getType), excludeFCalls) ||
SafeRecursiveCalls(sctx.program, p.ws, p.pc),
- { (t: TypeTree) => Label(t, "B", None)},
- { (l: Label[String]) => l.getType }
+ { (t: TypeTree) => NonTerminal(t, "B", None)},
+ { (l: NonTerminal[String]) => l.getType }
), 1)
- type L = Label[String]
+ type L = NonTerminal[String]
val getNext: () => Int = {
var counter = -1
@@ -41,7 +41,7 @@ case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisConte
def computeProductions(t: L)(implicit ctx: LeonContext): Seq[Gen] = {
t match {
- case Label(_, "B", _) => normalGrammar.computeProductions(t)
+ case NonTerminal(_, "B", _) => normalGrammar.computeProductions(t)
case _ =>
val allSimilar = similarCache.getOrElse {
@@ -59,7 +59,7 @@ case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisConte
def getLabel(t: TypeTree) = {
val tpe = bestRealType(t)
val c = getNext()
- Label(tpe, "G"+c)
+ NonTerminal(tpe, "G"+c)
}
def isCommutative(e: Expr) = e match {
diff --git a/src/main/scala/leon/grammars/SizeBoundedGrammar.scala b/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
index 8756b136a..1b25e30f6 100644
--- a/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
+++ b/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
@@ -6,13 +6,13 @@ package grammars
import purescala.Types._
import leon.utils.SeqUtils.sumTo
-case class SizedLabel[T <% Typed](underlying: T, size: Int) extends Typed {
+case class SizedLabel[T <: Typed](underlying: T, size: Int) extends Typed {
val getType = underlying.getType
override def asString(implicit ctx: LeonContext) = underlying.asString+"|"+size+"|"
}
-case class SizeBoundedGrammar[T <% Typed](g: ExpressionGrammar[T]) extends ExpressionGrammar[SizedLabel[T]] {
+case class SizeBoundedGrammar[T <: Typed](g: ExpressionGrammar[T]) extends ExpressionGrammar[SizedLabel[T]] {
def computeProductions(sl: SizedLabel[T])(implicit ctx: LeonContext): Seq[Gen] = {
if (sl.size <= 0) {
Nil
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 3d39ae7e7..c975fd2d3 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -137,6 +137,8 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
private val freeVars = new IncrementalSet[Identifier]()
private val constraints = new IncrementalSeq[Expr]()
+ val tr = implicitly[Z3AST => Printable]
+
val unrollingBank = new UnrollingBank(context, templateGenerator)
private val incrementals: List[IncrementalState] = List(
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index 990be35e1..97b810ac3 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -26,7 +26,7 @@ case object BottomUpTEGIS extends BottomUpTEGISLike[TypeTree]("BU TEGIS") {
def getRootLabel(tpe: TypeTree): TypeTree = tpe
}
-abstract class BottomUpTEGISLike[T <% Typed](name: String) extends Rule(name) {
+abstract class BottomUpTEGISLike[T <: Typed](name: String) extends Rule(name) {
def getGrammar(sctx: SynthesisContext, p: Problem): ExpressionGrammar[T]
def getRootLabel(tpe: TypeTree): T
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 4824d3e53..d577f7f9f 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -22,7 +22,7 @@ import evaluators._
import datagen._
import codegen.CodeGenParams
-abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
+abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
case class CegisParams(
grammar: ExpressionGrammar[T],
diff --git a/src/main/scala/leon/synthesis/rules/CEGLESS.scala b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
index 6b0bbdd15..e2e8c9fab 100644
--- a/src/main/scala/leon/synthesis/rules/CEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
@@ -11,7 +11,7 @@ import utils._
import grammars._
import Witnesses._
-case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
+case object CEGLESS extends CEGISLike[NonTerminal[String]]("CEGLESS") {
def getParams(sctx: SynthesisContext, p: Problem) = {
val TopLevelAnds(clauses) = p.ws
@@ -30,11 +30,11 @@ case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
}
}
- val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[Label[String]]](Empty())(_ || _)
+ val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[NonTerminal[String]]](Empty())(_ || _)
CegisParams(
grammar = guidedGrammar,
- rootLabel = { (tpe: TypeTree) => Label(tpe, "G0") },
+ rootLabel = { (tpe: TypeTree) => NonTerminal(tpe, "G0") },
maxUnfoldings = (0 +: guides.map(depth(_) + 1)).max
)
}
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
index 2e9da57ce..164e396be 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -17,7 +17,7 @@ import scala.collection.mutable.{HashMap => MutableMap}
import bonsai.enumerators._
-abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
+abstract class TEGISLike[T <: Typed](name: String) extends Rule(name) {
case class TegisParams(
grammar: ExpressionGrammar[T],
rootLabel: TypeTree => T,
diff --git a/src/main/scala/leon/synthesis/rules/TEGLESS.scala b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
index d8de10cbb..f56b26b26 100644
--- a/src/main/scala/leon/synthesis/rules/TEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
@@ -10,7 +10,7 @@ import utils._
import Witnesses._
import grammars._
-case object TEGLESS extends TEGISLike[Label[String]]("TEGLESS") {
+case object TEGLESS extends TEGISLike[NonTerminal[String]]("TEGLESS") {
def getParams(sctx: SynthesisContext, p: Problem) = {
val TopLevelAnds(clauses) = p.ws
@@ -28,11 +28,11 @@ case object TEGLESS extends TEGISLike[Label[String]]("TEGLESS") {
}
}
- val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[Label[String]]](Empty())(_ || _)
+ val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[NonTerminal[String]]](Empty())(_ || _)
TegisParams(
grammar = guidedGrammar,
- rootLabel = { (tpe: TypeTree) => Label(tpe, "G0") }
+ rootLabel = { (tpe: TypeTree) => NonTerminal(tpe, "G0") }
)
}
}
--
GitLab