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

Fix choose not returning a stable type, add constructor to help

parent ad6aeaa2
Branches
Tags
No related merge requests found
...@@ -24,4 +24,12 @@ object Constructors { ...@@ -24,4 +24,12 @@ object Constructors {
case xs => case xs =>
LetTuple(xs, value, body) LetTuple(xs, value, body)
} }
def tupleChoose(ch: Choose): Expr = {
if (ch.vars.size > 1) {
ch
} else {
Tuple(Seq(ch))
}
}
} }
...@@ -63,7 +63,7 @@ object ConvertHoles extends LeonPhase[Program, Program] { ...@@ -63,7 +63,7 @@ object ConvertHoles extends LeonPhase[Program, Program] {
BooleanLiteral(true) BooleanLiteral(true)
} }
val withChoose = letTuple(holes, Choose(cids, pred), newBody) val withChoose = letTuple(holes, tupleChoose(Choose(cids, pred)), newBody)
fd.body = Some(withChoose) fd.body = Some(withChoose)
} }
......
...@@ -54,7 +54,7 @@ object ConvertWithOracle extends LeonPhase[Program, Program] { ...@@ -54,7 +54,7 @@ object ConvertWithOracle extends LeonPhase[Program, Program] {
BooleanLiteral(true) BooleanLiteral(true)
} }
Some(letTuple(os, Choose(chooseOs, pred), b)) Some(letTuple(os, tupleChoose(Choose(chooseOs, pred)), b))
case None => case None =>
None None
} }
......
...@@ -3,26 +3,6 @@ import leon.collection._ ...@@ -3,26 +3,6 @@ import leon.collection._
import leon.lang.synthesis._ import leon.lang.synthesis._
object Holes { object Holes {
def abs1(a: Int) = {
if (?(true, false)) {
a
} else {
-a
}
} ensuring {
_ >= 0
}
def abs2(a: Int) = {
if (???[Boolean]) {
a
} else {
-a
}
} ensuring {
_ >= 0
}
def abs3(a: Int) = { def abs3(a: Int) = {
if (?(a > 0, a < 0)) { if (?(a > 0, a < 0)) {
a a
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment