diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-04 17:31:16 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:18:56 -0400 |
commit | 9643b7b7a735afc408ca6a172e2719653553627a (patch) | |
tree | a608396a89759a3d3d6ead5b659c23612ff9d56c /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill | |
parent | complete vsconfig files #19 (diff) | |
download | VIATRA-Generator-9643b7b7a735afc408ca6a172e2719653553627a.tar.gz VIATRA-Generator-9643b7b7a735afc408ca6a172e2719653553627a.tar.zst VIATRA-Generator-9643b7b7a735afc408ca6a172e2719653553627a.zip |
Begin handing of scope and fix type definitions.
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill')
25 files changed, 174 insertions, 138 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 462a940b..9a2a1b15 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 d8b8ca61..ce05b92c 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/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java index e1a1ca6e..1846ba2e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java | |||
@@ -10,6 +10,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | |||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException; | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException; |
@@ -30,7 +31,8 @@ public class VampireSolver extends LogicReasoner { | |||
30 | VampireLanguageStandaloneSetup.doSetup(); | 31 | VampireLanguageStandaloneSetup.doSetup(); |
31 | } | 32 | } |
32 | 33 | ||
33 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); | 34 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper( |
35 | new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); | ||
34 | 36 | ||
35 | private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper(); | 37 | private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper(); |
36 | 38 | ||
@@ -48,7 +50,9 @@ public class VampireSolver extends LogicReasoner { | |||
48 | String fileURI = null; | 50 | String fileURI = null; |
49 | String vampireCode = null; | 51 | String vampireCode = null; |
50 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); | 52 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); |
51 | if (vampireConfig.writeToFile) { | 53 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || |
54 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); | ||
55 | if (writeFile) { | ||
52 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); | 56 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); |
53 | } | 57 | } |
54 | long _currentTimeMillis = System.currentTimeMillis(); | 58 | long _currentTimeMillis = System.currentTimeMillis(); |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java index d392016e..1f6b3d42 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java | |||
@@ -4,7 +4,4 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | |||
4 | 4 | ||
5 | @SuppressWarnings("all") | 5 | @SuppressWarnings("all") |
6 | public class VampireSolverConfiguration extends LogicSolverConfiguration { | 6 | public class VampireSolverConfiguration extends LogicSolverConfiguration { |
7 | public int symmetry = 0; | ||
8 | |||
9 | public boolean writeToFile = false; | ||
10 | } | 7 | } |
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 d248b361..379d0683 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 d747e8ab..76dd192f 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 4dc095c0..936ab9ca 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 9a948c6f..e0f442f5 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 new file mode 100644 index 00000000..493ff288 --- /dev/null +++ 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 4ef4809b..13281767 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 0f4acafe..1a777880 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 7d6865bb..e8658e7b 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 6db26bf7..aec1688a 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 8c96afa7..e77b9866 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 2427721d..100a52b8 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 d2c93ab4..231c1995 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 28c5d0f7..b67a307c 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/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore index 3d29fb07..ec8107e8 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore | |||
@@ -37,3 +37,4 @@ | |||
37 | /.VampireSolverException.java._trace | 37 | /.VampireSolverException.java._trace |
38 | /.VampireSolutionModel.java._trace | 38 | /.VampireSolutionModel.java._trace |
39 | /.VampireCallerWithTimeout.java._trace | 39 | /.VampireCallerWithTimeout.java._trace |
40 | /.Logic2VampireLanguageMapper_ScopeMapper.java._trace | ||
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 a1d80e58..89c9637e 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 | |||
@@ -4,6 +4,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | |||
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_ConstantMapper; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; | 9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; |
@@ -84,6 +85,9 @@ public class Logic2VampireLanguageMapper { | |||
84 | private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); | 85 | private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); |
85 | 86 | ||
86 | @Accessors(AccessorType.PUBLIC_GETTER) | 87 | @Accessors(AccessorType.PUBLIC_GETTER) |
88 | private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this); | ||
89 | |||
90 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
87 | private final Logic2VampireLanguageMapper_TypeMapper typeMapper; | 91 | private final Logic2VampireLanguageMapper_TypeMapper typeMapper; |
88 | 92 | ||
89 | public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) { | 93 | public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) { |
@@ -112,6 +116,7 @@ public class Logic2VampireLanguageMapper { | |||
112 | if (_not) { | 116 | if (_not) { |
113 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); | 117 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); |
114 | } | 118 | } |
119 | this.scopeMapper.transformScope(config, trace); | ||
115 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | 120 | trace.constantDefinitions = this.collectConstantDefinitions(problem); |
116 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | 121 | trace.relationDefinitions = this.collectRelationDefinitions(problem); |
117 | final Consumer<Relation> _function_3 = (Relation it) -> { | 122 | final Consumer<Relation> _function_3 = (Relation it) -> { |
@@ -316,13 +321,13 @@ public class Logic2VampireLanguageMapper { | |||
316 | 321 | ||
317 | /** | 322 | /** |
318 | * def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | 323 | * def dispatch protected VLSTerm transformSymbolicReference(Relation relation, |
319 | * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 324 | * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, |
320 | * Map<Variable, VLSVariable> variables) { | 325 | * Map<Variable, VLSVariable> variables) { |
321 | * if (trace.relationDefinitions.containsKey(relation)) { | 326 | * if (trace.relationDefinitions.containsKey(relation)) { |
322 | * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), | 327 | * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), |
323 | * parameterSubstitutions, trace, variables) | 328 | * parameterSubstitutions, trace, variables) |
324 | * } | 329 | * } |
325 | * else { | 330 | * else { |
326 | * // if (relationMapper.transformToHostedField(relation, trace)) { | 331 | * // if (relationMapper.transformToHostedField(relation, trace)) { |
327 | * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) | 332 | * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) |
328 | * // // R(a,b) => | 333 | * // // R(a,b) => |
@@ -348,7 +353,7 @@ public class Logic2VampireLanguageMapper { | |||
348 | * // rightOperand = target | 353 | * // rightOperand = target |
349 | * // ] | 354 | * // ] |
350 | * // } | 355 | * // } |
351 | * } | 356 | * } |
352 | * } | 357 | * } |
353 | */ | 358 | */ |
354 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 359 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
@@ -436,6 +441,11 @@ public class Logic2VampireLanguageMapper { | |||
436 | } | 441 | } |
437 | 442 | ||
438 | @Pure | 443 | @Pure |
444 | public Logic2VampireLanguageMapper_ScopeMapper getScopeMapper() { | ||
445 | return this.scopeMapper; | ||
446 | } | ||
447 | |||
448 | @Pure | ||
439 | public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() { | 449 | public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() { |
440 | return this.typeMapper; | 450 | return this.typeMapper; |
441 | } | 451 | } |
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 new file mode 100644 index 00000000..86d8b648 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |||
@@ -0,0 +1,96 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
14 | import java.util.List; | ||
15 | import org.eclipse.emf.common.util.EList; | ||
16 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
17 | import org.eclipse.xtext.xbase.lib.Extension; | ||
18 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
19 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
20 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
21 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
22 | |||
23 | @SuppressWarnings("all") | ||
24 | public class Logic2VampireLanguageMapper_ScopeMapper { | ||
25 | @Extension | ||
26 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
27 | |||
28 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
29 | |||
30 | private final Logic2VampireLanguageMapper base; | ||
31 | |||
32 | public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) { | ||
33 | this.base = base; | ||
34 | } | ||
35 | |||
36 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | ||
37 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
38 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
39 | it.setName("A"); | ||
40 | }; | ||
41 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
42 | final List<VLSConstant> instances = CollectionLiterals.<VLSConstant>newArrayList(); | ||
43 | for (int i = 0; (i < config.typeScopes.minNewElements); i++) { | ||
44 | { | ||
45 | final int num = (i + 1); | ||
46 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
47 | final Procedure1<VLSConstant> _function_1 = (VLSConstant it) -> { | ||
48 | it.setName(("o" + Integer.valueOf(num))); | ||
49 | }; | ||
50 | final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); | ||
51 | instances.add(cst); | ||
52 | } | ||
53 | } | ||
54 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
55 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
56 | it.setName("typeScope"); | ||
57 | it.setFofRole("axiom"); | ||
58 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
59 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
60 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
61 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
62 | _variables.add(_duplicate); | ||
63 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
64 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | ||
65 | it_2.setLeft(this.support.topLevelTypeFunc()); | ||
66 | final Function1<VLSConstant, VLSEquality> _function_4 = (VLSConstant i) -> { | ||
67 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
68 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { | ||
69 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
70 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { | ||
71 | it_4.setName(variable.getName()); | ||
72 | }; | ||
73 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_6); | ||
74 | it_3.setLeft(_doubleArrow); | ||
75 | it_3.setRight(i); | ||
76 | }; | ||
77 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); | ||
78 | }; | ||
79 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4))); | ||
80 | }; | ||
81 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | ||
82 | it_1.setOperand(_doubleArrow); | ||
83 | }; | ||
84 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
85 | it.setFofFormula(_doubleArrow); | ||
86 | }; | ||
87 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
88 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
89 | _formulas.add(cstDec); | ||
90 | } | ||
91 | |||
92 | public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | ||
93 | _transformScope(config, trace); | ||
94 | return; | ||
95 | } | ||
96 | } | ||
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 e1be7df5..b111732f 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 | |||
@@ -50,6 +50,29 @@ public class Logic2VampireLanguageMapper_Support { | |||
50 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_"); | 50 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_"); |
51 | } | 51 | } |
52 | 52 | ||
53 | protected VLSVariable duplicate(final VLSVariable vrbl) { | ||
54 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
55 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
56 | it.setName(vrbl.getName()); | ||
57 | }; | ||
58 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
59 | } | ||
60 | |||
61 | protected VLSFunction topLevelTypeFunc() { | ||
62 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
63 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
64 | it.setConstant("object"); | ||
65 | EList<VLSTerm> _terms = it.getTerms(); | ||
66 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
67 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it_1) -> { | ||
68 | it_1.setName("A"); | ||
69 | }; | ||
70 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
71 | _terms.add(_doubleArrow); | ||
72 | }; | ||
73 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
74 | } | ||
75 | |||
53 | protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) { | 76 | protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) { |
54 | int _size = operands.size(); | 77 | int _size = operands.size(); |
55 | boolean _equals = (_size == 1); | 78 | boolean _equals = (_size == 1); |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java index d674ac71..f7c6cb70 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java | |||
@@ -1,7 +1,6 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; |
@@ -13,7 +12,7 @@ import java.util.Map; | |||
13 | public class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace { | 12 | public class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace { |
14 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); | 13 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); |
15 | 14 | ||
16 | public final Map<DefinedElement, VLSEquality> definedElement2Declaration = new HashMap<DefinedElement, VLSEquality>(); | 15 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); |
17 | 16 | ||
18 | public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>(); | 17 | public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>(); |
19 | 18 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java index 0f5e4e7a..71e98871 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java | |||
@@ -7,7 +7,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage | |||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes; | 7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; | 8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
@@ -27,10 +26,10 @@ import java.util.ArrayList; | |||
27 | import java.util.Collection; | 26 | import java.util.Collection; |
28 | import java.util.List; | 27 | import java.util.List; |
29 | import org.eclipse.emf.common.util.EList; | 28 | import org.eclipse.emf.common.util.EList; |
29 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
30 | import org.eclipse.xtext.xbase.lib.Extension; | 30 | import org.eclipse.xtext.xbase.lib.Extension; |
31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | 32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; |
33 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
34 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 33 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
35 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 34 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
36 | 35 | ||
@@ -58,14 +57,10 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
58 | { | 57 | { |
59 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 58 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
60 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 59 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
61 | it.setConstant(this.support.toIDMultiple("type", type.getName())); | 60 | it.setConstant(this.support.toIDMultiple("t", type.getName())); |
62 | EList<VLSTerm> _terms = it.getTerms(); | 61 | EList<VLSTerm> _terms = it.getTerms(); |
63 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 62 | VLSVariable _duplicate = this.support.duplicate(variable); |
64 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 63 | _terms.add(_duplicate); |
65 | it_1.setName(variable.getName()); | ||
66 | }; | ||
67 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
68 | _terms.add(_doubleArrow); | ||
69 | }; | 64 | }; |
70 | final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 65 | final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); |
71 | typeTrace.type2Predicate.put(type, typePred); | 66 | typeTrace.type2Predicate.put(type, typePred); |
@@ -74,6 +69,22 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
74 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); | 69 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); |
75 | for (final TypeDefinition type_1 : _filter) { | 70 | for (final TypeDefinition type_1 : _filter) { |
76 | { | 71 | { |
72 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); | ||
73 | EList<DefinedElement> _elements = type_1.getElements(); | ||
74 | for (final DefinedElement e : _elements) { | ||
75 | { | ||
76 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
77 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
78 | it.setConstant(this.support.toIDMultiple("e", e.getName(), type_1.getName())); | ||
79 | EList<VLSTerm> _terms = it.getTerms(); | ||
80 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
81 | _terms.add(_duplicate); | ||
82 | }; | ||
83 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
84 | typeTrace.element2Predicate.put(e, enumElemPred); | ||
85 | orElems.add(enumElemPred); | ||
86 | } | ||
87 | } | ||
77 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 88 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
78 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 89 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
79 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName())); | 90 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName())); |
@@ -81,53 +92,15 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
81 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 92 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
82 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 93 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
83 | EList<VLSVariable> _variables = it_1.getVariables(); | 94 | EList<VLSVariable> _variables = it_1.getVariables(); |
84 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 95 | VLSVariable _duplicate = this.support.duplicate(variable); |
85 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> { | 96 | _variables.add(_duplicate); |
86 | it_2.setName(variable.getName()); | ||
87 | }; | ||
88 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3); | ||
89 | _variables.add(_doubleArrow); | ||
90 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 97 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
91 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | 98 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { |
92 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 99 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate)); |
93 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_3) -> { | 100 | it_2.setRight(this.support.unfoldOr(orElems)); |
94 | it_3.setConstant(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate).getConstant()); | ||
95 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
96 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
97 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { | ||
98 | it_4.setName("A"); | ||
99 | }; | ||
100 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_6); | ||
101 | _terms.add(_doubleArrow_1); | ||
102 | }; | ||
103 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | ||
104 | it_2.setLeft(_doubleArrow_1); | ||
105 | CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate); | ||
106 | final Function1<DefinedElement, VLSEquality> _function_6 = (DefinedElement e) -> { | ||
107 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
108 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { | ||
109 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
110 | final Procedure1<VLSVariable> _function_8 = (VLSVariable it_4) -> { | ||
111 | it_4.setName(variable.getName()); | ||
112 | }; | ||
113 | VLSVariable _doubleArrow_2 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_8); | ||
114 | it_3.setLeft(_doubleArrow_2); | ||
115 | VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); | ||
116 | final Procedure1<VLSDoubleQuote> _function_9 = (VLSDoubleQuote it_4) -> { | ||
117 | String _name = e.getName(); | ||
118 | String _plus = ("\"a" + _name); | ||
119 | String _plus_1 = (_plus + "\""); | ||
120 | it_4.setValue(_plus_1); | ||
121 | }; | ||
122 | VLSDoubleQuote _doubleArrow_3 = ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function_9); | ||
123 | it_3.setRight(_doubleArrow_3); | ||
124 | }; | ||
125 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); | ||
126 | }; | ||
127 | it_2.setRight(this.support.unfoldOr(ListExtensions.<DefinedElement, VLSEquality>map(type_1.getElements(), _function_6))); | ||
128 | }; | 101 | }; |
129 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | 102 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); |
130 | it_1.setOperand(_doubleArrow_1); | 103 | it_1.setOperand(_doubleArrow); |
131 | }; | 104 | }; |
132 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | 105 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); |
133 | it.setFofFormula(_doubleArrow); | 106 | it.setFofFormula(_doubleArrow); |
@@ -201,19 +174,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log | |||
201 | _variables.add(_doubleArrow); | 174 | _variables.add(_doubleArrow); |
202 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 175 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
203 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | 176 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { |
204 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 177 | it_2.setLeft(this.support.topLevelTypeFunc()); |
205 | final Procedure1<VLSFunction> _function_6 = (VLSFunction it_3) -> { | ||
206 | it_3.setConstant("object"); | ||
207 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
208 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
209 | final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> { | ||
210 | it_4.setName("A"); | ||
211 | }; | ||
212 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_7); | ||
213 | _terms.add(_doubleArrow_1); | ||
214 | }; | ||
215 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_6); | ||
216 | it_2.setLeft(_doubleArrow_1); | ||
217 | Collection<VLSTerm> _values = typeTrace.type2And.values(); | 178 | Collection<VLSTerm> _values = typeTrace.type2And.values(); |
218 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | 179 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); |
219 | it_2.setRight(this.support.unfoldOr(_arrayList)); | 180 | it_2.setRight(this.support.unfoldOr(_arrayList)); |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java index f4380894..f4b5a1d2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java | |||
@@ -1,59 +1,5 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireSolutionModel; | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; | ||
9 | import org.eclipse.xtext.xbase.lib.Extension; | ||
10 | import org.eclipse.xtext.xbase.lib.Functions.Function2; | ||
11 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
12 | |||
13 | @SuppressWarnings("all") | 3 | @SuppressWarnings("all") |
14 | public class Vampire2LogicMapper { | 4 | public class Vampire2LogicMapper { |
15 | @Extension | ||
16 | private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE; | ||
17 | |||
18 | public LogicResult transformOutput(final LogicProblem problem, final int requiredNumberOfSolution, final VampireSolutionModel vampireSolution, final Logic2VampireLanguageMapperTrace trace, final long transformationTime) { | ||
19 | throw new Error("Unresolved compilation problems:" | ||
20 | + "\nThe method or field aswers is undefined for the type VampireSolutionModel" | ||
21 | + "\nThe method or field key is undefined for the type Object" | ||
22 | + "\nThe method or field monitoredAlloySolution is undefined" | ||
23 | + "\nThe method or field monitoredAlloySolution is undefined" | ||
24 | + "\nThe method or field monitoredAlloySolution is undefined" | ||
25 | + "\nThe method or field monitoredAlloySolution is undefined" | ||
26 | + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution" | ||
27 | + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution" | ||
28 | + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution" | ||
29 | + "\nmap cannot be resolved" | ||
30 | + "\ntoList cannot be resolved" | ||
31 | + "\nfinishedBeforeTimeout cannot be resolved" | ||
32 | + "\n! cannot be resolved" | ||
33 | + "\nlast cannot be resolved" | ||
34 | + "\nsatisfiable cannot be resolved" | ||
35 | + "\n|| cannot be resolved"); | ||
36 | } | ||
37 | |||
38 | public Statistics transformStatistics(final /* MonitoredAlloySolution */Object solution, final long transformationTime) { | ||
39 | throw new Error("Unresolved compilation problems:" | ||
40 | + "\nCannot cast from Object to int" | ||
41 | + "\nCannot cast from Object to int" | ||
42 | + "\naswers cannot be resolved" | ||
43 | + "\nsize cannot be resolved" | ||
44 | + "\naswers cannot be resolved" | ||
45 | + "\nget cannot be resolved" | ||
46 | + "\nvalue cannot be resolved" | ||
47 | + "\nintValue cannot be resolved" | ||
48 | + "\nkodkodTime cannot be resolved" | ||
49 | + "\nkodkodTime cannot be resolved" | ||
50 | + "\nwarnings cannot be resolved"); | ||
51 | } | ||
52 | |||
53 | public Long sum(final Iterable<Long> ints) { | ||
54 | final Function2<Long, Long, Long> _function = (Long p1, Long p2) -> { | ||
55 | return Long.valueOf(((p1).longValue() + (p2).longValue())); | ||
56 | }; | ||
57 | return IterableExtensions.<Long>reduce(ints, _function); | ||
58 | } | ||
59 | } | 5 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java index c665b9a6..3c43c4ea 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java | |||
@@ -10,8 +10,7 @@ public class VampireSolutionModel { | |||
10 | @Override | 10 | @Override |
11 | @Pure | 11 | @Pure |
12 | public int hashCode() { | 12 | public int hashCode() { |
13 | int result = 1; | 13 | return 1; |
14 | return result; | ||
15 | } | 14 | } |
16 | 15 | ||
17 | @Override | 16 | @Override |