From 0cb1ea618fd2af34281b71bfa4fa020d59b5d8db Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Mon, 7 Dec 2015 21:43:36 +0100
Subject: [PATCH] Removing the body of the function when adding examples.
---
.../synthesis/disambiguation/ExamplesAdder.scala | 8 ++++++++
.../leon/synthesis/disambiguation/Question.scala | 2 +-
.../synthesis/disambiguation/QuestionBuilder.scala | 10 +++++-----
.../scala/leon/synthesis/rules/StringRender.scala | 14 +++-----------
testcases/stringrender/GrammarRender.scala | 3 +++
5 files changed, 20 insertions(+), 17 deletions(-)
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index 31463d4e7..109cd677d 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -40,6 +40,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
} }
if(i == -1) {
fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), and(post, Passes(inputVariables, Variable(id), newCases))))
+ ctx0.reporter.info("No top-level passes in postcondition, adding it: " + fd)
} else {
val newPasses = exprs(i) match {
case Passes(in, out, cases) =>
@@ -48,14 +49,21 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
}
val newPost = and(exprs.updated(i, newPasses) : _*)
fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), newPost))
+ ctx0.reporter.info("Adding the example to the passes postcondition: " + fd)
}
}
} else {
fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), and(post, Passes(inputVariables, Variable(id), newCases))))
+ ctx0.reporter.info("No passes in postcondition, adding it:" + fd)
}
case None =>
val id = FreshIdentifier("res", fd.returnType, false)
fd.postcondition = Some(Lambda(Seq(ValDef(id, None)), Passes(inputVariables, Variable(id), newCases)))
+ ctx0.reporter.info("No postcondition, adding it: " + fd)
+ }
+ fd.body match { // TODO: Is it correct to discard the choose construct inside the body?
+ case Some(Choose(Lambda(Seq(ValDef(id, tpe)), bodyChoose))) => fd.body = Some(Hole(id.getType, Nil))
+ case _ =>
}
}
diff --git a/src/main/scala/leon/synthesis/disambiguation/Question.scala b/src/main/scala/leon/synthesis/disambiguation/Question.scala
index 4074b0abe..eed7bfc1a 100644
--- a/src/main/scala/leon/synthesis/disambiguation/Question.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/Question.scala
@@ -6,4 +6,4 @@ import purescala.Expressions.Expr
/**
* @author Mikael
*/
-case class Question[T <: Expr](inputs: List[Expr], current_output: T, other_outputs: List[T])
\ No newline at end of file
+case class Question[T <: Expr](inputs: Seq[Expr], current_output: T, other_outputs: List[T])
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
index cb29b9b19..08d2daabc 100644
--- a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
@@ -83,7 +83,7 @@ object QuestionBuilder {
* @return An ordered
*
*/
-class QuestionBuilder[T <: Expr](input: List[Identifier], ruleApplication: RuleClosed, filter: Expr => Option[T])(implicit c: LeonContext, p: Program) {
+class QuestionBuilder[T <: Expr](input: Seq[Identifier], solutions: Stream[Solution], filter: Expr => Option[T])(implicit c: LeonContext, p: Program) {
import QuestionBuilder._
private var _argTypes = input.map(_.getType)
private var _questionSorMethod: QuestionSortingType = QuestionSortingType.IncreasingInputSize
@@ -113,7 +113,7 @@ class QuestionBuilder[T <: Expr](input: List[Identifier], ruleApplication: RuleC
/** Returns a list of input/output questions to ask to the user. */
def result(): List[Question[T]] = {
- if(ruleApplication.solutions.isEmpty) return Nil
+ if(solutions.isEmpty) return Nil
val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions)
val values = enum.iterator(tupleTypeWrap(_argTypes))
@@ -123,8 +123,8 @@ class QuestionBuilder[T <: Expr](input: List[Identifier], ruleApplication: RuleC
val enumerated_inputs = instantiations.take(expressionsToTake).toList
- val solution = ruleApplication.solutions.head
- val alternatives = ruleApplication.solutions.drop(1).take(solutionsToTake).toList
+ val solution = solutions.head
+ val alternatives = solutions.drop(1).take(solutionsToTake).toList
val questions = ListBuffer[Question[T]]()
for{possible_input <- enumerated_inputs
current_output_nonfiltered <- run(solution, possible_input)
@@ -136,7 +136,7 @@ class QuestionBuilder[T <: Expr](input: List[Identifier], ruleApplication: RuleC
if alternative_output != current_output
} yield alternative_output_filtered).distinct
if(alternative_outputs.nonEmpty) {
- questions += Question(possible_input.map(_._2), current_output, alternative_outputs.sortWith((e,f) => _alternativeSortMethod.compare(e, f) < 0))
+ questions += Question(possible_input.map(_._2), current_output, alternative_outputs.sortWith((e,f) => _alternativeSortMethod.compare(e, f) <= 0))
}
}
questions.toList.sortBy(_questionSorMethod(_))
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index c088c2018..30ef401de 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, (expr: Expr) => expr match {
+ val qb = new disambiguation.QuestionBuilder(input, r.solutions, (expr: Expr) => expr match {
case s@StringLiteral(slv) if !slv.contains(EDIT_ME) => Some(s)
case _ => None
})
@@ -257,7 +257,7 @@ case object StringRender extends Rule("StringRender") {
}
val funName3 = funName2.replaceAll("[^a-zA-Z0-9_]","")
val funName = funName3(0).toLower + funName3.substring(1)
- val funId = FreshIdentifier(funName, alwaysShowUniqueID = false)
+ val funId = FreshIdentifier(funName, alwaysShowUniqueID = true)
val argId= FreshIdentifier(tpe.typeToConvert.asString(hctx.context).toLowerCase()(0).toString, tpe.typeToConvert)
val fd = new FunDef(funId, Nil, ValDef(argId) :: Nil, StringType) // Empty function.
fd
@@ -425,15 +425,7 @@ case object StringRender extends Rule("StringRender") {
))
hctx.reporter.debug("Inferred expression:\n" + expr + toDebug)
- val res = findSolutions(examples, expr, funDefs.values.toSeq)
- res match {
- case r: RuleClosed =>
- val questions = askQuestion(p.as, r)(hctx.context, hctx.program)
- println("Questions:")
- println(questions.map(q => "For (" + q.inputs.mkString(", ") + "), res = " + q.current_output + ", could also be " + q.other_outputs.toSet.map((s: StringLiteral) => s.asString).mkString(",")).mkString("\n"))
- case _ =>
- }
- res
+ findSolutions(examples, expr, funDefs.values.toSeq)
}
ruleInstantiations.toList
diff --git a/testcases/stringrender/GrammarRender.scala b/testcases/stringrender/GrammarRender.scala
index 59928dceb..f0c1e5929 100644
--- a/testcases/stringrender/GrammarRender.scala
+++ b/testcases/stringrender/GrammarRender.scala
@@ -238,4 +238,7 @@ S0 -> S0 t1"""
def synthesizePlainTextRules(s: Grammar): String = {
???[String]
} ensuring psPlainTextRules(s)
+
+ def allGrammarsAreIdentical(g: Grammar, g2: Grammar) = (g == g2 || g.rules == g2.rules) holds
+
}
\ No newline at end of file
--
GitLab