Skip to content
Snippets Groups Projects
Commit eef2b813 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Simplify val hole = choose(); ... hole for single holes

parent b8da1b14
Branches
Tags
No related merge requests found
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment