From 96aaf81612d6c8176149c77817101b239fc52d62 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Tue, 15 Aug 2017 03:32:05 +0200 Subject: Viatra Solver result support for primitive types --- .../dse/PartialModelAsLogicInterpretation.xtend | 103 ++++++++++++++++++--- 1 file changed, 89 insertions(+), 14 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse') 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 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement +import java.math.BigDecimal import java.util.HashMap import java.util.List import java.util.Map import org.eclipse.emf.ecore.EObject +import org.eclipse.xtext.xbase.lib.Functions.Function1 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink +import java.util.TreeSet class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ val PartialInterpretation partialInterpretation val Map trace; val Map type2Interpretation val Map relation2Interpretation + val Map elementBackwardTrace + val Map booleanForwardTrace + val Map integerForwardTrace + val Map realForwardTrace + val Map stringForwardTrace new(PartialInterpretation partialInterpretation, Map forwardMap) { this.partialInterpretation = partialInterpretation this.trace = forwardMap this.type2Interpretation = initTypes(partialInterpretation.partialtypeinterpratation) this.relation2Interpretation = initRelations(partialInterpretation.partialrelationinterpretation) + this.elementBackwardTrace = initElementBackwardTrace(trace) + this.booleanForwardTrace = initialisePrimitiveElementTrace( + null,null,null,partialInterpretation.booleanelements,[it.value]) + integerForwardTrace = initialisePrimitiveElementTrace( + 0,[it+1],[it],partialInterpretation.integerelements,[it.value]) + realForwardTrace = initialisePrimitiveElementTrace( + BigDecimal::ZERO,[it.add(BigDecimal.ONE)],[it],partialInterpretation.realelements,[it.value]) + stringForwardTrace = initialisePrimitiveElementTrace( + 0,[it+1],['''String«it»'''],partialInterpretation.stringelement,[it.value]) + } + + private def Map initialisePrimitiveElementTrace( + Seed initialSeed, + Function1 nextSeed, + Function1 seed2Value, + Iterable elements, + Function1 element2Value) + { + val forwardMap = new HashMap + + val assignedElements = elements.filter[it.valueSet] + for(assignedElement : assignedElements) { + forwardMap.put(element2Value.apply(assignedElement),assignedElement) + } + + val unsassignedElements = elements.filter[!it.valueSet] + var seed = initialSeed + var newValue = seed2Value.apply(seed) + for(unassignedElement : unsassignedElements) { + while(forwardMap.keySet.contains(newValue)) { + seed = nextSeed.apply(seed) + newValue = seed2Value.apply(seed) + } + forwardMap.put(newValue,unassignedElement) + } + + return forwardMap } def initTypes(List types) { @@ -56,10 +105,23 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ return t2.elements.map[it.elementLookupBackward] } - def elementLookupForward(DefinedElement e) { + def dispatch elementLookupForward(DefinedElement e) { if(this.trace.containsKey(e)) return e.lookup(trace) as DefinedElement else return e; } + def dispatch elementLookupForward(BooleanElement e) { + this.booleanForwardTrace.get(e) + } + def dispatch elementLookupForward(Integer e) { + this.integerForwardTrace.get(e) + } + def dispatch elementLookupForward(BigDecimal e) { + this.realForwardTrace.get(e) + } + def dispatch elementLookupForward(String e) { + this.stringForwardTrace.get(e) + } + def elementLookupBackward(DefinedElement e) { if(this.elementBackwardTrace.containsKey(e)) return e.lookup(this.elementBackwardTrace) else return e; @@ -71,14 +133,18 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { if(parameterSubstitution.size == 2) { - val param1 = (parameterSubstitution.get(0) as DefinedElement).elementLookupForward - val param2 = (parameterSubstitution.get(1) as DefinedElement).elementLookupForward - val r1 = relation.lookup(trace) as RelationDeclaration - val r2 = r1.lookup(this.relation2Interpretation) - val links = r2.relationlinks.filter(BinaryElementRelationLink) - val existLink = links.exists[it.param1 == param1 && it.param2 == param2] - //println(existLink) - return existLink + val param1 = parameterSubstitution.get(0).elementLookupForward + val param2 = parameterSubstitution.get(1).elementLookupForward + if(param1 != null && param2 != null) { + val r1 = relation.lookup(trace) as RelationDeclaration + val r2 = r1.lookup(this.relation2Interpretation) + val links = r2.relationlinks.filter(BinaryElementRelationLink) + val existLink = links.exists[it.param1 == param1 && it.param2 == param2] + //println(existLink) + return existLink + } else { + return false + } } else throw new UnsupportedOperationException } @@ -86,6 +152,15 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ throw new UnsupportedOperationException("TODO: auto-generated method stub") } - override getMinimalInteger() {0} - override getMaximalInteger() {0} + override getAllIntegersInStructure() { + new TreeSet(this.integerForwardTrace.keySet) + } + + override getAllRealsInStructure() { + new TreeSet(this.realForwardTrace.keySet) + } + + override getAllStringsInStructure() { + new TreeSet(this.stringForwardTrace.keySet) + } } \ No newline at end of file -- cgit v1.2.3-54-g00ecf