mid-measurement push

3 files changed, 48 insertions, 8 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
index 4c2f1952..1fda24d9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
@@ -24,7 +24,8 @@ enum BackendSolver {
         IPROVER,
         PARADOX,
         VAMPIRE,
-        Z3
+        Z3,
+        LOCVAMP
         //add needed things
 }
 
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 9ec08163..042caa86 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
@@ -20,6 +20,7 @@ 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.workspace.ReasonerWorkspace
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl
 
 class VampireSolver extends LogicReasoner {
 
@@ -128,17 +129,17 @@ class VampireSolver extends LogicReasoner {
                                                         it.name = "satOut"
                                                         it.value = satOut
                                                 ]
-                                                it.entries += createRealStatisticEntry => [
+                                                it.entries += createStringStatisticEntry => [
                                                         it.name = "satTime"
-                                                        it.value = Double.parseDouble(satTime)
+                                                        it.value = satTime
                                                 ]
                                                 it.entries += createStringStatisticEntry => [
                                                         it.name = "modOut"
                                                         it.value = modOut
                                                 ]
-                                                it.entries += createRealStatisticEntry => [
+                                                it.entries += createStringStatisticEntry => [
                                                         it.name = "modTime"
-                                                        it.value = Double.parseDouble(modTime)
+                                                        it.value = modTime
                                                 ]
 
                                         ]
@@ -148,6 +149,7 @@ class VampireSolver extends LogicReasoner {
                         } else {
 
                                 // Start: Solving .tptp problem
+                                println()
                                 val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
                                 // Finish: Solving .tptp problem
                                 // Start: Vampire -> Logic mapping
@@ -159,7 +161,44 @@ class VampireSolver extends LogicReasoner {
                                 val backTransformationTime = System.currentTimeMillis - backTransformationStart
                                 // Finish: Vampire -> Logic Mapping
 //              print(vampSol.generatedModel.tfformulas.size)
-                                return logicResult // currently only a ModelResult
+
+//                              return logicResult // currently only a ModelResult
+
+                                var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl]
+//                              
+                                var modOut = "no"
+                                if(model.length >0){
+                                        modOut = "FiniteModel"
+                                }
+                                
+                                val realModOut=modOut
+ 
+                                
+                                return createModelResult => [
+                                        it.problem = null
+                                        it.representation += createVampireModel => []
+                                        it.trace = trace
+                                        it.statistics = createStatistics => [
+                                                it.transformationTime = transformationTime as int
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "satOut"
+                                                        it.value = "-"
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "satTime"
+                                                        it.value = "-"
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "modOut"
+                                                        it.value = realModOut
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "modTime"
+                                                        it.value = (vampSol.solverTime/1000.0).toString
+                                                ]
+
+                                        ]
+                                ]
                         }
                 }
                 return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution,
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 6d301442..c277759a 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
@@ -54,7 +54,7 @@ class VampireHandler {
                 val TEMPNAME = "TEMP.tptp"

 //              val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements +

 //                      "_" + configuration.iteration + ".tptp"

-                val SOLNNAME = "solution" + "_" + configuration.typeScopes.maxNewElements + "_" + configuration.iteration +

+                val SOLNNAME = "solution" + "_" + configuration.typeScopes.minNewElements + "_" + configuration.iteration +

                         ".tptp"

                 val PATH = "C:/cygwin64/bin"

 

@@ -70,7 +70,7 @@ class VampireHandler {
                 var long startTime = -1 as long

                 var long solverTime = -1 as long

                 var Process p = null

-                if (configuration.solver == BackendSolver::VAMPIRE) {

+                if (configuration.solver == BackendSolver::LOCVAMP) {

 

                         var OPTION = " --mode casc_sat "

                         if (configuration.runtimeLimit != -1) {