From 101707b6482bd213efea81e97bc82436eda6390d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 9 Jul 2015 17:18:35 +0200
Subject: [PATCH] Correct typo
---
src/main/scala/leon/datagen/NaiveDataGen.scala | 2 +-
src/main/scala/leon/datagen/VanuatooDataGen.scala | 2 +-
src/main/scala/leon/purescala/Definitions.scala | 8 ++++----
src/main/scala/leon/purescala/ExprOps.scala | 4 ++--
src/main/scala/leon/purescala/MethodLifting.scala | 8 ++++----
src/main/scala/leon/purescala/Types.scala | 4 ++--
src/main/scala/leon/solvers/ADTManager.scala | 2 +-
.../scala/leon/solvers/smtlib/SMTLIBSolver.scala | 2 +-
.../scala/leon/solvers/z3/AbstractZ3Solver.scala | 2 +-
.../scala/leon/synthesis/PartialSolution.scala | 6 +++---
.../scala/leon/synthesis/graph/DotGenerator.scala | 2 +-
src/main/scala/leon/synthesis/graph/Graph.scala | 14 +++++++-------
src/main/scala/leon/synthesis/graph/Search.scala | 14 +++++++-------
.../scala/leon/synthesis/rules/ADTInduction.scala | 4 ++--
.../leon/synthesis/rules/ADTLongInduction.scala | 4 ++--
src/main/scala/leon/synthesis/rules/ADTSplit.scala | 2 +-
.../leon/synthesis/utils/ExpressionGrammar.scala | 8 ++++----
.../scala/leon/termination/ChainComparator.scala | 2 +-
.../scala/leon/termination/StructuralSize.scala | 2 +-
src/main/scala/leon/utils/TypingPhase.scala | 2 +-
.../scala/leon/verification/InductionTactic.scala | 4 ++--
.../scala/leon/test/synthesis/SynthesisSuite.scala | 4 ++--
22 files changed, 51 insertions(+), 51 deletions(-)
diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index 9726d1876..394993520 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 c4100ceef..013b8d870 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 6841dccc7..149940742 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 778c0679c..41276c204 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 e87c332e9..5f41bc811 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 54e633e08..bbd1884d0 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 2ea69dd3f..96c8ad60b 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 9b78a1fbb..a261fc10c 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 9d57eb723..e3fd1fbc4 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 774e76254..d3443db76 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 2db8025dc..e44496a2d 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 c4e13648b..aac4d2fd2 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 501004cfa..9f1726d98 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 c493a540e..45509bdb7 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 bdf0f4cf7..3f39582e3 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 111757777..a57cdfb15 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 8e6fec782..0aad97735 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 16d4cb460..a3ab3f8f4 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 6e0bed6c0..99b3c18f6 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 ec5d8048d..0f47e61ac 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 7bbd332c6..8ce88e490 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 b8ef5681f..35c7d6f6e 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
}
--
GitLab