From 8af821e133a51179c1692cd48fb03cad80124e54 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 24 Apr 2019 19:54:57 -0400 Subject: VAMPIRE : initial model handling almost done. only typeScope remains #40 --- .../builder/Logic2VampireLanguageMapper.xtend | 8 +-- .../builder/Logic2VampireLanguageMapperTrace.xtend | 1 + ...c2VampireLanguageMapper_ContainmentMapper.xtend | 63 +++++++++---------- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 70 ++++++++++++++++++---- .../Logic2VampireLanguageMapper_TypeMapper.xtend | 30 ++++++++-- 5 files changed, 119 insertions(+), 53 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index 2be6c093..13db3c99 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend @@ -78,10 +78,7 @@ class Logic2VampireLanguageMapper { if (!problem.types.isEmpty) { typeMapper.transformTypes(problem.types, problem.elements, this, trace) } - - // SCOPE MAPPER - scopeMapper.transformScope(config, trace) - + // RELATION MAPPER trace.relationDefinitions = problem.collectRelationDefinitions problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] @@ -89,6 +86,9 @@ class Logic2VampireLanguageMapper { // CONTAINMENT MAPPER containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) + // SCOPE MAPPER + scopeMapper.transformScope(problem.types, config, trace) + // CONSTANT MAPPER // only transforms definitions trace.constantDefinitions = problem.collectConstantDefinitions diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend index b9928383..e0089c41 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend @@ -31,6 +31,7 @@ class Logic2VampireLanguageMapperTrace { public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace public var Map definedElement2String = new HashMap + public var topLvlElementIsInInitialModel = null public val Map type2Predicate = new HashMap; public val Map element2Predicate = new HashMap diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index c56b54be..9f29ea49 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend @@ -15,6 +15,7 @@ import java.util.Map import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl class Logic2VampireLanguageMapper_ContainmentMapper { val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -36,7 +37,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { val containmentListCopy = hierarchy.typesOrderedInHierarchy val relationsList = hierarchy.containmentRelations val toRemove = newArrayList - + // STEP 1 // Find root element for (l : relationsList) { @@ -48,7 +49,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { containmentListCopy.remove(c) } } - + // OLD // for (c : containmentListCopy) { // if(c.isIsAbstract) { @@ -58,42 +59,43 @@ class Logic2VampireLanguageMapper_ContainmentMapper { // State that there must exist 1 and only 1 root element // val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString // val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) - var topTermVar = containmentListCopy.get(0) for (l : relationsList) { var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type - if(containmentListCopy.contains(pointingFrom)) { - //The correct topTerm will be identified + if (containmentListCopy.contains(pointingFrom)) { + // The correct topTerm will be identified topTermVar = pointingFrom } } - + val topName = topTermVar.lookup(trace.type2Predicate).constant.toString val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate)) - - - + var topLvlIsInInitModel = false var topLvlString = "" - for ( c : topTermVar.subtypes) { - if (c.class.simpleName.equals("TypeDefinitionImpl") ) { + var listToCheck = newArrayList(topTermVar) + listToCheck.addAll(topTermVar.subtypes) + for (c : listToCheck) { + if (c.class == typeof(TypeDefinitionImpl)) { - for (d : (c as TypeDefinition).elements) { - if (trace.definedElement2String.containsKey(d)) { - topLvlIsInInitModel = true - topLvlString = d.lookup(trace.definedElement2String) + if((c as TypeDefinition).elements.length >1) { + throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model") + } + + for (d : (c as TypeDefinition).elements) { + if (trace.definedElement2String.containsKey(d)) { + topLvlIsInInitModel = true + topLvlString = d.lookup(trace.definedElement2String) + } } } - - } - - + } + + trace.topLvlElementIsInInitialModel = topLvlIsInInitModel val topInIM = topLvlIsInInitModel val topStr = topLvlString - print(topInIM) - print(topStr) - + val contTop = createVLSFofFormula => [ it.name = support.toIDMultiple("containment_topLevel", topName) it.fofRole = "axiom" @@ -105,7 +107,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { it.right = createVLSEquality => [ it.left = support.duplicate(variable) it.right = createVLSConstant => [ - it.name = if (topInIM) topStr else "o1" + it.name = if(topInIM) topStr else "o1" ] ] ] @@ -119,8 +121,8 @@ class Logic2VampireLanguageMapper_ContainmentMapper { ] trace.specification.formulas += contTop - // STEP 2 - // for each edge, if the pointedTo element exists,the edge must exist also +// STEP 2 +// for each edge, if the pointedTo element exists,the edge must exist also val varA = createVLSVariable => [it.name = "A"] val varB = createVLSVariable => [it.name = "B"] val varC = createVLSVariable => [it.name = "C"] @@ -207,23 +209,22 @@ class Logic2VampireLanguageMapper_ContainmentMapper { // STEP 4 // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) // Attempt 1: all possibilities, even the impossible one, based on MM constraints, are listed - - val variables = newArrayList val disjunctionList = newArrayList val conjunctionList = newArrayList for (var i = 1; i <= config.contCycleLevel; i++) { val ind = i - variables.add(createVLSVariable => [it.name = ("V"+Integer.toString(ind))]) - for ( var j = 0; j < i;j++){ + variables.add(createVLSVariable => [it.name = ("V" + Integer.toString(ind))]) + for (var j = 0; j < i; j++) { for (l : relationsList) { - val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), newArrayList(variables.get(j), variables.get((j+1)%i))) + val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), + newArrayList(variables.get(j), variables.get((j + 1) % i))) disjunctionList.add(rel) } conjunctionList.add(support.unfoldOr(disjunctionList)) disjunctionList.clear } - + val contCycleForm = createVLSFofFormula => [ it.name = support.toIDMultiple("containment_noCycle", Integer.toString(ind)) it.fofRole = "axiom" diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index c50aa770..ec841546 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend @@ -5,8 +5,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition import java.util.ArrayList import java.util.HashMap +import java.util.List import java.util.Map import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* @@ -21,7 +23,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { this.base = base } - def dispatch public void transformScope(VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { + def dispatch public void transformScope(List types, VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { val ABSOLUTE_MIN = 0 val ABSOLUTE_MAX = Integer.MAX_VALUE @@ -31,8 +33,22 @@ class Logic2VampireLanguageMapper_ScopeMapper { // 1. make a list of constants equaling the min number of specified objects //These numbers do not include enums or initial model elements - val GLOBAL_MIN = config.typeScopes.minNewElements - val GLOBAL_MAX = config.typeScopes.maxNewElements + //Number of defined non-abstract elements that are not enum elements + //Equals the number of elements in te initial model + var elemsInIM = trace.definedElement2String.size +// var elemsInIM = 0 +// +// for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { +// val len = t.name.length +// val isNotEnum = !t.name.substring(len-4, len).equals("enum") +// if (isNotEnum) { +// elemsInIM += 1 +// } +// } + + //TODO handle errors related to GLOBAL_MIN/MAX < 0 + val GLOBAL_MIN = config.typeScopes.minNewElements-elemsInIM + val GLOBAL_MAX = config.typeScopes.maxNewElements-elemsInIM val localInstances = newArrayList @@ -63,31 +79,61 @@ class Logic2VampireLanguageMapper_ScopeMapper { // Handling Minimum_Specific var i = 1 + if (trace.topLvlElementIsInInitialModel as Boolean){ + i = 0 + } var minNum = -1 var Map startPoints = new HashMap - for (t : config.typeScopes.minNewElementsByType.keySet) { - minNum = t.lookup(config.typeScopes.minNewElementsByType) +// var inIM = false + for (tConfig : config.typeScopes.minNewElementsByType.keySet) { +// var numIniIntModel = 0 +// for (elem : trace.definedElement2String.keySet) { +// println(elem.definedInType) +// for (tDefined : elem.definedInType) { +// inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined) +// } +// if (inIM) { +// numIniIntModel += 1 +// } +// inIM = false +// } + + minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel if (minNum != 0) { getInstanceConstants(i + minNum, i, localInstances, trace, true, false) - startPoints.put(t, i) + startPoints.put(tConfig, i) i += minNum - makeFofFormula(localInstances, trace, true, t) + makeFofFormula(localInstances, trace, true, tConfig) } } // TODO: calc sum of mins, compare to current value of i // Handling Maximum_Specific - for (t : config.typeScopes.maxNewElementsByType.keySet) { - var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) - minNum = t.lookup(config.typeScopes.minNewElementsByType) - var startpoint = t.lookup(startPoints) + for (tConfig : config.typeScopes.maxNewElementsByType.keySet) { + +// var numIniIntModel = 0 +// for (elem : trace.definedElement2String.keySet) { +// println(elem.definedInType) +// for (tDefined : elem.definedInType) { +// inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined) +// } +// if (inIM) { +// numIniIntModel += 1 +// } +// inIM = false +// } + + var maxNum = tConfig.lookup(config.typeScopes.maxNewElementsByType)//-numIniIntModel + minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel + var startpoint = tConfig.lookup(startPoints) if (minNum != 0) { getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) } + //I do not understand the line below if (maxNum != minNum) { var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum) getInstanceConstants(instEndInd, i, localInstances, trace, false, false) - makeFofFormula(localInstances, trace, false, t) + makeFofFormula(localInstances, trace, false, tConfig) } } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index 2a121446..1b30393f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend @@ -44,13 +44,31 @@ class Logic2VampireLanguageMapper_TypeMapper { trace.type2Predicate.put(type, typePred) } - // 2. Map each ENUM type definition to fof formula - // This also Handles initial Model stuff - for (type : types.filter(TypeDefinition)) { + // 2. Map each ENUM/InitialModelElement type definition to fof formula + // In the case where , for example, a supertype that is abstract has a subtype of which an instance is in the initial model, + // The logic problem will contain a TypeDefinition for the subtype as well as for the supertype + // This defined elemtn for the supertype will be abstract, and we do not wish to associate a constant to it, or associate it with a type + // Within our vampireproblem.tptp + for (type : types.filter(TypeDefinition).filter[!isIsAbstract]) { + + //Detect if it is a defined element (from initial model) + //Otherwise it is an Enum + + //val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract + //^does not work in cases where a defined type already has a supertype from within the MM + +// var isNotEnumVar = !type.supertypes.isEmpty +// if(isNotEnumVar) { +// for (sup : type.supertypes){ +// type.name.contains(sup.name) +// } +// } +// +// val isNotEnum = isNotEnumVar - //Detect if is an Enum - //Otherwise, it is a defined element (from initial model) - val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract + //Another possibility is.. + val len = type.name.length + val isNotEnum = !type.name.substring(len-4, len).equals("enum") // Create a VLSFunction for each Enum Element val List orElems = newArrayList -- cgit v1.2.3-54-g00ecf