From d1b2d628bf515f0a1772eaff7366f9c29c1b02ce Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 16 Aug 2017 17:13:22 +0200 Subject: Mapping of primitive types in patterns --- .../logic2viatra/patterns/GenericTypeIndexer.xtend | 2 +- .../logic2viatra/patterns/PatternGenerator.xtend | 94 ++++++++++++++++++++-- .../patterns/RelationDeclarationIndexer.xtend | 15 +--- .../patterns/RelationDefinitionIndexer.xtend | 5 +- .../patterns/RelationRefinementGenerator.xtend | 4 +- .../logic2viatra/patterns/TypeIndexer.xtend | 24 +++++- .../TypeIndexerWithPreliminaryTypeAnalysis.xtend | 2 +- .../InstanceModel2Logic.xtend | 5 +- .../InstanceModel2PartialInterpretation.xtend | 10 +-- 9 files changed, 128 insertions(+), 33 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/patterns/GenericTypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend index 23bdda35..a703ba4b 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend @@ -7,7 +7,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult -class GenericTypeIndexer implements TypeIndexer { +class GenericTypeIndexer extends TypeIndexer { val PatternGenerator base; new(PatternGenerator base) { 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 2986e344..6e1e5765 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 @@ -21,6 +21,11 @@ import java.util.HashSet import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.DefinedByDerivedFeature +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference class PatternGenerator { @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) @@ -126,13 +131,28 @@ class PatternGenerator { relation.annotations.filter(DefinedByDerivedFeature).head.query } + private def allTypeReferences(LogicProblem problem) { + problem.eAllContents.filter(TypeReference).toIterable + } + protected def hasBoolean(LogicProblem problem) { + problem.allTypeReferences.exists[it instanceof BoolTypeReference] + } + protected def hasInteger(LogicProblem problem) { + problem.allTypeReferences.exists[it instanceof IntTypeReference] + } + protected def hasReal(LogicProblem problem) { + problem.allTypeReferences.exists[it instanceof RealTypeReference] + } + protected def hasString(LogicProblem problem) { + problem.allTypeReferences.exists[it instanceof StringTypeReference] + } + public def transformBaseProperties( LogicProblem problem, PartialInterpretation emptySolution, Map fqn2PQuery, TypeAnalysisResult typeAnalysisResult ) { - return ''' import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" @@ -146,7 +166,7 @@ class PatternGenerator { } ///////////////////////// - // 0.1 Existance + // 0.1 Existence ///////////////////////// private pattern mustExist(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement) { find interpretation(problem,interpetation); @@ -154,19 +174,52 @@ class PatternGenerator { } or { find interpretation(problem,interpetation); PartialInterpretation.newElements(interpetation,element); - } + } or { + find interpretation(problem,interpetation); + PartialInterpretation.booleanelements(interpetation,element); + } or { + find interpretation(problem,interpetation); + PartialInterpretation.integerelements(interpetation,element); + } or { + find interpretation(problem,interpetation); + PartialInterpretation.realelements(interpetation,element); + } + find interpretation(problem,interpetation); + PartialInterpretation.stringelements(interpetation,element); + } private pattern mayExist(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement) { find mustExist(problem,interpetation,element); } or { find interpretation(problem,interpetation); - neg find closeWorld(interpetation); + neg find elementCloseWorld(interpetation); PartialInterpretation.openWorldElementPrototypes(interpetation,element); + } or { + find interpretation(problem,interpetation); + neg find integerCloseWorld(interpetation); + PartialInterpretation.newIntegers(interpetation,element) + } or { + find interpretation(problem,interpetation); + neg find realCloseWorld(interpetation); + PartialInterpretation.newReals(interpetation,element) + } or { + find interpretation(problem,interpetation); + neg find stringCloseWorld(interpetation); + PartialInterpretation.newStrings(interpetation,element) } - private pattern closeWorld(interpetation:PartialInterpretation) { + private pattern elementCloseWorld(interpetation:PartialInterpretation) { PartialInterpretation.maxNewElements(interpetation,0); } + private pattern integerCloseWorld(interpetation:PartialInterpretation) { + PartialInterpretation.maxNewIntegers(interpetation,0); + } + private pattern realCloseWorld(interpetation:PartialInterpretation) { + PartialInterpretation.maxNewReals(interpetation,0); + } + private pattern stringCloseWorld(interpetation:PartialInterpretation) { + PartialInterpretation.maxNewStrings(interpetation,0); + } //////////////////////// // 0.2 Equivalence @@ -187,6 +240,37 @@ class PatternGenerator { ////////// // 1.1 Type Indexers ////////// + // 1.1.1 primitive Type Indexers + ////////// + pattern instaneofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + find interpretation(problem,interpretation); + PartialInterpretation.booleanelements(interpretation,element); + } + pattern instaneofInteger(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + find interpretation(problem,interpretation); + PartialInterpretation.integerelements(interpretation,element); + } or { + find interpretation(problem,interpretation); + PartialInterpretation.newIntegers(interpetation,element); + } + pattern instaneofReal(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + find interpretation(problem,interpretation); + PartialInterpretation.realements(interpretation,element); + } or { + find interpretation(problem,interpretation); + PartialInterpretation.newReals(interpetation,element); + } + pattern instaneofString(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + find interpretation(problem,interpretation); + PartialInterpretation.stringelements(interpretation,element); + } or { + find interpretation(problem,interpretation); + PartialInterpretation.newStrings(interpetation,element); + } + + ////////// + // 1.1.2 domain-specific Type Indexers + ////////// «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)» ////////// diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend index e6d92cc6..f384cd50 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend @@ -1,10 +1,8 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality import java.util.HashMap @@ -86,8 +84,8 @@ class RelationDeclarationIndexer { find mayExist(problem, interpretation, source); find mayExist(problem, interpretation, target); // Type consistency - «transformTypeConsistency(relation.parameters.get(0),"source")» - «transformTypeConsistency(relation.parameters.get(1),"target")» + «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")» + «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")» «IF upperMultiplicities.containsKey(relation)» // There are "numberOfExistingReferences" currently existing instances of the reference from the source, // the upper bound of the multiplicity should be considered. @@ -142,13 +140,4 @@ class RelationDeclarationIndexer { «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)» } ''' - - protected def CharSequence transformTypeConsistency(TypeReference reference, String name) { - if(reference instanceof ComplexTypeReference) { - this.base.typeIndexer.referInstanceOf(reference.referred,Modality.MAY,name) - } else { - return '''// Primitive type of «name» is already enforced''' - } - - } } \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend index 7792eccb..b400652f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend @@ -103,7 +103,10 @@ class RelationDefinitionIndexer { constraint.getVariableInTuple(1).canonizeName, modality.toMustMay) } else if (key instanceof EAttribute) { - return '''// attribute reference omitted'''//base.referRelationByName() + return base.referAttributeByName(key, + constraint.getVariableInTuple(0).canonizeName, + constraint.getVariableInTuple(1).canonizeName, + modality.toMustMay) } else throw new UnsupportedOperationException('''unknown key: «key.class»''') } else { throw new UnsupportedOperationException() diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend index 7b175227..f9e9baea 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend @@ -30,8 +30,8 @@ class RelationRefinementGenerator { «ENDIF» find mustExist(problem, interpretation, from); find mustExist(problem, interpretation, to); - «base.typeIndexer.referInstanceOf((relationRefinement.key.parameters.get(0) as ComplexTypeReference).referred, Modality::MUST,"from")» - «base.typeIndexer.referInstanceOf((relationRefinement.key.parameters.get(1) as ComplexTypeReference).referred, Modality::MUST,"to")» + «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» + «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend index 6c450664..9afec0de 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend @@ -6,11 +6,33 @@ import org.eclipse.emf.ecore.EClass import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference -interface TypeIndexer { +abstract class TypeIndexer { public def CharSequence getRequiredQueries() public def boolean requiresTypeAnalysis() public def CharSequence generateInstanceOfQueries(LogicProblem problem,PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) public def CharSequence referInstanceOf(Type type, Modality modality, String variableName) public def CharSequence referInstanceOf(EClass type, Modality modality, String variableName) + + public def dispatch CharSequence referInstanceOfByReference(ComplexTypeReference reference, Modality modality, String variableName) { + reference.referred.referInstanceOf(modality,variableName) + } + public def dispatch CharSequence referInstanceOfByReference(BoolTypeReference reference, Modality modality, String variableName) { + '''find instaneofBoolean(problem, interpretation, «variableName»);''' + } + public def dispatch CharSequence referInstanceOfByReference(IntTypeReference reference, Modality modality, String variableName) { + '''find pattern instaneofInteger(problem, interpretation, «variableName»);''' + } + public def dispatch CharSequence referInstanceOfByReference(RealTypeReference reference, Modality modality, String variableName) { + '''find pattern instaneofReal(problem, interpretation, «variableName»);''' + } + public def dispatch CharSequence referInstanceOfByReference(StringTypeReference reference, Modality modality, String variableName) { + '''find pattern instaneofString(problem, interpretation, «variableName»);''' + } + } \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend index 4e30ec78..73e43d52 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend @@ -9,7 +9,7 @@ import org.eclipse.emf.ecore.EClass import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeRefinementPrecondition import java.util.Collections -class TypeIndexerWithPreliminaryTypeAnalysis implements TypeIndexer{ +class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ val PatternGenerator base; new(PatternGenerator base) { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2Logic.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2Logic.xtend index 216ae348..d2b59754 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2Logic.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2Logic.xtend @@ -13,10 +13,9 @@ class InstanceModel2Logic { public def transform( TracedOutput metamodelTranslationResult, - List objects, - TypeScopes typeScopes) + List objects) { - val res1 = this.instanceModel2PartialInterpretation.transform(metamodelTranslationResult,objects,true,typeScopes) + val res1 = instanceModel2PartialInterpretation.transform(metamodelTranslationResult,objects,true) this.partialInterpretation2Logic.transformPartialIntepretation2Logic(metamodelTranslationResult.output,res1) return metamodelTranslationResult//.output } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend index 4c6cf769..080ad963 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend @@ -30,22 +30,20 @@ class InstanceModel2PartialInterpretation { public def transform( TracedOutput metamodelTranslationResult, Resource resource, - boolean withID, - TypeScopes typeScopes) + boolean withID) { val objects = resource.allContents.toList - return transform(metamodelTranslationResult,objects,withID,typeScopes) + return transform(metamodelTranslationResult,objects,withID) } public def transform( TracedOutput metamodelTranslationResult, List objects, - boolean withID, - TypeScopes typeScopes) + boolean withID) { val problem = metamodelTranslationResult.output val ecore2LogicTrace = metamodelTranslationResult.trace - val tracedOutput = partialInterpretationInitialiser.initialisePartialInterpretation(problem, typeScopes) + val tracedOutput = partialInterpretationInitialiser.initialisePartialInterpretation(problem, new TypeScopes) val partialInterpretation = tracedOutput.output val partialInterpretationTrace = tracedOutput.trace -- cgit v1.2.3-54-g00ecf