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 ++++++++++++++++------ 4 files changed, 60 insertions(+), 23 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver') 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..