4 files changed, 283 insertions, 1 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 9b316210..cd48a032 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
@@ -55,7 +55,7 @@ class Logic2VampireLanguageMapper {
        }
        public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem,
-                VampireSolverConfiguration configuration) {
+                VampireSolverConfiguration config) {
                // create model bases
                // TODO
                val initialComment = createVLSComment => [
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
index 01c4f5af..41e2137c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -97,6 +97,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                }
                // 5. create fof function that is an or with all the elements in map
+                // Do this only if there are more than 1 type
                val hierarch = createVLSFofFormula => [
                        it.name = "hierarchyHandler"
                        it.fofRole = "axiom"
@@ -115,6 +116,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                ]
                trace.specification.formulas += hierarch
        }
        def boolean dfsSupertypeCheck(Type type, Type type2) {
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
new file mode 100644
index 00000000..5cb0198e
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
@@ -0,0 +1,66 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
+class Vampire2LogicMapper {
+        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
+        
+        public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) {
+                val models = vampireSolution.aswers.map[it.key].toList
+                
+                if(!monitoredAlloySolution.finishedBeforeTimeout) {
+                        return createInsuficientResourcesResult => [
+                                it.problem = problem
+                                it.representation += models
+                                it.trace = trace
+                                it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
+                        ]
+                } else {
+                        if(models.last.satisfiable || requiredNumberOfSolution == -1) {
+                                return createModelResult => [
+                                        it.problem = problem
+                                        it.representation += models
+                                        it.trace = trace
+                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
+                                ]
+                        } else {
+                                return createInconsistencyResult => [
+                                        it.problem = problem
+                                        it.representation += models
+                                        it.trace = trace
+                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
+                                ]
+                        }
+                }
+        }
+        
+        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
+                createStatistics => [
+                        it.transformationTime = transformationTime as int
+                        for(solutionIndex : 0..<solution.aswers.size) {
+                                val solutionTime = solution.aswers.get(solutionIndex).value
+                                 it.entries+= createIntStatisticEntry => [
+                                        it.name = '''Answer«solutionIndex»Time'''
+                                        it.value = solutionTime.intValue
+                                ]
+                        }
+                        it.entries+= createIntStatisticEntry => [
+                                it.name = "Alloy2KodKodTransformationTime"
+                                it.value = solution.kodkodTime as int
+                        ]
+                        it.entries+= createIntStatisticEntry => [
+                                it.name = "Alloy2KodKodTransformationTime"
+                                it.value = solution.kodkodTime as int
+                        ]
+                        it.entries+= createStringStatisticEntry => [
+                                it.name = "warnings"
+                                it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
+                        ]
+                ]
+        }
+        
+        def sum(Iterable<Long> ints) {
+                ints.reduce[p1, p2|p1+p2]
+        }
+}
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
new file mode 100644
index 00000000..aefa1a7e
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
@@ -0,0 +1,214 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireBackendSolver
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
+import com.google.common.util.concurrent.SimpleTimeLimiter
+import com.google.common.util.concurrent.UncheckedTimeoutException
+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.TimeUnit
+import org.eclipse.emf.common.command.Command
+import org.eclipse.xtend.lib.annotations.Data
+class VampireSolverException 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 VampireSolutionModel{
+//      List<String> warnings
+//      List<String> debugs
+//      long kodkodTime
+//      val List<Pair<A4Solution, Long>> aswers
+//      val boolean finishedBeforeTimeout
+}
+class VampireHandler {
+        //val fileName = "problem.als"
+        
+        public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration,String vampireCode) {
+                /*
+                //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.getSolver, configuration)
+                        if(configuration.getSolver.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 limiter = new SimpleTimeLimiter
+                val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration)
+                var List<Pair<A4Solution, Long>> answers
+                var boolean finished
+                if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) {
+                        answers = callable.call
+                        finished = true
+                } else {
+                        try{
+                                answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true)
+                                finished = true
+                        } catch (UncheckedTimeoutException e) {
+                                answers = callable.partialAnswers
+                                finished = false
+                        }
+                }
+                new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished)
+                */
+        }
+        /*
+        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)
+        }
+*/
+}
+/*
+class VampireCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
+        
+        val List<String> warnings
+        val List<String> debugs
+        val A4Reporter reporter
+        val A4Options options
+        
+        val Command command
+        val CompModule compModule
+        val AlloySolverConfiguration configuration
+        
+        val List<Pair<A4Solution,Long>> answers = new LinkedList()
+        
+        new(List<String> warnings,
+                List<String> 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 {
+        VampireBackendSolver backendSolver
+        String path
+        String[] options
+}
+*/

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 9b316210..cd48a032 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
@@ -55,7 +55,7 @@ class Logic2VampireLanguageMapper {
55	}	55	}
56		56
57	public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem,	57	public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem,
58	VampireSolverConfiguration configuration) {	58	VampireSolverConfiguration config) {
59	// create model bases	59	// create model bases
60	// TODO	60	// TODO
61	val initialComment = createVLSComment => [	61	val initialComment = createVLSComment => [


diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend index 01c4f5af..41e2137c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -97,6 +97,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
97	}	97	}
98		98
99	// 5. create fof function that is an or with all the elements in map	99	// 5. create fof function that is an or with all the elements in map
		100	// Do this only if there are more than 1 type
100	val hierarch = createVLSFofFormula => [	101	val hierarch = createVLSFofFormula => [
101	it.name = "hierarchyHandler"	102	it.name = "hierarchyHandler"
102	it.fofRole = "axiom"	103	it.fofRole = "axiom"
@@ -115,6 +116,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
115	]	116	]
116		117
117	trace.specification.formulas += hierarch	118	trace.specification.formulas += hierarch
		119
118	}	120	}
119		121
120	def boolean dfsSupertypeCheck(Type type, Type type2) {	122	def boolean dfsSupertypeCheck(Type type, Type type2) {


diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend new file mode 100644 index 00000000..5cb0198e --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
@@ -0,0 +1,66 @@
		1	package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
		2
		3	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
		4	import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
		5
		6	class Vampire2LogicMapper {
		7	val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
		8
		9	public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) {
		10	val models = vampireSolution.aswers.map[it.key].toList
		11
		12	if(!monitoredAlloySolution.finishedBeforeTimeout) {
		13	return createInsuficientResourcesResult => [
		14	it.problem = problem
		15	it.representation += models
		16	it.trace = trace
		17	it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
		18	]
		19	} else {
		20	if(models.last.satisfiable \|\| requiredNumberOfSolution == -1) {
		21	return createModelResult => [
		22	it.problem = problem
		23	it.representation += models
		24	it.trace = trace
		25	it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
		26	]
		27	} else {
		28	return createInconsistencyResult => [
		29	it.problem = problem
		30	it.representation += models
		31	it.trace = trace
		32	it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
		33	]
		34	}
		35	}
		36	}
		37
		38	def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
		39	createStatistics => [
		40	it.transformationTime = transformationTime as int
		41	for(solutionIndex : 0..<solution.aswers.size) {
		42	val solutionTime = solution.aswers.get(solutionIndex).value
		43	it.entries+= createIntStatisticEntry => [
		44	it.name = '''Answer«solutionIndex»Time'''
		45	it.value = solutionTime.intValue
		46	]
		47	}
		48	it.entries+= createIntStatisticEntry => [
		49	it.name = "Alloy2KodKodTransformationTime"
		50	it.value = solution.kodkodTime as int
		51	]
		52	it.entries+= createIntStatisticEntry => [
		53	it.name = "Alloy2KodKodTransformationTime"
		54	it.value = solution.kodkodTime as int
		55	]
		56	it.entries+= createStringStatisticEntry => [
		57	it.name = "warnings"
		58	it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
		59	]
		60	]
		61	}
		62
		63	def sum(Iterable<Long> ints) {
		64	ints.reduce[p1, p2\|p1+p2]
		65	}
		66	}


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 new file mode 100644 index 00000000..aefa1a7e --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
@@ -0,0 +1,214 @@
		1	package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
		2
		3	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireBackendSolver
		4	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
		5	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
		6	import com.google.common.util.concurrent.SimpleTimeLimiter
		7	import com.google.common.util.concurrent.UncheckedTimeoutException
		8	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
		9	import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
		10	import java.util.ArrayList
		11	import java.util.HashMap
		12	import java.util.LinkedList
		13	import java.util.List
		14	import java.util.Map
		15	import java.util.concurrent.Callable
		16	import java.util.concurrent.TimeUnit
		17	import org.eclipse.emf.common.command.Command
		18	import org.eclipse.xtend.lib.annotations.Data
		19
		20	class VampireSolverException extends Exception{
		21	new(String s) { super(s) }
		22	new(String s, Exception e) { super(s,e) }
		23	new(String s, List<String> errors, Exception e) {
		24	super(s + '\n' + errors.join('\n'), e)
		25	}
		26	}
		27
		28	@Data class VampireSolutionModel{
		29	// List<String> warnings
		30	// List<String> debugs
		31	// long kodkodTime
		32	// val List<Pair<A4Solution, Long>> aswers
		33	// val boolean finishedBeforeTimeout
		34
		35
		36	}
		37
		38	class VampireHandler {
		39
		40	//val fileName = "problem.als"
		41
		42	public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration,String vampireCode) {
		43	/*
		44	//Prepare
		45	val warnings = new LinkedList<String>
		46	val debugs = new LinkedList<String>
		47	val runtime = new ArrayList<Long>
		48	val reporter = new A4Reporter() {
		49	override debug(String message) { debugs += message }
		50	override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime }
		51	override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime }
		52	override warning(ErrorWarning msg) { warnings += msg.message }
		53	}
		54
		55	val options = new A4Options() => [
		56	it.symmetry = configuration.symmetry
		57	it.noOverflow = true
		58	it.solver = getSolver(configuration.getSolver, configuration)
		59	if(configuration.getSolver.externalSolver) {
		60	it.solverDirectory = configuration.solverPath
		61	}
		62	//it.inferPartialInstance
		63	//it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString
		64	]
		65
		66	// Transform
		67	var Command command = null;
		68	var CompModule compModule = null
		69
		70	// Start: Alloy -> Kodkod
		71	val kodkodTransformStart = System.currentTimeMillis();
		72	try {
		73	compModule = CompUtil.parseEverything_fromString(reporter,alloyCode)
		74	if(compModule.allCommands.size != 1)
		75	throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''')
		76	command = compModule.allCommands.head
		77	} catch (Err e){
		78	throw new AlloySolverException(e.message,warnings,e)
		79	}
		80	val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart
		81	// Finish: Alloy -> Kodkod
		82
		83	val limiter = new SimpleTimeLimiter
		84	val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration)
		85	var List<Pair<A4Solution, Long>> answers
		86	var boolean finished
		87	if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) {
		88	answers = callable.call
		89	finished = true
		90	} else {
		91	try{
		92	answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true)
		93	finished = true
		94	} catch (UncheckedTimeoutException e) {
		95	answers = callable.partialAnswers
		96	finished = false
		97	}
		98	}
		99
		100	new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished)
		101	*/
		102	}
		103	/*
		104	val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap
		105	def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) {
		106	val config = new SolverConfiguration(backedSolver,path,options)
		107	if(previousSolverConfigurations.containsKey(config)) {
		108	return previousSolverConfigurations.get(config)
		109	} else {
		110	val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»'''
		111	val newSolver = A4Options.SatSolver.make(id,id,path,options)
		112	previousSolverConfigurations.put(config,newSolver)
		113	return newSolver
		114	}
		115	}
		116
		117	def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) {
		118	switch(backedSolver){
		119	case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE
		120	case SpearPIPE: return A4Options.SatSolver.SpearPIPE
		121	case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI
		122	case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI
		123	case LingelingJNI: return A4Options.SatSolver.LingelingJNI
		124	case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null)
		125	case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI
		126	case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI
		127	case SAT4J: return A4Options.SatSolver.SAT4J
		128	case CNF: return A4Options.SatSolver.CNF
		129	case KodKod: return A4Options.SatSolver.KK
		130	}
		131	}
		132
		133	def isExternalSolver(AlloyBackendSolver backedSolver) {
		134	return !(backedSolver == AlloyBackendSolver.SAT4J)
		135	}
		136	*/
		137	}
		138	/*
		139	class VampireCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
		140
		141	val List<String> warnings
		142	val List<String> debugs
		143	val A4Reporter reporter
		144	val A4Options options
		145
		146	val Command command
		147	val CompModule compModule
		148	val AlloySolverConfiguration configuration
		149
		150	val List<Pair<A4Solution,Long>> answers = new LinkedList()
		151
		152	new(List<String> warnings,
		153	List<String> debugs,
		154	A4Reporter reporter,
		155	A4Options options,
		156	Command command,
		157	CompModule compModule,
		158	AlloySolverConfiguration configuration)
		159	{
		160	this.warnings = warnings
		161	this.debugs = debugs
		162	this.reporter = reporter
		163	this.options = options
		164	this.command = command
		165	this.compModule = compModule
		166	this.configuration = configuration
		167	}
		168
		169	override call() throws Exception {
		170	val startTime = System.currentTimeMillis
		171
		172	// Start: Execute
		173	var A4Solution lastAnswer = null
		174	try {
		175	if(!configuration.progressMonitor.isCancelled) {
		176	do{
		177	if(lastAnswer == null) {
		178	lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
		179	} else {
		180	lastAnswer = lastAnswer.next
		181	}
		182	configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution)
		183
		184	val runtime = System.currentTimeMillis -startTime
		185	synchronized(this) {
		186	answers += (lastAnswer->runtime)
		187	}
		188	} while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled)
		189
		190	}
		191	}catch(Exception e) {
		192	warnings +=e.message
		193	}
		194	// Finish: execute
		195	return answers
		196	}
		197
		198	def hasEnoughSolution(List<?> answers) {
		199	if(configuration.solutionScope.numberOfRequiredSolution < 0) return false
		200	else return answers.size() == configuration.solutionScope.numberOfRequiredSolution
		201	}
		202
		203	public def getPartialAnswers() {
		204	return answers
		205	}
		206
		207	}
		208	/*
		209	@Data class SolverConfiguration {
		210	VampireBackendSolver backendSolver
		211	String path
		212	String[] options
		213	}
		214	*/