diff options
author | 2019-04-04 20:08:30 -0400 | |
---|---|---|
committer | 2019-04-04 20:08:30 -0400 | |
commit | e8ec04bff69e414b0f1b67c060d235a844c0018b (patch) | |
tree | c49d4969e9a024045361a4eb1034dc6c43c8725f /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner | |
parent | Facilitate #31, close #36 (diff) | |
download | VIATRA-Generator-e8ec04bff69e414b0f1b67c060d235a844c0018b.tar.gz VIATRA-Generator-e8ec04bff69e414b0f1b67c060d235a844c0018b.tar.zst VIATRA-Generator-e8ec04bff69e414b0f1b67c060d235a844c0018b.zip |
Add small detail to #36
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner')
-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 | } |