Last active
May 13, 2016 15:19
-
-
Save Sumith1896/979cf662c7833783376e4226a4cff12f to your computer and use it in GitHub Desktop.
Filling DP table in order
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
package wihtOrb | |
import leon._ | |
import mem._ | |
import lang._ | |
import annotation._ | |
import com.sun.xml.internal.bind.v2.runtime.reflect.Lister.Pack | |
import instrumentation._ | |
import invariant._ | |
object orderedFill { | |
def fillTable(i: BigInt, j: BigInt, m: BigInt, n: BigInt): BigInt = { | |
require(i >= 0 && j >= 0 && m >= i && n >= j) | |
if (i == m && j == n) | |
BigInt(0) | |
else if(j == n) | |
fillTable(i + 1, 0, m, n) | |
else | |
fillTable(i, j + 1, m, n) | |
} ensuring (time <= ? * (m - i) * n + ? * (n - j) + ?) | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
However, the benchmark still doesn't work. Try increasing UNROLL_BOund in the file leon.invaraint.engine.RefinementEngine