From 04b59e1e638c19149eb27bcaec31c6fd9a9bbb84 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 13 Mar 2019 19:08:37 -0400 Subject: Implement type scope for specific types --- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 73 ++++++++++++++-------- 1 file changed, 48 insertions(+), 25 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder') 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 2da4cfd7..5c5eaff3 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 @@ -1,13 +1,15 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration -import java.util.List +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import java.util.ArrayList +import java.util.Map import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import java.util.HashMap class Logic2VampireLanguageMapper_ScopeMapper { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -21,9 +23,9 @@ class Logic2VampireLanguageMapper_ScopeMapper { def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { -// HANDLE ERRORS RELATED TO MAX > MIN -// HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS -// NOT SPECIFIED MEANS =0 ? +// TODO HANDLE ERRORS RELATED TO MAX > MIN +// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS +// TODO NOT SPECIFIED MEANS =0 ? // 1. make a list of constants equaling the min number of specified objects val GLOBAL_MIN = config.typeScopes.minNewElements val GLOBAL_MAX = config.typeScopes.maxNewElements @@ -32,42 +34,47 @@ class Logic2VampireLanguageMapper_ScopeMapper { // Handling Minimum_General if (GLOBAL_MIN != 0) { - getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false) // fix last param - makeFofFormula(localInstances, trace, true, "object") + getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) // fix last param + makeFofFormula(localInstances, trace, true, null) } // Handling Maximum_General if (GLOBAL_MAX != 0) { - getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true) // fix last param - makeFofFormula(localInstances, trace, false, "object") + getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) // fix last param + makeFofFormula(localInstances, trace, false, null) } // Handling Minimum_Specific var i = 0 var minNum = -1 + var Map startPoints = new HashMap for (t : config.typeScopes.minNewElementsByType.keySet) { minNum = t.lookup(config.typeScopes.minNewElementsByType) if (minNum != 0) { - getInstanceConstants(i+minNum, i, localInstances, trace, false) + getInstanceConstants(i + minNum, i, localInstances, trace, true, false) + startPoints.put(t, i) i += minNum - makeFofFormula(localInstances, trace, true, t.toString)//fix last param + makeFofFormula(localInstances, trace, true, t) } } - //TODO: calc sum of mins, compare to current value of i - + // 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) - if (maxNum != 0) { - var forLimit = Math.min(GLOBAL_MAX, i+maxNum-minNum) - getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false) - makeFofFormula(localInstances, trace, false, t.toString)//fix last param + var startpoint = t.lookup(startPoints) + if (minNum != 0) { + getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) + } + 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 +// 3. Specify uniqueness of elements if (trace.uniqueInstances.length != 0) { val uniqueness = createVLSFofFormula => [ it.name = "typeUniqueness" @@ -79,10 +86,12 @@ class Logic2VampireLanguageMapper_ScopeMapper { } - def protected void getInstanceConstants(int numElems, int init, ArrayList list, - Logic2VampireLanguageMapperTrace trace, boolean addToTrace) { - list.clear - for (var i = init; i < numElems; i++) { + def protected void getInstanceConstants(int endInd, int startInd, ArrayList list, + Logic2VampireLanguageMapperTrace trace, boolean clear, boolean addToTrace) { + if (clear) { + list.clear + } + for (var i = startInd; i < endInd; i++) { val num = i + 1 val cst = createVLSConstant => [ it.name = "o" + num @@ -94,7 +103,20 @@ class Logic2VampireLanguageMapper_ScopeMapper { } } - def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, String name) { + def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, + Type type) { + var nm = "" + var VLSFunction tm = null + if (type === null) { + nm = "object" + tm = support.topLevelTypeFunc + } else { + nm = type.lookup(trace.type2Predicate).constant.toString + tm = support.duplicate(type.lookup(trace.type2Predicate)) + } + val name = nm + val term = tm + val cstDec = createVLSFofFormula => [ it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name) it.fofRole = "axiom" @@ -109,15 +131,16 @@ class Logic2VampireLanguageMapper_ScopeMapper { it.right = i ] ]) - it.right = support.topLevelTypeFunc + it.right = term } else { + it.left = term it.right = support.unfoldOr(list.map [ i | createVLSEquality => [ it.left = createVLSVariable => [it.name = variable.name] it.right = i ] ]) - it.left = support.topLevelTypeFunc + } ] ] -- cgit v1.2.3-54-g00ecf