diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend')
| -rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend | 48 |
1 files changed, 27 insertions, 21 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 5e8819a6..741389bb 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 | |||
| @@ -93,30 +93,36 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
| 93 | } | 93 | } |
| 94 | 94 | ||
| 95 | // 3. Specify uniqueness of elements | 95 | // 3. Specify uniqueness of elements |
| 96 | // TEMP | ||
| 97 | val DUPLICATES = true | ||
| 98 | |||
| 96 | val numInst = trace.uniqueInstances.length | 99 | val numInst = trace.uniqueInstances.length |
| 97 | var ind = 1 | 100 | var ind = 1 |
| 98 | if (numInst != 0) { | 101 | if (numInst != 0) { |
| 99 | /* | 102 | if (DUPLICATES) { |
| 100 | * // SHORTER | 103 | // W/ DUPLICATES |
| 101 | * for (e : trace.uniqueInstances.subList(0, numInst-1)) { | 104 | for (e : trace.uniqueInstances) { |
| 102 | /*/ | 105 | val x = ind |
| 103 | // LONGER | 106 | val uniqueness = createVLSFofFormula => [ |
| 104 | for (e : trace.uniqueInstances) { | 107 | it.name = support.toIDMultiple("t_uniqueness", e.name) |
| 105 | // */ | 108 | it.fofRole = "axiom" |
| 106 | val x = ind | 109 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) |
| 107 | val uniqueness = createVLSFofFormula => [ | 110 | ] |
| 108 | it.name = support.toIDMultiple("t_uniqueness", e.name) | 111 | trace.specification.formulas += uniqueness |
| 109 | it.fofRole = "axiom" | 112 | ind++ |
| 110 | /* | 113 | } |
| 111 | * // SHORTER | 114 | } else { |
| 112 | * it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e) | 115 | // W/O DUPLICATES |
| 113 | /*/ | 116 | for (e : trace.uniqueInstances.subList(0, numInst - 1)) { |
| 114 | // LONGER | 117 | val x = ind |
| 115 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) | 118 | val uniqueness = createVLSFofFormula => [ |
| 116 | // */ | 119 | it.name = support.toIDMultiple("t_uniqueness", e.name) |
| 117 | ] | 120 | it.fofRole = "axiom" |
| 118 | trace.specification.formulas += uniqueness | 121 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e) |
| 119 | ind++ | 122 | ] |
| 123 | trace.specification.formulas += uniqueness | ||
| 124 | ind++ | ||
| 125 | } | ||
| 120 | } | 126 | } |
| 121 | } | 127 | } |
| 122 | } | 128 | } |