From 9ef9aef5ef8baa7e579d4eb4a5d27a7983f32c8b 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/builder/VampireHandler.java | 64 ++++++++++------------ 1 file changed, 30 insertions(+), 34 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java index 1479e6b7..7f6ce1c6 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java @@ -1,59 +1,55 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl; import com.google.common.base.Objects; import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; import java.io.BufferedReader; import java.io.InputStream; import java.io.InputStreamReader; import java.util.List; -import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.common.util.URI; import org.eclipse.emf.ecore.EObject; -import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.xtext.xbase.lib.CollectionLiterals; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.Exceptions; +import org.eclipse.xtext.xbase.lib.InputOutput; @SuppressWarnings("all") public class VampireHandler { public EList callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) { try { - EList _xblockexpression = null; - { - final String CMD = "cmd /c "; - final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; - final String VAMPNAME = "vampire.exe"; - final String TEMPNAME = "TEMP.tptp"; - final String OPTION = " --mode casc_sat "; - final String SOLNNAME = "solution.tptp"; - final String PATH = "C:/cygwin64/bin"; - final URI wsURI = workspace.getWorkspaceURI(); - final String tempLoc = (wsURI + TEMPNAME); - String _plus = (wsURI + SOLNNAME); - final String solnLoc = (_plus + " "); - final String vampLoc = (VAMPDIR + VAMPNAME); - String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); - final Process p = Runtime.getRuntime().exec((((((CMD + vampLoc) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.newArrayList(("Path=" + PATH)), String.class))); - p.waitFor(); - InputStream _inputStream = p.getInputStream(); - InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream); - final BufferedReader reader = new BufferedReader(_inputStreamReader); - final List output = CollectionLiterals.newArrayList(); - String line = ""; - while ((!Objects.equal((line = reader.readLine()), null))) { - output.add((line + "\n")); - } - workspace.getFile(TEMPNAME).delete(); - Map _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap(); - VampireLanguageFactoryImpl _vampireLanguageFactoryImpl = new VampireLanguageFactoryImpl(); - _extensionToFactoryMap.put("*", _vampireLanguageFactoryImpl); - _xblockexpression = workspace.readModel(VampireModel.class, SOLNNAME).eResource().getContents(); + final String CMD = "cmd /c "; + final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; + final String VAMPNAME = "vampire.exe"; + final String TEMPNAME = "TEMP.tptp"; + final String OPTION = " --mode casc_sat "; + final String SOLNNAME = "solution.tptp"; + final String PATH = "C:/cygwin64/bin"; + final URI wsURI = workspace.getWorkspaceURI(); + final String tempLoc = (wsURI + TEMPNAME); + String _plus = (wsURI + SOLNNAME); + final String solnLoc = (_plus + " "); + final String vampLoc = (VAMPDIR + VAMPNAME); + String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); + final Process p = Runtime.getRuntime().exec((((((CMD + vampLoc) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.newArrayList(("Path=" + PATH)), String.class))); + p.waitFor(); + InputStream _inputStream = p.getInputStream(); + InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream); + final BufferedReader reader = new BufferedReader(_inputStreamReader); + final List output = CollectionLiterals.newArrayList(); + String line = ""; + while ((!Objects.equal((line = reader.readLine()), null))) { + output.add((line + "\n")); } - return _xblockexpression; + workspace.getFile(TEMPNAME).delete(); + final EList root = workspace.readModel(VampireModel.class, SOLNNAME).eResource().getContents(); + EObject _get = root.get(0); + InputOutput.>println(((VampireModelImpl) _get).getComments()); + return root; } catch (Throwable _e) { throw Exceptions.sneakyThrow(_e); } -- cgit v1.2.3-70-g09d2