From 7021a4d1f2805ebf3145cbc3893761d12f23361f Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 1 Aug 2019 01:00:12 +0200 Subject: Configurability and better statistics for measurements --- .../ModelGenerationMethodProvider.xtend | 54 ++++++++++++++---- .../cardinality/PolyhedronScopePropagator.xtend | 33 ++++++++++- .../cardinality/RelationConstraintCalculator.xtend | 7 ++- .../logic2viatra/cardinality/ScopePropagator.xtend | 22 ++++++-- .../cardinality/ScopePropagatorStrategy.java | 18 ------ .../cardinality/ScopePropagatorStrategy.xtend | 64 ++++++++++++++++++++++ .../logic2viatra/patterns/PatternProvider.xtend | 2 +- .../rules/RefinementRuleProvider.xtend | 40 ++++++++++---- .../viatrasolver/reasoner/ViatraReasoner.xtend | 28 ++++++++-- .../reasoner/ViatraReasonerConfiguration.xtend | 8 ++- .../dse/BestFirstStrategyForModelGeneration.java | 1 + 11 files changed, 217 insertions(+), 60 deletions(-) delete mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend (limited to 'Solvers') 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 4b278188..8e061b63 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 @@ -27,6 +27,7 @@ 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 @@ -35,7 +36,25 @@ class ModelGenerationStatistics { transformationExecutionTime += amount } - public var long PreliminaryTypeAnalisisTime = 0 + public var long scopePropagationTime = 0 + + synchronized def addScopePropagationTime(long amount) { + scopePropagationTime += amount + } + + public var long preliminaryTypeAnalisisTime = 0 + + public var int decisionsTried = 0 + + synchronized def incrementDecisionCount() { + decisionsTried++ + } + + public var int scopePropagatorInvocations + + synchronized def incrementScopePropagationCount() { + scopePropagatorInvocations++ + } } @Data class ModelGenerationMethod { @@ -84,12 +103,12 @@ class ModelGenerationMethodProvider { val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles) - val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries) + val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries, statistics) scopePropagator.propagateAllScopeConstraints - val // LinkedHashMap, BatchTransformationRule>> - objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, + val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, nameNewElements, statistics) - val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, statistics) + val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator, + statistics) val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) val unfinishedWF = queries.getUnfinishedWFQueries.values @@ -118,15 +137,26 @@ class ModelGenerationMethodProvider { } private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, - PartialInterpretation emptySolution, GeneratedPatterns queries) { + PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) { switch (scopePropagatorStrategy) { - case BasicTypeHierarchy: - new ScopePropagator(emptySolution) - case PolyhedralTypeHierarchy, - case PolyhedralRelations: { + case ScopePropagatorStrategy.BasicTypeHierarchy: + new ScopePropagator(emptySolution, statistics) + ScopePropagatorStrategy.Polyhedral: { val types = queries.refineObjectQueries.keySet.map[newType].toSet - val solver = new CbcPolyhedronSolver - new PolyhedronScopePropagator(emptySolution, types, queries.multiplicityConstraintQueries, + val solver = switch (scopePropagatorStrategy.solver) { + case Z3Integer: + new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) + case Z3Real: + new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) + case Cbc: + new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) + case Clp: + new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) + default: + throw new IllegalArgumentException("Unknown polyhedron solver: " + + scopePropagatorStrategy.solver) + } + new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing) } default: 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 f6b101b6..e7e40ab0 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 @@ -2,9 +2,12 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality import com.google.common.collect.ImmutableList import com.google.common.collect.ImmutableMap +import com.google.common.collect.ImmutableSet import com.google.common.collect.Maps import com.google.common.collect.Sets +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnifinishedMultiplicityQueries import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation @@ -30,13 +33,14 @@ class PolyhedronScopePropagator extends ScopePropagator { val LinearBoundedExpression topLevelBounds val Polyhedron polyhedron val PolyhedronSaturationOperator operator + val Set relevantRelations List updaters = emptyList - new(PartialInterpretation p, Set possibleNewDynamicTypes, + new(PartialInterpretation p, ModelGenerationStatistics statistics, Set possibleNewDynamicTypes, Map unfinishedMultiplicityQueries, IQuerySpecification> hasElementInContainmentQuery, PolyhedronSolver solver, boolean propagateRelations) { - super(p) + super(p, statistics) val builder = new PolyhedronBuilder(p) builder.buildPolyhedron(possibleNewDynamicTypes) scopeBounds = builder.scopeBounds @@ -54,11 +58,14 @@ class PolyhedronScopePropagator extends ScopePropagator { } builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, maximumNumberOfNewNodes) + relevantRelations = builder.relevantRelations updaters = builder.updaters + } else { + relevantRelations = emptySet } } - override void propagateAllScopeConstraints() { + override void doPropagateAllScopeConstraints() { resetBounds() populatePolyhedronFromScope() // println(polyhedron) @@ -73,6 +80,13 @@ class PolyhedronScopePropagator extends ScopePropagator { } } } + + override propagateAdditionToRelation(Relation r) { + super.propagateAdditionToRelation(r) + if (relevantRelations.contains(r)) { + propagateAllScopeConstraints() + } + } def resetBounds() { for (dimension : polyhedron.dimensions) { @@ -188,6 +202,7 @@ class PolyhedronScopePropagator extends ScopePropagator { Map scopeBounds LinearBoundedExpression topLevelBounds Polyhedron polyhedron + Set relevantRelations List updaters def buildPolyhedron(Set possibleNewDynamicTypes) { @@ -222,9 +237,21 @@ class PolyhedronScopePropagator extends ScopePropagator { buildNonContainmentConstraints(constraint, pair.value) } } + buildRelevantRelations(constraints.keySet) updaters = updatersBuilder.build addCachedConstraintsToPolyhedron() } + + private def buildRelevantRelations(Set constraints) { + val builder = ImmutableSet.builder + for (constraint : constraints) { + builder.add(constraint.relation) + if (constraint.inverseRelation !== null) { + builder.add(constraint.inverseRelation) + } + } + relevantRelations = builder.build + } private def addCachedConstraintsToPolyhedron() { val constraints = new HashSet diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend index ffa9e6e6..52a390a8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend @@ -20,6 +20,7 @@ class RelationConstraints { @Data class RelationMultiplicityConstraint { Relation relation + Relation inverseRelation boolean containment boolean container int lowerBound @@ -47,7 +48,7 @@ class RelationMultiplicityConstraint { } def constrainsRemainingInverse() { - !containment && inverseUpperBoundFinite + lowerBound >= 1 && !containment && inverseUpperBoundFinite } def constrainsRemainingContents() { @@ -119,8 +120,8 @@ class RelationConstraintCalculator { inverseUpperMultiplicity = upperMultiplicities.get(relation) container = containmentRelations.contains(inverseRelation) } - val constraint = new RelationMultiplicityConstraint(relation, containment, container, lowerMultiplicity, - upperMultiplicity, inverseUpperMultiplicity) + val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container, + lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity) if (constraint.isActive) { if (relation.parameters.size != 2) { throw new IllegalArgumentException('''Relation «relation.name» has multiplicity or containment constraints, but it is not binary''') 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 3b442cd3..7be6635c 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 @@ -1,5 +1,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation @@ -11,14 +13,15 @@ import java.util.Set import org.eclipse.xtend.lib.annotations.Accessors class ScopePropagator { - @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation - Map type2Scope - + @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation + val ModelGenerationStatistics statistics + val Map type2Scope val Map> superScopes val Map> subScopes - new(PartialInterpretation p) { + new(PartialInterpretation p, ModelGenerationStatistics statistics) { partialInterpretation = p + this.statistics = statistics type2Scope = new HashMap for (scope : p.scopes) { type2Scope.put(scope.targetTypeInterpretation, scope) @@ -57,8 +60,13 @@ class ScopePropagator { } } while (changed) } - + def propagateAllScopeConstraints() { + statistics.incrementScopePropagationCount() + doPropagateAllScopeConstraints() + } + + protected def doPropagateAllScopeConstraints() { var boolean hadChanged do { hadChanged = false @@ -95,6 +103,10 @@ 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) { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java deleted file mode 100644 index b1c5a658..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java +++ /dev/null @@ -1,18 +0,0 @@ -package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality; - -public enum ScopePropagatorStrategy { - BasicTypeHierarchy, - - PolyhedralTypeHierarchy, - - PolyhedralRelations { - @Override - public boolean requiresUpperBoundIndexing() { - return true; - } - }; - - public boolean requiresUpperBoundIndexing() { - return false; - } -} 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 new file mode 100644 index 00000000..37e56c9a --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend @@ -0,0 +1,64 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import org.eclipse.xtend.lib.annotations.Data +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +enum PolyhedralScopePropagatorConstraints { + TypeHierarchy, + Relational +} + +enum PolyhedralScopePropagatorSolver { + Z3Real, + Z3Integer, + Cbc, + Clp +} + +abstract class ScopePropagatorStrategy { + public static val BasicCount = new Simple("BasicCount") + + public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") + + private new() { + } + + def boolean requiresUpperBoundIndexing() + + static class Simple extends ScopePropagatorStrategy { + val String name + + @FinalFieldsConstructor + private new() { + } + + override requiresUpperBoundIndexing() { + false + } + + override toString() { + name + } + } + + @Data + static class Polyhedral extends ScopePropagatorStrategy { + public static val UNLIMITED_TIME = -1 + + val PolyhedralScopePropagatorConstraints constraints + val PolyhedralScopePropagatorSolver solver + val double timeoutSeconds + + @FinalFieldsConstructor + new() { + } + + new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) { + this(constraints, solver, UNLIMITED_TIME) + } + + override requiresUpperBoundIndexing() { + constraints == PolyhedralScopePropagatorConstraints.Relational + } + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index b10c8e88..eadf0ae0 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend @@ -69,7 +69,7 @@ class PatternProvider { val startTime = System.nanoTime val result = typeAnalysis.performTypeAnalysis(problem, emptySolution) val typeAnalysisTime = System.nanoTime - startTime - statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime + statistics.preliminaryTypeAnalisisTime = typeAnalysisTime result } else { null diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index 5fefa551..bf816de9 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend @@ -98,10 +98,12 @@ class RefinementRuleProvider { val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container] inverseRelationInterpretation.relationlinks+=newLink2 + val propagatorStartTime = System.nanoTime + statistics.addExecutionTime(propagatorStartTime-startTime) + // Scope propagation scopePropagator.propagateAdditionToType(typeInterpretation) - - statistics.addExecutionTime(System.nanoTime-startTime) + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) ] } else { ruleBuilder.action[match | @@ -132,10 +134,12 @@ class RefinementRuleProvider { val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] relationInterpretation.relationlinks+=newLink + val propagatorStartTime = System.nanoTime + statistics.addExecutionTime(propagatorStartTime-startTime) + // Scope propagation scopePropagator.propagateAdditionToType(typeInterpretation) - - statistics.addExecutionTime(System.nanoTime-startTime) + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) ] } } else { @@ -162,29 +166,31 @@ class RefinementRuleProvider { typeInterpretation.elements += newElement typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] + val propagatorStartTime = System.nanoTime + statistics.addExecutionTime(propagatorStartTime-startTime) + // Scope propagation scopePropagator.propagateAdditionToType(typeInterpretation) - - statistics.addExecutionTime(System.nanoTime-startTime) + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) ] } return ruleBuilder.build } - def createRelationRefinementRules(GeneratedPatterns patterns, ModelGenerationStatistics statistics) { + def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { val res = new LinkedHashMap for(LHSEntry: patterns.refinerelationQueries.entrySet) { val declaration = LHSEntry.key.key val inverseReference = LHSEntry.key.value val lhs = LHSEntry.value as IQuerySpecification> - val rule = createRelationRefinementRule(declaration,inverseReference,lhs,statistics) + val rule = createRelationRefinementRule(declaration,inverseReference,lhs,scopePropagator,statistics) res.put(LHSEntry.key,rule) } return res } def private BatchTransformationRule> - createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification> lhs, ModelGenerationStatistics statistics) + createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification> lhs, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation != null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' val ruleBuilder = factory.createRule @@ -201,7 +207,13 @@ class RefinementRuleProvider { val trg = match.get(4) as DefinedElement val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] relationInterpretation.relationlinks += link - statistics.addExecutionTime(System.nanoTime-startTime) + + val propagatorStartTime = System.nanoTime + statistics.addExecutionTime(propagatorStartTime-startTime) + + // Scope propagation + scopePropagator.propagateAdditionToRelation(declaration) + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) ] } else { ruleBuilder.action [ match | @@ -217,7 +229,13 @@ class RefinementRuleProvider { relationInterpretation.relationlinks += link val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src] inverseInterpretation.relationlinks += inverseLink - statistics.addExecutionTime(System.nanoTime-startTime) + + val propagatorStartTime = System.nanoTime + statistics.addExecutionTime(propagatorStartTime-startTime) + + // Scope propagation + scopePropagator.propagateAdditionToRelation(declaration) + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) ] } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index a8db5e43..1abde0a8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend @@ -39,6 +39,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel import org.eclipse.viatra.dse.solutionstore.SolutionStore import org.eclipse.viatra.dse.statecode.IStateCoderFactory +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory class ViatraReasoner extends LogicReasoner { val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() @@ -137,11 +138,14 @@ class ViatraReasoner extends LogicReasoner { dse.setInitialModel(emptySolution, false) - val IStateCoderFactory statecoder = if (viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) { + val IStateCoderFactory statecoder = switch (viatraConfig.stateCoderStrategy) { + case Neighbourhood: + new NeighbourhoodBasedStateCoderFactory + case PairwiseNeighbourhood: new PairwiseNeighbourhoodBasedStateCoderFactory - } else { + default: new IdentifierBasedStateCoderFactory - } + } dse.stateCoderFactory = statecoder dse.maxNumberOfThreads = 1 @@ -183,9 +187,13 @@ class ViatraReasoner extends LogicReasoner { it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime / 1000000) as int ] + it.entries += createIntStatisticEntry => [ + it.name = "ScopePropagationTime" + it.value = (method.statistics.scopePropagationTime / 1000000) as int + ] it.entries += createIntStatisticEntry => [ it.name = "TypeAnalysisTime" - it.value = (method.statistics.PreliminaryTypeAnalisisTime / 1000000) as int + it.value = (method.statistics.preliminaryTypeAnalisisTime / 1000000) as int ] it.entries += createIntStatisticEntry => [ it.name = "StateCoderTime" @@ -199,6 +207,18 @@ class ViatraReasoner extends LogicReasoner { it.name = "SolutionCopyTime" it.value = (solutionCopier.getTotalCopierRuntime / 1000000) as int ] + it.entries += createIntStatisticEntry => [ + it.name = "States" + it.value = dse.numberOfStates as int + ] + it.entries += createIntStatisticEntry => [ + it.name = "Decisions" + it.value = method.statistics.decisionsTried + ] + it.entries += createIntStatisticEntry => [ + it.name = "ScopePropagations" + it.value = method.statistics.scopePropagatorInvocations + ] if (diversityChecker.isActive) { it.entries += createIntStatisticEntry => [ it.name = "SolutionDiversityCheckTime" diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index 7a3a2d67..a2f9cebe 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend @@ -14,9 +14,12 @@ import java.util.LinkedList import java.util.List import java.util.Set import org.eclipse.xtext.xbase.lib.Functions.Function1 +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver enum StateCoderStrategy { Neighbourhood, + PairwiseNeighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity @@ -25,7 +28,7 @@ enum StateCoderStrategy { class ViatraReasonerConfiguration extends LogicSolverConfiguration { // public var Iterable existingQueries public var nameNewElements = false - public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood + public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.PairwiseNeighbourhood public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis /** * Once per 1/randomBacktrackChance the search selects a random state. @@ -50,9 +53,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { * Configuration for cutting search space. */ public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint - - public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.PolyhedralTypeHierarchy + public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.BasicTypeHierarchy public var List costObjectives = newArrayList } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index 144e7484..5af7fc69 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java @@ -189,6 +189,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // } logger.debug("Executing new activation: " + nextActivation); context.executeAcitvationId(nextActivation); + method.getStatistics().incrementDecisionCount(); visualiseCurrentState(); // for(ViatraQueryMatcher matcher : matchers) { -- cgit v1.2.3-54-g00ecf