diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-25 04:15:39 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-25 04:15:39 -0400 |
commit | 25a4b1b53add70e268c3083682f8a3508c618ec2 (patch) | |
tree | 6d46e62be49cfe6c5640e2e9af80aae90da6a212 /Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | |
parent | mid-measurement push (diff) | |
download | VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.gz VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.zst VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.zip |
VAMPIRE: post-submission push
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend')
-rw-r--r-- | Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | 228 |
1 files changed, 228 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend new file mode 100644 index 00000000..eee2d649 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | |||
@@ -0,0 +1,228 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4.A4Reporter | ||
4 | import edu.mit.csail.sdg.alloy4.Err | ||
5 | import edu.mit.csail.sdg.alloy4.ErrorWarning | ||
6 | import edu.mit.csail.sdg.alloy4compiler.ast.Command | ||
7 | import edu.mit.csail.sdg.alloy4compiler.parser.CompModule | ||
8 | import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil | ||
9 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Options | ||
10 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver | ||
11 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
12 | import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod | ||
13 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | ||
14 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
15 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
17 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
18 | import java.util.ArrayList | ||
19 | import java.util.HashMap | ||
20 | import java.util.LinkedList | ||
21 | import java.util.List | ||
22 | import java.util.Map | ||
23 | import java.util.concurrent.Callable | ||
24 | import java.util.concurrent.ExecutionException | ||
25 | import java.util.concurrent.ExecutorService | ||
26 | import java.util.concurrent.Executors | ||
27 | import java.util.concurrent.TimeUnit | ||
28 | import java.util.concurrent.TimeoutException | ||
29 | import org.eclipse.xtend.lib.annotations.Data | ||
30 | |||
31 | class AlloySolverException extends Exception{ | ||
32 | new(String s) { super(s) } | ||
33 | new(String s, Exception e) { super(s,e) } | ||
34 | new(String s, List<String> errors, Exception e) { | ||
35 | super(s + '\n' + errors.join('\n'), e) | ||
36 | } | ||
37 | } | ||
38 | |||
39 | @Data class MonitoredAlloySolution{ | ||
40 | List<String> warnings | ||
41 | List<String> debugs | ||
42 | long kodkodTime | ||
43 | val List<Pair<A4Solution, Long>> aswers | ||
44 | val boolean finishedBeforeTimeout | ||
45 | } | ||
46 | |||
47 | class AlloyHandler { | ||
48 | |||
49 | //val fileName = "problem.als" | ||
50 | |||
51 | def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { | ||
52 | |||
53 | //Prepare | ||
54 | val warnings = new LinkedList<String> | ||
55 | val debugs = new LinkedList<String> | ||
56 | val runtime = new ArrayList<Long> | ||
57 | val reporter = new A4Reporter() { | ||
58 | override debug(String message) { debugs += message } | ||
59 | override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
60 | override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
61 | override warning(ErrorWarning msg) { warnings += msg.message } | ||
62 | } | ||
63 | |||
64 | val options = new A4Options() => [ | ||
65 | it.symmetry = configuration.symmetry | ||
66 | it.noOverflow = true | ||
67 | it.solver = getSolver(configuration.solver, configuration) | ||
68 | if(configuration.solver.externalSolver) { | ||
69 | it.solverDirectory = configuration.solverPath | ||
70 | } | ||
71 | //it.inferPartialInstance | ||
72 | //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString | ||
73 | ] | ||
74 | |||
75 | // Transform | ||
76 | var Command command = null; | ||
77 | var CompModule compModule = null | ||
78 | |||
79 | // Start: Alloy -> Kodkod | ||
80 | val kodkodTransformStart = System.currentTimeMillis(); | ||
81 | try { | ||
82 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) | ||
83 | if(compModule.allCommands.size != 1) | ||
84 | throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') | ||
85 | command = compModule.allCommands.head | ||
86 | } catch (Err e){ | ||
87 | throw new AlloySolverException(e.message,warnings,e) | ||
88 | } | ||
89 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | ||
90 | // Finish: Alloy -> Kodkod | ||
91 | |||
92 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) | ||
93 | var List<Pair<A4Solution, Long>> answers | ||
94 | var boolean finished | ||
95 | if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { | ||
96 | answers = callable.call | ||
97 | finished = true | ||
98 | } else { | ||
99 | val ExecutorService executor = Executors.newCachedThreadPool(); | ||
100 | val future = executor.submit(callable) | ||
101 | try{ | ||
102 | answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS) | ||
103 | finished = true | ||
104 | } catch (TimeoutException ex) { | ||
105 | // handle the timeout | ||
106 | } catch (InterruptedException e) { | ||
107 | // handle the interrupts | ||
108 | } catch (ExecutionException e) { | ||
109 | // handle other exceptions | ||
110 | } finally { | ||
111 | future.cancel(true); | ||
112 | |||
113 | answers = callable.partialAnswers | ||
114 | finished = false | ||
115 | } | ||
116 | } | ||
117 | |||
118 | new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) | ||
119 | } | ||
120 | |||
121 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap | ||
122 | def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { | ||
123 | val config = new SolverConfiguration(backedSolver,path,options) | ||
124 | if(previousSolverConfigurations.containsKey(config)) { | ||
125 | return previousSolverConfigurations.get(config) | ||
126 | } else { | ||
127 | val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' | ||
128 | val newSolver = A4Options.SatSolver.make(id,id,path,options) | ||
129 | previousSolverConfigurations.put(config,newSolver) | ||
130 | return newSolver | ||
131 | } | ||
132 | } | ||
133 | |||
134 | def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { | ||
135 | switch(backedSolver){ | ||
136 | case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE | ||
137 | case SpearPIPE: return A4Options.SatSolver.SpearPIPE | ||
138 | case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI | ||
139 | case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI | ||
140 | case LingelingJNI: return A4Options.SatSolver.LingelingJNI | ||
141 | case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) | ||
142 | case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI | ||
143 | case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI | ||
144 | case SAT4J: return A4Options.SatSolver.SAT4J | ||
145 | case CNF: return A4Options.SatSolver.CNF | ||
146 | case KodKod: return A4Options.SatSolver.KK | ||
147 | } | ||
148 | } | ||
149 | |||
150 | def isExternalSolver(AlloyBackendSolver backedSolver) { | ||
151 | return !(backedSolver == AlloyBackendSolver.SAT4J) | ||
152 | } | ||
153 | } | ||
154 | |||
155 | class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | ||
156 | |||
157 | val List<String> warnings | ||
158 | val List<String> debugs | ||
159 | val A4Reporter reporter | ||
160 | val A4Options options | ||
161 | |||
162 | val Command command | ||
163 | val CompModule compModule | ||
164 | val AlloySolverConfiguration configuration | ||
165 | |||
166 | val List<Pair<A4Solution,Long>> answers = new LinkedList() | ||
167 | |||
168 | new(List<String> warnings, | ||
169 | List<String> debugs, | ||
170 | A4Reporter reporter, | ||
171 | A4Options options, | ||
172 | Command command, | ||
173 | CompModule compModule, | ||
174 | AlloySolverConfiguration configuration) | ||
175 | { | ||
176 | this.warnings = warnings | ||
177 | this.debugs = debugs | ||
178 | this.reporter = reporter | ||
179 | this.options = options | ||
180 | this.command = command | ||
181 | this.compModule = compModule | ||
182 | this.configuration = configuration | ||
183 | } | ||
184 | |||
185 | override call() throws Exception { | ||
186 | val startTime = System.currentTimeMillis | ||
187 | |||
188 | // Start: Execute | ||
189 | var A4Solution lastAnswer = null | ||
190 | try { | ||
191 | if(!configuration.progressMonitor.isCancelled) { | ||
192 | do{ | ||
193 | if(lastAnswer == null) { | ||
194 | lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | ||
195 | } else { | ||
196 | lastAnswer = lastAnswer.next | ||
197 | } | ||
198 | configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) | ||
199 | |||
200 | val runtime = System.currentTimeMillis -startTime | ||
201 | synchronized(this) { | ||
202 | answers += (lastAnswer->runtime) | ||
203 | } | ||
204 | } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) | ||
205 | |||
206 | } | ||
207 | }catch(Exception e) { | ||
208 | warnings +=e.message | ||
209 | } | ||
210 | // Finish: execute | ||
211 | return answers | ||
212 | } | ||
213 | |||
214 | def hasEnoughSolution(List<?> answers) { | ||
215 | if(configuration.solutionScope.numberOfRequiredSolution < 0) return false | ||
216 | else return answers.size() == configuration.solutionScope.numberOfRequiredSolution | ||
217 | } | ||
218 | |||
219 | public def getPartialAnswers() { | ||
220 | return answers | ||
221 | } | ||
222 | } | ||
223 | |||
224 | @Data class SolverConfiguration { | ||
225 | AlloyBackendSolver backedSolver | ||
226 | String path | ||
227 | String[] options | ||
228 | } \ No newline at end of file | ||