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 --- .../ModelGenerationMethodProvider.xtend | 9 ++-- .../logic2viatra/patterns/PatternGenerator.xtend | 12 ++++- .../logic2viatra/patterns/PatternProvider.xtend | 20 +++++--- .../UnitPropagationPreconditionGenerator.xtend | 42 ++++++++++++---- .../dse/BestFirstStrategyForModelGeneration.java | 18 ++++--- .../dse/ModelGenerationCompositeObjective.xtend | 2 +- .../viatrasolver/reasoner/dse/NumericSolver.xtend | 58 +++++++++++++--------- 7 files changed, 106 insertions(+), 55 deletions(-) (limited to 'Solvers') 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 975ace2f..be11ed78 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 @@ -38,7 +38,8 @@ class ModelGenerationStatistics { Collection>> invalidWF - Map>> unitPropagationPreconditions + Map>> mustUnitPropagationPreconditions + Map>> currentUnitPropagationPreconditions Collection>> allPatterns } @@ -81,7 +82,8 @@ class ModelGenerationMethodProvider { val invalidWF = queries.getInvalidWFQueries.values - val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns + val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns + val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns return new ModelGenerationMethod( statistics, @@ -90,7 +92,8 @@ class ModelGenerationMethodProvider { unfinishedMultiplicities, unfinishedWF, invalidWF, - unitPropagationPreconditions, + mustUnitPropagationPreconditions, + currentUnitPropagationPreconditions, queries.allQueries ) } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index d5ebe318..219f99e9 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend @@ -26,6 +26,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.xtend.lib.annotations.Accessors import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import org.eclipse.xtend.lib.annotations.Data +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint + +@Data class PatternGeneratorResult { + CharSequence patternText + HashMap constraint2MustPreconditionName + HashMap constraint2CurrentPreconditionName +} class PatternGenerator { @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) @@ -149,7 +157,7 @@ class PatternGenerator { problem.allTypeReferences.exists[it instanceof StringTypeReference] } - public def transformBaseProperties( + public def PatternGeneratorResult transformBaseProperties( LogicProblem problem, PartialInterpretation emptySolution, Map fqn2PQuery, @@ -398,6 +406,6 @@ class PatternGenerator { ''' val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) val second = up.definitions - return (first+second) -> up.constraint2PreconditionName + return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName) } } 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 18e3018a..750107f6 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 @@ -31,7 +31,8 @@ import java.util.HashMap public Map>> refineObjectQueries public Map>> refineTypeQueries public Map, IQuerySpecification>> refinerelationQueries - public Map>> unitPropagationPreconditionPatterns + public Map>> mustUnitPropagationPreconditionPatterns + public Map>> currentUnitPropagationPreconditionPatterns public Collection>> allQueries } @@ -60,14 +61,15 @@ class PatternProvider { null } val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) - val baseIndexerFile = patternGeneratorResult.key - val unitPropagationTrace = patternGeneratorResult.value + val baseIndexerFile = patternGeneratorResult.patternText + val mustUnitPropagationTrace = patternGeneratorResult.constraint2MustPreconditionName + val currentUnitPropagationTrace = patternGeneratorResult.constraint2CurrentPreconditionName if(writeToFile) { workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) } val ParseUtil parseUtil = new ParseUtil val generatedQueries = parseUtil.parse(baseIndexerFile) - val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,unitPropagationTrace,generatedQueries); + val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,mustUnitPropagationTrace,currentUnitPropagationTrace,generatedQueries); return runtimeQueries } @@ -76,7 +78,8 @@ class PatternProvider { LogicProblem problem, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult, - HashMap unitPropagationTrace, + HashMap mustUnitPropagationTrace, + HashMap currentUnitPropagationTrace, Map>> queries ) { val Map>> @@ -92,7 +95,9 @@ class PatternProvider { val Map, IQuerySpecification>> refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] val Map>> - unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)] + mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)] + val Map>> + currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)] return new GeneratedPatterns( invalidWFQueries, unfinishedWFQueries, @@ -100,7 +105,8 @@ class PatternProvider { refineObjectsQueries, refineTypeQueries, refineRelationQueries, - unitPropagationPreconditionPatterns, + mustUnitPropagationPreconditionPatterns, + currentUnitPropagationPreconditionPatterns, queries.values ) } 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 d487db64..91a7a2c2 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 @@ -61,7 +61,8 @@ class UnitPropagationPreconditionGenerationResult { @Data class UnitPropagationPreconditionFinalResult { CharSequence definitions - HashMap constraint2PreconditionName + HashMap constraint2MustPreconditionName + HashMap constraint2CurrentPreconditionName } class UnitPropagationPreconditionGenerator { @@ -81,25 +82,34 @@ class UnitPropagationPreconditionGenerator { // Create an empty result val res = new UnitPropagationPreconditionGenerationResult val wfs = base.wfQueries(problem)//.map[it.patternPQuery] - val Map>> mainPropagationNames = new HashMap + val Map>> mainMustPropagationNames = new HashMap + val Map>> mainCurrentPropagationNames = new HashMap for(wf : wfs) { val query = wf.patternPQuery as PQuery val relation = wf.target val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) for(referredCheck : allReferredChecks) { - val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) - if(!mainPropagationNames.containsKey(referredCheck)) { - mainPropagationNames.put(referredCheck,new LinkedList) + val mustPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) + val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT) + if(!mainMustPropagationNames.containsKey(referredCheck)) { + mainMustPropagationNames.put(referredCheck,new LinkedList) } - if(propagationPrecondition !== null) { - mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size) + if(!mainCurrentPropagationNames.containsKey(referredCheck)) { + mainCurrentPropagationNames.put(referredCheck,new LinkedList) + } + if(mustPropagationPrecondition !== null) { + mainMustPropagationNames.get(referredCheck).add(mustPropagationPrecondition->query.parameterNames.size) + } + if(currentPropagationPrecondition !== null) { + mainCurrentPropagationNames.get(referredCheck).add(currentPropagationPrecondition->query.parameterNames.size) } } } val preconditions = new LinkedList - val constraint2Precondition = new HashMap - for(entry : mainPropagationNames.entrySet) { + val constraint2MustPrecondition = new HashMap + val constraint2CurrentPrecondition = new HashMap + for(entry : mainMustPropagationNames.entrySet) { val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; val def = ''' pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») @@ -107,7 +117,17 @@ class UnitPropagationPreconditionGenerator { { find «propagation.key»(problem,interpretation,«FOR index : 0.. 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