VAMPIRE: adapt grammar to Vampire solution + get model from text

21 files changed, 280 insertions, 290 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 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<Variable, VLSVariable> variables) {
-                createVLSReal => [it.value = literal.value.toString()]
-        }
+//      def dispatch protected VLSTerm transformTerm(RealLiteral literal, Logic2VampireLanguageMapperTrace trace,
+//              Map<Variable, VLSVariable> variables) {
+//              createVLSReal => [it.value = literal.value.toString()]
+//      }
 
         def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> 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<String> errors, Exception e) {

                 super(s + '\n' + errors.join('\n'), e)

         }

 }

 

-@Data class VampireSolutionModel{

+@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"

-        

+        // 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<String> 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<String> 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<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 }

+                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<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

-                        }

-                }

+                return root

 

-                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)

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

+         */

         }

-*/

-}

 /*

-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

-        }

-

+ * 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)

+ * }

+ */

 }

 /*

-@Data class SolverConfiguration {

-        VampireBackendSolver backendSolver

-        String path

-        String[] options

-}

-*/

+ * 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/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index a7942958..43992ea0 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 487f9569..19608361 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index bd61b874..791a9524 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index 2e58cecd..89003c27 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index 1b894303..b37d993a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 4b7fd4bf..45afcecc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 6626adf4..0f4dc63a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index 339baea9..ab58fcab 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index 868f30e7..cf19663e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index 08ffcb3b..0b2cb192 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index 65f58281..58da7ccd 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -16,7 +16,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

@@ -44,7 +43,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or;

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition;

@@ -98,7 +96,7 @@ public class Logic2VampireLanguageMapper {
   public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) {

     VLSComment _createVLSComment = this.factory.createVLSComment();

     final Procedure1<VLSComment> _function = (VLSComment it) -> {

-      it.setComment("This is an initial Test Comment");

+      it.setComment("%This is an initial Test Comment");

     };

     final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function);

     VampireModel _createVampireModel = this.factory.createVampireModel();

@@ -202,14 +200,6 @@ public class Logic2VampireLanguageMapper {
     return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function);

   }

   

-  protected VLSTerm _transformTerm(final RealLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

-    VLSReal _createVLSReal = this.factory.createVLSReal();

-    final Procedure1<VLSReal> _function = (VLSReal it) -> {

-      it.setValue(literal.getValue().toString());

-    };

-    return ObjectExtensions.<VLSReal>operator_doubleArrow(_createVLSReal, _function);

-  }

-  

   protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

     VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

     final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> {

@@ -394,8 +384,6 @@ public class Logic2VampireLanguageMapper {
       return _transformTerm((Not)and, trace, variables);

     } else if (and instanceof Or) {

       return _transformTerm((Or)and, trace, variables);

-    } else if (and instanceof RealLiteral) {

-      return _transformTerm((RealLiteral)and, trace, variables);

     } else if (and instanceof InstanceOf) {

       return _transformTerm((InstanceOf)and, trace, variables);

     } else if (and instanceof SymbolicValue) {

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
index dd549c29..7daf1b2f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
@@ -15,6 +15,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

@@ -37,7 +38,6 @@ import org.eclipse.emf.common.util.EList;
 import org.eclipse.xtext.xbase.lib.CollectionLiterals;

 import org.eclipse.xtext.xbase.lib.Conversions;

 import org.eclipse.xtext.xbase.lib.Extension;

-import org.eclipse.xtext.xbase.lib.InputOutput;

 import org.eclipse.xtext.xbase.lib.ObjectExtensions;

 import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;

 

@@ -123,7 +123,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

       final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {

-        EList<VLSVariable> _variables = it_1.getVariables();

+        EList<VLSVariableDeclaration> _variables = it_1.getVariables();

         VLSVariable _duplicate = this.support.duplicate(this.variable);

         _variables.add(_duplicate);

         VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -193,10 +193,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
           it.setFofRole("axiom");

           VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

           final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> {

-            EList<VLSVariable> _variables = it_1.getVariables();

+            EList<VLSVariableDeclaration> _variables = it_1.getVariables();

             VLSVariable _duplicate = this.support.duplicate(varA);

             _variables.add(_duplicate);

-            EList<VLSVariable> _variables_1 = it_1.getVariables();

+            EList<VLSVariableDeclaration> _variables_1 = it_1.getVariables();

             VLSVariable _duplicate_1 = this.support.duplicate(varB);

             _variables_1.add(_duplicate_1);

             VLSImplies _createVLSImplies = this.factory.createVLSImplies();

@@ -206,10 +206,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
               final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> {

                 VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier();

                 final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> {

-                  EList<VLSVariable> _variables_2 = it_4.getVariables();

+                  EList<VLSVariableDeclaration> _variables_2 = it_4.getVariables();

                   VLSVariable _duplicate_2 = this.support.duplicate(varC);

                   _variables_2.add(_duplicate_2);

-                  EList<VLSVariable> _variables_3 = it_4.getVariables();

+                  EList<VLSVariableDeclaration> _variables_3 = it_4.getVariables();

                   VLSVariable _duplicate_3 = this.support.duplicate(varB);

                   _variables_3.add(_duplicate_3);

                   it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB)));

@@ -234,18 +234,13 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
     Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet();

     for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) {

       {

-        VLSFunction _key = e.getKey();

-        String _plus = (_key + "   ");

-        List<VLSFunction> _value = e.getValue();

-        String _plus_1 = (_plus + _value);

-        InputOutput.<String>println(_plus_1);

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

         final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {

           it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString()));

           it.setFofRole("axiom");

           VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

           final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {

-            EList<VLSVariable> _variables = it_1.getVariables();

+            EList<VLSVariableDeclaration> _variables = it_1.getVariables();

             VLSVariable _duplicate = this.support.duplicate(varA);

             _variables.add(_duplicate);

             VLSImplies _createVLSImplies = this.factory.createVLSImplies();

@@ -253,7 +248,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
               it_2.setLeft(this.support.duplicate(e.getKey(), varA));

               VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

               final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> {

-                EList<VLSVariable> _variables_1 = it_3.getVariables();

+                EList<VLSVariableDeclaration> _variables_1 = it_3.getVariables();

                 VLSVariable _duplicate_1 = this.support.duplicate(varB);

                 _variables_1.add(_duplicate_1);

                 int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length;

@@ -313,9 +308,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
           final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_1) -> {

             VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

             final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_2) -> {

-              EList<VLSVariable> _variables = it_2.getVariables();

+              EList<VLSVariableDeclaration> _variables = it_2.getVariables();

               List<VLSVariable> _duplicate = this.support.duplicate(variables);

-              Iterables.<VLSVariable>addAll(_variables, _duplicate);

+              Iterables.<VLSVariableDeclaration>addAll(_variables, _duplicate);

               it_2.setOperand(this.support.unfoldAnd(conjunctionList));

             };

             VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7);

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
index c6565f6a..657c3292 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -9,6 +9,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;

@@ -76,7 +77,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

       final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {

         for (final VLSVariable v : relVar2VLS) {

-          EList<VLSVariable> _variables = it_1.getVariables();

+          EList<VLSVariableDeclaration> _variables = it_1.getVariables();

           VLSVariable _duplicate = this.support.duplicate(v);

           _variables.add(_duplicate);

         }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index c2e4033b..6d4767a7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -13,6 +13,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

 import com.google.common.base.Objects;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;

@@ -244,7 +245,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

       final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {

-        EList<VLSVariable> _variables = it_1.getVariables();

+        EList<VLSVariableDeclaration> _variables = it_1.getVariables();

         VLSVariable _duplicate = this.support.duplicate(this.variable);

         _variables.add(_duplicate);

         VLSImplies _createVLSImplies = this.factory.createVLSImplies();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
index f1d73bec..6cd53fae 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -13,6 +13,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

@@ -323,9 +324,9 @@ public class Logic2VampireLanguageMapper_Support {
       if (isUniversal) {

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

         final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> {

-          EList<VLSVariable> _variables = it.getVariables();

+          EList<VLSVariableDeclaration> _variables = it.getVariables();

           Collection<VLSVariable> _values = variableMap.values();

-          Iterables.<VLSVariable>addAll(_variables, _values);

+          Iterables.<VLSVariableDeclaration>addAll(_variables, _values);

           VLSImplies _createVLSImplies = this.factory.createVLSImplies();

           final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> {

             it_1.setLeft(this.unfoldAnd(typedefs));

@@ -341,9 +342,9 @@ public class Logic2VampireLanguageMapper_Support {
           typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));

           VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

           final Procedure1<VLSExistentialQuantifier> _function_2 = (VLSExistentialQuantifier it) -> {

-            EList<VLSVariable> _variables = it.getVariables();

+            EList<VLSVariableDeclaration> _variables = it.getVariables();

             Collection<VLSVariable> _values = variableMap.values();

-            Iterables.<VLSVariable>addAll(_variables, _values);

+            Iterables.<VLSVariableDeclaration>addAll(_variables, _values);

             it.setOperand(this.unfoldAnd(typedefs));

           };

           _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2);

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
index 73e59774..7921f204 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -15,6 +15,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

@@ -143,7 +144,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
             it.setFofRole("axiom");

             VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

             final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> {

-              EList<VLSVariable> _variables = it_1.getVariables();

+              EList<VLSVariableDeclaration> _variables = it_1.getVariables();

               VLSVariable _duplicate = this.support.duplicate(variable);

               _variables.add(_duplicate);

               VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -193,7 +194,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
                 it.setFofRole("axiom");

                 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

                 final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {

-                  EList<VLSVariable> _variables = it_1.getVariables();

+                  EList<VLSVariableDeclaration> _variables = it_1.getVariables();

                   VLSVariable _duplicate = this.support.duplicate(variable);

                   _variables.add(_duplicate);

                   VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -263,7 +264,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
         it.setFofRole("axiom");

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

         final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {

-          EList<VLSVariable> _variables = it_1.getVariables();

+          EList<VLSVariableDeclaration> _variables = it_1.getVariables();

           VLSVariable _duplicate = this.support.duplicate(variable);

           _variables.add(_duplicate);

           VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -291,7 +292,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
         it.setFofRole("axiom");

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

         final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> {

-          EList<VLSVariable> _variables = it_1.getVariables();

+          EList<VLSVariableDeclaration> _variables = it_1.getVariables();

           VLSVariable _duplicate = this.support.duplicate(variable);

           _variables.add(_duplicate);

           VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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<EObject> callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) {

     try {

-      EList<EObject> _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.<String>newArrayList(("Path=" + PATH)), String.class)));

-        p.waitFor();

-        InputStream _inputStream = p.getInputStream();

-        InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream);

-        final BufferedReader reader = new BufferedReader(_inputStreamReader);

-        final List<String> output = CollectionLiterals.<String>newArrayList();

-        String line = "";

-        while ((!Objects.equal((line = reader.readLine()), null))) {

-          output.add((line + "\n"));

-        }

-        workspace.getFile(TEMPNAME).delete();

-        Map<String, Object> _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap();

-        VampireLanguageFactoryImpl _vampireLanguageFactoryImpl = new VampireLanguageFactoryImpl();

-        _extensionToFactoryMap.put("*", _vampireLanguageFactoryImpl);

-        _xblockexpression = workspace.<VampireModel>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.<String>newArrayList(("Path=" + PATH)), String.class)));

+      p.waitFor();

+      InputStream _inputStream = p.getInputStream();

+      InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream);

+      final BufferedReader reader = new BufferedReader(_inputStreamReader);

+      final List<String> output = CollectionLiterals.<String>newArrayList();

+      String line = "";

+      while ((!Objects.equal((line = reader.readLine()), null))) {

+        output.add((line + "\n"));

       }

-      return _xblockexpression;

+      workspace.getFile(TEMPNAME).delete();

+      final EList<EObject> root = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents();

+      EObject _get = root.get(0);

+      InputOutput.<EList<VLSComment>>println(((VampireModelImpl) _get).getComments());

+      return root;

     } catch (Throwable _e) {

       throw Exceptions.sneakyThrow(_e);

     }