From eef2b813cd097e0109b193022c2c73ce9d084db6 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 19 Aug 2015 18:09:05 +0200
Subject: [PATCH] Simplify val hole = choose(); ... hole for single holes
---
src/main/scala/leon/synthesis/ConvertHoles.scala | 11 +++++++----
1 file changed, 7 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 4c27e9b96..543b37784 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -80,10 +80,13 @@ object ConvertHoles extends LeonPhase[Program, Program] {
val choose = Choose(spec)
+ val newBody = if (holes.size == 1) {
+ replaceFromIDs(Map(holes.head -> choose), withoutHoles)
+ } else {
+ letTuple(holes, choose, withoutHoles)
+ }
- val valuations = letTuple(holes, choose, withoutHoles)
-
- withPostcondition(withPrecondition(valuations, pre), post)
+ withPostcondition(withPrecondition(newBody, pre), post)
} else {
e
@@ -93,7 +96,7 @@ object ConvertHoles extends LeonPhase[Program, Program] {
}
}
-
+
def run(ctx: LeonContext)(pgm: Program): Program = {
pgm.definedFunctions.foreach(fd => fd.fullBody = convertHoles(fd.fullBody,ctx) )
pgm
--
GitLab