Objective POC implementation

8 files changed, 284 insertions, 9 deletions

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 8831b0ff..6898550d 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,5 +1,7 @@
 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

@@ -25,6 +27,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObject
 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.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

@@ -84,9 +88,36 @@ class ViatraReasoner extends LogicReasoner {
                         wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF)

                 ))

 

+                val extermalObjectives = 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)

+                        dse.addObjective(costObjective)

+                        if (objectiveConfig.findExtremum) {

+                                extermalObjectives += costObjective

+                        }

+                }

+

                 val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolutions)

                 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))

-                val solutionSaver = new ViatraReasonerSolutionSaver(newArrayOfSize(0, 0))

+                val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extermalObjectives))

                 val solutionCopier = solutionSaver.solutionCopier

                 solutionStore.withSolutionSaver(solutionSaver)

                 dse.solutionStore = solutionStore

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 9ef23c59..e6aee20c 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
@@ -7,18 +7,22 @@ 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.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold

 import java.util.LinkedList

 import java.util.List

 import java.util.Set

 import org.eclipse.xtext.xbase.lib.Functions.Function1

 

 enum StateCoderStrategy {

-        Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity

+        Neighbourhood,

+        NeighbourhoodWithEquivalence,

+        IDBased,

+        DefinedByDiversity

 }

 

-class ViatraReasonerConfiguration extends LogicSolverConfiguration{

-        //public var Iterable<PQuery> existingQueries

-        

+class ViatraReasonerConfiguration extends LogicSolverConfiguration {

+        // public var Iterable<PQuery> existingQueries

         public var nameNewElements = false

         public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood

         public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis

@@ -26,7 +30,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
          * Once per 1/randomBacktrackChance the search selects a random state.

          */

         public var int randomBacktrackChance = 20;

-        

+

         /**

          * Describes the required diversity between the solutions.

          * Null means that the solutions have to have different state codes only.

@@ -44,7 +48,9 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
         /**

          * Configuration for cutting search space.

          */

-         public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint

+        public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint

+

+        public var List<CostObjectiveConfiguration> costObjectives = newArrayList

 }

 

 class DiversityDescriptor {

@@ -73,4 +79,16 @@ class SearchSpaceConstraint {
         public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE

         public var int maxDepth = UNLIMITED_MAXDEPTH

         public var List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList

-}
\ No newline at end of file
+}

+

+class CostObjectiveConfiguration {

+        public var List<CostObjectiveElementConfiguration> elements = newArrayList

+        public var ObjectiveKind kind

+        public var ObjectiveThreshold threshold

+        public var boolean findExtremum

+}

+

+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/DseUtils.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend
index 3a897aa3..3c2e3319 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend
@@ -1,5 +1,6 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
 
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective
 import org.eclipse.viatra.dse.base.ThreadContext
 import org.eclipse.viatra.dse.objectives.Comparators
 import org.eclipse.viatra.dse.objectives.Fitness
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
index af6d1bbd..9a33753c 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
@@ -1,6 +1,7 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

 import com.google.common.collect.ImmutableList

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective

 import java.util.Comparator

 import java.util.List

 import org.eclipse.viatra.dse.base.ThreadContext

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend
new file mode 100644
index 00000000..241bef2a
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend
@@ -0,0 +1,102 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import java.util.Comparator
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.Data
+
+abstract class ObjectiveThreshold {
+        public static val NO_THRESHOLD = new hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold {
+                override isHard() {
+                        false
+                }
+
+                override satisfiesThreshold(double cost, Comparator<Double> comparator) {
+                        true
+                }
+        }
+
+        private new() {
+        }
+
+        def boolean isHard() {
+                true
+        }
+
+        def boolean satisfiesThreshold(double cost, Comparator<Double> comparator)
+
+        @Data
+        static class Exclusive extends ObjectiveThreshold {
+                val double threshold
+
+                override satisfiesThreshold(double cost, Comparator<Double> comparator) {
+                        comparator.compare(threshold, cost) > 0
+                }
+        }
+
+        @Data
+        static class Inclusive extends ObjectiveThreshold {
+                val double threshold
+
+                override satisfiesThreshold(double cost, Comparator<Double> comparator) {
+                        comparator.compare(threshold, cost) >= 0
+                }
+        }
+}
+
+abstract class AbstractThreeValuedObjective implements IThreeValuedObjective {
+        @Accessors val String name
+        @Accessors ObjectiveKind kind
+        @Accessors ObjectiveThreshold threshold
+        @Accessors int level
+
+        protected new(String name, ObjectiveKind kind, ObjectiveThreshold threshold, int level) {
+                this.name = name
+                this.kind = kind
+                this.threshold = threshold
+                this.level = level
+        }
+
+        abstract def double getLowestPossibleFitness(ThreadContext threadContext)
+
+        abstract def double getHighestPossibleFitness(ThreadContext threadContext)
+
+        override getWorstPossibleFitness(ThreadContext threadContext) {
+                switch (kind) {
+                        case LOWER_IS_BETTER:
+                                getHighestPossibleFitness(threadContext)
+                        case HIGHER_IS_BETTER:
+                                getLowestPossibleFitness(threadContext)
+                        default:
+                                throw new IllegalStateException("Unknown three valued objective kind: " + kind)
+                }
+        }
+
+        override getBestPossibleFitness(ThreadContext threadContext) {
+                switch (kind) {
+                        case LOWER_IS_BETTER:
+                                getLowestPossibleFitness(threadContext)
+                        case HIGHER_IS_BETTER:
+                                getHighestPossibleFitness(threadContext)
+                        default:
+                                throw new IllegalStateException("Unknown three valued objective kind: " + kind)
+                }
+        }
+
+        override isHardObjective() {
+                threshold.hard
+        }
+
+        override satisifiesHardObjective(Double fitness) {
+                threshold.satisfiesThreshold(fitness, comparator)
+        }
+
+        override getComparator() {
+                kind.comparator
+        }
+
+        override setComparator(Comparator<Double> comparator) {
+                kind = ObjectiveKind.fromComparator(comparator)
+        }
+
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend
index 8c93d4ec..4a870a3e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend
@@ -1,4 +1,4 @@
-package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
 
 import org.eclipse.viatra.dse.base.ThreadContext
 import org.eclipse.viatra.dse.objectives.IObjective
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java
new file mode 100644
index 00000000..f65428fe
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java
@@ -0,0 +1,36 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization;
+
+import java.util.Comparator;
+
+import org.eclipse.viatra.dse.objectives.Comparators;
+
+public enum ObjectiveKind {
+        LOWER_IS_BETTER {
+
+                @Override
+                public Comparator<Double> getComparator() {
+                        return Comparators.LOWER_IS_BETTER;
+                }
+
+        },
+        HIGHER_IS_BETTER {
+
+                @Override
+                public Comparator<Double> getComparator() {
+                        return Comparators.HIGHER_IS_BETTER;
+                }
+
+        };
+
+        public abstract Comparator<Double> getComparator();
+
+        public static ObjectiveKind fromComparator(Comparator<Double> comparator) {
+                if (Comparators.LOWER_IS_BETTER.equals(comparator)) {
+                        return ObjectiveKind.LOWER_IS_BETTER;
+                } else if (Comparators.HIGHER_IS_BETTER.equals(comparator)) {
+                        return ObjectiveKind.HIGHER_IS_BETTER;
+                } else {
+                        throw new IllegalStateException("Only LOWER_IS_BETTER and HIGHER_IS_BETTER comparators are supported.");
+                }
+        }
+}
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
new file mode 100644
index 00000000..362ef4a3
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend
@@ -0,0 +1,86 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
+
+import com.google.common.collect.ImmutableList
+import java.util.Collection
+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
+
+@Data
+class ThreeValuedCostElement {
+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentMatchQuery
+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayMatchQuery
+        val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustMatchQuery
+        val int weight
+}
+
+class ThreeValuedCostObjective extends AbstractThreeValuedObjective {
+        val Collection<ThreeValuedCostElement> costElements
+        Collection<CostElementMatchers> matchers
+
+        new(String name, Collection<ThreeValuedCostElement> costElements, ObjectiveKind kind, ObjectiveThreshold threshold,
+                int level) {
+                super(name, kind, threshold, level)
+                this.costElements = costElements
+        }
+
+        override createNew() {
+                new ThreeValuedCostObjective(name, costElements, kind, threshold, level)
+        }
+
+        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 getFitness(ThreadContext context) {
+                var int cost = 0
+                for (matcher : matchers) {
+                        cost += matcher.weight * matcher.currentMatcher.countMatches
+                }
+                cost as double
+        }
+
+        override getLowestPossibleFitness(ThreadContext threadContext) {
+                var int cost = 0
+                for (matcher : matchers) {
+                        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 as double
+        }
+
+        override getHighestPossibleFitness(ThreadContext threadContext) {
+                var int cost = 0
+                for (matcher : matchers) {
+                        if (matcher.weight <= 0) {
+                                cost += matcher.weight * matcher.mustMatcher.countMatches
+                        } else if (matcher.mayMatcher.countMatches > 0) {
+                                // TODO Count may matches.
+                                return Double.POSITIVE_INFINITY
+                        }
+                }
+                cost as double
+        }
+
+        @Data
+        private static class CostElementMatchers {
+                val ViatraQueryMatcher<? extends IPatternMatch> currentMatcher
+                val ViatraQueryMatcher<? extends IPatternMatch> mayMatcher
+                val ViatraQueryMatcher<? extends IPatternMatch> mustMatcher
+                val int weight
+        }
+}