diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala index 9d48defd51899f3f756ed6f8e16f5115f090748f..913ae4376721933527b1a54c6470af5c6741bd33 100644 --- a/src/main/scala/leon/synthesis/ExamplesBank.scala +++ b/src/main/scala/leon/synthesis/ExamplesBank.scala @@ -185,16 +185,16 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb: QualifiedExamplesBank(nas, xs, eb flatMapIns { (in: Seq[Expr]) => List(toKeep.map(in)) }) } + def evalIns: QualifiedExamplesBank = copy( eb = flatMapIns { mapping => + val evalAs = evaluator.evalEnv(mapping) + List(as map evalAs) + }) + /** Filter inputs through expr which is an expression evaluating to a boolean */ def filterIns(expr: Expr): QualifiedExamplesBank = { filterIns(m => evaluator.eval(expr, m).result.contains(BooleanLiteral(true))) } - def evalIns: QualifiedExamplesBank = flatMapIns { mapping => - val evalAs = evaluator.evalEnv(mapping) - List(as map evalAs) - } - /** Filters inputs through the predicate pred, with an assignment of input variables to expressions. */ def filterIns(pred: Map[Identifier, Expr] => Boolean): QualifiedExamplesBank = { QualifiedExamplesBank(as, xs, @@ -212,14 +212,14 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb: /** Maps inputs through the function f * * @return A new ExampleBank */ - def flatMapIns(f: Seq[(Identifier, Expr)] => List[Seq[Expr]]): QualifiedExamplesBank = { - copy(eb = eb flatMap { + def flatMapIns(f: Seq[(Identifier, Expr)] => List[Seq[Expr]]): ExamplesBank = { + eb flatMap { case InExample(in) => f(as zip in).map(InExample) case InOutExample(in, out) => f(as zip in).map(InOutExample(_, out)) - }) + } } } diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala index 379eaf59f63961256260cd2cae2a7c4c4a4c7d40..0c2e1e7e89e0c111afe0b16a7b8009afbca9fb32 100644 --- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala +++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala @@ -100,7 +100,7 @@ case object ADTSplit extends Rule("ADT Split.") { } } } else { - p.qeb + p.eb } } val newAs = if (isInputVar) args ::: oas else p.as