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/reasoner/builder/VampireHandler.java | |
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/reasoner/builder/VampireHandler.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java | 53 |
1 files changed, 51 insertions, 2 deletions
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 | } |