From 5ac36bba74bcf71224d4895cccdae253b07ccbc9 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 7 Mar 2018 12:48:01 -0500 Subject: Rebooting Z3 solver Containment vs Inheritance still has a bug --- .../Logic2SMT_TypeMapperInterpretation.xtend | 2 +- .../dslreasoner/smt/reasoner/Logic2SmtMapper.xtend | 315 ++++++++++++++++++++- .../Logic2Smt_TypeMapper_FilteredTypes.xtend | 129 +++++++-- ...Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ | 44 ++- .../inf/dslreasoner/smt/reasoner/SMTSolver.xtend | 3 +- .../smt/reasoner/builder/SmtSolverHandler.xtend | 8 +- 6 files changed, 437 insertions(+), 64 deletions(-) (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner') diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend index 44708f44..e7f35626 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend @@ -23,7 +23,7 @@ class Logic2SMT_TypeMapperInterpretation { } public def getElements(Type type) { - return type2Elements.get(type) + return type.lookup(this.type2Elements) } public def ValueType logicElement2Smt(DefinedElement element) { diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend index aad43716..ec1502e5 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend @@ -1,5 +1,6 @@ package hu.bme.mit.inf.dslreasoner.smt.reasoner +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And @@ -42,13 +43,17 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr @@ -60,6 +65,7 @@ import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory +import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil import java.util.ArrayList import java.util.HashMap import java.util.LinkedHashMap @@ -72,18 +78,14 @@ import org.eclipse.xtend.lib.annotations.Accessors import org.eclipse.xtext.xbase.lib.Functions.Function0 import org.eclipse.xtext.xbase.lib.Functions.Function1 import org.eclipse.xtext.xbase.lib.Functions.Function2 + import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy -import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder class Logic2SmtMapper{ val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport @Accessors val Logic2Smt_TypeMapper typeMapper; - LogicProblemBuilder b - new(Logic2Smt_TypeMapper typeMapper) { this.typeMapper = typeMapper } @@ -109,11 +111,16 @@ class Logic2SmtMapper{ problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)] documentInput.assertions += problem.assertions.map[transformAssertion(trace)] + + if(!problem.containmentHierarchies.empty) { + transformContainmentV1(documentInput,problem.containmentHierarchies.head,trace) + } // End trafo document.input.assertions.forEach[it.value.nameAllUnnamedVariable] document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable] document.cleanDocument + document.orderDefinitions return new TracedOutput(document,trace) } @@ -1000,15 +1007,269 @@ class Logic2SmtMapper{ /////////// - /*def transformContainment(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) { - val containmentRelation_oo = createSMTFunctionDefinition=>[ - it.name="containment!oo" - it.range=createSMTBoolTypeReference - val child = createSMTSortedVariable => [ - it.name = + def transformContainmentV1(SMTInput document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) { + val extension builder = new LogicProblemBuilder + val types = h.typesOrderedInHierarchy + + val rootRelations = new HashMap + for(type: types) { + val rootRelation = RelationDeclaration('''Root «type.name»''',type) + rootRelations.put(type,rootRelation) + this.transformRelationDeclaration(rootRelation,document,trace) + } + val possibleParentRelations = types.toInvertedMap[type| + h.containmentRelations.filter[it.parameters.get(1) === type] + //TODO inheritance + ] + + // root is true only for at most one element in every root type + for(root: rootRelations.entrySet) { + val a1 = Assertion(Forall[ + val r1 = addVar(root.key) + val r2 = addVar(root.key) + (root.value.call(r1) && root.value.call(r2)) => (r1 == r2) + ]) + document.assertions+=this.transformAssertion(a1,trace) + } + // only one of the root entries is true +// val a2 = Assertion( +// rootRelations.entrySet.map[selected| +// rootRelations.entrySet.map[other| +// if(selected == other) { +// Exists[ +// val r = addVar(other.key) +// other.value.call(r) +// ] +// } else { +// Forall[ +// val r = addVar(other.key) +// !other.value.call(r) +// ] +// } +// ].And +// ].Or +// ) +// document.assertions+=this.transformAssertion(a2,trace) +// // the root has no parent +// for(root : rootRelations.entrySet) { +// val parentRelations = root.key.lookup(possibleParentRelations) +// val a3 = Assertion(Forall[ +// val r = addVar(root.key) +// root.value.call(r) => parentRelations.map[containment | +// Forall[ +// val container = addVar(containment.parameters.get(0)) +// !containment.call(container,r) +// ] +// ].And +// ]) +// document.assertions+=this.transformAssertion(a3,trace) +// } +// // no element has two parents +// for(root : rootRelations.entrySet) { +// val parentRelations = root.key.lookup(possibleParentRelations) +// val a4 = Assertion(Forall[ +// val element = addVar(root.key) +// parentRelations.map[selected | +// Forall[ +// val container = addVar(selected.parameters.get(0)) +// selected.call(container,element) => ( +// Forall[ +// val other = addVar(selected.parameters.get(0)) +// (!selected.call(other,element)) || (other == element) +// ] && +// parentRelations.filter[it !==selected].map[otherContainment | +// Forall[ +// val other = addVar(otherContainment.parameters.get(0)) +// otherContainment.call(other,element) +// ] +// ].And) +// +// ] +// ].And +// ]) +// document.assertions+=this.transformAssertion(a4,trace) +// } + + // an element is not root, then it has a container + for(root : rootRelations.entrySet) { + val parentRelations = root.key.lookup(possibleParentRelations) + val a5 = Assertion(Forall[ + val element = addVar(root.key) + !root.value.call(element) => + parentRelations.map[selected | + Exists[ + val container = addVar(selected.parameters.get(0)) + selected.call(container,element) + ] + ].Or + ]) + document.assertions+=this.transformAssertion(a5,trace) + } +// +// // no circle in containment +// for(length : 1..5) { +// val paths = h.containmentRelations.paths(length) +// val loopPaths = paths.filter[path| +// val first = (path.head.parameters.get(0) as ComplexTypeReference).referred +// val last = (path.last.parameters.get(1) as ComplexTypeReference).referred +// hasCommonElement(first,last) +// ] +// for(loopPath : loopPaths) { +// val variableIndexes = 0..> paths(Iterable relations, int length) { +// if(length == 0) { +// return #[] +// } else if(length == 1) { +// return relations.map[#[it]] +// } else { +// val previous = paths(relations,length-1) +// val List> res = new ArrayList(previous.size*relations.size) +// for(p:previous) { +// for(r:relations) { +// val lastType = (p.last.parameters.get(1) as ComplexTypeReference).referred +// val firstType = (r.parameters.get(0) as ComplexTypeReference).referred +// val hasCommonElement = hasCommonElement(lastType, firstType) +// if(hasCommonElement) { +// res.add(new ArrayList(p) => [add(r)]) +// } +// } +// } +// return res +// } + } + + protected def boolean hasCommonElement(Type lastType, Type firstType) { + val a = lastType.transitiveClosureStar[subtypes] + val b = firstType.transitiveClosureStar[subtypes] + return a.exists[b.contains(it)] + } + + def transformContainmentV2(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) { + val typeConstraintsOfTypesInContainment = h.typesOrderedInHierarchy + .map[typeMapper.transformTypeReference(it,trace)].flatten + val relationsOfTypeConstraints = h.containmentRelations.map[it] + val typesOfTypeConstraints = typeConstraintsOfTypesInContainment + .map[(it.type as SMTComplexTypeReference).referred] + .toSet + + // Root declaration + val rootRelations = new HashMap + for(t : typesOfTypeConstraints) { + val rootRelation = createSMTFunctionDeclaration => [ + it.name = toID('''root «t.name»''') + it.range = createSMTBoolTypeReference + it.parameters += createSMTComplexTypeReference => [ + it.referred = t + ] + ] + document.input.functionDeclarations += rootRelation + rootRelations.put(t,rootRelation) + } + // root is true only for one element in every root type + for(entry : rootRelations.entrySet) { + document.input.assertions += createSMTAssertion => [ + it.value = createSMTForall => [ + val r1 = createSMTSortedVariable => [ + it.name = "r1" + it.range = createSMTComplexTypeReference => [it.referred = entry.key] + ] + val r2 = createSMTSortedVariable => [ + it.name = "r2" + it.range = createSMTComplexTypeReference => [it.referred = entry.key] + ] + + it.quantifiedVariables += r1 + it.quantifiedVariables += r2 + + it.expression = createSMTImpl => [ + it.leftOperand = createSMTAnd => [ + it.operands += createSMTSymbolicValue => [ + it.symbolicReference = entry.value + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r1] + ] + it.operands += createSMTSymbolicValue => [ + it.symbolicReference = entry.value + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r2] + ] + ] + it.rightOperand = createSMTEquals => [ + it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = r1] + it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = r2] + ] + ] + ] + ] + } + // only one of the root entries is true + document.input.assertions += createSMTAssertion => [ + it.value = createSMTOr =>[or | + for(selectedCombination : rootRelations.entrySet) { + or.operands += createSMTAnd => [and | + for(otherCombination : rootRelations.entrySet) { + if(selectedCombination == otherCombination) { + and.operands += createSMTExists => [ + val r = createSMTSortedVariable => [ + it.name = "r" + it.range = createSMTComplexTypeReference => [it.referred = otherCombination.key] + ] + it.quantifiedVariables += r + it.expression = createSMTSymbolicValue => [ + it.symbolicReference = otherCombination.value + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r] + ] + ] + } else { + and.operands += createSMTForall => [ + val r = createSMTSortedVariable => [ + it.name = "r" + it.range = createSMTComplexTypeReference => [it.referred = otherCombination.key] + ] + it.quantifiedVariables += r + it.expression = createSMTNot=> [ + it.operand = createSMTSymbolicValue => [ + it.symbolicReference = otherCombination.value + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = r] + ] + ] + ] + } + } + ] + } ] ] - }*/ + + // the root has no parent + throw new UnsupportedOperationException('''Unfinished version''') + + // no element has two parents + + // an element is either root or has parent + + // no circle in containment + } /////////// @@ -1052,4 +1313,34 @@ class Logic2SmtMapper{ def private dispatch replaceWith(EObject object) { null } + + def orderDefinitions(SMTDocument document) { + val definitionsInDocument = document.input.functionDefinition + val List definitionsInOrder = new ArrayList(definitionsInDocument.size) + while(!definitionsInDocument.empty) { + val selection = definitionsInDocument.selectOneUnreferenced + definitionsInOrder.add(selection) + definitionsInDocument.remove(selection) + } + document.input.functionDefinition.addAll(definitionsInOrder) + } + + def referencedDefinitions(SMTFunctionDefinition definition) { + definition + .eAllContents + .filter(SMTSymbolicValue) + .map[it.symbolicReference] + .filter(SMTFunctionDefinition) + .toList + } + + def selectOneUnreferenced(List definitions) { + for(definition : definitions) { + val references = definition.referencedDefinitions + if(references.forall[!definitions.contains(it)]) { + return definition + } + } + throw new AssertionError('''Recursion in function definitions! definitions: «definitions.map[name].toList»''') + } } \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend index c9bafa6c..2796e077 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend @@ -27,8 +27,10 @@ import java.util.HashMap import java.util.LinkedList import java.util.List import java.util.Map +import org.eclipse.emf.ecore.EObject import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine import org.eclipse.viatra.query.runtime.emf.EMFScope +import org.eclipse.xtext.EcoreUtil2 import org.eclipse.xtext.xbase.lib.Functions.Function0 import org.eclipse.xtext.xbase.lib.Functions.Function1 @@ -63,32 +65,77 @@ class Logic2Smt_TypeMapperTrace_FilteredTypes implements Logic2Smt_TypeMapperTra val a = this val b = new Logic2Smt_TypeMapperTrace_FilteredTypes - b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name]) - - b.newObjects = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head - b.oldObjects = newModel.typeDeclarations.filter[it.name == a.oldObjects.name].head as SMTEnumeratedTypeDeclaration - b.elementMap = a.elementMap.copyMap(b.oldObjects.elements,[name]) + b.independentClasses = copyMap(a.independentClasses,newModel.typeDeclarations,[name]) + b.independentClasses.values.validate(newModel) + b.newObjects = newModel.typeDeclarations.copyValue(a.newObjects,[name]) + b.newObjects.validate(newModel) + b.oldObjects = newModel.typeDeclarations.copyValue(a.oldObjects,[name]) as SMTEnumeratedTypeDeclaration + b.oldObjects.validate(newModel) + b.elementMap = a.elementMap.copyMap( + newModel.typeDeclarations + .filter(SMTEnumeratedTypeDeclaration) + .map[it.elements] + .flatten, + [name] + ) + b.elementMap.values.validate(newModel) - b.oldObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head as SMTEnumeratedTypeDeclaration + b.oldObjectTypes = newModel.typeDeclarations.copyValue(a.newObjects,[name]) as SMTEnumeratedTypeDeclaration + b.oldObjectTypes.validate(newModel) b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name]) - b.oldObjectTypeFunction = newModel.functionDefinition.filter[it.name == a.oldObjectTypeFunction.name].head + b.oldObjectTypeMap.values.validate(newModel) + b.oldObjectTypeFunction = newModel.functionDefinition.copyValue(a.oldObjectTypeFunction,[name]) + b.oldObjectTypeFunction.validate(newModel) b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) + b.oldObjectTypePredicates.values.validate(newModel) - b.newObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjectTypes.name].head as SMTEnumeratedTypeDeclaration + b.newObjectTypes = newModel.typeDeclarations.copyValue(a.newObjectTypes,[name]) as SMTEnumeratedTypeDeclaration + b.newObjectTypes.validate(newModel) b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name]) - b.newObjectTypeFunction = newModel.functionDeclarations.filter[it.name == a.newObjectTypeFunction.name].head + b.newObjectTypeMap.values.validate(newModel) + b.newObjectTypeFunction = newModel.functionDeclarations.copyValue(a.newObjectTypeFunction,[name]) + b.newObjectTypeFunction.validate(newModel) b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) - + b.newObjectTypePredicates.values.validate(newModel) return b } + + def public static copyValue(Iterable collection, Type target, Function1 extractor) { + if(target===null) { + return null + } else { + val targetValue = extractor.apply(target) + val res = collection.filter[extractor.apply(it)==targetValue].head + return res + } + } + + def validate(EObject element, EObject other) { + if(element != null) { + val headOfElement = EcoreUtil2.getContainerOfType(element,SMTDocument) + val expectedHeadOfElement = EcoreUtil2.getContainerOfType(other,SMTDocument) + if(headOfElement !== expectedHeadOfElement) { + throw new AssertionError(''' + Element in different resource: «element» + Expected root: «expectedHeadOfElement» + Found root: «headOfElement»''') + } + } + } + def validate(Iterable iterable, EObject root) { + if(iterable !== null) + for(element : iterable) { + element.validate(root) + } + } } class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE - private def toID(List names) {names.join("!") } - private def toID(String name) {name.split("\\s+").toID} + private def String toID(List names) { names.map[split("\\s+").join("!")].join("!") } + private def String toID(String name) { name.split("\\s+").join("!")} override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes @@ -105,7 +152,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty // 0. map the simple types - this.transformIndependentTypes(independentTypes,trace) + this.transformIndependentTypes(independentTypes,trace,document) // 1. Has old elements => create supertype for it if(hasOldElements) { @@ -135,7 +182,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { return types.size == 1 && types.head.isIndependentType } - protected def transformIndependentTypes(Iterable types,Logic2SmtMapperTrace trace) { + protected def transformIndependentTypes(Iterable types,Logic2SmtMapperTrace trace, SMTInput document) { for(type: types) { val independentSMTType = createSMTEnumeratedTypeDeclaration => [ name = toID(#["oldType",type.name]) @@ -146,6 +193,7 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { independentSMTType.elements += enumLiteral trace.typeTrace.elementMap.put(element,enumLiteral) } + document.typeDeclarations += independentSMTType } } @@ -474,26 +522,45 @@ class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { val engine = ViatraQueryEngine.on(new EMFScope(problem)) val supertypeStarMatcher = SupertypeStarMatcher.on(engine) - val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet + - trace.typeTrace.newObjectTypeMap.keySet) - .toInvertedMap[new LinkedList] + val Map> type2Elements = new HashMap + for(key : problem.types) { + type2Elements.put(key,new LinkedList) + } - val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse - for(oldElement: trace.typeTrace.elementMap.values) { - val type = interpretation.queryEngine.resolveFunctionDefinition( - trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral - val dynamicType = type.lookup(inverseOldTypeMap) - val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) - supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)] + if(trace.typeTrace.independentClasses != null) { + for(type : trace.typeTrace.independentClasses.keySet) { + if(type instanceof TypeDefinition) { + type.lookup(type2Elements).addAll(type.elements) + } else { + throw new AssertionError('''Independent classes are type definitions, but got: "«type»"''') + } + } } - val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse - for(newElement: newElements.map[value as SMTSymbolicDeclaration]) { - val type = interpretation.queryEngine.resolveFunctionDeclaration( - trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral - val dynamicType = type.lookup(inverseNewTypeMap) - val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) - supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)] + if(trace.typeTrace.oldObjectTypeFunction != null) { + val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse + for(oldElement: trace.typeTrace.elementMap.values) { + val type = interpretation.queryEngine.resolveFunctionDefinition( + trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral + val dynamicType = type.lookup(inverseOldTypeMap) + val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) + for(superType : supertypes) { + superType.lookup(type2Elements) += oldElement.lookup(smt2logic) + } + } + } + + if(trace.typeTrace.newObjectTypeFunction !== null) { + val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse + for(newElement: newElements.map[value as SMTSymbolicDeclaration]) { + val type = interpretation.queryEngine.resolveFunctionDeclaration( + trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral + val dynamicType = type.lookup(inverseNewTypeMap) + val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) + for(superType : supertypes) { + superType.lookup(type2Elements) += newElement.lookup(smt2logic) + } + } } return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic) diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ index 79fc38e6..ceb7cc06 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ @@ -1,24 +1,38 @@ package hu.bme.mit.inf.dslreasoner.smt.reasoner -import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type -import java.util.HashMap -import java.util.Map -import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput -import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition -import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral -import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement -import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +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.logic.model.logiclanguage.TypeDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem -import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes +import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher +import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSetTypeDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import java.util.ArrayList +import java.util.HashMap +import java.util.LinkedList import java.util.List -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import java.util.Map import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine import org.eclipse.viatra.query.runtime.emf.EMFScope +import org.eclipse.xtext.xbase.lib.Functions.Function0 +import org.eclipse.xtext.xbase.lib.Functions.Function1 + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class Logic2Smt_TypeMapperTrace_FilteredTypesSimple implements Logic2Smt_TypeMapperTrace{ public var Map independentClasses = new HashMap @@ -58,8 +72,8 @@ class Logic2Smt_TypeMapper_FilteredTypesSimple implements Logic2Smt_TypeMapper{ val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE - private def toID(List names) {names.join("!") } - private def toID(String name) {name.split("\\s+").toID} + private def String toID(List names) { names.map[split("\\s+").join("!")].join("!") } + private def String toID(String name) { name.split("\\s+").join("!")} override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes @@ -80,7 +94,7 @@ class Logic2Smt_TypeMapper_FilteredTypesSimple implements Logic2Smt_TypeMapper{ this.transformUndefinedElements(scopes,trace,document) - this.transforTypes(connectedTypes, connectedElements, trace, document, engine) + this.transformType(connectedTypes, connectedElements, trace, document, engine) // 3.2: Type definition to new elements if(hasNewElements) { this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine); diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend index 4e2e1890..76b1ddbd 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend @@ -35,8 +35,7 @@ class SMTSolver extends LogicReasoner{ handler.callSolver(input,configuration) val solverTime = System.currentTimeMillis - solverTimeStart val outputModel = workspace.reloadModel(typeof(SMTDocument), "problem.smt2") - EcoreUtil.resolveAll(outputModel) - workspace.deactivateModel("problem.smt2") + EcoreUtil.resolveAll(outputModel.eResource) return backMapper.transformOutput(problem,outputModel.output,trace, transformationTime, solverTime) } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''') } diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend index 38ae1dae..d2c54aaf 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend @@ -17,9 +17,12 @@ class SmtSolverException extends Exception{ class SmtSolverHandler { public def callSolver(URI resourceURI, SmtSolverConfiguration configuration) { + val URI smtUri = CommonPlugin.resolve(resourceURI) val File smtFile = new File(smtUri.toFileString()) + val path = configuration.solverPath + if(path===null) {throw new IllegalArgumentException('''Path to solver is not specified!''')} val params = '''/smt2 /st« IF configuration.runtimeLimit != SmtSolverConfiguration::Unlimited» /T:«configuration.runtimeLimit»«ENDIF»« @@ -28,9 +31,9 @@ class SmtSolverHandler { » «smtFile.path»''' val Runtime runTime = Runtime.getRuntime() - + try { - val process = runTime.exec(configuration.solverPath + " " + params) + val process = runTime.exec(path + " " + params) val FileWriter writer = new FileWriter(smtFile,true) writer.append("\n--------------\n") @@ -44,7 +47,6 @@ class SmtSolverHandler { return resourceURI } - def private void printStream(InputStream inputStream) throws IOException { val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream)) var int line = -1 -- cgit v1.2.3-54-g00ecf