diff options
author | 2019-03-06 17:46:15 -0500 | |
---|---|---|
committer | 2019-03-06 17:46:15 -0500 | |
commit | 1cdcfeeda9f2d35655ffec9fca9f64f92101ce53 (patch) | |
tree | 38d5bab4cda0e8abdcba071fbd81259c1bbd07ae /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner | |
parent | Implement Enum handling and study hierarchy handling (diff) | |
download | VIATRA-Generator-1cdcfeeda9f2d35655ffec9fca9f64f92101ce53.tar.gz VIATRA-Generator-1cdcfeeda9f2d35655ffec9fca9f64f92101ce53.tar.zst VIATRA-Generator-1cdcfeeda9f2d35655ffec9fca9f64f92101ce53.zip |
Fix Enum handling for Paradox Integration
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_TypeMapper.xtend | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index f2a7b3f2..ee6365dd 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | |||
@@ -90,7 +90,7 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
90 | trace.specification.formulas += res | 90 | trace.specification.formulas += res |
91 | 91 | ||
92 | // Create objects for the enum elements | 92 | // Create objects for the enum elements |
93 | val List<VLSFunction> enumScopeElems = newArrayList | 93 | val List<VLSTerm> enumScopeElems = newArrayList |
94 | for (var i = 0; i < type.elements.length; i++) { | 94 | for (var i = 0; i < type.elements.length; i++) { |
95 | val num = i + 1 | 95 | val num = i + 1 |
96 | val cstTerm = createVLSFunctionAsTerm => [ | 96 | val cstTerm = createVLSFunctionAsTerm => [ |
@@ -100,6 +100,18 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
100 | trace.uniqueInstances.add(cst) | 100 | trace.uniqueInstances.add(cst) |
101 | val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm) | 101 | val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm) |
102 | enumScopeElems.add(fct) | 102 | enumScopeElems.add(fct) |
103 | |||
104 | //For paradox Only | ||
105 | for (var j = 0; j < type.elements.length; j++) { | ||
106 | if(j != i) { | ||
107 | val op = support.duplicate(type.elements.get(j).lookup(trace.element2Predicate), cstTerm) | ||
108 | val negFct = createVLSUnaryNegation => [ | ||
109 | it.operand = op | ||
110 | ] | ||
111 | enumScopeElems.add(negFct) | ||
112 | } | ||
113 | } | ||
114 | //End Paradox | ||
103 | // enumScopeElems.add(support.topLevelTypeFunc(cstTerm)) | 115 | // enumScopeElems.add(support.topLevelTypeFunc(cstTerm)) |
104 | } | 116 | } |
105 | 117 | ||