From 15602c7cfbfc80b8c826855b94c9f9582650dd21 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 29 Aug 2019 06:26:02 -0400 Subject: VAMPIRE: adapt grammar to Vampire solution + get model from text --- .../vampire/reasoner/VampireSolver.xtend | 14 +- .../builder/Logic2VampireLanguageMapper.xtend | 10 +- ...c2VampireLanguageMapper_ContainmentMapper.xtend | 2 +- .../vampire/reasoner/builder/VampireHandler.xtend | 417 ++++++++++----------- 4 files changed, 225 insertions(+), 218 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill') 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 6bb49080..1fd40801 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 @@ -6,6 +6,8 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage 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 ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel +import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException @@ -13,7 +15,7 @@ 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 hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper +import org.eclipse.emf.ecore.resource.Resource class VampireSolver extends LogicReasoner { @@ -55,6 +57,16 @@ class VampireSolver extends LogicReasoner { if (writeFile) { fileURI = workspace.writeModel(vampireProblem, fileName).toFileString } + + + +// Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("tptp", new VampireLanguageFactoryImpl) +//// val Resource resource = Resource. +//// Resource.getResource(wsURI+"problem.tptp") as Resource +//// resource +// val model = workspace.readModel(VampireModel, "problem.tptp").eResource.contents +// println(model) + // Result as String val transformationTime = System.currentTimeMillis - transformationStart 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 13db3c99..a2449fc0 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 @@ -61,7 +61,7 @@ class Logic2VampireLanguageMapper { // create model bases // TODO val initialComment = createVLSComment => [ - it.comment = "This is an initial Test Comment" + it.comment = "%This is an initial Test Comment" ] val specification = createVampireModel => [ @@ -163,10 +163,10 @@ class Logic2VampireLanguageMapper { createVLSInt => [it.value = literal.value.toString()] } - def dispatch protected VLSTerm transformTerm(RealLiteral literal, Logic2VampireLanguageMapperTrace trace, - Map variables) { - createVLSReal => [it.value = literal.value.toString()] - } +// def dispatch protected VLSTerm transformTerm(RealLiteral literal, Logic2VampireLanguageMapperTrace trace, +// Map variables) { +// createVLSReal => [it.value = literal.value.toString()] +// } def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace, Map variables) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index 93c28e7c..c79003bd 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend @@ -189,7 +189,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { // STEP 2 CONT'D for (e : type2cont.entrySet) { - println(e.key + " " + e.value) +// println(e.key + " " + e.value) val relFormula = createVLSFofFormula => [ it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) it.fofRole = "axiom" 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 index 274396ee..f0426245 100644 --- 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 @@ -9,31 +9,35 @@ import java.util.List import org.eclipse.emf.ecore.resource.Resource import org.eclipse.xtend.lib.annotations.Data import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl +import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl + +class VampireSolverException extends Exception { + new(String s) { + super(s) + } + + new(String s, Exception e) { + super(s, e) + } -class VampireSolverException extends Exception{ - new(String s) { super(s) } - new(String s, Exception e) { super(s,e) } new(String s, List errors, Exception e) { super(s + '\n' + errors.join('\n'), e) } } -@Data class VampireSolutionModel{ +@Data class VampireSolutionModel { // List warnings // List debugs // long kodkodTime // val List> aswers // val boolean finishedBeforeTimeout - - } class VampireHandler { - //val fileName = "problem.als" - + // val fileName = "problem.als" public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration) { - + val CMD = "cmd /c " val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\" val VAMPNAME = "vampire.exe" @@ -41,222 +45,213 @@ class VampireHandler { val OPTION = " --mode casc_sat " val SOLNNAME = "solution.tptp" val PATH = "C:/cygwin64/bin" - + val wsURI = workspace.workspaceURI val tempLoc = wsURI + TEMPNAME val solnLoc = wsURI + SOLNNAME + " " val vampLoc = VAMPDIR + VAMPNAME - - - //1. create temp file for vampire problem + + // 1. create temp file for vampire problem var tempURI = workspace.writeModel(problem, TEMPNAME).toFileString - - //2. run command and save to - //need to have cygwin downloaded - - - - - val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) - //2.1 determine time left - p.waitFor - - //2.2 store output into local variable - val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); - val List output = newArrayList - var line = ""; - while ((line = reader.readLine())!= null) { - output.add(line + "\n"); - } + // 2. run command and save to + // need to have cygwin downloaded + val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH)) + // 2.1 determine time left + p.waitFor -// println(output.toString()) + // 2.2 store output into local variable + val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream())); + val List output = newArrayList - //4. delete temp file - workspace.getFile(TEMPNAME).delete - - //5. determine and return whether or not finite model was found - - //6. save solution as a .tptp model - Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new VampireLanguageFactoryImpl) - workspace.readModel(VampireModel, SOLNNAME).eResource.contents - - - - - - - - - /* - //Prepare - val warnings = new LinkedList - val debugs = new LinkedList - val runtime = new ArrayList - val reporter = new A4Reporter() { - override debug(String message) { debugs += message } - override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } - override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } - override warning(ErrorWarning msg) { warnings += msg.message } + var line = ""; + while ((line = reader.readLine()) != null) { + output.add(line + "\n"); } + +// println(output.toString()) + // 4. delete temp file + workspace.getFile(TEMPNAME).delete + + // 5. determine and return whether or not finite model was found + // 6. save solution as a .tptp model + val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents - 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 + + + println((root.get(0) as VampireModelImpl ).comments) - val limiter = new SimpleTimeLimiter - val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) - var List> answers - var boolean finished - if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { - answers = callable.call - finished = true - } else { - try{ - answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) - finished = true - } catch (UncheckedTimeoutException e) { - answers = callable.partialAnswers - finished = false - } - } + return root - new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) - */ - } /* - val static Map previousSolverConfigurations = new HashMap - def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { - val config = new SolverConfiguration(backedSolver,path,options) - if(previousSolverConfigurations.containsKey(config)) { - return previousSolverConfigurations.get(config) - } else { - val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' - val newSolver = A4Options.SatSolver.make(id,id,path,options) - previousSolverConfigurations.put(config,newSolver) - return newSolver - } - } - - def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { - switch(backedSolver){ - case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE - case SpearPIPE: return A4Options.SatSolver.SpearPIPE - case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI - case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI - case LingelingJNI: return A4Options.SatSolver.LingelingJNI - case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) - case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI - case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI - case SAT4J: return A4Options.SatSolver.SAT4J - case CNF: return A4Options.SatSolver.CNF - case KodKod: return A4Options.SatSolver.KK - } - } - - def isExternalSolver(AlloyBackendSolver backedSolver) { - return !(backedSolver == AlloyBackendSolver.SAT4J) + * //Prepare + * val warnings = new LinkedList + * val debugs = new LinkedList + * val runtime = new ArrayList + * val reporter = new A4Reporter() { + * override debug(String message) { debugs += message } + * override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } + * override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } + * override warning(ErrorWarning msg) { warnings += msg.message } + * } + * + * val options = new A4Options() => [ + * it.symmetry = configuration.symmetry + * it.noOverflow = true + * it.solver = getSolver(configuration.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> 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) + */ } -*/ -} /* -class VampireCallerWithTimeout implements Callable>>{ - - val List warnings - val List debugs - val A4Reporter reporter - val A4Options options - - val Command command - val CompModule compModule - val AlloySolverConfiguration configuration - - val List> answers = new LinkedList() - - new(List warnings, - List debugs, - A4Reporter reporter, - A4Options options, - Command command, - CompModule compModule, - AlloySolverConfiguration configuration) - { - this.warnings = warnings - this.debugs = debugs - this.reporter = reporter - this.options = options - this.command = command - this.compModule = compModule - this.configuration = configuration - } - - override call() throws Exception { - val startTime = System.currentTimeMillis - - // Start: Execute - var A4Solution lastAnswer = null - try { - if(!configuration.progressMonitor.isCancelled) { - do{ - if(lastAnswer == null) { - lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) - } else { - lastAnswer = lastAnswer.next - } - configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) - - val runtime = System.currentTimeMillis -startTime - synchronized(this) { - answers += (lastAnswer->runtime) - } - } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) - - } - }catch(Exception e) { - warnings +=e.message - } - // Finish: execute - return answers - } - - def hasEnoughSolution(List answers) { - if(configuration.solutionScope.numberOfRequiredSolution < 0) return false - else return answers.size() == configuration.solutionScope.numberOfRequiredSolution - } - - public def getPartialAnswers() { - return answers - } - + * val static Map previousSolverConfigurations = new HashMap + * def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { + * val config = new SolverConfiguration(backedSolver,path,options) + * if(previousSolverConfigurations.containsKey(config)) { + * return previousSolverConfigurations.get(config) + * } else { + * val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' + * val newSolver = A4Options.SatSolver.make(id,id,path,options) + * previousSolverConfigurations.put(config,newSolver) + * return newSolver + * } + * } + * + * def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { + * switch(backedSolver){ + * case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE + * case SpearPIPE: return A4Options.SatSolver.SpearPIPE + * case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI + * case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI + * case LingelingJNI: return A4Options.SatSolver.LingelingJNI + * case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) + * case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI + * case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI + * case SAT4J: return A4Options.SatSolver.SAT4J + * case CNF: return A4Options.SatSolver.CNF + * case KodKod: return A4Options.SatSolver.KK + * } + * } + * + * def isExternalSolver(AlloyBackendSolver backedSolver) { + * return !(backedSolver == AlloyBackendSolver.SAT4J) + * } + */ } /* -@Data class SolverConfiguration { - VampireBackendSolver backendSolver - String path - String[] options -} -*/ + * class VampireCallerWithTimeout implements Callable>>{ + * + * val List warnings + * val List debugs + * val A4Reporter reporter + * val A4Options options + * + * val Command command + * val CompModule compModule + * val AlloySolverConfiguration configuration + * + * val List> answers = new LinkedList() + * + * new(List warnings, + * List debugs, + * A4Reporter reporter, + * A4Options options, + * Command command, + * CompModule compModule, + * AlloySolverConfiguration configuration) + * { + * this.warnings = warnings + * this.debugs = debugs + * this.reporter = reporter + * this.options = options + * this.command = command + * this.compModule = compModule + * this.configuration = configuration + * } + * + * override call() throws Exception { + * val startTime = System.currentTimeMillis + * + * // Start: Execute + * var A4Solution lastAnswer = null + * try { + * if(!configuration.progressMonitor.isCancelled) { + * do{ + * if(lastAnswer == null) { + * lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) + * } else { + * lastAnswer = lastAnswer.next + * } + * configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) + * + * val runtime = System.currentTimeMillis -startTime + * synchronized(this) { + * answers += (lastAnswer->runtime) + * } + * } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) + * + * } + * }catch(Exception e) { + * warnings +=e.message + * } + * // Finish: execute + * return answers + * } + * + * def hasEnoughSolution(List answers) { + * if(configuration.solutionScope.numberOfRequiredSolution < 0) return false + * else return answers.size() == configuration.solutionScope.numberOfRequiredSolution + * } + * + * public def getPartialAnswers() { + * return answers + * } + + * } + * /* + * @Data class SolverConfiguration { + * VampireBackendSolver backendSolver + * String path + * String[] options + * } + */ -- cgit v1.2.3-54-g00ecf