From c300e9e7918aa71b04cb681c558eb282dd1fb390 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 1 Aug 2019 14:45:26 +0200 Subject: Counting scope propagator (simpler than BasicTypeHierarchy) --- .../ModelGenerationMethodProvider.xtend | 7 +- .../cardinality/PolyhedronScopePropagator.xtend | 2 +- .../logic2viatra/cardinality/ScopePropagator.xtend | 73 ++------------------ .../cardinality/ScopePropagatorStrategy.xtend | 2 +- .../cardinality/TypeHierarchyScopePropagator.xtend | 77 ++++++++++++++++++++++ 5 files changed, 90 insertions(+), 71 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index 8e061b63..23632d4d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend @@ -10,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider @@ -27,7 +29,6 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule import org.eclipse.xtend.lib.annotations.Data -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver class ModelGenerationStatistics { public var long transformationExecutionTime = 0 @@ -139,8 +140,10 @@ class ModelGenerationMethodProvider { private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) { switch (scopePropagatorStrategy) { - case ScopePropagatorStrategy.BasicTypeHierarchy: + case ScopePropagatorStrategy.Count: new ScopePropagator(emptySolution, statistics) + case ScopePropagatorStrategy.BasicTypeHierarchy: + new TypeHierarchyScopePropagator(emptySolution, statistics) ScopePropagatorStrategy.Polyhedral: { val types = queries.refineObjectQueries.keySet.map[newType].toSet val solver = switch (scopePropagatorStrategy.solver) { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index e7e40ab0..7c05e818 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend @@ -28,7 +28,7 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher import org.eclipse.viatra.query.runtime.emf.EMFScope import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor -class PolyhedronScopePropagator extends ScopePropagator { +class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { val Map scopeBounds val LinearBoundedExpression topLevelBounds val Polyhedron polyhedron diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend index 7be6635c..0bdb202e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend @@ -16,8 +16,8 @@ class ScopePropagator { @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation val ModelGenerationStatistics statistics val Map type2Scope - val Map> superScopes - val Map> subScopes + @Accessors(PROTECTED_GETTER) val Map> superScopes + @Accessors(PROTECTED_GETTER) val Map> subScopes new(PartialInterpretation p, ModelGenerationStatistics statistics) { partialInterpretation = p @@ -60,26 +60,14 @@ class ScopePropagator { } } while (changed) } - + def propagateAllScopeConstraints() { statistics.incrementScopePropagationCount() doPropagateAllScopeConstraints() } - protected def doPropagateAllScopeConstraints() { - var boolean hadChanged - do { - hadChanged = false - for (superScopeEntry : superScopes.entrySet) { - val sub = superScopeEntry.key - hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged - hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged - for (sup : superScopeEntry.value) { - hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged - hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged - } - } - } while (hadChanged) + protected def void doPropagateAllScopeConstraints() { + // Nothing to propagate. } def propagateAdditionToType(PartialTypeInterpratation t) { @@ -103,60 +91,11 @@ class ScopePropagator { // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') } - + def void propagateAdditionToRelation(Relation r) { // Nothing to propagate. } - private def propagateLowerLimitUp(Scope subScope, Scope superScope) { - if (subScope.minNewElements > superScope.minNewElements) { - superScope.minNewElements = subScope.minNewElements - return true - } else { - return false - } - } - - private def propagateUpperLimitDown(Scope subScope, Scope superScope) { - if (superScope.maxNewElements >= 0 && - (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { -// println(''' -// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -// subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» -// ''') - subScope.maxNewElements = superScope.maxNewElements - return true - } else { - return false - } - } - - private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { - if (subScope.minNewElements > p.minNewElements) { -// println(''' -// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes -// p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» -// ''') - p.minNewElements = subScope.minNewElements - return true - } else { - return false - } - } - - private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { - if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { -// println(''' -// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes -// subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» -// ''') - subScope.maxNewElements = p.maxNewElements - return true - } else { - return false - } - } - private def removeOne(Scope scope) { if (scope.maxNewElements === 0) { throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend index 37e56c9a..b0ed75cb 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend @@ -16,7 +16,7 @@ enum PolyhedralScopePropagatorSolver { } abstract class ScopePropagatorStrategy { - public static val BasicCount = new Simple("BasicCount") + public static val Count = new Simple("Count") public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend new file mode 100644 index 00000000..be8ef00a --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend @@ -0,0 +1,77 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope + +class TypeHierarchyScopePropagator extends ScopePropagator { + + new(PartialInterpretation p, ModelGenerationStatistics statistics) { + super(p, statistics) + } + + protected override doPropagateAllScopeConstraints() { + var boolean hadChanged + do { + hadChanged = false + for (superScopeEntry : superScopes.entrySet) { + val sub = superScopeEntry.key + hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged + hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged + for (sup : superScopeEntry.value) { + hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged + hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged + } + } + } while (hadChanged) + } + + private def propagateLowerLimitUp(Scope subScope, Scope superScope) { + if (subScope.minNewElements > superScope.minNewElements) { + superScope.minNewElements = subScope.minNewElements + return true + } else { + return false + } + } + + private def propagateUpperLimitDown(Scope subScope, Scope superScope) { + if (superScope.maxNewElements >= 0 && + (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» +// subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» +// ''') + subScope.maxNewElements = superScope.maxNewElements + return true + } else { + return false + } + } + + private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { + if (subScope.minNewElements > p.minNewElements) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes +// p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» +// ''') + p.minNewElements = subScope.minNewElements + return true + } else { + return false + } + } + + private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { + if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes +// subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» +// ''') + subScope.maxNewElements = p.maxNewElements + return true + } else { + return false + } + } +} -- cgit v1.2.3-54-g00ecf