diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-09-08 16:12:55 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:42:29 -0400 |
commit | 4aee5bcc86b9e6b515fbbdac030df42147be7dc1 (patch) | |
tree | ce9f8aa1cf0ab33d4304b9ce3a0abf4beb7b757a /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner | |
parent | VAMPIRE: complete first version of VampireModelInterpretation (diff) | |
download | VIATRA-Generator-4aee5bcc86b9e6b515fbbdac030df42147be7dc1.tar.gz VIATRA-Generator-4aee5bcc86b9e6b515fbbdac030df42147be7dc1.tar.zst VIATRA-Generator-4aee5bcc86b9e6b515fbbdac030df42147be7dc1.zip |
VAMPIRE: Implement wf constraint handling
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner')
17 files changed, 104 insertions, 9 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 a1d6f783..972af7b4 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 6ac0457b..071db3ce 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 f5991439..b1e3b95d 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 0d6c8b61..31cc2f43 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 659d4637..552bcd6c 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 927327e1..680bcfe1 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 d8fc0296..9cc64d7c 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 bc3caa3b..803b5fed 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 299c4e0c..0083e90f 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 da8c1d26..7e8b1703 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 adc3fff4..081757ca 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 2ab5b32f..3471f95b 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 41af19ec..1c707ca6 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 2b46d5c2..d8e3808c 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 58da7ccd..f8a65187 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 | |||
@@ -21,6 +21,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | |||
21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
24 | import com.google.common.base.Objects; | ||
24 | import com.google.common.collect.Iterables; | 25 | import com.google.common.collect.Iterables; |
25 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; |
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; | 27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; |
@@ -52,6 +53,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | |||
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 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; |
56 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl; | ||
55 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 57 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
56 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 58 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
57 | import java.util.Arrays; | 59 | import java.util.Arrays; |
@@ -117,7 +119,8 @@ public class Logic2VampireLanguageMapper { | |||
117 | } | 119 | } |
118 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | 120 | trace.relationDefinitions = this.collectRelationDefinitions(problem); |
119 | final Consumer<Relation> _function_3 = (Relation it) -> { | 121 | final Consumer<Relation> _function_3 = (Relation it) -> { |
120 | this.relationMapper.transformRelation(it, trace); | 122 | Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper(); |
123 | this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper); | ||
121 | }; | 124 | }; |
122 | problem.getRelations().forEach(_function_3); | 125 | problem.getRelations().forEach(_function_3); |
123 | this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); | 126 | this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); |
@@ -169,7 +172,9 @@ public class Logic2VampireLanguageMapper { | |||
169 | { | 172 | { |
170 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 173 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
171 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 174 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
172 | it.setName(this.support.toID(assertion.getName())); | 175 | String _name = assertion.getName(); |
176 | String _plus = ("assertion_" + _name); | ||
177 | it.setName(this.support.toID(_plus)); | ||
173 | it.setFofRole("axiom"); | 178 | it.setFofRole("axiom"); |
174 | it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); | 179 | it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); |
175 | }; | 180 | }; |
@@ -346,7 +351,13 @@ public class Logic2VampireLanguageMapper { | |||
346 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 351 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
347 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 352 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
348 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 353 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
349 | it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); | 354 | Class<? extends Relation> _class = relation.getClass(); |
355 | boolean _equals = Objects.equal(_class, RelationDeclarationImpl.class); | ||
356 | if (_equals) { | ||
357 | it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); | ||
358 | } else { | ||
359 | it.setConstant(CollectionsUtil.<RelationDefinition, VLSFunction>lookup(((RelationDefinition) relation), trace.relDef2Predicate).getConstant()); | ||
360 | } | ||
350 | EList<VLSTerm> _terms = it.getTerms(); | 361 | EList<VLSTerm> _terms = it.getTerms(); |
351 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { | 362 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { |
352 | return this.transformTerm(p, trace, variables); | 363 | 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/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index 4e77d45d..22df456b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java | |||
@@ -55,6 +55,10 @@ public class Logic2VampireLanguageMapperTrace { | |||
55 | 55 | ||
56 | public Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap<VLSFunction, RelationDeclaration>(); | 56 | public Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap<VLSFunction, RelationDeclaration>(); |
57 | 57 | ||
58 | public Map<RelationDefinition, VLSFunction> relDef2Predicate = new HashMap<RelationDefinition, VLSFunction>(); | ||
59 | |||
60 | public Map<VLSFunction, RelationDefinition> predicate2RelDef = new HashMap<VLSFunction, RelationDefinition>(); | ||
61 | |||
58 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | 62 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); |
59 | 63 | ||
60 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); | 64 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); |
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 143d3db5..c175c72a 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 | |||
@@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
@@ -17,11 +18,15 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | |||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
20 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 22 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
21 | import java.util.ArrayList; | 23 | import java.util.ArrayList; |
22 | import java.util.Arrays; | 24 | import java.util.Arrays; |
25 | import java.util.HashMap; | ||
23 | import java.util.List; | 26 | import java.util.List; |
27 | import java.util.Map; | ||
24 | import org.eclipse.emf.common.util.EList; | 28 | import org.eclipse.emf.common.util.EList; |
29 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
25 | import org.eclipse.xtext.xbase.lib.Conversions; | 30 | import org.eclipse.xtext.xbase.lib.Conversions; |
26 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | 31 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; |
27 | import org.eclipse.xtext.xbase.lib.Extension; | 32 | import org.eclipse.xtext.xbase.lib.Extension; |
@@ -41,7 +46,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
41 | this.base = base; | 46 | this.base = base; |
42 | } | 47 | } |
43 | 48 | ||
44 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { | 49 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { |
45 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); | 50 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); |
46 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | 51 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); |
47 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | 52 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; |
@@ -109,19 +114,94 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
109 | _formulas.add(comply); | 114 | _formulas.add(comply); |
110 | } | 115 | } |
111 | 116 | ||
112 | public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { | 117 | public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { |
118 | final Map<Variable, VLSVariable> relVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
119 | final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList(); | ||
120 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
121 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
122 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
123 | for (final Integer i : _doubleDotLessThan) { | ||
124 | { | ||
125 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
126 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
127 | it.setName(this.support.toIDMultiple("V", i.toString())); | ||
128 | }; | ||
129 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
130 | relVar2VLS.put(r.getVariables().get((i).intValue()), v); | ||
131 | vars.add(v); | ||
132 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
133 | final Type relType = ((ComplexTypeReference) _get).getReferred(); | ||
134 | final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v); | ||
135 | relVar2TypeDecComply.add(varTypeComply); | ||
136 | } | ||
137 | } | ||
138 | final String[] nameArray = r.getName().split(" "); | ||
139 | String relNameVar = ""; | ||
140 | int _length_1 = nameArray.length; | ||
141 | boolean _equals = (_length_1 == 3); | ||
142 | if (_equals) { | ||
143 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
144 | } else { | ||
145 | relNameVar = r.getName(); | ||
146 | } | ||
147 | final String relName = relNameVar; | ||
148 | final VLSTerm definition = mapper.transformTerm(r.getValue(), trace, relVar2VLS); | ||
149 | final VLSTerm compliance = this.support.unfoldAnd(relVar2TypeDecComply); | ||
150 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
151 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
152 | it.setLeft(compliance); | ||
153 | it.setRight(definition); | ||
154 | }; | ||
155 | final VLSAnd compDefn = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
156 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
157 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
158 | it.setName(this.support.toID(relName)); | ||
159 | it.setFofRole("axiom"); | ||
160 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
161 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
162 | for (final VLSVariable v : vars) { | ||
163 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
164 | VLSVariable _duplicate = this.support.duplicate(v); | ||
165 | _variables.add(_duplicate); | ||
166 | } | ||
167 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
168 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
169 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
170 | final Procedure1<VLSFunction> _function_4 = (VLSFunction it_3) -> { | ||
171 | it_3.setConstant(this.support.toIDMultiple("r", relName)); | ||
172 | for (final VLSVariable v_1 : vars) { | ||
173 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
174 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); | ||
175 | _terms.add(_duplicate_1); | ||
176 | } | ||
177 | }; | ||
178 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_4); | ||
179 | trace.relDef2Predicate.put(r, rel); | ||
180 | trace.predicate2RelDef.put(rel, r); | ||
181 | it_2.setLeft(this.support.duplicate(rel)); | ||
182 | it_2.setRight(compDefn); | ||
183 | }; | ||
184 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
185 | it_1.setOperand(_doubleArrow); | ||
186 | }; | ||
187 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
188 | it.setFofFormula(_doubleArrow); | ||
189 | }; | ||
190 | final VLSFofFormula relDef = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
191 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
192 | _formulas.add(relDef); | ||
113 | } | 193 | } |
114 | 194 | ||
115 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { | 195 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { |
116 | if (r instanceof RelationDeclaration) { | 196 | if (r instanceof RelationDeclaration) { |
117 | _transformRelation((RelationDeclaration)r, trace); | 197 | _transformRelation((RelationDeclaration)r, trace, mapper); |
118 | return; | 198 | return; |
119 | } else if (r instanceof RelationDefinition) { | 199 | } else if (r instanceof RelationDefinition) { |
120 | _transformRelation((RelationDefinition)r, trace); | 200 | _transformRelation((RelationDefinition)r, trace, mapper); |
121 | return; | 201 | return; |
122 | } else { | 202 | } else { |
123 | throw new IllegalArgumentException("Unhandled parameter types: " + | 203 | throw new IllegalArgumentException("Unhandled parameter types: " + |
124 | Arrays.<Object>asList(r, trace).toString()); | 204 | Arrays.<Object>asList(r, trace, mapper).toString()); |
125 | } | 205 | } |
126 | } | 206 | } |
127 | } | 207 | } |