Skip to content
Snippets Groups Projects
Commit e230f2b0 authored by Régis Blanc's avatar Régis Blanc
Browse files

testcase for finite sort, with 3 elements

parent 77a19904
No related branches found
No related tags found
No related merge requests found
import leon.Utils._
object FiniteSort {
def sort3(x1: Int, x2: Int, x3: Int): (Int, Int, Int) = {
choose((z1: Int, z2: Int, z3: Int) =>
z1 <= z2 && z2 <= z3 && (
(z1 == x1 && z2 == x2 && z3 == x3) ||
(z1 == x1 && z2 == x3 && z3 == x2) ||
(z1 == x2 && z2 == x1 && z3 == x3) ||
(z1 == x2 && z2 == x3 && z3 == x1) ||
(z1 == x3 && z2 == x1 && z3 == x2) ||
(z1 == x3 && z2 == x2 && z3 == x1)
)
)
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment