From 4fe7fce97aedbd516109ef81afc33e00112b7b68 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 28 Aug 2020 18:58:37 +0200 Subject: Must unit propagation --- .../ModelGenerationMethodProvider.xtend | 14 +- .../cardinality/LinearTypeConstraintHint.xtend | 4 +- .../logic2viatra/cardinality/ScopePropagator.xtend | 14 +- .../logic2viatra/patterns/PatternGenerator.xtend | 4 +- .../logic2viatra/patterns/PatternProvider.xtend | 11 +- .../patterns/RelationDeclarationIndexer.xtend | 2 +- .../patterns/RelationRefinementGenerator.xtend | 137 ++++++--- .../rules/RefinementRuleProvider.xtend | 338 +++++++++++++++------ .../viatrasolver/reasoner/ViatraReasoner.xtend | 4 + .../dse/BestFirstStrategyForModelGeneration.java | 4 +- 10 files changed, 384 insertions(+), 148 deletions(-) (limited to 'Solvers/VIATRA-Solver') 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 431ae386..3bcd9116 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 @@ -49,6 +49,12 @@ class ModelGenerationStatistics { synchronized def addScopePropagationTime(long amount) { scopePropagationTime += amount } + + public var long mustRelationPropagationTime = 0 + + synchronized def addMustRelationPropagationTime(long amount) { + mustRelationPropagationTime += amount + } public var long preliminaryTypeAnalisisTime = 0 @@ -133,9 +139,11 @@ class ModelGenerationMethodProvider { val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) scopePropagator.propagateAllScopeConstraints + val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, + queries, scopePropagator, statistics) val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, - queries, scopePropagator, nameNewElements, statistics) - val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator, + queries, unitRulePropagator, nameNewElements, statistics) + val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator, statistics) val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, @@ -158,7 +166,7 @@ class ModelGenerationMethodProvider { val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( - queries.refineTypeQueries.values).addAll(queries.refinerelationQueries.values).addAll(queries. + queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll(queries. multiplicityConstraintQueries.values.flatMap[allQueries]).addAll(queries.unfinishedWFQueries.values).addAll( queries.invalidWFQueries.values).addAll(queries.mustUnitPropagationPreconditionPatterns.values).addAll( queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend index 8c21ca1d..31f98e36 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend @@ -3,8 +3,10 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import java.util.Map import org.eclipse.viatra.query.runtime.api.IPatternMatch import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery interface LinearTypeExpressionBuilderFactory { def ViatraQueryMatcher createMatcher(String queryName) @@ -24,7 +26,7 @@ interface RelationConstraintUpdater { } interface LinearTypeConstraintHint { - def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator) + def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator, Map fqnToPQuery) def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) } 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 93b83577..cacba3c6 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 @@ -19,6 +19,8 @@ class ScopePropagator { val Map type2Scope @Accessors(PROTECTED_GETTER) val Map> superScopes @Accessors(PROTECTED_GETTER) val Map> subScopes + + @Accessors(PUBLIC_GETTER) var scopePropagationNeeded = false new(PartialInterpretation p, ModelGenerationStatistics statistics) { partialInterpretation = p @@ -64,7 +66,8 @@ class ScopePropagator { copyScopeBoundsToHeuristic() } - def propagateAllScopeConstraints() { + def void propagateAllScopeConstraints() { + scopePropagationNeeded = false if (!valid) { return } @@ -93,6 +96,7 @@ class ScopePropagator { if (isPrimitive) { return } + scopePropagationNeeded = true // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') val targetScope = type2Scope.get(t) if (targetScope !== null) { @@ -117,6 +121,12 @@ 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 addedToRelation(Relation r) { + if (isPropagationNeededAfterAdditionToRelation(r)) { + scopePropagationNeeded = true + } + } protected def setScopesInvalid() { partialInterpretation.minNewElements = Integer.MAX_VALUE @@ -127,7 +137,7 @@ class ScopePropagator { } } - def isPropagationNeededAfterAdditionToRelation(Relation r) { + protected def isPropagationNeededAfterAdditionToRelation(Relation r) { false } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index a3efcf76..edf92343 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend @@ -369,13 +369,13 @@ class PatternGenerator { ////////// // 4.3 Relation refinement ////////// - «relationRefinementGenerator.generateRefineReference(problem)» + «relationRefinementGenerator.generateRefineReference(problem, unitPropagationPatternGenerators)» ////////// // 5 Hints ////////// «FOR hint : hints» - «hint.getAdditionalPatterns(this)» + «hint.getAdditionalPatterns(this, fqn2PQuery)» «ENDFOR» «FOR generator : unitPropagationPatternGenerators» «generator.getAdditionalPatterns(this, fqn2PQuery)» 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 21fd1989..2e786286 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 @@ -38,7 +38,8 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* public IQuerySpecification> hasElementInContainmentQuery public Map>> refineObjectQueries public Map>> refineTypeQueries - public Map, IQuerySpecification>> refinerelationQueries + public Map, IQuerySpecification>> refineRelationQueries + public Map, IQuerySpecification>> mustRelationPropagationQueries public Map>> mustUnitPropagationPreconditionPatterns public Map>> currentUnitPropagationPreconditionPatterns public Map modalRelationQueries @@ -70,7 +71,6 @@ class UnifinishedMultiplicityQueries { } class PatternProvider { - val TypeAnalysis typeAnalysis = new TypeAnalysis def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, @@ -98,7 +98,8 @@ class PatternProvider { val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText) val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, patternGeneratorResult.constraint2MustPreconditionName, - patternGeneratorResult.constraint2CurrentPreconditionName, relationConstraints, generatedQueries) + patternGeneratorResult.constraint2CurrentPreconditionName, relationConstraints, + unitPropagationPatternGenerators, generatedQueries) return runtimeQueries } @@ -110,6 +111,7 @@ class PatternProvider { HashMap mustUnitPropagationTrace, HashMap currentUnitPropagationTrace, RelationConstraints relationConstraints, + Collection unitPropagationPatternGenerators, Map>> queries ) { val Map>> invalidWFQueries = patternGenerator. @@ -136,6 +138,8 @@ class PatternProvider { ] val Map, IQuerySpecification>> refineRelationQueries = patternGenerator. relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] + val Map, IQuerySpecification>> mustRelationPropagationQueries = patternGenerator. + relationRefinementGenerator.getMustPropagationQueries(problem, unitPropagationPatternGenerators).mapValues[it.lookup(queries)] val Map>> mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace. mapValues[it.lookup(queries)] val Map>> currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace. @@ -158,6 +162,7 @@ class PatternProvider { refineObjectsQueries, refineTypeQueries, refineRelationQueries, + mustRelationPropagationQueries, mustUnitPropagationPreconditionPatterns, currentUnitPropagationPreconditionPatterns, modalRelationQueries, diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend index 29d3eb61..23ba3cad 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend @@ -113,7 +113,7 @@ class RelationDeclarationIndexer { // 2. Circle in the containment hierarchy neg «base.containmentIndexer.referTransitiveMustContains("source","target")» «ENDIF» - «IF mustNotRelations.empty» + «IF !mustNotRelations.empty» // ![] unit propagation relations «FOR mustNotRelation : mustNotRelations» neg find «mustNotRelation»(problem, interpretation, source, target); diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend index 783cd36b..6f5f2402 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend @@ -1,10 +1,17 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns +import com.google.common.collect.ImmutableList +import com.google.common.collect.ImmutableMap +import com.google.common.collect.ImmutableSet import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import java.util.Collection import java.util.LinkedList +import java.util.Map +import java.util.Set +import org.eclipse.xtend2.lib.StringConcatenationClient class RelationRefinementGenerator { PatternGenerator base; @@ -13,53 +20,61 @@ class RelationRefinementGenerator { this.base = base } - def CharSequence generateRefineReference(LogicProblem p) ''' - «FOR relationRefinement : this.getRelationRefinements(p)» - pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( - problem:LogicProblem, interpretation:PartialInterpretation, - relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», - from: DefinedElement, to: DefinedElement) - { - find interpretation(problem,interpretation); - PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); - PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); - «IF relationRefinement.value !== null» - PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); - PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); + def CharSequence generateRefineReference(LogicProblem p, + Collection unitPropagationPatternGenerators) { + val mustRelations = getMustRelations(unitPropagationPatternGenerators) + + ''' + «FOR relationRefinement : this.getRelationRefinements(p)» + pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», + from: DefinedElement, to: DefinedElement) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); + PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); + «IF relationRefinement.value !== null» + PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); + PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); + «ENDIF» + find mustExist(problem, interpretation, from); + find mustExist(problem, interpretation, to); + «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» + «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» + «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» + neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» + } + + «IF isMustPropagationQueryNeeded(relationRefinement.key, relationRefinement.value, mustRelations)» + pattern «mustPropagationQueryName(relationRefinement.key)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», + from: DefinedElement, to: DefinedElement) + «FOR body : getMustPropagationBodies(relationRefinement.key, relationRefinement.value, mustRelations) SEPARATOR " or "» + { + «referRefinementQuery(relationRefinement.key, relationRefinement.value, "relationIterpretation", "oppositeInterpretation", "from", "to")» + «body» + } + «ENDFOR» «ENDIF» - find mustExist(problem, interpretation, from); - find mustExist(problem, interpretation, to); - «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» - «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» - «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» - neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» - } - «ENDFOR» - ''' + «ENDFOR» + ''' + } def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { '''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' } + def String mustPropagationQueryName(RelationDeclaration relation) { + '''mustPropagation_«base.canonizeName(relation.name)»''' + } + def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, String inverseInterpretationName, String sourceName, String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);''' def getRefineRelationQueries(LogicProblem p) { -// val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet -// p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»'''] - /* - * val res = new LinkedHashMap - * for(relation: getRelationRefinements(p)) { - * if(inverseRelations.containsKey(relation)) { - * val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»''' - * res.put(relation -> inverseRelations.get(relation),name) - * } else { - * val name = '''refineRelation_«base.canonizeName(relation.name)»''' - * res.put(relation -> null,name) - * } - * } - return res*/ getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)] } @@ -83,4 +98,54 @@ class RelationRefinementGenerator { } return list } + + def getMustPropagationQueries(LogicProblem p, + Collection unitPropagationPatternGenerators) { + val refinements = getRelationRefinements(p) + val mustRelations = getMustRelations(unitPropagationPatternGenerators) + refinements.filter[isMustPropagationQueryNeeded(key, value, mustRelations)].toInvertedMap [ + mustPropagationQueryName(key) + ] + } + + private def getMustRelations(Collection unitPropagationPatternGenerators) { + ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustPatterns.entrySet].groupBy[key].mapValues [ + ImmutableSet.copyOf(map[value]) + ]) + } + + private def isMustPropagationQueryNeeded(Relation relation, Relation inverseRelation, + Map> mustRelations) { + val mustSet = mustRelations.get(relation) + if (mustSet !== null && !mustSet.empty) { + return true + } + if (inverseRelation !== null) { + val inverseMustSet = mustRelations.get(inverseRelation) + if (inverseMustSet !== null && !inverseMustSet.empty) { + return true + } + } + false + } + + private def getMustPropagationBodies(Relation relation, Relation inverseRelation, + Map> mustRelations) { + val builder = ImmutableList.builder() + val mustSet = mustRelations.get(relation) + if (mustSet !== null) { + for (refinementQuery : mustSet) { + builder.add('''find «refinementQuery»(problem, interpretation, from, to);''') + } + } + if (inverseRelation !== null && inverseRelation != relation) { + val inverseMustSet = mustRelations.get(inverseRelation) + if (inverseMustSet !== null) { + for (refinementQuery : inverseMustSet) { + builder.add('''find «refinementQuery»(problem, interpretation, to, from);''') + } + } + } + builder.build + } } 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 699b095d..dca10baf 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 @@ -1,5 +1,6 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules +import com.google.common.collect.ImmutableList import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference @@ -29,12 +30,14 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory import java.lang.reflect.Field import java.util.HashMap +import java.util.Iterator import java.util.LinkedHashMap import java.util.LinkedList import java.util.List import java.util.Map import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine import org.eclipse.viatra.query.runtime.api.GenericPatternMatch +import org.eclipse.viatra.query.runtime.api.IPatternMatch import org.eclipse.viatra.query.runtime.api.IQuerySpecification import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher @@ -43,6 +46,7 @@ import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory import org.eclipse.xtend.lib.annotations.Data +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor import org.eclipse.xtext.xbase.lib.Functions.Function0 class RefinementRuleProvider { @@ -50,57 +54,55 @@ class RefinementRuleProvider { val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE - var AdvancedViatraQueryEngine queryEngine - var Field delayMessageDelivery - def canonizeName(String name) { return name.replace(' ', '_') } + def createUnitPrulePropagator(LogicProblem p, PartialInterpretation i, GeneratedPatterns patterns, + ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { + new UnitRulePropagator(p, i, this, scopePropagator, patterns.mustRelationPropagationQueries, statistics) + } + def LinkedHashMap>> createObjectRefinementRules( LogicProblem p, PartialInterpretation i, GeneratedPatterns patterns, - ScopePropagator scopePropagator, + UnitRulePropagator unitRulePropagator, boolean nameNewElement, ModelGenerationStatistics statistics ) { val res = new LinkedHashMap val recursiveObjectCreation = recursiveObjectCreation(p, i) - queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine - delayMessageDelivery = queryEngine.class.getDeclaredField("delayMessageDelivery") - delayMessageDelivery.accessible = true for (LHSEntry : patterns.refineObjectQueries.entrySet) { val containmentRelation = LHSEntry.key.containmentRelation val inverseRelation = LHSEntry.key.inverseContainment val type = LHSEntry.key.newType val lhs = LHSEntry.value as IQuerySpecification> val rule = createObjectCreationRule(p, containmentRelation, inverseRelation, type, - recursiveObjectCreation.get(type), lhs, nameNewElement, scopePropagator, statistics) + recursiveObjectCreation.get(type), lhs, nameNewElement, unitRulePropagator, statistics) res.put(LHSEntry.key, rule) } return res } def private createObjectCreationRule(LogicProblem p, Relation containmentRelation, Relation inverseRelation, - Type type, List recursiceObjectCreations, + Type type, List recursiveObjectCreations, IQuerySpecification> lhs, boolean nameNewElement, - ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { + UnitRulePropagator unitRulePropagator, ModelGenerationStatistics statistics) { val name = '''addObject_«type.name.canonizeName»«IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' val ruleBuilder = factory.createRule(lhs).name(name) if (containmentRelation !== null) { if (inverseRelation !== null) { ruleBuilder.action [ match | statistics.incrementTransformationCount -// println(name) +// println(name) + val startTime = System.nanoTime // val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation val inverseRelationInterpretation = match.get(3) as PartialRelationInterpretation val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation val container = match.get(5) as DefinedElement - - val startTime = System.nanoTime createObjectActionWithContainmentAndInverse( nameNewElement, interpretation, @@ -109,29 +111,24 @@ class RefinementRuleProvider { relationInterpretation, inverseRelationInterpretation, [createDefinedElement], - recursiceObjectCreations, - scopePropagator + recursiveObjectCreations, + unitRulePropagator ) statistics.addExecutionTime(System.nanoTime - startTime) - flushQueryEngine(scopePropagator) - - // Scope propagation - val propagatorStartTime = System.nanoTime - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) + unitRulePropagator.propagate ] } else { ruleBuilder.action [ match | statistics.incrementTransformationCount // println(name) + val startTime = System.nanoTime // val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation val container = match.get(4) as DefinedElement - val startTime = System.nanoTime createObjectActionWithContainment( nameNewElement, interpretation, @@ -139,44 +136,34 @@ class RefinementRuleProvider { container, relationInterpretation, [createDefinedElement], - recursiceObjectCreations, - scopePropagator + recursiveObjectCreations, + unitRulePropagator ) statistics.addExecutionTime(System.nanoTime - startTime) - flushQueryEngine(scopePropagator) - - // Scope propagation - val propagatorStartTime = System.nanoTime - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) + unitRulePropagator.propagate ] } } else { ruleBuilder.action [ match | statistics.incrementTransformationCount // println(name) + val startTime = System.nanoTime // val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation - val startTime = System.nanoTime createObjectAction( nameNewElement, interpretation, typeInterpretation, [createDefinedElement], - recursiceObjectCreations, - scopePropagator + recursiveObjectCreations, + unitRulePropagator ) statistics.addExecutionTime(System.nanoTime - startTime) - flushQueryEngine(scopePropagator) - - // Scope propagation - val propagatorStartTime = System.nanoTime - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) + unitRulePropagator.propagate ] } return ruleBuilder.build @@ -342,14 +329,14 @@ class RefinementRuleProvider { [createStringElement] } - def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, + def createRelationRefinementRules(GeneratedPatterns patterns, UnitRulePropagator unitRulePropagator, ModelGenerationStatistics statistics) { val res = new LinkedHashMap - for (LHSEntry : patterns.refinerelationQueries.entrySet) { + 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, scopePropagator, statistics) + val rule = createRelationRefinementRule(declaration, inverseReference, lhs, unitRulePropagator, statistics) res.put(LHSEntry.key, rule) } return res @@ -357,57 +344,29 @@ class RefinementRuleProvider { def private BatchTransformationRule> createRelationRefinementRule( RelationDeclaration declaration, Relation inverseRelation, - IQuerySpecification> lhs, ScopePropagator scopePropagator, + IQuerySpecification> lhs, UnitRulePropagator unitRulePropagator, ModelGenerationStatistics statistics) { val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' val ruleBuilder = factory.createRule(lhs).name(name) if (inverseRelation === null) { ruleBuilder.action [ match | statistics.incrementTransformationCount - // println(name) - // val problem = match.get(0) as LogicProblem - // val interpretation = match.get(1) as PartialInterpretation - val relationInterpretation = match.get(2) as PartialRelationInterpretation - val src = match.get(3) as DefinedElement - val trg = match.get(4) as DefinedElement - val startTime = System.nanoTime - createRelationLinkAction(src, trg, relationInterpretation) + createRelationLinkAction(match, unitRulePropagator) statistics.addExecutionTime(System.nanoTime - startTime) - // Scope propagation - if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { - flushQueryEngine(scopePropagator) - - val propagatorStartTime = System.nanoTime - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) - } + unitRulePropagator.propagate ] } else { ruleBuilder.action [ match | statistics.incrementTransformationCount // println(name) - // val problem = match.get(0) as LogicProblem - // val interpretation = match.get(1) as PartialInterpretation - val relationInterpretation = match.get(2) as PartialRelationInterpretation - val inverseInterpretation = match.get(3) as PartialRelationInterpretation - val src = match.get(4) as DefinedElement - val trg = match.get(5) as DefinedElement - val startTime = System.nanoTime - createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) + createRelationLinkWithInverse(match, unitRulePropagator) statistics.addExecutionTime(System.nanoTime - startTime) - // Scope propagation - if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { - flushQueryEngine(scopePropagator) - - val propagatorStartTime = System.nanoTime - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) - } + unitRulePropagator.propagate ] } @@ -418,7 +377,7 @@ class RefinementRuleProvider { // Actions // /////////////////////// protected def void createObjectAction(boolean nameNewElement, ObjectCreationInterpretationData data, - DefinedElement container, ScopePropagator scopePropagator) { + DefinedElement container, UnitRulePropagator unitRulePropagator) { if (data.containerInterpretation !== null) { if (data.containerInverseInterpretation !== null) { createObjectActionWithContainmentAndInverse( @@ -430,7 +389,7 @@ class RefinementRuleProvider { data.containerInverseInterpretation, data.constructor, data.recursiveConstructors, - scopePropagator + unitRulePropagator ) } else { createObjectActionWithContainment( @@ -441,7 +400,7 @@ class RefinementRuleProvider { data.containerInterpretation, data.constructor, data.recursiveConstructors, - scopePropagator + unitRulePropagator ) } } else { @@ -451,7 +410,7 @@ class RefinementRuleProvider { data.typeInterpretation, data.constructor, data.recursiveConstructors, - scopePropagator + unitRulePropagator ) } @@ -466,7 +425,7 @@ class RefinementRuleProvider { PartialRelationInterpretation inverseRelationInterpretation, Function0 constructor, List recursiceObjectCreations, - ScopePropagator scopePropagator + UnitRulePropagator unitRulePropagator ) { val newElement = constructor.apply if (nameNewElement) { @@ -486,14 +445,16 @@ class RefinementRuleProvider { inverseRelationInterpretation.relationlinks += newLink2 // Scope propagation - scopePropagator.decrementTypeScope(typeInterpretation) + unitRulePropagator.decrementTypeScope(typeInterpretation) + unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) + unitRulePropagator.addedToRelation(inverseRelationInterpretation.interpretationOf) // Existence interpretation.newElements += newElement // Do recursive object creation for (newConstructor : recursiceObjectCreations) { - createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) + createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator) } return newElement @@ -507,7 +468,7 @@ class RefinementRuleProvider { PartialRelationInterpretation relationInterpretation, Function0 constructor, List recursiceObjectCreations, - ScopePropagator scopePropagator + UnitRulePropagator unitRulePropagator ) { val newElement = constructor.apply if (nameNewElement) { @@ -522,16 +483,17 @@ class RefinementRuleProvider { // ContainmentRelation val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] relationInterpretation.relationlinks += newLink + unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) // Scope propagation - scopePropagator.decrementTypeScope(typeInterpretation) + unitRulePropagator.decrementTypeScope(typeInterpretation) // Existence interpretation.newElements += newElement // Do recursive object creation for (newConstructor : recursiceObjectCreations) { - createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) + createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator) } return newElement @@ -539,7 +501,7 @@ class RefinementRuleProvider { protected def createObjectAction(boolean nameNewElement, PartialInterpretation interpretation, PartialTypeInterpratation typeInterpretation, Function0 constructor, - List recursiceObjectCreations, ScopePropagator scopePropagator) { + List recursiceObjectCreations, UnitRulePropagator unitRulePropagator) { val newElement = constructor.apply if (nameNewElement) { newElement.name = '''new «interpretation.newElements.size»''' @@ -552,38 +514,220 @@ class RefinementRuleProvider { } // Scope propagation - scopePropagator.decrementTypeScope(typeInterpretation) + unitRulePropagator.decrementTypeScope(typeInterpretation) // Existence interpretation.newElements += newElement // Do recursive object creation for (newConstructor : recursiceObjectCreations) { - createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) + createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator) } return newElement } - protected def boolean createRelationLinkAction(DefinedElement src, DefinedElement trg, - PartialRelationInterpretation relationInterpretation) { + protected def createRelationLinkAction(IPatternMatch match, UnitRulePropagator unitRulePropagator) { + // val problem = match.get(0) as LogicProblem + // val interpretation = match.get(1) as PartialInterpretation + val relationInterpretation = match.get(2) as PartialRelationInterpretation + val src = match.get(3) as DefinedElement + val trg = match.get(4) as DefinedElement + createRelationLinkAction(src, trg, relationInterpretation, unitRulePropagator) + } + + protected def void createRelationLinkAction(DefinedElement src, DefinedElement trg, + PartialRelationInterpretation relationInterpretation, UnitRulePropagator unitRulePropagator) { val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] relationInterpretation.relationlinks += link + unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) } - protected def boolean createRelationLinkWithInverse(DefinedElement src, DefinedElement trg, - PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation) { + protected def void createRelationLinkWithInverse(IPatternMatch match, UnitRulePropagator unitRulePropagator) { + // val problem = match.get(0) as LogicProblem + // val interpretation = match.get(1) as PartialInterpretation + val relationInterpretation = match.get(2) as PartialRelationInterpretation + val inverseInterpretation = match.get(3) as PartialRelationInterpretation + val src = match.get(4) as DefinedElement + val trg = match.get(5) as DefinedElement + createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation, unitRulePropagator) + } + + protected def void createRelationLinkWithInverse(DefinedElement src, DefinedElement trg, + PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation, + UnitRulePropagator unitRulePropagator) { val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] relationInterpretation.relationlinks += link val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src] inverseInterpretation.relationlinks += inverseLink + unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) + unitRulePropagator.addedToRelation(inverseInterpretation.interpretationOf) } - protected def flushQueryEngine(ScopePropagator scopePropagator) { - if (scopePropagator.queryEngineFlushRequiredBeforePropagation && queryEngine.updatePropagationDelayed) { - delayMessageDelivery.setBoolean(queryEngine, false) - queryEngine.getQueryBackend(ReteBackendFactory.INSTANCE).flushUpdates - delayMessageDelivery.setBoolean(queryEngine, true) + static class UnitRulePropagator { + val LogicProblem p + val PartialInterpretation i + val RefinementRuleProvider refinementRuleProvider + var AdvancedViatraQueryEngine queryEngine + var Field delayMessageDelivery + val ScopePropagator scopePropagator + val List> propagators + val ModelGenerationStatistics statistics + + new(LogicProblem p, PartialInterpretation i, RefinementRuleProvider refinementRuleProvider, + ScopePropagator scopePropagator, + Map, IQuerySpecification>> mustRelationPropagationQueries, + ModelGenerationStatistics statistics) { + this.p = p + this.i = i + this.refinementRuleProvider = refinementRuleProvider + queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine + delayMessageDelivery = queryEngine.class.getDeclaredField("delayMessageDelivery") + delayMessageDelivery.accessible = true + this.scopePropagator = scopePropagator + propagators = ImmutableList.copyOf(mustRelationPropagationQueries.entrySet.map [ entry | + val matcher = queryEngine.getMatcher(entry.value) + getPropagator(entry.key.key, entry.key.value, matcher) + ]) + this.statistics = statistics + } + + def decrementTypeScope(PartialTypeInterpratation partialTypeInterpratation) { + scopePropagator.decrementTypeScope(partialTypeInterpratation) + } + + def addedToRelation(Relation r) { + scopePropagator.addedToRelation(r) + } + + def propagate() { + var boolean changed + do { + val scopeChanged = propagateScope() + val mustChanged = propagateMustRelations() + changed = scopeChanged || mustChanged + } while (changed) + } + + protected def flushQueryEngine() { + if (queryEngine.updatePropagationDelayed) { + delayMessageDelivery.setBoolean(queryEngine, false) + queryEngine.getQueryBackend(ReteBackendFactory.INSTANCE).flushUpdates + delayMessageDelivery.setBoolean(queryEngine, true) + } + } + + protected def propagateScope() { + if (scopePropagator.scopePropagationNeeded) { + if (scopePropagator.queryEngineFlushRequiredBeforePropagation) { + flushQueryEngine() + } + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) + true + } else { + false + } + } + + protected def propagateMustRelations() { + if (propagators.empty) { + return false + } + flushQueryEngine() + val propagatorStartTime = System.nanoTime + var changed = false + for (propagator : propagators) { + changed = propagator.propagate(p, i, refinementRuleProvider, this) || changed + } + statistics.addMustRelationPropagationTime(System.nanoTime - propagatorStartTime) + changed + } + + private static def getPropagator(Relation relation, Relation inverseRelation, + ViatraQueryMatcher matcher) { + if (inverseRelation === null) { + new MustRelationPropagator(matcher) + } else if (relation == inverseRelation) { + new MustRelationPropagatorWithSelfInverse(matcher) + } else { + new MustRelationPropagatorWithInverse(matcher) + } + } + + @FinalFieldsConstructor + private static abstract class AbstractMustRelationPropagator { + val ViatraQueryMatcher matcher + + def propagate(LogicProblem p, PartialInterpretation i, RefinementRuleProvider refinementRuleProvider, + UnitRulePropagator unitRulePropagator) { + val iterator = getIterator(p, i) + if (!iterator.hasNext) { + return false + } + iterate(iterator, refinementRuleProvider, unitRulePropagator) + true + } + + def iterate(Iterator iterator, RefinementRuleProvider refinementRuleProvider, + UnitRulePropagator unitRulePropagator) { + while (iterator.hasNext) { + doPropagate(iterator.next, refinementRuleProvider, unitRulePropagator) + } + } + + protected def getIterator(LogicProblem p, PartialInterpretation i) { + val partialMatch = matcher.newEmptyMatch + partialMatch.set(0, p) + partialMatch.set(1, i) + matcher.streamAllMatches(partialMatch).iterator + } + + protected def void doPropagate(T match, RefinementRuleProvider refinementRuleProvider, + UnitRulePropagator unitRulePropagator) + } + + private static class MustRelationPropagator extends AbstractMustRelationPropagator { + new(ViatraQueryMatcher matcher) { + super(matcher) + } + + override protected doPropagate(T match, RefinementRuleProvider refinementRuleProvider, + UnitRulePropagator unitRulePropagator) { + refinementRuleProvider.createRelationLinkAction(match, unitRulePropagator) + } + } + + private static class MustRelationPropagatorWithInverse extends AbstractMustRelationPropagator { + new(ViatraQueryMatcher matcher) { + super(matcher) + } + + override protected doPropagate(T match, RefinementRuleProvider refinementRuleProvider, + UnitRulePropagator unitRulePropagator) { + refinementRuleProvider.createRelationLinkWithInverse(match, unitRulePropagator) + } + } + + private static class MustRelationPropagatorWithSelfInverse extends MustRelationPropagatorWithInverse { + new(ViatraQueryMatcher matcher) { + super(matcher) + } + + override iterate(Iterator iterator, RefinementRuleProvider refinementRuleProvider, + UnitRulePropagator unitRulePropagator) { + val pairs = newHashSet + while (iterator.hasNext) { + val match = iterator.next + val src = match.get(4) as DefinedElement + val trg = match.get(5) as DefinedElement + if (!pairs.contains(trg -> src)) { + pairs.add(src -> trg) + doPropagate(match, refinementRuleProvider, unitRulePropagator) + } + } + } } } } 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 67d25208..8e05665c 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 @@ -228,6 +228,10 @@ class ViatraReasoner extends LogicReasoner { it.name = "ScopePropagationTime" it.value = (method.statistics.scopePropagationTime / 1000000) as int ] + it.entries += createIntStatisticEntry => [ + it.name = "MustRelationPropagationTime" + it.value = (method.statistics.mustRelationPropagationTime / 1000000) as int + ] it.entries += createIntStatisticEntry => [ it.name = "TypeAnalysisTime" it.value = (method.statistics.preliminaryTypeAnalisisTime / 1000000) as int 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 a2de1abc..4800f71d 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 @@ -307,7 +307,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { public List times = new LinkedList(); private void saveTimes() { - long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder)this.context.getStateCoder()).getStatecoderRuntime()/1000000; long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000; long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000; long activationSelection = this.activationSelector.getRuntime()/1000000; @@ -317,8 +316,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000; long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000; this.times.add( - "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ - "|StateCoderTime:"+statecoderTime+ + "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ "|ForwardTime:"+forwardTime+ "|Backtrackingtime:"+backtrackingTime+ "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+ -- cgit v1.2.3-70-g09d2