aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
diff options
context:
space:
mode:
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.xtend417
1 files changed, 206 insertions, 211 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
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
9import org.eclipse.emf.ecore.resource.Resource 9import org.eclipse.emf.ecore.resource.Resource
10import org.eclipse.xtend.lib.annotations.Data 10import org.eclipse.xtend.lib.annotations.Data
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl 11import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl
13
14class 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
13class 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
31class VampireHandler { 36class 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/*
187class 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 */
generated by cgit v1.2.3-54-g00ecf (git 2.45.1) at 2024-05-28 01:21:19 +0000