diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-05 13:37:02 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:22:39 -0400 |
commit | f019f3ec81976f8e05d0c7458aba2f29b18461d0 (patch) | |
tree | d9c338f8ddf33bbdd35018404b57608782796b26 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse | |
parent | Begin handing of scope and fix type definitions. (diff) | |
download | VIATRA-Generator-f019f3ec81976f8e05d0c7458aba2f29b18461d0.tar.gz VIATRA-Generator-f019f3ec81976f8e05d0c7458aba2f29b18461d0.tar.zst VIATRA-Generator-f019f3ec81976f8e05d0c7458aba2f29b18461d0.zip |
Implement type scope handling
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse')
20 files changed, 97 insertions, 66 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 9a2a1b15..4a4eedf5 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 ce05b92c..55f0ac1e 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 379d0683..e91f89cc 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 76dd192f..154ff393 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 936ab9ca..5d6ad730 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 e0f442f5..7c787543 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 493ff288..34f3b285 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 13281767..f8d6cd3f 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 1a777880..7b2b11f8 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/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin index e8658e7b..7e8336e2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_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_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin index aec1688a..a2229dba 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index e77b9866..d82649ff 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 100a52b8..030a0be9 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 231c1995..87203ed8 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 b67a307c..65689b0c 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.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index 89c9637e..6643576f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java | |||
@@ -273,7 +273,7 @@ public class Logic2VampireLanguageMapper { | |||
273 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 273 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
274 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 274 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
275 | TypeReference _range = instanceOf.getRange(); | 275 | TypeReference _range = instanceOf.getRange(); |
276 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | 276 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); |
277 | EList<VLSTerm> _terms = it.getTerms(); | 277 | EList<VLSTerm> _terms = it.getTerms(); |
278 | VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); | 278 | VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); |
279 | _terms.add(_transformTerm); | 279 | _terms.add(_transformTerm); |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java index 561402a7..bce50fcc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | |||
@@ -61,7 +61,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
61 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 61 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
62 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 62 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
63 | TypeReference _range = variable.getRange(); | 63 | TypeReference _range = variable.getRange(); |
64 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | 64 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); |
65 | EList<VLSTerm> _terms = it.getTerms(); | 65 | EList<VLSTerm> _terms = it.getTerms(); |
66 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 66 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); |
67 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 67 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { |
@@ -75,7 +75,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
75 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); | 75 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); |
76 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { | 76 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { |
77 | TypeReference _range = variable.getRange(); | 77 | TypeReference _range = variable.getRange(); |
78 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | 78 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); |
79 | EList<VLSTerm> _terms = it.getTerms(); | 79 | EList<VLSTerm> _terms = it.getTerms(); |
80 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 80 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); |
81 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> { | 81 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> { |
@@ -215,7 +215,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
215 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 215 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
216 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 216 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
217 | TypeReference _get = r.getParameters().get((i).intValue()); | 217 | TypeReference _get = r.getParameters().get((i).intValue()); |
218 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _get).getReferred().getName())); | 218 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _get).getReferred().getName())); |
219 | EList<VLSTerm> _terms = it.getTerms(); | 219 | EList<VLSTerm> _terms = it.getTerms(); |
220 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 220 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); |
221 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 221 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { |
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 86d8b648..8967839d 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 | |||
@@ -51,42 +51,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
51 | instances.add(cst); | 51 | instances.add(cst); |
52 | } | 52 | } |
53 | } | 53 | } |
54 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 54 | if ((config.typeScopes.minNewElements != 0)) { |
55 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 55 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
56 | it.setName("typeScope"); | 56 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
57 | it.setFofRole("axiom"); | 57 | it.setName("typeScope"); |
58 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 58 | it.setFofRole("axiom"); |
59 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 59 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
60 | EList<VLSVariable> _variables = it_1.getVariables(); | 60 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
61 | VLSVariable _duplicate = this.support.duplicate(variable); | 61 | EList<VLSVariable> _variables = it_1.getVariables(); |
62 | _variables.add(_duplicate); | 62 | VLSVariable _duplicate = this.support.duplicate(variable); |
63 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 63 | _variables.add(_duplicate); |
64 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | 64 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
65 | it_2.setLeft(this.support.topLevelTypeFunc()); | 65 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { |
66 | final Function1<VLSConstant, VLSEquality> _function_4 = (VLSConstant i) -> { | 66 | it_2.setLeft(this.support.topLevelTypeFunc()); |
67 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 67 | final Function1<VLSConstant, VLSEquality> _function_4 = (VLSConstant i) -> { |
68 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { | 68 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
69 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 69 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { |
70 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { | 70 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); |
71 | it_4.setName(variable.getName()); | 71 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { |
72 | it_4.setName(variable.getName()); | ||
73 | }; | ||
74 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_6); | ||
75 | it_3.setLeft(_doubleArrow); | ||
76 | it_3.setRight(i); | ||
72 | }; | 77 | }; |
73 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_6); | 78 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); |
74 | it_3.setLeft(_doubleArrow); | ||
75 | it_3.setRight(i); | ||
76 | }; | 79 | }; |
77 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); | 80 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4))); |
78 | }; | 81 | }; |
79 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4))); | 82 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); |
83 | it_1.setOperand(_doubleArrow); | ||
80 | }; | 84 | }; |
81 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | 85 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); |
82 | it_1.setOperand(_doubleArrow); | 86 | it.setFofFormula(_doubleArrow); |
83 | }; | 87 | }; |
84 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | 88 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); |
85 | it.setFofFormula(_doubleArrow); | 89 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
86 | }; | 90 | _formulas.add(cstDec); |
87 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | 91 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
88 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 92 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { |
89 | _formulas.add(cstDec); | 93 | it.setName("typeUniqueness"); |
94 | it.setFofRole("axiom"); | ||
95 | it.setFofFormula(this.support.establishUniqueness(instances)); | ||
96 | }; | ||
97 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2); | ||
98 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
99 | _formulas_1.add(uniqueness); | ||
100 | } | ||
90 | } | 101 | } |
91 | 102 | ||
92 | public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 103 | 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_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index b111732f..dfe624be 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |||
@@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
@@ -25,6 +26,7 @@ import java.util.List; | |||
25 | import java.util.Map; | 26 | import java.util.Map; |
26 | import org.eclipse.emf.common.util.EList; | 27 | import org.eclipse.emf.common.util.EList; |
27 | import org.eclipse.xtend2.lib.StringConcatenation; | 28 | import org.eclipse.xtend2.lib.StringConcatenation; |
29 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
28 | import org.eclipse.xtext.xbase.lib.Conversions; | 30 | import org.eclipse.xtext.xbase.lib.Conversions; |
29 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | 31 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; |
30 | import org.eclipse.xtext.xbase.lib.Extension; | 32 | import org.eclipse.xtext.xbase.lib.Extension; |
@@ -73,6 +75,36 @@ public class Logic2VampireLanguageMapper_Support { | |||
73 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 75 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
74 | } | 76 | } |
75 | 77 | ||
78 | public VLSTerm establishUniqueness(final List<VLSConstant> terms) { | ||
79 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); | ||
80 | List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); | ||
81 | for (final VLSConstant t1 : _subList) { | ||
82 | List<VLSConstant> _subList_1 = terms.subList(0, terms.indexOf(t1)); | ||
83 | for (final VLSConstant t2 : _subList_1) { | ||
84 | { | ||
85 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); | ||
86 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { | ||
87 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
88 | final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> { | ||
89 | it_1.setName(t2.getName()); | ||
90 | }; | ||
91 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); | ||
92 | it.setLeft(_doubleArrow); | ||
93 | VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); | ||
94 | final Procedure1<VLSConstant> _function_2 = (VLSConstant it_1) -> { | ||
95 | it_1.setName(t1.getName()); | ||
96 | }; | ||
97 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2); | ||
98 | it.setRight(_doubleArrow_1); | ||
99 | }; | ||
100 | final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | ||
101 | eqs.add(eq); | ||
102 | } | ||
103 | } | ||
104 | } | ||
105 | return this.unfoldAnd(eqs); | ||
106 | } | ||
107 | |||
76 | protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) { | 108 | protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) { |
77 | int _size = operands.size(); | 109 | int _size = operands.size(); |
78 | boolean _equals = (_size == 1); | 110 | boolean _equals = (_size == 1); |
@@ -180,7 +212,7 @@ public class Logic2VampireLanguageMapper_Support { | |||
180 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 212 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
181 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 213 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
182 | TypeReference _range = variable.getRange(); | 214 | TypeReference _range = variable.getRange(); |
183 | it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | 215 | it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); |
184 | EList<VLSTerm> _terms = it.getTerms(); | 216 | EList<VLSTerm> _terms = it.getTerms(); |
185 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 217 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
186 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 218 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { |
@@ -229,7 +261,7 @@ public class Logic2VampireLanguageMapper_Support { | |||
229 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 261 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
230 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 262 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
231 | TypeReference _range = variable.getRange(); | 263 | TypeReference _range = variable.getRange(); |
232 | it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | 264 | it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); |
233 | EList<VLSTerm> _terms = it.getTerms(); | 265 | EList<VLSTerm> _terms = it.getTerms(); |
234 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 266 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
235 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 267 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java index 71e98871..1e845d94 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java | |||
@@ -115,47 +115,39 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
115 | return Boolean.valueOf((!_isIsAbstract)); | 115 | return Boolean.valueOf((!_isIsAbstract)); |
116 | }; | 116 | }; |
117 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); | 117 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); |
118 | for (final Type type_2 : _filter_1) { | 118 | for (final Type t1 : _filter_1) { |
119 | { | 119 | { |
120 | for (final Type type2 : types) { | 120 | for (final Type t2 : types) { |
121 | if ((Objects.equal(type_2, type2) || this.dfsSupertypeCheck(type_2, type2))) { | 121 | if ((Objects.equal(t1, t2) || this.dfsSupertypeCheck(t1, t2))) { |
122 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 122 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
123 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { | 123 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { |
124 | it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant()); | 124 | it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(t2, typeTrace.type2Predicate).getConstant()); |
125 | EList<VLSTerm> _terms = it.getTerms(); | 125 | EList<VLSTerm> _terms = it.getTerms(); |
126 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 126 | VLSVariable _duplicate = this.support.duplicate(variable); |
127 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> { | 127 | _terms.add(_duplicate); |
128 | it_1.setName("A"); | ||
129 | }; | ||
130 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3); | ||
131 | _terms.add(_doubleArrow); | ||
132 | }; | 128 | }; |
133 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2); | 129 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2); |
134 | typeTrace.type2PossibleNot.put(type2, _doubleArrow); | 130 | typeTrace.type2PossibleNot.put(t2, _doubleArrow); |
135 | } else { | 131 | } else { |
136 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 132 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); |
137 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { | 133 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { |
138 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); | 134 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); |
139 | final Procedure1<VLSFunction> _function_4 = (VLSFunction it_1) -> { | 135 | final Procedure1<VLSFunction> _function_4 = (VLSFunction it_1) -> { |
140 | it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant()); | 136 | it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(t2, typeTrace.type2Predicate).getConstant()); |
141 | EList<VLSTerm> _terms = it_1.getTerms(); | 137 | EList<VLSTerm> _terms = it_1.getTerms(); |
142 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 138 | VLSVariable _duplicate = this.support.duplicate(variable); |
143 | final Procedure1<VLSVariable> _function_5 = (VLSVariable it_2) -> { | 139 | _terms.add(_duplicate); |
144 | it_2.setName("A"); | ||
145 | }; | ||
146 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_5); | ||
147 | _terms.add(_doubleArrow_1); | ||
148 | }; | 140 | }; |
149 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_4); | 141 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_4); |
150 | it.setOperand(_doubleArrow_1); | 142 | it.setOperand(_doubleArrow_1); |
151 | }; | 143 | }; |
152 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); | 144 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); |
153 | typeTrace.type2PossibleNot.put(type2, _doubleArrow_1); | 145 | typeTrace.type2PossibleNot.put(t2, _doubleArrow_1); |
154 | } | 146 | } |
155 | } | 147 | } |
156 | Collection<VLSTerm> _values = typeTrace.type2PossibleNot.values(); | 148 | Collection<VLSTerm> _values = typeTrace.type2PossibleNot.values(); |
157 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | 149 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); |
158 | typeTrace.type2And.put(type_2, this.support.unfoldAnd(_arrayList)); | 150 | typeTrace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); |
159 | typeTrace.type2PossibleNot.clear(); | 151 | typeTrace.type2PossibleNot.clear(); |
160 | } | 152 | } |
161 | } | 153 | } |
@@ -166,21 +158,17 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
166 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 158 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
167 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | 159 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { |
168 | EList<VLSVariable> _variables = it_1.getVariables(); | 160 | EList<VLSVariable> _variables = it_1.getVariables(); |
169 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 161 | VLSVariable _duplicate = this.support.duplicate(variable); |
170 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_2) -> { | 162 | _variables.add(_duplicate); |
171 | it_2.setName("A"); | ||
172 | }; | ||
173 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_4); | ||
174 | _variables.add(_doubleArrow); | ||
175 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 163 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
176 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | 164 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { |
177 | it_2.setLeft(this.support.topLevelTypeFunc()); | 165 | it_2.setLeft(this.support.topLevelTypeFunc()); |
178 | Collection<VLSTerm> _values = typeTrace.type2And.values(); | 166 | Collection<VLSTerm> _values = typeTrace.type2And.values(); |
179 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | 167 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); |
180 | it_2.setRight(this.support.unfoldOr(_arrayList)); | 168 | it_2.setRight(this.support.unfoldOr(_arrayList)); |
181 | }; | 169 | }; |
182 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | 170 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); |
183 | it_1.setOperand(_doubleArrow_1); | 171 | it_1.setOperand(_doubleArrow); |
184 | }; | 172 | }; |
185 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); | 173 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); |
186 | it.setFofFormula(_doubleArrow); | 174 | it.setFofFormula(_doubleArrow); |