4 files changed, 30 insertions, 19 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 0ec4d0da..3b5cec0a 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
@@ -9,6 +9,8 @@ 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.VLSFiniteModelImpl
 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
@@ -16,7 +18,6 @@ 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.vampireLanguage.VampireModel
 
 class VampireSolver extends LogicReasoner {
 
@@ -82,10 +83,12 @@ class VampireSolver extends LogicReasoner {
                 // Start: Vampire -> Logic mapping
                 val backTransformationStart = System.currentTimeMillis
                 // Backwards Mapper
-                val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime)
+                val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,solvingTime)
 
                 val backTransformationTime = System.currentTimeMillis - backTransformationStart
                 // Finish: Vampire -> Logic Mapping
+                
+//              print(vampSol.generatedModel.tfformulas.size)
                 return logicResult //currently only a ModelResult
         }
 
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 a0084204..489bf423 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
@@ -21,7 +21,9 @@ class Vampire2LogicMapper {
         }

 

         def transformStatistics(MonitoredVampireSolution solution, long transformationTime) {

-                return createStatistics

+                return createStatistics => [

+                        it.transformationTime = solution.solverTime as int

+                ]

 //              createStatistics => [

 //                      it.transformationTime = transformationTime as int

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

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 ce672211..74532ee5 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
@@ -28,7 +28,7 @@ class VampireSolverException extends Exception {
 @Data class MonitoredVampireSolution {

 //      List<String> warnings

 //      List<String> debugs

-//      long kodkodTime

+        long solverTime

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

         val VampireModel generatedModel

 //      val boolean finishedBeforeTimeout

@@ -43,8 +43,8 @@ class VampireHandler {
                 val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"

                 val VAMPNAME = "vampire.exe"

                 val TEMPNAME = "TEMP.tptp"

-                val OPTION = " --mode casc_sat "

-                val SOLNNAME = "solution.tptp"

+                val OPTION = " --mode casc_sat -t 300 "

+                val SOLNNAME = "_solution" + configuration.typeScopes.maxNewElements + ".tptp"

                 val PATH = "C:/cygwin64/bin"

 

                 val wsURI = workspace.workspaceURI

@@ -57,9 +57,11 @@ class VampireHandler {
 

                 // 2. run command and save to 

                 // need to have cygwin downloaded

+                var startTime = System.currentTimeMillis

                 val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH))

                 // 2.1 determine time left

                 p.waitFor

+                val solverTime = System.currentTimeMillis - startTime

 

                 // 2.2 store output into local variable

                 val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream()));

@@ -80,7 +82,7 @@ class VampireHandler {
 

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

                 

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

+                return new MonitoredVampireSolution(solverTime, 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
index 9eb47f41..063dcf2a 100644
--- 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
@@ -33,6 +33,7 @@ import java.util.Map
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
 import java.util.concurrent.TimeUnit
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTermImpl
 
 class VampireModelInterpretation implements LogicModelInterpretation {
         protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
@@ -79,10 +80,10 @@ class VampireModelInterpretation implements LogicModelInterpretation {
 //              println()
 //              println(trace.type2Predicate)
                 // Fill keys of map
-                println(trace.type2Predicate.keySet)
+//              println(trace.type2Predicate.keySet)
                 val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl]
                 val allTypeFunctions = trace.predicate2Type
-                println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl])
+//              println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl])
 
                 for (type : allTypeDecls) {
                         type2DefinedElement.put(type as TypeDeclaration, newArrayList)
@@ -97,7 +98,7 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                 for (formula : typeFormulas) {
                         // get associated type
                         val associatedTypeName = (formula as VLSTffFormula).name.substring(10)
-                        print(associatedTypeName)
+//                      print(associatedTypeName)
                         val associatedFunctions = allTypeFunctions.keySet.filter[constant == associatedTypeName]
                         if (associatedFunctions.length > 0) {
                                 val associatedFunction = associatedFunctions.get(0) as VLSFunction
@@ -132,7 +133,7 @@ class VampireModelInterpretation implements LogicModelInterpretation {
 
                 }
 
-                printMap()
+//              printMap()
 
                 // 3. get relations
                 // Fill keys of map
@@ -153,6 +154,7 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                 val relFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_r_"]
 
                 for (formula : relFormulas) {
+//                      println(formula)
                         // get associated type
                         val associatedRelName = (formula as VLSTffFormula).name.substring(10)
 
@@ -169,7 +171,7 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                                 end = false
                                 val List<String[]> instances = newArrayList
                                 while (!end) {
-                                        if (andFormulaTerm.class == VLSAndImpl) {
+                                        if (andFormulaTerm.class != null && andFormulaTerm.class == VLSAndImpl) {
                                                 val andFormula = andFormulaTerm as VLSAnd
                                                 val andRight = andFormula.right
                                                 addRelIfNotNeg(andRight, instances)
@@ -202,6 +204,7 @@ class VampireModelInterpretation implements LogicModelInterpretation {
 
                 }
                 println()
+                println("--------END ELEMENTS MAP----------")
         }
 
         def printMap2() {
@@ -226,7 +229,8 @@ class VampireModelInterpretation implements LogicModelInterpretation {
         }
 
         def private addRelIfNotNeg(VLSTerm term, List<String[]> list) {
-                if (term.class != VLSUnaryNegationImpl) {
+//              println("xxx   " + term.class)
+                if (term.class != VLSUnaryNegationImpl && term.class != VLSTermImpl) {
                         val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor
                         val nodeName2 = ((term as VLSFunction).terms.get(1) as VLSFunctionAsTerm).functor
                         val strArr = newArrayList(nodeName1, nodeName2)
@@ -247,9 +251,9 @@ class VampireModelInterpretation implements LogicModelInterpretation {
         }
 
         def private dispatch getElementsDispatch(TypeDefinition declaration) {
-                println("~~" + declaration)
-                println(declaration.elements)
-                println()
+//              println("~~" + declaration)
+//              println(declaration.elements)
+//              println()
                 return declaration.elements
         }
 
@@ -258,18 +262,18 @@ class VampireModelInterpretation implements LogicModelInterpretation {
         }
 
         override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
-                print("-- " + relation.name)
+//              print("-- " + relation.name)
                 val node1 = (parameterSubstitution.get(0) as DefinedElement).name
                 val node2 = (parameterSubstitution.get(1) as DefinedElement).name
                 val realRelations = relation.lookup(relDec2Inst)
                 for (real : realRelations) {
                         if (real.contains(node1) && real.contains(node2)) {
-                                println("  true")
+//                              println("  true")
                                 TimeUnit.MILLISECONDS.sleep(10)
                                 return true
                         }
                 }
-                println("  false")
+//              println("  false")
                 TimeUnit.MILLISECONDS.sleep(10)
                 return false
         }