diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill')
18 files changed, 211 insertions, 79 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 be554f99..b2e83781 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 0ee9b884..ec4554da 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 8e96ba14..85d288b2 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 ee720e29..f43d3267 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 528da797..a49422be 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_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index a1204329..e9060301 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.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 3413fc3f..ca19d1c9 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 a53a998a..bd348286 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 f265f6a3..274a1261 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 efde8350..2e16b79c 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 2cabecc8..b363474f 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 57844580..82ee023c 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 24898f59..e378eda2 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 a9589e7e..427ec9c1 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_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 8c0ae38d..7bc70e9d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | |||
@@ -10,9 +10,12 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | |||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
18 | import com.google.common.base.Objects; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; |
@@ -21,9 +24,13 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | |||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; |
22 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 25 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
23 | import java.util.ArrayList; | 26 | import java.util.ArrayList; |
27 | import java.util.HashMap; | ||
24 | import java.util.List; | 28 | import java.util.List; |
29 | import java.util.Map; | ||
30 | import java.util.Set; | ||
25 | import org.eclipse.emf.common.util.EList; | 31 | import org.eclipse.emf.common.util.EList; |
26 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 32 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
33 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
27 | import org.eclipse.xtext.xbase.lib.Extension; | 34 | import org.eclipse.xtext.xbase.lib.Extension; |
28 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 35 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
29 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 36 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
@@ -107,69 +114,155 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
107 | it.setName("B"); | 114 | it.setName("B"); |
108 | }; | 115 | }; |
109 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | 116 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); |
117 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
118 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it) -> { | ||
119 | it.setName("C"); | ||
120 | }; | ||
121 | final VLSVariable varC = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_3); | ||
110 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); | 122 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); |
123 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); | ||
111 | for (final Relation l_1 : relationsList) { | 124 | for (final Relation l_1 : relationsList) { |
112 | { | 125 | { |
113 | final String relName = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString(); | 126 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList); |
114 | TypeReference _get = l_1.getParameters().get(0); | 127 | TypeReference _get = l_1.getParameters().get(1); |
115 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | 128 | Type _referred = ((ComplexTypeReference) _get).getReferred(); |
116 | final Type fromType = ((Type) _referred); | 129 | final Type toType = ((Type) _referred); |
117 | TypeReference _get_1 = l_1.getParameters().get(1); | 130 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); |
118 | Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred(); | 131 | this.addToMap(type2cont, toFunc, rel); |
119 | final Type toType = ((Type) _referred_1); | 132 | EList<Type> _subtypes = toType.getSubtypes(); |
120 | final ArrayList<VLSFunction> listForAnd = CollectionLiterals.<VLSFunction>newArrayList(); | 133 | for (final Type c : _subtypes) { |
121 | listForAnd.add(this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList)); | 134 | this.addToMap(type2cont, toFunc, rel); |
135 | } | ||
136 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
137 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
138 | it.setName(this.support.toIDMultiple("noDupCont", rel.getConstant().toString())); | ||
139 | it.setFofRole("axiom"); | ||
140 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
141 | final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> { | ||
142 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
143 | VLSVariable _duplicate = this.support.duplicate(varA); | ||
144 | _variables.add(_duplicate); | ||
145 | EList<VLSVariable> _variables_1 = it_1.getVariables(); | ||
146 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | ||
147 | _variables_1.add(_duplicate_1); | ||
148 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
149 | final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> { | ||
150 | it_2.setLeft(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varA, varB))); | ||
151 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
152 | final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> { | ||
153 | VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier(); | ||
154 | final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> { | ||
155 | EList<VLSVariable> _variables_2 = it_4.getVariables(); | ||
156 | VLSVariable _duplicate_2 = this.support.duplicate(varC); | ||
157 | _variables_2.add(_duplicate_2); | ||
158 | EList<VLSVariable> _variables_3 = it_4.getVariables(); | ||
159 | VLSVariable _duplicate_3 = this.support.duplicate(varB); | ||
160 | _variables_3.add(_duplicate_3); | ||
161 | it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB))); | ||
162 | }; | ||
163 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier_1, _function_8); | ||
164 | it_3.setOperand(_doubleArrow); | ||
165 | }; | ||
166 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_7); | ||
167 | it_2.setRight(_doubleArrow); | ||
168 | }; | ||
169 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6); | ||
170 | it_1.setOperand(_doubleArrow); | ||
171 | }; | ||
172 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_5); | ||
173 | it.setFofFormula(_doubleArrow); | ||
174 | }; | ||
175 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); | ||
176 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
177 | _formulas_1.add(relFormula); | ||
178 | } | ||
179 | } | ||
180 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); | ||
181 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { | ||
182 | { | ||
122 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 183 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
123 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 184 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
124 | it.setName(this.support.toIDMultiple("containment", relName)); | 185 | it.setName(this.support.toIDMultiple("containment", e.getKey().getConstant().toString())); |
125 | it.setFofRole("axiom"); | 186 | it.setFofRole("axiom"); |
126 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 187 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
127 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | 188 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
128 | EList<VLSVariable> _variables = it_1.getVariables(); | 189 | EList<VLSVariable> _variables = it_1.getVariables(); |
129 | VLSVariable _duplicate = this.support.duplicate(varA); | 190 | VLSVariable _duplicate = this.support.duplicate(varA); |
130 | _variables.add(_duplicate); | 191 | _variables.add(_duplicate); |
131 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 192 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
132 | final Procedure1<VLSImplies> _function_5 = (VLSImplies it_2) -> { | 193 | final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> { |
133 | it_2.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate), varA)); | 194 | it_2.setLeft(this.support.duplicate(e.getKey(), varA)); |
134 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | 195 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); |
135 | final Procedure1<VLSExistentialQuantifier> _function_6 = (VLSExistentialQuantifier it_3) -> { | 196 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> { |
136 | EList<VLSVariable> _variables_1 = it_3.getVariables(); | 197 | EList<VLSVariable> _variables_1 = it_3.getVariables(); |
137 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | 198 | VLSVariable _duplicate_1 = this.support.duplicate(varB); |
138 | _variables_1.add(_duplicate_1); | 199 | _variables_1.add(_duplicate_1); |
139 | it_3.setOperand(this.support.unfoldAnd(listForAnd)); | 200 | int _length = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; |
201 | boolean _greaterThan = (_length > 1); | ||
202 | if (_greaterThan) { | ||
203 | it_3.setOperand(this.makeUnique(e.getValue())); | ||
204 | } else { | ||
205 | it_3.setOperand(e.getValue().get(0)); | ||
206 | } | ||
140 | }; | 207 | }; |
141 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_6); | 208 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); |
142 | it_2.setRight(_doubleArrow); | 209 | it_2.setRight(_doubleArrow); |
143 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
144 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { | ||
145 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
146 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
147 | final Procedure1<VLSConstant> _function_8 = (VLSConstant it_4) -> { | ||
148 | it_4.setName("o1"); | ||
149 | }; | ||
150 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_8); | ||
151 | it_3.setRight(_doubleArrow_1); | ||
152 | }; | ||
153 | ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); | ||
154 | }; | 210 | }; |
155 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_5); | 211 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6); |
156 | it_1.setOperand(_doubleArrow); | 212 | it_1.setOperand(_doubleArrow); |
157 | }; | 213 | }; |
158 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | 214 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); |
159 | it.setFofFormula(_doubleArrow); | 215 | it.setFofFormula(_doubleArrow); |
160 | }; | 216 | }; |
161 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | 217 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); |
162 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | 218 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
163 | _formulas_1.add(relFormula); | 219 | _formulas_1.add(relFormula); |
164 | TypeReference _get_2 = l_1.getParameters().get(1); | 220 | } |
165 | Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred(); | 221 | } |
166 | Type pointingTo = ((Type) _referred_2); | 222 | } |
167 | containmentListCopy.remove(pointingTo); | 223 | |
168 | EList<Type> _subtypes = pointingTo.getSubtypes(); | 224 | protected VLSTerm makeUnique(final List<VLSFunction> list) { |
169 | for (final Type c : _subtypes) { | 225 | final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList(); |
170 | containmentListCopy.remove(c); | 226 | final List<VLSTerm> uniqueRels = CollectionLiterals.<VLSTerm>newArrayList(); |
227 | for (final VLSFunction t1 : list) { | ||
228 | { | ||
229 | for (final VLSFunction t2 : list) { | ||
230 | boolean _equals = Objects.equal(t1, t2); | ||
231 | if (_equals) { | ||
232 | final VLSFunction fct = this.support.duplicate(t2); | ||
233 | possibleNots.add(fct); | ||
234 | } else { | ||
235 | final VLSFunction op = this.support.duplicate(t2); | ||
236 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
237 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { | ||
238 | it.setOperand(op); | ||
239 | }; | ||
240 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function); | ||
241 | possibleNots.add(negFct); | ||
242 | } | ||
171 | } | 243 | } |
244 | uniqueRels.add(this.support.unfoldAnd(possibleNots)); | ||
245 | possibleNots.clear(); | ||
246 | } | ||
247 | } | ||
248 | return this.support.unfoldOr(uniqueRels); | ||
249 | } | ||
250 | |||
251 | protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) { | ||
252 | Object _xifexpression = null; | ||
253 | boolean _containsKey = type2cont.containsKey(toFunc); | ||
254 | boolean _not = (!_containsKey); | ||
255 | if (_not) { | ||
256 | _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel)); | ||
257 | } else { | ||
258 | boolean _xifexpression_1 = false; | ||
259 | boolean _contains = type2cont.get(toFunc).contains(rel); | ||
260 | boolean _not_1 = (!_contains); | ||
261 | if (_not_1) { | ||
262 | _xifexpression_1 = type2cont.get(toFunc).add(rel); | ||
172 | } | 263 | } |
264 | _xifexpression = Boolean.valueOf(_xifexpression_1); | ||
173 | } | 265 | } |
266 | return _xifexpression; | ||
174 | } | 267 | } |
175 | } | 268 | } |
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 | ||
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 119d01f1..64129bf3 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 | |||
@@ -14,6 +14,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | |||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
17 | import com.google.common.base.Objects; | ||
17 | import com.google.common.collect.Iterables; | 18 | import com.google.common.collect.Iterables; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; |
@@ -173,31 +174,28 @@ public class Logic2VampireLanguageMapper_Support { | |||
173 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 174 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
174 | } | 175 | } |
175 | 176 | ||
176 | public VLSTerm establishUniqueness(final List<VLSConstant> terms) { | 177 | public VLSTerm establishUniqueness(final List<VLSConstant> terms, final VLSConstant t2) { |
177 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); | 178 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); |
178 | List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); | 179 | for (final VLSConstant t1 : terms) { |
179 | for (final VLSConstant t1 : _subList) { | 180 | boolean _notEquals = (!Objects.equal(t1, t2)); |
180 | List<VLSConstant> _subList_1 = terms.subList(0, terms.indexOf(t1)); | 181 | if (_notEquals) { |
181 | for (final VLSConstant t2 : _subList_1) { | 182 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); |
182 | { | 183 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { |
183 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); | 184 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); |
184 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { | 185 | final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> { |
185 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | 186 | it_1.setName(t2.getName()); |
186 | final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> { | ||
187 | it_1.setName(t2.getName()); | ||
188 | }; | ||
189 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); | ||
190 | it.setLeft(_doubleArrow); | ||
191 | VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); | ||
192 | final Procedure1<VLSConstant> _function_2 = (VLSConstant it_1) -> { | ||
193 | it_1.setName(t1.getName()); | ||
194 | }; | ||
195 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2); | ||
196 | it.setRight(_doubleArrow_1); | ||
197 | }; | 187 | }; |
198 | final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | 188 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); |
199 | eqs.add(eq); | 189 | it.setLeft(_doubleArrow); |
200 | } | 190 | VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); |
191 | final Procedure1<VLSConstant> _function_2 = (VLSConstant it_1) -> { | ||
192 | it_1.setName(t1.getName()); | ||
193 | }; | ||
194 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2); | ||
195 | it.setRight(_doubleArrow_1); | ||
196 | }; | ||
197 | final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | ||
198 | eqs.add(eq); | ||
201 | } | 199 | } |
202 | } | 200 | } |
203 | return this.unfoldAnd(eqs); | 201 | return this.unfoldAnd(eqs); |
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 ec759ebf..9b8f049d 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 | |||
@@ -223,31 +223,68 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
223 | trace.type2PossibleNot.clear(); | 223 | trace.type2PossibleNot.clear(); |
224 | } | 224 | } |
225 | } | 225 | } |
226 | final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList(); | ||
227 | for (final Type t : types) { | ||
228 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
229 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | ||
230 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate))); | ||
231 | }; | ||
232 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | ||
233 | type2Not.add(_doubleArrow); | ||
234 | } | ||
226 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 235 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
227 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | 236 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { |
237 | it.setName("notObjectHandler"); | ||
238 | it.setFofRole("axiom"); | ||
239 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
240 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | ||
241 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
242 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
243 | _variables.add(_duplicate); | ||
244 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
245 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | ||
246 | VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); | ||
247 | final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_3) -> { | ||
248 | it_3.setOperand(this.support.topLevelTypeFunc()); | ||
249 | }; | ||
250 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_6); | ||
251 | it_2.setLeft(_doubleArrow_1); | ||
252 | it_2.setRight(this.support.unfoldAnd(type2Not)); | ||
253 | }; | ||
254 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | ||
255 | it_1.setOperand(_doubleArrow_1); | ||
256 | }; | ||
257 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | ||
258 | it.setFofFormula(_doubleArrow_1); | ||
259 | }; | ||
260 | final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_3); | ||
261 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
262 | _formulas.add(notObj); | ||
263 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
264 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
228 | it.setName("inheritanceHierarchyHandler"); | 265 | it.setName("inheritanceHierarchyHandler"); |
229 | it.setFofRole("axiom"); | 266 | it.setFofRole("axiom"); |
230 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 267 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
231 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | 268 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
232 | EList<VLSVariable> _variables = it_1.getVariables(); | 269 | EList<VLSVariable> _variables = it_1.getVariables(); |
233 | VLSVariable _duplicate = this.support.duplicate(variable); | 270 | VLSVariable _duplicate = this.support.duplicate(variable); |
234 | _variables.add(_duplicate); | 271 | _variables.add(_duplicate); |
235 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 272 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
236 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | 273 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { |
237 | it_2.setLeft(this.support.topLevelTypeFunc()); | 274 | it_2.setLeft(this.support.topLevelTypeFunc()); |
238 | Collection<VLSTerm> _values = trace.type2And.values(); | 275 | Collection<VLSTerm> _values = trace.type2And.values(); |
239 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); | 276 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); |
240 | it_2.setRight(this.support.unfoldOr(reversedList)); | 277 | it_2.setRight(this.support.unfoldOr(reversedList)); |
241 | }; | 278 | }; |
242 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | 279 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); |
243 | it_1.setOperand(_doubleArrow); | 280 | it_1.setOperand(_doubleArrow_1); |
244 | }; | 281 | }; |
245 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); | 282 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); |
246 | it.setFofFormula(_doubleArrow); | 283 | it.setFofFormula(_doubleArrow_1); |
247 | }; | 284 | }; |
248 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | 285 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); |
249 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 286 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
250 | _xblockexpression = _formulas.add(hierarch); | 287 | _xblockexpression = _formulas_1.add(hierarch); |
251 | } | 288 | } |
252 | return _xblockexpression; | 289 | return _xblockexpression; |
253 | } | 290 | } |