Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Filling DP table in order
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) + ?)
}
@ravimad
Copy link

ravimad commented May 13, 2016

? * (expr) is extracted differently. So it will work

@ravimad
Copy link

ravimad commented May 13, 2016

However, the benchmark still doesn't work. Try increasing UNROLL_BOund in the file leon.invaraint.engine.RefinementEngine

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment