Polyhedron scope propagator for non-containment references

4 files changed, 38 insertions, 16 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 101f0a3e..a8db5e43 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
@@ -12,7 +12,6 @@ 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.ScopePropagator

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage

@@ -21,6 +20,7 @@ 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.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

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation

@@ -130,6 +130,7 @@ class ViatraReasoner extends LogicReasoner {
 

                 dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationGlobalConstraint(method.invalidWF))

                 dse.addGlobalConstraint(new SurelyViolatedObjectiveGlobalConstraint(solutionSaver))

+                dse.addGlobalConstraint(new InconsistentScopeGlobalConstraint)

                 for (additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) {

                         dse.addGlobalConstraint(additionalConstraint.apply(method))

                 }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend
new file mode 100644
index 00000000..2e039ca2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend
@@ -0,0 +1,25 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+
+import org.eclipse.viatra.dse.objectives.IGlobalConstraint
+import org.eclipse.viatra.dse.base.ThreadContext
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+
+class InconsistentScopeGlobalConstraint implements IGlobalConstraint {
+
+        override init(ThreadContext context) {
+                // Nothing to initialize.
+        }
+
+        override createNew() {
+                this
+        }
+
+        override getName() {
+                class.name
+        }
+
+        override checkGlobalConstraint(ThreadContext context) {
+                val partialModel = context.model as PartialInterpretation
+                partialModel.minNewElements <= partialModel.maxNewElements || partialModel.maxNewElements < 0
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend
index f54a31ca..8ed3e912 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend
@@ -9,9 +9,7 @@ class SurelyViolatedObjectiveGlobalConstraint implements IGlobalConstraint {
         val ViatraReasonerSolutionSaver solutionSaver
 
         override init(ThreadContext context) {
-                if (solutionSaver !== null) {
-                        return
-                }
+                // Nothing to initialize.
         }
 
         override createNew() {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
index e0111cf6..bf34aeeb 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
@@ -1,23 +1,21 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

-import org.eclipse.viatra.dse.objectives.IObjective

-import org.eclipse.viatra.query.runtime.api.IPatternMatch

-import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher

-import org.eclipse.viatra.query.runtime.api.IQuerySpecification

+import java.util.ArrayList

 import java.util.Collection

-import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine

-import org.eclipse.viatra.query.runtime.emf.EMFScope

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

+import java.util.Comparator

 import java.util.List

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

 import org.eclipse.viatra.dse.objectives.Comparators

-import java.util.ArrayList

-import java.util.Comparator

+import org.eclipse.viatra.dse.objectives.IObjective

+import org.eclipse.viatra.query.runtime.api.IPatternMatch

+import org.eclipse.viatra.query.runtime.api.IQuerySpecification

+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher

 

 class UnfinishedWFObjective implements IObjective {

         Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs

         val List<ViatraQueryMatcher<?>> matchers

         

-        public new(Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) {

+        new(Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) {

                 this.unfinishedWFs = unfinishedWFs

                 matchers = new ArrayList(unfinishedWFs.size)

         }

@@ -48,9 +46,9 @@ class UnfinishedWFObjective implements IObjective {
         override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }

         

         override setComparator(Comparator<Double> comparator) {

-                throw new UnsupportedOperationException("TODO: auto-generated method stub")

+                throw new UnsupportedOperationException()

         }

         override setLevel(int level) {

-                throw new UnsupportedOperationException("TODO: auto-generated method stub")

+                throw new UnsupportedOperationException()

         }

 }
\ No newline at end of file