4 files changed, 38 insertions, 33 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 b223dbe5..4e9737cb 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
@@ -8,6 +8,7 @@ class VampireSolverConfiguration extends LogicSolverConfiguration {
         public var boolean uniquenessDuplicates = false
         public var int iteration = -1
         public var BackendSolver solver = BackendSolver::VAMP
+        public var genModel = true
         //choose needed backend solver
 //      public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
 }
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 3281a196..85b81a8c 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
@@ -31,29 +31,32 @@ class VampireSolver extends LogicReasoner {
         val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
         val VampireHandler handler = new VampireHandler
 
-        var fileName = "problem.tptp"
+//      var fileName = "problem.tptp"
 
-        def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) {
-                fileName = location + fileName
-                solve(problem, config, workspace)
-        }
+//      def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) {
+//              fileName = location + fileName
+//              solve(problem, config, workspace)
+//      }
 
         override solve(LogicProblem problem, LogicSolverConfiguration config,
                 ReasonerWorkspace workspace) throws LogicReasonerException {
                 val vampireConfig = config.asConfig
+                var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + vampireConfig.typeScopes.maxNewElements + ".tptp"
 
                 // Start: Logic -> Vampire mapping
                 val transformationStart = System.currentTimeMillis
                 // TODO
                 val result = forwardMapper.transformProblem(problem, vampireConfig)
                 val transformationTime = System.currentTimeMillis - transformationStart
-                
+
                 val vampireProblem = result.output
                 val forwardTrace = result.trace
 
                 var String fileURI = null;
                 var String vampireCode = null;
                 vampireCode = workspace.writeModelToString(vampireProblem, fileName)
+                
+                
 
                 val writeFile = (
                         vampireConfig.documentationLevel === DocumentationLevel::NORMAL ||
@@ -61,35 +64,33 @@ class VampireSolver extends LogicReasoner {
                 if (writeFile) {
                         fileURI = workspace.writeModel(vampireProblem, fileName).toFileString
                 }
-                
-                
-                
+
 //              Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("tptp", new VampireLanguageFactoryImpl)
 ////            val Resource resource = Resource.
 ////            Resource.getResource(wsURI+"problem.tptp") as Resource
 ////            resource
 //              val model = workspace.readModel(VampireModel, "problem.tptp").eResource.contents
 //              println(model)
-                
-
-                // Result as String
-                
                 // Finish: Logic -> Vampire mapping
-                
-                // Start: Solving .tptp problem
-                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)
+                if (vampireConfig.genModel) {
 
-                val backTransformationTime = System.currentTimeMillis - backTransformationStart
-                // Finish: Vampire -> Logic Mapping
-                
+                        // Start: Solving .tptp problem
+                        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
+                        // Finish: Vampire -> Logic Mapping
 //              print(vampSol.generatedModel.tfformulas.size)
-                return logicResult //currently only a ModelResult
+                        return logicResult // currently only a ModelResult
+                }
+                
+                return backwardMapper.transformOutput(problem,
+                                vampireConfig.solutionScope.numberOfRequiredSolution, new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime)
         }
 
         def asConfig(LogicSolverConfiguration configuration) {
@@ -105,9 +106,9 @@ class VampireSolver extends LogicReasoner {
 //       * 
         override getInterpretations(ModelResult modelResult) {
 //               val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
-                val sols = modelResult.representation// as List<A4Solution>
-                //val res = answers.map 
-                sols.map[
+                val sols = modelResult.representation // as List<A4Solution>
+                // val res = answers.map 
+                sols.map [
                         new VampireModelInterpretation(
 //                              forwardMapper.typeMapper.typeInterpreter,
                                 it as VampireModel,
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 df3cfd82..39862c65 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
@@ -25,8 +25,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

         def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config,

                 Logic2VampireLanguageMapperTrace trace) {

-                val ABSOLUTE_MIN = 0

-                val ABSOLUTE_MAX = Integer.MAX_VALUE

+                

 

 //              TODO HANDLE ERRORS RELATED TO MAX > MIN

 //              TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS

@@ -40,6 +39,8 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                 // Number of defined non-abstract elements that are not enum elements

                 // Equals the number of elements in te initial model

                 var elemsInIM = trace.definedElement2String.size

+                val ABSOLUTE_MIN = 0

+                val ABSOLUTE_MAX = -1-elemsInIM

 //              var elemsInIM = 0

 //              

 //              for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) {

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 c1eb3382..47eae807 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
@@ -52,8 +52,10 @@ class VampireHandler {
 

                 val CMD = "cmd /c "

                 val TEMPNAME = "TEMP.tptp"

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

-                        "_" + configuration.iteration + ".tptp"

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

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

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

+                        ".tptp"

                 val PATH = "C:/cygwin64/bin"

 

                 val wsURI = workspace.workspaceURI