diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-21 11:47:31 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:35:28 -0400 |
commit | 36b3b957df6ff37d3c0b7196943c825b4fb0fffd (patch) | |
tree | d07725e7eb845f6c5eeba4d55c3ec4f9edcc9bca /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |
parent | Add gitignore, commit everything (diff) | |
download | VIATRA-Generator-36b3b957df6ff37d3c0b7196943c825b4fb0fffd.tar.gz VIATRA-Generator-36b3b957df6ff37d3c0b7196943c825b4fb0fffd.tar.zst VIATRA-Generator-36b3b957df6ff37d3c0b7196943c825b4fb0fffd.zip |
Add to containment, add notObject case.
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 | 22 |
1 files changed, 13 insertions, 9 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 d2a6bff2..7aca7633 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 | |||
@@ -96,15 +96,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
96 | int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; | 96 | int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; |
97 | boolean _notEquals = (_length != 0); | 97 | boolean _notEquals = (_length != 0); |
98 | if (_notEquals) { | 98 | if (_notEquals) { |
99 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 99 | for (final VLSConstant e : trace.uniqueInstances) { |
100 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 100 | { |
101 | it.setName("typeUniqueness"); | 101 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
102 | it.setFofRole("axiom"); | 102 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
103 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances)); | 103 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); |
104 | }; | 104 | it.setFofRole("axiom"); |
105 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 105 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); |
106 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 106 | }; |
107 | _formulas.add(uniqueness); | 107 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); |
108 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
109 | _formulas.add(uniqueness); | ||
110 | } | ||
111 | } | ||
108 | } | 112 | } |
109 | } | 113 | } |
110 | 114 | ||