From 3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Sat, 9 May 2020 20:33:19 +0200 Subject: Numeric Solver integration to exploration --- .../viatrasolver/reasoner/ViatraReasoner.xtend | 2 +- .../dse/BestFirstStrategyForModelGeneration.java | 32 ++++-- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 114 +++++++++++++++++++++ .../reasoner/dse/SolutionStoreWithCopy.xtend | 3 +- 4 files changed, 140 insertions(+), 11 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf') 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> matchers; + //private Collection> 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>(); - for(IQuerySpecification> p : this.method.getAllPatterns()) { - //System.out.println(p.getSimpleName()); - ViatraQueryMatcher matcher = p.getMatcher(engine); - matchers.add(matcher); - } +// matchers = new LinkedList>(); +// for(IQuerySpecification> p : this.method.getAllPatterns()) { +// //System.out.println(p.getSimpleName()); +// ViatraQueryMatcher 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(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 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> + 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 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 elements, Map 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 elements, Map solution, Map 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 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 -- cgit v1.2.3-54-g00ecf