From 598daf4605d97466d07c74b1bc76d165be145288 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 25 Apr 2019 02:50:40 -0400 Subject: VAMPIRE: fixed MANY bugs in containment and scope. #40 is good for now --- .../builder/Logic2VampireLanguageMapperTrace.xtend | 1 + ...c2VampireLanguageMapper_ContainmentMapper.xtend | 38 ++++++-- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 101 +++++++++++---------- 3 files changed, 82 insertions(+), 58 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill') 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 e0089c41..e94584ae 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 @@ -32,6 +32,7 @@ class Logic2VampireLanguageMapperTrace { public var Map definedElement2String = new HashMap public var topLvlElementIsInInitialModel = null + public var topLevelType = 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 9f29ea49..93c28e7c 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 @@ -70,6 +70,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { val topName = topTermVar.lookup(trace.type2Predicate).constant.toString val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate)) + trace.topLevelType = topTermVar var topLvlIsInInitModel = false var topLvlString = "" @@ -129,16 +130,22 @@ class Logic2VampireLanguageMapper_ContainmentMapper { val varList = newArrayList(varB, varA) val Map> type2cont = new HashMap for (l : relationsList) { - val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList) + val rel = (l as RelationDeclaration).lookup(trace.rel2Predicate) // val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type) val toFunc = toType.lookup(trace.type2Predicate) - addToMap(type2cont, toFunc, rel) - - for (c : toType.subtypes) { - addToMap(type2cont, toFunc, rel) + addToMap(type2cont, support.duplicate(toFunc), support.duplicate(rel, varList)) + + var subTypes = newArrayList + support.listSubtypes(toType, subTypes) + for (c : subTypes) { + addToMap(type2cont, support.duplicate(c.lookup(trace.type2Predicate)), support.duplicate(rel, varList)) } + + + + // for (c : support.listSubtypes(toType)) { // addToMap(type2cont, toFunc, rel) // } @@ -182,6 +189,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { // STEP 2 CONT'D for (e : type2cont.entrySet) { + println(e.key + " " + e.value) val relFormula = createVLSFofFormula => [ it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) it.fofRole = "axiom" @@ -192,6 +200,11 @@ class Logic2VampireLanguageMapper_ContainmentMapper { it.left = support.duplicate(e.key, varA) it.right = createVLSExistentialQuantifier => [ it.variables += support.duplicate(varB) +// for ( x : type2cont.entrySet) { +// if (support.dfsSupertypeCheck(e.key, x.key)) { +// e.value.addAll(x.value) +// } +// } if (e.value.length > 1) { it.operand = makeUnique(e.value) } else { @@ -264,11 +277,20 @@ class Logic2VampireLanguageMapper_ContainmentMapper { } protected def Object addToMap(Map> type2cont, VLSFunction toFunc, VLSFunction rel) { - if (!type2cont.containsKey(toFunc)) { + var keyInMap = false + var existingKey = createVLSFunction + for (k : type2cont.keySet) { + if (k.constant.equals(toFunc.constant)) { + keyInMap = true + existingKey = k + } + } + + if (!keyInMap) { type2cont.put(toFunc, newArrayList(rel)) } else { - if (!type2cont.get(toFunc).contains(rel)) { - type2cont.get(toFunc).add(rel) + if (!type2cont.get(existingKey).contains(rel)) { + type2cont.get(existingKey).add(rel) // type2cont.replace(toFunc, newArrayList(firstRel)) } 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 ec841546..df3cfd82 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 @@ -23,18 +23,22 @@ class Logic2VampireLanguageMapper_ScopeMapper { this.base = base } - def dispatch public void transformScope(List types, 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 // TODO HANDLE ERRORS RELATED TO MAX > MIN // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS -// TODO HANDLE - // 1. make a list of constants equaling the min number of specified objects - //These numbers do not include enums or initial model elements +// TODO HANDLE case where init model does not satisfy for example ine and only one criterion of toplvl elem +// We are currently ignoring all typescope spec related to the topLevel type +// TODO Case where typeScope spec continas numbers for a type and its subtype +// We shouldnt waste constants for each one - //Number of defined non-abstract elements that are not enum elements - //Equals the number of elements in te initial model + // 1. make a list of constants equaling the min number of specified objects + // These numbers do not include enums or initial model elements + // 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 // @@ -45,10 +49,9 @@ class Logic2VampireLanguageMapper_ScopeMapper { // 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 + // 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 @@ -79,62 +82,60 @@ class Logic2VampireLanguageMapper_ScopeMapper { // Handling Minimum_Specific var i = 1 - if (trace.topLvlElementIsInInitialModel as Boolean){ + if (trace.topLvlElementIsInInitialModel as Boolean) { i = 0 } var minNum = -1 var Map startPoints = new HashMap -// 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 + for (t : config.typeScopes.minNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) { + var numIniIntModel = 0 + for (elem : trace.definedElement2String.keySet) { + for (tDefined : elem.definedInType) { + if (support.dfsSubtypeCheck(t, tDefined)) { + numIniIntModel += 1 + } + } + } + minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel if (minNum != 0) { getInstanceConstants(i + minNum, i, localInstances, trace, true, false) - startPoints.put(tConfig, i) + startPoints.put(t, i) i += minNum - makeFofFormula(localInstances, trace, true, tConfig) + makeFofFormula(localInstances, trace, true, t) } } // TODO: calc sum of mins, compare to current value of i // Handling Maximum_Specific - 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) + for (t : config.typeScopes.maxNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) { + + var numIniIntModel = 0 + for (elem : trace.definedElement2String.keySet) { + if (elem.definedInType == t) { + numIniIntModel += 1 + } + } + + var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) - numIniIntModel + if (config.typeScopes.minNewElementsByType.keySet.contains(t)) { + minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel + } else { + minNum = 0 + } + if (minNum != 0) { + var startpoint = t.lookup(startPoints) 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, tConfig) + else { + localInstances.clear } + // 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) +// } } // 3. Specify uniqueness of elements -- cgit v1.2.3-54-g00ecf