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 | |
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')
4 files changed, 71 insertions, 15 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend index 22bd4ab5..b9928383 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend | |||
@@ -30,6 +30,8 @@ class Logic2VampireLanguageMapperTrace { | |||
30 | //Necessary containers | 30 | //Necessary containers |
31 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace | 31 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace |
32 | 32 | ||
33 | public var Map<DefinedElement, String> definedElement2String = new HashMap | ||
34 | |||
33 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; | 35 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; |
34 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap | 36 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap |
35 | public val Map<Type, VLSTerm> type2PossibleNot = new HashMap | 37 | public val Map<Type, VLSTerm> type2PossibleNot = new HashMap |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index 8e0e0b11..c56b54be 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend | |||
@@ -14,10 +14,11 @@ import java.util.List | |||
14 | import java.util.Map | 14 | import java.util.Map |
15 | 15 | ||
16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
17 | 18 | ||
18 | class Logic2VampireLanguageMapper_ContainmentMapper { | 19 | class Logic2VampireLanguageMapper_ContainmentMapper { |
19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 20 | val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
20 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | 21 | val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support |
21 | val Logic2VampireLanguageMapper base | 22 | val Logic2VampireLanguageMapper base |
22 | private val VLSVariable variable = createVLSVariable => [it.name = "A"] | 23 | private val VLSVariable variable = createVLSVariable => [it.name = "A"] |
23 | 24 | ||
@@ -34,6 +35,8 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
34 | 35 | ||
35 | val containmentListCopy = hierarchy.typesOrderedInHierarchy | 36 | val containmentListCopy = hierarchy.typesOrderedInHierarchy |
36 | val relationsList = hierarchy.containmentRelations | 37 | val relationsList = hierarchy.containmentRelations |
38 | val toRemove = newArrayList | ||
39 | |||
37 | // STEP 1 | 40 | // STEP 1 |
38 | // Find root element | 41 | // Find root element |
39 | for (l : relationsList) { | 42 | for (l : relationsList) { |
@@ -46,16 +49,51 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
46 | } | 49 | } |
47 | } | 50 | } |
48 | 51 | ||
49 | for (c : containmentListCopy) { | 52 | // OLD |
50 | if(c.isIsAbstract) { | 53 | // for (c : containmentListCopy) { |
51 | containmentListCopy.remove(c) | 54 | // if(c.isIsAbstract) { |
52 | } | 55 | // toRemove.add(c) |
53 | } | 56 | // } |
54 | 57 | // } | |
55 | // State that there must exist 1 and only 1 root element | 58 | // State that there must exist 1 and only 1 root element |
56 | val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString | 59 | // val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString |
57 | val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) | 60 | // val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) |
58 | 61 | ||
62 | var topTermVar = containmentListCopy.get(0) | ||
63 | for (l : relationsList) { | ||
64 | var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type | ||
65 | if(containmentListCopy.contains(pointingFrom)) { | ||
66 | //The correct topTerm will be identified | ||
67 | topTermVar = pointingFrom | ||
68 | } | ||
69 | } | ||
70 | |||
71 | val topName = topTermVar.lookup(trace.type2Predicate).constant.toString | ||
72 | val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate)) | ||
73 | |||
74 | |||
75 | |||
76 | var topLvlIsInInitModel = false | ||
77 | var topLvlString = "" | ||
78 | for ( c : topTermVar.subtypes) { | ||
79 | if (c.class.simpleName.equals("TypeDefinitionImpl") ) { | ||
80 | |||
81 | for (d : (c as TypeDefinition).elements) { | ||
82 | if (trace.definedElement2String.containsKey(d)) { | ||
83 | topLvlIsInInitModel = true | ||
84 | topLvlString = d.lookup(trace.definedElement2String) | ||
85 | } | ||
86 | } | ||
87 | |||
88 | } | ||
89 | |||
90 | |||
91 | } | ||
92 | val topInIM = topLvlIsInInitModel | ||
93 | val topStr = topLvlString | ||
94 | print(topInIM) | ||
95 | print(topStr) | ||
96 | |||
59 | val contTop = createVLSFofFormula => [ | 97 | val contTop = createVLSFofFormula => [ |
60 | it.name = support.toIDMultiple("containment_topLevel", topName) | 98 | it.name = support.toIDMultiple("containment_topLevel", topName) |
61 | it.fofRole = "axiom" | 99 | it.fofRole = "axiom" |
@@ -67,7 +105,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
67 | it.right = createVLSEquality => [ | 105 | it.right = createVLSEquality => [ |
68 | it.left = support.duplicate(variable) | 106 | it.left = support.duplicate(variable) |
69 | it.right = createVLSConstant => [ | 107 | it.right = createVLSConstant => [ |
70 | it.name = "o1" | 108 | it.name = if (topInIM) topStr else "o1" |
71 | ] | 109 | ] |
72 | ] | 110 | ] |
73 | ] | 111 | ] |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index 4a8d2827..c50aa770 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend | |||
@@ -30,6 +30,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
30 | // TODO HANDLE | 30 | // TODO HANDLE |
31 | // 1. make a list of constants equaling the min number of specified objects | 31 | // 1. make a list of constants equaling the min number of specified objects |
32 | //These numbers do not include enums or initial model elements | 32 | //These numbers do not include enums or initial model elements |
33 | |||
33 | val GLOBAL_MIN = config.typeScopes.minNewElements | 34 | val GLOBAL_MIN = config.typeScopes.minNewElements |
34 | val GLOBAL_MAX = config.typeScopes.maxNewElements | 35 | val GLOBAL_MAX = config.typeScopes.maxNewElements |
35 | 36 | ||
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 => [ |