From c24f4f75a4f40646ee3eedb084772d9ee501e5b2 Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Thu, 4 Jun 2020 11:37:41 +0200 Subject: [PATCH] Optimize and refactor TermGraphUnifier. Beautify the code. Avoid internalizing a (sub-)term that has not been unified with a variable, thus saving on unnecessary accounting. --- .../mps/unification/TermGraphUnifier.kt | 187 ++++++++++-------- 1 file changed, 107 insertions(+), 80 deletions(-) diff --git a/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt b/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt index 26363ca2..6485414a 100644 --- a/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt +++ b/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt @@ -17,6 +17,7 @@ package jetbrains.mps.unification import gnu.trove.list.array.TIntArrayList +import gnu.trove.map.hash.TIntIntHashMap import gnu.trove.map.hash.TIntObjectHashMap import jetbrains.mps.logic.reactor.logical.Logical import jetbrains.mps.unification.Substitution.FailureCause.CYCLE_DETECTED @@ -53,6 +54,7 @@ import java.util.* */ typealias IntList = TIntArrayList +typealias IntIntHashMap = TIntIntHashMap typealias IntAnyHashMap = TIntObjectHashMap class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID, @@ -65,57 +67,72 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID, } fun unify(a: Term, b: Term): Substitution { - return if (unifClosure(toInner(a), toInner(b))) { - findSolution(toInner(a)) + return if (unifClosure(toInt(a), toInt(b))) { + findSolution(a, Unification.EMPTY_SUBSTITUTION) } else { failedSubstitution(failureCause, *failureDetails) } } - private fun findSolution(s: Int): Substitution { - return findSolution(s, Unification.EMPTY_SUBSTITUTION) - } - - private fun findSolution(s: Int, defSubs: Substitution) : Substitution { - val (_, z) = findSchema(s) - val vars = innerVars[find(z)] - - if (isAcyclic(z)) { return defSubs } // not part of a cycle - if (isVisited(z)) { return failedSubstitution(CYCLE_DETECTED) } // there exists a cycle - + private fun findSolution(term: Term, defSubs: Substitution) : Substitution { var subs = defSubs - if (origin[z].`is`(FUN)) { - setVisited(z) - for (c in origin[z].arguments()) { - subs = findSolution(toInner(c), subs) - if (!subs.isSuccessful) break - } - clearVisited(z) - } - if (subs.isSuccessful) { - setAcyclic(z) - - // avoid unnecessary instatiation - val success = if (subs is SuccessfulSubstitution) subs as SuccessfulSubstitution - else SuccessfulSubstitution(subs) - - if (vars != null) { - for (v in vars) { - if (trivialBindings || v != z) { - // Keep the order of variables within a binding - if (origin[z].`is`(VAR) && origin[z].compareTo(origin[v]) < 0) { - success.addBinding(fromInner(z), fromInner(v)) - - } else { - success.addBinding(fromInner(v), fromInner(z)) - } - } + // use the "shortcut" solution for terms that have not been internalized, + // meaning such terms have not gone through a unification, thus have not + // been assigned either class or schema + if (!isInternalized(term)) { + if (term.`is`(FUN)) { + for (c in term.arguments()) { + subs = findSolution(c, subs) + if (!subs.isSuccessful) break } + } else { + // VAR or REF has to be processed recursively to account for + // possible cycles + toInt(term) + } + } + + if (isInternalized(term)) { + val (_, z) = findSchema(toInt(term)) + val vars = intVars[find(z)] + + if (isAcyclic(z)) { return defSubs } // not part of a cycle + if (isVisited(z)) { return failedSubstitution(CYCLE_DETECTED) } // there exists a cycle + + if (origin[z].`is`(FUN)) { + setVisited(z) + for (c in origin[z].arguments()) { + subs = findSolution(c, subs) + if (!subs.isSuccessful) break + } + clearVisited(z) } - subs = success + if (subs.isSuccessful) { + setAcyclic(z) + + // avoid unnecessary instatiation + val success = if (subs is SuccessfulSubstitution) subs as SuccessfulSubstitution + else SuccessfulSubstitution(subs) + + if (vars != null) { + for (v in vars) { + if (trivialBindings || v != z) { + // Keep the order of variables within a binding + if (origin[z].`is`(VAR) && origin[z].compareTo(origin[v]) < 0) { + success.addBinding(fromInner(z), fromInner(v)) + + } else { + success.addBinding(fromInner(v), fromInner(z)) + } + } + } + } + + subs = success + } } return subs @@ -148,7 +165,7 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID, val zsit = origin[zs].arguments().iterator() val ztit = origin[zt].arguments().iterator() while (zsit.hasNext() && ztit.hasNext()) { - if (!unifClosure(toInner(zsit.next()), toInner(ztit.next()))) { + if (!unifClosure(toInt(zsit.next()), toInt(ztit.next()))) { return false // arguments mismatch } } @@ -187,9 +204,9 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID, } setSize(s, ssize + tsize) - prependVars(s, innerVars[t]) + prependVars(s, intVars[t]) setKlass(t, s) - + // copy the schema val zs = schema(s) val zt = schema(t) @@ -223,9 +240,9 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID, private fun prependVars(t: Int, vars: TIntArrayList?) { if (vars?.isEmpty ?: true) { return } - val newVars = IntList(innerVars[t] ?: EMPTY_LIST) + val newVars = IntList(intVars[t] ?: EMPTY_LIST) newVars.addAll(vars) - innerVars.put (t, newVars) + intVars.put (t, newVars) } @@ -241,36 +258,35 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID, private fun getRef(zs: Int): Int = if (origin[zs].`is`(REF)) - toInner(origin[zs].get()) + toInt(origin[zs].get()) else zs - private fun toInner(term: Term): Int { - // Variables with matching symbols are all treated as a single term. - val key = if (term.`is`(VAR)) idSymbol(term.symbol()) else term - return if (backref.containsKey(key)) { - backref[key] !! + private fun toInt(term: Term): Int { + val key = intKey(term) + return if (terms.containsKey(key)) { + terms[key] } else { val wrapped = wrapper.wrap(term) val next = origin.size origin.add(wrapped) - - // initialize internal structures - innerSchema.add(next) - innerClass.add(next) - innerSize.add(1) - innerAcyclic.add(0) - innerVisited.add(0) - + terms.put(key, next) + initData(next) if (wrapped.`is`(VAR)) { - innerVars.put(next, IntList(intArrayOf(next))) + intVars.put(next, IntList(intArrayOf(next))) } - backref.put(key, next) + next } } + private fun isInternalized(term: Term): Boolean = terms.containsKey(intKey(term)) + + private fun intKey(term: Term) = + // Variables with matching symbols are all treated as a single term. + System.identityHashCode(if (term.`is`(VAR)) idSymbol(term.symbol()) else term) + private fun fromInner(t: Int): Term { return wrapper.unwrap(origin[t]) } @@ -286,36 +302,47 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID, return if (this == null) that == null else this.equals(that) } - private fun klass(t: Int): Int = innerClass[t] + private fun initData(nextId: Int) { + // initialize internal structures + intSchema.add(nextId) + intClass.add(nextId) + intSize.add(1) + intAcyclic.add(0) + intVisited.add(0) + } - private fun setKlass(t: Int, klass: Int): Unit { innerClass[t] = klass } + private fun schema(t: Int): Int = intSchema[t] - private fun schema(t: Int): Int = innerSchema[t] + private fun setSchema(t: Int, schema: Int) { intSchema[t] = schema } - private fun setSchema(t: Int, schema: Int): Unit { innerSchema[t] = schema } + private fun klass(t: Int): Int = intClass[t] - private fun size(t: Int): Int = innerSize[t] + private fun setKlass(t: Int, klass: Int) { intClass[t] = klass } - private fun setSize(t: Int, size: Int): Unit { innerSize[t] = size } + private fun size(t: Int): Int = intSize[t] - private fun isAcyclic(t: Int): Boolean = innerAcyclic[t] != 0 + private fun setSize(t: Int, size: Int) { intSize[t] = size } - private fun setAcyclic(t: Int): Unit { innerAcyclic[t] = 1 } + private fun isAcyclic(t: Int): Boolean = (intAcyclic[t]) != 0 - private fun isVisited(t: Int): Boolean = innerVisited[t] != 0 + private fun setAcyclic(t: Int) { intAcyclic[t] = 1 } - private fun setVisited(t: Int): Unit { innerVisited[t] = 1 } + private fun isVisited(t: Int): Boolean = intVisited[t] != 0 - private fun clearVisited(t: Int): Unit { innerVisited[t] = 0 } + private fun setVisited(t: Int) { intVisited[t] = 1 } + + private fun clearVisited(t: Int) { intVisited[t] = 0 } private var failureCause: Substitution.FailureCause = Substitution.FailureCause.UKNOWN private var failureDetails = emptyArray() - private val backref = IdentityHashMap() - private val innerVars = IntAnyHashMap() + private val origin = ArrayList() - private val innerClass = IntList() - private val innerSchema = IntList() - private val innerSize = IntList() - private val innerAcyclic = IntList() - private val innerVisited = IntList() -} \ No newline at end of file + private val terms = IntIntHashMap() + private val intVars = IntAnyHashMap() + private val intClass = IntList() + private val intSchema = IntList() + private val intSize = IntList() + private val intAcyclic = IntList() + private val intVisited = IntList() +} +