From 4cb0aa5a0b9adac2bb8d4a995be015651bdd5628 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 30 Jul 2019 18:57:01 +0200 Subject: Polyhedron scope propagator for non-containment references --- .../viatrasolver/logic2viatra/Modality.java | 31 +- .../cardinality/PolyhedronScopePropagator.xtend | 80 ++++- .../logic2viatra/patterns/GenericTypeIndexer.xtend | 321 +++++++++------------ .../patterns/GenericTypeRefinementGenerator.xtend | 184 ++++++------ .../logic2viatra/patterns/TypeIndexer.xtend | 122 ++++++-- .../TypeIndexerWithPreliminaryTypeAnalysis.xtend | 144 +++------ .../logic2viatra/patterns/UnfinishedIndexer.xtend | 15 +- .../viatrasolver/reasoner/ViatraReasoner.xtend | 3 +- .../dse/InconsistentScopeGlobalConstraint.xtend | 25 ++ .../SurelyViolatedObjectiveGlobalConstraint.xtend | 4 +- .../reasoner/dse/UnfinishedWFObjective.xtend | 22 +- 11 files changed, 515 insertions(+), 436 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java index d2132cea..f3a6ec32 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java @@ -2,21 +2,46 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra; public enum Modality { MUST, MAY, CURRENT; + public boolean isMust() { return this == MUST; } + public boolean isMay() { return this == MAY; } + public boolean isCurrent() { return this == CURRENT; } + public boolean isMustOrCurrent() { return isMust() || isCurrent(); } + public Modality getDual() { - if(this.isCurrent()) return CURRENT; - else if(this.isMust())return MAY; - else return MUST; + switch (this) { + case CURRENT: + return CURRENT; + case MUST: + return MAY; + case MAY: + return MUST; + default: + throw new UnsupportedOperationException("Unknown Modality: " + this); + } + } + + public Modality toBase() { + if (this.isCurrent()) { + return MUST; + } else { + return this; + } + } + + @Override + public String toString() { + return super.toString().toLowerCase(); } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index e9c155f5..f6b101b6 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend @@ -50,7 +50,7 @@ class PolyhedronScopePropagator extends ScopePropagator { throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") } if (maximumNumberOfNewNodes <= 0) { - throw new IllegalStateException("Maximum number of new nodes is negative") + throw new IllegalStateException("Maximum number of new nodes is not positive") } builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, maximumNumberOfNewNodes) @@ -65,7 +65,7 @@ class PolyhedronScopePropagator extends ScopePropagator { val result = operator.saturate() // println(polyhedron) if (result == PolyhedronSaturationResult.EMPTY) { - throw new IllegalStateException("Scope bounds cannot be satisfied") + setScopesInvalid() } else { populateScopesFromPolyhedron() if (result != PolyhedronSaturationResult.SATURATED) { @@ -146,6 +146,15 @@ class PolyhedronScopePropagator extends ScopePropagator { } } + private def setScopesInvalid() { + partialInterpretation.minNewElements = Integer.MAX_VALUE + partialInterpretation.maxNewElements = 0 + for (scope : partialInterpretation.scopes) { + scope.minNewElements = Integer.MAX_VALUE + scope.maxNewElements = 0 + } + } + private static def getCalculatedMultiplicity(ViatraQueryMatcher matcher, PartialInterpretation p) { val match = matcher.newEmptyMatch @@ -276,6 +285,37 @@ class PolyhedronScopePropagator extends ScopePropagator { private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, UnifinishedMultiplicityQueries queries) { + if (constraint.constrainsRemainingInverse) { + if (queries.unfinishedMultiplicityQuery === null) { + throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries") + } + val unfinishedMultiplicityMatcher = queries.unfinishedMultiplicityQuery.getMatcher(queryEngine) + if (queries.remainingInverseMultiplicityQuery === null) { + throw new IllegalArgumentException( + "Reference constraints need remaining inverse multiplicity queries") + } + val remainingInverseMultiplicityMatcher = queries.remainingInverseMultiplicityQuery.getMatcher( + queryEngine) + val availableMultiplicityCoefficients = new HashMap + availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, + subtypeDimensions.get(constraint.targetType)) + availableMultiplicityCoefficients.addCoefficients(-constraint.lowerBound, + subtypeDimensions.get(constraint.targetType)) + val availableMultiplicity = availableMultiplicityCoefficients.toExpression + updatersBuilder.add( + new UnfinishedMultiplicityConstraintUpdater(constraint.relation.name, availableMultiplicity, + unfinishedMultiplicityMatcher, remainingInverseMultiplicityMatcher)) + } + if (constraint.constrainsUnrepairable) { + if (queries.unrepairableMultiplicityQuery === null) { + throw new IllegalArgumentException("Reference constraints need unrepairable multiplicity queries") + } + val unrepairableMultiplicityMatcher = queries.unrepairableMultiplicityQuery.getMatcher(queryEngine) + val targetTypeCardinality = typeBounds.get(constraint.targetType) + updatersBuilder.add( + new UnrepairableMultiplicityConstraintUpdater(constraint.relation.name, targetTypeCardinality, + unrepairableMultiplicityMatcher)) + } } private def addCoefficients(Map accumulator, int scale, Map a) { @@ -410,4 +450,40 @@ class PolyhedronScopePropagator extends ScopePropagator { matcher.countMatches(match) != 0 } } + + @FinalFieldsConstructor + static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { + val String name + val LinearBoundedExpression availableMultiplicityExpression + val ViatraQueryMatcher unfinishedMultiplicityMatcher + val ViatraQueryMatcher remainingInverseMultiplicityMatcher + + override update(PartialInterpretation p) { + val unfinishedMultiplicity = unfinishedMultiplicityMatcher.getCalculatedMultiplicity(p) + if (unfinishedMultiplicity === null) { + throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) + } + val remainingInverseMultiplicity = remainingInverseMultiplicityMatcher.getCalculatedMultiplicity(p) + if (remainingInverseMultiplicity === null) { + throw new IllegalArgumentException("Remaining inverse multiplicity is missing for " + name) + } + val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity + availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) + } + } + + @FinalFieldsConstructor + static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { + val String name + val LinearBoundedExpression targetCardinalityExpression + val ViatraQueryMatcher unrepairableMultiplicityMatcher + + override update(PartialInterpretation p) { + val value = unrepairableMultiplicityMatcher.getCalculatedMultiplicity(p) + if (value === null) { + throw new IllegalArgumentException("Unrepairable multiplicity is missing for " + name) + } + targetCardinalityExpression.tightenLowerBound(value) + } + } } 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 d6a15c1a..0e0f1f02 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 @@ -1,209 +1,150 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type -import org.eclipse.emf.ecore.EClass +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 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 extends TypeIndexer { - val PatternGenerator base; - new(PatternGenerator base) { - this.base = base + super(base) } + override requiresTypeAnalysis() { false } - - public override getRequiredQueries() ''' - private pattern newELement(interpretation: PartialInterpretation, element: DefinedElement) { - PartialInterpretation.newElements(interpretation,element); - } - - private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { - find interpretation(problem,interpetation); - LogicProblem.types(problem,type); - PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); - PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); - } - - private pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { - find interpretation(problem,interpetation); - find mustExist(problem,interpetation,element); - LogicProblem.types(problem,type); - TypeDefinition.elements(type,element); - } or { - find mustExist(problem,interpetation,element); - find typeInterpretation(problem,interpetation,type,typeInterpretation); - PartialComplexTypeInterpretation.elements(typeInterpretation,element); - } - - /** - * Direct supertypes of a type. - */ - private pattern supertypeDirect(subtype : Type, supertype : Type) { - Type.supertypes(subtype, supertype); - } - - /** - * All supertypes of a type. - */ - private pattern supertypeStar(subtype: Type, supertype: Type) { - subtype == supertype; - } or { - find supertypeDirect+(subtype,supertype); - } - - /// Complex type reasoning patterns /// - // - // In a valid type system, for each element e there is exactly one type T where - // 1: T(e) - but we dont know this for type declaration - // 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. - // 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: - // D(e) && D-->T && !T(e) - // 3: There is no T' that T'->T and T'(e) - // 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T: - // D(e) && ![T--->D] && T(e) - // 4: T is not abstract - // Such type T is called Dynamic type of e, while other types are called static types. - // - // The following patterns checks the possible dynamic types for an element - - private pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) { - // 1: T(e) - find directInstanceOf(problem,interpretation,element,dynamic); - // 2e is not true: D(e) && D-->T && !T(e) - neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); - // 3e is not true: D(e) && ![T--->D] && T(e) - neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); - // 4: T is not abstract - Type.isAbstract(dynamic,false); - } - - - private pattern isPrimitive(element: PrimitiveElement) { - PrimitiveElement(element); - } - - private pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) - // case 1: element is defined at least once - { - LogicProblem.types(problem,dynamic); - // select a random definition 'randomType' - find directInstanceOf(problem,interpretation,element,randomType); - // dynamic is a subtype of 'randomType' - find supertypeStar(dynamic,randomType); - // 2e is not true: D(e) && D-->T && !T(e) - neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); - // 3e is not true: D(e) && ![T--->D] && T(e) - neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); - // 4: T is not abstract - Type.isAbstract(dynamic,false); - // 5. element is not primitive datatype - neg find isPrimitive(element); - } or - // case 2: element is not defined anywhere - { - find mayExist(problem,interpretation,element); - // there is no definition - neg find directInstanceOf(problem,interpretation,element,_); - // 2e is not true: D(e) && D-->T && !T(e) - // because non of the definition contains element, the type cannot have defined supertype - LogicProblem.types(problem,dynamic); - PartialInterpretation.problem(interpretation,problem); - neg find typeWithDefinedSupertype(dynamic); - // 3e is not true: D(e) && ![T--->D] && T(e) - // because there is no definition, dynamic covers all definition + + override getRequiredQueries() ''' + «super.requiredQueries» + + /** + * Direct supertypes of a type. + */ + private pattern supertypeDirect(subtype : Type, supertype : Type) { + Type.supertypes(subtype, supertype); + } + + /** + * All supertypes of a type. + */ + private pattern supertypeStar(subtype: Type, supertype: Type) { + subtype == supertype; + } or { + find supertypeDirect+(subtype,supertype); + } + + /// Complex type reasoning patterns /// + // + // In a valid type system, for each element e there is exactly one type T where + // 1: T(e) - but we dont know this for type declaration + // 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. + // 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: + // D(e) && D-->T && !T(e) + // 3: There is no T' that T'->T and T'(e) + // 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T: + // D(e) && ![T--->D] && T(e) // 4: T is not abstract - Type.isAbstract(dynamic,false); - // 5. element is not primitive datatype - neg find isPrimitive(element); - } - - /** - * supertype -------> element <------- otherSupertype - * A A - * | | - * wrongDynamic -----------------------------X - */ - private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) { - find directInstanceOf(problem,interpretation,element,supertype); - find directInstanceOf(problem,interpretation,element,otherSupertype); - find supertypeStar(wrongDynamic,supertype); - neg find supertypeStar(wrongDynamic,otherSupertype); - } - - /** - * supertype -------> element <---X--- otherSupertype - * A A - * | | - * wrongDynamic -----------------------------+ - */ - private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) { - find directInstanceOf(problem,interpretation,element,supertype); - neg find elementInTypeDefinition(element,otherSupertype); - TypeDefinition(otherSupertype); - find supertypeStar(wrongDynamic, supertype); - find supertypeStar(wrongDynamic, otherSupertype); - } - - private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) { - TypeDefinition.elements(definition,element); - } - - private pattern typeWithDefinedSupertype(type:Type) { - find supertypeStar(type,definedSupertype); - TypeDefinition(definedSupertype); - } - - private pattern scopeDisallowsNewElementsFromType(typeInterpretation:PartialComplexTypeInterpretation) { - Scope.targetTypeInterpretation(scope,typeInterpretation); - Scope.maxNewElements(scope,0); - } - ''' - - public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) { - ''' - «FOR type:problem.types» - «problem.generateMustInstenceOf(type)» - «problem.generateMayInstanceOf(type)» - «ENDFOR» - ''' - } - - private def patternName(Type type, Modality modality) - '''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»''' - - private def generateMustInstenceOf(LogicProblem problem, Type type) { - ''' + // Such type T is called Dynamic type of e, while other types are called static types. + // + // The following patterns checks the possible dynamic types for an element + + private pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) { + // 1: T(e) + find directInstanceOf(problem,interpretation,element,dynamic); + // 2e is not true: D(e) && D-->T && !T(e) + neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); + // 3e is not true: D(e) && ![T--->D] && T(e) + neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); + // 4: T is not abstract + Type.isAbstract(dynamic,false); + } + + private pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) + // case 1: element is defined at least once + { + LogicProblem.types(problem,dynamic); + // select a random definition 'randomType' + find directInstanceOf(problem,interpretation,element,randomType); + // dynamic is a subtype of 'randomType' + find supertypeStar(dynamic,randomType); + // 2e is not true: D(e) && D-->T && !T(e) + neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); + // 3e is not true: D(e) && ![T--->D] && T(e) + neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); + // 4: T is not abstract + Type.isAbstract(dynamic,false); + // 5. element is not primitive datatype + neg find isPrimitive(element); + } or + // case 2: element is not defined anywhere + { + find mayExist(problem,interpretation,element); + // there is no definition + neg find directInstanceOf(problem,interpretation,element,_); + // 2e is not true: D(e) && D-->T && !T(e) + // because non of the definition contains element, the type cannot have defined supertype + LogicProblem.types(problem,dynamic); + PartialInterpretation.problem(interpretation,problem); + neg find typeWithDefinedSupertype(dynamic); + // 3e is not true: D(e) && ![T--->D] && T(e) + // because there is no definition, dynamic covers all definition + // 4: T is not abstract + Type.isAbstract(dynamic,false); + // 5. element is not primitive datatype + neg find isPrimitive(element); + } + /** - * An element must be an instance of type "«type.name»". + * supertype -------> element <------- otherSupertype + * A A + * | | + * wrongDynamic -----------------------------X */ - private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { - Type.name(type,"«type.name»"); - find directInstanceOf(problem,interpretation,element,type); + private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) { + find directInstanceOf(problem,interpretation,element,supertype); + find directInstanceOf(problem,interpretation,element,otherSupertype); + find supertypeStar(wrongDynamic,supertype); + neg find supertypeStar(wrongDynamic,otherSupertype); } - ''' - } - - private def generateMayInstanceOf(LogicProblem problem, Type type) { - ''' + /** - * An element may be an instance of type "«type.name»". + * supertype -------> element <---X--- otherSupertype + * A A + * | | + * wrongDynamic -----------------------------+ */ - private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { - Type.name(type,"«type.name»"); - find possibleDynamicType(problem,interpretation,dynamic,element); - find supertypeStar(dynamic,type); - neg find scopeDisallowsNewElementsFromType(dynamic); + private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) { + find directInstanceOf(problem,interpretation,element,supertype); + neg find elementInTypeDefinition(element,otherSupertype); + TypeDefinition(otherSupertype); + find supertypeStar(wrongDynamic, supertype); + find supertypeStar(wrongDynamic, otherSupertype); + } + + private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) { + TypeDefinition.elements(definition,element); + } + + private pattern typeWithDefinedSupertype(type:Type) { + find supertypeStar(type,definedSupertype); + TypeDefinition(definedSupertype); + } + + private pattern scopeDisallowsNewElementsFromType(typeInterpretation:PartialComplexTypeInterpretation) { + Scope.targetTypeInterpretation(scope,typeInterpretation); + Scope.maxNewElements(scope,0); } + ''' + + protected override generateMayInstanceOf(LogicProblem problem, Type type, TypeAnalysisResult typeAnalysisResult) { + ''' + /** + * An element may be an instance of type "«type.name»". + */ + private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + Type.name(type,"«type.name»"); + find possibleDynamicType(problem,interpretation,dynamic,element); + find supertypeStar(dynamic,type); + neg find scopeDisallowsNewElementsFromType(dynamic); + } ''' } - - public override referInstanceOf(Type type, Modality modality, String variableName) { - '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' - } - public override referInstanceOf(EClass type, Modality modality, String variableName) { - '''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''«type.name» class''')»(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/GenericTypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend index c9f6abce..52f0cbea 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend @@ -14,107 +14,111 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { new(PatternGenerator base) { super(base) } + override requiresTypeAnalysis() { false } - - override generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + + override generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, + TypeAnalysisResult typeAnalysisResult) { val containment = p.containmentHierarchies.head val newObjectTypes = p.types.filter(TypeDeclaration).filter[!isAbstract] val inverseRelations = new HashMap - p.annotations.filter(InverseRelationAssertion).forEach[ - inverseRelations.put(it.inverseA,it.inverseB) - inverseRelations.put(it.inverseB,it.inverseA) + p.annotations.filter(InverseRelationAssertion).forEach [ + inverseRelations.put(it.inverseA, it.inverseB) + inverseRelations.put(it.inverseB, it.inverseA) ] return ''' - pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation) - «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{ - find interpretation(problem,interpretation); - «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» - find mustExist(problem, interpretation, root); - }«ENDFOR» - «FOR type:newObjectTypes» - «IF(containment.typesOrderedInHierarchy.contains(type))» - «FOR containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]» - «IF inverseRelations.containsKey(containmentRelation)» - pattern «this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)»( - problem:LogicProblem, interpretation:PartialInterpretation, - relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation ,typeInterpretation:PartialComplexTypeInterpretation, - container:DefinedElement) - { - find interpretation(problem,interpretation); - PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); - PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); - PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); - PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation); - PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"«inverseRelations.get(containmentRelation).name»"); - «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» - «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» - «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» - find mustExist(problem, interpretation, container); - neg find mustExist(problem, interpretation, newObject); - } - «ELSE» - pattern «this.patternName(containmentRelation,null,type)»( - problem:LogicProblem, interpretation:PartialInterpretation, - relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation, - container:DefinedElement) - { - find interpretation(problem,interpretation); - PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); - PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); - PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); - «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» - «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» - «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» - find mustExist(problem, interpretation, container); - neg find mustExist(problem, interpretation, newObject); - } - «ENDIF» - «ENDFOR» - pattern «patternName(null,null,type)»( - problem:LogicProblem, interpretation:PartialInterpretation, - typeInterpretation:PartialComplexTypeInterpretation) - { + pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation) + «FOR type : containment.typesOrderedInHierarchy SEPARATOR "or"»{ find interpretation(problem,interpretation); - neg find «hasElementInContainmentName»(problem,interpretation); - PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialComplexTypeInterpretation.interpretationOf.name(type,"«type.name»"); - «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» - find mayExist(problem, interpretation, newObject); - neg find mustExist(problem, interpretation, newObject); - } - «ELSE» - pattern createObject_«this.patternName(null,null,type)»( - problem:LogicProblem, interpretation:PartialInterpretation, - typeInterpretation:PartialComplexTypeInterpretation) - { - find interpretation(problem,interpretation); - PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); - «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» - find mayExist(problem, interpretation, newObject); - neg find mustExist(problem, interpretation, newObject); - } - «ENDIF» - «ENDFOR» + «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» + find mustExist(problem, interpretation, root); + }«ENDFOR» + «FOR type : newObjectTypes» + «IF(containment.typesOrderedInHierarchy.contains(type))» + «FOR containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]» + «IF inverseRelations.containsKey(containmentRelation)» + pattern «this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation ,typeInterpretation:PartialComplexTypeInterpretation, + container:DefinedElement) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); + PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); + PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation); + PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"«inverseRelations.get(containmentRelation).name»"); + «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» + «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» + find mustExist(problem, interpretation, container); + neg find mustExist(problem, interpretation, newObject); + } + «ELSE» + pattern «this.patternName(containmentRelation,null,type)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation, + container:DefinedElement) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); + PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); + «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» + «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» + find mustExist(problem, interpretation, container); + neg find mustExist(problem, interpretation, newObject); + } + «ENDIF» + «ENDFOR» + pattern «patternName(null,null,type)»( + problem:LogicProblem, interpretation:PartialInterpretation, + typeInterpretation:PartialComplexTypeInterpretation) + { + find interpretation(problem,interpretation); + neg find «hasElementInContainmentName»(problem,interpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialComplexTypeInterpretation.interpretationOf.name(type,"«type.name»"); + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» + find mayExist(problem, interpretation, newObject); + neg find mustExist(problem, interpretation, newObject); + } + «ELSE» + pattern createObject_«this.patternName(null,null,type)»( + problem:LogicProblem, interpretation:PartialInterpretation, + typeInterpretation:PartialComplexTypeInterpretation) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» + find mayExist(problem, interpretation, newObject); + neg find mustExist(problem, interpretation, newObject); + } + «ENDIF» + «ENDFOR» ''' } - override generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + override generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, + TypeAnalysisResult typeAnalysisResult) { return ''' - «FOR type : p.types.filter(TypeDeclaration).filter[!it.isAbstract]» - pattern refineTypeTo_«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation, object: DefinedElement) { - find interpretation(problem,interpretation); - find mustExist(problem, interpretation, object); - «base.typeIndexer.referInstanceOf(type,Modality.MAY,"object")» - neg «base.typeIndexer.referInstanceOf(type,Modality.MUST,"object")» - } - «ENDFOR» + «FOR type : p.types.filter(TypeDeclaration).filter[!it.isAbstract]» + pattern refineTypeTo_«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation, object: DefinedElement) { + find interpretation(problem,interpretation); + find mustExist(problem, interpretation, object); + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"object")» + neg «base.typeIndexer.referInstanceOf(type,Modality.MUST,"object")» + } + «ENDFOR» ''' } - - override getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + + override getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, + TypeAnalysisResult typeAnalysisResult) { p.types.filter(TypeDeclaration).toInvertedMap['''refineTypeTo_«base.canonizeName(it.name)»'''] - } -} \ 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/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 d1d57189..7d687e99 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 @@ -1,52 +1,122 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type -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.ComplexTypeReference 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 +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import java.math.BigDecimal +import org.eclipse.emf.ecore.EClass +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor +@FinalFieldsConstructor 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) { + @Accessors(PROTECTED_GETTER) val PatternGenerator base + + def CharSequence getRequiredQueries() ''' + private pattern typeInterpretation(problem:LogicProblem, interpretation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { + find interpretation(problem,interpretation); + LogicProblem.types(problem,type); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); + } + + private pattern directInstanceOf(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, type:Type) { + find interpretation(problem,interpretation); + LogicProblem.types(problem,type); + TypeDefinition.elements(type,element); + } or { + find interpretation(problem,interpretation); + find typeInterpretation(problem,interpretation,type,typeInterpretation); + PartialComplexTypeInterpretation.elements(typeInterpretation,element); + } + + private pattern isPrimitive(element: PrimitiveElement) { + PrimitiveElement(element); + } + ''' + + def boolean requiresTypeAnalysis() + + def CharSequence generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution, + TypeAnalysisResult typeAnalysisResult) ''' + «FOR type : problem.types» + «problem.generateMustInstenceOf(type, typeAnalysisResult)» + «problem.generateMayInstanceOf(type, typeAnalysisResult)» + «ENDFOR» + ''' + + protected def CharSequence generateMustInstenceOf(LogicProblem problem, Type type, + TypeAnalysisResult typeAnalysisResult) ''' + /** + * An element must be an instance of type "«type.name»". + */ + private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + Type.name(type,"«type.name»"); + find directInstanceOf(problem,interpretation,element,type); + } + ''' + + protected def CharSequence generateMayInstanceOf(LogicProblem problem, Type type, + TypeAnalysisResult typeAnalysisResult) + + protected def patternName(Type type, + Modality modality) '''«modality.toBase»InstanceOf«base.canonizeName(type.name)»''' + + def referInstanceOf(Type type, Modality modality, String variableName) { + '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' + } + + def referInstanceOf(EClass type, Modality modality, String variableName) { + '''find «modality.toBase»InstanceOf«base.canonizeName('''«type.name» class''')»(problem,interpretation,«variableName»);''' + } + + def dispatch CharSequence referInstanceOfByReference(ComplexTypeReference reference, Modality modality, + String variableName) { + reference.referred.referInstanceOf(modality, variableName) + } + + def dispatch CharSequence referInstanceOfByReference(BoolTypeReference reference, Modality modality, + String variableName) { '''BooleanElement(«variableName»);''' } - public def dispatch CharSequence referInstanceOfByReference(IntTypeReference reference, Modality modality, String variableName) { + + def dispatch CharSequence referInstanceOfByReference(IntTypeReference reference, Modality modality, + String variableName) { '''IntegerElement(«variableName»);''' } - public def dispatch CharSequence referInstanceOfByReference(RealTypeReference reference, Modality modality, String variableName) { + + def dispatch CharSequence referInstanceOfByReference(RealTypeReference reference, Modality modality, + String variableName) { '''RealElement(«variableName»);''' } - public def dispatch CharSequence referInstanceOfByReference(StringTypeReference reference, Modality modality, String variableName) { + + def dispatch CharSequence referInstanceOfByReference(StringTypeReference reference, Modality modality, + String variableName) { '''StringElement(«variableName»);''' } - public def dispatch CharSequence referPrimitiveValue(String variableName, Boolean value) { + + def dispatch CharSequence referPrimitiveValue(String variableName, Boolean value) { '''BooleanElement.value(«variableName»,«value»);''' } - public def dispatch CharSequence referPrimitiveValue(String variableName, Integer value) { + + def dispatch CharSequence referPrimitiveValue(String variableName, Integer value) { '''IntegerElement.value(«variableName»,«value»);''' } - public def dispatch CharSequence referPrimitiveValue(String variableName, BigDecimal value) { + + def dispatch CharSequence referPrimitiveValue(String variableName, BigDecimal value) { '''RealElement.value(«variableName»,«value»);''' } - ///TODO: de-escaping string literals - public def dispatch CharSequence referPrimitiveValue(String variableName, String value) { + + def dispatch CharSequence referPrimitiveValue(String variableName, String value) { + // /TODO: de-escaping string literals '''StringElement.value(«variableName»,"«value»");''' } -} \ 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 d3af0426..0393b803 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 @@ -4,113 +4,51 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeRefinementPrecondition -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation -import org.eclipse.emf.ecore.EClass -class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ - val PatternGenerator base; - +class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer { new(PatternGenerator base) { - this.base = base + super(base) } + override requiresTypeAnalysis() { true } - - override getRequiredQueries() ''' - private pattern typeInterpretation(problem:LogicProblem, interpretation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { - find interpretation(problem,interpretation); - LogicProblem.types(problem,type); - PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); - } - - private pattern directInstanceOf(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, type:Type) { - find interpretation(problem,interpretation); - LogicProblem.types(problem,type); - TypeDefinition.elements(type,element); - } or { - find interpretation(problem,interpretation); - find typeInterpretation(problem,interpretation,type,typeInterpretation); - PartialComplexTypeInterpretation.elements(typeInterpretation,element); - } - - private pattern isPrimitive(element: PrimitiveElement) { - PrimitiveElement(element); - } - ''' - - override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { - val mayNewTypePreconditions = typeAnalysisResult.mayNewTypePreconditions - - return ''' - «FOR type:problem.types» - «problem.generateMustInstenceOf(type)» - «problem.generateMayInstanceOf(type,mayNewTypePreconditions.get(type))» - «ENDFOR» - ''' - } - - private def patternName(Type type, Modality modality) - '''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»''' - - private def generateMustInstenceOf(LogicProblem problem, Type type) { - ''' - /** - * An element must be an instance of type "«type.name»". - */ - private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { - Type.name(type,"«type.name»"); - find directInstanceOf(problem,interpretation,element,type); - } - ''' - } - - private def generateMayInstanceOf(LogicProblem problem, Type type, TypeRefinementPrecondition precondition) { - val inhibitorTypes = if(precondition!=null) { - precondition.inhibitorTypes - } else { - null - } + + protected override generateMayInstanceOf(LogicProblem problem, Type type, TypeAnalysisResult typeAnalysisResult) { + val precondition = typeAnalysisResult?.mayNewTypePreconditions?.get(type) + val inhibitorTypes = precondition?.inhibitorTypes ''' - private pattern scopeDisallowsNew«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation) { - find interpretation(problem,interpretation); - PartialInterpretation.scopes(interpretation,scope); - Scope.targetTypeInterpretation(scope,typeInterpretation); - Scope.maxNewElements(scope,0); - PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); - Type.name(type,"«type.name»"); - } - - /** - * An element may be an instance of type "«type.name»". - */ - private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) - «IF inhibitorTypes !== null»{ - find interpretation(problem,interpretation); - PartialInterpretation.newElements(interpretation,element); - «FOR inhibitorType : inhibitorTypes» - neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» - «ENDFOR» - neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); - neg find isPrimitive(element); - } or { - find interpretation(problem,interpretation); - PartialInterpretation.openWorldElements(interpretation,element); - «FOR inhibitorType : inhibitorTypes» - neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» - «ENDFOR» - neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); - neg find isPrimitive(element); - } or - «ENDIF» - { «referInstanceOf(type,Modality.MUST,"element")» } + private pattern scopeDisallowsNew«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation) { + find interpretation(problem,interpretation); + PartialInterpretation.scopes(interpretation,scope); + Scope.targetTypeInterpretation(scope,typeInterpretation); + Scope.maxNewElements(scope,0); + PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); + Type.name(type,"«type.name»"); + } + + /** + * An element may be an instance of type "«type.name»". + */ + private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) + «IF inhibitorTypes !== null» + { + find interpretation(problem,interpretation); + PartialInterpretation.newElements(interpretation,element); + «FOR inhibitorType : inhibitorTypes» + neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» + «ENDFOR» + neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); + neg find isPrimitive(element); + } or { + find interpretation(problem,interpretation); + PartialInterpretation.openWorldElements(interpretation,element); + «FOR inhibitorType : inhibitorTypes» + neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» + «ENDFOR» + neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); + neg find isPrimitive(element); + } or + «ENDIF» + { «referInstanceOf(type,Modality.MUST,"element")» } ''' } - - public override referInstanceOf(Type type, Modality modality, String variableName) { - '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' - } - public override referInstanceOf(EClass type, Modality modality, String variableName) { - '''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''«type.name» class''')»(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/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend index 286756a8..15b5a047 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend @@ -74,7 +74,7 @@ class UnfinishedIndexer { «ENDIF» «IF indexUpperMultiplicities» - «IF constraint.constrainsUnrepairable» + «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse» private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { find interpretation(problem,interpretation); find mustExist(problem,interpretation,source); @@ -84,15 +84,17 @@ class UnfinishedIndexer { neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» } - + «ENDIF» + + «IF constraint.constrainsUnrepairable» private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { find interpretation(problem,interpretation); find mustExist(problem,interpretation,object); «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); - numerOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); - check(numerOfRepairMatches < missingMultiplicity); - unrepairableMultiplicity == eval(missingMultiplicity-numerOfRepairMatches); + numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); + check(numberOfRepairMatches < missingMultiplicity); + unrepairableMultiplicity == eval(missingMultiplicity-numberOfRepairMatches); } private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) { @@ -112,7 +114,8 @@ class UnfinishedIndexer { «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» check(numberOfExistingReferences < «constraint.inverseUpperBound»); - remainingMultiplicity == eval(«constraint.inverseUpperBound»-numberOfExistingReferences); + numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object); + remainingMultiplicity == eval(Math.min(«constraint.inverseUpperBound»-numberOfExistingReferences, numberOfRepairMatches)); } pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { 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 101f0a3e..a8db5e43 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 @@ -12,7 +12,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage @@ -21,6 +20,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.sta import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation @@ -130,6 +130,7 @@ class ViatraReasoner extends LogicReasoner { dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationGlobalConstraint(method.invalidWF)) dse.addGlobalConstraint(new SurelyViolatedObjectiveGlobalConstraint(solutionSaver)) + dse.addGlobalConstraint(new InconsistentScopeGlobalConstraint) for (additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) { dse.addGlobalConstraint(additionalConstraint.apply(method)) } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend new file mode 100644 index 00000000..2e039ca2 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend @@ -0,0 +1,25 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse + +import org.eclipse.viatra.dse.objectives.IGlobalConstraint +import org.eclipse.viatra.dse.base.ThreadContext +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation + +class InconsistentScopeGlobalConstraint implements IGlobalConstraint { + + override init(ThreadContext context) { + // Nothing to initialize. + } + + override createNew() { + this + } + + override getName() { + class.name + } + + override checkGlobalConstraint(ThreadContext context) { + val partialModel = context.model as PartialInterpretation + partialModel.minNewElements <= partialModel.maxNewElements || partialModel.maxNewElements < 0 + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend index f54a31ca..8ed3e912 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend @@ -9,9 +9,7 @@ class SurelyViolatedObjectiveGlobalConstraint implements IGlobalConstraint { val ViatraReasonerSolutionSaver solutionSaver override init(ThreadContext context) { - if (solutionSaver !== null) { - return - } + // Nothing to initialize. } override createNew() { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend index e0111cf6..bf34aeeb 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend @@ -1,23 +1,21 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse -import org.eclipse.viatra.dse.objectives.IObjective -import org.eclipse.viatra.query.runtime.api.IPatternMatch -import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher -import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import java.util.ArrayList import java.util.Collection -import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine -import org.eclipse.viatra.query.runtime.emf.EMFScope -import org.eclipse.viatra.dse.base.ThreadContext +import java.util.Comparator import java.util.List +import org.eclipse.viatra.dse.base.ThreadContext import org.eclipse.viatra.dse.objectives.Comparators -import java.util.ArrayList -import java.util.Comparator +import org.eclipse.viatra.dse.objectives.IObjective +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher class UnfinishedWFObjective implements IObjective { Collection>> unfinishedWFs val List> matchers - public new(Collection>> unfinishedWFs) { + new(Collection>> unfinishedWFs) { this.unfinishedWFs = unfinishedWFs matchers = new ArrayList(unfinishedWFs.size) } @@ -48,9 +46,9 @@ class UnfinishedWFObjective implements IObjective { override satisifiesHardObjective(Double fitness) { return fitness <=0.01 } override setComparator(Comparator comparator) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + throw new UnsupportedOperationException() } override setLevel(int level) { - throw new UnsupportedOperationException("TODO: auto-generated method stub") + throw new UnsupportedOperationException() } } \ No newline at end of file -- cgit v1.2.3-54-g00ecf