separated must and current UP rules to support non-prop neg finds

3 files changed, 46 insertions, 32 deletions

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 18fe94e4..45dffe7c 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
@@ -147,7 +147,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                 if (!context.checkGlobalConstraints()) {

                         logger.info("Global contraint is not satisifed in the first state. Terminate.");

                         return;

-                } else if(!numericSolver.isSatisfiable()) {

+                } else if(!numericSolver.maySatisfiable()) {

                         logger.info("Numeric contraints are not satisifed in the first state. Terminate.");

                         return;

                 }

@@ -228,7 +228,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                                 } else if (!context.checkGlobalConstraints()) {

                                         logger.debug("Global contraint is not satisifed.");

                                         context.backtrack();

-                                } else if (!numericSolver.isSatisfiable()) {

+                                } else if (!numericSolver.maySatisfiable()) {

                                         logger.debug("Numeric constraints are not satisifed.");

                                         context.backtrack();

                                 } else {

@@ -284,13 +284,15 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
         private void checkForSolution(final Fitness fittness) {

                 if (fittness.isSatisifiesHardObjectives()) {

                         if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {

-                                Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context);

-                                numericSolver.fillSolutionCopy(trace);

-                                solutionStoreWithDiversityDescriptor.newSolution(context);

-                                solutionStore.newSolution(context);

-                                configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);

+                                if(numericSolver.currentSatisfiable()) {

+                                        Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context);

+                                        numericSolver.fillSolutionCopy(trace);

+                                        solutionStoreWithDiversityDescriptor.newSolution(context);

+                                        solutionStore.newSolution(context);

+                                        configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);

 

-                                logger.debug("Found a solution.");

+                                        logger.debug("Found a solution.");

+                                }

                         }

                 }

         }

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 a75ddf76..9e4792e0 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
@@ -62,7 +62,7 @@ class ModelGenerationCompositeObjective implements IObjective{
                 }

                 var sum = 0.0

                 sum += scopeFitnes

-                sum +=Math.sqrt(multiplicity *0.1)

+                sum +=multiplicity

                 sum += unfinishedWFsFitness//*0.5

                 

                 println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')

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 71793aa6..fe378bd3 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,30 +1,29 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse

 

-import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod

-import java.util.HashMap

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

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

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

-import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint

 import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator

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

-import org.eclipse.emf.ecore.EObject

-import java.util.Map

-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.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.StringElement

+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 java.util.List

+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement

 import java.math.BigDecimal

-import java.util.LinkedHashSet

+import java.util.HashMap

 import java.util.LinkedHashMap

+import java.util.LinkedHashSet

+import java.util.List

+import java.util.Map

+import org.eclipse.emf.ecore.EObject

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

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

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

+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint

 

 class NumericSolver {

         val ThreadContext threadContext;

-        val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

+        val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

+        val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

         NumericTranslator t = new NumericTranslator

         

         val boolean caching;

@@ -38,11 +37,17 @@ class NumericSolver {
         new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) {

                 this.threadContext = threadContext

                 val engine = threadContext.queryEngine

-                for(entry : method.unitPropagationPreconditions.entrySet) {

+                for(entry : method.mustUnitPropagationPreconditions.entrySet) {

+                        val constraint = entry.key

+                        val querySpec = entry.value

+                        val matcher = querySpec.getMatcher(engine);

+                        constraint2MustUnitPropagationPrecondition.put(constraint,matcher)

+                }

+                for(entry : method.currentUnitPropagationPreconditions.entrySet) {

                         val constraint = entry.key

                         val querySpec = entry.value

                         val matcher = querySpec.getMatcher(engine);

-                        constraint2UnitPropagationPrecondition.put(constraint,matcher)

+                        constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher)

                 }

                 this.caching = caching

         }

@@ -52,14 +57,21 @@ class NumericSolver {
         def getNumberOfSolverCalls(){numberOfSolverCalls}

         def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls}

         

-        def boolean isSatisfiable() {

+        def boolean maySatisfiable() {

+                isSatisfiable(this.constraint2MustUnitPropagationPrecondition)

+        }

+        def boolean currentSatisfiable() {

+                isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition)

+        }

+        

+        private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) {

                 val start = System.nanoTime

                 var boolean finalResult 

-                if(constraint2UnitPropagationPrecondition.empty){

+                if(matches.empty){

                         finalResult=true

                 } else {

                         val propagatedConstraints = new HashMap

-                        for(entry : constraint2UnitPropagationPrecondition.entrySet) {

+                        for(entry : matches.entrySet) {

                                 val constraint = entry.key

                                 //println(constraint)

                                 val allMatches = entry.value.allMatches.map[it.toArray]

@@ -108,11 +120,11 @@ class NumericSolver {
         def fillSolutionCopy(Map<EObject, EObject> trace) {

                 val model = threadContext.getModel as PartialInterpretation

                 val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList

-                if(constraint2UnitPropagationPrecondition.empty) {

+                if(constraint2CurrentUnitPropagationPrecondition.empty) {

                         fillWithDefaultValues(dataObjects,trace)

                 } else {

                         val propagatedConstraints = new HashMap

-                        for(entry : constraint2UnitPropagationPrecondition.entrySet) {

+                        for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) {

                                 val constraint = entry.key

                                 val allMatches = entry.value.allMatches.map[it.toArray]

                                 propagatedConstraints.put(constraint,allMatches)