diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index 9726d1876529d0717113a07823eeee2c11a7cb2b..3949935200be25d5c219e1752ea1b197c173ed02 100644
--- a/src/main/scala/leon/datagen/NaiveDataGen.scala
+++ b/src/main/scala/leon/datagen/NaiveDataGen.scala
@@ -55,7 +55,7 @@ class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds :
// We prioritize base cases among the children.
// Otherwise we run the risk of infinite recursion when
// generating lists.
- val ccChildren = act.knownCCDescendents
+ val ccChildren = act.knownCCDescendants
val (leafs,conss) = ccChildren.partition(_.fields.isEmpty)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index c4100ceef464368de733a11ca9b67f2a5c3226b4..013b8d870a287abf716900f1d98a92650fa3f0f5 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -134,7 +134,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
case act: AbstractClassType =>
constructors.getOrElse(act, {
- val cs = act.knownCCDescendents.map {
+ val cs = act.knownCCDescendants.map {
cct => getConstructorFor(cct, act)
}.toList
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 6841dccc776ffcaee7d92e4144a777adfe0ead74..149940742fd55824e2295f0ad11590c646f418d3 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -138,7 +138,7 @@ object Definitions {
// Guarantees that a parent always appears before its children
def classHierarchies = classHierarchyRoots map { root =>
- root +: root.knownDescendents
+ root +: root.knownDescendants
}
def singleCaseClasses = {
@@ -225,14 +225,14 @@ object Definitions {
def knownChildren: Seq[ClassDef] = _children
- def knownDescendents: Seq[ClassDef] = {
+ def knownDescendants: Seq[ClassDef] = {
knownChildren ++ knownChildren.flatMap {
- case acd: AbstractClassDef => acd.knownDescendents
+ case acd: AbstractClassDef => acd.knownDescendants
case _ => Nil
}
}
- def knownCCDescendents: Seq[CaseClassDef] = knownDescendents.collect {
+ def knownCCDescendants: Seq[CaseClassDef] = knownDescendants.collect {
case ccd: CaseClassDef =>
ccd
}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 778c0679c85556ffb547aef153bdde232839d9da..41276c20412ab4464aa8cbb7a1123dbdd37681cc 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1244,7 +1244,7 @@ object ExprOps {
def isInductiveOn(sf: SolverFactory[Solver])(expr: Expr, on: Identifier): Boolean = on match {
case IsTyped(origId, AbstractClassType(cd, tps)) =>
- val toCheck = cd.knownDescendents.collect {
+ val toCheck = cd.knownDescendants.collect {
case ccd: CaseClassDef =>
val cct = CaseClassType(ccd, tps)
@@ -1465,7 +1465,7 @@ object ExprOps {
def typesOf(tpe: TypeTree): Set[CaseClassDef] = tpe match {
case AbstractClassType(ctp, _) =>
- ctp.knownDescendents.collect { case c: CaseClassDef => c }.toSet
+ ctp.knownDescendants.collect { case c: CaseClassDef => c }.toSet
case CaseClassType(ctd, _) =>
Set(ctd)
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index e87c332e9598c4ab3c46e64031f2508b7a13b36e..5f41bc81188ae93ea5384341b535abf0a1ec53dd 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -139,7 +139,7 @@ object MethodLifting extends TransformationPhase {
nfd.setPos(fd)
nfd.addFlag(IsMethod(cd))
- if (cd.knownDescendents.forall( _.methods.forall(_.id != fd.id))) {
+ if (cd.knownDescendants.forall( _.methods.forall(_.id != fd.id))) {
val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
// Don't need to compose methods
nfd.fullBody = postMap {
@@ -153,16 +153,16 @@ object MethodLifting extends TransformationPhase {
/* (Type) parameter substitutions that look at all subclasses */
val paramsMap = (for {
- c <- cd.knownDescendents :+ cd
+ c <- cd.knownDescendants :+ cd
m <- c.methods if m.id == fd.id
(from,to) <- m.params zip fdParams
} yield (from.id, to.id)).toMap
val classParamsMap = (for {
- c <- cd.knownDescendents :+ cd
+ c <- cd.knownDescendants :+ cd
(from, to) <- c.tparams zip ctParams
} yield (from, to.tp)).toMap
val methodParamsMap = (for {
- c <- cd.knownDescendents :+ cd
+ c <- cd.knownDescendants :+ cd
m <- c.methods if m.id == fd.id
(from,to) <- m.tparams zip fd.tparams
} yield (from, to.tp)).toMap
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 54e633e08bfa893178d984d9d1ab12925452a630..bbd1884d071c32c25c2ff6aa03fc3f288abbe1ab 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -93,9 +93,9 @@ object Types {
}
}
- def knownDescendents = classDef.knownDescendents.map( _.typed(tps) )
+ def knownDescendants = classDef.knownDescendants.map( _.typed(tps) )
- def knownCCDescendents = classDef.knownCCDescendents.map( _.typed(tps) )
+ def knownCCDescendants = classDef.knownCCDescendants.map( _.typed(tps) )
lazy val fieldsTypes = fields.map(_.getType)
diff --git a/src/main/scala/leon/solvers/ADTManager.scala b/src/main/scala/leon/solvers/ADTManager.scala
index 2ea69dd3ff585c2ee2e7b41c12d9e212df0fca0e..96c8ad60b762c76775cc3c7b21ae5171aa8cd710 100644
--- a/src/main/scala/leon/solvers/ADTManager.scala
+++ b/src/main/scala/leon/solvers/ADTManager.scala
@@ -28,7 +28,7 @@ class ADTManager(ctx: LeonContext) {
getHierarchy(p)
case None => (ct, ct match {
case act: AbstractClassType =>
- act.knownCCDescendents
+ act.knownCCDescendants
case cct: CaseClassType =>
List(cct)
})
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 9b78a1fbb57eb43652bcc4283c932047e80e2cce..a261fc10c38cf8b9ab3adfd3fba4b1b25e000526 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -331,7 +331,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
declareSort(cct)
val cases = cct match {
case act: AbstractClassType =>
- act.knownCCDescendents
+ act.knownCCDescendants
case cct: CaseClassType =>
Seq(cct)
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 9d57eb723046037bd5887af621b8783b2b24b5cd..e3fd1fbc472cde897fe90916666c18e4fe09172d 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -468,7 +468,7 @@ trait AbstractZ3Solver
selector(rec(cc))
case IsInstanceOf(act: AbstractClassType, e) =>
- act.knownCCDescendents match {
+ act.knownCCDescendants match {
case Seq(cct) =>
rec(IsInstanceOf(cct, e))
case more =>
diff --git a/src/main/scala/leon/synthesis/PartialSolution.scala b/src/main/scala/leon/synthesis/PartialSolution.scala
index 774e76254bcd50017e4a9ad161671a61d2257e8e..d3443db76c73e403ca287f754a07a0c6c0f060f1 100644
--- a/src/main/scala/leon/synthesis/PartialSolution.scala
+++ b/src/main/scala/leon/synthesis/PartialSolution.scala
@@ -30,7 +30,7 @@ class PartialSolution(g: Graph, includeUntrusted: Boolean = false) {
solveWith(on.parent, sol)
case Some(an: AndNode) =>
- val ssols = for (d <- an.descendents) yield {
+ val ssols = for (d <- an.descendants) yield {
if (d == n) {
sol
} else {
@@ -66,7 +66,7 @@ class PartialSolution(g: Graph, includeUntrusted: Boolean = false) {
}
if (n.isExpanded) {
- val descs = on.descendents.filterNot(_.isDeadEnd)
+ val descs = on.descendants.filterNot(_.isDeadEnd)
if (descs.isEmpty) {
completeProblem(on.p)
} else {
@@ -86,7 +86,7 @@ class PartialSolution(g: Graph, includeUntrusted: Boolean = false) {
}
if (n.isExpanded) {
- an.ri.onSuccess(n.descendents.map(getSolutionFor)) match {
+ an.ri.onSuccess(n.descendants.map(getSolutionFor)) match {
case Some(sol) =>
sol
diff --git a/src/main/scala/leon/synthesis/graph/DotGenerator.scala b/src/main/scala/leon/synthesis/graph/DotGenerator.scala
index 2db8025dc1c2bbda6c65800ffc7cc7f272042313..e44496a2de7feb1a6936af8e49a62a86e140c21a 100644
--- a/src/main/scala/leon/synthesis/graph/DotGenerator.scala
+++ b/src/main/scala/leon/synthesis/graph/DotGenerator.scala
@@ -117,7 +117,7 @@ class DotGenerator(g: Graph) {
}
private def collectEdges(from: Node): Set[(Node, Node)] = {
- from.descendents.flatMap { d =>
+ from.descendants.flatMap { d =>
Set(from -> d) ++ collectEdges(d)
}.toSet
}
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index c4e13648b9d2071c0ce41208b42850b2bdb0d336..aac4d2fd2cc06805cf1c623e4e599337d31ca24e 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -17,7 +17,7 @@ sealed class Graph(val cm: CostModel, problem: Problem) {
if (!from.isExpanded) {
self
} else {
- from.descendents.foldLeft(self) {
+ from.descendants.foldLeft(self) {
case ((c,t), d) =>
val (sc, st) = getStats(d)
(c+sc, t+st)
@@ -28,7 +28,7 @@ sealed class Graph(val cm: CostModel, problem: Problem) {
sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
var parents: List[Node] = parent.toList
- var descendents: List[Node] = Nil
+ var descendants: List[Node] = Nil
// indicates whether this particular node has already been expanded
var isExpanded: Boolean = false
@@ -75,7 +75,7 @@ sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
case None =>
val costs = if (isExpanded) {
- Some(descendents.map { _.cost })
+ Some(descendants.map { _.cost })
} else {
None
}
@@ -141,9 +141,9 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
info(prefix+" - "+p.asString)
}
- descendents = probs.map(p => new OrNode(cm, Some(this), p))
+ descendants = probs.map(p => new OrNode(cm, Some(this), p))
- selected = descendents
+ selected = descendants
updateCost()
}
@@ -162,7 +162,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
solveds += desc
// Everything is solved correctly
- if (solveds.size == descendents.size) {
+ if (solveds.size == descendants.size) {
isSolved = true
parents.foreach(_.onSolved(this))
}
@@ -198,7 +198,7 @@ class OrNode(cm: CostModel, parent: Option[Node], val p: Problem) extends Node(c
val ris = getInstantiations(hctx)
- descendents = ris.map(ri => new AndNode(cm, Some(this), ri))
+ descendants = ris.map(ri => new AndNode(cm, Some(this), ri))
selected = List()
updateCost()
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index 501004cfaceac30fdd04b0e5b9d701c4c75b0de1..9f1726d98c9c55d06484d88a81209814c63a6eaa 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/src/main/scala/leon/synthesis/graph/Search.scala
@@ -53,8 +53,8 @@ abstract class Search(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: C
case Nil =>
Some(n)
case x :: xs =>
- if (n.isExpanded && n.descendents.size > x) {
- traversePathFrom(n.descendents(x), xs)
+ if (n.isExpanded && n.descendants.size > x) {
+ traversePathFrom(n.descendants(x), xs)
} else {
None
}
@@ -92,11 +92,11 @@ class SimpleSearch(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: Cost
} else if (!n.isDeadEnd) {
n match {
case an: AndNode =>
- an.descendents.foreach(findIn)
+ an.descendants.foreach(findIn)
case on: OrNode =>
- if (on.descendents.nonEmpty) {
- findIn(on.descendents.minBy(_.cost))
+ if (on.descendants.nonEmpty) {
+ findIn(on.descendants.minBy(_.cost))
}
}
}
@@ -233,7 +233,7 @@ class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel
if (cd.isEmpty) {
println(title(pathToString(cd)+" \u2510 "+displayNode(n)))
- for ((sn, i) <- n.descendents.zipWithIndex) {
+ for ((sn, i) <- n.descendants.zipWithIndex) {
val sp = cd ::: List(i)
if (sn.isSolved) {
@@ -247,7 +247,7 @@ class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel
}
}
} else {
- displayPath(n.descendents(cd.head), cd.tail)
+ displayPath(n.descendants(cd.head), cd.tail)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index c493a540e3d88ab28d6677119bf88955c203ffe8..45509bdb78981d841a807b5a6ecece6a949bb8b8 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -33,7 +33,7 @@ case object ADTInduction extends Rule("ADT Induction") {
ct.fields.exists(_.getType == origId.getType)
}
- val isRecursive = ct.knownCCDescendents.exists(isAlternativeRecursive)
+ val isRecursive = ct.knownCCDescendants.exists(isAlternativeRecursive)
// Map for getting a formula in the context of within the recursive function
val substMap = residualMap + (origId -> Variable(inductOn))
@@ -44,7 +44,7 @@ case object ADTInduction extends Rule("ADT Induction") {
val innerPC = substAll(substMap, p.pc)
val innerWS = substAll(substMap, p.ws)
- val subProblemsInfo = for (cct <- ct.knownCCDescendents) yield {
+ val subProblemsInfo = for (cct <- ct.knownCCDescendants) yield {
var recCalls = Map[List[Identifier], List[Expr]]()
var postFs = List[Expr]()
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index bdf0f4cf7610019244e05c46b418e4df1cc1a014..3f39582e316b7ce686fc89eada8b0d90fec49b84 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -34,7 +34,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
ct.fields.exists(_.getType == origId.getType)
}
- val isRecursive = ct.knownCCDescendents.exists(isAlternativeRecursive)
+ val isRecursive = ct.knownCCDescendants.exists(isAlternativeRecursive)
// Map for getting a formula in the context of within the recursive function
val substMap = residualMap + (origId -> Variable(inductOn))
@@ -66,7 +66,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
val InductCase(ids, calls, pat, pc, trMap) = ic
(for (id <- ids if isRec(id)) yield {
- for (cct <- ct.knownCCDescendents) yield {
+ for (cct <- ct.knownCCDescendants) yield {
val subIds = cct.fields.map(vd => FreshIdentifier(vd.id.name, vd.getType, true)).toList
val newIds = ids.filterNot(_ == id) ++ subIds
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 1117577772616ad3909561903ec00364a47daaa9..a57cdfb155a24bd110be2b39297620fff03eddad 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -20,7 +20,7 @@ case object ADTSplit extends Rule("ADT Split.") {
val candidates = p.as.collect {
case IsTyped(id, act @ AbstractClassType(cd, tpes)) =>
- val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
+ val optCases = for (dcd <- cd.knownDescendants.sortBy(_.id.name)) yield dcd match {
case ccd : CaseClassDef =>
val cct = CaseClassType(ccd, tpes)
val toSat = and(p.pc, IsInstanceOf(cct, Variable(id)))
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index 8e6fec7829361303ec2b7987c9801ab22bb2a2d1..0aad97735d15c348d606801bf1e96eed66de1f8f 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -117,7 +117,7 @@ object ExpressionGrammars {
)
case act: AbstractClassType =>
- act.knownCCDescendents.map { cct =>
+ act.knownCCDescendants.map { cct =>
Generator[TypeTree, Expr](cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
}
@@ -181,7 +181,7 @@ object ExpressionGrammars {
)
case act: AbstractClassType =>
- act.knownCCDescendents.map { cct =>
+ act.knownCCDescendants.map { cct =>
Generator[TypeTree, Expr](cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
}
@@ -313,7 +313,7 @@ object ExpressionGrammars {
def ccVariations(gl: L, cc: CaseClass): Seq[(L, Gen)] = {
val CaseClass(cct, args) = cc
- val neighbors = cct.root.knownCCDescendents diff Seq(cct)
+ val neighbors = cct.root.knownCCDescendants diff Seq(cct)
for (scct <- neighbors if scct.fieldsTypes == cct.fieldsTypes) yield {
gl -> Generator[L, Expr](Nil, { _ => CaseClass(scct, args) })
@@ -466,7 +466,7 @@ object ExpressionGrammars {
def computeProductions(l: Label[T]): Seq[Gen] = g.computeProductions(l).flatMap {
case g: Generator[Label[T], Expr] =>
if (l.depth == Some(bound) && g.subTrees.nonEmpty) {
- None
+ None
} else if (l.depth.exists(_ > bound)) {
None
} else {
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index 16d4cb460319633a02998f583c4866849b0af89a..a3ab3f8f4fb40eac7871bc4eee73ec4bb3414213 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -17,7 +17,7 @@ trait ChainComparator { self : StructuralSize =>
def unapply(c: ClassType): Option[(CaseClassType, Seq[(Identifier, TypeTree)])] = c match {
case cct @ CaseClassType(ccd, _) =>
if (cct.fields.exists(arg => isSubtypeOf(arg.getType, cct.root))) None
- else if (ccd.hasParent && ccd.parent.get.knownDescendents.size > 1) None
+ else if (ccd.hasParent && ccd.parent.get.knownDescendants.size > 1) None
else Some((cct, cct.fields.map(arg => arg.id -> arg.getType)))
case _ => None
}
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 6e0bed6c082acecb7f95d556dff3b1f59df4c62c..99b3c18f66237796d0dfae14c9d24ebb06c26a3b 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -74,7 +74,7 @@ trait StructuralSize {
expr.getType match {
case (ct: ClassType) =>
val fd = funDef(ct, {
- case (act: AbstractClassType) => act.knownCCDescendents map caseClassType2MatchCase
+ case (act: AbstractClassType) => act.knownCCDescendants map caseClassType2MatchCase
case (cct: CaseClassType) => Seq(caseClassType2MatchCase(cct))
})
FunctionInvocation(TypedFunDef(fd, ct.tps), Seq(expr))
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index ec5d8048d20b7cb9693455b55036ff01ba71fa14..0f47e61ac0e8fa4d373e287f87160fd98e57673b 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -82,7 +82,7 @@ object TypingPhase extends LeonPhase[Program, Program] {
// Part (3)
pgm.definedClasses.foreach {
case acd: AbstractClassDef =>
- if (acd.knownCCDescendents.isEmpty) {
+ if (acd.knownCCDescendants.isEmpty) {
ctx.reporter.error(acd.getPos, "Class "+acd.id.asString(ctx)+" has no concrete descendant!")
}
case _ =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 7bbd332c617dcc45887d528e289119d09aff74a1..8ce88e490c507a53914acd29067088ed5a4a9d0f 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -30,7 +30,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
override def generatePostconditions(fd: FunDef): Seq[VC] = {
(fd.body, firstAbsClassDef(fd.params), fd.postcondition) match {
case (Some(body), Some((parentType, arg)), Some(post)) =>
- for (cct <- parentType.knownCCDescendents) yield {
+ for (cct <- parentType.knownCCDescendants) yield {
val selectors = selectorsOfParentType(parentType, cct, arg.toVariable)
val subCases = selectors.map { sel =>
@@ -66,7 +66,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
for {
((fi@FunctionInvocation(tfd, args), pre), path) <- calls
- cct <- parentType.knownCCDescendents
+ cct <- parentType.knownCCDescendants
} yield {
val selectors = selectorsOfParentType(parentType, cct, arg.toVariable)
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index b8ef5681f52ea8d138d5f76481d94bc365cdf9e2..35c7d6f6efd51aa19c0fa04623e5be9d74321e0a 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -39,7 +39,7 @@ class SynthesisSuite extends LeonTestSuite {
} else {
strat match {
case Decomp(_, sub) =>
- (an.descendents zip sub).forall {
+ (an.descendants zip sub).forall {
case (n, strat) => synthesizeFrom(sctx, n, strat)
}
case _ =>
@@ -50,7 +50,7 @@ class SynthesisSuite extends LeonTestSuite {
case on: OrNode =>
on.expand(SearchContext(sctx, ci, on, this))
- val ns = on.descendents.filter {
+ val ns = on.descendants.filter {
case an: AndNode => matchingDesc(an.ri, strat.ruleName)
case _ => false
}