aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2Logic.xtend22
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend144
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend172
3 files changed, 338 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2Logic.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2Logic.xtend
new file mode 100644
index 00000000..d2b59754
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2Logic.xtend
@@ -0,0 +1,22 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
4import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
5import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
6import java.util.List
7import org.eclipse.emf.ecore.EObject
8import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
9
10class InstanceModel2Logic {
11 val InstanceModel2PartialInterpretation instanceModel2PartialInterpretation = new InstanceModel2PartialInterpretation
12 val PartialInterpretation2Logic partialInterpretation2Logic = new PartialInterpretation2Logic
13
14 public def transform(
15 TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelTranslationResult,
16 List<EObject> objects)
17 {
18 val res1 = instanceModel2PartialInterpretation.transform(metamodelTranslationResult,objects,true)
19 this.partialInterpretation2Logic.transformPartialIntepretation2Logic(metamodelTranslationResult.output,res1)
20 return metamodelTranslationResult//.output
21 }
22} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
new file mode 100644
index 00000000..9a737ab9
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
@@ -0,0 +1,144 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
10import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
11import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.Problem2PartialInterpretationTrace
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory
15import java.util.HashMap
16import java.util.List
17import java.util.Map
18import org.eclipse.emf.common.util.Enumerator
19import org.eclipse.emf.ecore.EObject
20import org.eclipse.emf.ecore.resource.Resource
21
22import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
23
24class InstanceModel2PartialInterpretation {
25 val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
26 val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE
27 val Ecore2Logic ecore2Logic = new Ecore2Logic
28 val partialInterpretationInitialiser = new PartialInterpretationInitialiser
29
30 public def transform(
31 TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelTranslationResult,
32 Resource resource,
33 boolean withID)
34 {
35 val objects = resource.allContents.toList
36 return transform(metamodelTranslationResult,objects,withID)
37 }
38
39 public def transform(
40 TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelTranslationResult,
41 List<EObject> objects,
42 boolean withID)
43 {
44 val problem = metamodelTranslationResult.output
45 val ecore2LogicTrace = metamodelTranslationResult.trace
46 val tracedOutput = partialInterpretationInitialiser.initialisePartialInterpretation(problem, new TypeScopes)
47 val partialInterpretation = tracedOutput.output
48 val partialInterpretationTrace = tracedOutput.trace
49
50 val Map<EObject,DefinedElement> object2DefinedElement = new HashMap
51
52 // EObject -> DefinedElement
53 for(objectIndex : 0..<objects.size) {
54 val object = objects.get(objectIndex)
55 val element = createDefinedElement => [
56 it.name = if(withID)
57 { '''PartialObject«objectIndex»''' } else
58 { null }
59 ]
60
61 // Add element to interpretation
62 partialInterpretation.newElements += element
63
64 // Define the types
65 val type = ecore2Logic.TypeofEClass(ecore2LogicTrace,object.eClass) as TypeDeclaration
66 val interpretation = type.lookup(partialInterpretationTrace.type2Interpretation)
67 interpretation.elements += element
68 interpretation.supertypeInterpretation.forEach[elements += element]
69
70 // Trace handling
71 object2DefinedElement.put(object, element)
72 }
73
74 val referencesUsed = ecore2Logic.allReferencesInScope(ecore2LogicTrace).toSet
75 val attributesUsed = ecore2Logic.allAttributesInScope(ecore2LogicTrace).toSet
76 for(source : objects) {
77 // Translating the references
78 for(reference : source.eClass.EAllReferences.filter[
79 referencesUsed.contains(it) && !it.derived])
80 {
81 val type = ecore2Logic.relationOfReference(ecore2LogicTrace,reference)
82 val interpretation = type.lookup(partialInterpretationTrace.relation2Interpretation)
83 val sourceElement = source.lookup(object2DefinedElement)
84 if(reference.isMany) {
85 val listOfTargets = source.eGet(reference) as List<? extends EObject>
86 for(target : listOfTargets) {
87 if(target !== null && object2DefinedElement.containsKey(target)) {
88 val targetElement = target.lookup(object2DefinedElement)
89 translateLink(interpretation,sourceElement,targetElement)
90 }
91 }
92 } else {
93 val target = source.eGet(reference) as EObject
94 if(target !== null && object2DefinedElement.containsKey(target)) {
95 val targetElement = target.lookup(object2DefinedElement)
96 translateLink(interpretation,sourceElement,targetElement)
97 }
98 }
99 }
100
101 // Transforming the attributes
102 for(attribute : source.eClass.EAllAttributes.filter[attributesUsed.contains(it) && !it.derived]) {
103 val type = ecore2Logic.relationOfAttribute(ecore2LogicTrace,attribute)
104 val interpretation = type.lookup(partialInterpretationTrace.relation2Interpretation)
105 val sourceElement = source.lookup(object2DefinedElement)
106 if(attribute.isMany) {
107 val listOfTargets = source.eGet(attribute) as List<? extends EObject>
108 for(target : listOfTargets) {
109 val value = translateValue(target,ecore2LogicTrace,partialInterpretationTrace)
110 if(value !== null) {
111 translateLink(interpretation,sourceElement,value)
112 }
113 }
114 } else {
115 val target = source.eGet(attribute)
116 if(target !== null) {
117 val value = translateValue(target,ecore2LogicTrace,partialInterpretationTrace)
118 if(value !== null) {
119 translateLink(interpretation,sourceElement,value)
120 }
121 }
122 }
123 }
124 }
125
126 return partialInterpretation
127 }
128
129 protected def translateLink(PartialRelationInterpretation interpretation, DefinedElement source, DefinedElement target) {
130 interpretation.relationlinks += createBinaryElementRelationLink => [it.param1 = source it.param2 = target]
131 }
132
133 dispatch protected def translateValue(Enumerator value, Ecore2Logic_Trace ecore2LogicTrace, Problem2PartialInterpretationTrace partialInterpretationTrace) {
134 val term = this.ecore2Logic.Literal(ecore2LogicTrace,value)
135 if(term instanceof DefinedElement) {
136 return term
137 }
138 else throw new AssertionError('''term should be a defined element?''')
139 }
140
141 dispatch protected def translateValue(Object value, Ecore2Logic_Trace ecore2LogicTrace, Problem2PartialInterpretationTrace partialInterpretationTrace) {
142 //throw new UnsupportedOperationException('''Mapping of «value.class.simpleName» in partial models is currently not supported!''')
143 }
144} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
new file mode 100644
index 00000000..3a85536b
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
@@ -0,0 +1,172 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
10import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
11import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.Partial2logicannotationsFactory
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink
17import java.util.ArrayList
18import java.util.HashMap
19import java.util.HashSet
20import java.util.Map
21import java.util.Set
22import org.eclipse.emf.ecore.util.EcoreUtil
23import org.eclipse.xtend.lib.annotations.Data
24
25import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
26
27@Data class PartialInterpretation2Logic_Trace {
28 Map<DefinedElement,DefinedElement> new2Old = new HashMap
29
30 Map<TypeDeclaration, TypeDefinition> definedPart = new HashMap
31 Map<TypeDeclaration, TypeDeclaration> undefinedPart = new HashMap
32 Set<Type> originalTypes = new HashSet
33 Set<TypeDeclaration> splittedTypes = new HashSet
34}
35
36class PartialInterpretation2Logic {
37 val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
38 val extension LogicProblemBuilder builder = new LogicProblemBuilder
39
40 def transformPartialIntepretation2Logic(LogicProblem p, PartialInterpretation i) {
41 val trace = new PartialInterpretation2Logic_Trace()
42 trace.originalTypes.addAll(p.types)
43 if(! i.newElements.empty) {
44
45 // Elements adding
46 addExistingElementToProblem(p,i,trace)
47
48 // Types
49 for(partialTypeDeclaration : i.partialtypeinterpratation) {
50 splitTypeIntoTwo(p,partialTypeDeclaration,trace)
51 }
52 connectSplittings(p,trace)
53
54 // Relations
55 for(partialRelationInterpretation : i.partialrelationinterpretation) {
56 //println(partialRelationInterpretation.interpretationOf.name)
57 relationLinksToAssertion(p,partialRelationInterpretation,trace)
58 }
59 }
60 }
61
62 private def addExistingElementToProblem(LogicProblem p, PartialInterpretation i,PartialInterpretation2Logic_Trace trace) {
63// val newElements = new ArrayList(i.newElements)
64// var newElementIndex = 1
65// for(newElement : newElements) {
66// newElement.name = '''o «newElementIndex++»'''
67// p.elements += newElement
68// }
69 p.elements += i.newElements
70 }
71
72 private def splitTypeIntoTwo(LogicProblem p, PartialTypeInterpratation partialTypeDeclaration,PartialInterpretation2Logic_Trace trace) {
73 if(!partialTypeDeclaration.elements.empty) {
74 val declaration = partialTypeDeclaration.interpretationOf
75
76 val definedPart = createTypeDefinition => [
77 it.name = '''«declaration.name» DefinedPart'''
78 it.elements += partialTypeDeclaration.elements
79 it.isAbstract = declaration.isIsAbstract
80 ]
81 val undefinedPart = createTypeDeclaration => [
82 it.name = '''«declaration.name» UndefinedPart'''
83 it.isAbstract = declaration.isIsAbstract
84 ]
85 declaration.isAbstract = true
86
87 trace.definedPart.put(declaration,definedPart)
88 trace.undefinedPart.put(declaration,undefinedPart)
89 trace.splittedTypes.add(declaration)
90 p.add(definedPart)
91 p.add(undefinedPart)
92 Supertype(definedPart,declaration)
93 Supertype(undefinedPart,declaration)
94
95 for(containment : p.containmentHierarchies) {
96 if(containment.typesOrderedInHierarchy.contains(declaration)) {
97 containment.typesOrderedInHierarchy += definedPart
98 containment.typesOrderedInHierarchy += undefinedPart
99 }
100 }
101 }
102 }
103
104 private def connectSplittings(LogicProblem p,PartialInterpretation2Logic_Trace trace) {
105 val originalTypes = p.types.filter[originalType(trace)].toList
106 for(type : originalTypes) {
107 val superTypes = new ArrayList(type.supertypes.filter[originalType(trace)].toList)
108 for(supertype : superTypes) {
109 if(type.isSplitted(trace)) {
110 if(supertype.isSplitted(trace)) {
111 Supertype((type as TypeDeclaration).lookup(trace.definedPart), (supertype as TypeDeclaration).lookup(trace.definedPart))
112 Supertype((type as TypeDeclaration).lookup(trace.undefinedPart), (supertype as TypeDeclaration).lookup(trace.undefinedPart))
113 } else {
114 // Do nothing
115 }
116 } else {
117 if(supertype.isSplitted(trace)) {
118 Supertype(type, (supertype as TypeDeclaration).lookup(trace.undefinedPart))
119 } else if(supertype instanceof TypeDefinition) {
120 // Do nothing
121 }
122 }
123 }
124 }
125 }
126
127 private def originalType(Type type,PartialInterpretation2Logic_Trace trace) {
128 return trace.originalTypes.contains(type)
129 }
130 private def isSplitted(Type t, PartialInterpretation2Logic_Trace trace) {
131 trace.splittedTypes.contains(t)
132 }
133
134 private def relationLinksToAssertion(LogicProblem p, PartialRelationInterpretation r,PartialInterpretation2Logic_Trace trace) {
135 val relation = r.interpretationOf
136 val links = r.relationlinks
137 if(links.size == 0) {
138 // No assertion for empty relations
139 return
140 } else {
141 val term = if(links.size == 1) {
142 createLink(links.head,relation)
143 } else {
144 links.map[link|createLink(link,relation)].And
145 }
146 val assertion = Assertion('''PartialInterpretation «r.interpretationOf.name»''',term)
147 val ^annotation= Partial2logicannotationsFactory.eINSTANCE.createPartialModelRelation2Assertion
148 ^annotation.target = assertion
149 ^annotation.targetRelation = relation
150 ^annotation.links += links.map[EcoreUtil.copy(it)]
151 //val error= assertion.eAllContents.toIterable.filter(SymbolicValue).filter[it.symbolicReference === null]
152 //error.forEach[println("error")]
153 p.add(assertion)
154 p.annotations+= ^annotation
155 }
156
157 }
158
159 def private createLink(RelationLink link, SymbolicDeclaration relationDeclaration) {
160 if(link instanceof BinaryElementRelationLink) {
161 if((link.param1 !== null) && (link.param2 !== null)) {
162 return createSymbolicValue=>[
163 it.symbolicReference=relationDeclaration
164 it.parameterSubstitutions += createSymbolicValue => [it.symbolicReference = link.param1]
165 it.parameterSubstitutions += createSymbolicValue => [it.symbolicReference = link.param2]
166 ]
167 } else {
168 throw new IllegalArgumentException
169 }
170 } else throw new UnsupportedOperationException
171 }
172} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-28 17:20:41 +0000