Propagation history feature, tests. Minor refactorings.

This commit is contained in:
Fedor Isakov 2016-03-07 15:23:57 +01:00
parent 63bb7f578d
commit ec6ce31cc2
8 changed files with 230 additions and 134 deletions

View File

@ -14,7 +14,7 @@ import java.util.*
* @author Fedor Isakov
*/
class Handler : Matcher.AuxOccurrences {
class Handler : Matcher.AuxOccurrencesLookup {
val sessionSolver: SessionSolver
@ -52,7 +52,14 @@ class Handler : Matcher.AuxOccurrences {
}
}
fun occurrences(): Set<ConstraintOccurrence> = occurrenceStore.allOccurrences().toSet()
fun allOccurrences(): Set<ConstraintOccurrence> =
occurrenceStore.allOccurrences().toSet()
fun constraintSymbols(): Set<ConstraintSymbol> =
occurrenceStore.allOccurrences().map { co -> co.constraint().symbol() }.toSet()
fun occurrences(symbol: ConstraintSymbol): Set<ConstraintOccurrence> =
occurrenceStore.allOccurrences().filter { co -> co.constraint().symbol() == symbol }.toSet()
fun tell(constraint: Constraint) {
try {
@ -70,7 +77,7 @@ class Handler : Matcher.AuxOccurrences {
}
}
override fun findOccurrences(
override fun lookupAuxOccurrences(
symbol: ConstraintSymbol,
logicals: Iterable<Logical<*>>,
values: Iterable<Any>,
@ -107,6 +114,7 @@ class Handler : Matcher.AuxOccurrences {
activationStack.push(match)
trace.trigger(match)
matcher.recordPropagation(match)
for ((cst, occ) in match.discarded) {
occurrenceStore.discard(occ)

View File

@ -1,5 +1,8 @@
package jetbrains.mps.logic.reactor.core
import com.github.andrewoma.dexx.collection.ConsList
import com.github.andrewoma.dexx.collection.Maps
import com.github.andrewoma.dexx.collection.List as PersList
import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence
import jetbrains.mps.logic.reactor.evaluation.MatchRule
import jetbrains.mps.logic.reactor.logical.Logical
@ -18,9 +21,9 @@ import jetbrains.mps.unification.Unification
class Matcher {
interface AuxOccurrences {
interface AuxOccurrencesLookup {
fun findOccurrences(
fun lookupAuxOccurrences(
symbol: ConstraintSymbol,
logicals: Iterable<Logical<*>>,
values: Iterable<Any> = emptyList(),
@ -29,12 +32,13 @@ class Matcher {
}
val rules: RuleIndex
val aux: AuxOccurrences
val profiler: Profiler?
private val auxLookup: AuxOccurrencesLookup
private val profiler: Profiler?
private val propHistory = PropagationHistory()
constructor(rules: Collection<Rule>, aux: AuxOccurrences, profiler: Profiler? = null) {
constructor(rules: Collection<Rule>, aux: AuxOccurrencesLookup, profiler: Profiler? = null) {
this.rules = RuleIndex(rules)
this.aux = aux
this.auxLookup = aux
this.profiler = profiler
}
@ -49,16 +53,60 @@ class Matcher {
matchedDiscarded.map { cst -> PartialMatch(r, profiler).discard(cst, occ) }
}
partialMatches?.flatMap { pm -> pm.completeMatch(aux) }?.filter { pm -> pm.matches() } ?: emptySequence()
partialMatches?.flatMap { pm ->
pm.completeMatch(auxLookup) }?.filter { pm ->
pm.matches() && !propHistory.isRecorded(pm) } ?: emptySequence<PartialMatch>()
})
}
fun recordPropagation(pm: PartialMatch) = propHistory.record(pm)
}
private class PropagationHistory {
var recordedPropagation = Maps.of<Rule, PersList<List<IdWrapper<ConstraintOccurrence>>>>()
fun isRecorded(pm: PartialMatch): Boolean {
if (!pm.isPropagation()) return false
val test = pm.kept.map { pair -> IdWrapper(pair.second) }.sortedBy { idOcc -> idOcc.idHash }.toList()
return recordedPropagation.get(pm.rule)?.let { hist ->
hist.any { recorded ->
recorded == test
} // use the reference equality via IdWrapper
} ?: false
}
fun record(pm: PartialMatch): PartialMatch {
if (pm.isPropagation()) {
val idOccs = pm.kept.map { pair -> IdWrapper(pair.second) }.sortedBy { id -> id.idHash }.toList()
val hist = recordedPropagation.get(pm.rule) ?: ConsList.empty<List<IdWrapper<ConstraintOccurrence>>>()
recordedPropagation = recordedPropagation.put(pm.rule, hist.prepend(idOccs))
}
return pm
}
}
private class IdWrapper<T>(val wrapped: T) {
val idHash = System.identityHashCode(wrapped)
override fun hashCode(): Int = idHash
override fun equals(other: Any?): Boolean {
if (other is IdWrapper<*>)
return this.wrapped === other.wrapped // referential equality!
return false
}
override fun toString(): String = "${wrapped.toString()} #$idHash"
}
/**
* True iff the constraint matches the occurrence.

View File

@ -86,13 +86,13 @@ class MemEvaluationSession : EvaluationSession {
override fun sessionSolver(): SessionSolver = program.sessionSolver()
override fun constraintSymbols(): Iterable<ConstraintSymbol> =
handler.occurrences().map { co -> co.constraint().symbol() }.toSet()
handler.constraintSymbols()
override fun constraintOccurrences(): Iterable<ConstraintOccurrence> =
handler.occurrences()
handler.allOccurrences()
override fun constraintOccurrences(symbol: ConstraintSymbol): Iterable<ConstraintOccurrence> =
handler.occurrences().filter { co -> co.constraint().symbol() == symbol }
handler.occurrences(symbol)
private class Backend : EvaluationSession.Backend {

View File

@ -125,7 +125,7 @@ class OccurrenceStore : LogicalObserver {
}
private data class MemConstraintOccurrence(val handler: Handler, val constraint: Constraint, val arguments: List<*>, val id: Int) :
private data class MemConstraintOccurrence(val handler: Handler, val constraint: Constraint, val arguments: List<*>) :
ConstraintOccurrence,
LogicalObserver,
StoreItem
@ -135,12 +135,8 @@ private data class MemConstraintOccurrence(val handler: Handler, val constraint:
override var stored = false
companion object {
val random = Random()
}
constructor(handler: Handler, constraint: Constraint, arguments: Collection<*>) :
this(handler, constraint, ArrayList(arguments), random.nextInt())
this(handler, constraint, ArrayList(arguments))
{
for (a in arguments) {
if (a is Logical<*>) {

View File

@ -45,7 +45,7 @@ class PartialMatch(val rule: Rule, val profiler: Profiler? = null) : MatchRule {
}
}
fun completeMatch(aux: Matcher.AuxOccurrences) : Sequence<PartialMatch> {
fun completeMatch(aux: Matcher.AuxOccurrencesLookup) : Sequence<PartialMatch> {
if (!isPartial()) return sequenceOf(this)
return profiler.profile<Sequence<PartialMatch>>("completeMatch", {
@ -67,7 +67,7 @@ class PartialMatch(val rule: Rule, val profiler: Profiler? = null) : MatchRule {
})
}
fun findOccurrences(aux: Matcher.AuxOccurrences, cst: Constraint): Sequence<ConstraintOccurrence> {
fun findOccurrences(aux: Matcher.AuxOccurrencesLookup, cst: Constraint): Sequence<ConstraintOccurrence> {
val logicals = HashSet<Logical<*>>()
val values = HashSet<Any>()
@ -77,7 +77,7 @@ class PartialMatch(val rule: Rule, val profiler: Profiler? = null) : MatchRule {
else
values.add(arg!!)
}
return aux.findOccurrences(cst.symbol(), logicals, values, { occ -> !hasOccurrence(occ) })
return aux.lookupAuxOccurrences(cst.symbol(), logicals, values, { occ -> !hasOccurrence(occ) })
}
fun keep (constraint: Constraint, occ: ConstraintOccurrence) = PartialMatch(this, Pair(constraint, occ), null)
@ -153,6 +153,8 @@ class PartialMatch(val rule: Rule, val profiler: Profiler? = null) : MatchRule {
})
}
fun isPropagation(): Boolean = !kept.isEmpty && discarded.isEmpty
fun logicalContext(): LogicalContext = logicalContext
override fun rule(): Rule = rule

View File

@ -11,6 +11,8 @@ import org.junit.Assert.*
import org.junit.Before
import org.junit.BeforeClass
import org.junit.Test
import solver.eq
import solver.is_eq
/**
* @author Fedor Isakov
@ -30,6 +32,10 @@ class TestHandler {
sessionSolver.tell(PredicateSymbol("equals", 2), left, right)
}
private fun <T : Any> Handler.is_eq(left: Logical<T>, right: Logical<T>): Boolean {
return sessionSolver.ask(PredicateSymbol("equals", 2), left, right)
}
companion object {
@BeforeClass @JvmStatic fun setup() {
@ -54,7 +60,7 @@ class TestHandler {
handler().apply { queue(occurrence("main")) }.let { rh ->
assertEquals(
setOf(ConstraintSymbol("main", 0), ConstraintSymbol("foo", 0)),
rh.occurrences().map { it.constraint().symbol() }.toSet())
rh.allOccurrences().map { it.constraint().symbol() }.toSet())
}
}
}
@ -83,7 +89,7 @@ class TestHandler {
handler().apply { queue(occurrence("main")) }.let { rh ->
assertEquals(
setOf(ConstraintSymbol("bar", 0), ConstraintSymbol("foo", 0)),
rh.occurrences().map { it.constraint().symbol() }.toSet())
rh.allOccurrences().map { it.constraint().symbol() }.toSet())
}
}
}
@ -167,7 +173,7 @@ class TestHandler {
handler().apply { queue(occurrence("main")) }.let { rh ->
assertEquals(
setOf(ConstraintSymbol("main", 0), ConstraintSymbol("next", 0)),
rh.occurrences().map { it.constraint().symbol() }.toSet())
rh.allOccurrences().map { it.constraint().symbol() }.toSet())
assertEquals("expected", test)
}
}
@ -222,8 +228,8 @@ class TestHandler {
val a = logical<String>("a")
a.set("value")
queue(occurrence("foo", a))
assertEquals(1, occurrences().size)
val co = occurrences().first()
assertEquals(1, allOccurrences().size)
val co = allOccurrences().first()
assertEquals(ConstraintSymbol("bar",1), co.constraint().symbol())
assertEquals(1, co.arguments().size)
val arg = co.arguments().first()
@ -253,7 +259,7 @@ class TestHandler {
queue(occurrence("foo"))
assertEquals(
setOf(ConstraintSymbol("expected1", 0), ConstraintSymbol("expected2", 0)),
occurrences().map { co -> co.constraint().symbol() }.toSet())
allOccurrences().map { co -> co.constraint().symbol() }.toSet())
}
}
@ -278,7 +284,7 @@ class TestHandler {
queue(occurrence("foo"))
assertEquals(
setOf(ConstraintSymbol("expected1", 0), ConstraintSymbol("expected2", 0)),
occurrences().map { co -> co.constraint().symbol() }.toSet())
allOccurrences().map { co -> co.constraint().symbol() }.toSet())
}
}
@ -315,11 +321,11 @@ class TestHandler {
)
).handler().run {
queue(occurrence("foo"))
assertEquals(3, occurrences().count())
assertEquals(3, allOccurrences().count())
assertEquals(
setOf(ConstraintSymbol("expected1", 0), ConstraintSymbol("expected2", 0), ConstraintSymbol("expected3", 1)),
occurrences().map { co -> co.constraint().symbol() }.toSet())
val ex3 = occurrences().filter { co -> co.constraint().symbol() == ConstraintSymbol("expected3", 1) }.first()
allOccurrences().map { co -> co.constraint().symbol() }.toSet())
val ex3 = allOccurrences().filter { co -> co.constraint().symbol() == ConstraintSymbol("expected3", 1) }.first()
assertEquals(999, (ex3.arguments().first() as Logical<Int>).value())
}
}
@ -356,11 +362,11 @@ class TestHandler {
).handler().run {
handler = this
queue(occurrence("foo"))
assertEquals(3, occurrences().count())
assertEquals(3, allOccurrences().count())
assertEquals(
setOf(ConstraintSymbol("expected1", 0), ConstraintSymbol("expected2", 0), ConstraintSymbol("expected3", 1)),
occurrences().map { co -> co.constraint().symbol() }.toSet())
val ex3 = occurrences().filter { co -> co.constraint().symbol() == ConstraintSymbol("expected3", 1) }.first()
allOccurrences().map { co -> co.constraint().symbol() }.toSet())
val ex3 = allOccurrences().filter { co -> co.constraint().symbol() == ConstraintSymbol("expected3", 1) }.first()
assertEquals(123, (ex3.arguments().first() as Logical<Int>).value())
}
}
@ -397,16 +403,144 @@ class TestHandler {
).handler().run {
handler = this
queue(occurrence("foo"))
assertEquals(3, occurrences().count())
assertEquals(
setOf(ConstraintSymbol("expected1", 0), ConstraintSymbol("expected2", 0), ConstraintSymbol("expected3", 1)),
occurrences().map { co -> co.constraint().symbol() }.toSet())
val ex3 = occurrences().filter { co -> co.constraint().symbol() == ConstraintSymbol("expected3", 1) }.first()
assertEquals(3, allOccurrences().count())
assertEquals(setOf( ConstraintSymbol("expected1", 0),
ConstraintSymbol("expected2", 0),
ConstraintSymbol("expected3", 1)),
allOccurrences().map { co -> co.constraint().symbol() }.toSet())
val ex3 = allOccurrences().filter { co -> co.constraint().symbol() == ConstraintSymbol("expected3", 1) }.first()
assertEquals(123, (ex3.arguments().first() as Logical<Int>).value())
}
}
@Test
fun correctRulesOrder() {
val X= metaLogical<Int>("X")
program(
rule("main",
headReplaced( constraint("main") ), body( statement({ x -> x.set(1) }, X),
constraint("bar"),
constraint("foo", X) )
),
rule("foo_if_zero",
headReplaced( constraint("foo", X) ), guard( expression({ x -> x.get() == 0 }, X) ),
body( constraint("foo_zero") )
),
rule("foo_and_bar",
headReplaced( constraint("foo", X) ),
headKept( constraint("bar") ),
body( constraint("foo_and_bar") )
),
rule("foo_if_non_zero",
headReplaced( constraint("foo", X) ),
guard( expression({ x -> x.get() != 0 }, X) ),
body( constraint("foo_non_zero") )
)
).handler().run {
queue(occurrence("main"))
assertEquals(setOf(ConstraintSymbol("bar", 0), ConstraintSymbol("foo_and_bar", 0)), constraintSymbols())
assertEquals(1, occurrences(ConstraintSymbol("foo_and_bar", 0)).count())
assertEquals(1, occurrences(ConstraintSymbol("bar", 0)).count())
}
}
@Test
fun reactivateOnUnion() {
val (X,Y) = metaLogical<Int>("X", "Y")
val (C,D) = metaLogical<Int>("C", "D")
var handler : Handler? = null
program(
rule("main",
headReplaced( constraint("main") ), body( statement({ c -> c.set(0) }, C),
constraint("foo", X, C),
constraint("foo", Y, C),
statement({ x, y -> handler!!.eq(x, y) }, X, Y) )
),
rule("capture_foo",
headKept( constraint("foo", X, C) ),
body( statement({ c, d -> d.set(c.get() + 1) }, C, D),
constraint("capture", D) )
),
rule("capture_foo_foo",
headKept( constraint("foo", X, C) ),
headReplaced( constraint("foo", Y, C) ), guard( expression({x, y -> handler!!.is_eq(x, y) }, X, Y)),
body( constraint("replaced") )
)
).handler().run {
handler = this
queue(occurrence("main"))
assertEquals(setOf( ConstraintSymbol("foo", 2),
ConstraintSymbol("capture", 1),
ConstraintSymbol("replaced", 0)),
constraintSymbols())
assertEquals(1, occurrences(ConstraintSymbol("foo", 2)).count())
assertEquals(2, occurrences(ConstraintSymbol("capture", 1)).count())
assertEquals(1, occurrences(ConstraintSymbol("replaced", 0)).count())
}
}
@Test
fun propagationHistory() {
val (X,Y,Z) = metaLogical<Int>("X", "Y", "Z")
var handler : Handler? = null
program(
rule("main",
headReplaced( constraint("main") ), body( statement({ x, y -> handler!!.eq(x, y) }, X, Y), // rank(X) = 1
constraint("foo", Y),
constraint("bar", Z),
// update Z's parent
statement({ x, z -> handler!!.eq(x, z) }, X, Z) )
),
rule("foobar",
headKept( constraint("foo", X) ),
headKept( constraint("bar", Y) ),
body( constraint("foobar") )
)
).handler().run {
handler = this
queue(occurrence("main"))
assertEquals(setOf( ConstraintSymbol("foo", 1),
ConstraintSymbol("bar", 1),
ConstraintSymbol("foobar", 0)),
constraintSymbols())
assertEquals(1, occurrences(ConstraintSymbol("foo", 1)).count())
assertEquals(1, occurrences(ConstraintSymbol("bar", 1)).count())
assertEquals(1, occurrences(ConstraintSymbol("foobar", 0)).count())
}
}
@Test
fun reactivateOnUnionKeepValue() {
val (X,Y,Z) = metaLogical<Int>("X", "Y", "Z")
var handler : Handler? = null
program(
rule("main",
headReplaced( constraint("main") ), body( statement({ x, y -> handler!!.eq(x, y) }, X, Y), // rank(X) = 1
statement({ z -> z.set(42) }, Z),
constraint("foo", Z),
statement({ x, z -> handler!!.eq(x, z) }, X, Z) )
),
rule("capture_foo_free",
headKept( constraint("foo", X) ), guard( expression({ x -> x.getNullable() == null }, X) ),
body( constraint("free") )
),
rule("capture_foo_assigned",
headKept( constraint("foo", X) ), guard( expression({ x -> x.getNullable() != null }, X) ),
body( constraint("assigned") )
)
).handler().run {
handler = this
queue(occurrence("main"))
assertEquals(setOf( ConstraintSymbol("foo", 1),
ConstraintSymbol("assigned", 0)),
constraintSymbols())
assertEquals(1, occurrences(ConstraintSymbol("foo", 1)).count())
assertEquals(1, occurrences(ConstraintSymbol("assigned", 0)).count())
}
}
}

View File

@ -18,8 +18,8 @@ class TestMatcher {
val stored = occurrence.toList()
val aux = object : Matcher.AuxOccurrences {
override fun findOccurrences(
val aux = object : Matcher.AuxOccurrencesLookup {
override fun lookupAuxOccurrences(
symbol: ConstraintSymbol,
logicals: Iterable<Logical<*>>,
values: Iterable<Any>,

View File

@ -112,98 +112,6 @@ class TestProgram {
}
}
@Test
fun correctRulesOrder() {
val X= metaLogical<Int>("X")
program(
rule("main",
headReplaced( constraint("main") ), body( statement({ x -> x.set(1) }, X),
constraint("bar"),
constraint("foo", X) )
),
rule("foo_if_zero",
headReplaced( constraint("foo", X) ), guard( expression({ x -> x.get() == 0 }, X) ),
body( constraint("foo_zero") )
),
rule("foo_and_bar",
headReplaced( constraint("foo", X) ),
headKept( constraint("bar") ),
body( constraint("foo_and_bar") )
),
rule("foo_if_non_zero",
headReplaced( constraint("foo", X) ),
guard( expression({ x -> x.get() != 0 }, X) ),
body( constraint("foo_non_zero") )
)
).session("correctRulesOrder").run {
assertEquals(setOf(ConstraintSymbol("bar", 0), ConstraintSymbol("foo_and_bar", 0)), constraintSymbols())
assertEquals(1, constraintOccurrences(ConstraintSymbol("foo_and_bar", 0)).count())
assertEquals(1, constraintOccurrences(ConstraintSymbol("bar", 0)).count())
}
}
@Test
fun reactivateOnUnion() {
val (X,Y) = metaLogical<Int>("X", "Y")
val S = metaLogical<String>("S")
program(
rule("main",
headReplaced( constraint("main") ), body( constraint("foo", X, S),
constraint("foo", Y, S),
statement({ x, y -> x eq y }, X, Y) )
),
rule("capture_foo",
headKept( constraint("foo", X, S) ),
body( constraint("capture", S) )
),
rule("capture_foo_foo",
headKept( constraint("foo", X, S) ),
headReplaced( constraint("foo", Y, S) ), guard( expression({x, y -> x is_eq y }, X, Y)),
body( constraint("replaced") )
)
).session("reactivateOnUnion").run {
assertEquals(setOf( ConstraintSymbol("foo", 2),
ConstraintSymbol("capture", 1),
ConstraintSymbol("replaced", 0)),
constraintSymbols())
assertEquals(1, constraintOccurrences(ConstraintSymbol("foo", 2)).count())
// FIXME: this count should be 2 instead as per the "activation history" feature
assertEquals(3, constraintOccurrences(ConstraintSymbol("capture", 1)).count())
assertEquals(1, constraintOccurrences(ConstraintSymbol("replaced", 0)).count())
}
}
@Test
fun reactivateOnUnionKeepValue() {
val (X,Y,Z) = metaLogical<Int>("X", "Y", "Z")
program(
rule("main",
headReplaced( constraint("main") ), body( statement({ x, y -> x eq y }, X, Y), // rank(X) = 1
statement({ z -> z.set(42) }, Z),
constraint("foo", Z),
statement({ x, z -> x eq z }, X, Z) )
),
rule("capture_foo_free",
headKept( constraint("foo", X) ), guard( expression({x -> x.getNullable() == null }, X) ),
body( constraint("free") )
),
rule("capture_foo_assigned",
headKept( constraint("foo", X) ), guard( expression({x -> x.getNullable() != null }, X) ),
body( constraint("assigned") )
)
).session("reactivateOnUnionKeepValue").run {
assertEquals(setOf( ConstraintSymbol("foo", 1),
ConstraintSymbol("assigned", 0)),
constraintSymbols())
assertEquals(1, constraintOccurrences(ConstraintSymbol("foo", 1)).count())
// FIXME: this count should be 1 instead as per the "activation history" feature (??? not sure)
assertEquals(2, constraintOccurrences(ConstraintSymbol("assigned", 0)).count())
}
}
@Test
fun gcd() {
val (M, N, TMP) = metaLogical<Int>("M", "N", "TMP")