Optimizing the aux lookup of constraints by moving the constraint symbol to the top of the search term.
This commit is contained in:
parent
3dd42efe32
commit
b891f0fa47
|
|
@ -236,7 +236,7 @@ internal class MatchTrie(val rule: Rule,
|
|||
when (arg) {
|
||||
is Logical<*> -> fromArgs.addAll(aux.forLogical(arg))
|
||||
|
||||
is Term -> fromArgs.addAll(aux.forTerm(arg))
|
||||
is Term -> fromArgs.addAll(aux.forTermAndConstraint(arg, cst))
|
||||
|
||||
is Any -> fromArgs.addAll(aux.forValue(arg))
|
||||
}
|
||||
|
|
|
|||
|
|
@ -174,42 +174,3 @@ fun Any?.asTerm(): Term = when (this) {
|
|||
// FIXME: "unpacking" the logicals
|
||||
fun Term.toValue(): Any? = if (this is Constant) this.symbol() else this
|
||||
|
||||
abstract class TermImpl(val symbol: Any) : Term {
|
||||
|
||||
override fun symbol() = symbol
|
||||
|
||||
override fun compareTo(other: Term): Int {
|
||||
return if (this.javaClass === other.javaClass)
|
||||
symbol.toString().compareTo(symbol.toString())
|
||||
else
|
||||
this.javaClass.toString().compareTo(other.javaClass.toString())
|
||||
}
|
||||
}
|
||||
|
||||
open class Function(symbol: Any, val arguments: List<Term>) : TermImpl(symbol) {
|
||||
|
||||
override fun arguments(): Collection<Term> = arguments
|
||||
|
||||
override fun `is`(kind: Term.Kind?): Boolean = (kind === Term.Kind.FUN)
|
||||
|
||||
override fun get(): Term = this
|
||||
}
|
||||
|
||||
class Constant(symbol: Any) : Function(symbol, emptyList()) {}
|
||||
|
||||
class WrapConstant(val orig: Term) : Function(orig, emptyList()) {}
|
||||
|
||||
class WrapFreeLogical(val logical: Logical<*>) : Function(logical.findRoot(), emptyList()) {}
|
||||
|
||||
class WrapGroundLogical(val logical: Logical<Term>) :
|
||||
Function(logical.findRoot().value().symbol(),
|
||||
logical.findRoot().value().arguments().toList()) {}
|
||||
|
||||
class Variable(symbol: Any) : TermImpl(symbol) {
|
||||
|
||||
override fun arguments(): Collection<Term> = emptyList()
|
||||
|
||||
override fun `is`(kind: Term.Kind): Boolean = (kind === Term.Kind.VAR)
|
||||
|
||||
override fun get(): Term = TODO()
|
||||
}
|
||||
|
|
@ -46,6 +46,8 @@ interface OccurrenceIndex {
|
|||
|
||||
fun forTerm(term: Term): Iterable<ConstraintOccurrence>
|
||||
|
||||
fun forTermAndConstraint(term: Term, cst: Constraint): Iterable<ConstraintOccurrence>
|
||||
|
||||
fun forValue(value: Any): Iterable<ConstraintOccurrence>
|
||||
|
||||
}
|
||||
|
|
@ -57,13 +59,13 @@ class OccurrenceStore : LogicalObserver, OccurrenceIndex {
|
|||
|
||||
val currentFrame: () -> StoreHolder
|
||||
|
||||
lateinit var symbol2occurrences: PersMap<ConstraintSymbol, IdHashSet<ConstraintOccurrence>>
|
||||
var symbol2occurrences: PersMap<ConstraintSymbol, IdHashSet<ConstraintOccurrence>>
|
||||
|
||||
lateinit var logical2occurrences: PersMap<IdWrapper<Logical<*>>, IdHashSet<ConstraintOccurrence>>
|
||||
var logical2occurrences: PersMap<IdWrapper<Logical<*>>, IdHashSet<ConstraintOccurrence>>
|
||||
|
||||
lateinit var term2occurrences: TermTrie<ConstraintOccurrence>
|
||||
var term2occurrences: TermTrie<ConstraintOccurrence>
|
||||
|
||||
lateinit var value2occurrences: PersMap<Any, IdHashSet<ConstraintOccurrence>>
|
||||
var value2occurrences: PersMap<Any, IdHashSet<ConstraintOccurrence>>
|
||||
|
||||
constructor(copyFrom: OccurrenceStore, currentFrame: () -> StoreHolder)
|
||||
{
|
||||
|
|
@ -88,7 +90,7 @@ class OccurrenceStore : LogicalObserver, OccurrenceIndex {
|
|||
when (value) {
|
||||
is Term -> {
|
||||
for (occ in toMerge) {
|
||||
this.term2occurrences = term2occurrences.put(value, occ)
|
||||
this.term2occurrences = term2occurrences.put(value.withConstraint(occ.constraint()), occ)
|
||||
}
|
||||
}
|
||||
is Any -> {
|
||||
|
|
@ -144,7 +146,7 @@ class OccurrenceStore : LogicalObserver, OccurrenceIndex {
|
|||
currentFrame().addObserver(value) { frame -> frame.store() }
|
||||
}
|
||||
is Term -> {
|
||||
this.term2occurrences = term2occurrences.put(value, occ)
|
||||
this.term2occurrences = term2occurrences.put(value.withConstraint(occ.constraint()), occ)
|
||||
}
|
||||
is Any -> {
|
||||
this.value2occurrences = value2occurrences.put(value,
|
||||
|
|
@ -222,15 +224,37 @@ class OccurrenceStore : LogicalObserver, OccurrenceIndex {
|
|||
}
|
||||
|
||||
override fun forTerm(term: Term): Iterable<ConstraintOccurrence> {
|
||||
return term2occurrences.lookupValues(term).filter { it.isStored() }
|
||||
return term2occurrences.lookupValues(term.withAny()).filter { it.isStored() }
|
||||
}
|
||||
|
||||
override fun forTermAndConstraint(term: Term, cst: Constraint): Iterable<ConstraintOccurrence> {
|
||||
return term2occurrences.lookupValues(term.withConstraint(cst)).filter { it.isStored() }
|
||||
}
|
||||
|
||||
override fun forValue(value: Any): Iterable<ConstraintOccurrence> {
|
||||
return (value2occurrences[value] ?: emptySet()).filter { co -> co.isStored() }
|
||||
}
|
||||
|
||||
private fun Term.withConstraint(cst: Constraint): Term = Function(CONSTRAINT, listOf(Function(cst.symbol(), emptyList()), this))
|
||||
|
||||
private fun Term.withAny(): Term = Function(CONSTRAINT, listOf(Variable(ANY), this))
|
||||
|
||||
private companion object {
|
||||
|
||||
private val CONSTRAINT = object : Any() {
|
||||
override fun toString(): String = "CONSTRAINT"
|
||||
}
|
||||
|
||||
private val ANY = object : Any() {
|
||||
override fun toString(): String = "ANY"
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
||||
private data class MemConstraintOccurrence(val currentFrame: () -> HandlerFrame, val constraint: Constraint, val arguments: List<*>) :
|
||||
ConstraintOccurrence,
|
||||
LogicalObserver,
|
||||
|
|
|
|||
|
|
@ -0,0 +1,44 @@
|
|||
package jetbrains.mps.logic.reactor.core
|
||||
|
||||
import jetbrains.mps.logic.reactor.logical.Logical
|
||||
import jetbrains.mps.unification.Term
|
||||
|
||||
abstract class TermImpl(val symbol: Any) : Term {
|
||||
|
||||
override fun symbol() = symbol
|
||||
|
||||
override fun compareTo(other: Term): Int {
|
||||
return if (this.javaClass === other.javaClass)
|
||||
symbol.toString().compareTo(symbol.toString())
|
||||
else
|
||||
this.javaClass.toString().compareTo(other.javaClass.toString())
|
||||
}
|
||||
}
|
||||
|
||||
open class Function(symbol: Any, val arguments: List<Term>) : TermImpl(symbol) {
|
||||
|
||||
override fun arguments(): Collection<Term> = arguments
|
||||
|
||||
override fun `is`(kind: Term.Kind?): Boolean = (kind === Term.Kind.FUN)
|
||||
|
||||
override fun get(): Term = this
|
||||
}
|
||||
|
||||
class Constant(symbol: Any) : Function(symbol, emptyList()) {}
|
||||
|
||||
class WrapConstant(val orig: Term) : Function(orig, emptyList()) {}
|
||||
|
||||
class WrapFreeLogical(val logical: Logical<*>) : Function(logical.findRoot(), emptyList()) {}
|
||||
|
||||
class WrapGroundLogical(val logical: Logical<Term>) :
|
||||
Function(logical.findRoot().value().symbol(),
|
||||
logical.findRoot().value().arguments().toList()) {}
|
||||
|
||||
class Variable(symbol: Any) : TermImpl(symbol) {
|
||||
|
||||
override fun arguments(): Collection<Term> = emptyList()
|
||||
|
||||
override fun `is`(kind: Term.Kind): Boolean = (kind === Term.Kind.VAR)
|
||||
|
||||
override fun get(): Term = TODO()
|
||||
}
|
||||
|
|
@ -1,6 +1,7 @@
|
|||
import jetbrains.mps.logic.reactor.core.*
|
||||
import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence
|
||||
import jetbrains.mps.logic.reactor.logical.Logical
|
||||
import jetbrains.mps.logic.reactor.program.Constraint
|
||||
import jetbrains.mps.logic.reactor.program.ConstraintSymbol
|
||||
import jetbrains.mps.unification.Term
|
||||
import jetbrains.mps.unification.Unification
|
||||
|
|
@ -32,6 +33,11 @@ class TestMatcher {
|
|||
co.arguments().any { it is Term && Unification.unify(it, term).isSuccessful }
|
||||
}
|
||||
|
||||
override fun forTermAndConstraint(term: Term, cst: Constraint): Iterable<ConstraintOccurrence> =
|
||||
stored.filter { co ->
|
||||
co.constraint().symbol() == cst.symbol() && co.arguments().any { it is Term && Unification.unify(it, term).isSuccessful }
|
||||
}
|
||||
|
||||
override fun forValue(value: Any): Iterable<ConstraintOccurrence> =
|
||||
stored.filter { co -> co.arguments().contains(value) }
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue