From f06427cd7375551582461f91b3458339a8227f9b Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 2 Nov 2020 02:02:40 +0100 Subject: Optimizing generator with linear objective functions --- .../META-INF/MANIFEST.MF | 3 +- .../ModelGenerationMethodProvider.xtend | 226 --------------------- .../logic2viatra/ModelGenerationStatistics.xtend | 47 +++++ .../logic2viatra/TypeInferenceMethod.xtend | 44 ++++ .../ExtendedLinearExpressionBuilderFactory.xtend | 140 +++++++++++++ ...ExtendedPolyhedronScopePropagatorStrategy.xtend | 63 ++++++ .../cardinality/PolyhedronScopePropagator.xtend | 54 ++--- .../PolyhedronScopePropagatorStrategy.xtend | 92 +++++++++ .../cardinality/PolyhedronSolver.xtend | 13 +- .../META-INF/MANIFEST.MF | 1 + ...odelGenerationMethodBasedGlobalConstraint.xtend | 1 - .../reasoner/ModelGenerationMethodProvider.xtend | 201 ++++++++++++++++++ .../viatrasolver/reasoner/ViatraReasoner.xtend | 102 ++++------ .../reasoner/ViatraReasonerConfiguration.xtend | 4 +- .../dse/BestFirstStrategyForModelGeneration.java | 7 +- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 2 +- .../dse/PartialModelAsLogicInterpretation.xtend | 3 +- .../viatrasolver/reasoner/dse/SolutionCopier.xtend | 8 +- .../reasoner/dse/ViatraReasonerSolutionSaver.xtend | 112 +++++++++- .../optimization/CostElementMatchers.xtend | 137 +++++++++++++ .../reasoner/optimization/CostObjectiveHint.xtend | 68 +++++++ .../optimization/IObjectiveBoundsProvider.xtend | 8 + .../optimization/ThreeValuedCostObjective.xtend | 99 +++++---- .../ThreeValuedCostObjectiveProvider.xtend | 205 +++++++++++++++++++ 24 files changed, 1236 insertions(+), 404 deletions(-) delete mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend (limited to 'Solvers/VIATRA-Solver') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF index b9da0f0b..ec1557e8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF @@ -8,7 +8,8 @@ Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval, hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators, hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, - hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries, + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", 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 deleted file mode 100644 index 3bcd9116..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ /dev/null @@ -1,226 +0,0 @@ -package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra - -import com.google.common.collect.ImmutableMap -import com.google.common.collect.ImmutableSet -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 -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation -import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace -import java.util.Collection -import java.util.List -import java.util.Map -import java.util.Set -import org.eclipse.viatra.query.runtime.api.GenericQueryGroup -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 -import org.eclipse.viatra.query.runtime.emf.EMFScope -import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint -import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery -import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule -import org.eclipse.xtend.lib.annotations.Data - -class ModelGenerationStatistics { - public var long transformationExecutionTime = 0 - - synchronized def addExecutionTime(long amount) { - transformationExecutionTime += amount - } - - public var long scopePropagationTime = 0 - - synchronized def addScopePropagationTime(long amount) { - scopePropagationTime += amount - } - - public var long mustRelationPropagationTime = 0 - - synchronized def addMustRelationPropagationTime(long amount) { - mustRelationPropagationTime += amount - } - - 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 { - ModelGenerationStatistics statistics - - Collection> objectRefinementRules - Collection> relationRefinementRules - - List unfinishedMultiplicities - - Collection>> unfinishedWF - - Collection>> invalidWF - - Map>> mustUnitPropagationPreconditions - Map>> currentUnitPropagationPreconditions - - Map modalRelationQueries - - Collection>> allPatterns -} - -enum TypeInferenceMethod { - Generic, - PreliminaryAnalysis -} - -class ModelGenerationMethodProvider { - val PatternProvider patternProvider = new PatternProvider - val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider - val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider - val relationConstraintCalculator = new RelationConstraintCalculator - - def ModelGenerationMethod createModelGenerationMethod( - LogicProblem logicProblem, - PartialInterpretation emptySolution, - ReasonerWorkspace workspace, - boolean nameNewElements, - TypeInferenceMethod typeInferenceMethod, - boolean calculateObjectCreationCosts, - ScopePropagatorStrategy scopePropagatorStrategy, - Collection hints, - Collection unitPropagationPatternGenerators, - DocumentationLevel debugLevel - ) { - val statistics = new ModelGenerationStatistics - val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) - - val Set existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). - map[it.patternPQuery as PQuery].toSet - - val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) - val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, - workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, - unitPropagationPatternGenerators, writeFiles) - - 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, unitRulePropagator, nameNewElements, statistics) - val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator, - statistics) - - val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, - calculateObjectCreationCosts) - - val unfinishedWF = queries.getUnfinishedWFQueries.values - - val modalRelationQueriesBuilder = ImmutableMap.builder - for (entry : queries.modalRelationQueries.entrySet) { - val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head - if (annotation !== null) { - modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) - } - } - val modalRelationQueries = modalRelationQueriesBuilder.build - - val invalidWF = queries.getInvalidWFQueries.values - - val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns - val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns - - val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( - 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 - val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) - GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) - - return new ModelGenerationMethod( - statistics, - objectRefinementRules.values, - relationRefinementRules.values, - unfinishedMultiplicities, - unfinishedWF, - invalidWF, - mustUnitPropagationPreconditions, - currentUnitPropagationPreconditions, - modalRelationQueries, - queries.allQueries - ) - } - - private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, - 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.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) - case Z3Real: - new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) - case Cbc: - new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) - case Clp: - new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) - default: - throw new IllegalArgumentException("Unknown polyhedron solver: " + - scopePropagatorStrategy.solver) - } - new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, - queries.hasElementInContainmentQuery, 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/ModelGenerationStatistics.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend new file mode 100644 index 00000000..bd5bf807 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend @@ -0,0 +1,47 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra + +class ModelGenerationStatistics { + public var long transformationExecutionTime = 0 + + synchronized def addExecutionTime(long amount) { + transformationExecutionTime += amount + } + + public var long scopePropagationTime = 0 + + synchronized def addScopePropagationTime(long amount) { + scopePropagationTime += amount + } + + public var long mustRelationPropagationTime = 0 + + synchronized def addMustRelationPropagationTime(long amount) { + mustRelationPropagationTime += amount + } + + 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++ + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend new file mode 100644 index 00000000..9296a0be --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend @@ -0,0 +1,44 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra + +import com.google.common.collect.ImmutableMap +import com.google.common.collect.ImmutableSet +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.CachingSimplePolyhedronScopePropagatorStrategy +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 +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.util.Collection +import java.util.List +import java.util.Map +import java.util.Set +import org.eclipse.viatra.query.runtime.api.GenericQueryGroup +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 +import org.eclipse.viatra.query.runtime.emf.EMFScope +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule +import org.eclipse.xtend.lib.annotations.Data + +enum TypeInferenceMethod { + Generic, + PreliminaryAnalysis +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend new file mode 100644 index 00000000..6054affe --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend @@ -0,0 +1,140 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import com.google.common.collect.ImmutableList +import com.google.common.collect.ImmutableMap +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import java.util.ArrayList +import java.util.HashMap +import java.util.HashSet +import java.util.List +import java.util.Map +import java.util.Set +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +interface BoundSaturationListener { + def void boundsSaturated(Integer lower, Integer upper) +} + +interface ExtendedLinearExpressionBuilderFactory { + def ExtendedLinearExpressionBuilder createBuilder() + + def Dimension getDimension(IPatternMatch patternMatch) +} + +interface ExtendedLinearExpressionBuilder extends LinearTypeExpressionBuilder { + override ExtendedLinearExpressionBuilder add(int scale, Type type) + + def ExtendedLinearExpressionBuilder add(int scale, IPatternMatch patternMatch) + + def ExtendedLinearExpressionBuilder add(int scale, Dimension dimension) + + def LinearBoundedExpression build(BoundSaturationListener listener) +} + +class ExtendedPolyhedronBuilder implements ExtendedLinearExpressionBuilderFactory { + val Map typeBounds + val Map, LinearBoundedExpression> expressionsCache + + val ImmutableList.Builder dimensions = ImmutableList.builder + val Set constraints = new HashSet + val Set expressionsToSaturate = new HashSet + val Map patternMatchCounts = new HashMap + @Accessors(PUBLIC_GETTER) val List> saturationListeners = new ArrayList + + new(Polyhedron polyhedron, Map typeBounds, + Map, LinearBoundedExpression> initialExpressionsCache) { + this.typeBounds = typeBounds + this.expressionsCache = new HashMap(initialExpressionsCache) + dimensions.addAll(polyhedron.dimensions) + constraints.addAll(polyhedron.constraints) + expressionsToSaturate.addAll(polyhedron.expressionsToSaturate) + } + + override createBuilder() { + new ExtendedLinearExpressionBuilderImpl(this) + } + + override getDimension(IPatternMatch patternMatch) { + patternMatchCounts.computeIfAbsent(patternMatch) [ key | + val dimension = new Dimension(key.toString, 0, null) + dimensions.add(dimension) + dimension + ] + } + + def buildPolyhedron() { + new Polyhedron( + dimensions.build, + ImmutableList.copyOf(constraints), + ImmutableList.copyOf(expressionsToSaturate) + ) + } + + @FinalFieldsConstructor + private static class ExtendedLinearExpressionBuilderImpl implements ExtendedLinearExpressionBuilder { + val ExtendedPolyhedronBuilder polyhedronBuilder + + val Map coefficients = new HashMap + + override add(int scale, Type type) { + val expression = polyhedronBuilder.typeBounds.get(type) + if (expression === null) { + throw new IllegalArgumentException("Unknown Type: " + type) + } + add(scale, expression) + } + + override add(int scale, IPatternMatch patternMatch) { + val dimension = polyhedronBuilder.getDimension(patternMatch) + add(scale, dimension) + } + + private def add(int scale, LinearBoundedExpression expression) { + switch (expression) { + Dimension: add(scale, expression) + LinearConstraint: add(scale, expression.coefficients) + default: throw new IllegalArgumentException("Unknown LinearBoundedExpression: " + expression) + } + } + + private def add(int scale, Map coefficients) { + for (pair : coefficients.entrySet) { + add(scale * pair.value, pair.key) + } + this + } + + override add(int scale, Dimension dimension) { + coefficients.merge(dimension, scale)[a, b|a + b] + this + } + + override build() { + val filteredCoefficients = ImmutableMap.copyOf(coefficients.filter [ _, coefficient | + coefficient != 0 + ]) + polyhedronBuilder.expressionsCache.computeIfAbsent(filteredCoefficients) [ map | + if (map.size == 1) { + val pair = map.entrySet.head + if (pair.value == 1) { + return pair.key + } + } + val constraint = new LinearConstraint(map) + polyhedronBuilder.constraints.add(constraint) + constraint + ] + } + + override build(BoundSaturationListener listener) { + val expression = build() + if (listener !== null) { + polyhedronBuilder.expressionsToSaturate.add(expression) + polyhedronBuilder.saturationListeners.add(expression -> listener) + } + expression + } + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend new file mode 100644 index 00000000..32923396 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend @@ -0,0 +1,63 @@ +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.ModelGenerationStatistics +import java.util.Collection +import java.util.Map +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation + +interface PolyhedronExtensionOperator { + def void extendPolyhedron(ExtendedLinearExpressionBuilderFactory factory) +} + +class ExtendedPolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy { + val PolyhedronSolver solver + val Collection extensionOperators + + var Map typeBounds + var Map, LinearBoundedExpression> initialExpressionsCache + + new(PolyhedronSolver solver, Collection extensionOperators, + ModelGenerationStatistics statistics) { + super(statistics) + this.solver = solver + this.extensionOperators = extensionOperators + } + + override setPolyhedron(Polyhedron polyhedron, Map typeBounds, + Map, LinearBoundedExpression> initialExpressionsCache) { + super.setPolyhedron(polyhedron, typeBounds, initialExpressionsCache) + this.typeBounds = typeBounds + this.initialExpressionsCache = initialExpressionsCache + } + + override isRelevantRelation(Relation relation) { + true + } + + override protected doSaturate() { + val builder = new ExtendedPolyhedronBuilder(polyhedron, typeBounds, initialExpressionsCache) + for (extensionOperator : extensionOperators) { + extensionOperator.extendPolyhedron(builder) + } + val extendedPolyhedron = builder.buildPolyhedron() + val saturationOperator = solver.createSaturationOperator(extendedPolyhedron) + val result = try { + saturationOperator.saturate() + } finally { + saturationOperator.close() + } + if (result == PolyhedronSaturationResult.EMPTY) { + // The partial model cannot be refined any more, we can't provide objective bounds. + for (pair : builder.saturationListeners) { + pair.value.boundsSaturated(null, null) + } + return false + } + for (pair : builder.saturationListeners) { + val expression = pair.key + pair.value.boundsSaturated(expression.lowerBound, expression.upperBound) + } + true + } +} 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 c28d4caa..ad8f94ab 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,7 +1,5 @@ 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 @@ -23,7 +21,6 @@ import java.util.HashSet import java.util.List import java.util.Map import java.util.Set -import javax.naming.OperationNotSupportedException import org.eclipse.viatra.query.runtime.api.IPatternMatch import org.eclipse.viatra.query.runtime.api.IQuerySpecification import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine @@ -32,31 +29,29 @@ 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 PolyhedronScopePropagatorStrategy strategy 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, Map>> allPatternsByName, - Collection hints, PolyhedronSolver solver, boolean propagateRelations, - boolean updateHeuristic) { + Collection hints, PolyhedronScopePropagatorStrategy strategy, + boolean propagateRelations, boolean updateHeuristic) { super(p, statistics) this.updateHeuristic = updateHeuristic + this.strategy = strategy val builder = new PolyhedronBuilder(p) builder.buildPolyhedron(possibleNewDynamicTypes) scopeBounds = builder.scopeBounds topLevelBounds = builder.topLevelBounds polyhedron = builder.polyhedron - operator = solver.createSaturationOperator(polyhedron) + strategy.setPolyhedron(polyhedron, builder.typeBounds, builder.expressionsCache) propagateAllScopeConstraints() if (propagateRelations) { val maximumNumberOfNewNodes = topLevelBounds.upperBound @@ -80,30 +75,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { resetBounds() populatePolyhedronFromScope() // println(polyhedron) - 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) -// println("INVALID") - 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) + if (strategy.saturate) { + populateScopesFromPolyhedron() + } else { + setScopesInvalid() } // println(polyhedron) if (updateHeuristic) { @@ -112,9 +87,9 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } override isPropagationNeededAfterAdditionToRelation(Relation r) { - relevantRelations.contains(r) || super.isPropagationNeededAfterAdditionToRelation(r) + relevantRelations.contains(r) || strategy.isRelevantRelation(r) || super.isPropagationNeededAfterAdditionToRelation(r) } - + override isQueryEngineFlushRequiredBeforePropagation() { true } @@ -253,7 +228,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } buildRelevantRelations(constraints.keySet) for (hint : hints) { - updatersBuilder.add(hint.createConstraintUpdater(this)) + val updater = hint.createConstraintUpdater(this) + if (updater !== null) { + updatersBuilder.add(updater) + } } updaters = updatersBuilder.build addCachedConstraintsToPolyhedron() @@ -410,7 +388,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { for (scope : p.scopes) { switch (targetTypeInterpretation : scope.targetTypeInterpretation) { PartialPrimitiveInterpretation: - throw new OperationNotSupportedException("Primitive type scopes are not yet implemented") + throw new IllegalStateException("Primitive type scopes are not yet implemented") PartialComplexTypeInterpretation: { val complexType = targetTypeInterpretation.interpretationOf val typeBound = typeBounds.get(complexType) diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend new file mode 100644 index 00000000..f93dcd18 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend @@ -0,0 +1,92 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import com.google.common.cache.Cache +import com.google.common.cache.CacheBuilder +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics +import java.util.Map +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +@FinalFieldsConstructor +abstract class PolyhedronScopePropagatorStrategy { + val ModelGenerationStatistics statistics + + @Accessors(PUBLIC_GETTER) var Polyhedron polyhedron + + def void setPolyhedron(Polyhedron polyhedron, Map typeBounds, + Map, LinearBoundedExpression> initialExpressionsCache) { + if (this.polyhedron !== null) { + throw new IllegalStateException("polyhedron was already set") + } + this.polyhedron = polyhedron + initialize() + } + + def boolean saturate() { + if (polyhedron === null) { + throw new IllegalStateException("polyhedron was not set") + } + doSaturate() + } + + def boolean isRelevantRelation(Relation relation) { + false + } + + protected def incrementScopePropagationSolverCount() { + statistics.incrementScopePropagationSolverCount() + } + + protected def void initialize() { + } + + protected def boolean doSaturate() +} + +@FinalFieldsConstructor +class CachingSimplePolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy { + static val CACHE_SIZE = 10000 + + val PolyhedronSolver solver + + val Cache cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build + var PolyhedronSaturationOperator operator + + new(PolyhedronSolver solver, ModelGenerationStatistics statistics) { + super(statistics) + this.solver = solver + } + + override protected initialize() { + operator = solver.createSaturationOperator(polyhedron) + } + + override protected doSaturate() { + val signature = polyhedron.createSignature + val cachedSignature = cache.getIfPresent(signature) + switch (cachedSignature) { + case null: { + incrementScopePropagationSolverCount() + val result = operator.saturate() + if (result == PolyhedronSaturationResult.EMPTY) { + cache.put(signature, PolyhedronSignature.EMPTY) + false + } else { + val resultSignature = polyhedron.createSignature + cache.put(signature, resultSignature) + true + } + } + case PolyhedronSignature.EMPTY: + false + PolyhedronSignature.Bounds: { + polyhedron.applySignature(signature) + true + } + default: + throw new IllegalStateException("Unknown polyhedron signature: " + signature) + } + } +} 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 4e046190..21bd2d9e 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 @@ -116,7 +116,7 @@ abstract class PolyhedronSignature { } @Accessors -abstract class LinearBoundedExpression { +class Bounds { var Integer lowerBound var Integer upperBound @@ -132,12 +132,19 @@ abstract class LinearBoundedExpression { } } + def void assertBetween(Integer tighterLowerBound, Integer tighterUpperBound) { + tightenLowerBound(tighterLowerBound) + tightenUpperBound(tighterUpperBound) + } + def void assertEqualsTo(int bound) { - tightenLowerBound(bound) - tightenUpperBound(bound) + assertBetween(bound, bound) } } +abstract class LinearBoundedExpression extends Bounds { +} + @Accessors class Dimension extends LinearBoundedExpression { val String name diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF index 4ad61ccb..402a0b7d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF @@ -4,6 +4,7 @@ Bundle-Name: Reasoner Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner Bundle-Version: 1.0.0.qualifier Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner, + hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse, hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend index 9ef5e091..691e0645 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend @@ -1,7 +1,6 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner import org.eclipse.viatra.dse.objectives.IGlobalConstraint -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint { val protected ModelGenerationMethod method diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend new file mode 100644 index 00000000..25137eba --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend @@ -0,0 +1,201 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner + +import com.google.common.collect.ImmutableMap +import com.google.common.collect.ImmutableSet +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.ModelGenerationStatistics +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CachingSimplePolyhedronScopePropagatorStrategy +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.PolyhedronExtensionOperator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjectiveProvider +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.util.Collection +import java.util.List +import java.util.Map +import java.util.Set +import org.eclipse.viatra.dse.objectives.IObjective +import org.eclipse.viatra.query.runtime.api.GenericQueryGroup +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 +import org.eclipse.viatra.query.runtime.emf.EMFScope +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule +import org.eclipse.xtend.lib.annotations.Data +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedPolyhedronScopePropagatorStrategy + +@Data class ModelGenerationMethod { + ModelGenerationStatistics statistics + + Collection> objectRefinementRules + Collection> relationRefinementRules + + List unfinishedMultiplicities + + Collection>> unfinishedWF + + Collection>> invalidWF + + Map>> mustUnitPropagationPreconditions + Map>> currentUnitPropagationPreconditions + + Map modalRelationQueries + + Collection>> allPatterns + + Collection costObjectives + boolean optimizationProblem + ViatraReasonerSolutionSaver solutionSaver +} + +class ModelGenerationMethodProvider { + val PatternProvider patternProvider = new PatternProvider + val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider + val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider + val relationConstraintCalculator = new RelationConstraintCalculator + + def ModelGenerationMethod createModelGenerationMethod( + LogicProblem logicProblem, + PartialInterpretation emptySolution, + ReasonerWorkspace workspace, + ViatraReasonerConfiguration config + ) { + val statistics = new ModelGenerationStatistics + val debugLevel = config.documentationLevel + val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) + + val Set existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). + map[it.patternPQuery as PQuery].toSet + + val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) + val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, + workspace, config.typeInferenceMethod, config.scopePropagatorStrategy, relationConstraints, config.hints, + config.unitPropagationPatternGenerators, writeFiles) + + val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, + config.calculateObjectCreationCosts) + val unfinishedWF = queries.getUnfinishedWFQueries.values + val modalRelationQueriesBuilder = ImmutableMap.builder + for (entry : queries.modalRelationQueries.entrySet) { + val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head + if (annotation !== null) { + modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) + } + } + val modalRelationQueries = modalRelationQueriesBuilder.build + val invalidWF = queries.getInvalidWFQueries.values + val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns + val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns + val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( + queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll( + queries.mustRelationPropagationQueries.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 + val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) + GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) + + val objectiveProvider = new ThreeValuedCostObjectiveProvider(queryEngine, emptySolution, modalRelationQueries) + val transformedObjectives = objectiveProvider.getCostObjectives(config.costObjectives) + + val solutionSaver = new ViatraReasonerSolutionSaver(transformedObjectives.leveledExtremalObjectives, + config.solutionScope.numberOfRequiredSolutions, DiversityChecker.of(config.diversityRequirement)) + + val allHints = ImmutableSet.builder + allHints.addAll(config.hints) + for (hint : transformedObjectives.hints) { + hint.boundsProvider = solutionSaver + allHints.add(hint) + } + + val scopePropagator = createScopePropagator(config.scopePropagatorStrategy, emptySolution, allHints.build, + transformedObjectives.extensionOperators, queries, statistics) + scopePropagator.propagateAllScopeConstraints + val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, queries, + scopePropagator, statistics) + val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, + queries, unitRulePropagator, config.nameNewElements, statistics) + val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator, + statistics) + + return new ModelGenerationMethod( + statistics, + objectRefinementRules.values, + relationRefinementRules.values, + unfinishedMultiplicities, + unfinishedWF, + invalidWF, + mustUnitPropagationPreconditions, + currentUnitPropagationPreconditions, + modalRelationQueries, + queries.allQueries, + transformedObjectives.objectives, + transformedObjectives.optimizationProblem, + solutionSaver + ) + } + + private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, + PartialInterpretation emptySolution, Collection hints, + Collection extensionOperators, 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.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) + case Z3Real: + new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) + case Cbc: + new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) + case Clp: + new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) + default: + throw new IllegalArgumentException("Unknown polyhedron solver: " + + scopePropagatorStrategy.solver) + } + val strategy = if (extensionOperators.empty) { + new CachingSimplePolyhedronScopePropagatorStrategy(solver, statistics) + } else { + new ExtendedPolyhedronScopePropagatorStrategy(solver, extensionOperators, statistics) + } + new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, + queries.hasElementInContainmentQuery, allPatternsByName, hints, strategy, + 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.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 8e05665c..8e992741 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 @@ -1,7 +1,5 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner -import com.google.common.collect.ImmutableList -import com.google.common.collect.Lists import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException @@ -11,7 +9,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation @@ -22,7 +19,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.sta import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective @@ -32,11 +28,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement -import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace import java.util.List import java.util.Map @@ -86,13 +79,7 @@ class ViatraReasoner extends LogicReasoner { problem, emptySolution, workspace, - viatraConfig.nameNewElements, - viatraConfig.typeInferenceMethod, - viatraConfig.calculateObjectCreationCosts, - viatraConfig.scopePropagatorStrategy, - viatraConfig.hints, - viatraConfig.unitPropagationPatternGenerators, - viatraConfig.documentationLevel + viatraConfig ) val compositeObjective = new ModelGenerationCompositeObjective( @@ -112,45 +99,21 @@ class ViatraReasoner extends LogicReasoner { dse.addObjective(punishObjective) } - val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size) - for (entry : viatraConfig.costObjectives.indexed) { - val objectiveName = '''costObjective«entry.key»''' - val objectiveConfig = entry.value - val elementsBuilder = ImmutableList.builder - for (elementConfig : objectiveConfig.elements) { - val relationName = elementConfig.patternQualifiedName - val modalQueries = method.modalRelationQueries.get(relationName) - if (modalQueries === null) { - throw new IllegalArgumentException("Unknown relation: " + relationName) - } - elementsBuilder.add(new ThreeValuedCostElement( - modalQueries.currentQuery, - modalQueries.mayQuery, - modalQueries.mustQuery, - elementConfig.weight - )) - } - val costElements = elementsBuilder.build - val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind, - objectiveConfig.threshold, 3) + for (costObjective : method.costObjectives) { dse.addObjective(costObjective) - if (objectiveConfig.findExtremum) { - extremalObjectives += costObjective - } } - val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions - val solutionStore = if (extremalObjectives.empty) { - new SolutionStore(numberOfRequiredSolutions) - } else { + val solutionStore = if (method.optimizationProblem) { new SolutionStore() + } else { + new SolutionStore(numberOfRequiredSolutions) } solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) - val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement) val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) - val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions, - diversityChecker, numericSolver) + val solutionSaver = method.solutionSaver + solutionSaver.numericSolver = numericSolver val solutionCopier = solutionSaver.solutionCopier + val diversityChecker = solutionSaver.diversityChecker solutionStore.withSolutionSaver(solutionSaver) dse.solutionStore = solutionStore @@ -185,7 +148,8 @@ class ViatraReasoner extends LogicReasoner { dse.addTransformationRule(rule) } - val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, numericSolver) + val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, + numericSolver) viatraConfig.progressMonitor.workedForwardTransformation val transformationFinished = System.nanoTime val transformationTime = transformationFinished - transformationStartTime @@ -211,14 +175,15 @@ class ViatraReasoner extends LogicReasoner { it.value = (pair.value / 1000000) as int ] } - for(x: 0.. [ it.name = '''Solution«x+1»DetailedStatistics''' it.value = strategy.times.get(x) ] } it.entries += createIntStatisticEntry => [ - it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int + it.name = "ExplorationInitializationTime" + it.value = ((strategy.explorationStarted - transformationFinished) / 1000000) as int ] it.entries += createIntStatisticEntry => [ it.name = "TransformationExecutionTime" @@ -253,22 +218,28 @@ class ViatraReasoner extends LogicReasoner { it.value = dse.numberOfStates as int ] it.entries += createIntStatisticEntry => [ - it.name = "ForwardTime" it.value = (strategy.forwardTime/1000000) as int + it.name = "ForwardTime" + it.value = (strategy.forwardTime / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "BacktrackingTime" it.value = (strategy.backtrackingTime/1000000) as int + it.name = "BacktrackingTime" + it.value = (strategy.backtrackingTime / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "GlobalConstraintEvaluationTime" it.value = (strategy.globalConstraintEvaluationTime/1000000) as int + it.name = "GlobalConstraintEvaluationTime" + it.value = (strategy.globalConstraintEvaluationTime / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "FitnessCalculationTime" it.value = (strategy.fitnessCalculationTime/1000000) as int + it.name = "FitnessCalculationTime" + it.value = (strategy.fitnessCalculationTime / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "SolutionCopyTime" it.value = (solutionSaver.totalCopierRuntime/1000000) as int + it.name = "SolutionCopyTime" + it.value = (solutionSaver.totalCopierRuntime / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int + it.name = "ActivationSelectionTime" + it.value = (strategy.activationSelector.runtime / 1000000) as int ] it.entries += createIntStatisticEntry => [ it.name = "Decisions" @@ -287,27 +258,34 @@ class ViatraReasoner extends LogicReasoner { it.value = method.statistics.scopePropagatorSolverInvocations ] it.entries += createIntStatisticEntry => [ - it.name = "NumericalSolverSumTime" it.value = (strategy.numericSolver.runtime/1000000) as int + it.name = "NumericalSolverSumTime" + it.value = (strategy.numericSolver.runtime / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "NumericalSolverProblemFormingTime" it.value = (strategy.numericSolver.solverFormingProblem/1000000) as int + it.name = "NumericalSolverProblemFormingTime" + it.value = (strategy.numericSolver.solverFormingProblem / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "NumericalSolverSolvingTime" it.value = (strategy.numericSolver.solverSolvingProblem/1000000) as int + it.name = "NumericalSolverSolvingTime" + it.value = (strategy.numericSolver.solverSolvingProblem / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "NumericalSolverInterpretingSolution" it.value = (strategy.numericSolver.solverSolution/1000000) as int + it.name = "NumericalSolverInterpretingSolution" + it.value = (strategy.numericSolver.solverSolution / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int + it.name = "NumericalSolverCachingTime" + it.value = (strategy.numericSolver.cachingTime / 1000000) as int ] it.entries += createIntStatisticEntry => [ - it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls + it.name = "NumericalSolverCallNumber" + it.value = strategy.numericSolver.numberOfSolverCalls ] it.entries += createIntStatisticEntry => [ - it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls + it.name = "NumericalSolverCachedAnswerNumber" + it.value = strategy.numericSolver.numberOfCachedSolverCalls ] - if(diversityChecker.active) { + if (diversityChecker.active) { it.entries += createIntStatisticEntry => [ it.name = "SolutionDiversityCheckTime" it.value = (diversityChecker.totalRuntime / 1000000) as int diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index a2ed6016..fbe6da9d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend @@ -4,7 +4,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod 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.PolyhedralScopePropagatorConstraints @@ -12,6 +11,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostObjectiveHint import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold import java.util.LinkedList @@ -114,9 +114,11 @@ class CostObjectiveConfiguration { public var ObjectiveKind kind public var ObjectiveThreshold threshold public var boolean findExtremum + public var CostObjectiveHint hint } class CostObjectiveElementConfiguration { public var String patternQualifiedName public var int weight } + 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 4800f71d..4b7cead1 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 @@ -28,8 +28,6 @@ import org.eclipse.viatra.dse.objectives.Fitness; import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler; import org.eclipse.viatra.dse.solutionstore.SolutionStore; -import org.eclipse.viatra.query.runtime.api.IPatternMatch; -import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher; import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; @@ -37,12 +35,11 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod; import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; @@ -301,7 +298,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { return activationIds; } - private void checkForSolution(final Fitness fittness) { + private void checkForSolution(final Fitness fitness) { solutionStore.newSolution(context); } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index 066040a0..70e8e9c2 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend @@ -1,13 +1,13 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod import java.math.BigDecimal import java.util.HashMap import java.util.LinkedHashMap diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend index cfd11816..b48d0831 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend @@ -22,12 +22,13 @@ import java.util.List import java.util.Map import java.util.TreeSet import org.eclipse.emf.ecore.EObject +import org.eclipse.xtend.lib.annotations.Accessors import org.eclipse.xtext.xbase.lib.Functions.Function1 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ - val PartialInterpretation partialInterpretation + @Accessors val PartialInterpretation partialInterpretation val Map trace; val Map type2Interpretation val Map relation2Interpretation diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend index 38c8f5a1..33b69436 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend @@ -26,16 +26,12 @@ class CopiedSolution { * using the supplied {@link NumericSolver}. */ class SolutionCopier { - val NumericSolver numericSolver val copiedSolutions = new LinkedHashMap + @Accessors NumericSolver numericSolver long startTime = System.nanoTime @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 - new(NumericSolver numericSolver) { - this.numericSolver = numericSolver - } - def void copySolution(ThreadContext context, Object solutionId) { val existingCopy = copiedSolutions.get(solutionId) if (existingCopy === null) { @@ -47,7 +43,7 @@ class SolutionCopier { totalCopierRuntime += System.nanoTime - copyStart val copierRuntime = System.nanoTime - startTime val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime) - numericSolver.fillSolutionCopy(copiedSolution.trace) + numericSolver?.fillSolutionCopy(copiedSolution.trace) copiedSolutions.put(solutionId, copiedSolution) } else { existingCopy.current = true diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend index c0b5008c..e00f76ff 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend @@ -1,5 +1,9 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.DirectionalThresholdObjective +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IObjectiveBoundsProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold import java.util.HashMap import java.util.Map import org.eclipse.viatra.dse.api.DSEException @@ -18,24 +22,32 @@ import org.eclipse.xtend.lib.annotations.Accessors * Will also automatically fill any missing numerical values in the saved solutions * using the supplied {@link NumericSolver}. */ -class ViatraReasonerSolutionSaver implements ISolutionSaver { +class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsProvider { + static val TOLERANCE = 1e-10 + @Accessors val SolutionCopier solutionCopier - val NumericSolver numericSolver @Accessors val DiversityChecker diversityChecker + val IObjective[][] leveledExtremalObjectives val boolean hasExtremalObjectives val int numberOfRequiredSolutions val ObjectiveComparatorHelper comparatorHelper val Map trajectories = new HashMap - @Accessors(PUBLIC_SETTER) var Map solutionsCollection + @Accessors var NumericSolver numericSolver + @Accessors var Map solutionsCollection - new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker, NumericSolver numericSolver) { + new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) { this.diversityChecker = diversityChecker comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) + this.leveledExtremalObjectives = leveledExtremalObjectives hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] this.numberOfRequiredSolutions = numberOfRequiredSolutions - this.solutionCopier = new SolutionCopier(numericSolver) + this.solutionCopier = new SolutionCopier + } + + def setNumericSolver(NumericSolver numericSolver) { this.numericSolver = numericSolver + solutionCopier.numericSolver = numericSolver } override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { @@ -51,6 +63,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { if (!shouldSaveSolution(fitness, context)) { return false } + println("Found: " + fitness) val dominatedTrajectories = newArrayList for (entry : trajectories.entrySet) { val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) @@ -99,7 +112,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { } private def shouldSaveSolution(Fitness fitness, ThreadContext context) { - return fitness.satisifiesHardObjectives && numericSolver.currentSatisfiable + fitness.satisifiesHardObjectives && (numericSolver === null || numericSolver.currentSatisfiable) } private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, @@ -145,8 +158,93 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { } solutionsCollection.size < numberOfRequiredSolutions } - + def getTotalCopierRuntime() { solutionCopier.totalCopierRuntime } + + override computeRequiredBounds(IObjective objective, Bounds bounds) { + if (!hasExtremalObjectives) { + return + } + if (objective instanceof DirectionalThresholdObjective) { + switch (threshold : objective.threshold) { + case ObjectiveThreshold.NO_THRESHOLD: { + // No threshold to set. + } + ObjectiveThreshold.Exclusive: { + switch (kind : objective.kind) { + case HIGHER_IS_BETTER: + bounds.tightenLowerBound(Math.floor(threshold.threshold + 1) as int) + case LOWER_IS_BETTER: + bounds.tightenUpperBound(Math.ceil(threshold.threshold - 1) as int) + default: + throw new IllegalArgumentException("Unknown objective kind" + kind) + } + if (threshold.clampToThreshold) { + return + } + } + ObjectiveThreshold.Inclusive: { + switch (kind : objective.kind) { + case HIGHER_IS_BETTER: + bounds.tightenLowerBound(Math.ceil(threshold.threshold) as int) + case LOWER_IS_BETTER: + bounds.tightenUpperBound(Math.floor(threshold.threshold) as int) + default: + throw new IllegalArgumentException("Unknown objective kind" + kind) + } + if (threshold.clampToThreshold) { + return + } + } + default: + throw new IllegalArgumentException("Unknown threshold: " + threshold) + } + for (level : leveledExtremalObjectives) { + switch (level.size) { + case 0: { + // Nothing to do, wait for the next level. + } + case 1: { + val primaryObjective = level.get(0) + if (primaryObjective != objective) { + // There are no worst-case bounds for secondary objectives. + return + } + } + default: + // There are no worst-case bounds for Pareto front calculation. + return + } + } + val fitnessIterator = trajectories.values.iterator + if (!fitnessIterator.hasNext) { + return + } + val fitness = fitnessIterator.next.get(objective.name) + while (fitnessIterator.hasNext) { + val otherFitness = fitnessIterator.next.get(objective.name) + if (Math.abs(fitness - otherFitness) > TOLERANCE) { + throw new IllegalStateException("Inconsistent fitness: " + objective.name) + } + } + switch (kind : objective.kind) { + case HIGHER_IS_BETTER: + if (needsMoreSolutionsWithSameFitness) { + bounds.tightenLowerBound(Math.floor(fitness) as int) + } else { + bounds.tightenLowerBound(Math.floor(fitness + 1) as int) + } + case LOWER_IS_BETTER: + if (needsMoreSolutionsWithSameFitness) { + bounds.tightenUpperBound(Math.ceil(fitness) as int) + } else { + bounds.tightenUpperBound(Math.ceil(fitness - 1) as int) + } + default: + throw new IllegalArgumentException("Unknown objective kind" + kind) + } + } + } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend new file mode 100644 index 00000000..885b14e8 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend @@ -0,0 +1,137 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization + +import com.google.common.collect.ImmutableList +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage +import java.util.List +import org.eclipse.emf.ecore.EObject +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.xtend.lib.annotations.Data +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation + +@FunctionalInterface +interface ParameterScopeBound { + def double getUpperBound() +} + +@Data +class CostElementMatch { + val IPatternMatch match + val boolean must + + def isMulti() { + CostElementMatchers.isMultiMatch(match) + } +} + +@Data +class CostElementMatchers { + val ViatraQueryMatcher currentMatcher + val ViatraQueryMatcher mayMatcher + val ViatraQueryMatcher mustMatcher + val List parameterScopeBounds + val int weight + + def getCurrentNumberOfMatches() { + currentMatcher.countMatches + } + + def getMinimumNumberOfMatches() { + mustMatcher.countMatches + } + + def getMaximumNumberOfMatches() { + var double sum = 0 + val iterator = mayMatcher.streamAllMatches.iterator + while (iterator.hasNext) { + val match = iterator.next + var double product = 1 + val numberOfParameters = parameterScopeBounds.size + for (var int i = 0; i < numberOfParameters; i++) { + if (isMulti(match.get(i + 2))) { + val scopeBound = parameterScopeBounds.get(i) + product *= scopeBound.upperBound + } + + } + sum += product + } + sum + } + + def getMatches() { + ImmutableList.copyOf(mayMatcher.streamAllMatches.iterator.map [ match | + new CostElementMatch(match, mustMatcher.isMatch(match)) + ]) + } + + def projectMayMatch(IPatternMatch match, int... indices) { + mayMatcher.projectMatch(match, indices) + } + + private static def projectMatch(ViatraQueryMatcher matcher, IPatternMatch match, int... indices) { + checkMatch(match) + val n = matcher.specification.parameters.length - 2 + if (indices.length != n) { + throw new IllegalArgumentException("Invalid number of projection indices") + } + val newMatch = matcher.newEmptyMatch + newMatch.set(0, match.get(0)) + newMatch.set(1, match.get(1)) + for (var int i = 0; i < n; i++) { + newMatch.set(i + 2, match.get(indices.get(i))) + } + if (!matcher.hasMatch(newMatch)) { + throw new IllegalArgumentException("Projected match does not exist") + } + return newMatch + } + + private static def isMatch(ViatraQueryMatcher matcher, IPatternMatch match) { + val n = matcher.specification.parameters.length + if (n != match.specification.parameters.length) { + throw new IllegalArgumentException("Invalid number of match arguments") + } + val newMatch = matcher.newEmptyMatch + for (var int i = 0; i < n; i++) { + newMatch.set(i, match.get(i)) + } + return matcher.hasMatch(newMatch) + } + + static def isMulti(Object o) { + if (o instanceof EObject) { + switch (feature : o.eContainmentFeature) { + case LogicproblemPackage.eINSTANCE.logicProblem_Elements, + case PartialinterpretationPackage.eINSTANCE.partialInterpretation_NewElements: + false + case PartialinterpretationPackage.eINSTANCE.partialInterpretation_OpenWorldElements: + true + default: + throw new IllegalStateException("Unknown containment feature for element: " + feature) + } + } else { + false + } + } + + static def isMultiMatch(IPatternMatch match) { + checkMatch(match) + val n = match.specification.parameters.length + for (var int i = 2; i < n; i++) { + if (isMulti(match.get(i))) { + return true + } + } + false + } + + private static def checkMatch(IPatternMatch match) { + val n = match.specification.parameters.length + if (n < 2 || !(match.get(0) instanceof LogicProblem) || !(match.get(1) instanceof PartialInterpretation)) { + throw new IllegalArgumentException("Match is not from the partial interpretation") + } + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend new file mode 100644 index 00000000..2434073d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend @@ -0,0 +1,68 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization + +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedLinearExpressionBuilder +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator +import java.util.Map +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import org.eclipse.xtend.lib.annotations.Accessors + +abstract class CostObjectiveHint implements LinearTypeConstraintHint, BoundSaturationListener { + @Accessors ThreeValuedCostObjective objective + @Accessors IObjectiveBoundsProvider boundsProvider + + Integer bestUpper = null + + override getAdditionalPatterns(PatternGenerator patternGenerator, Map fqnToPQuery) { + '''''' + } + + override createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) { + null + } + + def isExact() { + false + } + + def PolyhedronExtensionOperator createPolyhedronExtensionOperator( + Map costElementMatchers) { + null + } + + def setObjective(ThreeValuedCostObjective objective) { + if (this.objective !== null) { + throw new IllegalStateException("Objective was already set") + } + this.objective = objective + } + + def setBoundsProvider(IObjectiveBoundsProvider boundsProvider) { + if (this.boundsProvider !== null) { + throw new IllegalStateException("Objective bounds provider was already set") + } + this.boundsProvider = boundsProvider + } + + protected def buildWithBounds(ExtendedLinearExpressionBuilder builder) { + val bounds = builder.build(this) + if (objective !== null && boundsProvider !== null) { + boundsProvider.computeRequiredBounds(objective, bounds) + } + if (exact && bestUpper !== null) { + bounds.tightenLowerBound(bestUpper) + } + bounds + } + + override boundsSaturated(Integer lower, Integer upper) { + if (upper !== null && (bestUpper === null || bestUpper < upper)) { + bestUpper = upper + } + objective?.boundsSaturated(lower, upper) + } + +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend new file mode 100644 index 00000000..3c4d36a5 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend @@ -0,0 +1,8 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization + +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds +import org.eclipse.viatra.dse.objectives.IObjective + +interface IObjectiveBoundsProvider { + def void computeRequiredBounds(IObjective objective, Bounds bounds) +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend index 0a6fd55b..9b1a7e9f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend @@ -1,85 +1,80 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization -import com.google.common.collect.ImmutableList -import java.util.Collection +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener +import java.util.Map import org.eclipse.viatra.dse.base.ThreadContext -import org.eclipse.viatra.query.runtime.api.IPatternMatch -import org.eclipse.viatra.query.runtime.api.IQuerySpecification -import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher -import org.eclipse.xtend.lib.annotations.Data +import org.eclipse.xtend.lib.annotations.Accessors -@Data -class ThreeValuedCostElement { - val IQuerySpecification> currentMatchQuery - val IQuerySpecification> mayMatchQuery - val IQuerySpecification> mustMatchQuery - val int weight -} - -class ThreeValuedCostObjective extends AbstractThreeValuedObjective { - val Collection costElements - Collection matchers +class ThreeValuedCostObjective extends AbstractThreeValuedObjective implements BoundSaturationListener { + @Accessors val Map matchers + double lowerBoundHint = Double.NEGATIVE_INFINITY + double upperBoundHint = Double.POSITIVE_INFINITY - new(String name, Collection costElements, ObjectiveKind kind, ObjectiveThreshold threshold, + new(String name, Map matchers, ObjectiveKind kind, ObjectiveThreshold threshold, int level) { super(name, kind, threshold, level) - this.costElements = costElements + this.matchers = matchers } override createNew() { - new ThreeValuedCostObjective(name, costElements, kind, threshold, level) + // new ThreeValuedCostObjective(name, matchers, kind, threshold, level) + throw new UnsupportedOperationException("ThreeValuedCostObjective can only be used from a single thread") } override init(ThreadContext context) { - val queryEngine = context.queryEngine - matchers = ImmutableList.copyOf(costElements.map [ element | - new CostElementMatchers( - queryEngine.getMatcher(element.currentMatchQuery), - queryEngine.getMatcher(element.mayMatchQuery), - queryEngine.getMatcher(element.mustMatchQuery), - element.weight - ) - ]) } override getRawFitness(ThreadContext context) { - var int cost = 0 - for (matcher : matchers) { - cost += matcher.weight * matcher.currentMatcher.countMatches + var double cost = 0 + for (matcher : matchers.values) { + cost += matcher.weight * matcher.currentNumberOfMatches } - cost as double + cost } override getLowestPossibleFitness(ThreadContext threadContext) { - var int cost = 0 - for (matcher : matchers) { + var double cost = 0 + for (matcher : matchers.values) { if (matcher.weight >= 0) { - cost += matcher.weight * matcher.mustMatcher.countMatches - } else if (matcher.mayMatcher.countMatches > 0) { - // TODO Count may matches. - return Double.NEGATIVE_INFINITY + cost += matcher.weight * matcher.minimumNumberOfMatches + } else { + cost += matcher.weight * matcher.maximumNumberOfMatches } } - cost as double + val boundWithHint = Math.max(lowerBoundHint, cost) + if (boundWithHint > upperBoundHint) { + throw new IllegalStateException("Inconsistent cost bounds") + } + boundWithHint } override getHighestPossibleFitness(ThreadContext threadContext) { - var int cost = 0 - for (matcher : matchers) { + var double cost = 0 + for (matcher : matchers.values) { if (matcher.weight <= 0) { - cost += matcher.weight * matcher.mustMatcher.countMatches - } else if (matcher.mayMatcher.countMatches > 0) { - return Double.POSITIVE_INFINITY + cost += matcher.weight * matcher.minimumNumberOfMatches + } else { + cost += matcher.weight * matcher.maximumNumberOfMatches } } - cost as double + val boundWithHint = Math.min(upperBoundHint, cost) + if (boundWithHint < lowerBoundHint) { + throw new IllegalStateException("Inconsistent cost bounds") + } + boundWithHint } - @Data - private static class CostElementMatchers { - val ViatraQueryMatcher currentMatcher - val ViatraQueryMatcher mayMatcher - val ViatraQueryMatcher mustMatcher - val int weight + override boundsSaturated(Integer lower, Integer upper) { + lowerBoundHint = if (lower === null) { + Double.NEGATIVE_INFINITY + } else { + lower + } + upperBoundHint = if (upper === null) { + Double.POSITIVE_INFINITY + } else { + upper + } + println('''Bounds saturated: «lower»..«upper»''') } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend new file mode 100644 index 00000000..c2750acd --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend @@ -0,0 +1,205 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization + +import com.google.common.collect.ImmutableList +import com.google.common.collect.ImmutableMap +import com.google.common.collect.Lists +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration +import java.util.Collection +import java.util.Map +import org.eclipse.viatra.dse.objectives.IObjective +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import org.eclipse.xtend.lib.annotations.Data + +@Data +class ThreeValuedCostObjectiveProviderResult { + val Collection objectives + val Collection hints + val Collection extensionOperators + val IObjective[][] leveledExtremalObjectives + val boolean optimizationProblem +} + +class ThreeValuedCostObjectiveProvider { + static val COST_OBJECTIVE_LEVEL = 3 + + val ViatraQueryEngine queryEngine + val Map modalRelationQueries + val Map qualifiedNameToRelationMap + val ParameterScopeBound defaultBounds + val ParameterScopeBound booleanBounds + val ParameterScopeBound integerBounds + val ParameterScopeBound realBounds + val ParameterScopeBound stringBounds + val Map typeDeclarationToBoundsMap + + new(ViatraQueryEngine queryEngine, PartialInterpretation interpretation, + Map modalRelationQueries) { + this.queryEngine = queryEngine + this.modalRelationQueries = modalRelationQueries + qualifiedNameToRelationMap = ImmutableMap.copyOf( + interpretation.problem.annotations.filter(TransfomedViatraQuery). + toMap([patternFullyQualifiedName], [target])) + defaultBounds = new PartialInterpretationBasedParameterScopeBound(interpretation) + var ParameterScopeBound booleanBounds = null + var ParameterScopeBound integerBounds = null + var ParameterScopeBound realBounds = null + var ParameterScopeBound stringBounds = null + val typeDeclarationToBoundsMapBuilder = ImmutableMap.builder + for (scope : interpretation.scopes) { + val bounds = new ScopeBasedParameterScopeBound(scope) + switch (typeInterpretation : scope.targetTypeInterpretation) { + PartialBooleanInterpretation: + if (booleanBounds === null) { + booleanBounds = bounds + } else { + throw new IllegalStateException("Duplicate partial boolean interpretation") + } + PartialIntegerInterpretation: + if (integerBounds === null) { + integerBounds = bounds + } else { + throw new IllegalStateException("Duplicate partial integer interpretation") + } + PartialRealInterpretation: + if (realBounds === null) { + realBounds = bounds + } else { + throw new IllegalStateException("Duplicate partial real interpretation") + } + PartialStringInterpretation: + if (stringBounds === null) { + stringBounds = bounds + } else { + throw new IllegalStateException("Duplicate partial string interpretation") + } + PartialComplexTypeInterpretation: + typeDeclarationToBoundsMapBuilder.put(typeInterpretation.interpretationOf, bounds) + } + } + this.booleanBounds = booleanBounds ?: defaultBounds + this.integerBounds = integerBounds ?: defaultBounds + this.realBounds = realBounds ?: defaultBounds + this.stringBounds = stringBounds ?: defaultBounds + typeDeclarationToBoundsMap = typeDeclarationToBoundsMapBuilder.build + } + + def getCostObjectives(Collection costObjectives) { + val objectives = ImmutableList.builder + val hints = ImmutableList.builder + val extensionOperators = ImmutableList.builder + val extremalObjectives = Lists.newArrayListWithExpectedSize(costObjectives.size) + for (entry : costObjectives.indexed) { + val objectiveName = '''costObjective«entry.key»''' + val objectiveConfig = entry.value + val costObjective = transformCostObjective(objectiveConfig, objectiveName) + objectives.add(costObjective) + if (objectiveConfig.findExtremum) { + extremalObjectives += costObjective + } + val hint = objectiveConfig.hint + if (hint !== null) { + hints.add(hint) + hint.objective = costObjective + val extensionOperator = hint.createPolyhedronExtensionOperator(costObjective.matchers) + if (extensionOperator !== null) { + extensionOperators.add(extensionOperator) + } + } + } + new ThreeValuedCostObjectiveProviderResult( + objectives.build, + hints.build, + extensionOperators.build, + newArrayList(extremalObjectives), + !extremalObjectives.empty + ) + } + + private def transformCostObjective(CostObjectiveConfiguration configuration, String name) { + val costElements = ImmutableMap.copyOf(configuration.elements.toMap([patternQualifiedName], [ + transformCostElement + ])) + new ThreeValuedCostObjective(name, costElements, configuration.kind, configuration.threshold, + COST_OBJECTIVE_LEVEL) + } + + private def transformCostElement(CostObjectiveElementConfiguration elementConfig) { + val relationName = elementConfig.patternQualifiedName + val modalQueries = modalRelationQueries.get(relationName) + if (modalQueries === null) { + throw new IllegalArgumentException("Unknown relation queries: " + relationName) + } + val relation = qualifiedNameToRelationMap.get(relationName) + if (relation === null) { + throw new IllegalArgumentException("Unknown transformed relation: " + relationName) + } + val parameterBounds = ImmutableList.copyOf(relation.parameters.map[parameterBound]) + new CostElementMatchers( + queryEngine.getMatcher(modalQueries.currentQuery), + queryEngine.getMatcher(modalQueries.mayQuery), + queryEngine.getMatcher(modalQueries.mustQuery), + parameterBounds, + elementConfig.weight + ) + } + + private def getParameterBound(TypeReference typeReference) { + switch (typeReference) { + BoolTypeReference: booleanBounds + IntTypeReference: integerBounds + RealTypeReference: realBounds + StringTypeReference: stringBounds + ComplexTypeReference: typeDeclarationToBoundsMap.getOrDefault(typeReference.referred, defaultBounds) + } + } + + private static abstract class AbstractParameterScopeBound implements ParameterScopeBound { + override getUpperBound() { + val rawValue = rawUpperBound + if (rawValue < 0) { + Double.POSITIVE_INFINITY + } else { + rawValue + } + } + + protected def int getRawUpperBound() + } + + @Data + private static class ScopeBasedParameterScopeBound extends AbstractParameterScopeBound { + val Scope scope + + override protected getRawUpperBound() { + scope.maxNewElements + } + } + + @Data + private static class PartialInterpretationBasedParameterScopeBound extends AbstractParameterScopeBound { + val PartialInterpretation interpretation + + override protected getRawUpperBound() { + interpretation.maxNewElements + } + } +} -- cgit v1.2.3-70-g09d2