From c1f957b545361d995bd20e796de525548f03c3fd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Wed, 20 Jan 2016 14:18:55 +0100
Subject: [PATCH] Added example simplification when asking questions.
---
src/main/scala/leon/purescala/ExprOps.scala | 6 ++++++
.../leon/synthesis/disambiguation/QuestionBuilder.scala | 5 ++++-
2 files changed, 10 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 51dd63d33..e6c87698c 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1440,6 +1440,12 @@ object ExprOps {
case Minus(Plus(e1, e2), Plus(e3, e4)) if e1 == e4 && e2 == e3 => InfiniteIntegerLiteral(0)
case Minus(Plus(e1, e2), Plus(Plus(e3, e4), e5)) if e1 == e4 && e2 == e3 => UMinus(e5)
+ case StringConcat(StringLiteral(""), a) => a
+ case StringConcat(a, StringLiteral("")) => a
+ case StringConcat(StringLiteral(a), StringLiteral(b)) => StringLiteral(a+b)
+ case StringConcat(StringLiteral(a), StringConcat(StringLiteral(b), c)) => StringConcat(StringLiteral(a+b), c)
+ case StringConcat(StringConcat(c, StringLiteral(a)), StringLiteral(b)) => StringConcat(c, StringLiteral(a+b))
+ case StringConcat(a, StringConcat(b, c)) => StringConcat(StringConcat(a, b), c)
//default
case e => e
}).copiedFrom(expr)
diff --git a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
index be10ff008..c66b1e846 100644
--- a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
@@ -136,7 +136,10 @@ class QuestionBuilder[T <: Expr](
val model = new ModelBuilder
model ++= elems
val modelResult = model.result()
- e.eval(s.term, modelResult).result.map(_._1)
+ for{x <- e.eval(s.term, modelResult).result
+ res = x._1
+ simp = ExprOps.simplifyArithmetic(res)}
+ yield simp
}
/** Returns a list of input/output questions to ask to the user. */
--
GitLab