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 | |
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')
20 files changed, 155 insertions, 36 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/lib/putVampireHere b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/lib/putVampireHere new file mode 100644 index 00000000..cc0bca68 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/lib/putVampireHere | |||
@@ -0,0 +1,2 @@ | |||
1 | put the Vampire executeable in this folder. | ||
2 | rename it to "vampire.exe" | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/lib/vampire.exe b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/lib/vampire.exe new file mode 100644 index 00000000..51b44f82 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/lib/vampire.exe | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend index 1d56892e..6bb49080 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend | |||
@@ -27,7 +27,12 @@ class VampireSolver extends LogicReasoner { | |||
27 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | 27 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper |
28 | val VampireHandler handler = new VampireHandler | 28 | val VampireHandler handler = new VampireHandler |
29 | 29 | ||
30 | val fileName = "vampireProblem.tptp" | 30 | var fileName = "problem.tptp" |
31 | |||
32 | def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { | ||
33 | fileName = location + fileName | ||
34 | solve(problem, config, workspace) | ||
35 | } | ||
31 | 36 | ||
32 | override solve(LogicProblem problem, LogicSolverConfiguration config, | 37 | override solve(LogicProblem problem, LogicSolverConfiguration config, |
33 | ReasonerWorkspace workspace) throws LogicReasonerException { | 38 | ReasonerWorkspace workspace) throws LogicReasonerException { |
@@ -54,26 +59,21 @@ class VampireSolver extends LogicReasoner { | |||
54 | // Result as String | 59 | // Result as String |
55 | val transformationTime = System.currentTimeMillis - transformationStart | 60 | val transformationTime = System.currentTimeMillis - transformationStart |
56 | // Finish: Logic -> Vampire mapping | 61 | // Finish: Logic -> Vampire mapping |
57 | /* | 62 | // Start: Solving .tptp problem |
58 | * // Start: Solving Alloy problem | 63 | val solverStart = System.currentTimeMillis |
59 | * val solverStart = System.currentTimeMillis | 64 | // Calling Solver (Currently Manually) |
60 | * //Calling Solver (Currently Manually) | 65 | val result2 = handler.callSolver(vampireProblem, workspace, vampireConfig) |
61 | * val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode) | 66 | // val result2 = null |
62 | * // val result2 = null | 67 | val solvingTime = System.currentTimeMillis - solverStart |
63 | * //TODO | 68 | // TODO |
64 | * //Backwards Mapper | 69 | // val backTransformationStart = System.currentTimeMillis |
65 | * val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | 70 | // // Backwards Mapper |
66 | * | 71 | // val logicResult = backwardMapper.transformOutput(problem, config.solutionScope.numberOfRequiredSolution, |
67 | * val solverFinish = System.currentTimeMillis-solverStart | 72 | // result2, forwardTrace, transformationTime) |
68 | * // Finish: Solving Alloy problem | 73 | // |
69 | * | 74 | // val backTransformationTime = System.currentTimeMillis - backTransformationStart |
70 | * if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) | 75 | // Finish: Solving Alloy problem |
71 | * | 76 | return null |
72 | * return logicResult | ||
73 | * | ||
74 | /*/ | ||
75 | return null // for now | ||
76 | // */ | ||
77 | } | 77 | } |
78 | 78 | ||
79 | def asConfig(LogicSolverConfiguration configuration) { | 79 | def asConfig(LogicSolverConfiguration configuration) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend index aefa1a7e..274396ee 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | |||
@@ -1,21 +1,14 @@ | |||
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.VampireBackendSolver | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
6 | import com.google.common.util.concurrent.SimpleTimeLimiter | ||
7 | import com.google.common.util.concurrent.UncheckedTimeoutException | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
9 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 5 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
10 | import java.util.ArrayList | 6 | import java.io.BufferedReader |
11 | import java.util.HashMap | 7 | import java.io.InputStreamReader |
12 | import java.util.LinkedList | ||
13 | import java.util.List | 8 | import java.util.List |
14 | import java.util.Map | 9 | import org.eclipse.emf.ecore.resource.Resource |
15 | import java.util.concurrent.Callable | ||
16 | import java.util.concurrent.TimeUnit | ||
17 | import org.eclipse.emf.common.command.Command | ||
18 | import org.eclipse.xtend.lib.annotations.Data | 10 | import org.eclipse.xtend.lib.annotations.Data |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl | ||
19 | 12 | ||
20 | class VampireSolverException extends Exception{ | 13 | class VampireSolverException extends Exception{ |
21 | new(String s) { super(s) } | 14 | new(String s) { super(s) } |
@@ -39,7 +32,62 @@ class VampireHandler { | |||
39 | 32 | ||
40 | //val fileName = "problem.als" | 33 | //val fileName = "problem.als" |
41 | 34 | ||
42 | public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration,String vampireCode) { | 35 | public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration) { |
36 | |||
37 | val CMD = "cmd /c " | ||
38 | val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" | ||
39 | val VAMPNAME = "vampire.exe" | ||
40 | val TEMPNAME = "TEMP.tptp" | ||
41 | val OPTION = " --mode casc_sat " | ||
42 | val SOLNNAME = "solution.tptp" | ||
43 | val PATH = "C:/cygwin64/bin" | ||
44 | |||
45 | val wsURI = workspace.workspaceURI | ||
46 | val tempLoc = wsURI + TEMPNAME | ||
47 | val solnLoc = wsURI + SOLNNAME + " " | ||
48 | val vampLoc = VAMPDIR + VAMPNAME | ||
49 | |||
50 | |||
51 | //1. create temp file for vampire problem | ||
52 | var tempURI = workspace.writeModel(problem, TEMPNAME).toFileString | ||
53 | |||
54 | //2. run command and save to | ||
55 | //need to have cygwin downloaded | ||
56 | |||
57 | |||
58 | |||
59 | |||
60 | val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) | ||
61 | //2.1 determine time left | ||
62 | p.waitFor | ||
63 | |||
64 | //2.2 store output into local variable | ||
65 | val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); | ||
66 | val List<String> output = newArrayList | ||
67 | |||
68 | var line = ""; | ||
69 | while ((line = reader.readLine())!= null) { | ||
70 | output.add(line + "\n"); | ||
71 | } | ||
72 | |||
73 | // println(output.toString()) | ||
74 | |||
75 | //4. delete temp file | ||
76 | workspace.getFile(TEMPNAME).delete | ||
77 | |||
78 | //5. determine and return whether or not finite model was found | ||
79 | |||
80 | //6. save solution as a .tptp model | ||
81 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new VampireLanguageFactoryImpl) | ||
82 | workspace.readModel(VampireModel, SOLNNAME).eResource.contents | ||
83 | |||
84 | |||
85 | |||
86 | |||
87 | |||
88 | |||
89 | |||
90 | |||
43 | /* | 91 | /* |
44 | //Prepare | 92 | //Prepare |
45 | val warnings = new LinkedList<String> | 93 | val warnings = new LinkedList<String> |
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 | } |