From 32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 25 Oct 2019 04:15:39 -0400 Subject: VAMPIRE: post-submission push --- .../alloy/reasoner/builder/AlloyHandler.xtend | 228 +++++++++++++++++++++ 1 file changed, 228 insertions(+) create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend') 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 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import edu.mit.csail.sdg.alloy4.A4Reporter +import edu.mit.csail.sdg.alloy4.Err +import edu.mit.csail.sdg.alloy4.ErrorWarning +import edu.mit.csail.sdg.alloy4compiler.ast.Command +import edu.mit.csail.sdg.alloy4compiler.parser.CompModule +import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil +import edu.mit.csail.sdg.alloy4compiler.translator.A4Options +import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution +import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.util.ArrayList +import java.util.HashMap +import java.util.LinkedList +import java.util.List +import java.util.Map +import java.util.concurrent.Callable +import java.util.concurrent.ExecutionException +import java.util.concurrent.ExecutorService +import java.util.concurrent.Executors +import java.util.concurrent.TimeUnit +import java.util.concurrent.TimeoutException +import org.eclipse.xtend.lib.annotations.Data + +class AlloySolverException extends Exception{ + new(String s) { super(s) } + new(String s, Exception e) { super(s,e) } + new(String s, List errors, Exception e) { + super(s + '\n' + errors.join('\n'), e) + } +} + +@Data class MonitoredAlloySolution{ + List warnings + List debugs + long kodkodTime + val List> aswers + val boolean finishedBeforeTimeout +} + +class AlloyHandler { + + //val fileName = "problem.als" + + def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { + + //Prepare + val warnings = new LinkedList + val debugs = new LinkedList + val runtime = new ArrayList + val reporter = new A4Reporter() { + override debug(String message) { debugs += message } + override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } + override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } + override warning(ErrorWarning msg) { warnings += msg.message } + } + + val options = new A4Options() => [ + it.symmetry = configuration.symmetry + it.noOverflow = true + it.solver = getSolver(configuration.solver, configuration) + if(configuration.solver.externalSolver) { + it.solverDirectory = configuration.solverPath + } + //it.inferPartialInstance + //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString + ] + + // Transform + var Command command = null; + var CompModule compModule = null + + // Start: Alloy -> Kodkod + val kodkodTransformStart = System.currentTimeMillis(); + try { + compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) + if(compModule.allCommands.size != 1) + throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') + command = compModule.allCommands.head + } catch (Err e){ + throw new AlloySolverException(e.message,warnings,e) + } + val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart + // Finish: Alloy -> Kodkod + + val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) + var List> answers + var boolean finished + if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { + answers = callable.call + finished = true + } else { + val ExecutorService executor = Executors.newCachedThreadPool(); + val future = executor.submit(callable) + try{ + answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS) + finished = true + } catch (TimeoutException ex) { + // handle the timeout + } catch (InterruptedException e) { + // handle the interrupts + } catch (ExecutionException e) { + // handle other exceptions + } finally { + future.cancel(true); + + answers = callable.partialAnswers + finished = false + } + } + + new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) + } + + val static Map previousSolverConfigurations = new HashMap + def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { + val config = new SolverConfiguration(backedSolver,path,options) + if(previousSolverConfigurations.containsKey(config)) { + return previousSolverConfigurations.get(config) + } else { + val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' + val newSolver = A4Options.SatSolver.make(id,id,path,options) + previousSolverConfigurations.put(config,newSolver) + return newSolver + } + } + + def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { + switch(backedSolver){ + case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE + case SpearPIPE: return A4Options.SatSolver.SpearPIPE + case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI + case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI + case LingelingJNI: return A4Options.SatSolver.LingelingJNI + case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) + case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI + case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI + case SAT4J: return A4Options.SatSolver.SAT4J + case CNF: return A4Options.SatSolver.CNF + case KodKod: return A4Options.SatSolver.KK + } + } + + def isExternalSolver(AlloyBackendSolver backedSolver) { + return !(backedSolver == AlloyBackendSolver.SAT4J) + } +} + +class AlloyCallerWithTimeout implements Callable>>{ + + val List warnings + val List debugs + val A4Reporter reporter + val A4Options options + + val Command command + val CompModule compModule + val AlloySolverConfiguration configuration + + val List> answers = new LinkedList() + + new(List warnings, + List debugs, + A4Reporter reporter, + A4Options options, + Command command, + CompModule compModule, + AlloySolverConfiguration configuration) + { + this.warnings = warnings + this.debugs = debugs + this.reporter = reporter + this.options = options + this.command = command + this.compModule = compModule + this.configuration = configuration + } + + override call() throws Exception { + val startTime = System.currentTimeMillis + + // Start: Execute + var A4Solution lastAnswer = null + try { + if(!configuration.progressMonitor.isCancelled) { + do{ + if(lastAnswer == null) { + lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) + } else { + lastAnswer = lastAnswer.next + } + configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) + + val runtime = System.currentTimeMillis -startTime + synchronized(this) { + answers += (lastAnswer->runtime) + } + } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) + + } + }catch(Exception e) { + warnings +=e.message + } + // Finish: execute + return answers + } + + def hasEnoughSolution(List answers) { + if(configuration.solutionScope.numberOfRequiredSolution < 0) return false + else return answers.size() == configuration.solutionScope.numberOfRequiredSolution + } + + public def getPartialAnswers() { + return answers + } +} + +@Data class SolverConfiguration { + AlloyBackendSolver backedSolver + String path + String[] options +} \ No newline at end of file -- cgit v1.2.3-70-g09d2