diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend | 73 |
1 files changed, 48 insertions, 25 deletions
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant | 3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
7 | import java.util.List | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
8 | import java.util.ArrayList | 8 | import java.util.ArrayList |
9 | import java.util.Map | ||
9 | 10 | ||
10 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
12 | import java.util.HashMap | ||
11 | 13 | ||
12 | class Logic2VampireLanguageMapper_ScopeMapper { | 14 | class Logic2VampireLanguageMapper_ScopeMapper { |
13 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 15 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -21,9 +23,9 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
21 | 23 | ||
22 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { | 24 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { |
23 | 25 | ||
24 | // HANDLE ERRORS RELATED TO MAX > MIN | 26 | // TODO HANDLE ERRORS RELATED TO MAX > MIN |
25 | // HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS | 27 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS |
26 | // NOT SPECIFIED MEANS =0 ? | 28 | // TODO NOT SPECIFIED MEANS =0 ? |
27 | // 1. make a list of constants equaling the min number of specified objects | 29 | // 1. make a list of constants equaling the min number of specified objects |
28 | val GLOBAL_MIN = config.typeScopes.minNewElements | 30 | val GLOBAL_MIN = config.typeScopes.minNewElements |
29 | val GLOBAL_MAX = config.typeScopes.maxNewElements | 31 | val GLOBAL_MAX = config.typeScopes.maxNewElements |
@@ -32,42 +34,47 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
32 | 34 | ||
33 | // Handling Minimum_General | 35 | // Handling Minimum_General |
34 | if (GLOBAL_MIN != 0) { | 36 | if (GLOBAL_MIN != 0) { |
35 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false) // fix last param | 37 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) // fix last param |
36 | makeFofFormula(localInstances, trace, true, "object") | 38 | makeFofFormula(localInstances, trace, true, null) |
37 | } | 39 | } |
38 | 40 | ||
39 | // Handling Maximum_General | 41 | // Handling Maximum_General |
40 | if (GLOBAL_MAX != 0) { | 42 | if (GLOBAL_MAX != 0) { |
41 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true) // fix last param | 43 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) // fix last param |
42 | makeFofFormula(localInstances, trace, false, "object") | 44 | makeFofFormula(localInstances, trace, false, null) |
43 | } | 45 | } |
44 | 46 | ||
45 | // Handling Minimum_Specific | 47 | // Handling Minimum_Specific |
46 | var i = 0 | 48 | var i = 0 |
47 | var minNum = -1 | 49 | var minNum = -1 |
50 | var Map<Type, Integer> startPoints = new HashMap | ||
48 | for (t : config.typeScopes.minNewElementsByType.keySet) { | 51 | for (t : config.typeScopes.minNewElementsByType.keySet) { |
49 | minNum = t.lookup(config.typeScopes.minNewElementsByType) | 52 | minNum = t.lookup(config.typeScopes.minNewElementsByType) |
50 | if (minNum != 0) { | 53 | if (minNum != 0) { |
51 | getInstanceConstants(i+minNum, i, localInstances, trace, false) | 54 | getInstanceConstants(i + minNum, i, localInstances, trace, true, false) |
55 | startPoints.put(t, i) | ||
52 | i += minNum | 56 | i += minNum |
53 | makeFofFormula(localInstances, trace, true, t.toString)//fix last param | 57 | makeFofFormula(localInstances, trace, true, t) |
54 | } | 58 | } |
55 | } | 59 | } |
56 | 60 | ||
57 | //TODO: calc sum of mins, compare to current value of i | 61 | // TODO: calc sum of mins, compare to current value of i |
58 | |||
59 | // Handling Maximum_Specific | 62 | // Handling Maximum_Specific |
60 | for (t : config.typeScopes.maxNewElementsByType.keySet) { | 63 | for (t : config.typeScopes.maxNewElementsByType.keySet) { |
61 | var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) | 64 | var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) |
62 | minNum = t.lookup(config.typeScopes.minNewElementsByType) | 65 | minNum = t.lookup(config.typeScopes.minNewElementsByType) |
63 | if (maxNum != 0) { | 66 | var startpoint = t.lookup(startPoints) |
64 | var forLimit = Math.min(GLOBAL_MAX, i+maxNum-minNum) | 67 | if (minNum != 0) { |
65 | getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false) | 68 | getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) |
66 | makeFofFormula(localInstances, trace, false, t.toString)//fix last param | 69 | } |
70 | if (maxNum != minNum) { | ||
71 | var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum) | ||
72 | getInstanceConstants(instEndInd, i, localInstances, trace, false, false) | ||
73 | makeFofFormula(localInstances, trace, false, t) | ||
67 | } | 74 | } |
68 | } | 75 | } |
69 | 76 | ||
70 | // 3. Specify uniqueness of elements | 77 | // 3. Specify uniqueness of elements |
71 | if (trace.uniqueInstances.length != 0) { | 78 | if (trace.uniqueInstances.length != 0) { |
72 | val uniqueness = createVLSFofFormula => [ | 79 | val uniqueness = createVLSFofFormula => [ |
73 | it.name = "typeUniqueness" | 80 | it.name = "typeUniqueness" |
@@ -79,10 +86,12 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
79 | 86 | ||
80 | } | 87 | } |
81 | 88 | ||
82 | def protected void getInstanceConstants(int numElems, int init, ArrayList list, | 89 | def protected void getInstanceConstants(int endInd, int startInd, ArrayList list, |
83 | Logic2VampireLanguageMapperTrace trace, boolean addToTrace) { | 90 | Logic2VampireLanguageMapperTrace trace, boolean clear, boolean addToTrace) { |
84 | list.clear | 91 | if (clear) { |
85 | for (var i = init; i < numElems; i++) { | 92 | list.clear |
93 | } | ||
94 | for (var i = startInd; i < endInd; i++) { | ||
86 | val num = i + 1 | 95 | val num = i + 1 |
87 | val cst = createVLSConstant => [ | 96 | val cst = createVLSConstant => [ |
88 | it.name = "o" + num | 97 | it.name = "o" + num |
@@ -94,7 +103,20 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
94 | } | 103 | } |
95 | } | 104 | } |
96 | 105 | ||
97 | def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, String name) { | 106 | def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, |
107 | Type type) { | ||
108 | var nm = "" | ||
109 | var VLSFunction tm = null | ||
110 | if (type === null) { | ||
111 | nm = "object" | ||
112 | tm = support.topLevelTypeFunc | ||
113 | } else { | ||
114 | nm = type.lookup(trace.type2Predicate).constant.toString | ||
115 | tm = support.duplicate(type.lookup(trace.type2Predicate)) | ||
116 | } | ||
117 | val name = nm | ||
118 | val term = tm | ||
119 | |||
98 | val cstDec = createVLSFofFormula => [ | 120 | val cstDec = createVLSFofFormula => [ |
99 | it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name) | 121 | it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name) |
100 | it.fofRole = "axiom" | 122 | it.fofRole = "axiom" |
@@ -109,15 +131,16 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
109 | it.right = i | 131 | it.right = i |
110 | ] | 132 | ] |
111 | ]) | 133 | ]) |
112 | it.right = support.topLevelTypeFunc | 134 | it.right = term |
113 | } else { | 135 | } else { |
136 | it.left = term | ||
114 | it.right = support.unfoldOr(list.map [ i | | 137 | it.right = support.unfoldOr(list.map [ i | |
115 | createVLSEquality => [ | 138 | createVLSEquality => [ |
116 | it.left = createVLSVariable => [it.name = variable.name] | 139 | it.left = createVLSVariable => [it.name = variable.name] |
117 | it.right = i | 140 | it.right = i |
118 | ] | 141 | ] |
119 | ]) | 142 | ]) |
120 | it.left = support.topLevelTypeFunc | 143 | |
121 | } | 144 | } |
122 | ] | 145 | ] |
123 | ] | 146 | ] |