Skip to content

Commit

Permalink
test CT speedup
Browse files Browse the repository at this point in the history
  • Loading branch information
breandan committed Apr 13, 2024
1 parent 95ecfaa commit 47d19fe
Show file tree
Hide file tree
Showing 4 changed files with 50 additions and 16 deletions.
8 changes: 5 additions & 3 deletions build.gradle.kts
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
import io.github.gradlenexus.publishplugin.NexusPublishExtension
import org.gradle.api.tasks.testing.logging.TestExceptionFormat.FULL
import org.gradle.api.tasks.testing.logging.TestLogEvent.*
import org.jetbrains.kotlin.gradle.dsl.JvmTarget
import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
import org.jetbrains.kotlin.gradle.targets.js.nodejs.*

Expand Down Expand Up @@ -80,7 +81,7 @@ repositories {
val javadocJar by tasks.registering(Jar::class) { archiveClassifier = "javadoc" }

rootProject.plugins.withType<NodeJsRootPlugin> {
rootProject.the<NodeJsRootExtension>().nodeVersion = "16.0.0"
rootProject.the<NodeJsRootExtension>().version = "16.0.0"
}

kotlin {
Expand Down Expand Up @@ -256,7 +257,7 @@ kotlin {

tasks {
withType<KotlinCompile> {
kotlinOptions.jvmTarget = "17"
compilerOptions.jvmTarget = JvmTarget.JVM_17
}

withType<Test> {
Expand Down Expand Up @@ -286,7 +287,8 @@ tasks {

listOf(
"Rewriter", "PrefAttach",
"rewriting.CipherSolver", "RegexDemo", "smt.TestSMT",
"rewriting.CipherSolver",
"RegexDemo", "smt.TestSMT"
).forEach { fileName ->
register(fileName, org.gradle.api.tasks.JavaExec::class) {
mainClass = "ai.hypergraph.kaliningraph.${fileName}Kt"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ typealias TSA = Set<Arc>
fun Arc.pretty() = "$π1 -<$π2>-> $π3"
fun Σᐩ.coords(): Pair<Int, Int> =
(length / 2 - 1).let { substring(2, it + 2).toInt() to substring(it + 3).toInt() }
// Triple representing (1) the global index of the state in the LA and the (2) x, (3) y coordinates
typealias STC = Triple<Int, Int, Int>
fun STC.coords() = π2 to π3

Expand Down Expand Up @@ -38,6 +39,14 @@ open class FSA(open val Q: TSA, open val init: Set<Σᐩ>, open val final: Set<
val stateCoords: Sequence<STC> by lazy { states.map { it.coords().let { (i, j) -> Triple(stateMap[it]!!, i, j) } }.asSequence() }

val validTriples by lazy { stateCoords.let { it * it * it }.filter { it.isValidStateTriple() }.toList() }
val validPairs by lazy { stateCoords.let { it * it }.filter { it.isValidStatePair() }.toSet() }

fun Π2A<STC>.isValidStatePair(): Boolean {
fun Pair<Int, Int>.dominates(other: Pair<Int, Int>) =
first <= other.first && second <= other.second

return first.coords().dominates(second.coords())
}

fun Π3A<STC>.isValidStateTriple(): Boolean {
fun Pair<Int, Int>.dominates(other: Pair<Int, Int>) =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -51,20 +51,27 @@ private infix fun CFG.intersectLevFSAP(fsa: FSA): CFG {

// For each production A → BC in P, for every p, q, r ∈ Q,
// we have the production [p,A,r] → [p,B,q] [q,C,r] in P′.
val prods = nonterminalProductions
.map { (a, b) -> ntMap[a]!! to b.map { ntMap[it]!! } }.toSet()
val prods: Set<Pair<Int, List<Int>>> = nonterminalProductions
.map { (a, bc) -> ntMap[a]!! to bc.map { ntMap[it]!! } }.toSet()
val lengthBoundsCache = lengthBounds.let { lb -> ntLst.map { lb[it] ?: 0..0 } }
val validTriples: List<Triple<STC, STC, STC>> = fsa.validTriples

val ct = prods.map { it.first }.toSet().flatMap { fsa.validPairs * setOf(it) }
val ct1: Map<Triple<Int, Int, Int>, Boolean> =
ct.associate { Pair(it.π11 to it.π3 to it.π21, lengthBoundsCache[it.π3].overlaps(fsa.SPLP(it.π1, it.π2))) }
val ct2: Map<Triple<Int, Int, Int>, Boolean> =
ct.associate { Pair(it.π11 to it.π3 to it.π21, fsa.obeys(it.π1, it.π2, it.π3, parikhMap)) }

val binaryProds =
prods.map {
// if (i % 100 == 0) println("Finished ${i}/${nonterminalProductions.size} productions")
val (A, B, C) = it.π1 to it.π2[0] to it.π2[1]
validTriples
// CFG ∩ FSA - in general we are not allowed to do this, but it works
// because we assume a Levenshtein FSA, which is monotone and acyclic.
.filter { it.isCompatibleWith(A to B to C, fsa, lengthBoundsCache) }
.filter { it.obeysLevenshteinParikhBounds(A to B to C, fsa, parikhMap) }
.filter { it.checkCT(A to B to C, ct1) }
.filter { it.checkCT(A to B to C, ct2) }
// .filter { it.obeysLevenshteinParikhBounds(A to B to C, fsa, parikhMap) }
.map { (a, b, c) ->
val (p, q, r) = fsa.stateLst[a.π1] to fsa.stateLst[b.π1] to fsa.stateLst[c.π1]
"[$p~${ntLst[A]}~$r]".also { nts.add(it) } to listOf("[$p~${ntLst[B]}~$q]", "[$q~${ntLst[C]}~$r]")
Expand Down Expand Up @@ -247,7 +254,7 @@ fun Π3A<STC>.isValidStateTriple(): Boolean {
// && obeys(second, third, nts.third)
//}

private fun FSA.obeys(a: STC, b: STC, nt: Int, parikhMap: ParikhMap): Bln {
fun FSA.obeys(a: STC, b: STC, nt: Int, parikhMap: ParikhMap): Bln {
val sl = levString.size <= max(a.second, b.second) // Part of the LA that handles extra

if (sl) return true
Expand All @@ -268,15 +275,20 @@ private fun manhattanDistance(first: Pair<Int, Int>, second: Pair<Int, Int>): In
(second.second - first.second).absoluteValue + (second.first - first.first).absoluteValue

// Range of the shortest path to the longest path, i.e., Manhattan distance
private fun FSA.SPLP(a: STC, b: STC) =
fun FSA.SPLP(a: STC, b: STC) =
(APSP[a.π1 to b.π1] ?: Int.MAX_VALUE)..//.also { /*if (Random.nextInt(100000) == 3) if(it == Int.MAX_VALUE) println("Miss! ${hash(a.π1, b.π1)} / ${a.first} / ${b.first}") else */
// if (it != Int.MAX_VALUE) println("Hit: ${hash(a.π1, b.π1)} / ${a.first} / ${b.first}") }..
manhattanDistance(a.coords(), b.coords())

private fun IntRange.overlaps(other: IntRange) =
fun IntRange.overlaps(other: IntRange) =
(other.first in first..last) || (other.last in first..last)

fun Π3A<STC>.isCompatibleWith(nts: Π3A<Int>, fsa: FSA, lengthBounds: List<IntRange>): Boolean =
lengthBounds[nts.first].overlaps(fsa.SPLP(first, third))
&& lengthBounds[nts.second].overlaps(fsa.SPLP(first, second))
&& lengthBounds[nts.third].overlaps(fsa.SPLP(second, third))
&& lengthBounds[nts.third].overlaps(fsa.SPLP(second, third))

fun Π3A<STC>.checkCT(nts: Π3A<Int>, ct: Map<Π3A<Int>, Boolean>): Boolean =
true == ct[π11 to nts.π1 to π31] &&
true == ct[π11 to nts.π2 to π21] &&
true == ct[π21 to nts.π3 to π31]
Original file line number Diff line number Diff line change
Expand Up @@ -167,9 +167,19 @@ private fun CFG.jvmIntersectLevFSAP(fsa: FSA, parikhMap: ParikhMap): CFG {
// we have the production [p,A,r] → [p,B,q] [q,C,r] in P′.
val prods = nonterminalProductions
.map { (a, b) -> ntMap[a]!! to b.map { ntMap[it]!! } }.toSet()
val lengthBoundsCache = lengthBounds.let { lb -> ntLst.map { lb[it] ?: 0..0 } }
val lengthBoundsCache = lengthBounds.let { lb -> nonterminals.map { lb[it] ?: 0..0 } }
val validTriples: List<Triple<STC, STC, STC>> = fsa.validTriples

val ct = (fsa.validPairs * nonterminals.indices.toSet()).toList()
val ct1: Map<Triple<Int, Int, Int>, Boolean> = ct.parallelStream()
.filter { lengthBoundsCache[it.π3].overlaps(fsa.SPLP(it.π1, it.π2)) }
.map { Pair(it.π11 to it.π3 to it.π21, true) }
.collect(Collectors.toMap({ it.first }, { it.second }))
val ct2: Map<Triple<Int, Int, Int>, Boolean> = ct.parallelStream()
.filter { fsa.obeys(it.π1, it.π2, it.π3, parikhMap) }
.map { Pair(it.π11 to it.π3 to it.π21, true) }
.collect(Collectors.toMap({ it.first }, { it.second }))

val elimCounter = AtomicInteger(0)
val counter = AtomicInteger(0)
val lpClock = TimeSource.Monotonic.markNow()
Expand All @@ -180,11 +190,12 @@ private fun CFG.jvmIntersectLevFSAP(fsa: FSA, parikhMap: ParikhMap): CFG {
validTriples.stream()
// CFG ∩ FSA - in general we are not allowed to do this, but it works
// because we assume a Levenshtein FSA, which is monotone and acyclic.
.filter { it.isCompatibleWith(A to B to C, fsa, lengthBoundsCache).also { if (!it) elimCounter.incrementAndGet() } }
.filter { it.obeysLevenshteinParikhBounds(A to B to C, fsa, parikhMap).also { if (!it) elimCounter.incrementAndGet() } }
// .filter { it.isCompatibleWith(A to B to C, fsa, lengthBoundsCache).also { if (!it) elimCounter.incrementAndGet() } }
.filter { it.checkCT(A to B to C, ct1).also { if (!it) elimCounter.incrementAndGet() } }
// .filter { it.obeysLevenshteinParikhBounds(A to B to C, fsa, parikhMap).also { if (!it) elimCounter.incrementAndGet() } }
.filter { it.checkCT(A to B to C, ct2).also { if (!it) elimCounter.incrementAndGet() } }
.map { (a, b, c) ->
if (MAX_PRODS < counter.incrementAndGet())
throw Exception("∩-grammar has too many productions! (>$MAX_PRODS)")
if (MAX_PRODS < counter.incrementAndGet()) throw Exception("∩-grammar has too many productions! (>$MAX_PRODS)")
val (p, q, r) = fsa.stateLst[a.π1] to fsa.stateLst[b.π1] to fsa.stateLst[c.π1]
"[$p~${ntLst[A]}~$r]".also { nts.add(it) } to listOf("[$p~${ntLst[B]}~$q]", "[$q~${ntLst[C]}~$r]")
}
Expand Down

0 comments on commit 47d19fe

Please sign in to comment.