From 6bd475a3eced9d9a912f76e24f91d2ad8da13d54 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Mon, 25 Jun 2018 00:16:48 +0200 Subject: Fixing multiple true/false + bug preventing generation without PS --- .../logic2viatra/patterns/GenericTypeIndexer.xtend | 7 ++++++ .../patterns/GenericTypeRefinementGenerator.xtend | 10 ++++----- .../logic2viatra/patterns/PatternGenerator.xtend | 26 +++++++++++----------- .../logic2viatra/patterns/TypeIndexer.xtend | 14 ++++++++++++ .../TypeIndexerWithPreliminaryTypeAnalysis.xtend | 26 +++++++++++++--------- ...TypeRefinementWithPreliminaryTypeAnalysis.xtend | 11 ++++----- 6 files changed, 60 insertions(+), 34 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns') 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 2dae95be..dce04a7f 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 @@ -80,6 +80,11 @@ class GenericTypeIndexer extends TypeIndexer { 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 { @@ -94,6 +99,8 @@ class GenericTypeIndexer extends TypeIndexer { 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 { 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 1aa3b955..2e03d6ed 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 @@ -28,7 +28,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { private pattern hasElementInContainment(problem:LogicProblem, interpretation:PartialInterpretation) «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{ find interpretation(problem,interpretation); - «base.typeIndexer.referInstanceOf(type,Modality.MAY,"root")» + «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» find mustExist(problem, interpretation, root); }«ENDFOR» «FOR type:newObjectTypes» @@ -37,7 +37,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { «IF inverseRelations.containsKey(containmentRelation)» pattern «this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)»( problem:LogicProblem, interpretation:PartialInterpretation, - relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation ,typeInterpretation:PartialTypeInterpratation, + relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation ,typeInterpretation:PartialComplexTypeInterpretation, container:DefinedElement) { find interpretation(problem,interpretation); @@ -56,7 +56,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { «ELSE» pattern «this.patternName(containmentRelation,null,type)»( problem:LogicProblem, interpretation:PartialInterpretation, - relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialTypeInterpratation, + relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation, container:DefinedElement) { find interpretation(problem,interpretation); @@ -74,7 +74,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { «ENDFOR» pattern «patternName(null,null,type)»( problem:LogicProblem, interpretation:PartialInterpretation, - typeInterpretation:PartialTypeInterpratation) + typeInterpretation:PartialComplexTypeInterpretation) { find interpretation(problem,interpretation); neg find hasElementInContainment(problem,interpretation); @@ -87,7 +87,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { «ELSE» pattern createObject_«this.patternName(null,null,type)»( problem:LogicProblem, interpretation:PartialInterpretation, - typeInterpretation:PartialTypeInterpratation) + typeInterpretation:PartialComplexTypeInterpretation) { find interpretation(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); 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 001ff13f..0fed5c76 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 @@ -163,35 +163,35 @@ class PatternGenerator { ////////// // 0. Util ////////// - private pattern interpretation(problem:LogicProblem, interpetation:PartialInterpretation) { - PartialInterpretation.problem(interpetation,problem); + private pattern interpretation(problem:LogicProblem, interpretation:PartialInterpretation) { + PartialInterpretation.problem(interpretation,problem); } ///////////////////////// // 0.1 Existence ///////////////////////// - private pattern mustExist(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement) { - find interpretation(problem,interpetation); + private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + find interpretation(problem,interpretation); LogicProblem.elements(problem,element); } or { - find interpretation(problem,interpetation); - PartialInterpretation.newElements(interpetation,element); + find interpretation(problem,interpretation); + PartialInterpretation.newElements(interpretation,element); } - private pattern mayExist(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement) { - find mustExist(problem,interpetation,element); + private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + find mustExist(problem,interpretation,element); } or { - find interpretation(problem,interpetation); - neg find elementCloseWorld(interpetation); - PartialInterpretation.openWorldElements(interpetation,element); + find interpretation(problem,interpretation); + neg find elementCloseWorld(element); + PartialInterpretation.openWorldElements(interpretation,element); } private pattern elementCloseWorld(element:DefinedElement) { PartialInterpretation.newElements(i,element); PartialInterpretation.maxNewElements(i,0); } or { - Scope.targetTypeInterpretation(scope,interpetation); - PartialTypeInterpratation.elements(interpetation,element); + Scope.targetTypeInterpretation(scope,interpretation); + PartialTypeInterpratation.elements(interpretation,element); Scope.maxNewElements(scope,0); } 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 630fad51..d1d57189 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 @@ -11,6 +11,7 @@ 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 +import java.math.BigDecimal abstract class TypeIndexer { public def CharSequence getRequiredQueries() @@ -34,5 +35,18 @@ abstract class TypeIndexer { public def dispatch CharSequence referInstanceOfByReference(StringTypeReference reference, Modality modality, String variableName) { '''StringElement(«variableName»);''' } + public def dispatch CharSequence referPrimitiveValue(String variableName, Boolean value) { + '''BooleanElement.value(«variableName»,«value»);''' + } + public def dispatch CharSequence referPrimitiveValue(String variableName, Integer value) { + '''IntegerElement.value(«variableName»,«value»);''' + } + public 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) { + '''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 7bdb9a5b..fde5f4b6 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,10 +4,9 @@ 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 -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeRefinementPrecondition -import java.util.Collections class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ val PatternGenerator base; @@ -18,22 +17,26 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ override requiresTypeAnalysis() { true } override getRequiredQueries() ''' - private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { - find interpretation(problem,interpetation); + private pattern typeInterpretation(problem:LogicProblem, interpretation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { + find interpretation(problem,interpretation); LogicProblem.types(problem,type); - PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); } - private pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { - find interpretation(problem,interpetation); + 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,interpetation); - find typeInterpretation(problem,interpetation,type,typeInterpretation); + 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) { @@ -73,15 +76,16 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ * 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»{ + «IF inhibitorTypes !== null»{ find interpretation(problem,interpretation); PartialInterpretation.newElements(interpretation,element); «FOR inhibitorType : inhibitorTypes» neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» «ENDFOR» + neg find isPrimitive(element); } or { find interpretation(problem,interpretation); - PartialInterpretation.openWorldElements(interpetation,element); + PartialInterpretation.openWorldElements(interpretation,element); } or «ENDIF» { «referInstanceOf(type,Modality.MUST,"element")» } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend index 7c5f507b..cbbbcb08 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend @@ -27,7 +27,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ private pattern hasElementInContainment(problem:LogicProblem, interpretation:PartialInterpretation) «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{ find interpretation(problem,interpretation); - «base.typeIndexer.referInstanceOf(type,Modality.MAY,"root")» + «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» find mustExist(problem, interpretation, root); }«ENDFOR» «FOR type:possibleNewDynamicType» @@ -36,7 +36,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ «IF inverseRelations.containsKey(containmentRelation)» pattern «this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)»( problem:LogicProblem, interpretation:PartialInterpretation, - relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation, typeInterpretation:PartialTypeInterpratation, + relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation, container:DefinedElement) { find interpretation(problem,interpretation); @@ -55,7 +55,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ «ELSE» pattern «this.patternName(containmentRelation,null,type)»( problem:LogicProblem, interpretation:PartialInterpretation, - relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialTypeInterpratation, + relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation, container:DefinedElement) { find interpretation(problem,interpretation); @@ -73,7 +73,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ «ENDFOR» pattern «patternName(null,null,type)»( problem:LogicProblem, interpretation:PartialInterpretation, - typeInterpretation:PartialTypeInterpratation) + typeInterpretation:PartialComplexTypeInterpretation) { find interpretation(problem,interpretation); neg find hasElementInContainment(problem,interpretation); @@ -86,7 +86,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ «ELSE» pattern «this.patternName(null,null,type)»( problem:LogicProblem, interpretation:PartialInterpretation, - typeInterpretation:PartialTypeInterpratation) + typeInterpretation:PartialComplexTypeInterpretation) { find interpretation(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); @@ -107,6 +107,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ pattern refineTypeTo_«base.canonizeName(newTypeRefinement.targetType.name)»(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) { find interpretation(problem,interpretation); PartialInterpretation.newElements(interpretation,element); + «base.typeIndexer.referInstanceOf(newTypeRefinement.targetType,Modality.MAY,"element")» «FOR inhibitorType : newTypeRefinement.inhibitorTypes» neg «base.typeIndexer.referInstanceOf(inhibitorType,Modality.MUST,"element")» «ENDFOR» -- cgit v1.2.3-54-g00ecf