diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java')
| -rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | 73 |
1 files changed, 42 insertions, 31 deletions
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) { |