Fix FAM Test. Begin Grammar Fix.

author: ArenBabikian <aren.babikian@mail.mcgill.ca> 2019-02-01 16:03:30 -0500
committer: ArenBabikian <aren.babikian@mail.mcgill.ca> 2020-06-07 19:06:28 -0400
commit: 57e614aabedc176ba9965d0ca5e6daa23c5f4758 (patch)
tree: 16806454dff463419af99b14f6abfab3d1fa5291 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
parent: FAM MM transformation works (diff)
download: VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.gz
VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.zst
VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.zip
1 files changed, 214 insertions, 0 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
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
+}
+*/
author	ArenBabikian <aren.babikian@mail.mcgill.ca>	2019-02-01 16:03:30 -0500
committer	ArenBabikian <aren.babikian@mail.mcgill.ca>	2020-06-07 19:06:28 -0400
commit	57e614aabedc176ba9965d0ca5e6daa23c5f4758 (patch)
tree	16806454dff463419af99b14f6abfab3d1fa5291 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
parent	FAM MM transformation works (diff)
download	VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.gz VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.zst VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.zip

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	*/