aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
committerLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
commit60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf
parentInitial commit, migrating from SVN (diff)
downloadVIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
Migrating Additional projects
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend112
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/Descriptor.xtend214
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/FurtherNodeDescriptorWithEquivalenceCounter.xtend16
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/NeighbourhoodWithTraces.xtend11
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2Hash.xtend25
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2ImmutableTypeLattice.xtend24
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2ImmutableTypeLatticeWithEquivalenceCounter.xtend56
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2NeighbourhoodRepresentation.xtend345
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/IdentifierBasedStateCoderFactory.xtend129
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend206
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend136
11 files changed, 1274 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
new file mode 100644
index 00000000..eeccbf76
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
@@ -0,0 +1,112 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
11import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
12import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialConstantInterpretation
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialFunctionInterpretation
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory
19import java.util.HashMap
20import java.util.Map
21import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
22import org.eclipse.viatra.query.runtime.emf.EMFScope
23import org.eclipse.xtend.lib.annotations.Data
24
25import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
26
27@Data class Problem2PartialInterpretationTrace {
28 Map<TypeDeclaration, PartialTypeInterpratation> type2Interpretation = new HashMap
29 Map<RelationDeclaration, PartialRelationInterpretation> relation2Interpretation = new HashMap
30}
31
32class PartialInterpretationInitialiser {
33 val extension PartialinterpretationFactory factory = PartialinterpretationFactory.eINSTANCE
34 val extension LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE
35
36 /**
37 * Initialises an empty partial interpretation from a logic problem
38 */
39 def TracedOutput<PartialInterpretation,Problem2PartialInterpretationTrace> initialisePartialInterpretation(
40 LogicProblem problem,
41 int minNewElement, int maxNewElement)
42 {
43 val engine = ViatraQueryEngine.on(new EMFScope(problem))
44 val trace = new Problem2PartialInterpretationTrace
45
46 val res = createPartialInterpretation => [
47 it.problem = problem
48 it.openWorldElementPrototype = createDefinedElement => [it.name = "Symbolic New Element"]
49 it.minNewElements = minNewElement
50 it.maxNewElements = maxNewElement
51
52 for(typeDeclaration : problem.types.filter(TypeDeclaration)) {
53 it.partialtypeinterpratation += typeDeclaration.initialisePartialTypeInterpretation(engine,trace)
54 }
55 problem.connectSuperypes(trace)
56
57 it.partialrelationinterpretation += problem.relations.filter(RelationDeclaration)
58 .map[initialisePartialRelationInterpretation(trace)]
59 it.partialfunctioninterpretation += problem.functions.filter(FunctionDeclaration)
60 .map[initialisePartialFunctionInterpretation(trace)]
61 it.partialconstantinterpretation += problem.constants.filter(ConstantDeclaration)
62 .map[initialisePartialConstantDeclaration(trace)]
63 ]
64
65 return new TracedOutput(res,trace)
66 }
67
68 /**
69 * Initialize type with existing elements
70 */
71 def private initialisePartialTypeInterpretation(TypeDeclaration t, ViatraQueryEngine engine, Problem2PartialInterpretationTrace trace) {
72 val supertypeMatcher = SupertypeStarMatcher.on(engine)
73 val res = createPartialTypeInterpratation => [
74 it.interpretationOf = t
75 it.elements += supertypeMatcher.getAllValuesOfsubtype(t)
76 .filter(TypeDefinition)
77 .map[elements].flatten
78 ]
79 trace.type2Interpretation.put(t,res)
80 return res
81 }
82
83 def private connectSuperypes(LogicProblem problem, Problem2PartialInterpretationTrace trace) {
84 for(typeDeclaration : problem.types.filter(TypeDeclaration)) {
85 val supertypes = typeDeclaration.<Type>transitiveClosurePlus[it.supertypes]
86 for(supertype : supertypes.filter(TypeDeclaration)) {
87 typeDeclaration.lookup(trace.type2Interpretation).supertypeInterpretation += supertype.lookup(trace.type2Interpretation)
88 //println('''«typeDeclaration.name» --> «supertype.name»''')
89 }
90 }
91 }
92
93 def private initialisePartialRelationInterpretation(RelationDeclaration r, Problem2PartialInterpretationTrace trace) {
94 val res = createPartialRelationInterpretation => [
95 it.interpretationOf = r
96 if(r.parameters.size==2) {
97 it.param1 = r.parameters.get(0)
98 it.param2 = r.parameters.get(1)
99 } else throw new UnsupportedOperationException
100 ]
101 trace.relation2Interpretation.put(r,res)
102 return res
103 }
104
105 def private PartialConstantInterpretation initialisePartialConstantDeclaration(ConstantDeclaration c, Problem2PartialInterpretationTrace trace) {
106 throw new UnsupportedOperationException
107 }
108
109 def private PartialFunctionInterpretation initialisePartialFunctionInterpretation(FunctionDeclaration f, Problem2PartialInterpretationTrace trace) {
110 throw new UnsupportedOperationException
111 }
112} \ 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/partialinterpretationlanguage/neighbourhood/Descriptor.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/Descriptor.xtend
new file mode 100644
index 00000000..41482b28
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/Descriptor.xtend
@@ -0,0 +1,214 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood
2
3import java.util.HashMap
4import java.util.Map
5import java.util.Set
6import org.eclipse.xtend.lib.annotations.Data
7
8@Data abstract class AbstractNodeDescriptor {
9 long dataHash
10
11// @Pure
12// @Override
13// override public boolean equals(Object obj) {
14// if (this === obj)
15// return true;
16// if (obj === null)
17// return false;
18// if (getClass() != obj.getClass())
19// return false;
20// val AbstractNodeDescriptor other = obj as AbstractNodeDescriptor;
21// if (other.dataHash != this.dataHash)
22// return false;
23// return true;
24// }
25}
26
27@Data class LocalNodeDescriptor extends AbstractNodeDescriptor{
28 Set<String> types
29 String id;
30 new(String id, Set<String> types) {
31 super(calcualteDataHash(id,types))
32 this.types = types
33 this.id = id
34 }
35
36 def private static calcualteDataHash(String id, Set<String> types) {
37 val int prime = 31;
38 var result = 0
39 if(id !== null)
40 result = id.hashCode();
41 if(types !== null) {
42 result = prime * result + types.hashCode
43 }
44 return result
45 }
46
47 override hashCode() {
48 return this.dataHash.hashCode
49 }
50
51 override toString() {
52 return class.name + this.dataHash
53 }
54
55// @Pure
56// @Override
57// override public boolean equals(Object obj) {
58// if (this === obj)
59// return true;
60// if (obj === null)
61// return false;
62// if (getClass() != obj.getClass())
63// return false;
64// val AbstractNodeDescriptor other = obj as AbstractNodeDescriptor;
65// if (other.dataHash != this.dataHash)
66// return false;
67// return true;
68// }
69
70// @Pure
71// override public boolean equals(Object obj) {
72// if (this === obj)
73// return true;
74// if (obj === null)
75// return false;
76// if (getClass() != obj.getClass())
77// return false;
78// if (!super.equals(obj))
79// return false;
80// val LocalNodeDescriptor other = obj as LocalNodeDescriptor;
81// if (this.clazz === null) {
82// if (other.clazz != null)
83// return false;
84// } else if (!this.clazz.equals(other.clazz))
85// return false;
86// return true;
87// }
88}
89
90@Data class IncomingRelation<FROM> {
91 FROM from
92 String type
93}
94
95@Data class OutgoingRelation<TO> {
96 TO to
97 String type
98}
99
100@Data class FurtherNodeDescriptor<NodeRep> extends AbstractNodeDescriptor{
101
102 NodeRep previousRepresentation
103 Map<IncomingRelation<NodeRep>,Integer> incomingEdges
104 Map<OutgoingRelation<NodeRep>,Integer> outgoingEdges
105
106 new(
107 NodeRep previousRepresentation,
108 Map<IncomingRelation<NodeRep>,Integer> incomingEdges,
109 Map<OutgoingRelation<NodeRep>,Integer> outgoingEdges)
110 {
111 super(calculateDataHash(previousRepresentation,incomingEdges,outgoingEdges))
112 this.previousRepresentation = previousRepresentation
113 this.incomingEdges = new HashMap(incomingEdges)
114 this.outgoingEdges = new HashMap(outgoingEdges)
115 }
116
117 static def private <NodeRep> int calculateDataHash(
118 NodeRep previousRepresentation,
119 Map<IncomingRelation<NodeRep>,Integer> incomingEdges,
120 Map<OutgoingRelation<NodeRep>,Integer> outgoingEdges)
121 {
122 val int prime = 31;
123 var int result = previousRepresentation.hashCode;
124 if(incomingEdges !== null)
125 result = prime * result + incomingEdges.hashCode();
126 if(outgoingEdges !== null)
127 result = prime * result + outgoingEdges.hashCode();
128 return result;
129 }
130
131 override hashCode() {
132 return this.dataHash.hashCode
133 }
134
135 override toString() {
136 return class.name + dataHash
137// return '''[«previousRepresentation»,(«FOR
138// in: incomingEdges.entrySet»(«in.key.type.name»=«in.key.from»,«in.value»)«ENDFOR»),(«FOR
139// out: outgoingEdges.entrySet»(«out.key.type.name»=«out.key.to»,«out.value»)«ENDFOR»),«FOR
140// att: attributeValues»(«att.type.name»=«att.value»)«ENDFOR»]'''
141 }
142
143// @Pure
144// @Override
145// override public boolean equals(Object obj) {
146// if (this === obj)
147// return true;
148// if (obj === null)
149// return false;
150// if (getClass() != obj.getClass())
151// return false;
152// val AbstractNodeDescriptor other = obj as AbstractNodeDescriptor;
153// if (other.dataHash != this.dataHash)
154// return false;
155// return true;
156// }
157
158// @Pure
159// override public boolean equals(Object obj) {
160// if (this === obj)
161// return true;
162// if (obj === null)
163// return false;
164// if (getClass() != obj.getClass())
165// return false;
166// if (!super.equals(obj))
167// return false;
168// val FurtherNodeDescriptor<?> other = obj as FurtherNodeDescriptor<?>;
169// if (this.previousRepresentation === null) {
170// if (other.previousRepresentation != null)
171// return false;
172//
173// }
174//// } else if (!this.previousRepresentation.equals(other.previousRepresentation))
175//// return false;
176// if (this.incomingEdges === null) {
177// if (other.incomingEdges != null)
178// return false;
179// } else if (!this.incomingEdges.equals(other.incomingEdges))
180// return false;
181// if (this.outgoingEdges === null) {
182// if (other.outgoingEdges != null)
183// return false;
184// } else if (!this.outgoingEdges.equals(other.outgoingEdges))
185// return false;
186// if (this.attributeValues === null) {
187// if (other.attributeValues != null)
188// return false;
189// } else if (!this.attributeValues.equals(other.attributeValues))
190// return false;
191// return true;
192// }
193}
194
195/*
196@Data
197class ModelDescriptor {
198 int dataHash
199 int unknownElements
200 Map<? extends AbstractNodeDescriptor,Integer> knownElements
201
202 public new(Map<? extends AbstractNodeDescriptor,Integer> knownElements, int unknownElements) {
203 this.dataHash = calculateDataHash(knownElements,unknownElements)
204 this.unknownElements = unknownElements
205 this.knownElements = knownElements
206 }
207
208 def private static calculateDataHash(Map<? extends AbstractNodeDescriptor,Integer> knownElements, int unknownElements)
209 {
210 val int prime = 31;
211 return knownElements.hashCode * prime + unknownElements.hashCode
212 }
213}
214*/ \ 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/partialinterpretationlanguage/neighbourhood/FurtherNodeDescriptorWithEquivalenceCounter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/FurtherNodeDescriptorWithEquivalenceCounter.xtend
new file mode 100644
index 00000000..22e890a2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/FurtherNodeDescriptorWithEquivalenceCounter.xtend
@@ -0,0 +1,16 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood
2
3import java.util.Map
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
5
6class FurtherNodeDescriptorWithEquivalenceCounter extends FurtherNodeDescriptor<AbstractNodeDescriptor> {
7
8 new(AbstractNodeDescriptor previousRepresentation,
9 Map<IncomingRelation<AbstractNodeDescriptor>, Integer> incomingEdges,
10 Map<OutgoingRelation<AbstractNodeDescriptor>, Integer> outgoingEdges,
11 Map<DefinedElement, FurtherNodeDescriptor<AbstractNodeDescriptor>> node2Representation)
12 {
13 super(previousRepresentation, incomingEdges, outgoingEdges)
14 }
15
16} \ 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/partialinterpretationlanguage/neighbourhood/NeighbourhoodWithTraces.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/NeighbourhoodWithTraces.xtend
new file mode 100644
index 00000000..76cc4ae1
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/NeighbourhoodWithTraces.xtend
@@ -0,0 +1,11 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
4import java.util.Map
5import org.eclipse.xtend.lib.annotations.Data
6
7@Data class NeighbourhoodWithTraces<ModelRep,NodeRep> {
8 ModelRep modelRepresentation
9 Map<DefinedElement,? extends NodeRep> nodeRepresentations
10 NeighbourhoodWithTraces<ModelRep,NodeRep> previousRepresentation
11}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2Hash.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2Hash.xtend
new file mode 100644
index 00000000..d474877d
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2Hash.xtend
@@ -0,0 +1,25 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood
2
3import java.util.Map
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
5
6class PartialInterpretation2Hash extends PartialInterpretation2NeighbourhoodRepresentation<Integer, Integer>{
7
8 protected new() {
9 super(false, true)
10 }
11
12 override protected createLocalRepresentation(Map<DefinedElement, LocalNodeDescriptor> node2Representation, Map<LocalNodeDescriptor, Integer> representation2Amount) {
13 return new NeighbourhoodWithTraces(
14 representation2Amount.hashCode,node2Representation.mapValues[it.hashCode],
15 null)
16 }
17
18 override protected createFurtherRepresentation(Map<FurtherNodeDescriptor<Integer>, Integer> nodeDescriptors, Map<DefinedElement, FurtherNodeDescriptor<Integer>> node2Representation, NeighbourhoodWithTraces<Integer, Integer> previous, boolean deepRepresentation) {
19 return new NeighbourhoodWithTraces(
20 nodeDescriptors.hashCode,
21 node2Representation.mapValues[it.hashCode],
22 if(deepRepresentation) {previous} else {null})
23 }
24
25}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2ImmutableTypeLattice.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2ImmutableTypeLattice.xtend
new file mode 100644
index 00000000..31181370
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2ImmutableTypeLattice.xtend
@@ -0,0 +1,24 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
4import java.util.Map
5
6class PartialInterpretation2ImmutableTypeLattice extends
7 PartialInterpretation2NeighbourhoodRepresentation<Map<? extends AbstractNodeDescriptor,Integer>, AbstractNodeDescriptor>{
8
9 public new() {
10 super(false, true)
11 }
12
13 override protected createLocalRepresentation(Map<DefinedElement, LocalNodeDescriptor> node2Representation, Map<LocalNodeDescriptor, Integer> representation2Amount) {
14 return new NeighbourhoodWithTraces(node2Representation.immutableCopy,node2Representation.immutableCopy,null)
15 }
16
17 override protected createFurtherRepresentation(Map<FurtherNodeDescriptor<AbstractNodeDescriptor>, Integer> nodeDescriptors, Map<DefinedElement, FurtherNodeDescriptor<AbstractNodeDescriptor>> node2Representation, NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> previous, boolean deepRepresentation) {
18 if(deepRepresentation) {
19 return new NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor>(nodeDescriptors,node2Representation,previous)
20 } else {
21 return new NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor>(nodeDescriptors,node2Representation,null)
22 }
23 }
24}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2ImmutableTypeLatticeWithEquivalenceCounter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2ImmutableTypeLatticeWithEquivalenceCounter.xtend
new file mode 100644
index 00000000..251a82f0
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2ImmutableTypeLatticeWithEquivalenceCounter.xtend
@@ -0,0 +1,56 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
4import java.util.Map
5import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
6import java.util.HashMap
7
8class PartialInterpretation2ImmutableTypeLatticeWithEquivalenceCounter extends
9 PartialInterpretation2NeighbourhoodRepresentation<
10 Map<? extends AbstractNodeDescriptor,Integer>, // <- Model Descriptor
11 AbstractNodeDescriptor> // <- Node Descriptor
12 {
13
14 protected new() {
15 super(true,false)
16 }
17
18 override protected createLocalRepresentation(Map<DefinedElement, LocalNodeDescriptor> node2Representation, Map<LocalNodeDescriptor, Integer> representation2Amount) {
19 return new NeighbourhoodWithTraces(node2Representation.immutableCopy,node2Representation.immutableCopy,null)
20 }
21
22 override protected createFurtherRepresentation(
23 Map<FurtherNodeDescriptor<AbstractNodeDescriptor>, Integer> nodeDescriptors,
24 Map<DefinedElement, FurtherNodeDescriptor<AbstractNodeDescriptor>> node2Representation,
25 NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> previous,
26 boolean deepRepresentation
27 ) {
28 if(deepRepresentation) {
29 return new NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor>(nodeDescriptors,node2Representation,previous)
30 } else {
31 return new NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor>(nodeDescriptors,node2Representation,null)
32 }
33 }
34
35 public def finalRepresentation(NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>,AbstractNodeDescriptor> representation) {
36 val node2Representation = representation.nodeRepresentations
37 val node2LocalRepresentation = new HashMap
38 //val localRepresentation2Node = new HashMap
39 for(entry: node2Representation.entrySet) {
40 val node = entry.key
41 val localNodeDescriptor = entry.value.toLocalDescriptor
42 node2LocalRepresentation.put(node,localNodeDescriptor)
43 }
44
45 }
46
47 public def LocalNodeDescriptor toLocalDescriptor(AbstractNodeDescriptor descriptor) {
48 if(descriptor instanceof LocalNodeDescriptor) {
49 return descriptor
50 } else if(descriptor instanceof FurtherNodeDescriptor<?>) {
51 (descriptor.previousRepresentation as AbstractNodeDescriptor).toLocalDescriptor
52 } else throw new IllegalArgumentException('''Unsupported descriptor type: «descriptor.class.simpleName»''')
53 }
54
55
56}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2NeighbourhoodRepresentation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2NeighbourhoodRepresentation.xtend
new file mode 100644
index 00000000..df6fb6ae
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/neighbourhood/PartialInterpretation2NeighbourhoodRepresentation.xtend
@@ -0,0 +1,345 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
8import java.util.HashMap
9import java.util.HashSet
10import java.util.LinkedList
11import java.util.List
12import java.util.Map
13import java.util.Set
14
15import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
16
17abstract class PartialInterpretation2NeighbourhoodRepresentation<ModelRepresentation,NodeRepresentation> {
18 private val boolean deepRepresentation
19 private val boolean mergeSimilarNeighbourhood
20
21 protected new(boolean deeprepresentation, boolean mergeSimilarNeighbourhood) {
22 this.deepRepresentation = deeprepresentation
23 this.mergeSimilarNeighbourhood = mergeSimilarNeighbourhood
24 }
25
26 public static val FixPointRage = -1
27 public static val FullParallels = Integer.MAX_VALUE
28 public static val MaxNumbers = Integer.MAX_VALUE
29
30 /**
31 * Creates a neighbourhood representation with traces
32 * @param model The model to be represented.
33 * @param range The range of the neighbourhood.
34 * @param parallels The maximal number of parallel references to be differentiated.
35 */
36 def public createRepresentation(PartialInterpretation model, int range, int parallels, int maxNumber) {
37 return createRepresentation(model,range,parallels,maxNumber,null,null)
38 }
39
40 def public createRepresentation(
41 PartialInterpretation model,
42 int range, int parallels, int maxNumber,
43 Set<TypeDeclaration> relevantTypes, Set<RelationDeclaration> relevantRelations)
44 {
45 val Map<DefinedElement, Set<String>> types = new HashMap
46 fillTypes(model,types,relevantTypes)
47 val Map<DefinedElement, List<IncomingRelation<DefinedElement>>> IncomingRelations = new HashMap;
48 val Map<DefinedElement, List<OutgoingRelation<DefinedElement>>> OutgoingRelations = new HashMap;
49 fillReferences(model,IncomingRelations,OutgoingRelations,relevantRelations)
50
51 val res = doRecursiveNeighbourCalculation(model,types,IncomingRelations,OutgoingRelations,range,parallels,maxNumber);
52
53 return res;
54 }
55
56 def private isRelevant(TypeDeclaration t, Set<TypeDeclaration> relevantTypes) {
57 if(relevantTypes === null) {
58 return true
59 } else {
60 return relevantTypes.contains(t)
61 }
62 }
63 def private isRelevant(RelationDeclaration r, Set<RelationDeclaration> relevantRelations) {
64 if(relevantRelations === null) {
65 return true
66 } else {
67 return relevantRelations.contains(r)
68 }
69 }
70
71 /**
72 * Creates a neighbourhood representation with traces
73 * @param model The model to be represented.
74 * @param IncomingRelations Requires the previously indexed incoming references.
75 * @param OutgoingRelations Requires the previously indexed outgoing references.
76 * @param range The range of the neighbourhood.
77 * @param parallels The maximal number of parallel references to be differentiated.
78 */
79 def private NeighbourhoodWithTraces<ModelRepresentation,NodeRepresentation> doRecursiveNeighbourCalculation(
80 PartialInterpretation model,
81 Map<DefinedElement, Set<String>> types,
82 Map<DefinedElement, List<IncomingRelation<DefinedElement>>> IncomingRelations,
83 Map<DefinedElement, List<OutgoingRelation<DefinedElement>>> OutgoingRelations,
84 int range, int parallels, int maxNumber)
85 {
86 if(range == 0){
87 val r = calculateLocalNodeDescriptors(model,types,maxNumber)
88 val res = this.createLocalRepresentation(r.value,r.key)
89 if(res.modelRepresentation === null) {
90 throw new IllegalArgumentException('''Model representation is null''')
91 } else if(res.nodeRepresentations === null || res.nodeRepresentations.empty) {
92 throw new IllegalArgumentException('''No node representation''')
93 } else if(res.previousRepresentation !== null) {
94 throw new IllegalArgumentException('''The previous representation of the first neighbourhood have to be null''')
95 } else return res
96 } else if(range > 0) {
97 val previous = doRecursiveNeighbourCalculation(model,types,IncomingRelations,OutgoingRelations,range-1,parallels,maxNumber)
98 val r = calculateFurtherNodeDescriptors(model,previous,IncomingRelations,OutgoingRelations,parallels,maxNumber)
99 //println('''Level «range» finished.''')
100 val res = createFurtherRepresentation(r.key,r.value,previous,deepRepresentation)
101 if(res.modelRepresentation === null) {
102 throw new IllegalArgumentException('''Model representation is null''')
103 } else if(res.nodeRepresentations === null || res.nodeRepresentations.empty) {
104 throw new IllegalArgumentException('''No node representation''')
105 } else if(res.previousRepresentation === null && deepRepresentation) {
106 throw new IllegalArgumentException('''Need previous representations''')
107 } else return res
108 } else if (range == FixPointRage) {
109 return refineUntilFixpoint(model,types,IncomingRelations,OutgoingRelations,parallels,maxNumber)
110 }
111 }
112
113 def private refineUntilFixpoint(
114 PartialInterpretation model,
115 Map<DefinedElement, Set<String>> types,
116 Map<DefinedElement, List<IncomingRelation<DefinedElement>>> IncomingRelations,
117 Map<DefinedElement, List<OutgoingRelation<DefinedElement>>> OutgoingRelations,
118 int parallels, int maxNumbers)
119 {
120 var lastRange = 0
121 val last = calculateLocalNodeDescriptors(model,types,maxNumbers)
122 var lastRepresentation = this.createLocalRepresentation(last.value,last.key)
123 //println('''Level 0 finished.''')
124 var boolean hasRefined
125 do {
126 val nextRange = lastRange+1
127 val next = calculateFurtherNodeDescriptors(model,lastRepresentation,IncomingRelations,OutgoingRelations,parallels,maxNumbers)
128 val nextRepresentation = createFurtherRepresentation(next.key,next.value,lastRepresentation,deepRepresentation)
129
130 val previousNumberOfTypes =lastRepresentation.nodeRepresentations.values.toSet.size
131 val nextNumberOfTypes = nextRepresentation.nodeRepresentations.values.toSet.size
132 hasRefined = nextNumberOfTypes > previousNumberOfTypes
133
134 lastRange = nextRange
135 lastRepresentation = nextRepresentation
136
137// if(hasRefined) {
138// println('''Level «nextRange» is calculated, number of types is refined: «previousNumberOfTypes» -> «nextNumberOfTypes»''')
139// } else {
140// println('''Level «nextRange» is calculated, but the number of types is not refined: «previousNumberOfTypes» = «nextNumberOfTypes»''')
141// }
142 } while (hasRefined)
143 return lastRepresentation
144 }
145
146 def private getElements(PartialInterpretation model) {
147 return model.problem.elements + model.newElements
148 }
149
150 def private fillTypes(PartialInterpretation model, Map<DefinedElement, Set<String>> node2Type, Set<TypeDeclaration> relevantTypes) {
151 for(element : model.elements) {
152 node2Type.put(element, new HashSet)
153 }
154
155// for(typeDefinition : model.problem.types.filter(TypeDefinition)) {
156// // Dont need
157// }
158 for(typeInterpretation : model.partialtypeinterpratation) {
159 val type = typeInterpretation.interpretationOf
160 if(type.isRelevant(relevantTypes)) {
161 for(element : typeInterpretation.elements) {
162 element.lookup(node2Type).add(type.name)
163 }
164 }
165 }
166 }
167
168 /**
169 * Indexes the references
170 */
171 def private fillReferences(PartialInterpretation model,
172 Map<DefinedElement, List<IncomingRelation<DefinedElement>>> IncomingRelations,
173 Map<DefinedElement, List<OutgoingRelation<DefinedElement>>> OutgoingRelations,
174 Set<RelationDeclaration> relevantRelations)
175 {
176 for(object : model.elements) {
177 IncomingRelations.put(object,new LinkedList)
178 OutgoingRelations.put(object,new LinkedList)
179 }
180 for(relationInterpretation : model.partialrelationinterpretation) {
181 val type = relationInterpretation.interpretationOf
182 if(type.isRelevant(relevantRelations)) {
183 for(link : relationInterpretation.relationlinks) {
184 if(link instanceof BinaryElementRelationLink) {
185 OutgoingRelations.get(link.param1) += new OutgoingRelation(link.param2,type.name)
186 IncomingRelations.get(link.param2) += new IncomingRelation(link.param1,type.name)
187 } else throw new UnsupportedOperationException
188 }
189 }
190 }
191 }
192
193 /**
194 * Creates a local representation of the objects (aka zero range neighbourhood)
195 */
196 def abstract protected NeighbourhoodWithTraces<ModelRepresentation,NodeRepresentation> createLocalRepresentation(
197 Map<DefinedElement, LocalNodeDescriptor> node2Representation,
198 Map<LocalNodeDescriptor, Integer> representation2Amount
199 )
200
201 /**
202 * Creates a
203 */
204 def abstract protected NeighbourhoodWithTraces<ModelRepresentation,NodeRepresentation> createFurtherRepresentation(
205 Map<FurtherNodeDescriptor<NodeRepresentation>, Integer> nodeDescriptors,
206 Map<DefinedElement, FurtherNodeDescriptor<NodeRepresentation>> node2Representation,
207 NeighbourhoodWithTraces<ModelRepresentation,NodeRepresentation> previous,
208 boolean deepRepresentation
209 )
210
211 def private addOne(int original, int max) {
212 if(original == Integer.MAX_VALUE) return Integer.MAX_VALUE
213 if(original +1 > max) return Integer.MAX_VALUE
214 else return original+1
215 }
216
217 private def calculateIncomingEdges(Map<DefinedElement, List<IncomingRelation<DefinedElement>>> IncomingRelations,
218 DefinedElement object, Map<DefinedElement, ? extends NodeRepresentation> previousNodeRepresentations, int parallel)
219 {
220 val Map<IncomingRelation<NodeRepresentation>, Integer> res = new HashMap
221 for (incomingConcreteEdge : IncomingRelations.get(object)) {
222 val IncomingRelation<NodeRepresentation> e = new IncomingRelation(
223 previousNodeRepresentations.get(incomingConcreteEdge.from), incomingConcreteEdge.type)
224 if (res.containsKey(e)) {
225 res.put(e, addOne(res.get(e),parallel))
226 } else {
227 res.put(e, 1)
228 }
229 }
230 return res
231 }
232
233 private def calcuateOutgoingEdges(Map<DefinedElement,List<OutgoingRelation<DefinedElement>>> OutgoingRelations,
234 DefinedElement object, Map<DefinedElement, ? extends NodeRepresentation> previousNodeRepresentations, int parallel)
235 {
236 val Map<OutgoingRelation<NodeRepresentation>,Integer> res= new HashMap
237 for(outgoingConcreteEdge : OutgoingRelations.get(object)) {
238 val OutgoingRelation<NodeRepresentation> e =
239 new OutgoingRelation(
240 previousNodeRepresentations.get(outgoingConcreteEdge.to),
241 outgoingConcreteEdge.type)
242 if(res.containsKey(e)) {
243 res.put(e,addOne(res.get(e),parallel))
244 } else {
245 res.put(e,1)
246 }
247 }
248 return res;
249 }
250
251 /*def private <KEY,VALUE> void addOrCreate_Set(Map<KEY,Set<VALUE>> map, KEY key, VALUE value) {
252 var Set<VALUE> s;
253 if(map.containsKey(key)) {
254 s = map.get(key);
255 } else {
256 s = new HashSet
257 map.put(key,s)
258 }
259 s.add(value)
260 }*/
261
262
263 private def calculateFurtherNodeDescriptors(
264 PartialInterpretation model,
265 NeighbourhoodWithTraces<ModelRepresentation, NodeRepresentation> previous,
266 Map<DefinedElement, List<IncomingRelation<DefinedElement>>> IncomingRelations,
267 Map<DefinedElement, List<OutgoingRelation<DefinedElement>>> OutgoingRelations,
268 int parallels, int maxNumber)
269 {
270 val previousNodeRepresentations = previous.nodeRepresentations
271 val node2Representation = new HashMap<DefinedElement,FurtherNodeDescriptor<NodeRepresentation>>
272 val Map<FurtherNodeDescriptor<NodeRepresentation>,Integer> descriptor2Number =
273 if(this.mergeSimilarNeighbourhood){ new HashMap } else { null }
274 val Map<FurtherNodeDescriptor<NodeRepresentation>,FurtherNodeDescriptor<NodeRepresentation>> uniqueDescription =
275 if(this.mergeSimilarNeighbourhood){ new HashMap } else { null }
276
277 for(object: model.elements) {
278 val incomingEdges = this.calculateIncomingEdges(IncomingRelations, object, previousNodeRepresentations,parallels)
279 val outgoingEdges = this.calcuateOutgoingEdges(OutgoingRelations,object, previousNodeRepresentations,parallels)
280
281 val previousType = previousNodeRepresentations.get(object)
282
283 if(previousType === null) {
284 println("Error in state coder")
285 }
286
287 val nodeDescriptor = new FurtherNodeDescriptor(
288 previousType,
289 incomingEdges,
290 outgoingEdges)
291
292 if(this.mergeSimilarNeighbourhood) {
293 if(descriptor2Number.containsKey(nodeDescriptor)) {
294 descriptor2Number.put(
295 nodeDescriptor,
296 addOne(descriptor2Number.get(nodeDescriptor),maxNumber)
297 )
298 node2Representation.put(object,uniqueDescription.get(nodeDescriptor))
299 } else {
300 descriptor2Number.put(nodeDescriptor,1)
301 uniqueDescription.put(nodeDescriptor,nodeDescriptor)
302 node2Representation.put(object,nodeDescriptor)
303 }
304 } else {
305 node2Representation.put(object,nodeDescriptor)
306 }
307 }
308
309 return descriptor2Number -> node2Representation
310 }
311
312 private def calculateLocalNodeDescriptors(
313 PartialInterpretation model,
314 Map<DefinedElement, Set<String>> types,
315 int maxNumber)
316 {
317 val Map<DefinedElement, LocalNodeDescriptor> node2Representation = new HashMap
318 val Map<LocalNodeDescriptor, Integer> representation2Amount =
319 if(mergeSimilarNeighbourhood){ new HashMap } else { null }
320 val Map<LocalNodeDescriptor, LocalNodeDescriptor> uniqueRepresentation =
321 if(this.mergeSimilarNeighbourhood){ new HashMap } else { null }
322
323 for(element : model.elements) {
324 var newDescriptor = new LocalNodeDescriptor(element.name,element.lookup(types))
325 if(this.mergeSimilarNeighbourhood){
326 if(uniqueRepresentation.containsKey(newDescriptor)) {
327 newDescriptor = newDescriptor.lookup(uniqueRepresentation)
328 node2Representation.put(element,newDescriptor)
329 representation2Amount.put(
330 newDescriptor,
331 addOne(newDescriptor.lookup(representation2Amount),maxNumber)
332 )
333 } else {
334 uniqueRepresentation.put(newDescriptor,newDescriptor)
335 node2Representation.put(element,newDescriptor)
336 representation2Amount.put(newDescriptor, 1)
337 }
338 } else {
339 node2Representation.put(element,newDescriptor)
340 }
341 }
342
343 return representation2Amount -> node2Representation
344 }
345} \ 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/partialinterpretationlanguage/statecoder/IdentifierBasedStateCoderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/IdentifierBasedStateCoderFactory.xtend
new file mode 100644
index 00000000..c421ace6
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/IdentifierBasedStateCoderFactory.xtend
@@ -0,0 +1,129 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
4import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
9import java.util.ArrayList
10import java.util.Comparator
11import java.util.LinkedList
12import java.util.List
13import java.util.SortedSet
14import java.util.TreeSet
15import org.eclipse.emf.common.notify.Notifier
16import org.eclipse.viatra.dse.statecode.IStateCoder
17import org.eclipse.viatra.dse.statecode.IStateCoderFactory
18import org.eclipse.viatra.query.runtime.api.IPatternMatch
19import org.eclipse.xtend.lib.annotations.Accessors
20import org.eclipse.xtend.lib.annotations.Data
21
22class IdentifierBasedStateCoderFactory implements IStateCoderFactory{
23
24 val List<IdentifierBasedStateCoder> statecoders = new LinkedList
25 synchronized override createStateCoder() {
26 val res = new IdentifierBasedStateCoder
27 statecoders += res
28 return res
29 }
30 def getSumStatecoderRuntime() {
31 statecoders.map[statecoderRuntime].reduce[p1, p2|p1+p2]
32 }
33}
34
35@Data
36class RelationStatecoder {
37 String relationName
38 SortedSet<Pair<Integer,Integer>> links;
39
40 static val comparator= new Comparator<Pair<Integer,Integer>>() {
41 override compare(Pair<Integer, Integer> o1, Pair<Integer, Integer> o2) {
42 if(o1.key > o2.key) {
43 return 1
44 } else if(o1.key < o2.key) {
45 return -1
46 } else {
47 return Integer.compare(o1.value,o2.value)
48 }
49 }
50 }
51
52 new(String relationName) {
53 this.relationName = relationName
54 links = new TreeSet(comparator)
55 }
56}
57
58@Data
59class IdentifierBasedStateCode {
60 int numberOfNewElement
61 SortedSet<RelationStatecoder> relationStatecoders
62
63 private static val comparator = new Comparator<RelationStatecoder>() {
64 override compare(RelationStatecoder o1, RelationStatecoder o2) {
65 o1.relationName.compareTo(o2.relationName)
66 }
67 }
68
69 public new(int numberOfNewElements) {
70 this.numberOfNewElement = numberOfNewElements
71 this.relationStatecoders = new TreeSet(comparator)
72 }
73}
74
75class IdentifierBasedStateCoder implements IStateCoder{
76 var PartialInterpretation model = null
77
78 @Accessors(PUBLIC_GETTER) var long statecoderRuntime = 0
79
80 override createActivationCode(IPatternMatch match) {
81 val startTime = System.nanoTime
82 val res = new ArrayList(match.parameterNames.size)
83 var index = 0
84 while(index < match.parameterNames.size) {
85 res.add(getID(match.get(index)))
86 index++
87 }
88 statecoderRuntime += (System.nanoTime - startTime)
89 return match.specification.fullyQualifiedName -> res
90 }
91
92 override createStateCode() {
93 val startTime = System.nanoTime
94 val res = new IdentifierBasedStateCode(model.newElements.size)
95 for(relation : model.partialrelationinterpretation) {
96 val relationCoder = new RelationStatecoder(relation.interpretationOf.name)
97 for(link: relation.relationlinks.filter(BinaryElementRelationLink)) {
98 relationCoder.links+=link.param1.ID -> link.param2.ID
99 }
100 res.relationStatecoders+=relationCoder
101 }
102 statecoderRuntime += (System.nanoTime - startTime)
103 return res
104 }
105
106 def getID(Object element) {
107 if(element instanceof DefinedElement) {
108 val container = element.eContainer
109 if(container instanceof LogicProblem) {
110 return -container.elements.indexOf(element)-1
111 } else if(container instanceof PartialInterpretation){
112 return container.newElements.indexOf(element)+1
113 }
114 } else if(element instanceof PartialInterpretation || element instanceof LogicProblem) {
115 return 0
116 } else if(element instanceof PartialRelationInterpretation) {
117 return element.interpretationOf.name.hashCode
118 } else if(element instanceof PartialTypeInterpratation) {
119 return element.interpretationOf.name.hashCode
120 } else {
121 println(element)
122 throw new UnsupportedOperationException('''Unsupported type: «element.class.simpleName»''')
123 }
124 }
125
126 override init(Notifier notifier) {
127 model = notifier as PartialInterpretation
128 }
129} \ 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/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
new file mode 100644
index 00000000..5fb85b0c
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
@@ -0,0 +1,206 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
7import java.util.ArrayList
8import java.util.LinkedList
9import java.util.List
10import java.util.Map
11import org.eclipse.emf.common.notify.Notifier
12import org.eclipse.emf.ecore.EClass
13import org.eclipse.emf.ecore.EObject
14import org.eclipse.emf.ecore.EStructuralFeature
15import org.eclipse.viatra.dse.statecode.IStateCoder
16import org.eclipse.viatra.dse.statecode.IStateCoderFactory
17import org.eclipse.viatra.query.runtime.api.IPatternMatch
18import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
19import org.eclipse.viatra.query.runtime.base.api.FeatureListener
20import org.eclipse.viatra.query.runtime.base.api.IndexingLevel
21import org.eclipse.viatra.query.runtime.base.api.InstanceListener
22import org.eclipse.viatra.query.runtime.emf.EMFBaseIndexWrapper
23import org.eclipse.viatra.query.runtime.emf.EMFScope
24import org.eclipse.xtend.lib.annotations.Accessors
25import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
26import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
27import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
28import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
29import java.util.Set
30import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
31import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
32import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2NeighbourhoodRepresentation
33
34class NeighbourhoodBasedStateCoderFactory implements IStateCoderFactory {
35 val List<NeighbourhoodBasedPartialInterpretationStateCoder> statecoders = new LinkedList
36
37 val int range
38 val int parallels
39 val int maxNumber
40 val Set<TypeDeclaration> relevantTypes
41 val Set<RelationDeclaration> relevantRelations
42
43 public new() {
44 this.range = PartialInterpretation2NeighbourhoodRepresentation::FixPointRage
45 this.parallels = PartialInterpretation2NeighbourhoodRepresentation::FullParallels
46 this.maxNumber = PartialInterpretation2NeighbourhoodRepresentation::MaxNumbers
47 this.relevantTypes = null
48 this.relevantRelations = null
49 }
50
51 public new(int range, int parallels, int maxNumber, Set<TypeDeclaration> relevantTypes, Set<RelationDeclaration> relevantRelations) {
52 this.range = range
53 this.parallels = parallels
54 this.maxNumber = maxNumber
55 this.relevantTypes = relevantTypes
56 this.relevantRelations = relevantRelations
57 }
58
59 synchronized override createStateCoder() {
60 val res = new NeighbourhoodBasedPartialInterpretationStateCoder(statecoders.size,
61 range,parallels,maxNumber,relevantTypes,relevantRelations)
62 statecoders += res
63 return res
64 }
65 def getSumStatecoderRuntime() {
66 statecoders.map[statecoderRuntime].reduce[p1, p2|p1+p2]
67 }
68}
69
70class NeighbourhoodBasedPartialInterpretationStateCoder implements IStateCoder{
71 val int id;
72 val int range
73 val int parallels
74 val int maxNumber
75 val Set<TypeDeclaration> relevantTypes
76 val Set<RelationDeclaration> relevantRelations
77
78 val calculator =
79 new PartialInterpretation2ImmutableTypeLattice
80 var PartialInterpretation target
81
82 private var Map<DefinedElement, ? extends AbstractNodeDescriptor> nodeRepresentations = null
83 private var Map<? extends AbstractNodeDescriptor, Integer> modelRepresentation = null
84
85 /*public new(int id) {
86 this.id = id
87 this.range = PartialInterpretation2NeighbourhoodRepresentation::FixPointRage
88 this.parallels = PartialInterpretation2NeighbourhoodRepresentation::FullParallels
89 this.maxNumber = maxNumber = PartialInterpretation2NeighbourhoodRepresentation::MaxNumbers
90 this.relevantTypes = relevantTypes
91 this.relevantRelations = relevantRelations
92 }*/
93
94 public new(int id, int range, int parallels, int maxNumber, Set<TypeDeclaration> relevantTypes, Set<RelationDeclaration> relevantRelations) {
95 this.id = id
96 this.range = range
97 this.parallels = parallels
98 this.maxNumber = maxNumber
99 this.relevantTypes = relevantTypes
100 this.relevantRelations = relevantRelations
101 }
102
103 @Accessors(PUBLIC_GETTER) var long statecoderRuntime = 0
104
105// val range = -1
106// val par = Integer.MAX_VALUE
107 //val deeprepresentation = false
108
109 /////////
110 // Caching version
111 /////////
112 synchronized private def refreshStateCodes() {
113 if(this.nodeRepresentations === null || this.modelRepresentation === null) {
114 val startTime = System.nanoTime
115 //relevantObjects.forEach[println(it)]
116 val code = calculator.createRepresentation(target,range,parallels,maxNumber,relevantTypes,relevantRelations)
117 this.modelRepresentation = code.modelRepresentation
118 this.nodeRepresentations = code.nodeRepresentations
119 statecoderRuntime += (System.nanoTime - startTime)
120 }
121 }
122 synchronized override createActivationCode(IPatternMatch match) {
123 refreshStateCodes
124
125 val startTime = System.nanoTime
126 val size = match.specification.parameters.size
127 val res = new ArrayList(size)
128 var int index = 0
129 while(index < size) {
130 res.add(getCode(match.get(index)))
131 index++
132 }
133 statecoderRuntime += (System.nanoTime - startTime)
134 return match.specification.fullyQualifiedName->res.hashCode
135 }
136
137 def private getCode(Object o) {
138 if(o instanceof DefinedElement) {
139 this.nodeRepresentations.get(o)
140 } else if(o instanceof PartialInterpretation || o instanceof LogicProblem) {
141 return null
142 } else if(o instanceof PartialRelationInterpretation) {
143 return o.interpretationOf.name
144 } else if(o instanceof PartialTypeInterpratation) {
145 return o.interpretationOf.name
146 } else {
147 throw new UnsupportedOperationException('''Unsupported type: «o.class.simpleName»''')
148 }
149 }
150
151 synchronized override createStateCode() {
152 refreshStateCodes
153 return this.modelRepresentation.hashCode
154 }
155 /////////
156 // Caching version
157 /////////
158
159 /////////
160 // Recalculating version
161 /////////
162// synchronized override createActivationCode(IPatternMatch match) {
163// val nodes = calculator.createRepresentation(getRelevantObjects().toList,range,par).nodeRepresentations
164// val res = match.toArray.map[objectInMatch |
165// nodes.get(objectInMatch)
166// ]
167// return res
168// }
169//
170// override createStateCode() {
171// return this.calculator.createRepresentation(getRelevantObjects().toList,range,par).modelRepresentation
172// }
173 /////////
174 // Recalculating version
175 /////////
176
177 override init(Notifier notifier) {
178 this.target = notifier as PartialInterpretation
179 val queryEngine = ViatraQueryEngine.on(new EMFScope(notifier))
180 val baseIndex = queryEngine.getBaseIndex() as EMFBaseIndexWrapper
181 val navigationHelper = baseIndex.getNavigationHelper();
182
183 val classes = PartialinterpretationPackage.eINSTANCE.EClassifiers.filter(EClass).toSet
184 val features = classes.map[it.EAllStructuralFeatures].flatten.toSet
185 navigationHelper.registerObservedTypes(
186 classes,
187 null,
188 features,
189 IndexingLevel.FULL);
190
191
192 navigationHelper.addFeatureListener(features, new FeatureListener() {
193 override public void featureInserted(EObject host, EStructuralFeature feature, Object value) { invalidate }
194 override public void featureDeleted(EObject host, EStructuralFeature feature, Object value) { invalidate }
195 });
196 navigationHelper.addInstanceListener(classes, new InstanceListener() {
197 override public void instanceInserted(EClass clazz, EObject instance) { invalidate }
198 override public void instanceDeleted(EClass clazz, EObject instance) { invalidate }
199 });
200 }
201
202 synchronized def public invalidate() {
203 this.nodeRepresentations = null
204 this.modelRepresentation = null
205 }
206}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend
new file mode 100644
index 00000000..819cae00
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/visualisation/PartialInterpretation2Gml.xtend
@@ -0,0 +1,136 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
5import java.util.Map
6import java.util.HashMap
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
12import java.util.Set
13
14class PartialInterpretation2Gml {
15 def public transform(PartialInterpretation i) {
16 val p = i.problem
17 val Map<DefinedElement, Integer> objectToID = new HashMap
18 val containmentRelations = p.containmentHierarchies.map[it.containmentRelations].flatten.toSet
19 '''
20 graph
21 [
22 «FOR object:p.elements + i.newElements SEPARATOR '\n'»
23 «this.transformObject(object,object.typesOfElement(i),objectToID)»
24 «ENDFOR»
25 «FOR relation:i.partialrelationinterpretation»
26 «FOR link:relation.relationlinks.filter(BinaryElementRelationLink)»
27 «transformLink(relation,link,objectToID,containmentRelations)»
28 «ENDFOR»
29 «ENDFOR»
30 ]
31 '''.toString
32 }
33 def typesOfElement(DefinedElement e, PartialInterpretation i) {
34 i.problem.types.filter(TypeDefinition).filter[it.elements.contains(e)] +
35 i.partialtypeinterpratation.filter[it.elements.contains(e)].map[it.interpretationOf]
36 }
37
38 val protected titleSize = 16
39 val protected attributeSize = 14
40 val protected borderDistance = 6
41 val protected attributeBorderDistance = 8
42 val protected ratio = 11.0/20.0
43
44 def protected transformObject(DefinedElement object,Iterable<Type> types,Map<DefinedElement, Integer> objectToID){
45 val title = object.transormTitle
46 val attributes = types.map[it.name]
47
48 var double width = title.length*titleSize + borderDistance*2;
49 for(x:attributes.map[length*attributeSize + borderDistance*2 + attributeBorderDistance*2])
50 width = Math::max(width,x)
51 width = width*ratio
52
53 val height = Math::max(
54 titleSize+4,
55 (attributes.size+1)*attributeSize + borderDistance*2)
56
57 val id = objectToID.size
58 objectToID.put(object,id)
59
60 '''
61 node
62 [
63 id «id»
64 graphics
65 [
66 w «width»
67 h «height»
68 type "rectangle"
69 fill "#FFFFFF"
70 fill2 "#FFFFFF"
71 outline "#000000"
72 ]
73 LabelGraphics
74 [
75 text "«title»"
76 outline "#000000"
77 fill "#FFFFFF"
78 fontSize «titleSize»
79 fontName "Monospace"
80 autoSizePolicy "node_width"
81 anchor "t"
82 borderDistance 0.0
83 ]
84 LabelGraphics
85 [
86 text "
87 «FOR attribute : attributes»
88 «attribute»
89 «ENDFOR»"
90 fontSize «attributeSize»
91 fontName "Consolas"
92 alignment "left"
93 anchor "tl"
94 borderDistance «borderDistance»
95 ]
96 ]
97 '''
98 }
99
100 def protected transormTitle(DefinedElement object) {
101 if(object.name!= null)object.name
102 else "null"
103 }
104
105 def protected transformLink(
106 PartialRelationInterpretation reference,
107 BinaryElementRelationLink link,
108 Map<DefinedElement, Integer> objectToID,
109 Set<Relation> containmentRelations)
110 {
111 '''
112 edge
113 [
114 source «objectToID.get(link.param1)»
115 target «objectToID.get(link.param2)»
116 graphics
117 [
118 fill "#000000"
119 «IF containmentRelations.contains(reference.interpretationOf)»
120 width 3
121 «ENDIF»
122 targetArrow "standard"
123 ]
124 LabelGraphics
125 [
126 text "«reference.interpretationOf.name»"
127 fontSize 14
128 fontName "Consolas"
129 configuration "AutoFlippingLabel"
130 model "six_pos"
131 position "thead"
132 ]
133 ]
134 '''
135 }
136} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 12:46:01 +0000