You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
164 lines
5.8 KiB
Kotlin
164 lines
5.8 KiB
Kotlin
package net.cijber.pubgrub
|
|
|
|
import net.cijber.pubgrub.packages.PackageSelection
|
|
import net.cijber.pubgrub.packages.PackageVersion
|
|
import net.cijber.pubgrub.stubs.PackageId
|
|
import net.cijber.pubgrub.stubs.PackageRetriever
|
|
import net.cijber.pubgrub.stubs.Version
|
|
import net.cijber.pubgrub.version.VersionRange
|
|
|
|
class Solver<P : PackageId, V : Version<V>>(
|
|
val packageRetriever: PackageRetriever<P, V>,
|
|
private val root: PackageVersion<P, V>
|
|
) {
|
|
private val incompatibilities: MutableMap<P, MutableList<Incompatibility<P, V>>> = mutableMapOf(
|
|
root.pkg to mutableListOf(
|
|
Incompatibility(
|
|
listOf(Term(PackageSelection(root.pkg, VersionRange.single(root.version)), true)),
|
|
IncompatibilityCause.Simple(IncompatibilityCause.SimpleCause.Root)
|
|
)
|
|
)
|
|
)
|
|
|
|
private val solution = PartialSolution<P, V>()
|
|
|
|
suspend fun solve() {
|
|
var next: P? = root.pkg
|
|
while (next != null) {
|
|
propagate(next)
|
|
next = choosePackageVersion()
|
|
}
|
|
}
|
|
|
|
private fun propagate(pkg: P) {
|
|
val changed = mutableSetOf(pkg)
|
|
|
|
while (changed.isNotEmpty()) {
|
|
val currentPkg = changed.first()
|
|
changed.remove(currentPkg)
|
|
|
|
for (incompat in incompatibilities.getOrPut(currentPkg, ::mutableListOf).reversed()) {
|
|
val result = propagateIncompatibility(incompat)
|
|
|
|
if (result == PropagationResult.Conflict) {
|
|
val rootCause = resolveConflict(incompat)
|
|
changed.clear()
|
|
@Suppress("UNCHECKED_CAST")
|
|
changed.add((propagateIncompatibility(rootCause) as? PropagationResult.Unsatisfied<P>)!!.pkg)
|
|
break
|
|
}
|
|
|
|
if (result is PropagationResult.Unsatisfied<*>) {
|
|
@Suppress("UNCHECKED_CAST")
|
|
changed.add(result.pkg as P)
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
private fun resolveConflict(incompat: Incompatibility<P, V>): Incompatibility<P, V> {
|
|
var workingIncompatibility = incompat
|
|
var newIncompatibility = false
|
|
while (!incompat.isFailure) {
|
|
var mostRecentTerm: Term<P, V>? = null
|
|
var mostRecentSatisfier: Assignment<P, V>? = null
|
|
var difference: Term<P, V>? = null
|
|
|
|
var previousSatisfierLevel = 1
|
|
|
|
for (term in workingIncompatibility.terms) {
|
|
val satisfier = solution.satisfier(term)
|
|
|
|
if (mostRecentSatisfier == null) {
|
|
mostRecentTerm = term
|
|
mostRecentSatisfier = satisfier
|
|
} else if (mostRecentSatisfier.index < satisfier.index) {
|
|
previousSatisfierLevel = maxOf(previousSatisfierLevel, mostRecentSatisfier.decisionLevel)
|
|
mostRecentTerm = term;
|
|
mostRecentSatisfier = satisfier;
|
|
difference = null;
|
|
} else {
|
|
previousSatisfierLevel = maxOf(previousSatisfierLevel, satisfier.decisionLevel)
|
|
}
|
|
|
|
if (mostRecentTerm == term) {
|
|
difference = mostRecentSatisfier.difference(mostRecentTerm)
|
|
if (difference != null) {
|
|
previousSatisfierLevel = maxOf(
|
|
previousSatisfierLevel,
|
|
solution.satisfier(difference.inverse).decisionLevel
|
|
)
|
|
}
|
|
}
|
|
}
|
|
|
|
if (previousSatisfierLevel < mostRecentSatisfier!!.decisionLevel ||
|
|
mostRecentSatisfier.cause == null
|
|
) {
|
|
solution.backtrack(previousSatisfierLevel);
|
|
if (newIncompatibility) {
|
|
addIncompatibility(workingIncompatibility)
|
|
}
|
|
|
|
return workingIncompatibility
|
|
}
|
|
|
|
val newTerms = workingIncompatibility.terms.filter { it != mostRecentTerm }.toMutableList()
|
|
|
|
mostRecentSatisfier.cause?.let {
|
|
newTerms.addAll(it.terms.filter { term -> term.pkg != mostRecentSatisfier.pkg })
|
|
}
|
|
|
|
if (difference != null) {
|
|
newTerms.add(difference.inverse)
|
|
}
|
|
|
|
workingIncompatibility = Incompatibility(
|
|
newTerms,
|
|
IncompatibilityCause.ConflictCause(workingIncompatibility, mostRecentSatisfier.cause!!)
|
|
)
|
|
}
|
|
|
|
error("Failed")
|
|
}
|
|
|
|
private fun addIncompatibility(incompat: Incompatibility<P, V>) {
|
|
for (term in incompat.terms) {
|
|
incompatibilities.getOrPut(term.pkg, { mutableListOf() }).add(incompat)
|
|
}
|
|
}
|
|
|
|
private fun propagateIncompatibility(incompatibility: Incompatibility<P, V>): PropagationResult {
|
|
val unsatisfied = run {
|
|
var unsatisfied: Term<P, V>? = null;
|
|
|
|
for (term in incompatibility.terms) {
|
|
when (val relation = solution.relation(term)) {
|
|
SetRelation.Disjoint -> return PropagationResult.None
|
|
SetRelation.Overlaps, SetRelation.Subset, SetRelation.Superset -> {
|
|
if (unsatisfied != null) {
|
|
return PropagationResult.None
|
|
}
|
|
|
|
unsatisfied = term
|
|
}
|
|
}
|
|
}
|
|
|
|
unsatisfied
|
|
} ?: return PropagationResult.Conflict
|
|
|
|
solution.derive(unsatisfied.pkgSelection, !unsatisfied.exclusive, incompatibility)
|
|
return PropagationResult.Unsatisfied(unsatisfied.pkg)
|
|
}
|
|
|
|
private sealed class PropagationResult {
|
|
object None : PropagationResult()
|
|
object Conflict : PropagationResult()
|
|
class Unsatisfied<P>(val pkg: P) : PropagationResult()
|
|
}
|
|
|
|
private fun choosePackageVersion(): P? {
|
|
return null
|
|
}
|
|
} |