diff --git a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala index e356d40bb5db668e1487792231d2b6b9dd6bd2c5..a33b71ca435123c3ee8de9385bde72528a26b1b3 100644 --- a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala +++ b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala @@ -81,10 +81,15 @@ object QuestionBuilder { * @param input The identifier of the unique function's input. Must be typed or the type should be defined by setArgumentType * @param ruleApplication The set of solutions for the body of f * @param filter A function filtering which outputs should be considered for comparison. + * It takes as input the sequence of outputs already considered for comparison, and the new output. + * It should return Some(result) if the result can be shown, and None else. * @return An ordered * */ -class QuestionBuilder[T <: Expr](input: Seq[Identifier], solutions: Stream[Solution], filter: Expr => Option[T])(implicit c: LeonContext, p: Program) { +class QuestionBuilder[T <: Expr]( + input: Seq[Identifier], + solutions: Stream[Solution], + filter: (Seq[T], Expr) => Option[T])(implicit c: LeonContext, p: Program) { import QuestionBuilder._ private var _argTypes = input.map(_.getType) private var _questionSorMethod: QuestionSortingType = QuestionSortingType.IncreasingInputSize @@ -132,13 +137,19 @@ class QuestionBuilder[T <: Expr](input: Seq[Identifier], solutions: Stream[Solut val questions = ListBuffer[Question[T]]() for{possible_input <- enumerated_inputs current_output_nonfiltered <- run(solution, possible_input) - current_output <- filter(current_output_nonfiltered)} { - val alternative_outputs = ( - for{alternative <- alternatives - alternative_output <- run(alternative, possible_input) - alternative_output_filtered <- filter(alternative_output) - if alternative_output != current_output - } yield alternative_output_filtered).distinct + current_output <- filter(Seq(), current_output_nonfiltered)} { + + val alternative_outputs = ((ListBuffer[T](current_output) /: alternatives) { (prev, alternative) => + run(alternative, possible_input) match { + case Some(alternative_output) if alternative_output != current_output => + filter(prev, alternative_output) match { + case Some(alternative_output_filtered) => + prev += alternative_output_filtered + case _ => prev + } + case _ => prev + } + }).drop(1).toList.distinct if(alternative_outputs.nonEmpty || keepEmptyAlternativeQuestions(current_output)) { questions += Question(possible_input.map(_._2), current_output, alternative_outputs.sortWith((e,f) => _alternativeSortMethod.compare(e, f) <= 0)) } diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala index d5c0b21e64e7f846fc5f829b0f6e5b10065fbf9f..5c393ad4ced2026ca5cea966fdbcc175a53153b1 100644 --- a/src/main/scala/leon/synthesis/rules/StringRender.scala +++ b/src/main/scala/leon/synthesis/rules/StringRender.scala @@ -189,7 +189,7 @@ case object StringRender extends Rule("StringRender") { /** Find ambiguities not containing _edit_me_ to ask to the user */ def askQuestion(input: List[Identifier], r: RuleClosed)(implicit c: LeonContext, p: Program): List[disambiguation.Question[StringLiteral]] = { //if !s.contains(EDIT_ME) - val qb = new disambiguation.QuestionBuilder(input, r.solutions, (expr: Expr) => expr match { + val qb = new disambiguation.QuestionBuilder(input, r.solutions, (seq: Seq[Expr], expr: Expr) => expr match { case s@StringLiteral(slv) if !slv.contains(EDIT_ME) => Some(s) case _ => None })