diff options
Diffstat (limited to 'Solvers/Vampire-Solver')
3 files changed, 25 insertions, 2 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 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index e85b5240..8a6f30f9 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java index f776371b..c101aa4c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java | |||
@@ -111,7 +111,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
111 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | 111 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); |
112 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 112 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
113 | _formulas.add(res); | 113 | _formulas.add(res); |
114 | final List<VLSFunction> enumScopeElems = CollectionLiterals.<VLSFunction>newArrayList(); | 114 | final List<VLSTerm> enumScopeElems = CollectionLiterals.<VLSTerm>newArrayList(); |
115 | for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { | 115 | for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { |
116 | { | 116 | { |
117 | final int num = (i + 1); | 117 | final int num = (i + 1); |
@@ -124,6 +124,17 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
124 | trace.uniqueInstances.add(cst); | 124 | trace.uniqueInstances.add(cst); |
125 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); | 125 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); |
126 | enumScopeElems.add(fct); | 126 | enumScopeElems.add(fct); |
127 | for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) { | ||
128 | if ((j != i)) { | ||
129 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm); | ||
130 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
131 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { | ||
132 | it.setOperand(op); | ||
133 | }; | ||
134 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); | ||
135 | enumScopeElems.add(negFct); | ||
136 | } | ||
137 | } | ||
127 | } | 138 | } |
128 | } | 139 | } |
129 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 140 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |