From f63a94c06268b5233264436cc538062f1f7b01bc Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 8 Oct 2019 03:00:08 -0400 Subject: VAMPIRE: fix bug in transformation, further implement measurement code --- .../reasoner/VampireAnalyzerConfiguration.xtend | 1 + .../vampire/reasoner/VampireSolver.xtend | 8 ++-- .../builder/Logic2VampireLanguageMapper.xtend | 56 +++++++++++++++++----- ...ogic2VampireLanguageMapper_RelationMapper.xtend | 49 +++++++++---------- .../reasoner/builder/Vampire2LogicMapper.xtend | 5 +- .../vampire/reasoner/builder/VampireHandler.xtend | 2 +- 6 files changed, 75 insertions(+), 46 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner') 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 relations, Logic2VampireLanguageMapperTrace trace) { + val List 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 variables) { // createVLSReal => [it.value = literal.value.toString()] // } - def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace, Map variables) { createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)] @@ -265,10 +298,10 @@ class Logic2VampireLanguageMapper { def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, Map 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 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 -- cgit v1.2.3-54-g00ecf