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 @@
+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.A4Solution
+import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
+import java.util.LinkedList
+import java.util.List
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
+import org.eclipse.xtend.lib.annotations.Data
+import java.util.Map
+import java.util.HashMap
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver
+import org.eclipse.emf.common.CommonPlugin
+import java.util.ArrayList
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
+class AlloySolverException extends Exception{
+        new(String s) { super(s) }
+        new(String s, Exception e) { super(s,e) }
+        new(String s, List<String> errors, Exception e) {
+                super(s + '\n' + errors.join('\n'), e)
+        }
+}
+@Data class MonitoredAlloySolution{
+        List<String> warnings
+        List<String> debugs
+        long kodkodTime
+        long runtimeTime
+        
+        A4Solution solution
+}
+class AlloyHandler {
+        
+        //val fileName = "problem.als"
+        
+        public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, String alloyCode) {
+                //Prepare
+                
+                val warnings = new LinkedList<String>
+                val debugs = new LinkedList<String>
+                val runtime = new ArrayList<Long>
+                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.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString
+                ]
+                
+                // Transform
+                var Command command = null;
+                var CompModule compModule = null
+                
+                val kodkodTransformStart = System.currentTimeMillis();
+                
+                try {
+                        if(configuration.writeToFile) {
+                                compModule = CompUtil.parseEverything_fromFile(reporter,null,path)
+                        } else {
+                                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
+                
+                //Execute
+                var A4Solution answer = null;
+                try {
+                        answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
+                }catch(Exception e) {
+                        warnings +=e.message
+                }
+                
+                var long runtimeFromAnswer;
+                if(runtime.empty) {
+                        runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish)
+                } else {
+                        runtimeFromAnswer = runtime.head
+                }
+                
+                return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer)
+        }
+        
+        val static Map<SolverConfiguration, SatSolver> 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)
+        }
+}
+@Data class SolverConfiguration {
+        AlloyBackendSolver backedSolver
+        String path
+        String[] options
+}

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	}