diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | 214 |
1 files changed, 214 insertions, 0 deletions
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 new file mode 100644 index 00000000..aefa1a7e --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | |||
@@ -0,0 +1,214 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireBackendSolver | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
5 | 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 | ||
10 | import java.util.ArrayList | ||
11 | import java.util.HashMap | ||
12 | import java.util.LinkedList | ||
13 | import java.util.List | ||
14 | import java.util.Map | ||
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 | ||
19 | |||
20 | class VampireSolverException extends Exception{ | ||
21 | new(String s) { super(s) } | ||
22 | new(String s, Exception e) { super(s,e) } | ||
23 | new(String s, List<String> errors, Exception e) { | ||
24 | super(s + '\n' + errors.join('\n'), e) | ||
25 | } | ||
26 | } | ||
27 | |||
28 | @Data class VampireSolutionModel{ | ||
29 | // List<String> warnings | ||
30 | // List<String> debugs | ||
31 | // long kodkodTime | ||
32 | // val List<Pair<A4Solution, Long>> aswers | ||
33 | // val boolean finishedBeforeTimeout | ||
34 | |||
35 | |||
36 | } | ||
37 | |||
38 | class VampireHandler { | ||
39 | |||
40 | //val fileName = "problem.als" | ||
41 | |||
42 | public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration,String vampireCode) { | ||
43 | /* | ||
44 | //Prepare | ||
45 | val warnings = new LinkedList<String> | ||
46 | val debugs = new LinkedList<String> | ||
47 | val runtime = new ArrayList<Long> | ||
48 | val reporter = new A4Reporter() { | ||
49 | override debug(String message) { debugs += message } | ||
50 | override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
51 | override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
52 | override warning(ErrorWarning msg) { warnings += msg.message } | ||
53 | } | ||
54 | |||
55 | val options = new A4Options() => [ | ||
56 | it.symmetry = configuration.symmetry | ||
57 | it.noOverflow = true | ||
58 | it.solver = getSolver(configuration.getSolver, configuration) | ||
59 | if(configuration.getSolver.externalSolver) { | ||
60 | it.solverDirectory = configuration.solverPath | ||
61 | } | ||
62 | //it.inferPartialInstance | ||
63 | //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString | ||
64 | ] | ||
65 | |||
66 | // Transform | ||
67 | var Command command = null; | ||
68 | var CompModule compModule = null | ||
69 | |||
70 | // Start: Alloy -> Kodkod | ||
71 | val kodkodTransformStart = System.currentTimeMillis(); | ||
72 | try { | ||
73 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) | ||
74 | if(compModule.allCommands.size != 1) | ||
75 | throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') | ||
76 | command = compModule.allCommands.head | ||
77 | } catch (Err e){ | ||
78 | throw new AlloySolverException(e.message,warnings,e) | ||
79 | } | ||
80 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | ||
81 | // Finish: Alloy -> Kodkod | ||
82 | |||
83 | val limiter = new SimpleTimeLimiter | ||
84 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) | ||
85 | var List<Pair<A4Solution, Long>> answers | ||
86 | var boolean finished | ||
87 | if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { | ||
88 | answers = callable.call | ||
89 | finished = true | ||
90 | } else { | ||
91 | try{ | ||
92 | answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) | ||
93 | finished = true | ||
94 | } catch (UncheckedTimeoutException e) { | ||
95 | answers = callable.partialAnswers | ||
96 | finished = false | ||
97 | } | ||
98 | } | ||
99 | |||
100 | new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) | ||
101 | */ | ||
102 | } | ||
103 | /* | ||
104 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap | ||
105 | def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { | ||
106 | val config = new SolverConfiguration(backedSolver,path,options) | ||
107 | if(previousSolverConfigurations.containsKey(config)) { | ||
108 | return previousSolverConfigurations.get(config) | ||
109 | } else { | ||
110 | val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' | ||
111 | val newSolver = A4Options.SatSolver.make(id,id,path,options) | ||
112 | previousSolverConfigurations.put(config,newSolver) | ||
113 | return newSolver | ||
114 | } | ||
115 | } | ||
116 | |||
117 | def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { | ||
118 | switch(backedSolver){ | ||
119 | case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE | ||
120 | case SpearPIPE: return A4Options.SatSolver.SpearPIPE | ||
121 | case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI | ||
122 | case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI | ||
123 | case LingelingJNI: return A4Options.SatSolver.LingelingJNI | ||
124 | case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) | ||
125 | case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI | ||
126 | case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI | ||
127 | case SAT4J: return A4Options.SatSolver.SAT4J | ||
128 | case CNF: return A4Options.SatSolver.CNF | ||
129 | case KodKod: return A4Options.SatSolver.KK | ||
130 | } | ||
131 | } | ||
132 | |||
133 | def isExternalSolver(AlloyBackendSolver backedSolver) { | ||
134 | return !(backedSolver == AlloyBackendSolver.SAT4J) | ||
135 | } | ||
136 | */ | ||
137 | } | ||
138 | /* | ||
139 | class VampireCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | ||
140 | |||
141 | val List<String> warnings | ||
142 | val List<String> debugs | ||
143 | val A4Reporter reporter | ||
144 | val A4Options options | ||
145 | |||
146 | val Command command | ||
147 | val CompModule compModule | ||
148 | val AlloySolverConfiguration configuration | ||
149 | |||
150 | val List<Pair<A4Solution,Long>> answers = new LinkedList() | ||
151 | |||
152 | new(List<String> warnings, | ||
153 | List<String> debugs, | ||
154 | A4Reporter reporter, | ||
155 | A4Options options, | ||
156 | Command command, | ||
157 | CompModule compModule, | ||
158 | AlloySolverConfiguration configuration) | ||
159 | { | ||
160 | this.warnings = warnings | ||
161 | this.debugs = debugs | ||
162 | this.reporter = reporter | ||
163 | this.options = options | ||
164 | this.command = command | ||
165 | this.compModule = compModule | ||
166 | this.configuration = configuration | ||
167 | } | ||
168 | |||
169 | override call() throws Exception { | ||
170 | val startTime = System.currentTimeMillis | ||
171 | |||
172 | // Start: Execute | ||
173 | var A4Solution lastAnswer = null | ||
174 | try { | ||
175 | if(!configuration.progressMonitor.isCancelled) { | ||
176 | do{ | ||
177 | if(lastAnswer == null) { | ||
178 | lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | ||
179 | } else { | ||
180 | lastAnswer = lastAnswer.next | ||
181 | } | ||
182 | configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) | ||
183 | |||
184 | val runtime = System.currentTimeMillis -startTime | ||
185 | synchronized(this) { | ||
186 | answers += (lastAnswer->runtime) | ||
187 | } | ||
188 | } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) | ||
189 | |||
190 | } | ||
191 | }catch(Exception e) { | ||
192 | warnings +=e.message | ||
193 | } | ||
194 | // Finish: execute | ||
195 | return answers | ||
196 | } | ||
197 | |||
198 | def hasEnoughSolution(List<?> answers) { | ||
199 | if(configuration.solutionScope.numberOfRequiredSolution < 0) return false | ||
200 | else return answers.size() == configuration.solutionScope.numberOfRequiredSolution | ||
201 | } | ||
202 | |||
203 | public def getPartialAnswers() { | ||
204 | return answers | ||
205 | } | ||
206 | |||
207 | } | ||
208 | /* | ||
209 | @Data class SolverConfiguration { | ||
210 | VampireBackendSolver backendSolver | ||
211 | String path | ||
212 | String[] options | ||
213 | } | ||
214 | */ | ||