diff options
author | 2019-09-08 16:12:55 -0400 | |
---|---|---|
committer | 2019-09-08 16:12:55 -0400 | |
commit | 71108d462c2695d917e87acea6f49d3f2954c6f4 (patch) | |
tree | 755962edeb635f46f1c860e2ff4dcc0235099597 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java | |
parent | VAMPIRE: complete first version of VampireModelInterpretation (diff) | |
download | VIATRA-Generator-71108d462c2695d917e87acea6f49d3f2954c6f4.tar.gz VIATRA-Generator-71108d462c2695d917e87acea6f49d3f2954c6f4.tar.zst VIATRA-Generator-71108d462c2695d917e87acea6f49d3f2954c6f4.zip |
VAMPIRE: Implement wf constraint handling
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java | 17 |
1 files changed, 14 insertions, 3 deletions
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); |