VAMPIRE: post-submission push

2 files changed, 25 insertions, 13 deletions

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>