aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-03-07 17:29:18 -0500
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-03-07 17:29:18 -0500
commit63cb743dacb8cd374777ba87783cbb96416d32e8 (patch)
treefee66ffc353ee9706c4bc333bb5092751f766051 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse
parentFix Enum handling for Paradox Integration (diff)
downloadVIATRA-Generator-63cb743dacb8cd374777ba87783cbb96416d32e8.tar.gz
VIATRA-Generator-63cb743dacb8cd374777ba87783cbb96416d32e8.tar.zst
VIATRA-Generator-63cb743dacb8cd374777ba87783cbb96416d32e8.zip
Improve TypeScope handling
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend3
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend118
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend28
3 files changed, 101 insertions, 48 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index deb24778..0ae06bc3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -7,6 +7,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction 7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm 8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable 9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory 11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
11import java.util.ArrayList 12import java.util.ArrayList
12import java.util.HashMap 13import java.util.HashMap
@@ -43,7 +44,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
43 44
44 } 45 }
45 46
46 val comply = createVLSFofFormula => [ 47 val comply = createVLSFofFormula=> [
47 val nameArray = r.name.split(" ") 48 val nameArray = r.name.split(" ")
48 it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2)) 49 it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2))
49 it.fofRole = "axiom" 50 it.fofRole = "axiom"
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 e5dfbf08..2da4cfd7 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
@@ -5,60 +5,124 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory 5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration 6import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
7import java.util.List 7import java.util.List
8import java.util.ArrayList
9
10import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
8 11
9class Logic2VampireLanguageMapper_ScopeMapper { 12class Logic2VampireLanguageMapper_ScopeMapper {
10 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE 13 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
11 private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support 14 private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
12 val Logic2VampireLanguageMapper base 15 val Logic2VampireLanguageMapper base
16 private val VLSVariable variable = createVLSVariable => [it.name = "A"]
13 17
14 public new(Logic2VampireLanguageMapper base) { 18 public new(Logic2VampireLanguageMapper base) {
15 this.base = base 19 this.base = base
16 } 20 }
17 21
18 def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { 22 def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
19 val VLSVariable variable = createVLSVariable => [it.name = "A"]
20 23
24// HANDLE ERRORS RELATED TO MAX > MIN
25// HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS
26// NOT SPECIFIED MEANS =0 ?
21 // 1. make a list of constants equaling the min number of specified objects 27 // 1. make a list of constants equaling the min number of specified objects
28 val GLOBAL_MIN = config.typeScopes.minNewElements
29 val GLOBAL_MAX = config.typeScopes.maxNewElements
30
22 val localInstances = newArrayList 31 val localInstances = newArrayList
23 for (var i = 0; i < config.typeScopes.minNewElements; i++) { 32
33 // Handling Minimum_General
34 if (GLOBAL_MIN != 0) {
35 getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false) // fix last param
36 makeFofFormula(localInstances, trace, true, "object")
37 }
38
39 // Handling Maximum_General
40 if (GLOBAL_MAX != 0) {
41 getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true) // fix last param
42 makeFofFormula(localInstances, trace, false, "object")
43 }
44
45 // Handling Minimum_Specific
46 var i = 0
47 var minNum = -1
48 for (t : config.typeScopes.minNewElementsByType.keySet) {
49 minNum = t.lookup(config.typeScopes.minNewElementsByType)
50 if (minNum != 0) {
51 getInstanceConstants(i+minNum, i, localInstances, trace, false)
52 i += minNum
53 makeFofFormula(localInstances, trace, true, t.toString)//fix last param
54 }
55 }
56
57 //TODO: calc sum of mins, compare to current value of i
58
59 // Handling Maximum_Specific
60 for (t : config.typeScopes.maxNewElementsByType.keySet) {
61 var maxNum = t.lookup(config.typeScopes.maxNewElementsByType)
62 minNum = t.lookup(config.typeScopes.minNewElementsByType)
63 if (maxNum != 0) {
64 var forLimit = Math.min(GLOBAL_MAX, i+maxNum-minNum)
65 getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false)
66 makeFofFormula(localInstances, trace, false, t.toString)//fix last param
67 }
68 }
69
70 // 3. Specify uniqueness of elements
71 if (trace.uniqueInstances.length != 0) {
72 val uniqueness = createVLSFofFormula => [
73 it.name = "typeUniqueness"
74 it.fofRole = "axiom"
75 it.fofFormula = support.establishUniqueness(trace.uniqueInstances)
76 ]
77 trace.specification.formulas += uniqueness
78 }
79
80 }
81
82 def protected void getInstanceConstants(int numElems, int init, ArrayList list,
83 Logic2VampireLanguageMapperTrace trace, boolean addToTrace) {
84 list.clear
85 for (var i = init; i < numElems; i++) {
24 val num = i + 1 86 val num = i + 1
25 val cst = createVLSConstant => [ 87 val cst = createVLSConstant => [
26 it.name = "o" + num 88 it.name = "o" + num
27 ] 89 ]
28 trace.uniqueInstances.add(cst) 90 if (addToTrace) {
29 localInstances.add(cst) 91 trace.uniqueInstances.add(cst)
92 }
93 list.add(cst)
30 } 94 }
95 }
31 96
32 // TODO: specify for the max 97 def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, String name) {
33 if (config.typeScopes.minNewElements != 0) { 98 val cstDec = createVLSFofFormula => [
34 // 2. Create initial fof formula to specify the number of elems 99 it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name)
35 val cstDec = createVLSFofFormula => [ 100 it.fofRole = "axiom"
36 it.name = "typeScope" 101 it.fofFormula = createVLSUniversalQuantifier => [
37 it.fofRole = "axiom" 102 it.variables += support.duplicate(variable)
38 it.fofFormula = createVLSUniversalQuantifier => [ 103 // check below
39 it.variables += support.duplicate(variable) 104 it.operand = createVLSImplies => [
40 // check below 105 if (minimum) {
41 it.operand = createVLSImplies => [ 106 it.left = support.unfoldOr(list.map [ i |
42 it.left = support.unfoldOr(localInstances.map [ i |
43 createVLSEquality => [ 107 createVLSEquality => [
44 it.left = createVLSVariable => [it.name = variable.name] 108 it.left = createVLSVariable => [it.name = variable.name]
45 it.right = i 109 it.right = i
46 ] 110 ]
47 ]) 111 ])
48 it.right = support.topLevelTypeFunc 112 it.right = support.topLevelTypeFunc
49 ] 113 } else {
114 it.right = support.unfoldOr(list.map [ i |
115 createVLSEquality => [
116 it.left = createVLSVariable => [it.name = variable.name]
117 it.right = i
118 ]
119 ])
120 it.left = support.topLevelTypeFunc
121 }
50 ] 122 ]
51 ] 123 ]
52 trace.specification.formulas += cstDec 124 ]
53 125 trace.specification.formulas += cstDec
54 // TODO: specify for scope per type
55 // 3. Specify uniqueness of elements
56 val uniqueness = createVLSFofFormula => [
57 it.name = "typeUniqueness"
58 it.fofRole = "axiom"
59 it.fofFormula = support.establishUniqueness(trace.uniqueInstances)
60 ]
61 trace.specification.formulas += uniqueness
62 }
63 } 126 }
127
64} 128}
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)
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-28 17:21:42 +0000