From 4797228669c5c657d3fe58c557c1c00ef7853a73 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Fri, 4 Dec 2015 18:55:34 +0100
Subject: [PATCH] Adding a function to find questions when returning a
solution.
---
.../leon/synthesis/rules/StringRender.scala | 33 +++++++++++++++++++
1 file changed, 33 insertions(+)
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 4153edee5..93e0a7b23 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -28,6 +28,8 @@ import leon.solvers.string.StringSolver
import scala.annotation.tailrec
import leon.purescala.DefOps
import leon.programsets.{UnionProgramSet, DirectProgramSet, JoinProgramSet}
+import bonsai.enumerators.MemoizedEnumerator
+import leon.grammars.ValueGrammar
/** A template generator for a given type tree.
@@ -181,6 +183,37 @@ case object StringRender extends Rule("StringRender") {
solutionStreamToRuleApplication(p, leon.utils.StreamUtils.interleave(tagged_solutions))
}
+ case class Question(input: Expr, current_output: String, other_outputs: Set[String])
+
+ /** Find ambiguities not containing _edit_me_ to ask to the user */
+ def askQuestion(argType: TypeTree, r: RuleClosed)(implicit c: LeonContext): List[Question] = {
+ if(r.solutions.isEmpty) return Nil
+ val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions)
+ val iter = enum.iterator(argType)
+ def run(s: Solution, elem: Expr): String = ???
+
+ val iterated = iter.take(15).toList
+
+ val solution = r.solutions.head
+ val alternatives = r.solutions.drop(1).take(15)
+ val questions = ListBuffer[Question]()
+ for(elem <- iterated) {
+ val current_output = run(solution, elem)
+ var possible_outputs = Set[String]()
+ for(alternative <- alternatives) {
+ run(alternative, elem) match {
+ case s if !s.contains("_edit_me_") && s != current_output => possible_outputs += s
+ case _ =>
+ }
+ }
+ if(possible_outputs.nonEmpty) {
+ questions += Question(elem, current_output, possible_outputs)
+ }
+ }
+ questions.toList.sortBy(question => ExprOps.count(e => 1)(question.input))
+ } //TODO: Need to ask these questions to the user, but in the background. Loop by adding new examples. Test with list.
+
+ /** Converts the stream of solutions to a RuleApplication */
def solutionStreamToRuleApplication(p: Problem, solutions: Stream[(Seq[(FunDef, WithIds[Expr])], WithIds[Expr], Assignment)]): RuleApplication = {
if(solutions.isEmpty) RuleFailed() else {
RuleClosed(
--
GitLab