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> 2019-02-01 16:03:30 -0500
commit: 717916e99b2c8e7965fb31f4448b4336d8c2f19a (patch)
tree: 074c77b8465f1e47e7a28af2d95f79c1f5abaf86 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse
parent: FAM MM transformation works (diff)
download: VIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.tar.gz
VIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.tar.zst
VIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.zip
5 files changed, 312 insertions, 28 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
index 64484b88..cbe53bff 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -1,18 +1,18 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner
+import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
 import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
-import java.io.PrintWriter
-import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes
 class VampireSolver extends LogicReasoner{
        
@@ -23,14 +23,14 @@ class VampireSolver extends LogicReasoner{
        }
        
         val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
-//       //not for now
+         val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
-//       val VampireHandler handler = new VampireHandler
+         val VampireHandler handler = new VampireHandler
-//       val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
         
-         val fileName = "problem.tptp"
         
-         override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
+         val fileName = "vampireProblem.tptp"
-                val vampireConfig = configuration.asConfig
+         
+         override solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace) throws LogicReasonerException {
+                val vampireConfig = config.asConfig
                
                // Start: Logic -> Vampire mapping
                val transformationStart = System.currentTimeMillis
@@ -41,36 +41,38 @@ class VampireSolver extends LogicReasoner{
                
                var String fileURI = null;
                var String vampireCode = null;
+                vampireCode = workspace.writeModelToString(vampireProblem,fileName)
                if(vampireConfig.writeToFile) {
                        fileURI = workspace.writeModel(vampireProblem,fileName).toFileString
-                } else {
+                }
-                        vampireCode = workspace.writeModelToString(vampireProblem,fileName)
+                
-                } 
+                //Result as String
+                                
                val transformationTime = System.currentTimeMillis - transformationStart
                // Finish: Logic -> Vampire mapping
                
-                //Creates a file containing the tptp code after transformation
+                                
-                val out = new PrintWriter("output/files/vampireCode.tptp")
+                /*        
-                out.println(vampireCode)
-                out.close()
-                
-                
-                /*      
-                 * not for now -> Start: Solving Alloy problem
-                 *  
                // Start: Solving Alloy problem
                val solverStart = System.currentTimeMillis
-                val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode)
+                //Calling Solver (Currently Manually)
-                val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
+                val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode)
+//              val result2 = null
+                //TODO
+                //Backwards Mapper
+                val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
+                
                val solverFinish = System.currentTimeMillis-solverStart
                // Finish: Solving Alloy problem
                                
                if(vampireConfig.writeToFile) workspace.deactivateModel(fileName)
                
                return logicResult
-                */
                
+                /*/
                return null // for now
+                //*/
        }
        
        def asConfig(LogicSolverConfiguration configuration){
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
+}
+*/
author	ArenBabikian <aren.babikian@mail.mcgill.ca>	2019-02-01 16:03:30 -0500
committer	ArenBabikian <aren.babikian@mail.mcgill.ca>	2019-02-01 16:03:30 -0500
commit	717916e99b2c8e7965fb31f4448b4336d8c2f19a (patch)
tree	074c77b8465f1e47e7a28af2d95f79c1f5abaf86 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse
parent	FAM MM transformation works (diff)
download	VIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.tar.gz VIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.tar.zst VIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.zip

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend index 64484b88..cbe53bff 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -1,18 +1,18 @@
1	package ca.mcgill.ecse.dslreasoner.vampire.reasoner	1	package ca.mcgill.ecse.dslreasoner.vampire.reasoner
2		2
		3	import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
3	import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated	4	import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated
		5	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper
		6	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes
		7	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper
		8	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
		9	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
4	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner	10	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
5	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException	11	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
6	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration	12	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
7	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem	13	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
8	import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult	14	import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
9	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper
10	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
11	import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace	15	import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
12	import java.io.PrintWriter
13	import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
14	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper
15	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes
16		16
17	class VampireSolver extends LogicReasoner{	17	class VampireSolver extends LogicReasoner{
18		18
@@ -23,14 +23,14 @@ class VampireSolver extends LogicReasoner{
23	}	23	}
24		24
25	val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)	25	val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
26	// //not for now	26	val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
27	// val VampireHandler handler = new VampireHandler	27	val VampireHandler handler = new VampireHandler
28	// val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
29		28
30	val fileName = "problem.tptp"
31		29
32	override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {	30	val fileName = "vampireProblem.tptp"
33	val vampireConfig = configuration.asConfig	31
		32	override solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace) throws LogicReasonerException {
		33	val vampireConfig = config.asConfig
34		34
35	// Start: Logic -> Vampire mapping	35	// Start: Logic -> Vampire mapping
36	val transformationStart = System.currentTimeMillis	36	val transformationStart = System.currentTimeMillis
@@ -41,36 +41,38 @@ class VampireSolver extends LogicReasoner{
41		41
42	var String fileURI = null;	42	var String fileURI = null;
43	var String vampireCode = null;	43	var String vampireCode = null;
		44	vampireCode = workspace.writeModelToString(vampireProblem,fileName)
44	if(vampireConfig.writeToFile) {	45	if(vampireConfig.writeToFile) {
45	fileURI = workspace.writeModel(vampireProblem,fileName).toFileString	46	fileURI = workspace.writeModel(vampireProblem,fileName).toFileString
46	} else {	47	}
47	vampireCode = workspace.writeModelToString(vampireProblem,fileName)	48
48	}	49	//Result as String
		50
		51
49	val transformationTime = System.currentTimeMillis - transformationStart	52	val transformationTime = System.currentTimeMillis - transformationStart
50	// Finish: Logic -> Vampire mapping	53	// Finish: Logic -> Vampire mapping
51		54
52	//Creates a file containing the tptp code after transformation	55
53	val out = new PrintWriter("output/files/vampireCode.tptp")	56	/*
54	out.println(vampireCode)
55	out.close()
56
57
58	/*
59	* not for now -> Start: Solving Alloy problem
60	*
61	// Start: Solving Alloy problem	57	// Start: Solving Alloy problem
62	val solverStart = System.currentTimeMillis	58	val solverStart = System.currentTimeMillis
63	val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode)	59	//Calling Solver (Currently Manually)
64	val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)	60	val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode)
		61	// val result2 = null
		62	//TODO
		63	//Backwards Mapper
		64	val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
		65
65	val solverFinish = System.currentTimeMillis-solverStart	66	val solverFinish = System.currentTimeMillis-solverStart
66	// Finish: Solving Alloy problem	67	// Finish: Solving Alloy problem
67		68
68	if(vampireConfig.writeToFile) workspace.deactivateModel(fileName)	69	if(vampireConfig.writeToFile) workspace.deactivateModel(fileName)
69		70
70	return logicResult	71	return logicResult
71	*/
72		72
		73	/*/
73	return null // for now	74	return null // for now
		75	//*/
74	}	76	}
75		77
76	def asConfig(LogicSolverConfiguration configuration){	78	def asConfig(LogicSolverConfiguration configuration){


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