diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-24 02:30:50 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:37:01 -0400 |
commit | 13cb6b35e97b79e8e4f415becf916dfaafc5d315 (patch) | |
tree | c628f428133a3d24eb9c1456eb00ab19d5797b4d /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | |
parent | VAMPIRE: close #22, improve test structure for #39, .vql file trouble (diff) | |
download | VIATRA-Generator-13cb6b35e97b79e8e4f415becf916dfaafc5d315.tar.gz VIATRA-Generator-13cb6b35e97b79e8e4f415becf916dfaafc5d315.tar.zst VIATRA-Generator-13cb6b35e97b79e8e4f415becf916dfaafc5d315.zip |
VAMPIRE: add to #40. I am tired
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 | 23 |
1 files changed, 19 insertions, 4 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 2f3af593..2a121446 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 | |||
@@ -33,14 +33,24 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
33 | // 1. Each type (class) is a predicate with a single variable as input | 33 | // 1. Each type (class) is a predicate with a single variable as input |
34 | for (type : types) { | 34 | for (type : types) { |
35 | val typePred = createVLSFunction => [ | 35 | val typePred = createVLSFunction => [ |
36 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) | 36 | if(type.name.split(" ").length == 3) { |
37 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0), type.name.split(" ").get(2)) | ||
38 | } | ||
39 | else { | ||
40 | it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) | ||
41 | } | ||
37 | it.terms += support.duplicate(variable) | 42 | it.terms += support.duplicate(variable) |
38 | ] | 43 | ] |
39 | trace.type2Predicate.put(type, typePred) | 44 | trace.type2Predicate.put(type, typePred) |
40 | } | 45 | } |
41 | 46 | ||
42 | // 2. Map each ENUM type definition to fof formula | 47 | // 2. Map each ENUM type definition to fof formula |
48 | // This also Handles initial Model stuff | ||
43 | for (type : types.filter(TypeDefinition)) { | 49 | for (type : types.filter(TypeDefinition)) { |
50 | |||
51 | //Detect if is an Enum | ||
52 | //Otherwise, it is a defined element (from initial model) | ||
53 | val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract | ||
44 | 54 | ||
45 | // Create a VLSFunction for each Enum Element | 55 | // Create a VLSFunction for each Enum Element |
46 | val List<VLSFunction> orElems = newArrayList | 56 | val List<VLSFunction> orElems = newArrayList |
@@ -104,15 +114,20 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
104 | for (var i = globalCounter; i < globalCounter + type.elements.length; i++) { | 114 | for (var i = globalCounter; i < globalCounter + type.elements.length; i++) { |
105 | // Create objects for the enum elements | 115 | // Create objects for the enum elements |
106 | val num = i + 1 | 116 | val num = i + 1 |
117 | val index = i-globalCounter | ||
118 | |||
107 | val cstTerm = createVLSFunctionAsTerm => [ | 119 | val cstTerm = createVLSFunctionAsTerm => [ |
108 | it.functor = "eo" + num | 120 | it.functor = "eo" + num |
109 | ] | 121 | ] |
122 | if (isNotEnum) { | ||
123 | trace.definedElement2String.put(type.elements.get(index),cstTerm.functor) | ||
124 | } | ||
125 | |||
110 | val cst = support.toConstant(cstTerm) | 126 | val cst = support.toConstant(cstTerm) |
111 | trace.uniqueInstances.add(cst) | 127 | trace.uniqueInstances.add(cst) |
112 | 128 | ||
113 | val index = i-globalCounter | ||
114 | val enumScope = createVLSFofFormula => [ | 129 | val enumScope = createVLSFofFormula => [ |
115 | it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString, | 130 | it.name = support.toIDMultiple(if(isNotEnum) "definedType" else "enumScope", type.lookup(trace.type2Predicate).constant.toString, |
116 | type.elements.get(index).name.split(" ").get(0)) | 131 | type.elements.get(index).name.split(" ").get(0)) |
117 | it.fofRole = "axiom" | 132 | it.fofRole = "axiom" |
118 | it.fofFormula = createVLSUniversalQuantifier => [ | 133 | it.fofFormula = createVLSUniversalQuantifier => [ |