From 91b772506f00ce2e317027dd384b82dc7a1295fd Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Mon, 11 May 2020 02:22:15 +0200 Subject: separated must and current UP rules to support non-prop neg finds --- .../dse/BestFirstStrategyForModelGeneration.java | 18 ++++--- .../dse/ModelGenerationCompositeObjective.xtend | 2 +- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 58 +++++++++++++--------- 3 files changed, 46 insertions(+), 32 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver') 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 trace = solutionStoreWithCopy.newSolution(context); - numericSolver.fillSolutionCopy(trace); - solutionStoreWithDiversityDescriptor.newSolution(context); - solutionStore.newSolution(context); - configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); + if(numericSolver.currentSatisfiable()) { + Map 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> + val constraint2MustUnitPropagationPrecondition = new HashMap> + val constraint2CurrentUnitPropagationPrecondition = new HashMap> 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> 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 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) -- cgit v1.2.3-54-g00ecf