diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index b9b3e20067f53acdedace7eea6b634a3647eb01d..47903f24f8f180c671f6241444c8dcdee85f73ae 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -181,15 +181,12 @@ trait Definitions { self: Trees =>
val flags: Set[ClassFlag]) extends ClassDef {
val isAbstract = true
- def descendants(implicit s: Symbols): Seq[ClassDef] = children
+ def descendants(implicit s: Symbols): Seq[CaseClassDef] = children
.map(id => s.getClass(id) match {
case ccd: CaseClassDef => ccd
case _ => throw NotWellFormedException(id, s)
})
- def ccDescendants(implicit s: Symbols): Seq[CaseClassDef] =
- descendants collect { case ccd: CaseClassDef => ccd }
-
def isInductive(implicit s: Symbols): Boolean = {
def induct(tpe: Type, seen: Set[ClassDef]): Boolean = tpe match {
case ct: ClassType =>
@@ -206,7 +203,7 @@ trait Definitions { self: Trees =>
}
if (this == root && !this.isAbstract) false
- else ccDescendants.exists { ccd =>
+ else descendants.exists { ccd =>
ccd.fields.exists(vd => induct(vd.getType, Set(root)))
}
}
@@ -275,7 +272,6 @@ trait Definitions { self: Trees =>
case class TypedAbstractClassDef(cd: AbstractClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
def descendants: Seq[TypedClassDef] = cd.descendants.map(_.typed(tps))
- def ccDescendants: Seq[TypedCaseClassDef] = cd.ccDescendants.map(_.typed(tps))
}
case class TypedCaseClassDef(cd: CaseClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 472d68a17a299fc64c82d69120da0b550a611d84..b8d259cd1821f33319e46b0067e5f552371c3a6a 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -276,7 +276,7 @@ trait Expressions { self: Trees =>
// Hacky, but ok
def optionType(implicit s: Symbols) = s.getFunction(id, tps).returnType.asInstanceOf[ClassType]
def optionChildren(implicit s: Symbols): (ClassType, ClassType) = {
- val children = optionType.tcd.asInstanceOf[TypedAbstractClassDef].ccDescendants.sortBy(_.fields.size)
+ val children = optionType.tcd.asInstanceOf[TypedAbstractClassDef].descendants.sortBy(_.fields.size)
val Seq(noneType, someType) = children.map(_.toType)
(noneType, someType)
}
diff --git a/src/main/scala/inox/ast/GenTreeOps.scala b/src/main/scala/inox/ast/GenTreeOps.scala
index c87ea98dc6ee25ccfb2f2fad0871396b5b66f7fb..7e179f003d468a1f1086aba2bc4d880209565229 100644
--- a/src/main/scala/inox/ast/GenTreeOps.scala
+++ b/src/main/scala/inox/ast/GenTreeOps.scala
@@ -232,7 +232,7 @@ trait GenTreeOps {
val Deconstructor(es, builder) = e
val newEss = es.map(rec)
- val newVs: Seq[SubTree] = leon.utils.SeqUtils.cartesianProduct(newEss).map { newEs =>
+ val newVs: Seq[SubTree] = SeqUtils.cartesianProduct(newEss).map { newEs =>
if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
builder(newEs).copiedFrom(e)
} else {
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 19202719bfc7ffb22935d03379a5b7b27a1c2298..889a31a190b70de955fc05475f462e3c58e28244 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -447,7 +447,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
}
val tcds = tcd match {
- case tacd: TypedAbstractClassDef => tacd.ccDescendants
+ case tacd: TypedAbstractClassDef => tacd.descendants
case tccd: TypedCaseClassDef => Seq(tccd)
}
@@ -476,7 +476,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
val tccd @ TypedCaseClassDef(cd, tps) = tcd match {
case tacd: TypedAbstractClassDef =>
- tacd.ccDescendants.filter(hasInstance(_)).sortBy(_.fields.size).head
+ tacd.descendants.filter(hasInstance(_)).sortBy(_.fields.size).head
case tccd: TypedCaseClassDef => tccd
}
@@ -534,7 +534,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
case Some(tccd: TypedCaseClassDef) =>
cartesianProduct(tccd.fieldsTypes map valuesOf) map (CaseClass(ct, _))
case Some(accd: TypedAbstractClassDef) =>
- interleave(accd.ccDescendants.map(tccd => valuesOf(tccd.toType)))
+ interleave(accd.descendants.map(tccd => valuesOf(tccd.toType)))
case None => throw ClassLookupException(ct.id)
}
}
diff --git a/src/main/scala/inox/ast/TypeOps.scala b/src/main/scala/inox/ast/TypeOps.scala
index 5f294f6c753db2f2b8f63900b5e6d7a2ef398957..d02ceb26c94abf0f67246df4985ad39833e6c61b 100644
--- a/src/main/scala/inox/ast/TypeOps.scala
+++ b/src/main/scala/inox/ast/TypeOps.scala
@@ -245,17 +245,17 @@ trait TypeOps {
Set(tpe) ++ (tpe match {
case ct: ClassType => ct.tcd match {
case tccd: TypedCaseClassDef => tccd.fieldsTypes
- case tacd: TypedAbstractClassDef => (Set(tacd) ++ tacd.ccDescendants).map(_.toType)
+ case tacd: TypedAbstractClassDef => (Set(tacd) ++ tacd.descendants).map(_.toType)
}
case _ => Set.empty
})
)
- })(accd.ccDescendants.map(_.toType).toSet)
+ })(accd.descendants.map(_.toType).toSet)
if (possibleChildTypes(accd.toType)) {
None
} else {
- cards(accd.ccDescendants.map(_.toType)).map(_.sum)
+ cards(accd.descendants.map(_.toType)).map(_.sum)
}
}
case _ => None
diff --git a/src/main/scala/inox/solvers/SolverUnsupportedError.scala b/src/main/scala/inox/solvers/SolverUnsupportedError.scala
deleted file mode 100644
index 48acc71f478f53fd6326d35bd850044a54f91868..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/SolverUnsupportedError.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Common.Tree
-
-object SolverUnsupportedError {
- def msg(t: Tree, s: Solver, reason: Option[String]) = {
- s"(of ${t.getClass}) is unsupported by solver ${s.name}" + reason.map(":\n " + _ ).getOrElse("")
- }
-}
-
-case class SolverUnsupportedError(t: Tree, s: Solver, reason: Option[String] = None)
- extends Unsupported(t, SolverUnsupportedError.msg(t,s,reason))(s.context)