From ed76bdae739b5f00103218a51782fbc79a099a8c Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Sun, 24 Jan 2016 20:45:46 +0100 Subject: [PATCH] Optimizing looking up constraint occurrences to complete a match. Parent observer for logicals, maintaining the logical-to-occurrence index in occurrence store. Some code refactoring. --- .../mps/logic/reactor/core/DexxCollections.kt | 37 ++++ .../mps/logic/reactor/core/Handler.kt | 115 +++---------- .../mps/logic/reactor/core/Logical.kt | 142 ++++++++++----- .../mps/logic/reactor/core/Matcher.kt | 159 ++--------------- .../mps/logic/reactor/core/OccurrenceStore.kt | 155 ++++++++++++++--- .../mps/logic/reactor/core/PartialMatch.kt | 161 ++++++++++++++++++ .../mps/logic/reactor/core/RuleIndex.kt | 5 +- reactor/Test/test/RulesHelper.kt | 18 +- reactor/Test/test/TestLogical.kt | 60 +++++++ reactor/Test/test/TestMatcher.kt | 19 ++- reactor/Test/test/TestProgram.kt | 1 - 11 files changed, 556 insertions(+), 316 deletions(-) create mode 100644 reactor/Core/src/jetbrains/mps/logic/reactor/core/DexxCollections.kt create mode 100644 reactor/Core/src/jetbrains/mps/logic/reactor/core/PartialMatch.kt create mode 100644 reactor/Test/test/TestLogical.kt diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/DexxCollections.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/DexxCollections.kt new file mode 100644 index 00000000..c4aa92d7 --- /dev/null +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/DexxCollections.kt @@ -0,0 +1,37 @@ +package jetbrains.mps.logic.reactor.core + +import com.github.andrewoma.dexx.collection.ConsList + +/** + * @author Fedor Isakov + */ + + +fun emptyConsList(): ConsList = ConsList.empty() + +fun cons(e: E): ConsList = emptyConsList().append(e) + +fun consListOf(vararg args: E): ConsList { + val builder = ConsList.factory().newBuilder() + for (e in args) { + builder.add(e) + } + return builder.build() +} + +fun ConsList.removeAt(idx: Int): ConsList { + if (idx < 0) throw IllegalArgumentException("index < 0") + val left = this.take(idx) + var right = this.drop(idx + 1) + for (e in left.reversed()) { + right = right.prepend(e) + } + return right +} + +fun ConsList?.remove(e: E): ConsList? { + return this?.run { + val idx = indexOf(e) + if (idx >= 0) removeAt(idx) else this + } +} \ No newline at end of file diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Handler.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Handler.kt index 599017ec..0ae61e74 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Handler.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Handler.kt @@ -28,10 +28,12 @@ class Handler : Matcher.AuxOccurrences { private val activeQueue = LinkedList() - private val activationStack = LinkedList() + private val activationStack = LinkedList() private val matcher: Matcher + private var processing = false + constructor( sessionSolver: SessionSolver, programRules: Iterable, @@ -46,7 +48,7 @@ class Handler : Matcher.AuxOccurrences { this.rules.addAll(programRules) this.matcher = Matcher(rules, this, profiler) if (occurrences != null) { - this.occurrenceStore.addAll(occurrences) + this.occurrenceStore.storeAll(occurrences) } } @@ -72,36 +74,19 @@ class Handler : Matcher.AuxOccurrences { } override fun findOccurrences( - constraint: Constraint, - acceptable: (ConstraintOccurrence) -> Boolean): Iterable + symbol: ConstraintSymbol, + logicals: Iterable>, + acceptable: (ConstraintOccurrence) -> Boolean): Sequence { - return profiler.profile>("findOccurrences", { - return occurrenceStore.allFor(constraint).filter { + return profiler.profile>("findOccurrences", { - co -> constraint.matches(co, profiler) && acceptable(co) + // first, try the logicals, then symbol + val fromLogicals = logicals.asSequence(). + flatMap { log -> occurrenceStore.forLogical(log) }. + filter { co -> co.constraint().symbol() == symbol } - } - - }) - } - - private fun store(occ: ConstraintOccurrence) { - occurrenceStore.add(occ) - } - - private fun discard(occ: ConstraintOccurrence) { - occurrenceStore.remove(occ) - occ.terminate() - } - - private fun activate(item: AndItem, logicalContext: LogicalContext) { - profiler.profile("activate", { - - when (item) { - is Constraint -> process(item.occurrence(this@Handler, logicalContext)) - is Predicate -> tellPredicate(item.invocation(logicalContext)) - else -> throw IllegalArgumentException("unknown item ${item}") - } + (if (fromLogicals.any()) fromLogicals else occurrenceStore.forSymbol(symbol)). + filter { acceptable(it) } }) } @@ -110,7 +95,7 @@ class Handler : Matcher.AuxOccurrences { profiler.profile("process_${active.constraint().symbol()}", { if (!active.isStored()) { - store(active) + occurrenceStore.store(active) trace.activate(active) } else { trace.reactivate(active) @@ -124,12 +109,16 @@ class Handler : Matcher.AuxOccurrences { trace.trigger(match) for ((cst, occ) in match.discarded) { - discard(occ) + occurrenceStore.discard(occ) trace.discard(occ) } for (item in match.rule.body()) { - activate(item, match.logicalContext()) + when (item) { + is Constraint -> process(item.occurrence(this@Handler, match.logicalContext())) + is Predicate -> tellPredicate(item.invocation(match.logicalContext())) + else -> throw IllegalArgumentException("unknown item ${item}") + } } trace.exit(match.rule) @@ -145,85 +134,35 @@ class Handler : Matcher.AuxOccurrences { private fun Rule.checkGuard(logicalContext: LogicalContext): Boolean = profiler.profile("checkGuard", { + return guard().all { prd -> askPredicate(prd.invocation(logicalContext)) } + }) private fun askPredicate(invocation: PredicateInvocation): Boolean = profiler.profile("ask_${invocation.predicate().symbol()}", { + return sessionSolver.ask(invocation.predicate().symbol(), * invocation.arguments().toTypedArray()) + }) private fun tellPredicate(invocation: PredicateInvocation) { profiler.profile("tell_${invocation.predicate().symbol()}", { + sessionSolver.tell(invocation.predicate().symbol(), * invocation.arguments().toTypedArray()) + }) } - private fun ConstraintOccurrence.isStored(): Boolean = - occurrenceStore.isStored(this) - } private val noLogicalContext: LogicalContext = object: LogicalContext { override fun variable(logicalPattern: LogicalPattern): Logical = TODO() } -private fun Constraint.occurrence(handler: Handler, context: LogicalContext): ConstraintOccurrence = - MemConstraintOccurrence(handler, this, occurrenceArguments(context)) - private fun Predicate.invocation(logicalContext: LogicalContext): PredicateInvocation = object: PredicateInvocation { override fun predicate(): Predicate = this@invocation override fun arguments(): Collection<*> = invocationArguments(logicalContext) } - -fun ConstraintOccurrence.terminate() { - if (this is MemConstraintOccurrence) { - _terminate() - } -} - -private data class MemConstraintOccurrence(val handler: Handler, val constraint: Constraint, val arguments: List<*>, val id: Int) : - ConstraintOccurrence, - LogicalValueObserver -{ - - var alive = true - - companion object { - val random = Random() - } - - constructor(handler: Handler, constraint: Constraint, arguments: Collection<*>) : - this(handler, constraint, ArrayList(arguments), random.nextInt()) - { - for (a in arguments) { - if (a is Logical<*>) { - a.addObserver(this) - } - } - } - - override fun constraint(): Constraint = constraint - - override fun arguments(): Collection<*> = arguments - - override fun valueUpdated(logical: Logical<*>) { - handler.queue(this) - } - - - fun _terminate() { - for (a in arguments) { - if (a is Logical<*>) { - a.removeObserver(this) - } - } - alive = false - } - - - override fun toString(): String = "${constraint().symbol()}(${arguments().joinToString()})" - -} diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Logical.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Logical.kt index bc06c2d7..989070a0 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Logical.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Logical.kt @@ -3,6 +3,7 @@ package jetbrains.mps.logic.reactor.core import jetbrains.mps.logic.reactor.logical.Logical import jetbrains.mps.logic.reactor.logical.LogicalPattern +import jetbrains.mps.logic.reactor.logical.NamingContext import jetbrains.mps.logic.reactor.logical.SolverLogical import java.util.* @@ -10,18 +11,22 @@ import java.util.* * @author Fedor Isakov */ -internal interface LogicalValueObserver { +interface LogicalObserver { fun valueUpdated(logical: Logical<*>) + fun parentUpdated(logical: Logical<*>) + } -internal fun Logical<*>.addObserver(observer: LogicalValueObserver) { - (this as MemLogical<*>).observers.add(observer) +fun Logical<*>.addObserver(observer: LogicalObserver) { + (this as MemLogical<*>).valueObservers.add(this.to(observer)) + (this as MemLogical<*>).parentObservers.add(this.to(observer)) } -internal fun Logical<*>.removeObserver(observer: LogicalValueObserver) { - (this as MemLogical<*>).observers.remove(observer) +fun Logical<*>.removeObserver(observer: LogicalObserver) { + (this as MemLogical<*>).valueObservers.removeAll { p -> p.second == observer } + (this as MemLogical<*>).parentObservers.removeAll { p -> p.second == observer } } fun LogicalPattern.logical(): Logical = MemLogical(name()) @@ -36,7 +41,7 @@ class MemLogical : SolverLogical { val name: String - var pattern: LogicalPattern? = null + val pattern: LogicalPattern var _parent: MemLogical? = null @@ -44,19 +49,24 @@ class MemLogical : SolverLogical { var rank = 0 - internal val observers = ArrayList() + internal val valueObservers = ArrayList, LogicalObserver>>() + + internal val parentObservers = ArrayList, LogicalObserver>>() constructor(value: T) { this.name = "$${++lastIdx}" + this.pattern = DefaultLogicalPattern(name) this._value = value } constructor(name: String) { this.name = "${name}_${++lastIdx}" + this.pattern = DefaultLogicalPattern(name) } constructor(name: String, value: T) { this.name = "${name}_${++lastIdx}" + this.pattern = DefaultLogicalPattern(name) this._value = value } @@ -73,50 +83,51 @@ class MemLogical : SolverLogical { override fun isWildcard(): Boolean = TODO() - override fun pattern(): LogicalPattern? = pattern + override fun pattern(): LogicalPattern = pattern override fun findRoot(): SolverLogical = find() override fun setValue(newValue: T) { this._value = newValue - notifyObservers() + notifyValueUpdated() } override fun union(other: SolverLogical, reconciler: SolverLogical.ValueReconciler) { - val leftRepr = this.find() - val rightRepr = (other as MemLogical).find() + val thisRepr = this.find() + val otherRepr = (other as MemLogical).find() - // invariant: leftRepr.rank > rightRepr.rank - if (leftRepr.rank() < rightRepr.rank()) { - rightRepr.union(leftRepr, reconciler); + // invariant: thisRepr.rank > otherRepr.rank + if (thisRepr.rank() < otherRepr.rank()) { + otherRepr.union(thisRepr, reconciler); return; - } else if (leftRepr.rank() == rightRepr.rank()) { - leftRepr.incRank(); + } else if (thisRepr.rank() == otherRepr.rank()) { + thisRepr.incRank(); } - rightRepr._parent = leftRepr + otherRepr.setParent(thisRepr) + thisRepr.mergeParentObservers(otherRepr) - val leftVal = leftRepr.value(); - val rightVal = rightRepr.value(); + val thisVal = thisRepr.value(); + val otherVal = otherRepr.value(); - if (leftVal == null && rightVal != null) { + if (thisVal == null && otherVal != null) { // var ground - leftRepr.setValue(rightVal); + thisRepr.setValue(otherVal); - } else if (leftVal != null && rightVal == null) { + } else if (thisVal != null && otherVal == null) { // ground var - // rightRepr.setValue(leftRepr.value()); + // otherRepr.setValue(thisRepr.value()); // TODO: no need to copy the value - rightRepr.notifyObservers(); + otherRepr.notifyValueUpdated(); - } else if (leftVal == null && rightVal == null) { + } else if (thisVal == null && otherVal == null) { // var var - leftRepr.mergeObservers(rightRepr); + thisRepr.mergeValueObservers(otherRepr); } else { // ground ground - reconciler.reconcile(leftVal, rightVal); + reconciler.reconcile(thisVal, otherVal); } } @@ -124,24 +135,6 @@ class MemLogical : SolverLogical { union(other, { a, b -> if (a != b) throw IllegalStateException("$a does not equal to $b")}) } - private fun rank(): Int = rank - - private fun incRank() { rank++ } - - private fun mergeObservers(mergeFrom: SolverLogical) { - val other = mergeFrom as MemLogical - observers.addAll(other.observers) - other.observers.clear() - } - - private fun notifyObservers() { - val obs = ArrayList(observers) - this.observers.clear() - for (o in obs) { - o.valueUpdated(this) - } - } - private fun find(): MemLogical { val tmp = _parent if (tmp == null) return this @@ -152,8 +145,67 @@ class MemLogical : SolverLogical { } } + private fun rank(): Int = rank + + private fun incRank() { rank++ } + + private fun setParent(parent: MemLogical) { + this._parent = parent + notifyParentUpdated() + } + + private fun mergeValueObservers(mergeFrom: SolverLogical) { + val other = mergeFrom as MemLogical + valueObservers.addAll(other.valueObservers) + other.valueObservers.clear() + } + + private fun mergeParentObservers(mergeFrom: SolverLogical) { + val other = mergeFrom as MemLogical + parentObservers.addAll(other.parentObservers) + other.parentObservers.clear() + } + + private fun notifyValueUpdated() { + val obs = ArrayList(valueObservers) + this.valueObservers.clear() + for (p in obs) { + p.second.valueUpdated(p.first) + } + } + + private fun notifyParentUpdated() { + val obs = ArrayList(parentObservers) + for (p in obs) { + p.second.parentUpdated(p.first) + } + } + override fun toString(): String = if (_parent != null) "${name}(^${_parent.toString()})" else "${name}=$_value" } + +data class DefaultLogicalPattern (val name: String) : LogicalPattern { + + override fun name(): String? { + throw UnsupportedOperationException() + } + + override fun name(namingContext: NamingContext?): String? { + throw UnsupportedOperationException() + } + + override fun isWildcard(): Boolean { + throw UnsupportedOperationException() + } + + override fun type(): Class? { + throw UnsupportedOperationException() + } + + override fun instance(): Logical? { + throw UnsupportedOperationException() + } +} \ No newline at end of file diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt index 7e4269ef..11c637f4 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt @@ -1,17 +1,16 @@ package jetbrains.mps.logic.reactor.core -import com.github.andrewoma.dexx.collection.ConsList import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence import jetbrains.mps.logic.reactor.evaluation.MatchRule import jetbrains.mps.logic.reactor.logical.Logical import jetbrains.mps.logic.reactor.logical.LogicalContext import jetbrains.mps.logic.reactor.logical.LogicalPattern import jetbrains.mps.logic.reactor.program.Constraint +import jetbrains.mps.logic.reactor.program.ConstraintSymbol import jetbrains.mps.logic.reactor.program.Rule +import jetbrains.mps.unification.Substitution import jetbrains.mps.unification.Term import jetbrains.mps.unification.Unification -import java.lang.String -import java.util.* /** * @author Fedor Isakov @@ -21,8 +20,10 @@ class Matcher { interface AuxOccurrences { - fun findOccurrences(constraint: Constraint, acceptable: (ConstraintOccurrence) -> Boolean): - Iterable + fun findOccurrences( + symbol: ConstraintSymbol, + logicals: Iterable>, + acceptable: (ConstraintOccurrence) -> Boolean): Sequence } @@ -36,148 +37,22 @@ class Matcher { this.profiler = profiler } - fun lookupMatches(occ: ConstraintOccurrence): Iterable { - return profiler.profile>("lookupMatches", { + fun lookupMatches(occ: ConstraintOccurrence): Sequence { + return profiler.profile>("lookupMatches", { - val partialMatches = rules.forSymbol(occ.constraint().symbol())?.flatMap { r -> - val matchedKept = r.headKept().filter { cst -> cst.matches(occ) } - val matchedDiscarded = r.headReplaced().filter { cst -> cst.matches(occ) } + val partialMatches = rules.forSymbol(occ.constraint().symbol())?.asSequence()?.flatMap { r -> + val matchedKept = r.headKept().filter { cst -> cst.matches(occ) }.asSequence() + val matchedDiscarded = r.headReplaced().filter { cst -> cst.matches(occ) }.asSequence() - matchedKept.map { cst -> PartialMatch(r).keep(cst, occ) } + - matchedDiscarded.map { cst -> PartialMatch(r).discard(cst, occ) } + matchedKept.map { cst -> PartialMatch(r, profiler).keep(cst, occ) } + + matchedDiscarded.map { cst -> PartialMatch(r, profiler).discard(cst, occ) } } - partialMatches?.flatMap { pm -> completeMatch(pm) }?.filter { pm -> pm.matches() } ?: emptyList() + partialMatches?.flatMap { pm -> pm.completeMatch(aux) }?.filter { pm -> pm.matches() } ?: emptySequence() }) } - private fun completeMatch(match: PartialMatch) : Iterable { - if (!match.isPartial()) return listOf(match) - - return profiler.profile>("completeMatch", { - - val keptToSatisfy = match.rule.headKept().filter { cst -> !match.kept.any { p -> cst === p.first } } - val matchesFromKept = keptToSatisfy.flatMap { cst -> - aux.findOccurrences(cst, { occ -> - profiler.profile("acceptable", { - - !match.hasOccurrence(occ) - - }) - }).flatMap { occ -> completeMatch(match.keep(cst, occ)) } - } - - val discardedToSatisfy = match.rule.headReplaced().filter { cst -> !match.discarded.any { p -> cst === p.first } } - val matchesFromDiscarded = discardedToSatisfy.flatMap { cst -> - aux.findOccurrences(cst, { occ -> - profiler.profile("acceptable", { - - !match.hasOccurrence(occ) - - }) - }).flatMap { occ -> completeMatch(match.discard(cst, occ)) } - } - - matchesFromKept + matchesFromDiscarded - - }) - } - - inner class PartialMatch(val rule: Rule) : MatchRule { - - var kept = ConsList.empty>() - private set - var discarded = ConsList.empty>() - private set - private lateinit var logicalContext : LogicalContext - - private constructor( - original : PartialMatch, - keep: Pair?, - discard: Pair?) : this(original.rule) - { - kept = if (keep != null) original.kept.append(keep) else original.kept - discarded = if (discard != null) original.discarded.append(discard) else original.discarded - } - - fun keep (constraint: Constraint, occ: ConstraintOccurrence) = PartialMatch(this, Pair(constraint, occ), null) - - fun discard (constraint: Constraint, occ: ConstraintOccurrence) = PartialMatch(this, null, Pair(constraint, occ)) - - fun hasOccurrence(occ: ConstraintOccurrence): Boolean { -// return profiler.profile("hasOccurrence", { - - return kept.any { p -> p.second === occ } || discarded.any { p -> p.second === occ } - -// }) - } - - fun isPartial() : Boolean { -// return profiler.profile("isPartial", { - - return rule.headKept().any { cst -> !kept.any { p -> p.first === cst } } || - rule.headReplaced().any { cst -> !discarded.any { p -> p.first === cst } } - -// }) - } - - fun occurrences(): Collection { -// return profiler.profile>("occurrences", { - - return rule.headKept().map { cst -> (kept.find { p -> p.first === cst }?.second) ?: TODO() } + - rule.headReplaced().map { cst -> discarded.find { p -> p.first === cst }?.second ?: TODO() } - -// }) - } - - fun matches(): Boolean { - return profiler.profile("matches", { - - val subst = Unification.unify(PartialMatchTerm(this), RuleTerm(this.rule)) - if (!subst.isSuccessful) return false - - // variables come from LogicalPattern instances in rules - // any successful binding results in either new Logical with associated value, - // or a new value for a Logical already existing in this context - - // only one parameter of the unification can contain variables, - // thus triangular form never has variables on the right hand side - this.logicalContext = object: LogicalContext { - - // invariant: the variables in substitution bindings can only be instances of LogicalPattern - val pattern2value: MutableMap, Any?> = HashMap(subst.bindings().map { b -> - (b.`var`().symbol() as LogicalPattern).to(b.term().toValue()) }.toMap()) - - val pattern2logical: MutableMap, Logical<*>> = HashMap() - - override fun variable(logicalPattern: LogicalPattern): Logical { - if (!pattern2logical.containsKey(logicalPattern)) { - if (pattern2value.containsKey(logicalPattern)) { - val value = pattern2value[logicalPattern] - pattern2logical[logicalPattern] = if (value is Logical<*>) value else MemLogical(value) - } - else { - pattern2logical[logicalPattern] = logicalPattern.logical() - } - } - return pattern2logical[logicalPattern] as Logical - } - } - return true - - }) - } - - fun logicalContext(): LogicalContext = logicalContext - - override fun rule(): Rule = rule - - override fun matchHeadKept(): Iterable = kept.map { p -> p.second } - - override fun matchHeadReplaced(): Iterable = discarded.map { p -> p.second } - - } } @@ -209,7 +84,7 @@ class ConstraintTerm(constraint: Constraint) : constraint.arguments().map { arg -> if (arg is LogicalPattern<*>) Variable(arg) else asTerm(arg) }) {} /** Function term with arguments == terms corresponding to constraint occurrences. Never contains variables. */ -class PartialMatchTerm(pm : Matcher.PartialMatch) : +class PartialMatchTerm(pm : PartialMatch) : Function(pm.rule.tag(), pm.occurrences().map { co -> ConstraintOccurrenceTerm(co) }) {} /** Function term with arguments == constraint occurrence arguments converted to terms. @@ -233,9 +108,9 @@ abstract class TermImpl(val symbol: Any) : Term { override fun compareTo(other: Term): Int { return if (this.javaClass == other.javaClass) - String.valueOf(symbol).compareTo(String.valueOf(symbol)) + symbol.toString().compareTo(symbol.toString()) else - String.valueOf(this.javaClass).compareTo(String.valueOf(other.javaClass)) + this.javaClass.toString().compareTo(other.javaClass.toString()) } } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceStore.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceStore.kt index a690c0bb..bdb130e8 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceStore.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceStore.kt @@ -1,6 +1,10 @@ package jetbrains.mps.logic.reactor.core +import com.github.andrewoma.dexx.collection.ConsList import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence +import jetbrains.mps.logic.reactor.logical.Logical +import jetbrains.mps.logic.reactor.logical.LogicalContext +import jetbrains.mps.logic.reactor.logical.LogicalPattern import jetbrains.mps.logic.reactor.program.Constraint import jetbrains.mps.logic.reactor.program.ConstraintSymbol import java.util.* @@ -9,50 +13,147 @@ import java.util.* * @author Fedor Isakov */ -class OccurrenceStore { +fun Constraint.occurrence(handler: Handler, context: LogicalContext): ConstraintOccurrence = + MemConstraintOccurrence(handler, this, occurrenceArguments(context)) - val symbol2list = HashMap>() +fun ConstraintOccurrence.isStored(): Boolean = + // TODO: superfluous cast + (this as StoreItem).stored - fun addAll(all: Iterable): Unit { +interface StoreItem { + var alive: Boolean + var stored: Boolean + fun terminate(): Unit +} + +class OccurrenceStore : LogicalObserver { + + val symbol2occurrences = HashMap>() + + val logical2occurrences = HashMap, ConsList>() + + override fun valueUpdated(logical: Logical<*>) { /* ignore */ } + + override fun parentUpdated(logical: Logical<*>) { + // TODO: should we care about the order in which occurrences are stored? + logical2occurrences[logical]?.let { toMerge -> + var newList = logical2occurrences[logical.findRoot()] ?: emptyConsList() + for (log in toMerge) { + newList = newList.prepend(log) + } + logical2occurrences[logical.findRoot()] = newList + } + logical2occurrences.remove(logical) + } + + fun storeAll(all: Iterable): Unit { for(occ in all) { - add(occ) + store(occ) } } - fun add(occ: ConstraintOccurrence): Unit { + fun store(occ: ConstraintOccurrence): Unit { val symbol = occ.constraint().symbol() - if (!symbol2list.containsKey(symbol)) { - symbol2list[symbol] = ArrayList() + + symbol2occurrences[symbol] = + symbol2occurrences[symbol]?.prepend(occ) ?: cons(occ) + + for (arg in occ.arguments()) { + when (arg) { + is Logical<*> -> { + logical2occurrences[arg] = + logical2occurrences[arg]?.prepend(occ) ?: cons(occ) + } + else -> { /* TODO: support indexing by value */ } + } } - symbol2list[symbol]!!.add(occ) + + // TODO: superfluous cast + (occ as StoreItem).stored = true } - fun remove(occ: ConstraintOccurrence): Unit { + fun discard(occ: ConstraintOccurrence): Unit { val symbol = occ.constraint().symbol() - if (symbol2list.containsKey(symbol)) { - symbol2list[symbol]!!.remove(occ) + + symbol2occurrences[symbol].remove(occ)?.let { newList -> + symbol2occurrences[symbol] = newList + } + + for (arg in occ.arguments()) { + when (arg) { + is Logical<*> -> { + logical2occurrences[arg].remove(occ)?. let { newList -> + logical2occurrences[arg] = newList + } + } + else -> { /* TODO: support indexing by value */ } + } + } + + + // TODO: superfluous cast + (occ as StoreItem).stored = false + occ.terminate() + } + + fun forSymbol(symbol: ConstraintSymbol): Sequence { + val list = symbol2occurrences[symbol] ?: emptyConsList() + return list.asSequence().filter { co -> co.isStored() } + } + + fun forLogical(ptr: Logical<*>): Sequence { + val list = logical2occurrences[ptr] ?: emptyConsList() + return list.asSequence().filter { co -> co.isStored() } + } + + fun allOccurrences(): Sequence = + symbol2occurrences.values.flatMap { it }.filter { co -> co.isStored() }.asSequence() + +} + +private data class MemConstraintOccurrence(val handler: Handler, val constraint: Constraint, val arguments: List<*>, val id: Int) : + ConstraintOccurrence, + LogicalObserver, + StoreItem +{ + + override var alive = true + + override var stored = false + + companion object { + val random = Random() + } + + constructor(handler: Handler, constraint: Constraint, arguments: Collection<*>) : + this(handler, constraint, ArrayList(arguments), random.nextInt()) + { + for (a in arguments) { + if (a is Logical<*>) { + a.addObserver(this) + } } } - fun isStored(occ: ConstraintOccurrence): Boolean { - val symbol = occ.constraint().symbol() - if (symbol2list.containsKey(symbol)) { - return symbol2list[symbol]!!.contains(occ) - } - else - return false + override fun constraint(): Constraint = constraint + + override fun arguments(): Collection<*> = arguments + + override fun valueUpdated(logical: Logical<*>) { + handler.queue(this) } - fun allFor(cst: Constraint): Iterable { - val symbol = cst.symbol() - if (symbol2list.containsKey(symbol)) { - return symbol2list[symbol]!! + override fun parentUpdated(logical: Logical<*>) { /* ignore */ } + + override fun terminate() { + for (a in arguments) { + if (a is Logical<*>) { + a.removeObserver(this) + } } - else - return emptyList() + alive = false } - fun allOccurrences(): Iterable = - symbol2list.values.flatMap { it } + override fun toString(): String = "${constraint().symbol()}(${arguments().joinToString()})" -} \ No newline at end of file +} diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/PartialMatch.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/PartialMatch.kt new file mode 100644 index 00000000..ca149211 --- /dev/null +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/PartialMatch.kt @@ -0,0 +1,161 @@ +package jetbrains.mps.logic.reactor.core + +import com.github.andrewoma.dexx.collection.Maps +import com.github.andrewoma.dexx.collection.Sets +import com.github.andrewoma.dexx.collection.Set as PersSet +import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence +import jetbrains.mps.logic.reactor.evaluation.MatchRule +import jetbrains.mps.logic.reactor.logical.Logical +import jetbrains.mps.logic.reactor.logical.LogicalContext +import jetbrains.mps.logic.reactor.logical.LogicalPattern +import jetbrains.mps.logic.reactor.program.Constraint +import jetbrains.mps.logic.reactor.program.Rule +import jetbrains.mps.unification.Unification +import java.util.HashMap + +/** + * @author Fedor Isakov + */ + +class PartialMatch(val rule: Rule, val profiler: Profiler? = null) : MatchRule { + + var kept = emptyConsList>() + private set + var discarded = emptyConsList>() + private set + var pattern2logical = Maps.of, PersSet>>() + private set + private lateinit var logicalContext : LogicalContext + + private constructor( + original : PartialMatch, + keep: Pair?, + discard: Pair?) : this(original.rule, original.profiler) + { + this.kept = if (keep != null) original.kept.prepend(keep) else original.kept + this.discarded = if (discard != null) original.discarded.prepend(discard) else original.discarded + + this.pattern2logical = original.pattern2logical + val pair = keep ?: discard!! + for ((ptr, log) in pair.first.arguments().zip(pair.second.arguments())) { + if (ptr is LogicalPattern<*> && log is Logical<*>) { + val logSet = pattern2logical.get(ptr) + this.pattern2logical = pattern2logical.put(ptr, logSet?.add(log) ?: Sets.of(log)) + } + } + } + + fun completeMatch(aux: Matcher.AuxOccurrences) : Sequence { + if (!isPartial()) return sequenceOf(this) + + return profiler.profile>("completeMatch", { + + val matchesFromKept = + rule.headKept(). + filter { cst -> !kept.any { p -> cst === p.first } }. + asSequence(). + flatMap { cst -> findOccurrences(aux, cst).flatMap { occ -> keep(cst, occ).completeMatch(aux) } } + + val matchesFromDiscarded = + rule.headReplaced(). + filter { cst -> !discarded.any { p -> cst === p.first } }. + asSequence(). + flatMap { cst -> findOccurrences(aux, cst).flatMap { occ -> discard(cst, occ).completeMatch(aux) } } + + matchesFromKept + matchesFromDiscarded + + }) + } + + fun findOccurrences(aux: Matcher.AuxOccurrences, cst: Constraint): Sequence { + val logicals = cst.arguments().flatMap { arg -> + if (arg is LogicalPattern<*>) + pattern2logical.get(arg)?.toList() ?: emptyList() + else + emptyList() + } + return aux.findOccurrences(cst.symbol(), logicals, { occ -> !hasOccurrence(occ) }) + } + + fun keep (constraint: Constraint, occ: ConstraintOccurrence) = PartialMatch(this, Pair(constraint, occ), null) + + fun discard (constraint: Constraint, occ: ConstraintOccurrence) = PartialMatch(this, null, Pair(constraint, occ)) + + fun hasOccurrence(occ: ConstraintOccurrence): Boolean { + // return profiler.profile("hasOccurrence", { + + return kept.any { p -> p.second === occ } || discarded.any { p -> p.second === occ } + + // }) + } + + fun isPartial() : Boolean { + // return profiler.profile("isPartial", { + + return rule.headKept().any { cst -> !kept.any { p -> p.first === cst } } || + rule.headReplaced().any { cst -> !discarded.any { p -> p.first === cst } } + + // }) + } + + fun occurrences(): Collection { + // return profiler.profile>("occurrences", { + + return rule.headKept(). + map { cst -> kept.find { p -> p.first === cst }?.second ?: throw IllegalStateException() } + + rule.headReplaced(). + map { cst -> discarded.find { p -> p.first === cst }?.second ?: throw IllegalStateException() } + + // }) + } + + fun matches(): Boolean { + return profiler.profile("matches_${rule.tag()}", { + + val subst = Unification.unify(PartialMatchTerm(this), RuleTerm(this.rule)) + if (!subst.isSuccessful) { + return false + } + + // variables come from LogicalPattern instances in rules + // any successful binding results in either new Logical with associated value, + // or a new value for a Logical already existing in this context + + // only one parameter of the unification can contain variables, + // thus triangular form never has variables on the right hand side + this.logicalContext = object: LogicalContext { + + // invariant: the variables in substitution bindings can only be instances of LogicalPattern + val ptr2val: MutableMap, Any?> = HashMap(subst.bindings().map { b -> + (b.`var`().symbol() as LogicalPattern).to(b.term().toValue()) + }.toMap()) + + val ptr2log: MutableMap, Logical<*>> = HashMap() + + override fun variable(logicalPattern: LogicalPattern): Logical { + if (!ptr2log.containsKey(logicalPattern)) { + if (ptr2val.containsKey(logicalPattern)) { + val value = ptr2val[logicalPattern] + ptr2log[logicalPattern] = if (value is Logical<*>) value else MemLogical(value) + } + else { + ptr2log[logicalPattern] = logicalPattern.logical() + } + } + return ptr2log[logicalPattern] as Logical + } + } + return true + + }) + } + + fun logicalContext(): LogicalContext = logicalContext + + override fun rule(): Rule = rule + + override fun matchHeadKept(): Iterable = kept.map { p -> p.second } + + override fun matchHeadReplaced(): Iterable = discarded.map { p -> p.second } + +} diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleIndex.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleIndex.kt index c72a6267..8e7f6ddb 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleIndex.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleIndex.kt @@ -1,5 +1,7 @@ package jetbrains.mps.logic.reactor.core +import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence +import jetbrains.mps.logic.reactor.logical.LogicalPattern import jetbrains.mps.logic.reactor.program.Constraint import jetbrains.mps.logic.reactor.program.ConstraintSymbol import jetbrains.mps.logic.reactor.program.Rule @@ -43,4 +45,5 @@ class RuleIndex : Iterable { if (!rs.contains(rule)) rs.add(rule) } -} \ No newline at end of file +} + diff --git a/reactor/Test/test/RulesHelper.kt b/reactor/Test/test/RulesHelper.kt index 7238a1c4..49bceb14 100644 --- a/reactor/Test/test/RulesHelper.kt +++ b/reactor/Test/test/RulesHelper.kt @@ -4,6 +4,7 @@ import jetbrains.mps.logic.reactor.logical.LogicalPattern import jetbrains.mps.logic.reactor.program.* import program.MemConstraint import TestConstraintOccurrence +import jetbrains.mps.logic.reactor.core.StoreItem import solver.EqualsSolver import java.util.* @@ -130,22 +131,29 @@ private fun buildConjunction(type: Class, return conjBuilder } -data class TestConstraintOccurrence(val constraint: Constraint, val arguments: List, val id: Int) : ConstraintOccurrence { +data class TestConstraintOccurrence(val constraint: Constraint, val arguments: List, val id: Int) : + ConstraintOccurrence, + StoreItem +{ + override var alive: Boolean = true + + override var stored: Boolean = false companion object { val random = Random() } - constructor(constraint: Constraint, arguments: List) : - this(constraint, arguments, random.nextInt()) {} - constructor(id: String, vararg args: Any) : - this(MemConstraint(ConstraintSymbol.symbol(id, args.size)), listOf(* args), random.nextInt()) {} + this(MemConstraint(ConstraintSymbol.symbol(id, args.size)), listOf(* args), random.nextInt()) {} override fun constraint(): Constraint = constraint override fun arguments(): Collection = arguments + override fun terminate() { + this.alive = false + } + override fun toString(): String = "${constraint().symbol()}(${arguments().joinToString()})" } \ No newline at end of file diff --git a/reactor/Test/test/TestLogical.kt b/reactor/Test/test/TestLogical.kt new file mode 100644 index 00000000..9336bc1a --- /dev/null +++ b/reactor/Test/test/TestLogical.kt @@ -0,0 +1,60 @@ +import jetbrains.mps.logic.reactor.core.LogicalObserver +import jetbrains.mps.logic.reactor.core.MemLogical +import jetbrains.mps.logic.reactor.core.addObserver +import jetbrains.mps.logic.reactor.logical.Logical +import org.junit.Test +import org.junit.Assert.* +import java.util.* + +/** + * @author Fedor Isakov + */ + +data class MockObserverEvent(val logical: Logical<*>, val event: String) {} + +fun value(logical: Logical<*>) = MockObserverEvent(logical, "value") + +fun parent(logical: Logical<*>) = MockObserverEvent(logical, "parent") + +class MockObserver : LogicalObserver { + + val events = ArrayList() + + override fun valueUpdated(logical: Logical<*>) { events.add(value(logical))} + + override fun parentUpdated(logical: Logical<*>) { events.add(parent(logical))} + + fun getAndClearEvents(): Set { + val tmp = ArrayList(events) + events.clear() + return tmp.toSet() + } +} + +class TestLogical { + + @Test + fun mergeObservers() { + val foo = MemLogical(name = "foo") + val bar = MemLogical(name = "bar") + val bazz = MemLogical(name = "bazz") + + val obs = MockObserver() + foo.addObserver(obs) + bar.addObserver(obs) + bazz.addObserver(obs) + + // bar -> foo + foo.union(bar) + assertEquals(setOf(parent(bar)), obs.getAndClearEvents()) + + // bazz -> foo + bazz.union(foo) + assertEquals(setOf(parent(bazz)), obs.getAndClearEvents()) + + assertSame(bazz.findRoot(), foo) + foo.setValue("test") + assertEquals(setOf(value(foo), value(bar), value(bazz)), obs.getAndClearEvents()) + } + +} diff --git a/reactor/Test/test/TestMatcher.kt b/reactor/Test/test/TestMatcher.kt index bfed1f25..859c5275 100644 --- a/reactor/Test/test/TestMatcher.kt +++ b/reactor/Test/test/TestMatcher.kt @@ -3,6 +3,7 @@ import jetbrains.mps.logic.reactor.core.logical import jetbrains.mps.logic.reactor.core.matches import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence import jetbrains.mps.logic.reactor.logical.Logical +import jetbrains.mps.logic.reactor.logical.LogicalPattern import jetbrains.mps.logic.reactor.program.Constraint import jetbrains.mps.logic.reactor.program.ConstraintSymbol import org.junit.Assert.* @@ -15,11 +16,15 @@ import org.junit.Test class TestMatcher { private fun Builder.matcher(vararg occurrence: ConstraintOccurrence): Matcher { + val stored = occurrence.toList() + val aux = object : Matcher.AuxOccurrences { - override fun findOccurrences(constraint: Constraint, acceptable: (ConstraintOccurrence) -> Boolean): - Iterable = - stored.filter { co -> constraint.matches(co) && acceptable(co) } + override fun findOccurrences( + symbol: ConstraintSymbol, + logicals: Iterable>, + acceptable: (ConstraintOccurrence) -> Boolean): Sequence = + stored.filter { co -> co.constraint().symbol() == symbol && acceptable(co) }.asSequence() } return Matcher(rules, aux) } @@ -68,7 +73,7 @@ class TestMatcher { assertFalse(matches.any { m -> m.isPartial() }) assertEquals(rules.toSet(), matches.map { m -> m.rule }.toSet()) matches.forEach { m -> assertTrue(m.kept.size() + m.discarded.size() == 1) } - matches.flatMap { m -> m.kept + m.discarded }.forEach { pair -> + matches.flatMap { m -> (m.kept + m.discarded).asSequence() }.forEach { pair -> val (cst, occ) = pair assert(cst.symbol().id() == "main") } @@ -152,7 +157,7 @@ class TestMatcher { ).matcher().run{ lookupMatches(occurrence("main", "bar")).let { matches -> assertFalse(matches.any { m -> m.isPartial() }) - assertEquals(rules.drop(1), matches.map { m -> m.rule }) + assertEquals(rules.drop(1), matches.map { m -> m.rule }.toList()) } } } @@ -241,7 +246,7 @@ class TestMatcher { matcher(occurrence("foo", 42)).lookupMatches(occurrence("foo", 16)).let { matches -> assertEquals(2, matches.count()) - assertEquals(listOf("main1", "main1"), matches.map { m -> m.rule.tag() }) + assertEquals(listOf("main1", "main1"), matches.map { m -> m.rule.tag() }.toList()) matches.map { m -> setOf(M, N).map { lp -> m.logicalContext().variable(lp).findRoot().value() } }.forEach { vals -> assertEquals(setOf(42, 16), vals.toSet()) @@ -255,7 +260,7 @@ class TestMatcher { matcher(occurrence("foo", x)).lookupMatches(occurrence("foo", y)).let { matches -> assertEquals(2, matches.count()) - assertEquals(listOf("main1", "main1"), matches.map { m -> m.rule.tag() }) + assertEquals(listOf("main1", "main1"), matches.map { m -> m.rule.tag() }.toList()) assertTrue(matches.all{ m -> m.occurrences().toSet().size == 2 }) } diff --git a/reactor/Test/test/TestProgram.kt b/reactor/Test/test/TestProgram.kt index d965dc07..8f232ee0 100644 --- a/reactor/Test/test/TestProgram.kt +++ b/reactor/Test/test/TestProgram.kt @@ -108,7 +108,6 @@ class TestProgram { val a = constraintOccurrences(ConstraintSymbol.symbol("val", 1)).first().arguments().first() assertEquals(0, (a as Logical).get()) assertEquals(5, constraintOccurrences(ConstraintSymbol.symbol("trail", 1)).count()) - println(constraintOccurrences(ConstraintSymbol.symbol("trail", 1))) } }