diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-04 14:43:17 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-04 14:43:17 -0400 |
commit | 4d01994940121fc255bd242358b5135a27e8dce5 (patch) | |
tree | 18fcfee794766df322e46898c03c7246a8eed6d9 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |
parent | Add to containment, add notObject case. (diff) | |
download | VIATRA-Generator-4d01994940121fc255bd242358b5135a27e8dce5.tar.gz VIATRA-Generator-4d01994940121fc255bd242358b5135a27e8dce5.tar.zst VIATRA-Generator-4d01994940121fc255bd242358b5135a27e8dce5.zip |
Closes #34, adds code to test cases where minScope>maxScope.
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 | 6 |
1 files changed, 4 insertions, 2 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 7aca7633..d40b0dd2 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,17 +47,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
47 | } | 47 | } |
48 | 48 | ||
49 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 49 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
50 | final int ABSOLUTE_MIN = 0; | ||
51 | final int ABSOLUTE_MAX = Integer.MAX_VALUE; | ||
50 | final int GLOBAL_MIN = config.typeScopes.minNewElements; | 52 | final int GLOBAL_MIN = config.typeScopes.minNewElements; |
51 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | 53 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; |
52 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); | 54 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); |
53 | if ((GLOBAL_MIN != 0)) { | 55 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { |
54 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); | 56 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); |
55 | for (final VLSConstant i : trace.uniqueInstances) { | 57 | for (final VLSConstant i : trace.uniqueInstances) { |
56 | localInstances.add(this.support.duplicate(i)); | 58 | localInstances.add(this.support.duplicate(i)); |
57 | } | 59 | } |
58 | this.makeFofFormula(localInstances, trace, true, null); | 60 | this.makeFofFormula(localInstances, trace, true, null); |
59 | } | 61 | } |
60 | if ((GLOBAL_MAX != 0)) { | 62 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { |
61 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); | 63 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); |
62 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); | 64 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); |
63 | } | 65 | } |