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/src/ca/mcgill/ecse/dslreasoner | |
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/src/ca/mcgill/ecse/dslreasoner')
2 files changed, 38 insertions, 19 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) { |