diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | 28 |
1 files changed, 8 insertions, 20 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 ee6365dd..e12180fa 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 | |||
@@ -48,7 +48,13 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
48 | val List<VLSFunction> orElems = newArrayList | 48 | val List<VLSFunction> orElems = newArrayList |
49 | for (e : type.elements) { | 49 | for (e : type.elements) { |
50 | val enumElemPred = createVLSFunction => [ | 50 | val enumElemPred = createVLSFunction => [ |
51 | it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2)) | 51 | val splitName = e.name.split(" ") |
52 | if( splitName.length > 2) { | ||
53 | it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) | ||
54 | } | ||
55 | else { | ||
56 | it.constant = support.toIDMultiple("e", splitName.get(0)) | ||
57 | } | ||
52 | it.terms += support.duplicate(variable) | 58 | it.terms += support.duplicate(variable) |
53 | ] | 59 | ] |
54 | // typeTrace.element2Predicate.put(e, enumElemPred) | 60 | // typeTrace.element2Predicate.put(e, enumElemPred) |
@@ -63,26 +69,8 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
63 | it.fofFormula = createVLSUniversalQuantifier => [ | 69 | it.fofFormula = createVLSUniversalQuantifier => [ |
64 | it.variables += support.duplicate(variable) | 70 | it.variables += support.duplicate(variable) |
65 | it.operand = createVLSEquivalent => [ | 71 | it.operand = createVLSEquivalent => [ |
66 | // it.left = createVLSFunction => [ | ||
67 | // it.constant = type.lookup(typeTrace.type2Predicate).constant | ||
68 | // it.terms += createVLSVariable => [it.name = "A"] | ||
69 | // ] | ||
70 | // it.left = type.lookup(typeTrace.type2Predicate) | ||
71 | it.left = type.lookup(trace.type2Predicate) | 72 | it.left = type.lookup(trace.type2Predicate) |
72 | |||
73 | it.right = support.unfoldOr(orElems) | 73 | it.right = support.unfoldOr(orElems) |
74 | |||
75 | // TEMPPPPPPP | ||
76 | // it.right = support.unfoldOr(type.elements.map [e | | ||
77 | // | ||
78 | // createVLSEquality => [ | ||
79 | // it.left = support.duplicate(variable) | ||
80 | // it.right = createVLSDoubleQuote => [ | ||
81 | // it.value = "\"a" + e.name + "\"" | ||
82 | // ] | ||
83 | // ] | ||
84 | // ]) | ||
85 | // END TEMPPPPP | ||
86 | ] | 74 | ] |
87 | ] | 75 | ] |
88 | 76 | ||
@@ -152,7 +140,7 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
152 | 140 | ||
153 | // 5. create fof function that is an or with all the elements in map | 141 | // 5. create fof function that is an or with all the elements in map |
154 | val hierarch = createVLSFofFormula => [ | 142 | val hierarch = createVLSFofFormula => [ |
155 | it.name = "hierarchyHandler" | 143 | it.name = "inheritanceHierarchyHandler" |
156 | it.fofRole = "axiom" | 144 | it.fofRole = "axiom" |
157 | it.fofFormula = createVLSUniversalQuantifier => [ | 145 | it.fofFormula = createVLSUniversalQuantifier => [ |
158 | it.variables += support.duplicate(variable) | 146 | it.variables += support.duplicate(variable) |