VAMPIRE: setup structure of model interpretation

4 files changed, 98 insertions, 67 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 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