aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-03-14 03:45:46 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2020-06-07 19:22:51 -0400
commitd7730cb0d684d6324622021a310d9b4a53e7531c (patch)
treeb631b8c666448b948bdf670fbf5ad7c2277496dd /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill
parentImplement type scope for specific types (diff)
downloadVIATRA-Generator-d7730cb0d684d6324622021a310d9b4a53e7531c.tar.gz
VIATRA-Generator-d7730cb0d684d6324622021a310d9b4a53e7531c.tar.zst
VIATRA-Generator-d7730cb0d684d6324622021a310d9b4a53e7531c.zip
Implement Containment mapping (partially) and revisit enum mapping
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend16
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend123
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend25
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend30
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend104
5 files changed, 233 insertions, 65 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index 1dbc0055..b7ad8f3d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -47,6 +47,8 @@ class Logic2VampireLanguageMapper {
47 private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support; 47 private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support;
48 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper( 48 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(
49 this) 49 this)
50 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(
51 this)
50 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( 52 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(
51 this) 53 this)
52 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper( 54 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(
@@ -80,24 +82,26 @@ class Logic2VampireLanguageMapper {
80 // SCOPE MAPPER 82 // SCOPE MAPPER
81 scopeMapper.transformScope(config, trace) 83 scopeMapper.transformScope(config, trace)
82 84
83 trace.constantDefinitions = problem.collectConstantDefinitions 85 // RELATION MAPPER
84 trace.relationDefinitions = problem.collectRelationDefinitions 86 trace.relationDefinitions = problem.collectRelationDefinitions
85
86 problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] 87 problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
88
89 // CONTAINMENT MAPPER
90 containmentMapper.transformContainment(problem.containmentHierarchies, trace)
87 91
92 // CONSTANT MAPPER
88 // only transforms definitions 93 // only transforms definitions
94 trace.constantDefinitions = problem.collectConstantDefinitions
89 // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)] 95 // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)]
90 problem.constants.filter(ConstantDefinition).forEach [ 96 problem.constants.filter(ConstantDefinition).forEach [
91 this.constantMapper.transformConstantDefinitionSpecification(it, trace) 97 this.constantMapper.transformConstantDefinitionSpecification(it, trace)
92 ] 98 ]
93 99
94 // ////////////////// 100 // ASSERTION MAPPER
95 // Transform Assertions
96 // //////////////////
97 for (assertion : problem.assertions) { 101 for (assertion : problem.assertions) {
98 transformAssertion(assertion, trace) 102 transformAssertion(assertion, trace)
99 } 103 }
100 104 // OUTPUT
101 return new TracedOutput(specification, trace) 105 return new TracedOutput(specification, trace)
102 } 106 }
103 107
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
new file mode 100644
index 00000000..0820f47d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
@@ -0,0 +1,123 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
2
3import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
4import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
6import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
7import java.util.List
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
10
11import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
14
15class Logic2VampireLanguageMapper_ContainmentMapper {
16 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
17 private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
18 val Logic2VampireLanguageMapper base
19 private val VLSVariable variable = createVLSVariable => [it.name = "A"]
20
21 public new(Logic2VampireLanguageMapper base) {
22 this.base = base
23 }
24
25 def public void transformContainment(List<ContainmentHierarchy> hierarchies,
26 Logic2VampireLanguageMapperTrace trace) {
27
28 // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST
29 // TEMP
30 val hierarchy = hierarchies.get(0)
31
32 val containmentListCopy = hierarchy.typesOrderedInHierarchy
33 val relationsList = hierarchy.containmentRelations
34 // STEP 1
35 // Find root element
36 for (l : relationsList) {
37 var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
38 containmentListCopy.remove(pointingTo)
39 for (c : pointingTo.subtypes) {
40 containmentListCopy.remove(c)
41 }
42 }
43
44 // State that there must exist 1 and only 1 root element
45 val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString
46 val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))
47
48 val contTop = createVLSFofFormula => [
49 it.name = support.toIDMultiple("containment_topLevel", topName)
50 it.fofRole = "axiom"
51
52 it.fofFormula = createVLSUniversalQuantifier => [
53 it.variables += support.duplicate(variable)
54 it.operand = createVLSEquivalent => [
55 it.left = topTerm
56 it.right = createVLSEquality => [
57 it.left = support.duplicate(variable)
58 it.right = createVLSConstant => [
59 it.name = "o1"
60 ]
61 ]
62 ]
63 ]
64// it.fofFormula = support.duplicate(
65// topTerm,
66// createVLSFunctionAsTerm => [
67// it.functor = "o1"
68// ]
69// )
70 ]
71 trace.specification.formulas += contTop
72
73 // STEP 2
74 // for each edge, if the pointedTo element exists,the edge must exist also
75 val varA = createVLSVariable => [it.name = "A"]
76 val varB = createVLSVariable => [it.name = "B"]
77 val varList = newArrayList(varB, varA)
78
79 for (l : relationsList) {
80 val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString
81 val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type
82 val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type
83
84 val relFormula = createVLSFofFormula => [
85 it.name = support.toIDMultiple("containment", relName)
86 it.fofRole = "axiom"
87
88 it.fofFormula = createVLSUniversalQuantifier => [
89 it.variables += support.duplicate(varA)
90 it.operand = createVLSImplies => [
91 it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA)
92 it.right = createVLSExistentialQuantifier => [
93 it.variables += support.duplicate(varB)
94 it.operand = createVLSAnd => [
95 it.left = support.duplicate(fromType.lookup(trace.type2Predicate), varB)
96 it.right = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate),
97 varList)
98 ]
99 ]
100
101 createVLSEquality => [
102 it.left = support.duplicate(variable)
103 it.right = createVLSConstant => [
104 it.name = "o1"
105 ]
106 ]
107 ]
108 ]
109 ]
110 trace.specification.formulas += relFormula
111 var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
112 containmentListCopy.remove(pointingTo)
113 for (c : pointingTo.subtypes) {
114 containmentListCopy.remove(c)
115 }
116 }
117
118 // STEP 3
119 // Ensure that an objct only has 1 parent
120 // STEP 4
121 // Ensure that there are no cycles in the hierarchy (maybe same as for step3?)
122 }
123}
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 5c5eaff3..548deda4 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
@@ -10,6 +10,8 @@ import java.util.Map
10 10
11import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 11import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
12import java.util.HashMap 12import java.util.HashMap
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
14import java.util.List
13 15
14class Logic2VampireLanguageMapper_ScopeMapper { 16class Logic2VampireLanguageMapper_ScopeMapper {
15 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE 17 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -24,7 +26,8 @@ class Logic2VampireLanguageMapper_ScopeMapper {
24 def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { 26 def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
25 27
26// TODO HANDLE ERRORS RELATED TO MAX > MIN 28// TODO HANDLE ERRORS RELATED TO MAX > MIN
27// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS 29// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS
30// TODO HANDLE
28// TODO NOT SPECIFIED MEANS =0 ? 31// TODO NOT SPECIFIED MEANS =0 ?
29 // 1. make a list of constants equaling the min number of specified objects 32 // 1. make a list of constants equaling the min number of specified objects
30 val GLOBAL_MIN = config.typeScopes.minNewElements 33 val GLOBAL_MIN = config.typeScopes.minNewElements
@@ -34,18 +37,22 @@ class Logic2VampireLanguageMapper_ScopeMapper {
34 37
35 // Handling Minimum_General 38 // Handling Minimum_General
36 if (GLOBAL_MIN != 0) { 39 if (GLOBAL_MIN != 0) {
37 getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) // fix last param 40 getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false)
41 for(i : trace.uniqueInstances){
42 localInstances.add(support.duplicate(i))
43 }
44
38 makeFofFormula(localInstances, trace, true, null) 45 makeFofFormula(localInstances, trace, true, null)
39 } 46 }
40 47
41 // Handling Maximum_General 48 // Handling Maximum_General
42 if (GLOBAL_MAX != 0) { 49 if (GLOBAL_MAX != 0) {
43 getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) // fix last param 50 getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true)
44 makeFofFormula(localInstances, trace, false, null) 51 makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)
45 } 52 }
46 53
47 // Handling Minimum_Specific 54 // Handling Minimum_Specific
48 var i = 0 55 var i = 1
49 var minNum = -1 56 var minNum = -1
50 var Map<Type, Integer> startPoints = new HashMap 57 var Map<Type, Integer> startPoints = new HashMap
51 for (t : config.typeScopes.minNewElementsByType.keySet) { 58 for (t : config.typeScopes.minNewElementsByType.keySet) {
@@ -106,13 +113,17 @@ class Logic2VampireLanguageMapper_ScopeMapper {
106 def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, 113 def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum,
107 Type type) { 114 Type type) {
108 var nm = "" 115 var nm = ""
109 var VLSFunction tm = null 116 var VLSTerm tm = null
110 if (type === null) { 117 if (type === null) {
111 nm = "object" 118 nm = "object"
112 tm = support.topLevelTypeFunc 119 tm = support.topLevelTypeFunc
113 } else { 120 } else {
114 nm = type.lookup(trace.type2Predicate).constant.toString 121 nm = type.lookup(trace.type2Predicate).constant.toString
115 tm = support.duplicate(type.lookup(trace.type2Predicate)) 122 tm = createVLSAnd => [
123 it.left = support.duplicate(type.lookup(trace.type2Predicate))
124 it.right = support.topLevelTypeFunc
125 ]
126// tm = support.duplicate(type.lookup(trace.type2Predicate))
116 } 127 }
117 val name = nm 128 val name = nm
118 val term = tm 129 val term = tm
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index 021cb0ea..8d00d3e7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -37,11 +37,11 @@ class Logic2VampireLanguageMapper_Support {
37 def protected VLSVariable duplicate(VLSVariable term) { 37 def protected VLSVariable duplicate(VLSVariable term) {
38 return createVLSVariable => [it.name = term.name] 38 return createVLSVariable => [it.name = term.name]
39 } 39 }
40 40
41 def protected VLSFunctionAsTerm duplicate(VLSFunctionAsTerm term) { 41 def protected VLSFunctionAsTerm duplicate(VLSFunctionAsTerm term) {
42 return createVLSFunctionAsTerm => [it.functor = term.functor] 42 return createVLSFunctionAsTerm => [it.functor = term.functor]
43 } 43 }
44 44
45 def protected VLSConstant duplicate(VLSConstant term) { 45 def protected VLSConstant duplicate(VLSConstant term) {
46 return createVLSConstant => [it.name = term.name] 46 return createVLSConstant => [it.name = term.name]
47 } 47 }
@@ -61,14 +61,23 @@ class Logic2VampireLanguageMapper_Support {
61 it.terms += duplicate(v) 61 it.terms += duplicate(v)
62 ] 62 ]
63 } 63 }
64 64
65 def protected VLSFunction duplicate(VLSFunction term, List<VLSVariable> vars) {
66 return createVLSFunction => [
67 it.constant = term.constant
68 for (v : vars) {
69 it.terms += duplicate(v)
70 }
71 ]
72 }
73
65 def protected VLSFunction duplicate(VLSFunction term, VLSFunctionAsTerm v) { 74 def protected VLSFunction duplicate(VLSFunction term, VLSFunctionAsTerm v) {
66 return createVLSFunction => [ 75 return createVLSFunction => [
67 it.constant = term.constant 76 it.constant = term.constant
68 it.terms += duplicate(v) 77 it.terms += duplicate(v)
69 ] 78 ]
70 } 79 }
71 80
72 def protected VLSConstant toConstant(VLSFunctionAsTerm term) { 81 def protected VLSConstant toConstant(VLSFunctionAsTerm term) {
73 return createVLSConstant => [ 82 return createVLSConstant => [
74 it.name = term.functor 83 it.name = term.functor
@@ -84,6 +93,13 @@ class Logic2VampireLanguageMapper_Support {
84 ] 93 ]
85 } 94 }
86 95
96 def protected VLSFunction topLevelTypeFunc(VLSVariable v) {
97 return createVLSFunction => [
98 it.constant = "object"
99 it.terms += duplicate(v)
100 ]
101 }
102
87 def protected VLSFunction topLevelTypeFunc(VLSFunctionAsTerm v) { 103 def protected VLSFunction topLevelTypeFunc(VLSFunctionAsTerm v) {
88 return createVLSFunction => [ 104 return createVLSFunction => [
89 it.constant = "object" 105 it.constant = "object"
@@ -173,14 +189,16 @@ class Logic2VampireLanguageMapper_Support {
173 */ 189 */
174 // QUANTIFIERS + VARIABLES 190 // QUANTIFIERS + VARIABLES
175 def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, 191 def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper,
176 QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables, boolean isUniversal) { 192 QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables,
193 boolean isUniversal) {
177 val variableMap = expression.quantifiedVariables.toInvertedMap [ v | 194 val variableMap = expression.quantifiedVariables.toInvertedMap [ v |
178 createVLSVariable => [it.name = toIDMultiple("V", v.name)] 195 createVLSVariable => [it.name = toIDMultiple("V", v.name)]
179 ] 196 ]
180 197
181 val typedefs = new ArrayList<VLSTerm> 198 val typedefs = new ArrayList<VLSTerm>
182 for (variable : expression.quantifiedVariables) { 199 for (variable : expression.quantifiedVariables) {
183 val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), variable.lookup(variableMap)) 200 val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate),
201 variable.lookup(variableMap))
184 typedefs.add(eq) 202 typedefs.add(eq)
185 } 203 }
186 if (isUniversal) { 204 if (isUniversal) {
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 e12180fa..4c4247ce 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
@@ -1,12 +1,12 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder 1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
2 2
3import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd
3import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction 4import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
4import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm 5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable 6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory 7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement 8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition 10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
11import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage 11import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
12import java.util.ArrayList 12import java.util.ArrayList
@@ -14,7 +14,6 @@ import java.util.Collection
14import java.util.List 14import java.util.List
15 15
16import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 16import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
17import java.util.Collections
18 17
19class Logic2VampireLanguageMapper_TypeMapper { 18class Logic2VampireLanguageMapper_TypeMapper {
20 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE 19 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -28,10 +27,8 @@ class Logic2VampireLanguageMapper_TypeMapper {
28 27
29 def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, 28 def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements,
30 Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { 29 Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
31
32// val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
33// trace.typeMapperTrace = typeTrace
34 val VLSVariable variable = createVLSVariable => [it.name = "A"] 30 val VLSVariable variable = createVLSVariable => [it.name = "A"]
31 var globalCounter = 0
35 32
36 // 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
37 for (type : types) { 34 for (type : types) {
@@ -39,94 +36,109 @@ class Logic2VampireLanguageMapper_TypeMapper {
39 it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) 36 it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
40 it.terms += support.duplicate(variable) 37 it.terms += support.duplicate(variable)
41 ] 38 ]
42// typeTrace.type2Predicate.put(type, typePred)
43 trace.type2Predicate.put(type, typePred) 39 trace.type2Predicate.put(type, typePred)
44 } 40 }
45 41
46 // 2. Map each ENUM type definition to fof formula 42 // 2. Map each ENUM type definition to fof formula
47 for (type : types.filter(TypeDefinition)) { 43 for (type : types.filter(TypeDefinition)) {
44
45 // Create a VLSFunction for each Enum Element
48 val List<VLSFunction> orElems = newArrayList 46 val List<VLSFunction> orElems = newArrayList
49 for (e : type.elements) { 47 for (e : type.elements) {
50 val enumElemPred = createVLSFunction => [ 48 val enumElemPred = createVLSFunction => [
51 val splitName = e.name.split(" ") 49 val splitName = e.name.split(" ")
52 if( splitName.length > 2) { 50 if (splitName.length > 2) {
53 it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) 51 it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2))
54 } 52 } else {
55 else {
56 it.constant = support.toIDMultiple("e", splitName.get(0)) 53 it.constant = support.toIDMultiple("e", splitName.get(0))
57 } 54 }
58 it.terms += support.duplicate(variable) 55 it.terms += support.duplicate(variable)
59 ] 56 ]
60// typeTrace.element2Predicate.put(e, enumElemPred)
61 trace.element2Predicate.put(e, enumElemPred) 57 trace.element2Predicate.put(e, enumElemPred)
62 orElems.add(enumElemPred)
63 } 58 }
64 59
60 // Similar to InheritanceHierarchy for the Enum
61 val List<VLSTerm> possibleNots = newArrayList
62 val List<VLSTerm> typeDefs = newArrayList
63
64 for (t1 : type.elements) {
65 for (t2 : type.elements) {
66 if (t1 == t2) {
67 val fct = support.duplicate(t2.lookup(trace.element2Predicate), variable)
68 possibleNots.add(fct)
69 } else {
70 val op = support.duplicate(t2.lookup(trace.element2Predicate), variable)
71 val negFct = createVLSUnaryNegation => [
72 it.operand = op
73 ]
74 possibleNots.add(negFct)
75 }
76 }
77 typeDefs.add(support.unfoldAnd(possibleNots))
78 possibleNots.clear
79 }
80
81 // Implement Enum Inheritence Hierarchy
65 val res = createVLSFofFormula => [ 82 val res = createVLSFofFormula => [
66 it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) 83 it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
67 // below is temporary solution
68 it.fofRole = "axiom" 84 it.fofRole = "axiom"
69 it.fofFormula = createVLSUniversalQuantifier => [ 85 it.fofFormula = createVLSUniversalQuantifier => [
70 it.variables += support.duplicate(variable) 86 it.variables += support.duplicate(variable)
71 it.operand = createVLSEquivalent => [ 87 it.operand = createVLSEquivalent => [
72 it.left = type.lookup(trace.type2Predicate) 88 it.left = type.lookup(trace.type2Predicate)
73 it.right = support.unfoldOr(orElems) 89 it.right = createVLSAnd => [
90 it.left = support.topLevelTypeFunc(variable)
91 it.right = support.unfoldOr(typeDefs)
92 ]
93// it.right = support.unfoldOr((typeDefs))
94
74 ] 95 ]
75 ] 96 ]
76
77 ] 97 ]
78 trace.specification.formulas += res 98 trace.specification.formulas += res
79 99
80 // Create objects for the enum elements 100 for (var i = globalCounter; i < globalCounter+type.elements.length; i++) {
81 val List<VLSTerm> enumScopeElems = newArrayList 101 // Create objects for the enum elements
82 for (var i = 0; i < type.elements.length; i++) {
83 val num = i + 1 102 val num = i + 1
84 val cstTerm = createVLSFunctionAsTerm => [ 103 val cstTerm = createVLSFunctionAsTerm => [
85 it.functor = "eo" + num 104 it.functor = "eo" + num
86 ] 105 ]
87 val cst = support.toConstant(cstTerm) 106 val cst = support.toConstant(cstTerm)
88 trace.uniqueInstances.add(cst) 107 trace.uniqueInstances.add(cst)
89 val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm) 108
90 enumScopeElems.add(fct) 109 val index = i
91 110 val enumScope = createVLSFofFormula => [
92 //For paradox Only 111 it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0),
93 for (var j = 0; j < type.elements.length; j++) { 112 type.elements.get(index).name.split(" ").get(0))
94 if(j != i) { 113 it.fofRole = "axiom"
95 val op = support.duplicate(type.elements.get(j).lookup(trace.element2Predicate), cstTerm) 114 it.fofFormula = createVLSUniversalQuantifier => [
96 val negFct = createVLSUnaryNegation => [ 115 it.variables += support.duplicate(variable)
97 it.operand = op 116 it.operand = createVLSEquivalent => [
117 it.left = createVLSEquality => [
118 it.left = support.duplicate(variable)
119 it.right = support.duplicate(support.toConstant(cstTerm))
120 ]
121 it.right = support.duplicate(type.elements.get(index).lookup(trace.element2Predicate),
122 variable)
98 ] 123 ]
99 enumScopeElems.add(negFct) 124 ]
100 } 125 ]
101 } 126
102 //End Paradox 127 trace.specification.formulas += enumScope
103// enumScopeElems.add(support.topLevelTypeFunc(cstTerm)) 128
104 } 129 }
105 130 globalCounter+=type.elements.size
106
107
108 val enumScope = createVLSFofFormula => [
109 it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0))
110 // below is temporary solution
111 it.fofRole = "axiom"
112 it.fofFormula = support.unfoldAnd(enumScopeElems)
113 ]
114
115 trace.specification.formulas += enumScope
116 } 131 }
117 132
118 // HIERARCHY HANDLER 133 // HIERARCHY HANDLER
119 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates 134 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
120 // and store in a map 135 // and store in a map
121// println(types.filter[!isIsAbstract]) 136 for (t1 : types.filter[!isIsAbstract]) {
122 for (t1 : types.filter[!isIsAbstract].filter(TypeDeclaration)) {
123 for (t2 : types) { 137 for (t2 : types) {
124 // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes 138 // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
125 if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { 139 if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
126// typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
127 trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) 140 trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
128 } else { 141 } else {
129// typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
130 trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ 142 trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
131 it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) 143 it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
132 ]) 144 ])
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-28 06:50:16 +0000