diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | 32 |
1 files changed, 18 insertions, 14 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index f5d35b28..bf7b70d0 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |||
@@ -47,11 +47,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
47 | this.base = base; | 47 | this.base = base; |
48 | } | 48 | } |
49 | 49 | ||
50 | public void _transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 50 | public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
51 | final int ABSOLUTE_MIN = 0; | 51 | final int ABSOLUTE_MIN = 0; |
52 | final int ABSOLUTE_MAX = Integer.MAX_VALUE; | 52 | final int ABSOLUTE_MAX = Integer.MAX_VALUE; |
53 | final int GLOBAL_MIN = config.typeScopes.minNewElements; | 53 | int elemsInIM = trace.definedElement2String.size(); |
54 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | 54 | final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); |
55 | final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); | ||
55 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); | 56 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); |
56 | final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); | 57 | final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); |
57 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { | 58 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { |
@@ -74,34 +75,37 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
74 | } | 75 | } |
75 | } | 76 | } |
76 | int i_1 = 1; | 77 | int i_1 = 1; |
78 | if ((((Boolean) trace.topLvlElementIsInInitialModel)).booleanValue()) { | ||
79 | i_1 = 0; | ||
80 | } | ||
77 | int minNum = (-1); | 81 | int minNum = (-1); |
78 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); | 82 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); |
79 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); | 83 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); |
80 | for (final Type t : _keySet) { | 84 | for (final Type tConfig : _keySet) { |
81 | { | 85 | { |
82 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); | 86 | minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig, config.typeScopes.minNewElementsByType)).intValue(); |
83 | if ((minNum != 0)) { | 87 | if ((minNum != 0)) { |
84 | this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); | 88 | this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); |
85 | startPoints.put(t, Integer.valueOf(i_1)); | 89 | startPoints.put(tConfig, Integer.valueOf(i_1)); |
86 | int _i = i_1; | 90 | int _i = i_1; |
87 | i_1 = (_i + minNum); | 91 | i_1 = (_i + minNum); |
88 | this.makeFofFormula(localInstances, trace, true, t); | 92 | this.makeFofFormula(localInstances, trace, true, tConfig); |
89 | } | 93 | } |
90 | } | 94 | } |
91 | } | 95 | } |
92 | Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); | 96 | Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); |
93 | for (final Type t_1 : _keySet_1) { | 97 | for (final Type tConfig_1 : _keySet_1) { |
94 | { | 98 | { |
95 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); | 99 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.maxNewElementsByType); |
96 | minNum = (CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); | 100 | minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.minNewElementsByType)).intValue(); |
97 | Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints); | 101 | Integer startpoint = CollectionsUtil.<Type, Integer>lookup(tConfig_1, startPoints); |
98 | if ((minNum != 0)) { | 102 | if ((minNum != 0)) { |
99 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); | 103 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); |
100 | } | 104 | } |
101 | if (((maxNum).intValue() != minNum)) { | 105 | if (((maxNum).intValue() != minNum)) { |
102 | int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); | 106 | int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); |
103 | this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); | 107 | this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); |
104 | this.makeFofFormula(localInstances, trace, false, t_1); | 108 | this.makeFofFormula(localInstances, trace, false, tConfig_1); |
105 | } | 109 | } |
106 | } | 110 | } |
107 | } | 111 | } |
@@ -246,8 +250,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
246 | _formulas.add(cstDec); | 250 | _formulas.add(cstDec); |
247 | } | 251 | } |
248 | 252 | ||
249 | public void transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 253 | public void transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
250 | _transformScope(config, trace); | 254 | _transformScope(types, config, trace); |
251 | return; | 255 | return; |
252 | } | 256 | } |
253 | } | 257 | } |