aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend164
1 files changed, 0 insertions, 164 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
deleted file mode 100644
index 09a7fa60..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
+++ /dev/null
@@ -1,164 +0,0 @@
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.LogiclanguageFactory
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
11import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink
15import java.util.ArrayList
16import java.util.HashMap
17import java.util.HashSet
18import java.util.Map
19import java.util.Set
20import org.eclipse.xtend.lib.annotations.Data
21
22import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
23import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
24import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
25
26@Data class PartialInterpretation2Logic_Trace {
27 Map<DefinedElement,DefinedElement> new2Old = new HashMap
28
29 Map<TypeDeclaration, TypeDefinition> definedPart = new HashMap
30 Map<TypeDeclaration, TypeDeclaration> undefinedPart = new HashMap
31 Set<Type> originalTypes = new HashSet
32 Set<TypeDeclaration> splittedTypes = new HashSet
33}
34
35class PartialInterpretation2Logic {
36 val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
37 val extension LogicProblemBuilder builder = new LogicProblemBuilder
38
39 def transformPartialIntepretation2Logic(LogicProblem p, PartialInterpretation i) {
40 val trace = new PartialInterpretation2Logic_Trace()
41 trace.originalTypes.addAll(p.types)
42 if(! i.newElements.empty) {
43
44 // Elements adding
45 addExistingElementToProblem(p,i,trace)
46
47 // Types
48 for(partialTypeDeclaration : i.partialtypeinterpratation) {
49 splitTypeIntoTwo(p,partialTypeDeclaration,trace)
50 }
51 connectSplittings(p,trace)
52
53 // Relations
54 for(partialRelationInterpretation : i.partialrelationinterpretation) {
55 //println(partialRelationInterpretation.interpretationOf.name)
56 relationLinksToAssertion(p,partialRelationInterpretation,trace)
57 }
58 }
59 }
60
61 private def addExistingElementToProblem(LogicProblem p, PartialInterpretation i,PartialInterpretation2Logic_Trace trace) {
62 val newElements = new ArrayList(i.newElements)
63 var newElementIndex = 1
64 for(newElement : newElements) {
65 newElement.name = '''o «newElementIndex++»'''
66 p.elements += newElement
67 }
68 }
69
70 private def splitTypeIntoTwo(LogicProblem p, PartialTypeInterpratation partialTypeDeclaration,PartialInterpretation2Logic_Trace trace) {
71 if(!partialTypeDeclaration.elements.empty) {
72 val declaration = partialTypeDeclaration.interpretationOf
73
74 val definedPart = createTypeDefinition => [
75 it.name = '''«declaration.name» DefinedPart'''
76 it.elements += partialTypeDeclaration.elements
77 it.isAbstract = declaration.isIsAbstract
78 ]
79 val undefinedPart = createTypeDeclaration => [
80 it.name = '''«declaration.name» UndefinedPart'''
81 it.isAbstract = declaration.isIsAbstract
82 ]
83 declaration.isAbstract = true
84
85 trace.definedPart.put(declaration,definedPart)
86 trace.undefinedPart.put(declaration,undefinedPart)
87 trace.splittedTypes.add(declaration)
88 p.add(definedPart)
89 p.add(undefinedPart)
90 Supertype(definedPart,declaration)
91 Supertype(undefinedPart,declaration)
92
93 for(containment : p.containmentHierarchies) {
94 if(containment.typesOrderedInHierarchy.contains(declaration)) {
95 containment.typesOrderedInHierarchy += definedPart
96 containment.typesOrderedInHierarchy += undefinedPart
97 }
98 }
99 }
100 }
101
102 private def connectSplittings(LogicProblem p,PartialInterpretation2Logic_Trace trace) {
103 val originalTypes = p.types.filter[originalType(trace)].toList
104 for(type : originalTypes) {
105 val superTypes = new ArrayList(type.supertypes.filter[originalType(trace)].toList)
106 for(supertype : superTypes) {
107 if(type.isSplitted(trace)) {
108 if(supertype.isSplitted(trace)) {
109 Supertype((type as TypeDeclaration).lookup(trace.definedPart), (supertype as TypeDeclaration).lookup(trace.definedPart))
110 Supertype((type as TypeDeclaration).lookup(trace.undefinedPart), (supertype as TypeDeclaration).lookup(trace.undefinedPart))
111 } else {
112 // Do nothing
113 }
114 } else {
115 if(supertype.isSplitted(trace)) {
116 Supertype(type, (supertype as TypeDeclaration).lookup(trace.undefinedPart))
117 } else if(supertype instanceof TypeDefinition) {
118 // Do nothing
119 }
120 }
121 }
122 }
123 }
124
125 private def originalType(Type type,PartialInterpretation2Logic_Trace trace) {
126 return trace.originalTypes.contains(type)
127 }
128 private def isSplitted(Type t, PartialInterpretation2Logic_Trace trace) {
129 trace.splittedTypes.contains(t)
130 }
131
132 private def relationLinksToAssertion(LogicProblem p, PartialRelationInterpretation r,PartialInterpretation2Logic_Trace trace) {
133 val relation = r.interpretationOf
134 val links = r.relationlinks
135 if(links.size == 0) {
136 return
137 } else {
138 val term = if(links.size == 1) {
139 createLink(links.head,relation)
140 } else {
141 links.map[link|createLink(link,relation)].And
142 }
143 val assertion = Assertion('''PartialInterpretation «r.interpretationOf.name»''',term)
144 //val error= assertion.eAllContents.toIterable.filter(SymbolicValue).filter[it.symbolicReference === null]
145 //error.forEach[println("error")]
146 p.add(assertion)
147 }
148
149 }
150
151 def private createLink(RelationLink link, SymbolicDeclaration relationDeclaration) {
152 if(link instanceof BinaryElementRelationLink) {
153 if((link.param1 !== null) && (link.param2 !== null)) {
154 return createSymbolicValue=>[
155 it.symbolicReference=relationDeclaration
156 it.parameterSubstitutions += createSymbolicValue => [it.symbolicReference = link.param1]
157 it.parameterSubstitutions += createSymbolicValue => [it.symbolicReference = link.param2]
158 ]
159 } else {
160 throw new IllegalArgumentException
161 }
162 } else throw new UnsupportedOperationException
163 }
164} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-24 06:08:37 +0000