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 | |
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')
18 files changed, 230 insertions, 96 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) |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 3f204913..5c634ba0 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index 10983f27..19d48790 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 00ebca4b..2db39cf0 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index 9641858d..1fba7ac4 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index 2b51fe5d..9ef3a39c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index 75482abc..687f4889 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index c394f878..d59b2e98 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 1ec5da80..eb12e24a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index 8a6f30f9..70eb3434 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index c000d128..0077e151 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 5eb63977..62de24fc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 501dbfb4..d00ac8ca 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 621c888a..b86330dc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index 15ba78c9..a412241a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |||
@@ -12,9 +12,13 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | |||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
16 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
15 | import java.util.ArrayList; | 17 | import java.util.ArrayList; |
18 | import java.util.Set; | ||
16 | import org.eclipse.emf.common.util.EList; | 19 | import org.eclipse.emf.common.util.EList; |
17 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 20 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
21 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
18 | import org.eclipse.xtext.xbase.lib.Extension; | 22 | import org.eclipse.xtext.xbase.lib.Extension; |
19 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 23 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
20 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 24 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
@@ -30,76 +34,146 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
30 | 34 | ||
31 | private final Logic2VampireLanguageMapper base; | 35 | private final Logic2VampireLanguageMapper base; |
32 | 36 | ||
37 | private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> { | ||
38 | it.setName("A"); | ||
39 | })); | ||
40 | |||
33 | public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) { | 41 | public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) { |
34 | this.base = base; | 42 | this.base = base; |
35 | } | 43 | } |
36 | 44 | ||
37 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 45 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
38 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 46 | final int GLOBAL_MIN = config.typeScopes.minNewElements; |
39 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | 47 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; |
40 | it.setName("A"); | 48 | final ArrayList<Object> localInstances = CollectionLiterals.<Object>newArrayList(); |
41 | }; | 49 | if ((GLOBAL_MIN != 0)) { |
42 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | 50 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false); |
43 | final ArrayList<VLSTerm> localInstances = CollectionLiterals.<VLSTerm>newArrayList(); | 51 | this.makeFofFormula(localInstances, trace, true, "object"); |
44 | for (int i = 0; (i < config.typeScopes.minNewElements); i++) { | 52 | } |
53 | if ((GLOBAL_MAX != 0)) { | ||
54 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true); | ||
55 | this.makeFofFormula(localInstances, trace, false, "object"); | ||
56 | } | ||
57 | int i = 0; | ||
58 | int minNum = (-1); | ||
59 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); | ||
60 | for (final Type t : _keySet) { | ||
61 | { | ||
62 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); | ||
63 | if ((minNum != 0)) { | ||
64 | this.getInstanceConstants((i + minNum), i, localInstances, trace, false); | ||
65 | int _i = i; | ||
66 | i = (_i + minNum); | ||
67 | this.makeFofFormula(localInstances, trace, true, t.toString()); | ||
68 | } | ||
69 | } | ||
70 | } | ||
71 | Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); | ||
72 | for (final Type t_1 : _keySet_1) { | ||
73 | { | ||
74 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); | ||
75 | minNum = (CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); | ||
76 | if (((maxNum).intValue() != 0)) { | ||
77 | int forLimit = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); | ||
78 | this.getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false); | ||
79 | this.makeFofFormula(localInstances, trace, false, t_1.toString()); | ||
80 | } | ||
81 | } | ||
82 | } | ||
83 | int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; | ||
84 | boolean _notEquals = (_length != 0); | ||
85 | if (_notEquals) { | ||
86 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
87 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
88 | it.setName("typeUniqueness"); | ||
89 | it.setFofRole("axiom"); | ||
90 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances)); | ||
91 | }; | ||
92 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
93 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
94 | _formulas.add(uniqueness); | ||
95 | } | ||
96 | } | ||
97 | |||
98 | protected void getInstanceConstants(final int numElems, final int init, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean addToTrace) { | ||
99 | list.clear(); | ||
100 | for (int i = init; (i < numElems); i++) { | ||
45 | { | 101 | { |
46 | final int num = (i + 1); | 102 | final int num = (i + 1); |
47 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | 103 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); |
48 | final Procedure1<VLSConstant> _function_1 = (VLSConstant it) -> { | 104 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { |
49 | it.setName(("o" + Integer.valueOf(num))); | 105 | it.setName(("o" + Integer.valueOf(num))); |
50 | }; | 106 | }; |
51 | final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); | 107 | final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); |
52 | trace.uniqueInstances.add(cst); | 108 | if (addToTrace) { |
53 | localInstances.add(cst); | 109 | trace.uniqueInstances.add(cst); |
110 | } | ||
111 | list.add(cst); | ||
54 | } | 112 | } |
55 | } | 113 | } |
56 | if ((config.typeScopes.minNewElements != 0)) { | 114 | } |
57 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 115 | |
58 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 116 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final String name) { |
59 | it.setName("typeScope"); | 117 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
60 | it.setFofRole("axiom"); | 118 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
61 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 119 | String _xifexpression = null; |
62 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 120 | if (minimum) { |
63 | EList<VLSVariable> _variables = it_1.getVariables(); | 121 | _xifexpression = "min"; |
64 | VLSVariable _duplicate = this.support.duplicate(variable); | 122 | } else { |
65 | _variables.add(_duplicate); | 123 | _xifexpression = "max"; |
66 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 124 | } |
67 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | 125 | it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); |
126 | it.setFofRole("axiom"); | ||
127 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
128 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
129 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
130 | VLSVariable _duplicate = this.support.duplicate(this.variable); | ||
131 | _variables.add(_duplicate); | ||
132 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
133 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
134 | if (minimum) { | ||
135 | final Function1<VLSTerm, VLSEquality> _function_3 = (VLSTerm i) -> { | ||
136 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
137 | final Procedure1<VLSEquality> _function_4 = (VLSEquality it_3) -> { | ||
138 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
139 | final Procedure1<VLSVariable> _function_5 = (VLSVariable it_4) -> { | ||
140 | it_4.setName(this.variable.getName()); | ||
141 | }; | ||
142 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_5); | ||
143 | it_3.setLeft(_doubleArrow); | ||
144 | it_3.setRight(i); | ||
145 | }; | ||
146 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_4); | ||
147 | }; | ||
148 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_3))); | ||
149 | it_2.setRight(this.support.topLevelTypeFunc()); | ||
150 | } else { | ||
68 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { | 151 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { |
69 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 152 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
70 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { | 153 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { |
71 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 154 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
72 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { | 155 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { |
73 | it_4.setName(variable.getName()); | 156 | it_4.setName(this.variable.getName()); |
74 | }; | 157 | }; |
75 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_6); | 158 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); |
76 | it_3.setLeft(_doubleArrow); | 159 | it_3.setLeft(_doubleArrow); |
77 | it_3.setRight(i); | 160 | it_3.setRight(i); |
78 | }; | 161 | }; |
79 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); | 162 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); |
80 | }; | 163 | }; |
81 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(localInstances, _function_4))); | 164 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); |
82 | it_2.setRight(this.support.topLevelTypeFunc()); | 165 | it_2.setLeft(this.support.topLevelTypeFunc()); |
83 | }; | 166 | } |
84 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
85 | it_1.setOperand(_doubleArrow); | ||
86 | }; | 167 | }; |
87 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | 168 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); |
88 | it.setFofFormula(_doubleArrow); | 169 | it_1.setOperand(_doubleArrow); |
89 | }; | 170 | }; |
90 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | 171 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); |
91 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 172 | it.setFofFormula(_doubleArrow); |
92 | _formulas.add(cstDec); | 173 | }; |
93 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 174 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); |
94 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | 175 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
95 | it.setName("typeUniqueness"); | 176 | _formulas.add(cstDec); |
96 | it.setFofRole("axiom"); | ||
97 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances)); | ||
98 | }; | ||
99 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2); | ||
100 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
101 | _formulas_1.add(uniqueness); | ||
102 | } | ||
103 | } | 177 | } |
104 | 178 | ||
105 | public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 179 | public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java index c101aa4c..b8d74f36 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java | |||
@@ -78,7 +78,14 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
78 | { | 78 | { |
79 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 79 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
80 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 80 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
81 | it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2])); | 81 | final String[] splitName = e.getName().split(" "); |
82 | int _length = splitName.length; | ||
83 | boolean _greaterThan = (_length > 2); | ||
84 | if (_greaterThan) { | ||
85 | it.setConstant(this.support.toIDMultiple("e", splitName[0], splitName[2])); | ||
86 | } else { | ||
87 | it.setConstant(this.support.toIDMultiple("e", splitName[0])); | ||
88 | } | ||
82 | EList<VLSTerm> _terms = it.getTerms(); | 89 | EList<VLSTerm> _terms = it.getTerms(); |
83 | VLSVariable _duplicate = this.support.duplicate(variable); | 90 | VLSVariable _duplicate = this.support.duplicate(variable); |
84 | _terms.add(_duplicate); | 91 | _terms.add(_duplicate); |
@@ -175,7 +182,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
175 | } | 182 | } |
176 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 183 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
177 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | 184 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { |
178 | it.setName("hierarchyHandler"); | 185 | it.setName("inheritanceHierarchyHandler"); |
179 | it.setFofRole("axiom"); | 186 | it.setFofRole("axiom"); |
180 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 187 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
181 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | 188 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { |