diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse')
18 files changed, 55 insertions, 99 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 bda7463e..4828107b 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 a062fcec..64061f82 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 5fc0da27..f0cd1c7c 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 562b9bbf..7d15db96 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 dd7bdf86..8fed8f56 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 496d27b3..a40e27e4 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 4a03f2ce..4b6b4a1e 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 511f4a1f..c3035658 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 37e9480c..2e21736e 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 f473c4bc..e870dabc 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 e53791d6..ed198ef6 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 1b112c56..83697125 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 c8284658..063650c5 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 89d4c657..e36d2270 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 3c98bd64..5e5be153 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 6643576f..dc2cd5ec 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 | |||
@@ -50,6 +50,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | |||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; | 50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; |
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; | 51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; |
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | 52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; |
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 55 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
55 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 56 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
@@ -262,18 +263,18 @@ public class Logic2VampireLanguageMapper { | |||
262 | } | 263 | } |
263 | 264 | ||
264 | protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 265 | protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
265 | return this.support.createUniversallyQuantifiedExpression(this, forall, trace, variables); | 266 | return this.support.createQuantifiedExpression(this, forall, trace, variables, true); |
266 | } | 267 | } |
267 | 268 | ||
268 | protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 269 | protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
269 | return this.support.createExistentiallyQuantifiedExpression(this, exists, trace, variables); | 270 | return this.support.createQuantifiedExpression(this, exists, trace, variables, false); |
270 | } | 271 | } |
271 | 272 | ||
272 | protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 273 | protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
273 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 274 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
274 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 275 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
275 | TypeReference _range = instanceOf.getRange(); | 276 | TypeReference _range = instanceOf.getRange(); |
276 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | 277 | it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate).getConstant()); |
277 | EList<VLSTerm> _terms = it.getTerms(); | 278 | EList<VLSTerm> _terms = it.getTerms(); |
278 | VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); | 279 | VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); |
279 | _terms.add(_transformTerm); | 280 | _terms.add(_transformTerm); |
@@ -303,12 +304,7 @@ public class Logic2VampireLanguageMapper { | |||
303 | } | 304 | } |
304 | 305 | ||
305 | protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 306 | protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
306 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 307 | return this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables)); |
307 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
308 | it.setName(this.support.toID(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables).getName())); | ||
309 | }; | ||
310 | final VLSVariable res = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
311 | return res; | ||
312 | } | 308 | } |
313 | 309 | ||
314 | protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 310 | protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
@@ -359,7 +355,7 @@ public class Logic2VampireLanguageMapper { | |||
359 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 355 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
360 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 356 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
361 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 357 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
362 | it.setConstant(this.support.toIDMultiple("rel", relation.getName())); | 358 | it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); |
363 | EList<VLSTerm> _terms = it.getTerms(); | 359 | EList<VLSTerm> _terms = it.getTerms(); |
364 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { | 360 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { |
365 | return this.transformTerm(p, trace, variables); | 361 | return this.transformTerm(p, trace, variables); |
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 4f5c6acc..d5745333 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 | |||
@@ -48,7 +48,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
48 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { | 48 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { |
49 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); | 49 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); |
50 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | 50 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); |
51 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
52 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | 51 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; |
53 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | 52 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); |
54 | for (final Integer i : _doubleDotLessThan) { | 53 | for (final Integer i : _doubleDotLessThan) { |
@@ -68,8 +67,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
68 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 67 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
69 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 68 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
70 | final String[] nameArray = r.getName().split(" "); | 69 | final String[] nameArray = r.getName().split(" "); |
71 | it.setName(this.support.toIDMultiple("compliance", nameArray[0], | 70 | it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2])); |
72 | nameArray[2])); | ||
73 | it.setFofRole("axiom"); | 71 | it.setFofRole("axiom"); |
74 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 72 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
75 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | 73 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { |
@@ -82,23 +80,16 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
82 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | 80 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { |
83 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 81 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
84 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | 82 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { |
85 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | 83 | it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2])); |
86 | int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | 84 | for (final VLSVariable v_1 : relVar2VLS) { |
87 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); | 85 | EList<VLSTerm> _terms = it_3.getTerms(); |
88 | for (final Integer i_1 : _doubleDotLessThan_1) { | 86 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); |
89 | { | 87 | _terms.add(_duplicate_1); |
90 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
91 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
92 | it_4.setName(relVar2VLS.get((i_1).intValue()).getName()); | ||
93 | }; | ||
94 | final VLSVariable v_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
95 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
96 | _terms.add(v_1); | ||
97 | } | ||
98 | } | 88 | } |
99 | }; | 89 | }; |
100 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | 90 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); |
101 | it_2.setLeft(_doubleArrow); | 91 | trace.rel2Predicate.put(r, rel); |
92 | it_2.setLeft(this.support.duplicate(rel)); | ||
102 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); | 93 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); |
103 | }; | 94 | }; |
104 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | 95 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); |
@@ -139,9 +130,9 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
139 | relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); | 130 | relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); |
140 | } | 131 | } |
141 | } | 132 | } |
133 | final String[] nameArray = reldef.getName().split(" "); | ||
142 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 134 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
143 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 135 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
144 | final String[] nameArray = reldef.getName().split(" "); | ||
145 | int _length = nameArray.length; | 136 | int _length = nameArray.length; |
146 | int _minus = (_length - 2); | 137 | int _minus = (_length - 2); |
147 | int _length_1 = nameArray.length; | 138 | int _length_1 = nameArray.length; |
@@ -190,7 +181,12 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
190 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 181 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); |
191 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 182 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
192 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 183 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
193 | it.setName(this.support.toIDMultiple("relation", reldef.getName())); | 184 | int _length = nameArray.length; |
185 | int _minus = (_length - 2); | ||
186 | int _length_1 = nameArray.length; | ||
187 | int _minus_1 = (_length_1 - 1); | ||
188 | it.setName(this.support.toIDMultiple("relation", nameArray[_minus], | ||
189 | nameArray[_minus_1])); | ||
194 | it.setFofRole("axiom"); | 190 | it.setFofRole("axiom"); |
195 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 191 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
196 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 192 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
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 35497eab..72ca44e9 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 | |||
@@ -20,6 +20,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | |||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
23 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
23 | import java.util.ArrayList; | 24 | import java.util.ArrayList; |
24 | import java.util.Collection; | 25 | import java.util.Collection; |
25 | import java.util.HashMap; | 26 | import java.util.HashMap; |
@@ -220,13 +221,13 @@ public class Logic2VampireLanguageMapper_Support { | |||
220 | * ids.map[it.split("\\s+").join("'")].join("'") | 221 | * ids.map[it.split("\\s+").join("'")].join("'") |
221 | * } | 222 | * } |
222 | */ | 223 | */ |
223 | protected VLSTerm createUniversallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 224 | protected VLSTerm createQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables, final boolean isUniversal) { |
224 | VLSUniversalQuantifier _xblockexpression = null; | 225 | VLSTerm _xblockexpression = null; |
225 | { | 226 | { |
226 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { | 227 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { |
227 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 228 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
228 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | 229 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { |
229 | it.setName(this.toIDMultiple("Var", v.getName())); | 230 | it.setName(this.toIDMultiple("V", v.getName())); |
230 | }; | 231 | }; |
231 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | 232 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); |
232 | }; | 233 | }; |
@@ -235,80 +236,43 @@ public class Logic2VampireLanguageMapper_Support { | |||
235 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); | 236 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); |
236 | for (final Variable variable : _quantifiedVariables) { | 237 | for (final Variable variable : _quantifiedVariables) { |
237 | { | 238 | { |
238 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 239 | TypeReference _range = variable.getRange(); |
239 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 240 | final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap)); |
240 | TypeReference _range = variable.getRange(); | ||
241 | it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | ||
242 | EList<VLSTerm> _terms = it.getTerms(); | ||
243 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
244 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
245 | it_1.setName(this.toIDMultiple("Var", variable.getName())); | ||
246 | }; | ||
247 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
248 | _terms.add(_doubleArrow); | ||
249 | }; | ||
250 | final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
251 | typedefs.add(eq); | 241 | typedefs.add(eq); |
252 | } | 242 | } |
253 | } | 243 | } |
254 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 244 | VLSTerm _xifexpression = null; |
255 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> { | 245 | if (isUniversal) { |
256 | EList<VLSVariable> _variables = it.getVariables(); | 246 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
257 | Collection<VLSVariable> _values = variableMap.values(); | 247 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> { |
258 | Iterables.<VLSVariable>addAll(_variables, _values); | 248 | EList<VLSVariable> _variables = it.getVariables(); |
259 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 249 | Collection<VLSVariable> _values = variableMap.values(); |
260 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> { | 250 | Iterables.<VLSVariable>addAll(_variables, _values); |
261 | it_1.setLeft(this.unfoldAnd(typedefs)); | 251 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
262 | it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | 252 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> { |
263 | }; | 253 | it_1.setLeft(this.unfoldAnd(typedefs)); |
264 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | 254 | it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); |
265 | it.setOperand(_doubleArrow); | 255 | }; |
266 | }; | 256 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); |
267 | _xblockexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | 257 | it.setOperand(_doubleArrow); |
268 | } | ||
269 | return _xblockexpression; | ||
270 | } | ||
271 | |||
272 | protected VLSTerm createExistentiallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
273 | VLSExistentialQuantifier _xblockexpression = null; | ||
274 | { | ||
275 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { | ||
276 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
277 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
278 | it.setName(this.toIDMultiple("Var", v.getName())); | ||
279 | }; | 258 | }; |
280 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | 259 | _xifexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); |
281 | }; | 260 | } else { |
282 | final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function); | 261 | VLSExistentialQuantifier _xblockexpression_1 = null; |
283 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
284 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); | ||
285 | for (final Variable variable : _quantifiedVariables) { | ||
286 | { | 262 | { |
287 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 263 | typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); |
288 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 264 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); |
289 | TypeReference _range = variable.getRange(); | 265 | final Procedure1<VLSExistentialQuantifier> _function_2 = (VLSExistentialQuantifier it) -> { |
290 | it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | 266 | EList<VLSVariable> _variables = it.getVariables(); |
291 | EList<VLSTerm> _terms = it.getTerms(); | 267 | Collection<VLSVariable> _values = variableMap.values(); |
292 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 268 | Iterables.<VLSVariable>addAll(_variables, _values); |
293 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 269 | it.setOperand(this.unfoldAnd(typedefs)); |
294 | it_1.setName(this.toIDMultiple("Var", variable.getName())); | ||
295 | }; | ||
296 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
297 | _terms.add(_doubleArrow); | ||
298 | }; | 270 | }; |
299 | final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 271 | _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2); |
300 | typedefs.add(eq); | ||
301 | } | 272 | } |
273 | _xifexpression = _xblockexpression_1; | ||
302 | } | 274 | } |
303 | typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | 275 | _xblockexpression = _xifexpression; |
304 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
305 | final Procedure1<VLSExistentialQuantifier> _function_1 = (VLSExistentialQuantifier it) -> { | ||
306 | EList<VLSVariable> _variables = it.getVariables(); | ||
307 | Collection<VLSVariable> _values = variableMap.values(); | ||
308 | Iterables.<VLSVariable>addAll(_variables, _values); | ||
309 | it.setOperand(this.unfoldAnd(typedefs)); | ||
310 | }; | ||
311 | _xblockexpression = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_1); | ||
312 | } | 276 | } |
313 | return _xblockexpression; | 277 | return _xblockexpression; |
314 | } | 278 | } |