diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-24 19:54:57 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:37:06 -0400 |
commit | 06b2801cd5893ced25745d79959592f99b4ef83b (patch) | |
tree | c1b5ae4feb156332847bf0cc7c30a30f5f893d64 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | |
parent | VAMPIRE: add to #40. I am tired (diff) | |
download | VIATRA-Generator-06b2801cd5893ced25745d79959592f99b4ef83b.tar.gz VIATRA-Generator-06b2801cd5893ced25745d79959592f99b4ef83b.tar.zst VIATRA-Generator-06b2801cd5893ced25745d79959592f99b4ef83b.zip |
VAMPIRE : initial model handling almost done. only typeScope remains #40
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 | 30 |
1 files changed, 24 insertions, 6 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 2a121446..1b30393f 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 | |||
@@ -44,13 +44,31 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
44 | trace.type2Predicate.put(type, typePred) | 44 | trace.type2Predicate.put(type, typePred) |
45 | } | 45 | } |
46 | 46 | ||
47 | // 2. Map each ENUM type definition to fof formula | 47 | // 2. Map each ENUM/InitialModelElement type definition to fof formula |
48 | // This also Handles initial Model stuff | 48 | // In the case where , for example, a supertype that is abstract has a subtype of which an instance is in the initial model, |
49 | for (type : types.filter(TypeDefinition)) { | 49 | // The logic problem will contain a TypeDefinition for the subtype as well as for the supertype |
50 | // This defined elemtn for the supertype will be abstract, and we do not wish to associate a constant to it, or associate it with a type | ||
51 | // Within our vampireproblem.tptp | ||
52 | for (type : types.filter(TypeDefinition).filter[!isIsAbstract]) { | ||
53 | |||
54 | //Detect if it is a defined element (from initial model) | ||
55 | //Otherwise it is an Enum | ||
56 | |||
57 | //val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract | ||
58 | //^does not work in cases where a defined type already has a supertype from within the MM | ||
59 | |||
60 | // var isNotEnumVar = !type.supertypes.isEmpty | ||
61 | // if(isNotEnumVar) { | ||
62 | // for (sup : type.supertypes){ | ||
63 | // type.name.contains(sup.name) | ||
64 | // } | ||
65 | // } | ||
66 | // | ||
67 | // val isNotEnum = isNotEnumVar | ||
50 | 68 | ||
51 | //Detect if is an Enum | 69 | //Another possibility is.. |
52 | //Otherwise, it is a defined element (from initial model) | 70 | val len = type.name.length |
53 | val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract | 71 | val isNotEnum = !type.name.substring(len-4, len).equals("enum") |
54 | 72 | ||
55 | // Create a VLSFunction for each Enum Element | 73 | // Create a VLSFunction for each Enum Element |
56 | val List<VLSFunction> orElems = newArrayList | 74 | val List<VLSFunction> orElems = newArrayList |