diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-02-01 16:03:30 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:06:28 -0400 |
commit | 57e614aabedc176ba9965d0ca5e6daa23c5f4758 (patch) | |
tree | 16806454dff463419af99b14f6abfab3d1fa5291 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse | |
parent | FAM MM transformation works (diff) | |
download | VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.gz VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.zst VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.zip |
Fix FAM Test. Begin Grammar Fix.
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse')
22 files changed, 181 insertions, 26 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 b9a5c4e7..462a940b 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 a9926cdc..d8b8ca61 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/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore index 9efd2ac5..70f60102 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore | |||
@@ -2,3 +2,9 @@ | |||
2 | /.TypeMappingTechnique.java._trace | 2 | /.TypeMappingTechnique.java._trace |
3 | /.VampireBackendSolver.java._trace | 3 | /.VampireBackendSolver.java._trace |
4 | /.VampireSolverConfiguration.java._trace | 4 | /.VampireSolverConfiguration.java._trace |
5 | /.VampireAnalyzerConfiguration.xtendbin | ||
6 | /.VampireSolver.xtendbin | ||
7 | /TypeMappingTechnique.java | ||
8 | /VampireBackendSolver.java | ||
9 | /VampireSolver.java | ||
10 | /VampireSolverConfiguration.java | ||
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 81cae109..e1a1ca6e 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 | |||
@@ -6,6 +6,8 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | |||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes; | 8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes; |
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; |
@@ -17,10 +19,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | |||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
19 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 21 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
20 | import java.io.PrintWriter; | ||
21 | import java.util.List; | 22 | import java.util.List; |
22 | import org.eclipse.xtend2.lib.StringConcatenation; | 23 | import org.eclipse.xtend2.lib.StringConcatenation; |
23 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
24 | 24 | ||
25 | @SuppressWarnings("all") | 25 | @SuppressWarnings("all") |
26 | public class VampireSolver extends LogicReasoner { | 26 | public class VampireSolver extends LogicReasoner { |
@@ -32,32 +32,28 @@ public class VampireSolver extends LogicReasoner { | |||
32 | 32 | ||
33 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); | 33 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); |
34 | 34 | ||
35 | private final String fileName = "problem.tptp"; | 35 | private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper(); |
36 | |||
37 | private final VampireHandler handler = new VampireHandler(); | ||
38 | |||
39 | private final String fileName = "vampireProblem.tptp"; | ||
36 | 40 | ||
37 | @Override | 41 | @Override |
38 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration configuration, final ReasonerWorkspace workspace) throws LogicReasonerException { | 42 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { |
39 | try { | 43 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); |
40 | final VampireSolverConfiguration vampireConfig = this.asConfig(configuration); | 44 | final long transformationStart = System.currentTimeMillis(); |
41 | final long transformationStart = System.currentTimeMillis(); | 45 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); |
42 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | 46 | final VampireModel vampireProblem = result.getOutput(); |
43 | final VampireModel vampireProblem = result.getOutput(); | 47 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); |
44 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | 48 | String fileURI = null; |
45 | String fileURI = null; | 49 | String vampireCode = null; |
46 | String vampireCode = null; | 50 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); |
47 | if (vampireConfig.writeToFile) { | 51 | if (vampireConfig.writeToFile) { |
48 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); | 52 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); |
49 | } else { | ||
50 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); | ||
51 | } | ||
52 | long _currentTimeMillis = System.currentTimeMillis(); | ||
53 | final long transformationTime = (_currentTimeMillis - transformationStart); | ||
54 | final PrintWriter out = new PrintWriter("output/files/vampireCode.tptp"); | ||
55 | out.println(vampireCode); | ||
56 | out.close(); | ||
57 | return null; | ||
58 | } catch (Throwable _e) { | ||
59 | throw Exceptions.sneakyThrow(_e); | ||
60 | } | 53 | } |
54 | long _currentTimeMillis = System.currentTimeMillis(); | ||
55 | final long transformationTime = (_currentTimeMillis - transformationStart); | ||
56 | return null; | ||
61 | } | 57 | } |
62 | 58 | ||
63 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | 59 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { |
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 e4083dc1..d248b361 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 bbda5634..d747e8ab 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 6c3f3a91..4dc095c0 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 9da7459d..9a948c6f 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_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 89400bab..4ef4809b 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 6113caa7..0f4acafe 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 d5504038..7d6865bb 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 3586a020..6db26bf7 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 new file mode 100644 index 00000000..8c96afa7 --- /dev/null +++ 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 new file mode 100644 index 00000000..2427721d --- /dev/null +++ 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 16b681bb..d2c93ab4 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 c2f817a5..28c5d0f7 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 d27ff186..3d29fb07 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 | |||
@@ -9,3 +9,31 @@ | |||
9 | /.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java._trace | 9 | /.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java._trace |
10 | /.Logic2VampireLanguageMapper_Support.java._trace | 10 | /.Logic2VampireLanguageMapper_Support.java._trace |
11 | /.Logic2VampireLanguageMapper_RelationMapper.java._trace | 11 | /.Logic2VampireLanguageMapper_RelationMapper.java._trace |
12 | /.Logic2VampireLanguageMapper.xtendbin | ||
13 | /.Logic2VampireLanguageMapperTrace.xtendbin | ||
14 | /.Logic2VampireLanguageMapper_ConstantMapper.xtendbin | ||
15 | /.Logic2VampireLanguageMapper_RelationMapper.xtendbin | ||
16 | /.Logic2VampireLanguageMapper_Support.xtendbin | ||
17 | /.Logic2VampireLanguageMapper_TypeMapper.xtendbin | ||
18 | /.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin | ||
19 | /.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin | ||
20 | /.VampireModelInterpretation_TypeInterpretation.xtendbin | ||
21 | /.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin | ||
22 | /Logic2VampireLanguageMapper.java | ||
23 | /Logic2VampireLanguageMapperTrace.java | ||
24 | /Logic2VampireLanguageMapper_ConstantMapper.java | ||
25 | /Logic2VampireLanguageMapper_RelationMapper.java | ||
26 | /Logic2VampireLanguageMapper_Support.java | ||
27 | /Logic2VampireLanguageMapper_TypeMapper.java | ||
28 | /Logic2VampireLanguageMapper_TypeMapperTrace.java | ||
29 | /Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java | ||
30 | /Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java | ||
31 | /VampireModelInterpretation_TypeInterpretation.java | ||
32 | /VampireModelInterpretation_TypeInterpretation_FilteredTypes.java | ||
33 | /.Vampire2LogicMapper.java._trace | ||
34 | /.VampireHandler.java._trace | ||
35 | /.MonitoredVampireSolution.java._trace | ||
36 | /.SolverConfiguration.java._trace | ||
37 | /.VampireSolverException.java._trace | ||
38 | /.VampireSolutionModel.java._trace | ||
39 | /.VampireCallerWithTimeout.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 b2dd06ef..a1d80e58 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 | |||
@@ -90,7 +90,7 @@ public class Logic2VampireLanguageMapper { | |||
90 | this.typeMapper = typeMapper; | 90 | this.typeMapper = typeMapper; |
91 | } | 91 | } |
92 | 92 | ||
93 | public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration configuration) { | 93 | public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) { |
94 | VLSComment _createVLSComment = this.factory.createVLSComment(); | 94 | VLSComment _createVLSComment = this.factory.createVLSComment(); |
95 | final Procedure1<VLSComment> _function = (VLSComment it) -> { | 95 | final Procedure1<VLSComment> _function = (VLSComment it) -> { |
96 | it.setComment("This is an initial Test Comment"); | 96 | it.setComment("This is an initial Test Comment"); |
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 new file mode 100644 index 00000000..f4380894 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java | |||
@@ -0,0 +1,59 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
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") | ||
14 | 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 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java new file mode 100644 index 00000000..1cac2633 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java | |||
@@ -0,0 +1,12 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | ||
6 | |||
7 | @SuppressWarnings("all") | ||
8 | public class VampireHandler { | ||
9 | public Object callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration, final String vampireCode) { | ||
10 | return null; | ||
11 | } | ||
12 | } | ||
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 new file mode 100644 index 00000000..c665b9a6 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java | |||
@@ -0,0 +1,35 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import org.eclipse.xtend.lib.annotations.Data; | ||
4 | import org.eclipse.xtext.xbase.lib.Pure; | ||
5 | import org.eclipse.xtext.xbase.lib.util.ToStringBuilder; | ||
6 | |||
7 | @Data | ||
8 | @SuppressWarnings("all") | ||
9 | public class VampireSolutionModel { | ||
10 | @Override | ||
11 | @Pure | ||
12 | public int hashCode() { | ||
13 | int result = 1; | ||
14 | return result; | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | @Pure | ||
19 | public boolean equals(final Object obj) { | ||
20 | if (this == obj) | ||
21 | return true; | ||
22 | if (obj == null) | ||
23 | return false; | ||
24 | if (getClass() != obj.getClass()) | ||
25 | return false; | ||
26 | return true; | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | @Pure | ||
31 | public String toString() { | ||
32 | ToStringBuilder b = new ToStringBuilder(this); | ||
33 | return b.toString(); | ||
34 | } | ||
35 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java new file mode 100644 index 00000000..b96df82a --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java | |||
@@ -0,0 +1,19 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import java.util.List; | ||
4 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
5 | |||
6 | @SuppressWarnings("all") | ||
7 | public class VampireSolverException extends Exception { | ||
8 | public VampireSolverException(final String s) { | ||
9 | super(s); | ||
10 | } | ||
11 | |||
12 | public VampireSolverException(final String s, final Exception e) { | ||
13 | super(s, e); | ||
14 | } | ||
15 | |||
16 | public VampireSolverException(final String s, final List<String> errors, final Exception e) { | ||
17 | super(((s + "\n") + IterableExtensions.join(errors, "\n")), e); | ||
18 | } | ||
19 | } | ||