VAMPIRE: fix bug in transformation, further implement measurement code

6 files changed, 75 insertions, 46 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 98967181..fc8d3e99 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
@@ -6,6 +6,7 @@ class VampireSolverConfiguration extends LogicSolverConfiguration {
         
         public var int contCycleLevel = 0
         public var boolean uniquenessDuplicates = false
+        public var int iteration = -1
         //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 3b5cec0a..3281a196 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
@@ -46,6 +46,8 @@ class VampireSolver extends LogicReasoner {
                 val transformationStart = System.currentTimeMillis
                 // TODO
                 val result = forwardMapper.transformProblem(problem, vampireConfig)
+                val transformationTime = System.currentTimeMillis - transformationStart
+                
                 val vampireProblem = result.output
                 val forwardTrace = result.trace
 
@@ -71,19 +73,17 @@ class VampireSolver extends LogicReasoner {
                 
 
                 // Result as String
-                val transformationTime = System.currentTimeMillis - transformationStart
+                
                 // Finish: Logic -> Vampire mapping
                 
                 // Start: Solving .tptp problem
-                val solverStart = System.currentTimeMillis
                 val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
-                val solvingTime = System.currentTimeMillis - solverStart
                 // Finish: Solving .tptp problem
                 
                 // Start: Vampire -> Logic mapping
                 val backTransformationStart = System.currentTimeMillis
                 // Backwards Mapper
-                val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,solvingTime)
+                val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime)
 
                 val backTransformationTime = System.currentTimeMillis - backTransformationStart
                 // Finish: Vampire -> Logic Mapping
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index b617912d..60309f2d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -79,14 +79,15 @@ class Logic2VampireLanguageMapper {
                 if (!problem.types.isEmpty) {
                         typeMapper.transformTypes(problem.types, problem.elements, this, trace)
                 }
-                
+
                 // RELATION MAPPER
                 trace.relationDefinitions = problem.collectRelationDefinitions
 //              println(problem.relations.filter[class == RelationDefinitionImpl])
+                toTrace(problem.relations.filter[class == RelationDefinitionImpl], trace)
                 problem.relations.forEach[this.relationMapper.transformRelation(it, trace, new Logic2VampireLanguageMapper)]
-                
+
                 // CONTAINMENT MAPPER
-                containmentMapper.transformContainment(config,problem.containmentHierarchies, trace)
+                containmentMapper.transformContainment(config, problem.containmentHierarchies, trace)
 
                 // SCOPE MAPPER
                 scopeMapper.transformScope(problem.types, config, trace)
@@ -107,6 +108,39 @@ class Logic2VampireLanguageMapper {
                 return new TracedOutput(specification, trace)
         }
 
+        def toTrace(Iterable<Relation> relations, Logic2VampireLanguageMapperTrace trace) {
+                val List<VLSVariable> vars = newArrayList
+                for (rel : relations) {
+                        //decide name
+                        val nameArray = rel.name.split(" ")
+                        var relNameVar = ""
+                        if (nameArray.length == 3) {
+                                relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
+                        } else {
+                                relNameVar = rel.name
+                        }
+                        val relName = relNameVar
+                        
+                        val relDef = rel as RelationDefinition
+                        for (i : 0 ..< rel.parameters.length) {
+
+                                val v = createVLSVariable => [
+                                        it.name = support.toIDMultiple("V", i.toString)
+                                ]
+                                vars.add(v)
+                        }
+
+                        val relFunc = createVLSFunction => [
+                                it.constant = support.toIDMultiple("r", relName)
+                                for (v : vars) {
+                                        it.terms += support.duplicate(v)
+                                }
+                        ]
+                        trace.relDef2Predicate.put(relDef, relFunc)
+                        trace.predicate2RelDef.put(relFunc, relDef)
+                }
+        }
+
         // End of transformProblem
         // ////////////
         // Type References
@@ -169,7 +203,6 @@ class Logic2VampireLanguageMapper {
 //              Map<Variable, VLSVariable> variables) {
 //              createVLSReal => [it.value = literal.value.toString()]
 //      }
-
         def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
                 createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)]
@@ -265,10 +298,10 @@ class Logic2VampireLanguageMapper {
         def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,
                 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
-                        val name = referred.lookup(trace.definedElement2String)
-                        return createVLSConstant => [
-                                it.name = name
-                        ]
+                val name = referred.lookup(trace.definedElement2String)
+                return createVLSConstant => [
+                        it.name = name
+                ]
 //              typeMapper.transformReference(referred, trace)
         }
 
@@ -390,12 +423,11 @@ class Logic2VampireLanguageMapper {
 //              }
                 return createVLSFunction => [
                         if (relation.class == RelationDeclarationImpl) {
-                                                        it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
-                        }
-                        else {
+                                it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
+                        } else {
                                 it.constant = (relation as RelationDefinition).lookup(trace.relDef2Predicate).constant
                         }
-                        
+
                         it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
                 ]
         }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index 181c59ca..efedf6dc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -23,7 +23,8 @@ class Logic2VampireLanguageMapper_RelationMapper {
                 this.base = base
         }
 
-        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) {
+        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace,
+                Logic2VampireLanguageMapper mapper) {
 
                 // 1. store all variables in support wrt their name
                 // 1.1 if variable has type, creating list of type declarations
@@ -42,19 +43,18 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
                 }
 
-                //deciding name of relation
+                // deciding name of relation
                 val nameArray = r.name.split(" ")
                 var relNameVar = ""
                 if (nameArray.length == 3) {
                         relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
-                }
-                else {
+                } else {
                         relNameVar = r.name
                 }
                 val relName = relNameVar
-                
-                val comply = createVLSFofFormula=> [
-                        
+
+                val comply = createVLSFofFormula => [
+
                         it.name = support.toIDMultiple("compliance", relName)
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
@@ -79,10 +79,10 @@ class Logic2VampireLanguageMapper_RelationMapper {
                 trace.specification.formulas += comply
         }
 
-        def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) {
-                
-//              println("XXXXXXXXXXXXXXXXX")
+        def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace,
+                Logic2VampireLanguageMapper mapper) {
 
+//              println("XXXXXXXXXXXXXXXXX")
 // 1. store all variables in support wrt their name
                 // 1.1 if variable has type, creating list of type declarations
                 val Map<Variable, VLSVariable> relVar2VLS = new HashMap
@@ -102,34 +102,30 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
                 }
 
-                //deciding name of relation
+                // deciding name of relation
                 val nameArray = r.name.split(" ")
                 var relNameVar = ""
                 if (nameArray.length == 3) {
                         relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
-                }
-                else {
+                } else {
                         relNameVar = r.name
                 }
                 val relName = relNameVar
-                
-                //define logic for pattern
+
+                // define logic for pattern
 //              val map = new HashMap
 //              map.put(r.variables.get(0), createVLSVariable)
                 val definition = mapper.transformTerm(r.value, trace, relVar2VLS)
-                
-                
-                
-                
-                //get entire contents of and
+
+                // get entire contents of and
                 val compliance = support.unfoldAnd(relVar2TypeDecComply)
-                val compDefn = createVLSAnd=> [
+                val compDefn = createVLSAnd => [
                         it.left = compliance
                         it.right = definition
                 ]
-                
-                val relDef = createVLSFofFormula=> [
-                        
+
+                val relDef = createVLSFofFormula => [
+
                         it.name = support.toID(relName)
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
@@ -143,14 +139,13 @@ class Logic2VampireLanguageMapper_RelationMapper {
                                                         it.terms += support.duplicate(v)
                                                 }
                                         ]
-                                        trace.relDef2Predicate.put(r, rel)
-                                        trace.predicate2RelDef.put(rel, r)
+//                                      trace.relDef2Predicate.put(r, rel)
+//                                      trace.predicate2RelDef.put(rel, r)
                                         it.left = support.duplicate(rel)
                                         it.right = compDefn
                                 ]
                         ]
                 ]
-
                 trace.specification.formulas += relDef
 
         }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
index 489bf423..e136d1c6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
@@ -8,7 +8,7 @@ class Vampire2LogicMapper {
 

 //      

         public def transformOutput(LogicProblem problem, int requiredNumberOfSolution,

-                MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace,

+                MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace, 

                 long transformationTime) {

 

                 // ModelRsult implements LogicResult

@@ -22,7 +22,8 @@ class Vampire2LogicMapper {
 

         def transformStatistics(MonitoredVampireSolution solution, long transformationTime) {

                 return createStatistics => [

-                        it.transformationTime = solution.solverTime as int

+                        it.solverTime = solution.solverTime as int

+                        it.transformationTime = transformationTime as int

                 ]

 //              createStatistics => [

 //                      it.transformationTime = transformationTime as int

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 74532ee5..c5cfb1c7 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
@@ -44,7 +44,7 @@ class VampireHandler {
                 val VAMPNAME = "vampire.exe"

                 val TEMPNAME = "TEMP.tptp"

                 val OPTION = " --mode casc_sat -t 300 "

-                val SOLNNAME = "_solution" + configuration.typeScopes.maxNewElements + ".tptp"

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

                 val PATH = "C:/cygwin64/bin"

 

                 val wsURI = workspace.workspaceURI