VAMPIRE: setup structure of model interpretation

47 files changed, 170 insertions, 114 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
index 5c47bacb..79296fd6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
index 656a2110..7781bf9d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
index 854cd91f..4d13e9b6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
index 3640f798..c07947c9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
index 310033e1..12c73d57 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
index ede1ce7d..656552a6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
index 78fbafbe..cdb80449 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
index df5e592d..b8138e88 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
index f40814b0..23feccda 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
index 9a9d2465..7fb53220 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
index ce4138d1..64554698 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
index 42ffb9cd..7a8125bb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
index db0f9d01..2f49f152 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
index b8872cf8..f762dd38 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
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 1fd40801..0ec4d0da 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
@@ -3,11 +3,12 @@ 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.Logic2VampireLanguageMapperTrace
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation
 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
@@ -15,7 +16,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 org.eclipse.emf.ecore.resource.Resource
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
 
 class VampireSolver extends LogicReasoner {
 
@@ -71,21 +72,21 @@ class VampireSolver extends LogicReasoner {
                 // Result as String
                 val transformationTime = System.currentTimeMillis - transformationStart
                 // Finish: Logic -> Vampire mapping
+                
                 // Start: Solving .tptp problem
                 val solverStart = System.currentTimeMillis
-                // Calling Solver (Currently Manually)
-                val result2 = handler.callSolver(vampireProblem, workspace, vampireConfig)
-                // val result2 = null
+                val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
                 val solvingTime = System.currentTimeMillis - solverStart
-                // TODO
-//              val backTransformationStart = System.currentTimeMillis
-//              // Backwards Mapper
-//              val logicResult = backwardMapper.transformOutput(problem, config.solutionScope.numberOfRequiredSolution,
-//                      result2, forwardTrace, transformationTime)
-//
-//              val backTransformationTime = System.currentTimeMillis - backTransformationStart
-                // Finish: Solving Alloy problem
-                return null
+                // Finish: Solving .tptp problem
+                
+                // Start: Vampire -> Logic mapping
+                val backTransformationStart = System.currentTimeMillis
+                // Backwards Mapper
+                val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime)
+
+                val backTransformationTime = System.currentTimeMillis - backTransformationStart
+                // Finish: Vampire -> Logic Mapping
+                return logicResult //currently only a ModelResult
         }
 
         def asConfig(LogicSolverConfiguration configuration) {
@@ -100,17 +101,17 @@ class VampireSolver extends LogicReasoner {
 //       * not for now
 //       * 
         override getInterpretations(ModelResult modelResult) {
-                // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
-//              val sols = modelResult.representation// as List<A4Solution>
-//              //val res = answers.map 
-//              sols.map[
-//                      new VampireModelInterpretation(
+//               val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
+                val sols = modelResult.representation// as List<A4Solution>
+                //val res = answers.map 
+                sols.map[
+                        new VampireModelInterpretation(
 //                              forwardMapper.typeMapper.typeInterpreter,
-//                              it as A4Solution,
+                                it as VampireModel,
 //                              forwardMapper,
-//                              modelResult.trace as Logic2AlloyLanguageMapperTrace
-//                      )
-//              ]
+                                modelResult.trace as Logic2VampireLanguageMapperTrace
+                        )
+                ]
         }
 //      */
 }
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
index 9c9e65b4..a0084204 100644
--- 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
@@ -4,39 +4,24 @@ 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)

-//                              ]

-//                      }

-//              }

-//      }

+        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE

+

 //      

-//      def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {

+        public def transformOutput(LogicProblem problem, int requiredNumberOfSolution,

+                MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace,

+                long transformationTime) {

+

+                // ModelRsult implements LogicResult

+                return createModelResult => [

+                        it.problem = problem

+                        it.representation += monitoredVampireSolution.generatedModel

+                        it.trace = trace

+                        it.statistics = transformStatistics(monitoredVampireSolution, transformationTime)

+                ]

+        }

+

+        def transformStatistics(MonitoredVampireSolution solution, long transformationTime) {

+                return createStatistics

 //              createStatistics => [

 //                      it.transformationTime = transformationTime as int

 //                      for(solutionIndex : 0..<solution.aswers.size) {

@@ -59,9 +44,6 @@ class Vampire2LogicMapper {
 //                              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
index f0426245..ce672211 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
@@ -25,11 +25,12 @@ class VampireSolverException extends Exception {
         }

 }

 

-@Data class VampireSolutionModel {

+@Data class MonitoredVampireSolution {

 //      List<String> warnings

 //      List<String> debugs

 //      long kodkodTime

 //      val List<Pair<A4Solution, Long>> aswers

+        val VampireModel generatedModel

 //      val boolean finishedBeforeTimeout

 }

 

@@ -76,12 +77,10 @@ class VampireHandler {
                 // 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

-                

-

 

-                println((root.get(0) as VampireModelImpl ).comments)

+//              println((root.get(0) as VampireModel ).comments)

                 

-                return root

+                return new MonitoredVampireSolution(root.get(0) as VampireModel)

 

         /*

          * //Prepare

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend
new file mode 100644
index 00000000..c2cffa6b
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend
@@ -0,0 +1,49 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+
+class VampireModelInterpretation implements LogicModelInterpretation {
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        
+        protected val Logic2VampireLanguageMapperTrace forwardTrace;
+        
+        
+        public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) {
+                this.forwardTrace = trace
+        }
+        
+        override getElements(Type type) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getInterpretation(ConstantDeclaration constant) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getAllIntegersInStructure() {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getAllRealsInStructure() {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getAllStringsInStructure() {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+}
\ No newline at end of file
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index b9600616..499504af 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
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 43992ea0..298a6c08 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/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
index 410b47ed..a7780e97 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
@@ -5,8 +5,10 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation;

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

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

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;

@@ -21,9 +23,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;

 import java.util.List;

 import org.eclipse.emf.common.util.EList;

-import org.eclipse.emf.ecore.EObject;

 import org.eclipse.xtend2.lib.StringConcatenation;

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

+import org.eclipse.xtext.xbase.lib.Functions.Function1;

+import org.eclipse.xtext.xbase.lib.ListExtensions;

 

 @SuppressWarnings("all")

 public class VampireSolver extends LogicReasoner {

@@ -72,10 +75,14 @@ public class VampireSolver extends LogicReasoner {
     long _currentTimeMillis = System.currentTimeMillis();

     final long transformationTime = (_currentTimeMillis - transformationStart);

     final long solverStart = System.currentTimeMillis();

-    final EList<EObject> result2 = this.handler.callSolver(vampireProblem, workspace, vampireConfig);

+    final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);

     long _currentTimeMillis_1 = System.currentTimeMillis();

     final long solvingTime = (_currentTimeMillis_1 - solverStart);

-    return null;

+    final long backTransformationStart = System.currentTimeMillis();

+    final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime);

+    long _currentTimeMillis_2 = System.currentTimeMillis();

+    final long backTransformationTime = (_currentTimeMillis_2 - backTransformationStart);

+    return logicResult;

   }

   

   public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) {

@@ -93,6 +100,17 @@ public class VampireSolver extends LogicReasoner {
   

   @Override

   public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) {

-    return null;

+    List<VampireModelInterpretation> _xblockexpression = null;

+    {

+      final EList<Object> sols = modelResult.getRepresentation();

+      final Function1<Object, VampireModelInterpretation> _function = (Object it) -> {

+        Object _trace = modelResult.getTrace();

+        return new VampireModelInterpretation(

+          ((VampireModel) it), 

+          ((Logic2VampireLanguageMapperTrace) _trace));

+      };

+      _xblockexpression = ListExtensions.<Object, VampireModelInterpretation>map(sols, _function);

+    }

+    return _xblockexpression;

   }

 }

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 19608361..863b572e 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 791a9524..410f2550 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 89003c27..b1b39a4f 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 b37d993a..3710e753 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 45afcecc..9dc7abaf 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 0f4dc63a..7029d196 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 ab58fcab..03aead59 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 cf19663e..62960704 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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index f8b35528..56a10b3c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.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 0b2cb192..319f863c 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/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
index ffd37ea3..3b6009bb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
index 9ddc7bd0..d8329084 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
index f4b5a1d2..29a2ecea 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
@@ -1,5 +1,36 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;

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

+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics;

+import org.eclipse.emf.common.util.EList;

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

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

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

+

 @SuppressWarnings("all")

 public class Vampire2LogicMapper {

+  @Extension

+  private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;

+  

+  public ModelResult transformOutput(final LogicProblem problem, final int requiredNumberOfSolution, final MonitoredVampireSolution monitoredVampireSolution, final Logic2VampireLanguageMapperTrace trace, final long transformationTime) {

+    ModelResult _createModelResult = this.resultFactory.createModelResult();

+    final Procedure1<ModelResult> _function = (ModelResult it) -> {

+      it.setProblem(problem);

+      EList<Object> _representation = it.getRepresentation();

+      VampireModel _generatedModel = monitoredVampireSolution.getGeneratedModel();

+      _representation.add(_generatedModel);

+      it.setTrace(trace);

+      it.setStatistics(this.transformStatistics(monitoredVampireSolution, transformationTime));

+    };

+    return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function);

+  }

+  

+  public Statistics transformStatistics(final MonitoredVampireSolution solution, final long transformationTime) {

+    return this.resultFactory.createStatistics();

+  }

 }

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 7f6ce1c6..4764ae28 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,9 +1,8 @@
 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.vampire.reasoner.builder.MonitoredVampireSolution;

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

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

@@ -16,11 +15,10 @@ import org.eclipse.emf.ecore.EObject;
 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) {

+  public MonitoredVampireSolution callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) {

     try {

       final String CMD = "cmd /c ";

       final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\";

@@ -48,8 +46,7 @@ public class VampireHandler {
       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;

+      return new MonitoredVampireSolution(((VampireModel) _get));

     } catch (Throwable _e) {

       throw Exceptions.sneakyThrow(_e);

     }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
deleted file mode 100644
index 3c43c4ea..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
+++ /dev/null
@@ -1,34 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

-

-import org.eclipse.xtend.lib.annotations.Data;

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

-import org.eclipse.xtext.xbase.lib.util.ToStringBuilder;

-

-@Data

-@SuppressWarnings("all")

-public class VampireSolutionModel {

-  @Override

-  @Pure

-  public int hashCode() {

-    return 1;

-  }

-  

-  @Override

-  @Pure

-  public boolean equals(final Object obj) {

-    if (this == obj)

-      return true;

-    if (obj == null)

-      return false;

-    if (getClass() != obj.getClass())

-      return false;

-    return true;

-  }

-  

-  @Override

-  @Pure

-  public String toString() {

-    ToStringBuilder b = new ToStringBuilder(this);

-    return b.toString();

-  }

-}

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
index 4f0bbdb1..dcbb21eb 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
@@ -560,7 +560,7 @@
   <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/>

   <elements name="Leaf literal FunctionType" definedInType="//@types.9"/>

   <elements name="o 1" definedInType="//@types.10"/>

-  <containmentHierarchies typesOrderedInHierarchy="//@types.1 //@types.5 //@types.6 //@types.3 //@types.8 //@types.7 //@types.0 //@types.2 //@types.4 //@types.10 //@types.11" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/>

+  <containmentHierarchies typesOrderedInHierarchy="//@types.5 //@types.4 //@types.3 //@types.6 //@types.7 //@types.8 //@types.1 //@types.0 //@types.2 //@types.10 //@types.11" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/>

   <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/>

   <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/>

   <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/>

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
index 4625bfbf..0c59b077 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
@@ -3,25 +3,27 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration

 import functionalarchitecture.Function

+import functionalarchitecture.FunctionalArchitectureModel

 import functionalarchitecture.FunctionalInterface

 import functionalarchitecture.FunctionalOutput

 import functionalarchitecture.FunctionalarchitecturePackage

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration

 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.logicresult.LogicResult

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult

+import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic

 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace

 import java.util.HashMap

 import org.eclipse.emf.ecore.resource.Resource

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl

-import functionalarchitecture.FunctionalArchitectureModel

 

 class FAMTest {

         def static void main(String[] args) {

                 val Ecore2Logic ecore2Logic = new Ecore2Logic

+                        val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)

                 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)

                 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic

 

@@ -93,6 +95,15 @@ class FAMTest {
                 ]

 

                 var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace)

+                

+                //visualisation, see 

+//              var interpretations = reasoner.getInterpretations(solution as ModelResult)

+//              

+//              for(interpretation : interpretations) {

+//                      val model = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace)

+//                      //look here: hu.bme.mit.inf.dslreasoner.application.execution.GenerationTaskExecutor

+//              }

+                //transform interpretation to ecore, and it is easy from there

 

                 /*/

                  * 

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
index 1bf1d5cb..9033512f 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
index f921c3b0..292bf88e 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
index 8da3064a..eb8d5506 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
index 241e8efd..1023ad44 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
index e6e6bbf4..c996fa4f 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
index ac49a9aa..aca97399 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
@@ -16,6 +16,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;

+import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic;

 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;

@@ -36,6 +37,7 @@ public class FAMTest {
   public static void main(final String[] args) {

     try {

       final Ecore2Logic ecore2Logic = new Ecore2Logic();

+      final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic);

       final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);

       final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();

       StringConcatenation _builder = new StringConcatenation();

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
index 8982a98b..796f7103 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
index 0d4e05e0..a2cecacf 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
index eb5c369d..c1a25e40 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin