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/xtend-gen/ca/mcgill | |
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/xtend-gen/ca/mcgill')
15 files changed, 129 insertions, 48 deletions
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) -> { |