diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-13 19:08:37 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:22:50 -0400 |
commit | 2ce7f84dc8e869bae343cec1376d2983af5e4de8 (patch) | |
tree | 4cf5b4916f887f9ee983bb8ef80e0eda123fc7b4 /Solvers/Vampire-Solver | |
parent | Improve TypeScope handling (diff) | |
download | VIATRA-Generator-2ce7f84dc8e869bae343cec1376d2983af5e4de8.tar.gz VIATRA-Generator-2ce7f84dc8e869bae343cec1376d2983af5e4de8.tar.zst VIATRA-Generator-2ce7f84dc8e869bae343cec1376d2983af5e4de8.zip |
Implement type scope for specific types
Diffstat (limited to 'Solvers/Vampire-Solver')
29 files changed, 86 insertions, 41 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin index a357265a..035b992e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin index d51853b3..3a2b0f09 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin index ac749133..b8a39035 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin index c4d049d4..c462e145 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin index 6c21f595..2d3b2709 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin index be25b151..8640966e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin index ce399e1c..183e5e40 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin index e279fc45..7c2fb4bf 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin index 9abf8fdb..415d0cc9 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin index 2b114f57..9d43d4a1 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin index 5f2366b0..d3a5a764 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin index d0414079..dd4b1eaa 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin index 56e0771f..a3a95c68 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin index 8ac45333..88c7412c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin | |||
Binary files differ | |||
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 2da4cfd7..5c5eaff3 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 | |||
@@ -1,13 +1,15 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant | 3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 4 | 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 hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
8 | import java.util.ArrayList | 8 | import java.util.ArrayList |
9 | import java.util.Map | ||
9 | 10 | ||
10 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
12 | import java.util.HashMap | ||
11 | 13 | ||
12 | class Logic2VampireLanguageMapper_ScopeMapper { | 14 | class Logic2VampireLanguageMapper_ScopeMapper { |
13 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 15 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -21,9 +23,9 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
21 | 23 | ||
22 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { | 24 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { |
23 | 25 | ||
24 | // HANDLE ERRORS RELATED TO MAX > MIN | 26 | // TODO HANDLE ERRORS RELATED TO MAX > MIN |
25 | // HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS | 27 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS |
26 | // NOT SPECIFIED MEANS =0 ? | 28 | // TODO NOT SPECIFIED MEANS =0 ? |
27 | // 1. make a list of constants equaling the min number of specified objects | 29 | // 1. make a list of constants equaling the min number of specified objects |
28 | val GLOBAL_MIN = config.typeScopes.minNewElements | 30 | val GLOBAL_MIN = config.typeScopes.minNewElements |
29 | val GLOBAL_MAX = config.typeScopes.maxNewElements | 31 | val GLOBAL_MAX = config.typeScopes.maxNewElements |
@@ -32,42 +34,47 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
32 | 34 | ||
33 | // Handling Minimum_General | 35 | // Handling Minimum_General |
34 | if (GLOBAL_MIN != 0) { | 36 | if (GLOBAL_MIN != 0) { |
35 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false) // fix last param | 37 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) // fix last param |
36 | makeFofFormula(localInstances, trace, true, "object") | 38 | makeFofFormula(localInstances, trace, true, null) |
37 | } | 39 | } |
38 | 40 | ||
39 | // Handling Maximum_General | 41 | // Handling Maximum_General |
40 | if (GLOBAL_MAX != 0) { | 42 | if (GLOBAL_MAX != 0) { |
41 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true) // fix last param | 43 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) // fix last param |
42 | makeFofFormula(localInstances, trace, false, "object") | 44 | makeFofFormula(localInstances, trace, false, null) |
43 | } | 45 | } |
44 | 46 | ||
45 | // Handling Minimum_Specific | 47 | // Handling Minimum_Specific |
46 | var i = 0 | 48 | var i = 0 |
47 | var minNum = -1 | 49 | var minNum = -1 |
50 | var Map<Type, Integer> startPoints = new HashMap | ||
48 | for (t : config.typeScopes.minNewElementsByType.keySet) { | 51 | for (t : config.typeScopes.minNewElementsByType.keySet) { |
49 | minNum = t.lookup(config.typeScopes.minNewElementsByType) | 52 | minNum = t.lookup(config.typeScopes.minNewElementsByType) |
50 | if (minNum != 0) { | 53 | if (minNum != 0) { |
51 | getInstanceConstants(i+minNum, i, localInstances, trace, false) | 54 | getInstanceConstants(i + minNum, i, localInstances, trace, true, false) |
55 | startPoints.put(t, i) | ||
52 | i += minNum | 56 | i += minNum |
53 | makeFofFormula(localInstances, trace, true, t.toString)//fix last param | 57 | makeFofFormula(localInstances, trace, true, t) |
54 | } | 58 | } |
55 | } | 59 | } |
56 | 60 | ||
57 | //TODO: calc sum of mins, compare to current value of i | 61 | // TODO: calc sum of mins, compare to current value of i |
58 | |||
59 | // Handling Maximum_Specific | 62 | // Handling Maximum_Specific |
60 | for (t : config.typeScopes.maxNewElementsByType.keySet) { | 63 | for (t : config.typeScopes.maxNewElementsByType.keySet) { |
61 | var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) | 64 | var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) |
62 | minNum = t.lookup(config.typeScopes.minNewElementsByType) | 65 | minNum = t.lookup(config.typeScopes.minNewElementsByType) |
63 | if (maxNum != 0) { | 66 | var startpoint = t.lookup(startPoints) |
64 | var forLimit = Math.min(GLOBAL_MAX, i+maxNum-minNum) | 67 | if (minNum != 0) { |
65 | getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false) | 68 | getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) |
66 | makeFofFormula(localInstances, trace, false, t.toString)//fix last param | 69 | } |
70 | if (maxNum != minNum) { | ||
71 | var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum) | ||
72 | getInstanceConstants(instEndInd, i, localInstances, trace, false, false) | ||
73 | makeFofFormula(localInstances, trace, false, t) | ||
67 | } | 74 | } |
68 | } | 75 | } |
69 | 76 | ||
70 | // 3. Specify uniqueness of elements | 77 | // 3. Specify uniqueness of elements |
71 | if (trace.uniqueInstances.length != 0) { | 78 | if (trace.uniqueInstances.length != 0) { |
72 | val uniqueness = createVLSFofFormula => [ | 79 | val uniqueness = createVLSFofFormula => [ |
73 | it.name = "typeUniqueness" | 80 | it.name = "typeUniqueness" |
@@ -79,10 +86,12 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
79 | 86 | ||
80 | } | 87 | } |
81 | 88 | ||
82 | def protected void getInstanceConstants(int numElems, int init, ArrayList list, | 89 | def protected void getInstanceConstants(int endInd, int startInd, ArrayList list, |
83 | Logic2VampireLanguageMapperTrace trace, boolean addToTrace) { | 90 | Logic2VampireLanguageMapperTrace trace, boolean clear, boolean addToTrace) { |
84 | list.clear | 91 | if (clear) { |
85 | for (var i = init; i < numElems; i++) { | 92 | list.clear |
93 | } | ||
94 | for (var i = startInd; i < endInd; i++) { | ||
86 | val num = i + 1 | 95 | val num = i + 1 |
87 | val cst = createVLSConstant => [ | 96 | val cst = createVLSConstant => [ |
88 | it.name = "o" + num | 97 | it.name = "o" + num |
@@ -94,7 +103,20 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
94 | } | 103 | } |
95 | } | 104 | } |
96 | 105 | ||
97 | def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, String name) { | 106 | def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, |
107 | Type type) { | ||
108 | var nm = "" | ||
109 | var VLSFunction tm = null | ||
110 | if (type === null) { | ||
111 | nm = "object" | ||
112 | tm = support.topLevelTypeFunc | ||
113 | } else { | ||
114 | nm = type.lookup(trace.type2Predicate).constant.toString | ||
115 | tm = support.duplicate(type.lookup(trace.type2Predicate)) | ||
116 | } | ||
117 | val name = nm | ||
118 | val term = tm | ||
119 | |||
98 | val cstDec = createVLSFofFormula => [ | 120 | val cstDec = createVLSFofFormula => [ |
99 | it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name) | 121 | it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name) |
100 | it.fofRole = "axiom" | 122 | it.fofRole = "axiom" |
@@ -109,15 +131,16 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
109 | it.right = i | 131 | it.right = i |
110 | ] | 132 | ] |
111 | ]) | 133 | ]) |
112 | it.right = support.topLevelTypeFunc | 134 | it.right = term |
113 | } else { | 135 | } else { |
136 | it.left = term | ||
114 | it.right = support.unfoldOr(list.map [ i | | 137 | it.right = support.unfoldOr(list.map [ i | |
115 | createVLSEquality => [ | 138 | createVLSEquality => [ |
116 | it.left = createVLSVariable => [it.name = variable.name] | 139 | it.left = createVLSVariable => [it.name = variable.name] |
117 | it.right = i | 140 | it.right = i |
118 | ] | 141 | ] |
119 | ]) | 142 | ]) |
120 | it.left = support.topLevelTypeFunc | 143 | |
121 | } | 144 | } |
122 | ] | 145 | ] |
123 | ] | 146 | ] |
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 5c634ba0..b86e8068 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 19d48790..052e0175 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 2db39cf0..1296bf9e 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 1fba7ac4..0210a300 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 9ef3a39c..fd625384 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 687f4889..978571d2 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 d59b2e98..b98f0332 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 eb12e24a..8238a89e 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 70eb3434..f64a218b 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 0077e151..cf8e4acd 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 62de24fc..07d5b7b4 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 d00ac8ca..983108a2 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 b86330dc..4442cdea 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 a412241a..1950cad0 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 | |||
@@ -6,6 +6,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage | |||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
@@ -15,6 +16,8 @@ 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.logic.model.logiclanguage.Type; |
16 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 17 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
17 | import java.util.ArrayList; | 18 | import java.util.ArrayList; |
19 | import java.util.HashMap; | ||
20 | import java.util.Map; | ||
18 | import java.util.Set; | 21 | import java.util.Set; |
19 | import org.eclipse.emf.common.util.EList; | 22 | import org.eclipse.emf.common.util.EList; |
20 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 23 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
@@ -47,24 +50,26 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
47 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | 50 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; |
48 | final ArrayList<Object> localInstances = CollectionLiterals.<Object>newArrayList(); | 51 | final ArrayList<Object> localInstances = CollectionLiterals.<Object>newArrayList(); |
49 | if ((GLOBAL_MIN != 0)) { | 52 | if ((GLOBAL_MIN != 0)) { |
50 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false); | 53 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); |
51 | this.makeFofFormula(localInstances, trace, true, "object"); | 54 | this.makeFofFormula(localInstances, trace, true, null); |
52 | } | 55 | } |
53 | if ((GLOBAL_MAX != 0)) { | 56 | if ((GLOBAL_MAX != 0)) { |
54 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true); | 57 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); |
55 | this.makeFofFormula(localInstances, trace, false, "object"); | 58 | this.makeFofFormula(localInstances, trace, false, null); |
56 | } | 59 | } |
57 | int i = 0; | 60 | int i = 0; |
58 | int minNum = (-1); | 61 | int minNum = (-1); |
62 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); | ||
59 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); | 63 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); |
60 | for (final Type t : _keySet) { | 64 | for (final Type t : _keySet) { |
61 | { | 65 | { |
62 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); | 66 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); |
63 | if ((minNum != 0)) { | 67 | if ((minNum != 0)) { |
64 | this.getInstanceConstants((i + minNum), i, localInstances, trace, false); | 68 | this.getInstanceConstants((i + minNum), i, localInstances, trace, true, false); |
69 | startPoints.put(t, Integer.valueOf(i)); | ||
65 | int _i = i; | 70 | int _i = i; |
66 | i = (_i + minNum); | 71 | i = (_i + minNum); |
67 | this.makeFofFormula(localInstances, trace, true, t.toString()); | 72 | this.makeFofFormula(localInstances, trace, true, t); |
68 | } | 73 | } |
69 | } | 74 | } |
70 | } | 75 | } |
@@ -73,10 +78,14 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
73 | { | 78 | { |
74 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); | 79 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); |
75 | minNum = (CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); | 80 | minNum = (CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); |
76 | if (((maxNum).intValue() != 0)) { | 81 | Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints); |
77 | int forLimit = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); | 82 | if ((minNum != 0)) { |
78 | this.getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false); | 83 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); |
79 | this.makeFofFormula(localInstances, trace, false, t_1.toString()); | 84 | } |
85 | if (((maxNum).intValue() != minNum)) { | ||
86 | int instEndInd = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); | ||
87 | this.getInstanceConstants(instEndInd, i, localInstances, trace, false, false); | ||
88 | this.makeFofFormula(localInstances, trace, false, t_1); | ||
80 | } | 89 | } |
81 | } | 90 | } |
82 | } | 91 | } |
@@ -95,9 +104,11 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
95 | } | 104 | } |
96 | } | 105 | } |
97 | 106 | ||
98 | protected void getInstanceConstants(final int numElems, final int init, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean addToTrace) { | 107 | protected void getInstanceConstants(final int endInd, final int startInd, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean clear, final boolean addToTrace) { |
99 | list.clear(); | 108 | if (clear) { |
100 | for (int i = init; (i < numElems); i++) { | 109 | list.clear(); |
110 | } | ||
111 | for (int i = startInd; (i < endInd); i++) { | ||
101 | { | 112 | { |
102 | final int num = (i + 1); | 113 | final int num = (i + 1); |
103 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | 114 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); |
@@ -113,7 +124,18 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
113 | } | 124 | } |
114 | } | 125 | } |
115 | 126 | ||
116 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final String name) { | 127 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { |
128 | String nm = ""; | ||
129 | VLSFunction tm = null; | ||
130 | if ((type == null)) { | ||
131 | nm = "object"; | ||
132 | tm = this.support.topLevelTypeFunc(); | ||
133 | } else { | ||
134 | nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString(); | ||
135 | tm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate)); | ||
136 | } | ||
137 | final String name = nm; | ||
138 | final VLSFunction term = tm; | ||
117 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 139 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
118 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 140 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
119 | String _xifexpression = null; | 141 | String _xifexpression = null; |
@@ -146,8 +168,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
146 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_4); | 168 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_4); |
147 | }; | 169 | }; |
148 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_3))); | 170 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_3))); |
149 | it_2.setRight(this.support.topLevelTypeFunc()); | 171 | it_2.setRight(term); |
150 | } else { | 172 | } else { |
173 | it_2.setLeft(term); | ||
151 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { | 174 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { |
152 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 175 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
153 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { | 176 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { |
@@ -162,7 +185,6 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
162 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); | 185 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); |
163 | }; | 186 | }; |
164 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); | 187 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); |
165 | it_2.setLeft(this.support.topLevelTypeFunc()); | ||
166 | } | 188 | } |
167 | }; | 189 | }; |
168 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | 190 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); |