diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-08-29 06:26:02 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:41:39 -0400 |
commit | 15602c7cfbfc80b8c826855b94c9f9582650dd21 (patch) | |
tree | 3f90d5812e68215838efd52372bcc26df88b9033 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder | |
parent | VAMPIRE: integrate local Vampire executeable #32 (diff) | |
download | VIATRA-Generator-15602c7cfbfc80b8c826855b94c9f9582650dd21.tar.gz VIATRA-Generator-15602c7cfbfc80b8c826855b94c9f9582650dd21.tar.zst VIATRA-Generator-15602c7cfbfc80b8c826855b94c9f9582650dd21.zip |
VAMPIRE: adapt grammar to Vampire solution + get model from text
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder')
3 files changed, 212 insertions, 217 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index 13db3c99..a2449fc0 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend | |||
@@ -61,7 +61,7 @@ class Logic2VampireLanguageMapper { | |||
61 | // create model bases | 61 | // create model bases |
62 | // TODO | 62 | // TODO |
63 | val initialComment = createVLSComment => [ | 63 | val initialComment = createVLSComment => [ |
64 | it.comment = "This is an initial Test Comment" | 64 | it.comment = "%This is an initial Test Comment" |
65 | ] | 65 | ] |
66 | 66 | ||
67 | val specification = createVampireModel => [ | 67 | val specification = createVampireModel => [ |
@@ -163,10 +163,10 @@ class Logic2VampireLanguageMapper { | |||
163 | createVLSInt => [it.value = literal.value.toString()] | 163 | createVLSInt => [it.value = literal.value.toString()] |
164 | } | 164 | } |
165 | 165 | ||
166 | def dispatch protected VLSTerm transformTerm(RealLiteral literal, Logic2VampireLanguageMapperTrace trace, | 166 | // def dispatch protected VLSTerm transformTerm(RealLiteral literal, Logic2VampireLanguageMapperTrace trace, |
167 | Map<Variable, VLSVariable> variables) { | 167 | // Map<Variable, VLSVariable> variables) { |
168 | createVLSReal => [it.value = literal.value.toString()] | 168 | // createVLSReal => [it.value = literal.value.toString()] |
169 | } | 169 | // } |
170 | 170 | ||
171 | def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace, | 171 | def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace, |
172 | Map<Variable, VLSVariable> variables) { | 172 | Map<Variable, VLSVariable> variables) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index 93c28e7c..c79003bd 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend | |||
@@ -189,7 +189,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
189 | 189 | ||
190 | // STEP 2 CONT'D | 190 | // STEP 2 CONT'D |
191 | for (e : type2cont.entrySet) { | 191 | for (e : type2cont.entrySet) { |
192 | println(e.key + " " + e.value) | 192 | // println(e.key + " " + e.value) |
193 | val relFormula = createVLSFofFormula => [ | 193 | val relFormula = createVLSFofFormula => [ |
194 | it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) | 194 | it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) |
195 | it.fofRole = "axiom" | 195 | it.fofRole = "axiom" |
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 274396ee..f0426245 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 | |||
@@ -9,31 +9,35 @@ import java.util.List | |||
9 | import org.eclipse.emf.ecore.resource.Resource | 9 | import org.eclipse.emf.ecore.resource.Resource |
10 | import org.eclipse.xtend.lib.annotations.Data | 10 | import org.eclipse.xtend.lib.annotations.Data |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl | ||
13 | |||
14 | class VampireSolverException extends Exception { | ||
15 | new(String s) { | ||
16 | super(s) | ||
17 | } | ||
18 | |||
19 | new(String s, Exception e) { | ||
20 | super(s, e) | ||
21 | } | ||
12 | 22 | ||
13 | class VampireSolverException extends Exception{ | ||
14 | new(String s) { super(s) } | ||
15 | new(String s, Exception e) { super(s,e) } | ||
16 | new(String s, List<String> errors, Exception e) { | 23 | new(String s, List<String> errors, Exception e) { |
17 | super(s + '\n' + errors.join('\n'), e) | 24 | super(s + '\n' + errors.join('\n'), e) |
18 | } | 25 | } |
19 | } | 26 | } |
20 | 27 | ||
21 | @Data class VampireSolutionModel{ | 28 | @Data class VampireSolutionModel { |
22 | // List<String> warnings | 29 | // List<String> warnings |
23 | // List<String> debugs | 30 | // List<String> debugs |
24 | // long kodkodTime | 31 | // long kodkodTime |
25 | // val List<Pair<A4Solution, Long>> aswers | 32 | // val List<Pair<A4Solution, Long>> aswers |
26 | // val boolean finishedBeforeTimeout | 33 | // val boolean finishedBeforeTimeout |
27 | |||
28 | |||
29 | } | 34 | } |
30 | 35 | ||
31 | class VampireHandler { | 36 | class VampireHandler { |
32 | 37 | ||
33 | //val fileName = "problem.als" | 38 | // val fileName = "problem.als" |
34 | |||
35 | public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration) { | 39 | public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration) { |
36 | 40 | ||
37 | val CMD = "cmd /c " | 41 | val CMD = "cmd /c " |
38 | val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" | 42 | val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" |
39 | val VAMPNAME = "vampire.exe" | 43 | val VAMPNAME = "vampire.exe" |
@@ -41,222 +45,213 @@ class VampireHandler { | |||
41 | val OPTION = " --mode casc_sat " | 45 | val OPTION = " --mode casc_sat " |
42 | val SOLNNAME = "solution.tptp" | 46 | val SOLNNAME = "solution.tptp" |
43 | val PATH = "C:/cygwin64/bin" | 47 | val PATH = "C:/cygwin64/bin" |
44 | 48 | ||
45 | val wsURI = workspace.workspaceURI | 49 | val wsURI = workspace.workspaceURI |
46 | val tempLoc = wsURI + TEMPNAME | 50 | val tempLoc = wsURI + TEMPNAME |
47 | val solnLoc = wsURI + SOLNNAME + " " | 51 | val solnLoc = wsURI + SOLNNAME + " " |
48 | val vampLoc = VAMPDIR + VAMPNAME | 52 | val vampLoc = VAMPDIR + VAMPNAME |
49 | 53 | ||
50 | 54 | // 1. create temp file for vampire problem | |
51 | //1. create temp file for vampire problem | ||
52 | var tempURI = workspace.writeModel(problem, TEMPNAME).toFileString | 55 | 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 | 56 | ||
68 | var line = ""; | 57 | // 2. run command and save to |
69 | while ((line = reader.readLine())!= null) { | 58 | // need to have cygwin downloaded |
70 | output.add(line + "\n"); | 59 | val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) |
71 | } | 60 | // 2.1 determine time left |
61 | p.waitFor | ||
72 | 62 | ||
73 | // println(output.toString()) | 63 | // 2.2 store output into local variable |
64 | val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); | ||
65 | val List<String> output = newArrayList | ||
74 | 66 | ||
75 | //4. delete temp file | 67 | var line = ""; |
76 | workspace.getFile(TEMPNAME).delete | 68 | while ((line = reader.readLine()) != null) { |
77 | 69 | output.add(line + "\n"); | |
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 | |||
91 | /* | ||
92 | //Prepare | ||
93 | val warnings = new LinkedList<String> | ||
94 | val debugs = new LinkedList<String> | ||
95 | val runtime = new ArrayList<Long> | ||
96 | val reporter = new A4Reporter() { | ||
97 | override debug(String message) { debugs += message } | ||
98 | override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
99 | override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
100 | override warning(ErrorWarning msg) { warnings += msg.message } | ||
101 | } | 70 | } |
71 | |||
72 | // println(output.toString()) | ||
73 | // 4. delete temp file | ||
74 | workspace.getFile(TEMPNAME).delete | ||
75 | |||
76 | // 5. determine and return whether or not finite model was found | ||
77 | // 6. save solution as a .tptp model | ||
78 | val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents | ||
102 | 79 | ||
103 | val options = new A4Options() => [ | 80 | |
104 | it.symmetry = configuration.symmetry | 81 | |
105 | it.noOverflow = true | 82 | println((root.get(0) as VampireModelImpl ).comments) |
106 | it.solver = getSolver(configuration.getSolver, configuration) | ||
107 | if(configuration.getSolver.externalSolver) { | ||
108 | it.solverDirectory = configuration.solverPath | ||
109 | } | ||
110 | //it.inferPartialInstance | ||
111 | //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString | ||
112 | ] | ||
113 | |||
114 | // Transform | ||
115 | var Command command = null; | ||
116 | var CompModule compModule = null | ||
117 | |||
118 | // Start: Alloy -> Kodkod | ||
119 | val kodkodTransformStart = System.currentTimeMillis(); | ||
120 | try { | ||
121 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) | ||
122 | if(compModule.allCommands.size != 1) | ||
123 | throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') | ||
124 | command = compModule.allCommands.head | ||
125 | } catch (Err e){ | ||
126 | throw new AlloySolverException(e.message,warnings,e) | ||
127 | } | ||
128 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | ||
129 | // Finish: Alloy -> Kodkod | ||
130 | 83 | ||
131 | val limiter = new SimpleTimeLimiter | 84 | return root |
132 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) | ||
133 | var List<Pair<A4Solution, Long>> answers | ||
134 | var boolean finished | ||
135 | if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { | ||
136 | answers = callable.call | ||
137 | finished = true | ||
138 | } else { | ||
139 | try{ | ||
140 | answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) | ||
141 | finished = true | ||
142 | } catch (UncheckedTimeoutException e) { | ||
143 | answers = callable.partialAnswers | ||
144 | finished = false | ||
145 | } | ||
146 | } | ||
147 | 85 | ||
148 | new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) | ||
149 | */ | ||
150 | } | ||
151 | /* | 86 | /* |
152 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap | 87 | * //Prepare |
153 | def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { | 88 | * val warnings = new LinkedList<String> |
154 | val config = new SolverConfiguration(backedSolver,path,options) | 89 | * val debugs = new LinkedList<String> |
155 | if(previousSolverConfigurations.containsKey(config)) { | 90 | * val runtime = new ArrayList<Long> |
156 | return previousSolverConfigurations.get(config) | 91 | * val reporter = new A4Reporter() { |
157 | } else { | 92 | * override debug(String message) { debugs += message } |
158 | val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' | 93 | * override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } |
159 | val newSolver = A4Options.SatSolver.make(id,id,path,options) | 94 | * override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } |
160 | previousSolverConfigurations.put(config,newSolver) | 95 | * override warning(ErrorWarning msg) { warnings += msg.message } |
161 | return newSolver | 96 | * } |
162 | } | 97 | * |
163 | } | 98 | * val options = new A4Options() => [ |
164 | 99 | * it.symmetry = configuration.symmetry | |
165 | def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { | 100 | * it.noOverflow = true |
166 | switch(backedSolver){ | 101 | * it.solver = getSolver(configuration.getSolver, configuration) |
167 | case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE | 102 | * if(configuration.getSolver.externalSolver) { |
168 | case SpearPIPE: return A4Options.SatSolver.SpearPIPE | 103 | * it.solverDirectory = configuration.solverPath |
169 | case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI | 104 | * } |
170 | case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI | 105 | * //it.inferPartialInstance |
171 | case LingelingJNI: return A4Options.SatSolver.LingelingJNI | 106 | * //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString |
172 | case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) | 107 | * ] |
173 | case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI | 108 | * |
174 | case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI | 109 | * // Transform |
175 | case SAT4J: return A4Options.SatSolver.SAT4J | 110 | * var Command command = null; |
176 | case CNF: return A4Options.SatSolver.CNF | 111 | * var CompModule compModule = null |
177 | case KodKod: return A4Options.SatSolver.KK | 112 | * |
178 | } | 113 | * // Start: Alloy -> Kodkod |
179 | } | 114 | * val kodkodTransformStart = System.currentTimeMillis(); |
180 | 115 | * try { | |
181 | def isExternalSolver(AlloyBackendSolver backedSolver) { | 116 | * compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) |
182 | return !(backedSolver == AlloyBackendSolver.SAT4J) | 117 | * if(compModule.allCommands.size != 1) |
118 | * throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') | ||
119 | * command = compModule.allCommands.head | ||
120 | * } catch (Err e){ | ||
121 | * throw new AlloySolverException(e.message,warnings,e) | ||
122 | * } | ||
123 | * val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | ||
124 | * // Finish: Alloy -> Kodkod | ||
125 | * | ||
126 | * val limiter = new SimpleTimeLimiter | ||
127 | * val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) | ||
128 | * var List<Pair<A4Solution, Long>> answers | ||
129 | * var boolean finished | ||
130 | * if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { | ||
131 | * answers = callable.call | ||
132 | * finished = true | ||
133 | * } else { | ||
134 | * try{ | ||
135 | * answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) | ||
136 | * finished = true | ||
137 | * } catch (UncheckedTimeoutException e) { | ||
138 | * answers = callable.partialAnswers | ||
139 | * finished = false | ||
140 | * } | ||
141 | * } | ||
142 | |||
143 | * new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) | ||
144 | */ | ||
183 | } | 145 | } |
184 | */ | ||
185 | } | ||
186 | /* | 146 | /* |
187 | class VampireCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | 147 | * val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap |
188 | 148 | * def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { | |
189 | val List<String> warnings | 149 | * val config = new SolverConfiguration(backedSolver,path,options) |
190 | val List<String> debugs | 150 | * if(previousSolverConfigurations.containsKey(config)) { |
191 | val A4Reporter reporter | 151 | * return previousSolverConfigurations.get(config) |
192 | val A4Options options | 152 | * } else { |
193 | 153 | * val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' | |
194 | val Command command | 154 | * val newSolver = A4Options.SatSolver.make(id,id,path,options) |
195 | val CompModule compModule | 155 | * previousSolverConfigurations.put(config,newSolver) |
196 | val AlloySolverConfiguration configuration | 156 | * return newSolver |
197 | 157 | * } | |
198 | val List<Pair<A4Solution,Long>> answers = new LinkedList() | 158 | * } |
199 | 159 | * | |
200 | new(List<String> warnings, | 160 | * def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { |
201 | List<String> debugs, | 161 | * switch(backedSolver){ |
202 | A4Reporter reporter, | 162 | * case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE |
203 | A4Options options, | 163 | * case SpearPIPE: return A4Options.SatSolver.SpearPIPE |
204 | Command command, | 164 | * case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI |
205 | CompModule compModule, | 165 | * case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI |
206 | AlloySolverConfiguration configuration) | 166 | * case LingelingJNI: return A4Options.SatSolver.LingelingJNI |
207 | { | 167 | * case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) |
208 | this.warnings = warnings | 168 | * case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI |
209 | this.debugs = debugs | 169 | * case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI |
210 | this.reporter = reporter | 170 | * case SAT4J: return A4Options.SatSolver.SAT4J |
211 | this.options = options | 171 | * case CNF: return A4Options.SatSolver.CNF |
212 | this.command = command | 172 | * case KodKod: return A4Options.SatSolver.KK |
213 | this.compModule = compModule | 173 | * } |
214 | this.configuration = configuration | 174 | * } |
215 | } | 175 | * |
216 | 176 | * def isExternalSolver(AlloyBackendSolver backedSolver) { | |
217 | override call() throws Exception { | 177 | * return !(backedSolver == AlloyBackendSolver.SAT4J) |
218 | val startTime = System.currentTimeMillis | 178 | * } |
219 | 179 | */ | |
220 | // Start: Execute | ||
221 | var A4Solution lastAnswer = null | ||
222 | try { | ||
223 | if(!configuration.progressMonitor.isCancelled) { | ||
224 | do{ | ||
225 | if(lastAnswer == null) { | ||
226 | lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | ||
227 | } else { | ||
228 | lastAnswer = lastAnswer.next | ||
229 | } | ||
230 | configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) | ||
231 | |||
232 | val runtime = System.currentTimeMillis -startTime | ||
233 | synchronized(this) { | ||
234 | answers += (lastAnswer->runtime) | ||
235 | } | ||
236 | } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) | ||
237 | |||
238 | } | ||
239 | }catch(Exception e) { | ||
240 | warnings +=e.message | ||
241 | } | ||
242 | // Finish: execute | ||
243 | return answers | ||
244 | } | ||
245 | |||
246 | def hasEnoughSolution(List<?> answers) { | ||
247 | if(configuration.solutionScope.numberOfRequiredSolution < 0) return false | ||
248 | else return answers.size() == configuration.solutionScope.numberOfRequiredSolution | ||
249 | } | ||
250 | |||
251 | public def getPartialAnswers() { | ||
252 | return answers | ||
253 | } | ||
254 | |||
255 | } | 180 | } |
256 | /* | 181 | /* |
257 | @Data class SolverConfiguration { | 182 | * class VampireCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ |
258 | VampireBackendSolver backendSolver | 183 | * |
259 | String path | 184 | * val List<String> warnings |
260 | String[] options | 185 | * val List<String> debugs |
261 | } | 186 | * val A4Reporter reporter |
262 | */ | 187 | * val A4Options options |
188 | * | ||
189 | * val Command command | ||
190 | * val CompModule compModule | ||
191 | * val AlloySolverConfiguration configuration | ||
192 | * | ||
193 | * val List<Pair<A4Solution,Long>> answers = new LinkedList() | ||
194 | * | ||
195 | * new(List<String> warnings, | ||
196 | * List<String> debugs, | ||
197 | * A4Reporter reporter, | ||
198 | * A4Options options, | ||
199 | * Command command, | ||
200 | * CompModule compModule, | ||
201 | * AlloySolverConfiguration configuration) | ||
202 | * { | ||
203 | * this.warnings = warnings | ||
204 | * this.debugs = debugs | ||
205 | * this.reporter = reporter | ||
206 | * this.options = options | ||
207 | * this.command = command | ||
208 | * this.compModule = compModule | ||
209 | * this.configuration = configuration | ||
210 | * } | ||
211 | * | ||
212 | * override call() throws Exception { | ||
213 | * val startTime = System.currentTimeMillis | ||
214 | * | ||
215 | * // Start: Execute | ||
216 | * var A4Solution lastAnswer = null | ||
217 | * try { | ||
218 | * if(!configuration.progressMonitor.isCancelled) { | ||
219 | * do{ | ||
220 | * if(lastAnswer == null) { | ||
221 | * lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | ||
222 | * } else { | ||
223 | * lastAnswer = lastAnswer.next | ||
224 | * } | ||
225 | * configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) | ||
226 | * | ||
227 | * val runtime = System.currentTimeMillis -startTime | ||
228 | * synchronized(this) { | ||
229 | * answers += (lastAnswer->runtime) | ||
230 | * } | ||
231 | * } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) | ||
232 | * | ||
233 | * } | ||
234 | * }catch(Exception e) { | ||
235 | * warnings +=e.message | ||
236 | * } | ||
237 | * // Finish: execute | ||
238 | * return answers | ||
239 | * } | ||
240 | * | ||
241 | * def hasEnoughSolution(List<?> answers) { | ||
242 | * if(configuration.solutionScope.numberOfRequiredSolution < 0) return false | ||
243 | * else return answers.size() == configuration.solutionScope.numberOfRequiredSolution | ||
244 | * } | ||
245 | * | ||
246 | * public def getPartialAnswers() { | ||
247 | * return answers | ||
248 | * } | ||
249 | |||
250 | * } | ||
251 | * /* | ||
252 | * @Data class SolverConfiguration { | ||
253 | * VampireBackendSolver backendSolver | ||
254 | * String path | ||
255 | * String[] options | ||
256 | * } | ||
257 | */ | ||