diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-05 13:37:02 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-05 13:37:02 -0500 |
commit | df12163128073296c4d811fa67b02e37ceb20179 (patch) | |
tree | 7509fdd478d6ff3d908d0ab5aa39ed9a8260f0b0 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |
parent | Begin handing of scope and fix type definitions. (diff) | |
download | VIATRA-Generator-df12163128073296c4d811fa67b02e37ceb20179.tar.gz VIATRA-Generator-df12163128073296c4d811fa67b02e37ceb20179.tar.zst VIATRA-Generator-df12163128073296c4d811fa67b02e37ceb20179.zip |
Implement type scope handling
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) { |