Numeric Solver integration to exploration

7 files changed, 149 insertions, 16 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
index e7342ff7..975ace2f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
@@ -17,6 +17,8 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 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 org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint

+import java.util.Map

 

 class ModelGenerationStatistics {

         public var long transformationExecutionTime = 0

@@ -36,6 +38,8 @@ class ModelGenerationStatistics {
          

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

          

+          Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditions

+         

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

 }

 enum TypeInferenceMethod {

@@ -77,6 +81,8 @@ class ModelGenerationMethodProvider {
                 

                 val invalidWF = queries.getInvalidWFQueries.values

                 

+                val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns

+                

                 return new ModelGenerationMethod(

                         statistics,

                         objectRefinementRules.values,

@@ -84,6 +90,7 @@ class ModelGenerationMethodProvider {
                         unfinishedMultiplicities,

                         unfinishedWF,

                         invalidWF,

+                        unitPropagationPreconditions,

                         queries.allQueries

                 )

         }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
index f576d1a1..18e3018a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
@@ -93,7 +93,6 @@ class PatternProvider {
                         refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]

                 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 

                         unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)]

-                unitPropagationPreconditionPatterns.entrySet.forEach[println(it.key + "->" +it.value)]

                 return new GeneratedPatterns(

                         invalidWFQueries,

                         unfinishedWFQueries,

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
index 6c68ec94..d487db64 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
@@ -100,11 +100,9 @@ class UnitPropagationPreconditionGenerator {
                 val preconditions = new LinkedList

                 val constraint2Precondition = new HashMap

                 for(entry : mainPropagationNames.entrySet) {

-                        val name = '''UPMUSTPropagate«res.getOrGenerateConstraintName(entry.key)»''';

+                        val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»''';

                         val def = '''

-                        pattern «name»(

-                                problem:LogicProblem, interpretation:PartialInterpretation,

-                                «FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)

+                        pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)

                                 «FOR propagation : entry.value SEPARATOR " or "»

                                         { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }

                                 «ENDFOR»'''

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 1e623823..cb73f4e8 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
@@ -77,7 +77,7 @@ class ViatraReasoner extends LogicReasoner{
                         scopePropagator,

                         viatraConfig.documentationLevel

                 )

-                println("parsed")

+                //println("parsed")

                 

                 dse.addObjective(new ModelGenerationCompositeObjective(

                         new ScopeObjective,

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 60f46033..1cd61e9a 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
@@ -17,10 +17,12 @@ import java.util.Comparator;
 import java.util.Iterator;

 import java.util.LinkedList;

 import java.util.List;

+import java.util.Map;

 import java.util.PriorityQueue;

 import java.util.Random;

 

 import org.apache.log4j.Logger;

+import org.eclipse.emf.ecore.EObject;

 import org.eclipse.emf.ecore.util.EcoreUtil;

 import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;

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

@@ -38,6 +40,7 @@ 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.viatra2logic.NumericProblemSolver;

 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;

@@ -80,12 +83,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
         private volatile boolean isInterrupted = false;

         private ModelResult modelResultByInternalSolver = null;

         private Random random = new Random();

-        private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;

+        //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;

         

         // Statistics

         private int numberOfStatecoderFail = 0;

         private int numberOfPrintedModel = 0;

         private int numberOfSolverCalls = 0;

+        

+        private NumericSolver numericSolver = null;

 

         public BestFirstStrategyForModelGeneration(

                         ReasonerWorkspace workspace,

@@ -112,14 +117,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                 this.context = context;

                 this.solutionStore = context.getGlobalContext().getSolutionStore();

                 

-                ViatraQueryEngine engine = context.getQueryEngine();

+//              ViatraQueryEngine engine = context.getQueryEngine();

 //              // TODO: visualisation

-                matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();

-                for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {

-                        //System.out.println(p.getSimpleName());

-                        ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);

-                        matchers.add(matcher);

-                }

+//              matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();

+//              for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {

+//                      //System.out.println(p.getSimpleName());

+//                      ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);

+//                      matchers.add(matcher);

+//              }

                 

                 this.solutionStoreWithCopy = new SolutionStoreWithCopy();

                 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);

@@ -131,6 +136,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                                 return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);

                         }

                 };

+                

+                this.numericSolver = new NumericSolver(context, method);

 

                 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);

         }

@@ -140,6 +147,9 @@ 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()) {

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

+                        return;

                 }

                 if (configuration.searchSpaceConstraints.maxDepth == 0) {

                         logger.info("Maximal depth is reached in the initial solution. Terminate.");

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

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

                                         context.backtrack();

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

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

+                                        context.backtrack();

                                 } else {

                                         final Fitness nextFitness = context.calculateFitness();

                                         checkForSolution(nextFitness);

@@ -272,7 +285,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
         private void checkForSolution(final Fitness fittness) {

                 if (fittness.isSatisifiesHardObjectives()) {

                         if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {

-                                solutionStoreWithCopy.newSolution(context);

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

+                                numericSolver.fillSolutionCopy(trace);

                                 solutionStoreWithDiversityDescriptor.newSolution(context);

                                 solutionStore.newSolution(context);

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

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
new file mode 100644
index 00000000..b72bdb44
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -0,0 +1,114 @@
+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.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.RealElement

+import java.util.List

+import java.math.BigDecimal

+

+class NumericSolver {

+        val ThreadContext threadContext;

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

+        NumericTranslator t = new NumericTranslator

+        

+        new(ThreadContext threadContext, ModelGenerationMethod method) {

+                this.threadContext = threadContext

+                val engine = threadContext.queryEngine

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

+                        val constraint = entry.key

+                        val querySpec = entry.value

+                        val matcher = querySpec.getMatcher(engine);

+                        constraint2UnitPropagationPrecondition.put(constraint,matcher)

+                }

+        }

+        

+        def boolean isSatisfiable() {

+                if(constraint2UnitPropagationPrecondition.empty) return true

+                else {

+                        val propagatedConstraints = new HashMap

+                        for(entry : constraint2UnitPropagationPrecondition.entrySet) {

+                                val constraint = entry.key

+                                //println(constraint)

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

+                                //println(allMatches.toList)

+                                propagatedConstraints.put(constraint,allMatches)

+                        }

+                        

+                        if(propagatedConstraints.values.forall[empty]) {

+                                return true

+                        } else {

+                                val res = t.delegateIsSatisfiable(propagatedConstraints)

+                                //println(res)

+                                return res

+                        }

+                }

+        }

+        

+        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) {

+                        fillWithDefaultValues(dataObjects,trace)

+                } else {

+                        val propagatedConstraints = new HashMap

+                        for(entry : constraint2UnitPropagationPrecondition.entrySet) {

+                                val constraint = entry.key

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

+                                propagatedConstraints.put(constraint,allMatches)

+                        }

+                        

+                        if(propagatedConstraints.values.forall[empty]) {

+                                fillWithDefaultValues(dataObjects,trace)

+                        } else {

+                                val solution = t.delegateGetSolution(dataObjects,propagatedConstraints)

+                                fillWithSolutions(dataObjects,solution,trace)

+                        }

+                }

+        }

+        

+        def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) {

+                for(element : elements) {

+                        if(element.valueSet==false) {

+                                val value = getDefaultValue(element)

+                                val target = trace.get(element) as PrimitiveElement

+                                target.fillWithValue(value)

+                        }

+                }

+        }

+        

+        def protected dispatch getDefaultValue(BooleanElement e) {false}

+        def protected dispatch getDefaultValue(IntegerElement e) {0}

+        def protected dispatch getDefaultValue(RealElement e) {0.0}

+        def protected dispatch getDefaultValue(StringElement e) {""}

+        

+        def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Integer> solution, Map<EObject, EObject> trace) {

+                for(element : elements) {

+                        if(element.valueSet==false) {

+                                if(solution.containsKey(element)) {

+                                        val value = solution.get(element)

+                                        val target = trace.get(element) as PrimitiveElement

+                                        target.fillWithValue(value)

+                                }

+                        }

+                }

+        }

+        

+        def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean}

+        def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer}

+        def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=BigDecimal.valueOf(value as Double) }

+        def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String}

+}
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
index a8b7301e..21867a4e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
@@ -25,7 +25,7 @@ class SolutionStoreWithCopy {
                 newSolution(context)

         }*/

         

-        def newSolution(ThreadContext context) {

+        def Map<EObject,EObject> newSolution(ThreadContext context) {

                 //print(System.nanoTime-initTime + ";")

                 val copyStart = System.nanoTime

                 val solution = context.model as PartialInterpretation

@@ -36,6 +36,7 @@ class SolutionStoreWithCopy {
                 copyTraces.add(copier)

                 runtime += System.nanoTime - copyStart

                 solutionTimes.add(System.nanoTime-sartTime)

+                return copier

         }

         def getSumRuntime() {

                 return runtime