diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-04 19:55:10 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:36:08 -0400 |
commit | 9a770703c17e1c758b71091fd364dcda1cefacc4 (patch) | |
tree | 4c39d83bd3a20d0d6b2230d79ac1731b810ef213 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner | |
parent | Closes #34, adds code to test cases where minScope>maxScope. (diff) | |
download | VIATRA-Generator-9a770703c17e1c758b71091fd364dcda1cefacc4.tar.gz VIATRA-Generator-9a770703c17e1c758b71091fd364dcda1cefacc4.tar.zst VIATRA-Generator-9a770703c17e1c758b71091fd364dcda1cefacc4.zip |
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner')
6 files changed, 58 insertions, 28 deletions
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 54fcdc86..5e8819a6 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 | |||
@@ -36,31 +36,30 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
36 | 36 | ||
37 | val localInstances = newArrayList | 37 | val localInstances = newArrayList |
38 | 38 | ||
39 | val consistant = GLOBAL_MAX > GLOBAL_MIN | ||
40 | |||
39 | // Handling Minimum_General | 41 | // Handling Minimum_General |
40 | if (GLOBAL_MIN != ABSOLUTE_MIN) { | 42 | if (GLOBAL_MIN != ABSOLUTE_MIN) { |
41 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) | 43 | // * |
42 | for (i : trace.uniqueInstances) { | 44 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant) |
43 | localInstances.add(support.duplicate(i)) | 45 | if (consistant) { |
46 | for (i : trace.uniqueInstances) { | ||
47 | localInstances.add(support.duplicate(i)) | ||
48 | } | ||
49 | makeFofFormula(localInstances, trace, true, null) | ||
50 | } else { | ||
51 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null) | ||
44 | } | 52 | } |
45 | |||
46 | makeFofFormula(localInstances, trace, true, null) | ||
47 | |||
48 | // //For testing Min>Max scope | ||
49 | // getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, true) | ||
50 | // makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null) | ||
51 | // //end for testing | ||
52 | |||
53 | } | 53 | } |
54 | 54 | ||
55 | // Handling Maximum_General | 55 | // Handling Maximum_General |
56 | if (GLOBAL_MAX != ABSOLUTE_MAX) { | 56 | if (GLOBAL_MAX != ABSOLUTE_MAX) { |
57 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) | 57 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant) |
58 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) | 58 | if (consistant) { |
59 | 59 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) | |
60 | // //For testing Min>Max scope | 60 | } else { |
61 | // getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, false) | 61 | makeFofFormula(localInstances, trace, false, null) |
62 | // makeFofFormula(localInstances, trace, false, null) | 62 | } |
63 | // //end for testing | ||
64 | } | 63 | } |
65 | 64 | ||
66 | // Handling Minimum_Specific | 65 | // Handling Minimum_Specific |
@@ -94,14 +93,30 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
94 | } | 93 | } |
95 | 94 | ||
96 | // 3. Specify uniqueness of elements | 95 | // 3. Specify uniqueness of elements |
97 | if (trace.uniqueInstances.length != 0) { | 96 | val numInst = trace.uniqueInstances.length |
97 | var ind = 1 | ||
98 | if (numInst != 0) { | ||
99 | /* | ||
100 | * // SHORTER | ||
101 | * for (e : trace.uniqueInstances.subList(0, numInst-1)) { | ||
102 | /*/ | ||
103 | // LONGER | ||
98 | for (e : trace.uniqueInstances) { | 104 | for (e : trace.uniqueInstances) { |
105 | // */ | ||
106 | val x = ind | ||
99 | val uniqueness = createVLSFofFormula => [ | 107 | val uniqueness = createVLSFofFormula => [ |
100 | it.name = support.toIDMultiple("t_uniqueness", e.name) | 108 | it.name = support.toIDMultiple("t_uniqueness", e.name) |
101 | it.fofRole = "axiom" | 109 | it.fofRole = "axiom" |
110 | /* | ||
111 | * // SHORTER | ||
112 | * it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e) | ||
113 | /*/ | ||
114 | // LONGER | ||
102 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) | 115 | it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) |
116 | // */ | ||
103 | ] | 117 | ] |
104 | trace.specification.formulas += uniqueness | 118 | trace.specification.formulas += uniqueness |
119 | ind++ | ||
105 | } | 120 | } |
106 | } | 121 | } |
107 | } | 122 | } |
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 b00dad42..dd88a53a 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 | |||
@@ -109,6 +109,8 @@ class Logic2VampireLanguageMapper_Support { | |||
109 | 109 | ||
110 | // TODO Make more general | 110 | // TODO Make more general |
111 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { | 111 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { |
112 | |||
113 | // OLD | ||
112 | // val List<VLSInequality> eqs = newArrayList | 114 | // val List<VLSInequality> eqs = newArrayList |
113 | // for (t1 : terms.subList(1, terms.length)) { | 115 | // for (t1 : terms.subList(1, terms.length)) { |
114 | // for (t2 : terms.subList(0, terms.indexOf(t1))) { | 116 | // for (t2 : terms.subList(0, terms.indexOf(t1))) { |
@@ -122,6 +124,8 @@ class Logic2VampireLanguageMapper_Support { | |||
122 | // } | 124 | // } |
123 | // } | 125 | // } |
124 | // return unfoldAnd(eqs) | 126 | // return unfoldAnd(eqs) |
127 | // END OLD | ||
128 | |||
125 | val List<VLSInequality> eqs = newArrayList | 129 | val List<VLSInequality> eqs = newArrayList |
126 | for (t1 : terms) { | 130 | for (t1 : terms) { |
127 | if (t1 != t2) { | 131 | if (t1 != t2) { |
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 6c46d2e3..2cc60591 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/.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 e5600049..1108945f 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 f9813a92..a473c586 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_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 d40b0dd2..24b46e3e 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 | |||
@@ -52,16 +52,25 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
52 | final int GLOBAL_MIN = config.typeScopes.minNewElements; | 52 | final int GLOBAL_MIN = config.typeScopes.minNewElements; |
53 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | 53 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; |
54 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); | 54 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); |
55 | final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); | ||
55 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { | 56 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { |
56 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); | 57 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant)); |
57 | for (final VLSConstant i : trace.uniqueInstances) { | 58 | if (consistant) { |
58 | localInstances.add(this.support.duplicate(i)); | 59 | for (final VLSConstant i : trace.uniqueInstances) { |
60 | localInstances.add(this.support.duplicate(i)); | ||
61 | } | ||
62 | this.makeFofFormula(localInstances, trace, true, null); | ||
63 | } else { | ||
64 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, true, null); | ||
59 | } | 65 | } |
60 | this.makeFofFormula(localInstances, trace, true, null); | ||
61 | } | 66 | } |
62 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { | 67 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { |
63 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); | 68 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant); |
64 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); | 69 | if (consistant) { |
70 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); | ||
71 | } else { | ||
72 | this.makeFofFormula(localInstances, trace, false, null); | ||
73 | } | ||
65 | } | 74 | } |
66 | int i_1 = 1; | 75 | int i_1 = 1; |
67 | int minNum = (-1); | 76 | int minNum = (-1); |
@@ -95,11 +104,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
95 | } | 104 | } |
96 | } | 105 | } |
97 | } | 106 | } |
98 | int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; | 107 | final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; |
99 | boolean _notEquals = (_length != 0); | 108 | int ind = 1; |
100 | if (_notEquals) { | 109 | if ((numInst != 0)) { |
101 | for (final VLSConstant e : trace.uniqueInstances) { | 110 | for (final VLSConstant e : trace.uniqueInstances) { |
102 | { | 111 | { |
112 | final int x = ind; | ||
103 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 113 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
104 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 114 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
105 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); | 115 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); |
@@ -109,6 +119,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
109 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 119 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); |
110 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 120 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
111 | _formulas.add(uniqueness); | 121 | _formulas.add(uniqueness); |
122 | ind++; | ||
112 | } | 123 | } |
113 | } | 124 | } |
114 | } | 125 | } |