diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | 145 |
1 files changed, 145 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend new file mode 100644 index 00000000..6bac4130 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend | |||
@@ -0,0 +1,145 @@ | |||
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.A4Solution | ||
11 | import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod | ||
12 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
13 | import java.util.LinkedList | ||
14 | import java.util.List | ||
15 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | ||
16 | import org.eclipse.xtend.lib.annotations.Data | ||
17 | import java.util.Map | ||
18 | import java.util.HashMap | ||
19 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver | ||
20 | import org.eclipse.emf.common.CommonPlugin | ||
21 | import java.util.ArrayList | ||
22 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | ||
23 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
24 | |||
25 | class AlloySolverException extends Exception{ | ||
26 | new(String s) { super(s) } | ||
27 | new(String s, Exception e) { super(s,e) } | ||
28 | new(String s, List<String> errors, Exception e) { | ||
29 | super(s + '\n' + errors.join('\n'), e) | ||
30 | } | ||
31 | } | ||
32 | |||
33 | @Data class MonitoredAlloySolution{ | ||
34 | List<String> warnings | ||
35 | List<String> debugs | ||
36 | long kodkodTime | ||
37 | long runtimeTime | ||
38 | |||
39 | A4Solution solution | ||
40 | } | ||
41 | |||
42 | class AlloyHandler { | ||
43 | |||
44 | //val fileName = "problem.als" | ||
45 | |||
46 | public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, String alloyCode) { | ||
47 | //Prepare | ||
48 | |||
49 | val warnings = new LinkedList<String> | ||
50 | val debugs = new LinkedList<String> | ||
51 | val runtime = new ArrayList<Long> | ||
52 | val reporter = new A4Reporter() { | ||
53 | override debug(String message) { debugs += message } | ||
54 | override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
55 | override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
56 | override warning(ErrorWarning msg) { warnings += msg.message } | ||
57 | } | ||
58 | |||
59 | val options = new A4Options() => [ | ||
60 | it.symmetry = configuration.symmetry | ||
61 | it.noOverflow = true | ||
62 | it.solver = getSolver(configuration.solver, configuration) | ||
63 | if(configuration.solver.externalSolver) { | ||
64 | it.solverDirectory = configuration.solverPath | ||
65 | } | ||
66 | it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString | ||
67 | ] | ||
68 | |||
69 | // Transform | ||
70 | var Command command = null; | ||
71 | var CompModule compModule = null | ||
72 | |||
73 | val kodkodTransformStart = System.currentTimeMillis(); | ||
74 | |||
75 | try { | ||
76 | if(configuration.writeToFile) { | ||
77 | compModule = CompUtil.parseEverything_fromFile(reporter,null,path) | ||
78 | } else { | ||
79 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) | ||
80 | } | ||
81 | if(compModule.allCommands.size != 1) | ||
82 | throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') | ||
83 | command = compModule.allCommands.head | ||
84 | } catch (Err e){ | ||
85 | throw new AlloySolverException(e.message,warnings,e) | ||
86 | } | ||
87 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | ||
88 | |||
89 | //Execute | ||
90 | var A4Solution answer = null; | ||
91 | try { | ||
92 | answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | ||
93 | }catch(Exception e) { | ||
94 | warnings +=e.message | ||
95 | } | ||
96 | |||
97 | var long runtimeFromAnswer; | ||
98 | if(runtime.empty) { | ||
99 | runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish) | ||
100 | } else { | ||
101 | runtimeFromAnswer = runtime.head | ||
102 | } | ||
103 | |||
104 | return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer) | ||
105 | } | ||
106 | |||
107 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap | ||
108 | def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { | ||
109 | val config = new SolverConfiguration(backedSolver,path,options) | ||
110 | if(previousSolverConfigurations.containsKey(config)) { | ||
111 | return previousSolverConfigurations.get(config) | ||
112 | } else { | ||
113 | val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' | ||
114 | val newSolver = A4Options.SatSolver.make(id,id,path,options) | ||
115 | previousSolverConfigurations.put(config,newSolver) | ||
116 | return newSolver | ||
117 | } | ||
118 | } | ||
119 | |||
120 | def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { | ||
121 | switch(backedSolver){ | ||
122 | case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE | ||
123 | case SpearPIPE: return A4Options.SatSolver.SpearPIPE | ||
124 | case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI | ||
125 | case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI | ||
126 | case LingelingJNI: return A4Options.SatSolver.LingelingJNI | ||
127 | case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) | ||
128 | case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI | ||
129 | case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI | ||
130 | case SAT4J: return A4Options.SatSolver.SAT4J | ||
131 | case CNF: return A4Options.SatSolver.CNF | ||
132 | case KodKod: return A4Options.SatSolver.KK | ||
133 | } | ||
134 | } | ||
135 | |||
136 | def isExternalSolver(AlloyBackendSolver backedSolver) { | ||
137 | return !(backedSolver == AlloyBackendSolver.SAT4J) | ||
138 | } | ||
139 | } | ||
140 | |||
141 | @Data class SolverConfiguration { | ||
142 | AlloyBackendSolver backedSolver | ||
143 | String path | ||
144 | String[] options | ||
145 | } | ||