diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-07 17:29:18 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:22:48 -0400 |
commit | 0380611be40f8f92256455e117f2f3c04b7dd216 (patch) | |
tree | 87feff0aadaa0395299d040bfe83adf77773bd58 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire | |
parent | Fix Enum handling for Paradox Integration (diff) | |
download | VIATRA-Generator-0380611be40f8f92256455e117f2f3c04b7dd216.tar.gz VIATRA-Generator-0380611be40f8f92256455e117f2f3c04b7dd216.tar.zst VIATRA-Generator-0380611be40f8f92256455e117f2f3c04b7dd216.zip |
Improve TypeScope handling
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire')
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 | |||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
11 | import java.util.ArrayList | 12 | import java.util.ArrayList |
12 | import java.util.HashMap | 13 | import 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 | |||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
7 | import java.util.List | 7 | import java.util.List |
8 | import java.util.ArrayList | ||
9 | |||
10 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
8 | 11 | ||
9 | class Logic2VampireLanguageMapper_ScopeMapper { | 12 | class 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) |