diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver')
2 files changed, 94 insertions, 29 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index e00c864a..438767cd 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | |||
@@ -10,6 +10,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | |||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | 14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory |
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory |
@@ -21,22 +22,13 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplici | |||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedWFObjective | 22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedWFObjective |
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter | 23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter |
23 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 24 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
25 | import java.util.List | ||
26 | import java.util.Map | ||
27 | import org.eclipse.emf.ecore.EObject | ||
24 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer | 28 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer |
25 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel | 29 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel |
26 | import org.eclipse.viatra.dse.solutionstore.SolutionStore | 30 | import org.eclipse.viatra.dse.solutionstore.SolutionStore |
27 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory | 31 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory |
28 | import java.util.List | ||
29 | import java.util.Map | ||
30 | import org.eclipse.viatra.dse.base.ThreadContext | ||
31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
32 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
33 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
34 | import java.util.Collection | ||
35 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
36 | import java.util.SortedMap | ||
37 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
38 | import org.eclipse.emf.ecore.EObject | ||
39 | import org.eclipse.emf.common.util.EList | ||
40 | 32 | ||
41 | class ViatraReasoner extends LogicReasoner{ | 33 | class ViatraReasoner extends LogicReasoner{ |
42 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() | 34 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() |
@@ -62,9 +54,7 @@ class ViatraReasoner extends LogicReasoner{ | |||
62 | 54 | ||
63 | val transformationStartTime = System.nanoTime | 55 | val transformationStartTime = System.nanoTime |
64 | 56 | ||
65 | val emptySolution = initialiser.initialisePartialInterpretation(problem, | 57 | val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output |
66 | viatraConfig.typeScopes.minNewElements, | ||
67 | viatraConfig.typeScopes.maxNewElements).output | ||
68 | emptySolution.problemConainer = problem | 58 | emptySolution.problemConainer = problem |
69 | 59 | ||
70 | val method = modelGenerationMethodProvider.createModelGenerationMethod( | 60 | val method = modelGenerationMethodProvider.createModelGenerationMethod( |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend index 56c3c852..3db21ea4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend | |||
@@ -4,34 +4,83 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | |||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation | 14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation |
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | ||
19 | import java.math.BigDecimal | ||
13 | import java.util.HashMap | 20 | import java.util.HashMap |
14 | import java.util.List | 21 | import java.util.List |
15 | import java.util.Map | 22 | import java.util.Map |
16 | import org.eclipse.emf.ecore.EObject | 23 | import org.eclipse.emf.ecore.EObject |
24 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
17 | 25 | ||
18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 26 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 27 | import java.util.TreeSet |
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink | ||
21 | 28 | ||
22 | class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | 29 | class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ |
23 | val PartialInterpretation partialInterpretation | 30 | val PartialInterpretation partialInterpretation |
24 | val Map<EObject, EObject> trace; | 31 | val Map<EObject, EObject> trace; |
25 | val Map<TypeDeclaration,PartialTypeInterpratation> type2Interpretation | 32 | val Map<TypeDeclaration,PartialTypeInterpratation> type2Interpretation |
26 | val Map<RelationDeclaration,PartialRelationInterpretation> relation2Interpretation | 33 | val Map<RelationDeclaration,PartialRelationInterpretation> relation2Interpretation |
34 | |||
27 | val Map<DefinedElement,DefinedElement> elementBackwardTrace | 35 | val Map<DefinedElement,DefinedElement> elementBackwardTrace |
36 | val Map<Boolean, BooleanElement> booleanForwardTrace | ||
37 | val Map<Integer, IntegerElement> integerForwardTrace | ||
38 | val Map<BigDecimal, RealElement> realForwardTrace | ||
39 | val Map<String, StringElement> stringForwardTrace | ||
28 | 40 | ||
29 | new(PartialInterpretation partialInterpretation, Map<EObject, EObject> forwardMap) { | 41 | new(PartialInterpretation partialInterpretation, Map<EObject, EObject> forwardMap) { |
30 | this.partialInterpretation = partialInterpretation | 42 | this.partialInterpretation = partialInterpretation |
31 | this.trace = forwardMap | 43 | this.trace = forwardMap |
32 | this.type2Interpretation = initTypes(partialInterpretation.partialtypeinterpratation) | 44 | this.type2Interpretation = initTypes(partialInterpretation.partialtypeinterpratation) |
33 | this.relation2Interpretation = initRelations(partialInterpretation.partialrelationinterpretation) | 45 | this.relation2Interpretation = initRelations(partialInterpretation.partialrelationinterpretation) |
46 | |||
34 | this.elementBackwardTrace = initElementBackwardTrace(trace) | 47 | this.elementBackwardTrace = initElementBackwardTrace(trace) |
48 | this.booleanForwardTrace = initialisePrimitiveElementTrace( | ||
49 | null,null,null,partialInterpretation.booleanelements,[it.value]) | ||
50 | integerForwardTrace = initialisePrimitiveElementTrace( | ||
51 | 0,[it+1],[it],partialInterpretation.integerelements,[it.value]) | ||
52 | realForwardTrace = initialisePrimitiveElementTrace( | ||
53 | BigDecimal::ZERO,[it.add(BigDecimal.ONE)],[it],partialInterpretation.realelements,[it.value]) | ||
54 | stringForwardTrace = initialisePrimitiveElementTrace( | ||
55 | 0,[it+1],['''StringĀ«itĀ»'''],partialInterpretation.stringelement,[it.value]) | ||
56 | } | ||
57 | |||
58 | private def <Seed,Type,ElementType extends PrimitiveElement> Map<Type,ElementType> initialisePrimitiveElementTrace( | ||
59 | Seed initialSeed, | ||
60 | Function1<Seed,Seed> nextSeed, | ||
61 | Function1<Seed,Type> seed2Value, | ||
62 | Iterable<ElementType> elements, | ||
63 | Function1<ElementType,Type> element2Value) | ||
64 | { | ||
65 | val forwardMap = new HashMap | ||
66 | |||
67 | val assignedElements = elements.filter[it.valueSet] | ||
68 | for(assignedElement : assignedElements) { | ||
69 | forwardMap.put(element2Value.apply(assignedElement),assignedElement) | ||
70 | } | ||
71 | |||
72 | val unsassignedElements = elements.filter[!it.valueSet] | ||
73 | var seed = initialSeed | ||
74 | var newValue = seed2Value.apply(seed) | ||
75 | for(unassignedElement : unsassignedElements) { | ||
76 | while(forwardMap.keySet.contains(newValue)) { | ||
77 | seed = nextSeed.apply(seed) | ||
78 | newValue = seed2Value.apply(seed) | ||
79 | } | ||
80 | forwardMap.put(newValue,unassignedElement) | ||
81 | } | ||
82 | |||
83 | return forwardMap | ||
35 | } | 84 | } |
36 | 85 | ||
37 | def initTypes(List<PartialTypeInterpratation> types) { | 86 | def initTypes(List<PartialTypeInterpratation> types) { |
@@ -56,10 +105,23 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | |||
56 | return t2.elements.map[it.elementLookupBackward] | 105 | return t2.elements.map[it.elementLookupBackward] |
57 | } | 106 | } |
58 | 107 | ||
59 | def elementLookupForward(DefinedElement e) { | 108 | def dispatch elementLookupForward(DefinedElement e) { |
60 | if(this.trace.containsKey(e)) return e.lookup(trace) as DefinedElement | 109 | if(this.trace.containsKey(e)) return e.lookup(trace) as DefinedElement |
61 | else return e; | 110 | else return e; |
62 | } | 111 | } |
112 | def dispatch elementLookupForward(BooleanElement e) { | ||
113 | this.booleanForwardTrace.get(e) | ||
114 | } | ||
115 | def dispatch elementLookupForward(Integer e) { | ||
116 | this.integerForwardTrace.get(e) | ||
117 | } | ||
118 | def dispatch elementLookupForward(BigDecimal e) { | ||
119 | this.realForwardTrace.get(e) | ||
120 | } | ||
121 | def dispatch elementLookupForward(String e) { | ||
122 | this.stringForwardTrace.get(e) | ||
123 | } | ||
124 | |||
63 | def elementLookupBackward(DefinedElement e) { | 125 | def elementLookupBackward(DefinedElement e) { |
64 | if(this.elementBackwardTrace.containsKey(e)) return e.lookup(this.elementBackwardTrace) | 126 | if(this.elementBackwardTrace.containsKey(e)) return e.lookup(this.elementBackwardTrace) |
65 | else return e; | 127 | else return e; |
@@ -71,14 +133,18 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | |||
71 | 133 | ||
72 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | 134 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { |
73 | if(parameterSubstitution.size == 2) { | 135 | if(parameterSubstitution.size == 2) { |
74 | val param1 = (parameterSubstitution.get(0) as DefinedElement).elementLookupForward | 136 | val param1 = parameterSubstitution.get(0).elementLookupForward |
75 | val param2 = (parameterSubstitution.get(1) as DefinedElement).elementLookupForward | 137 | val param2 = parameterSubstitution.get(1).elementLookupForward |
76 | val r1 = relation.lookup(trace) as RelationDeclaration | 138 | if(param1 != null && param2 != null) { |
77 | val r2 = r1.lookup(this.relation2Interpretation) | 139 | val r1 = relation.lookup(trace) as RelationDeclaration |
78 | val links = r2.relationlinks.filter(BinaryElementRelationLink) | 140 | val r2 = r1.lookup(this.relation2Interpretation) |
79 | val existLink = links.exists[it.param1 == param1 && it.param2 == param2] | 141 | val links = r2.relationlinks.filter(BinaryElementRelationLink) |
80 | //println(existLink) | 142 | val existLink = links.exists[it.param1 == param1 && it.param2 == param2] |
81 | return existLink | 143 | //println(existLink) |
144 | return existLink | ||
145 | } else { | ||
146 | return false | ||
147 | } | ||
82 | } else throw new UnsupportedOperationException | 148 | } else throw new UnsupportedOperationException |
83 | } | 149 | } |
84 | 150 | ||
@@ -86,6 +152,15 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | |||
86 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 152 | throw new UnsupportedOperationException("TODO: auto-generated method stub") |
87 | } | 153 | } |
88 | 154 | ||
89 | override getMinimalInteger() {0} | 155 | override getAllIntegersInStructure() { |
90 | override getMaximalInteger() {0} | 156 | new TreeSet(this.integerForwardTrace.keySet) |
157 | } | ||
158 | |||
159 | override getAllRealsInStructure() { | ||
160 | new TreeSet(this.realForwardTrace.keySet) | ||
161 | } | ||
162 | |||
163 | override getAllStringsInStructure() { | ||
164 | new TreeSet(this.stringForwardTrace.keySet) | ||
165 | } | ||
91 | } \ No newline at end of file | 166 | } \ No newline at end of file |