From 7379cc66fc3cc3b635df45072afc3dec42997c76 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 21 Oct 2019 17:14:25 -0400 Subject: mid-measurement push --- .../reasoner/VampireAnalyzerConfiguration.xtend | 3 +- .../vampire/reasoner/VampireSolver.xtend | 49 +++++++++++++++++++--- .../vampire/reasoner/builder/VampireHandler.xtend | 4 +- 3 files changed, 48 insertions(+), 8 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire') 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) { -- cgit v1.2.3-54-g00ecf