VAMPIRE: post-submission push

3 files changed, 35 insertions, 23 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 042caa86..59084843 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
@@ -153,21 +153,21 @@ class VampireSolver extends LogicReasoner {
                                 val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
                                 // 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
+//                              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
 //              print(vampSol.generatedModel.tfformulas.size)
 
 //                              return logicResult // currently only a ModelResult
 
-                                var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl]
+//                              var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl]
 //                              
                                 var modOut = "no"
-                                if(model.length >0){
+                                if(vampSol.finiteModelGenerated){
                                         modOut = "FiniteModel"
                                 }
                                 
@@ -201,8 +201,8 @@ class VampireSolver extends LogicReasoner {
                                 ]
                         }
                 }
-                return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution,
-                        new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime)
+//              return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution,
+//                      new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime)
         }
 
         def asConfig(LogicSolverConfiguration configuration) {
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
index a9516cc4..96c2da48 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -56,11 +56,11 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

                 val localInstances = newArrayList

 

-                val consistant = GLOBAL_MAX > GLOBAL_MIN

+                val consistant = GLOBAL_MAX >= GLOBAL_MIN

 

                 // Handling Minimum_General

                 if (GLOBAL_MIN != ABSOLUTE_MIN) {

-                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant)//may make not consistent here 

+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant)//may make not consistent here 

                         if (consistant) {

                                 for (i : trace.uniqueInstances) {

                                         localInstances.add(support.duplicate(i))

@@ -73,7 +73,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

                 // Handling Maximum_General

                 if (GLOBAL_MAX != ABSOLUTE_MAX) {

-                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, !consistant)

+                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant)

                         if (consistant) {

                                 makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)

                         } else {

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 c277759a..d7dd53f0 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
@@ -11,6 +11,7 @@ import org.eclipse.xtend.lib.annotations.Data
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl

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

+import java.io.FileReader

 

 class VampireSolverException extends Exception {

         new(String s) {

@@ -33,6 +34,7 @@ class VampireSolverException extends Exception {
 //      val List<Pair<A4Solution, Long>> aswers

         val VampireModel generatedModel

 //      val boolean finishedBeforeTimeout

+        val boolean finiteModelGenerated

 }

 

 class VampireHandler {

@@ -92,28 +94,38 @@ class VampireHandler {
                         p.waitFor

                         solverTime = System.currentTimeMillis - startTime

                 }

+                

 

                 // 2.1 determine time left

                 // 2.2 store output into local variable

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

+                val BufferedReader reader = new BufferedReader(new FileReader(solnLoc));

                 val List<String> output = newArrayList

 

                 var line = "";

                 while ((line = reader.readLine()) != null) {

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

+                        if (line == "Finite Model Found!") {

+                                return new MonitoredVampireSolution(solverTime, null, true)

+                        }

                 }

+                return new MonitoredVampireSolution(solverTime, null, false)

 

-//      println(output.toString())

-                // 4. delete temp file

-                workspace.getFile(TEMPNAME).delete

+        /*              var line = "";

+         *              while ((line = reader.readLine()) != null) {

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

+         *              }

 

-                // 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(output.toString())

+         *              // 4. delete temp file

+         *              workspace.getFile(TEMPNAME).delete

 

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

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

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

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

+         * 

+         */

         /*

          * //Prepare

          * val warnings = new LinkedList<String>