diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-08-28 05:56:34 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:41:36 -0400 |
commit | 4c34e22d23197ca6b03827a24e9339f88f82df5f (patch) | |
tree | 96450d132cc4bd6be7127a9bd11716e932bf3507 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire | |
parent | Pre-realisticBranchCreation Commit (diff) | |
download | VIATRA-Generator-4c34e22d23197ca6b03827a24e9339f88f82df5f.tar.gz VIATRA-Generator-4c34e22d23197ca6b03827a24e9339f88f82df5f.tar.zst VIATRA-Generator-4c34e22d23197ca6b03827a24e9339f88f82df5f.zip |
VAMPIRE: integrate local Vampire executeable #32
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire')
16 files changed, 72 insertions, 3 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 43712734..b9600616 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 b395b0c5..a7942958 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 d9d75887..410b47ed 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 | |||
@@ -20,7 +20,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | |||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
21 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 21 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
22 | import java.util.List; | 22 | import java.util.List; |
23 | import org.eclipse.emf.common.util.EList; | ||
24 | import org.eclipse.emf.ecore.EObject; | ||
23 | import org.eclipse.xtend2.lib.StringConcatenation; | 25 | import org.eclipse.xtend2.lib.StringConcatenation; |
26 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
24 | 27 | ||
25 | @SuppressWarnings("all") | 28 | @SuppressWarnings("all") |
26 | public class VampireSolver extends LogicReasoner { | 29 | public class VampireSolver extends LogicReasoner { |
@@ -36,7 +39,20 @@ public class VampireSolver extends LogicReasoner { | |||
36 | 39 | ||
37 | private final VampireHandler handler = new VampireHandler(); | 40 | private final VampireHandler handler = new VampireHandler(); |
38 | 41 | ||
39 | private final String fileName = "vampireProblem.tptp"; | 42 | private String fileName = "problem.tptp"; |
43 | |||
44 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace, final String location) { | ||
45 | try { | ||
46 | LogicResult _xblockexpression = null; | ||
47 | { | ||
48 | this.fileName = (location + this.fileName); | ||
49 | _xblockexpression = this.solve(problem, config, workspace); | ||
50 | } | ||
51 | return _xblockexpression; | ||
52 | } catch (Throwable _e) { | ||
53 | throw Exceptions.sneakyThrow(_e); | ||
54 | } | ||
55 | } | ||
40 | 56 | ||
41 | @Override | 57 | @Override |
42 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { | 58 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { |
@@ -55,6 +71,10 @@ public class VampireSolver extends LogicReasoner { | |||
55 | } | 71 | } |
56 | long _currentTimeMillis = System.currentTimeMillis(); | 72 | long _currentTimeMillis = System.currentTimeMillis(); |
57 | final long transformationTime = (_currentTimeMillis - transformationStart); | 73 | final long transformationTime = (_currentTimeMillis - transformationStart); |
74 | final long solverStart = System.currentTimeMillis(); | ||
75 | final EList<EObject> result2 = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | ||
76 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
77 | final long solvingTime = (_currentTimeMillis_1 - solverStart); | ||
58 | return null; | 78 | return null; |
59 | } | 79 | } |
60 | 80 | ||
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 3e571f5b..487f9569 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 6c116851..bd61b874 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 7ba8f303..2e58cecd 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index ad62b1f9..1b894303 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index 150ac835..4b7fd4bf 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index c181e53c..6626adf4 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 68d8cfb3..339baea9 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 1bef8bd1..868f30e7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index 9c4555e0..f8b35528 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 7bd6797c..08ffcb3b 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 6a10d85a..ffd37ea3 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 26460f68..9ddc7bd0 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/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java index 1cac2633..1479e6b7 100644 --- 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 | |||
@@ -2,11 +2,60 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | |||
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl; | ||
6 | import com.google.common.base.Objects; | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 7 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
8 | import java.io.BufferedReader; | ||
9 | import java.io.InputStream; | ||
10 | import java.io.InputStreamReader; | ||
11 | import java.util.List; | ||
12 | import java.util.Map; | ||
13 | import org.eclipse.emf.common.util.EList; | ||
14 | import org.eclipse.emf.common.util.URI; | ||
15 | import org.eclipse.emf.ecore.EObject; | ||
16 | import org.eclipse.emf.ecore.resource.Resource; | ||
17 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
18 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
19 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
6 | 20 | ||
7 | @SuppressWarnings("all") | 21 | @SuppressWarnings("all") |
8 | public class VampireHandler { | 22 | public class VampireHandler { |
9 | public Object callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration, final String vampireCode) { | 23 | public EList<EObject> callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) { |
10 | return null; | 24 | try { |
25 | EList<EObject> _xblockexpression = null; | ||
26 | { | ||
27 | final String CMD = "cmd /c "; | ||
28 | final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; | ||
29 | final String VAMPNAME = "vampire.exe"; | ||
30 | final String TEMPNAME = "TEMP.tptp"; | ||
31 | final String OPTION = " --mode casc_sat "; | ||
32 | final String SOLNNAME = "solution.tptp"; | ||
33 | final String PATH = "C:/cygwin64/bin"; | ||
34 | final URI wsURI = workspace.getWorkspaceURI(); | ||
35 | final String tempLoc = (wsURI + TEMPNAME); | ||
36 | String _plus = (wsURI + SOLNNAME); | ||
37 | final String solnLoc = (_plus + " "); | ||
38 | final String vampLoc = (VAMPDIR + VAMPNAME); | ||
39 | String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); | ||
40 | final Process p = Runtime.getRuntime().exec((((((CMD + vampLoc) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class))); | ||
41 | p.waitFor(); | ||
42 | InputStream _inputStream = p.getInputStream(); | ||
43 | InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream); | ||
44 | final BufferedReader reader = new BufferedReader(_inputStreamReader); | ||
45 | final List<String> output = CollectionLiterals.<String>newArrayList(); | ||
46 | String line = ""; | ||
47 | while ((!Objects.equal((line = reader.readLine()), null))) { | ||
48 | output.add((line + "\n")); | ||
49 | } | ||
50 | workspace.getFile(TEMPNAME).delete(); | ||
51 | Map<String, Object> _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap(); | ||
52 | VampireLanguageFactoryImpl _vampireLanguageFactoryImpl = new VampireLanguageFactoryImpl(); | ||
53 | _extensionToFactoryMap.put("*", _vampireLanguageFactoryImpl); | ||
54 | _xblockexpression = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents(); | ||
55 | } | ||
56 | return _xblockexpression; | ||
57 | } catch (Throwable _e) { | ||
58 | throw Exceptions.sneakyThrow(_e); | ||
59 | } | ||
11 | } | 60 | } |
12 | } | 61 | } |