From fc84d3fe670331bc89fb1e4c44104bc1fc811438 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 14 Aug 2019 18:26:33 +0200 Subject: Measurements WIP --- .../ModelGenerationMethodProvider.xtend | 35 +++++-- .../cardinality/LinearTypeConstraintHint.xtend | 30 ++++++ .../cardinality/PolyhedronScopePropagator.xtend | 106 ++++++++++++++++----- .../cardinality/PolyhedronSolver.xtend | 72 ++++++++++++-- .../cardinality/RelationConstraintCalculator.xtend | 5 +- .../logic2viatra/cardinality/ScopePropagator.xtend | 25 ++++- .../cardinality/ScopePropagatorStrategy.xtend | 11 ++- .../cardinality/TypeHierarchyScopePropagator.xtend | 20 ++-- .../cardinality/Z3PolyhedronSolver.xtend | 32 ++++++- .../logic2viatra/patterns/PatternGenerator.xtend | 18 +++- .../logic2viatra/patterns/PatternProvider.xtend | 6 +- .../patterns/RelationRefinementGenerator.xtend | 2 +- .../logic2viatra/patterns/UnfinishedIndexer.xtend | 26 +++-- .../rules/RefinementRuleProvider.xtend | 15 ++- 14 files changed, 329 insertions(+), 74 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src') 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 23632d4d..e45ec1c8 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 @@ -5,6 +5,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator @@ -46,16 +47,28 @@ class ModelGenerationStatistics { public var long preliminaryTypeAnalisisTime = 0 public var int decisionsTried = 0 - + synchronized def incrementDecisionCount() { decisionsTried++ } + + public var int transformationInvocations + synchronized def incrementTransformationCount() { + transformationInvocations++ + } + public var int scopePropagatorInvocations - + synchronized def incrementScopePropagationCount() { scopePropagatorInvocations++ } + + public var int scopePropagatorSolverInvocations + + synchronized def incrementScopePropagationSolverCount() { + scopePropagatorSolverInvocations++ + } } @Data class ModelGenerationMethod { @@ -93,6 +106,7 @@ class ModelGenerationMethodProvider { boolean nameNewElements, TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy, + Collection hints, DocumentationLevel debugLevel ) { val statistics = new ModelGenerationStatistics @@ -103,8 +117,8 @@ 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, statistics) + workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) + val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) scopePropagator.propagateAllScopeConstraints val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, nameNewElements, statistics) @@ -138,14 +152,20 @@ class ModelGenerationMethodProvider { } private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, - PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) { + PartialInterpretation emptySolution, Collection hints, GeneratedPatterns queries, + ModelGenerationStatistics statistics) { + if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { + throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") + } switch (scopePropagatorStrategy) { - case ScopePropagatorStrategy.Count: + case ScopePropagatorStrategy.None, + case ScopePropagatorStrategy.Basic: new ScopePropagator(emptySolution, statistics) case ScopePropagatorStrategy.BasicTypeHierarchy: new TypeHierarchyScopePropagator(emptySolution, statistics) ScopePropagatorStrategy.Polyhedral: { val types = queries.refineObjectQueries.keySet.map[newType].toSet + val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] val solver = switch (scopePropagatorStrategy.solver) { case Z3Integer: new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) @@ -160,7 +180,8 @@ class ModelGenerationMethodProvider { scopePropagatorStrategy.solver) } new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, - queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing) + queries.hasElementInContainmentQuery, allPatternsByName, hints, solver, + scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) } default: throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) 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 new file mode 100644 index 00000000..8c21ca1d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend @@ -0,0 +1,30 @@ +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 org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher + +interface LinearTypeExpressionBuilderFactory { + def ViatraQueryMatcher createMatcher(String queryName) + + def LinearTypeExpressionBuilder createBuilder() +} + +interface LinearTypeExpressionBuilder { + def LinearTypeExpressionBuilder add(int scale, Type type) + + def LinearBoundedExpression build() +} + +@FunctionalInterface +interface RelationConstraintUpdater { + def void update(PartialInterpretation p) +} + +interface LinearTypeConstraintHint { + def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator) + + 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/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 7c05e818..51dba244 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 @@ -1,5 +1,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality +import com.google.common.cache.Cache +import com.google.common.cache.CacheBuilder import com.google.common.collect.ImmutableList import com.google.common.collect.ImmutableMap import com.google.common.collect.ImmutableSet @@ -15,6 +17,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope import java.util.ArrayDeque import java.util.ArrayList +import java.util.Collection import java.util.HashMap import java.util.HashSet import java.util.List @@ -29,26 +32,33 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { + static val CACHE_SIZE = 10000 + + val boolean updateHeuristic val Map scopeBounds val LinearBoundedExpression topLevelBounds val Polyhedron polyhedron val PolyhedronSaturationOperator operator val Set relevantRelations + val Cache cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build List updaters = emptyList new(PartialInterpretation p, ModelGenerationStatistics statistics, Set possibleNewDynamicTypes, Map unfinishedMultiplicityQueries, IQuerySpecification> hasElementInContainmentQuery, - PolyhedronSolver solver, boolean propagateRelations) { + Map>> allPatternsByName, + Collection hints, PolyhedronSolver solver, boolean propagateRelations, + boolean updateHeuristic) { super(p, statistics) + this.updateHeuristic = updateHeuristic val builder = new PolyhedronBuilder(p) builder.buildPolyhedron(possibleNewDynamicTypes) scopeBounds = builder.scopeBounds topLevelBounds = builder.topLevelBounds polyhedron = builder.polyhedron operator = solver.createSaturationOperator(polyhedron) + propagateAllScopeConstraints() if (propagateRelations) { - propagateAllScopeConstraints() val maximumNumberOfNewNodes = topLevelBounds.upperBound if (maximumNumberOfNewNodes === null) { throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") @@ -57,7 +67,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { throw new IllegalStateException("Maximum number of new nodes is not positive") } builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, - maximumNumberOfNewNodes) + allPatternsByName, hints, maximumNumberOfNewNodes) relevantRelations = builder.relevantRelations updaters = builder.updaters } else { @@ -66,21 +76,40 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } override void doPropagateAllScopeConstraints() { + super.doPropagateAllScopeConstraints() resetBounds() populatePolyhedronFromScope() // println(polyhedron) - val result = operator.saturate() -// println(polyhedron) - if (result == PolyhedronSaturationResult.EMPTY) { - setScopesInvalid() - } else { - populateScopesFromPolyhedron() - if (result != PolyhedronSaturationResult.SATURATED) { - super.propagateAllScopeConstraints() + val signature = polyhedron.createSignature + val cachedSignature = cache.getIfPresent(signature) + switch (cachedSignature) { + case null: { + statistics.incrementScopePropagationSolverCount + val result = operator.saturate() + if (result == PolyhedronSaturationResult.EMPTY) { + cache.put(signature, PolyhedronSignature.EMPTY) + setScopesInvalid() + } else { + val resultSignature = polyhedron.createSignature + cache.put(signature, resultSignature) + populateScopesFromPolyhedron() + } } + case PolyhedronSignature.EMPTY: + setScopesInvalid() + PolyhedronSignature.Bounds: { + polyhedron.applySignature(signature) + populateScopesFromPolyhedron() + } + default: + throw new IllegalStateException("Unknown polyhedron signature: " + signature) + } +// println(polyhedron) + if (updateHeuristic) { + copyScopeBoundsToHeuristic() } } - + override propagateAdditionToRelation(Relation r) { super.propagateAdditionToRelation(r) if (relevantRelations.contains(r)) { @@ -186,7 +215,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } @FinalFieldsConstructor - private static class PolyhedronBuilder { + private static class PolyhedronBuilder implements LinearTypeExpressionBuilderFactory { static val INFINITY_SCALE = 10 val PartialInterpretation p @@ -197,6 +226,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { Map typeBounds int infinity ViatraQueryEngine queryEngine + Map>> allPatternsByName ImmutableList.Builder updatersBuilder Map scopeBounds @@ -222,9 +252,11 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { def buildMultiplicityConstraints( Map constraints, IQuerySpecification> hasElementInContainmentQuery, - int maximumNuberOfNewNodes) { + Map>> allPatternsByName, + Collection hints, int maximumNuberOfNewNodes) { infinity = maximumNuberOfNewNodes * INFINITY_SCALE queryEngine = ViatraQueryEngine.on(new EMFScope(p)) + this.allPatternsByName = allPatternsByName updatersBuilder = ImmutableList.builder val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType] for (pair : containmentConstraints.entrySet) { @@ -238,10 +270,13 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } } buildRelevantRelations(constraints.keySet) + for (hint : hints) { + updatersBuilder.add(hint.createConstraintUpdater(this)) + } updaters = updatersBuilder.build addCachedConstraintsToPolyhedron() } - + private def buildRelevantRelations(Set constraints) { val builder = ImmutableSet.builder for (constraint : constraints) { @@ -345,7 +380,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } } - private def addCoefficients(Map accumulator, int scale, Map a) { + private static def addCoefficients(Map accumulator, int scale, Map a) { for (pair : a.entrySet) { val dimension = pair.key val currentValue = accumulator.get(pair.key) ?: 0 @@ -411,14 +446,41 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } scopeBoundsBuilder.build } + + override createMatcher(String queryName) { + val querySpecification = allPatternsByName.get(queryName) + if (querySpecification === null) { + throw new IllegalArgumentException("Unknown pattern: " + queryName) + } + querySpecification.getMatcher(queryEngine) + } + + override createBuilder() { + new PolyhedronBuilderLinearTypeExpressionBuilder(this) + } } - private static interface RelationConstraintUpdater { - def void update(PartialInterpretation p) + @FinalFieldsConstructor + private static class PolyhedronBuilderLinearTypeExpressionBuilder implements LinearTypeExpressionBuilder { + val PolyhedronBuilder polyhedronBuilder + val Map coefficients = new HashMap + + override add(int scale, Type type) { + val typeCoefficients = polyhedronBuilder.subtypeDimensions.get(type) + if (typeCoefficients === null) { + throw new IllegalArgumentException("Unknown type: " + type) + } + PolyhedronBuilder.addCoefficients(coefficients, scale, typeCoefficients) + this + } + + override build() { + polyhedronBuilder.toExpression(coefficients) + } } @FinalFieldsConstructor - static class ContainmentConstraintUpdater implements RelationConstraintUpdater { + private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { val String name val LinearBoundedExpression orphansLowerBound val LinearBoundedExpression orphansUpperBound @@ -460,7 +522,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } @FinalFieldsConstructor - static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { + private static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { val LinearBoundedExpression typeCardinality val ViatraQueryMatcher hasElementInContainmentMatcher @@ -479,7 +541,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } @FinalFieldsConstructor - static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { + private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { val String name val LinearBoundedExpression availableMultiplicityExpression val ViatraQueryMatcher unfinishedMultiplicityMatcher @@ -500,7 +562,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } @FinalFieldsConstructor - static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { + private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { val String name val LinearBoundedExpression targetCardinalityExpression val ViatraQueryMatcher unrepairableMultiplicityMatcher diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend index 9c6cb82e..4e046190 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend @@ -3,6 +3,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality import java.util.List import java.util.Map import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.Data import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor interface PolyhedronSolver { @@ -52,16 +53,66 @@ class Polyhedron { val List expressionsToSaturate override toString() ''' - Dimensions: - «FOR dimension : dimensions» - «dimension» - «ENDFOR» - Constraints: - «FOR constraint : constraints» - «constraint» - «ENDFOR» + Dimensions: + «FOR dimension : dimensions» + «dimension» + «ENDFOR» + Constraints: + «FOR constraint : constraints» + «constraint» + «ENDFOR» ''' + def createSignature() { + val size = dimensions.size + constraints.size + val lowerBounds = newArrayOfSize(size) + val upperBounds = newArrayOfSize(size) + var int i = 0 + for (dimension : dimensions) { + lowerBounds.set(i, dimension.lowerBound) + upperBounds.set(i, dimension.upperBound) + i++ + } + for (constraint : constraints) { + lowerBounds.set(i, constraint.lowerBound) + upperBounds.set(i, constraint.upperBound) + i++ + } + new PolyhedronSignature.Bounds(lowerBounds, upperBounds) + } + + def applySignature(PolyhedronSignature.Bounds signature) { + val lowerBounds = signature.lowerBounds + val upperBounds = signature.upperBounds + var int i = 0 + for (dimension : dimensions) { + dimension.lowerBound = lowerBounds.get(i) + dimension.upperBound = upperBounds.get(i) + i++ + } + for (constraint : constraints) { + constraint.lowerBound = lowerBounds.get(i) + constraint.upperBound = upperBounds.get(i) + i++ + } + } +} + +abstract class PolyhedronSignature { + public static val EMPTY = new PolyhedronSignature { + override toString() { + "PolyhedronSignature.EMPTY" + } + } + + private new() { + } + + @Data + static class Bounds extends PolyhedronSignature { + val Integer[] lowerBounds + val Integer[] upperBounds + } } @Accessors @@ -80,6 +131,11 @@ abstract class LinearBoundedExpression { upperBound = tighterBound } } + + def void assertEqualsTo(int bound) { + tightenLowerBound(bound) + tightenUpperBound(bound) + } } @Accessors 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 52a390a8..013e53e1 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 @@ -117,9 +117,12 @@ class RelationConstraintCalculator { var inverseUpperMultiplicity = -1 val inverseRelation = inverseRelations.get(relation) if (inverseRelation !== null) { - inverseUpperMultiplicity = upperMultiplicities.get(relation) + inverseUpperMultiplicity = upperMultiplicities.get(inverseRelation) container = containmentRelations.contains(inverseRelation) } + if (containment) { + inverseUpperMultiplicity = 1 + } val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container, lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity) if (constraint.isActive) { 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 0bdb202e..2376fb38 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 @@ -14,7 +14,7 @@ import org.eclipse.xtend.lib.annotations.Accessors class ScopePropagator { @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation - val ModelGenerationStatistics statistics + @Accessors(PROTECTED_GETTER) val ModelGenerationStatistics statistics val Map type2Scope @Accessors(PROTECTED_GETTER) val Map> superScopes @Accessors(PROTECTED_GETTER) val Map> subScopes @@ -59,12 +59,21 @@ class ScopePropagator { } } } while (changed) + + copyScopeBoundsToHeuristic() } def propagateAllScopeConstraints() { statistics.incrementScopePropagationCount() doPropagateAllScopeConstraints() } + + protected def copyScopeBoundsToHeuristic() { + partialInterpretation.minNewElementsHeuristic = partialInterpretation.minNewElements + for (scope : partialInterpretation.scopes) { + scope.minNewElementsHeuristic = scope.minNewElements + } + } protected def void doPropagateAllScopeConstraints() { // Nothing to propagate. @@ -73,12 +82,17 @@ class ScopePropagator { def propagateAdditionToType(PartialTypeInterpratation t) { // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') val targetScope = type2Scope.get(t) - targetScope.removeOne - val sups = superScopes.get(targetScope) - sups.forEach[removeOne] + if (targetScope !== null) { + targetScope.removeOne + val sups = superScopes.get(targetScope) + sups.forEach[removeOne] + } if (this.partialInterpretation.minNewElements > 0) { this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 } + if (this.partialInterpretation.minNewElementsHeuristic > 0) { + this.partialInterpretation.minNewElementsHeuristic = this.partialInterpretation.minNewElementsHeuristic - 1 + } if (this.partialInterpretation.maxNewElements > 0) { this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 } else if (this.partialInterpretation.maxNewElements === 0) { @@ -105,5 +119,8 @@ class ScopePropagator { if (scope.minNewElements > 0) { scope.minNewElements = scope.minNewElements - 1 } + if (scope.minNewElementsHeuristic > 0) { + scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1 + } } } 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 b0ed75cb..3165917a 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,9 @@ enum PolyhedralScopePropagatorSolver { } abstract class ScopePropagatorStrategy { - public static val Count = new Simple("Count") + public static val None = new Simple("None") + + public static val Basic = new Simple("Basic") public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") @@ -47,14 +49,19 @@ abstract class ScopePropagatorStrategy { val PolyhedralScopePropagatorConstraints constraints val PolyhedralScopePropagatorSolver solver + val boolean updateHeuristic val double timeoutSeconds @FinalFieldsConstructor new() { } + new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver, boolean updateHeuristic) { + this(constraints, solver, updateHeuristic, UNLIMITED_TIME) + } + new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) { - this(constraints, solver, UNLIMITED_TIME) + this(constraints, solver, true) } override requiresUpperBoundIndexing() { 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 index be8ef00a..d1704b39 100644 --- 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 @@ -27,12 +27,16 @@ class TypeHierarchyScopePropagator extends ScopePropagator { } private def propagateLowerLimitUp(Scope subScope, Scope superScope) { + var changed = false if (subScope.minNewElements > superScope.minNewElements) { superScope.minNewElements = subScope.minNewElements - return true - } else { - return false + changed = true + } + if (subScope.minNewElementsHeuristic > superScope.minNewElementsHeuristic) { + superScope.minNewElementsHeuristic = subScope.minNewElementsHeuristic + changed = true } + changed } private def propagateUpperLimitDown(Scope subScope, Scope superScope) { @@ -50,16 +54,20 @@ class TypeHierarchyScopePropagator extends ScopePropagator { } private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { + var changed = false 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 + changed = true + } + if (subScope.minNewElementsHeuristic > p.minNewElementsHeuristic) { + p.minNewElementsHeuristic = subScope.minNewElementsHeuristic + changed = true } + changed } private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend index 23444956..3b831433 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend @@ -13,6 +13,7 @@ import java.math.BigDecimal import java.math.MathContext import java.math.RoundingMode import java.util.Map +import org.eclipse.xtend.lib.annotations.Accessors import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor class Z3PolyhedronSolver implements PolyhedronSolver { @@ -28,10 +29,33 @@ class Z3PolyhedronSolver implements PolyhedronSolver { } override createSaturationOperator(Polyhedron polyhedron) { + new DisposingZ3SaturationOperator(this, polyhedron) + } + + def createPersistentSaturationOperator(Polyhedron polyhedron) { new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds) } } +@FinalFieldsConstructor +class DisposingZ3SaturationOperator implements PolyhedronSaturationOperator { + val Z3PolyhedronSolver solver + @Accessors val Polyhedron polyhedron + + override saturate() { + val persistentOperator = solver.createPersistentSaturationOperator(polyhedron) + try { + persistentOperator.saturate + } finally { + persistentOperator.close + } + } + + override close() throws Exception { + // Nothing to close. + } +} + class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { static val INFINITY_SYMBOL_NAME = "oo" static val MULT_SYMBOL_NAME = "*" @@ -106,9 +130,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { IntNum: resultExpr.getInt() RatNum: - floor(resultExpr) + ceil(resultExpr) AlgebraicNum: - floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) + ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) default: if (isNegativeInfinity(resultExpr)) { null @@ -136,9 +160,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { IntNum: resultExpr.getInt() RatNum: - ceil(resultExpr) + floor(resultExpr) AlgebraicNum: - ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) + floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) default: if (isPositiveInfinity(resultExpr)) { null 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 1b0db90e..5c35fb54 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 @@ -16,8 +16,11 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Transform import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import java.util.Collection import java.util.HashMap import java.util.Map import org.eclipse.emf.ecore.EAttribute @@ -26,7 +29,6 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.xtend.lib.annotations.Accessors import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy class PatternGenerator { @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) @@ -104,7 +106,9 @@ class PatternGenerator { } def isRepresentative(Relation relation, Relation inverse) { - if (inverse === null) { + if (relation === null) { + return false + } else if (inverse === null) { return true } else { relation.name.compareTo(inverse.name) < 1 @@ -144,7 +148,8 @@ class PatternGenerator { PartialInterpretation emptySolution, Map fqn2PQuery, TypeAnalysisResult typeAnalysisResult, - RelationConstraints constraints + RelationConstraints constraints, + Collection hints ) { return ''' @@ -294,6 +299,13 @@ class PatternGenerator { // 4.3 Relation refinement ////////// «relationRefinementGenerator.generateRefineReference(problem)» + + ////////// + // 5 Hints + ////////// + «FOR hint : hints» + «hint.getAdditionalPatterns(this)» + «ENDFOR» ''' } } 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 eadf0ae0..f5c85524 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 @@ -26,6 +26,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.xtend.lib.annotations.Data import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint @Data class GeneratedPatterns { @@ -62,7 +63,8 @@ class PatternProvider { def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, Set existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, - ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, boolean writeToFile) { + ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, + Collection hints, boolean writeToFile) { val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { @@ -75,7 +77,7 @@ class PatternProvider { null } val baseIndexerFile = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, - typeAnalysisResult, relationConstraints) + typeAnalysisResult, relationConstraints, hints) if (writeToFile) { workspace.writeText('''generated3valued.vql_deactivated''', baseIndexerFile) } 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 fa73c861..d915d47e 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 @@ -44,7 +44,7 @@ class RelationRefinementGenerator { 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»);''' + 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 diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend index 15b5a047..a8a07756 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend @@ -1,5 +1,6 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns +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 hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint @@ -76,21 +77,26 @@ class UnfinishedIndexer { «IF indexUpperMultiplicities» «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse» private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { - find interpretation(problem,interpretation); - find mustExist(problem,interpretation,source); - «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» - find mustExist(problem,interpretation,target); - «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» - neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» - «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» + «IF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration» + «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")» + «ELSE» + «IF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration» + «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")» + «ELSE» + find interpretation(problem,interpretation); + find mustExist(problem,interpretation,source); + «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» + find mustExist(problem,interpretation,target); + «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» + neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» + «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» + «ENDIF» + «ENDIF» } «ENDIF» «IF constraint.constrainsUnrepairable» private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { - find interpretation(problem,interpretation); - find mustExist(problem,interpretation,object); - «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); check(numberOfRepairMatches < missingMultiplicity); 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 bf816de9..7891ebd8 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 @@ -67,7 +67,8 @@ class RefinementRuleProvider { if(containmentRelation != null) { if(inverseRelation!= null) { ruleBuilder.action[match | - //println(name) + statistics.incrementTransformationCount +// println(name) val startTime = System.nanoTime //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation @@ -107,7 +108,8 @@ class RefinementRuleProvider { ] } else { ruleBuilder.action[match | - //println(name) + statistics.incrementTransformationCount +// println(name) val startTime = System.nanoTime //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation @@ -144,6 +146,9 @@ class RefinementRuleProvider { } } 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 @@ -198,8 +203,9 @@ class RefinementRuleProvider { .precondition(lhs) if (inverseRelation == null) { ruleBuilder.action [ match | + statistics.incrementTransformationCount val startTime = System.nanoTime - //println(name) +// println(name) // val problem = match.get(0) as LogicProblem // val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation @@ -217,8 +223,9 @@ class RefinementRuleProvider { ] } else { ruleBuilder.action [ match | + statistics.incrementTransformationCount val startTime = System.nanoTime - //println(name) +// println(name) // val problem = match.get(0) as LogicProblem // val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation -- cgit v1.2.3-70-g09d2