From f87b4233437f0900c19f462b5e443a3c81b27b6e Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 15 Jan 2019 12:44:33 -0500 Subject: Initial workspace setup --- .../reasoner/VampireAnalyzerConfiguration.xtend | 22 ++ .../vampire/reasoner/VampireSolver.xtend | 102 ++++++ .../builder/Logic2VampireLanguageMapper.xtend | 386 +++++++++++++++++++++ .../builder/Logic2VampireLanguageMapperTrace.xtend | 39 +++ ...ogic2VampireLanguageMapper_ConstantMapper.xtend | 42 +++ ...ogic2VampireLanguageMapper_RelationMapper.xtend | 183 ++++++++++ .../Logic2VampireLanguageMapper_Support.xtend | 148 ++++++++ .../Logic2VampireLanguageMapper_TypeMapper.xtend | 19 + ...guageMapper_TypeMapperTrace_FilteredTypes.xtend | 21 ++ ...reLanguageMapper_TypeMapper_FilteredTypes.xtend | 158 +++++++++ ...ireModelInterpretation_TypeInterpretation.xtend | 5 + ...retation_TypeInterpretation_FilteredTypes.xtend | 5 + 12 files changed, 1130 insertions(+) create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill') 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 new file mode 100644 index 00000000..27e00ccf --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend @@ -0,0 +1,22 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration + +class VampireSolverConfiguration extends LogicSolverConfiguration { + + public var int symmetry = 0 // by default + //choose needed backend solver +// public var VampireBackendSolver solver = VampireBackendSolver.SAT4J + public var boolean writeToFile = false +} + + +enum VampireBackendSolver { + //add needed things +} + + +enum TypeMappingTechnique { + //default + FilteredTypes +} \ No newline at end of file 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 new file mode 100644 index 00000000..64484b88 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend @@ -0,0 +1,102 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner + +import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.io.PrintWriter +import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes + +class VampireSolver extends LogicReasoner{ + + new() { + VampireLanguagePackage.eINSTANCE.eClass + val x = new VampireLanguageStandaloneSetupGenerated + VampireLanguageStandaloneSetup::doSetup() + } + + val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) +// //not for now +// val VampireHandler handler = new VampireHandler +// val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper + + val fileName = "problem.tptp" + + override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { + val vampireConfig = configuration.asConfig + + // Start: Logic -> Vampire mapping + val transformationStart = System.currentTimeMillis + //TODO + val result = forwardMapper.transformProblem(problem,vampireConfig) + val vampireProblem = result.output + val forwardTrace = result.trace + + var String fileURI = null; + var String vampireCode = null; + if(vampireConfig.writeToFile) { + fileURI = workspace.writeModel(vampireProblem,fileName).toFileString + } else { + vampireCode = workspace.writeModelToString(vampireProblem,fileName) + } + val transformationTime = System.currentTimeMillis - transformationStart + // Finish: Logic -> Vampire mapping + + //Creates a file containing the tptp code after transformation + val out = new PrintWriter("output/files/vampireCode.tptp") + out.println(vampireCode) + out.close() + + + /* + * not for now -> Start: Solving Alloy problem + * + // Start: Solving Alloy problem + val solverStart = System.currentTimeMillis + val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode) + val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) + val solverFinish = System.currentTimeMillis-solverStart + // Finish: Solving Alloy problem + + if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) + + return logicResult + */ + + return null // for now + } + + def asConfig(LogicSolverConfiguration configuration){ + if(configuration instanceof VampireSolverConfiguration) { + return configuration + } else { + throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''') + } + } + +// /* +// * not for now +// * + override getInterpretations(ModelResult modelResult) { + //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] +// val sols = modelResult.representation// as List +// //val res = answers.map +// sols.map[ +// new VampireModelInterpretation( +// forwardMapper.typeMapper.typeInterpreter, +// it as A4Solution, +// forwardMapper, +// modelResult.trace as Logic2AlloyLanguageMapperTrace +// ) +// ] + } +// */ + +} \ No newline at end of file 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 new file mode 100644 index 00000000..5ec15541 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend @@ -0,0 +1,386 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel +import java.util.Collections +import java.util.HashMap +import java.util.List +import java.util.Map +import org.eclipse.xtend.lib.annotations.Accessors + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2VampireLanguageMapper { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support; + @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper( + this) + @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( + this) + @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper + + public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) { + this.typeMapper = typeMapper + } + + public def TracedOutput transformProblem(LogicProblem problem, + VampireSolverConfiguration configuration) { + // create model bases + // TODO + val initialComment = createVLSComment => [ + it.comment = "%This is an initial Test Comment \r" + ] + + val specification = createVampireModel => [ + it.comments += initialComment + ] + + val trace = new Logic2VampireLanguageMapperTrace => [ + it.specification = specification + +// it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem)) + ] + + // call mappers + if (!problem.types.isEmpty) { + typeMapper.transformTypes(problem.types, problem.elements, this, trace) + } + + trace.constantDefinitions = problem.collectConstantDefinitions + trace.relationDefinitions = problem.collectRelationDefinitions + + problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] + + // only transforms definitions + // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)] + problem.constants.filter(ConstantDefinition).forEach [ + this.constantMapper.transformConstantDefinitionSpecification(it, trace) + ] + + // ////////////////// + // Transform Assertions + // ////////////////// + for (assertion : problem.assertions) { + transformAssertion(assertion, trace) + } + + return new TracedOutput(specification, trace) + } + + // End of transformProblem + // //////////// + // Type References + // //////////// + def dispatch protected VLSTerm transformTypeReference(BoolTypeReference boolTypeReference, + Logic2VampireLanguageMapperTrace trace) { + // TODO, Not Now + // return createALSReference => [ it.referred = support.getBooleanType(trace) ] + } + + // //////////// + // Collectors + // //////////// + // exact Same as for Alloy + private def collectConstantDefinitions(LogicProblem problem) { + val res = new HashMap + problem.constants.filter(ConstantDefinition).filter[it.defines !== null].forEach [ + res.put(it.defines, it) + ] + return res + } + + private def collectRelationDefinitions(LogicProblem problem) { + val res = new HashMap + problem.relations.filter(RelationDefinition).filter[it.defines !== null].forEach [ + res.put(it.defines, it) + ] + return res + } + + // //////////// + // Assertions + Terms + // //////////// + def protected transformAssertion(Assertion assertion, Logic2VampireLanguageMapperTrace trace) { + val res = createVLSFofFormula => [ + it.name = support.toID(assertion.name) + // below is temporary solution + it.fofRole = "axiom" + it.fofFormula = assertion.value.transformTerm(trace, Collections.EMPTY_MAP) + // it.annotation = nothing + ] + trace.specification.formulas += res + } + + def dispatch protected VLSTerm transformTerm(BoolLiteral literal, Logic2VampireLanguageMapperTrace trace, + Map variables) { + if (literal.value == true) { + createVLSTrue + } else { + createVLSFalse + } + } + + def dispatch protected VLSTerm transformTerm(IntLiteral literal, Logic2VampireLanguageMapperTrace trace, + Map variables) { + createVLSInt => [it.value = literal.value.toString()] + } + + def dispatch protected VLSTerm transformTerm(RealLiteral literal, Logic2VampireLanguageMapperTrace trace, + 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)] + } + + def dispatch protected VLSTerm transformTerm(And and, Logic2VampireLanguageMapperTrace trace, + Map variables) { support.unfoldAnd(and.operands.map[transformTerm(trace, variables)]) } + + def dispatch protected VLSTerm transformTerm(Or or, Logic2VampireLanguageMapperTrace trace, + Map variables) { support.unfoldOr(or.operands.map[transformTerm(trace, variables)]) } + + def dispatch protected VLSTerm transformTerm(Impl impl, Logic2VampireLanguageMapperTrace trace, + Map variables) { + createVLSImplies => [ + left = impl.leftOperand.transformTerm(trace, variables) + right = impl.rightOperand.transformTerm(trace, variables) + ] + } + + def dispatch protected VLSTerm transformTerm(Iff iff, Logic2VampireLanguageMapperTrace trace, + Map variables) { + createVLSEquivalent => [ + left = iff.leftOperand.transformTerm(trace, variables) + right = iff.rightOperand.transformTerm(trace, variables) + ] + } + +// def dispatch protected VLSTerm transformTerm(MoreThan moreThan, Logic2VampireLanguageMapperTrace trace, Map variables) { +// createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } +// def dispatch protected VLSTerm transformTerm(LessThan lessThan, Logic2VampireLanguageMapperTrace trace, Map variables) { +// createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } +// def dispatch protected VLSTerm transformTerm(MoreOrEqualThan moreThan, Logic2VampireLanguageMapperTrace trace, Map variables) { +// createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } +// def dispatch protected VLSTerm transformTerm(LessOrEqualThan lessThan, Logic2VampireLanguageMapperTrace trace, Map variables) { +// createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } + def dispatch protected VLSTerm transformTerm(Equals equals, Logic2VampireLanguageMapperTrace trace, + Map variables) { + createVLSEquality => [ + left = equals.leftOperand.transformTerm(trace, variables) + right = equals.rightOperand.transformTerm(trace, variables) + ] + } + + def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, Map variables) { + support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } +// +// def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] } +// def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] } +// def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] } +// def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] } +// def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] } +// + def dispatch protected VLSTerm transformTerm(Forall forall, Logic2VampireLanguageMapperTrace trace, + Map variables) { + support.createUniversallyQuantifiedExpression(this, forall, trace, variables) + } + + def dispatch protected VLSTerm transformTerm(Exists exists, Logic2VampireLanguageMapperTrace trace, + Map variables) { + support.createExistentiallyQuantifiedExpression(this, exists, trace, variables) + } + + def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map variables) { + return createVLSFunction => [ + it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name ) + it.terms += instanceOf.value.transformTerm(trace, variables) + ] + } +// +// def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// return this.relationMapper.transformTransitiveRelationReference( +// tc.relation, +// tc.leftOperand.transformTerm(trace,variables), +// tc.rightOperand.transformTerm(trace,variables), +// trace +// ) +// } +// + def dispatch protected VLSTerm transformTerm(SymbolicValue symbolicValue, Logic2VampireLanguageMapperTrace trace, + Map variables) { + symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions, trace, + variables) + } + + def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { + typeMapper.transformReference(referred, trace) + } + + def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { + // might need to make sure that only declared csts get transformed. see for Alloy + val res = createVLSConstant => [ + // ask if necessary VLSConstantDeclaration and not just directly strng + it.name = support.toID(constant.name) + ] + // no postprocessing cuz booleans are accepted + return res + } + + // NOT NEEDED FOR NOW + // TODO + def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { +// val res = createVLSFunctionCall => [ +// it.referredDefinition = constant.lookup(trace.constantDefinition2Function) +// ] +// return support.postprocessResultOfSymbolicReference(constant.type,res,trace) + } + + def dispatch protected VLSTerm transformSymbolicReference(Variable variable, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { + + // cannot treat variable as function (constant) because of name ID not being the same + // below does not work + val res = createVLSVariable => [ +// it.name = support.toIDMultiple("Var", variable.lookup(variables).name) + it.name = support.toID(variable.lookup(variables).name) + ] + // no need for potprocessing cuz booleans are supported + return res + } + + // TODO + def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { +// if(trace.functionDefinitions.containsKey(function)) { +// return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) +// } else { +// if(functionMapper.transformedToHostedField(function,trace)) { +// val param = parameterSubstitutions.get(0).transformTerm(trace,variables) +// val res = createVLSJoin => [ +// leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace) +// rightOperand = createVLSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)] +// ] +// return support.postprocessResultOfSymbolicReference(function.range,res,trace) +// } else { +// val functionExpression = createVLSJoin=>[ +// leftOperand = createVLSReference => [referred = trace.logicLanguage] +// rightOperand = createVLSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)] +// ] +// val res = support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables) +// return support.postprocessResultOfSymbolicReference(function.range,res,trace) +// } +// } + } + + // TODO + def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { +// val result = createVLSFunctionCall => [ +// it.referredDefinition = function.lookup(trace.functionDefinition2Function) +// it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] +// ] +// return support.postprocessResultOfSymbolicReference(function.range,result,trace) + } + + // TODO + /* + def dispatch protected VLSTerm transformSymbolicReference(Relation relation, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { + if (trace.relationDefinitions.containsKey(relation)) { + this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), + parameterSubstitutions, trace, variables) + } + else { +// if (relationMapper.transformToHostedField(relation, trace)) { +// val VLSRelation = relation.lookup(trace.relationDeclaration2Field) +// // R(a,b) => +// // b in a.R +// return createVLSSubset => [ +// it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) +// it.rightOperand = createVLSJoin => [ +// it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) +// it.rightOperand = createVLSReference => [it.referred = VLSRelation] +// ] +// ] +// } else { +// val target = createVLSJoin => [ +// leftOperand = createVLSReference => [referred = trace.logicLanguage] +// rightOperand = createVLSReference => [ +// referred = relation.lookup(trace.relationDeclaration2Global) +// ] +// ] +// val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) +// +// return createVLSSubset => [ +// leftOperand = source +// rightOperand = target +// ] +// } + } + } + */ + + // TODO + def dispatch protected VLSTerm transformSymbolicReference(Relation relation, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { +// createVLSFunction => [ +// it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) +// it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] +// ] + return createVLSFunction => [ + it.constant = support.toIDMultiple("rel", relation.name) + it.terms += parameterSubstitutions.map[p | p.transformTerm(trace,variables)] + ] + } + + } + \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend new file mode 100644 index 00000000..135b3f07 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend @@ -0,0 +1,39 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel +import java.util.HashMap +import java.util.Map + +interface Logic2VampireLanguageMapper_TypeMapperTrace {} + +class Logic2VampireLanguageMapperTrace { +// public var ViatraQueryEngine incQueryEngine; + + //list of needed VLS components + public var VampireModel specification + public var VLSFofFormula logicLanguageBody + public var VLSTerm formula +//NOT NEEDED //public var VLSFunction constantDec + + public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace + + +//NOT NEEDED //public val Map constantDeclaration2LanguageField = new HashMap + //public val Map constantDefinition2Function = new HashMap + + public var Map constantDefinitions + + public var Map relationDefinitions + public val Map relationVar2VLS = new HashMap + public val Map relationVar2TypeDec = new HashMap + +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend new file mode 100644 index 00000000..2366ea15 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend @@ -0,0 +1,42 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory + +class Logic2VampireLanguageMapper_ConstantMapper { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + val Logic2VampireLanguageMapper base + + public new(Logic2VampireLanguageMapper base) { + this.base = base + } + +//NOT NEEDED +// def protected dispatch transformConstant(ConstantDeclaration constant, Logic2VampireLanguageMapperTrace trace) { +// val c = createVLSFunctionDeclaration=> [ +// it.name = support.toID(constant.name) +// ] +// trace.constantDec.constant = c +// trace.constantDeclaration2LanguageField.put(constant, c); +// +// } + +//NOT Used In Sample + def protected dispatch transformConstant(ConstantDefinition constant, Logic2VampireLanguageMapperTrace trace) { + //error + //TODO +// val c = createVLSFofFormula=> [ +// name = support.toID(constant.name) +// fofRole = "axiom" +// fofFormula = base.transformTypeReference() +// ] + } + + def protected transformConstantDefinitionSpecification(ConstantDefinition constant, Logic2VampireLanguageMapperTrace trace) { + //TODO + } + + +} \ No newline at end of file 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 new file mode 100644 index 00000000..60653a42 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend @@ -0,0 +1,183 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import java.util.ArrayList +import java.util.HashMap +import java.util.List +import java.util.Map + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2VampireLanguageMapper_RelationMapper { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + val Logic2VampireLanguageMapper base + + public new(Logic2VampireLanguageMapper base) { + this.base = base + } + + def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace) { + + // 1. store all variables in support wrt their name + // 1.1 if variable has type, creating list of type declarations + val Map relationVar2VLS = new HashMap + val Map relationVar2TypeDecComply = new HashMap + val Map relationVar2TypeDecRes = new HashMap + val typedefs = new ArrayList + for (variable : r.variables) { + val v = createVLSVariable => [ + it.name = support.toIDMultiple("Var", variable.name) + ] + relationVar2VLS.put(variable, v) + + val varTypeComply = createVLSFunction => [ + it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.terms += createVLSVariable => [ + it.name = support.toIDMultiple("Var", variable.name) + ] + ] + relationVar2TypeDecComply.put(variable, varTypeComply) + + val varTypeRes = createVLSFunction => [ + it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.terms += createVLSVariable => [ + it.name = support.toIDMultiple("Var", variable.name) + ] + ] + relationVar2TypeDecRes.put(variable, varTypeRes) + } + + val comply = createVLSFofFormula => [ + it.name = support.toIDMultiple("compliance", r.name) + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + for (variable : r.variables) { + val v = createVLSVariable => [ + it.name = variable.lookup(relationVar2VLS).name + ] + it.variables += v + + } + it.operand = createVLSImplies => [ + it.left = createVLSFunction => [ + it.constant = support.toIDMultiple("rel", r.name) + for (variable : r.variables) { + val v = createVLSVariable => [ + it.name = variable.lookup(relationVar2VLS).name + ] + it.terms += v + } + ] + it.right = support.unfoldAnd(new ArrayList(relationVar2TypeDecComply.values)) + ] + ] + ] + + val res = createVLSFofFormula => [ + it.name = support.toIDMultiple("relation", r.name) + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + for (variable : r.variables) { + val v = createVLSVariable => [ + it.name = variable.lookup(relationVar2VLS).name + ] + it.variables += v + + } + it.operand = createVLSImplies => [ + it.left = support.unfoldAnd(new ArrayList(relationVar2TypeDecRes.values)) + it.right = createVLSEquivalent => [ + it.left = createVLSFunction => [ + it.constant = support.toIDMultiple("rel", r.name) + for (variable : r.variables) { + val v = createVLSVariable => [ + it.name = variable.lookup(relationVar2VLS).name + ] + it.terms += v + + } + ] + it.right = base.transformTerm(r.value, trace, relationVar2VLS) + ] + + ] + + ] + + ] + + // trace.relationDefinition2Predicate.put(r,res) + trace.specification.formulas += comply; + trace.specification.formulas += res; + + } + + def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) { + + // 1. store all variables in support wrt their name + // 1.1 if variable has type, creating list of type declarations + val List relationVar2VLS = new ArrayList + val List relationVar2TypeDecComply = new ArrayList + val typedefs = new ArrayList + + for (i : 0.. [ + it.name = support.toIDMultiple("Var", i.toString) + ] + relationVar2VLS.add(v) + + val varTypeComply = createVLSFunction => [ + it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name) + it.terms += createVLSVariable => [ + it.name = support.toIDMultiple("Var", i.toString) + ] + ] + relationVar2TypeDecComply.add(varTypeComply) + + } + + + val comply = createVLSFofFormula => [ + it.name = support.toIDMultiple("compliance", r.name) + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + + for (i : 0.. [ + it.name = relationVar2VLS.get(i).name + ] + it.variables += v + + } + + it.operand = createVLSImplies => [ + it.left = createVLSFunction => [ + it.constant = support.toIDMultiple("rel", r.name) + + for (i : 0.. [ + it.name = relationVar2VLS.get(i).name + ] + it.terms += v + } + + ] + it.right = support.unfoldAnd(relationVar2TypeDecComply) + ] + ] + ] + + // trace.relationDefinition2Predicate.put(r,res) + trace.specification.formulas += comply + } + +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend new file mode 100644 index 00000000..ab92b42f --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend @@ -0,0 +1,148 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import java.util.ArrayList +import java.util.HashMap +import java.util.List +import java.util.Map +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import org.eclipse.emf.common.util.EList +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term + +class Logic2VampireLanguageMapper_Support { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + + // ID Handler + def protected String toIDMultiple(String... ids) { + ids.map[it.split("\\s+").join("_")].join("_") + } + + def protected String toID(String ids) { + ids.split("\\s+").join("_") + } + + // Support Functions + // booleans + // AND and OR + def protected VLSTerm unfoldAnd(List operands) { + if (operands.size == 1) { + return operands.head + } else if (operands.size > 1) { + return createVLSAnd => [ + left = operands.head + right = operands.subList(1, operands.size).unfoldAnd + ] + } else + throw new UnsupportedOperationException('''Logic operator with 0 operands!''') + } + + def protected VLSTerm unfoldOr(List operands) { + +// if(operands.size == 0) {basically return true} + /*else*/ if (operands.size == 1) { + return operands.head + } else if (operands.size > 1) { + return createVLSOr => [ + left = operands.head + right = operands.subList(1, operands.size).unfoldOr + ] + } else + throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP + } + + def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList operands, + Logic2VampireLanguageMapperTrace trace, Map variables) { + if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) } + else if(operands.size > 1) { + val notEquals = new ArrayList(operands.size*operands.size/2) + for(i:0..[ + it.left= m.transformTerm(operands.get(i),trace,variables) + it.right = m.transformTerm(operands.get(j),trace,variables) + ] + } + } + return notEquals.unfoldAnd + } + else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') + } + + // Symbolic + // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) { +// if(type instanceof BoolTypeReference) { +// return booleanToLogicValue(term ,trace) +// } +// else return term +// } +// def booleanToLogicValue(VLSTerm term, Logic2VampireLanguageMapperTrace trace) { +// throw new UnsupportedOperationException("TODO: auto-generated method stub") +// } + /* + * def protected String toID(List ids) { + * ids.map[it.split("\\s+").join("'")].join("'") + * } + */ + // QUANTIFIERS + VARIABLES + def protected VLSTerm createUniversallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, + QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables) { + val variableMap = expression.quantifiedVariables.toInvertedMap [ v | + createVLSVariable => [it.name = toIDMultiple("Var", v.name)] + ] + + val typedefs = new ArrayList + for (variable : expression.quantifiedVariables) { + val eq = createVLSFunction => [ + it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.terms += createVLSVariable => [ + it.name = toIDMultiple("Var", variable.name) + ] + + ] + typedefs.add(eq) + } + + + createVLSUniversalQuantifier => [ + it.variables += variableMap.values + it.operand = createVLSImplies => [ + it.left = unfoldAnd(typedefs) + it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)) + ] + ] + } + + def protected VLSTerm createExistentiallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, + QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables) { + val variableMap = expression.quantifiedVariables.toInvertedMap [ v | + createVLSVariable => [it.name = toIDMultiple("Var", v.name)] + ] + + val typedefs = new ArrayList + for (variable : expression.quantifiedVariables) { + val eq = createVLSFunction => [ + it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.terms += createVLSVariable => [ + it.name = toIDMultiple("Var", variable.name) + ] + ] + typedefs.add(eq) + } + + typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))) + createVLSExistentialQuantifier => [ + it.variables += variableMap.values + it.operand = unfoldAnd(typedefs) + + ] + } + + def protected withAddition(Map map1, Map map2) { + new HashMap(map1) => [putAll(map2)] + } + +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend new file mode 100644 index 00000000..1f071635 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend @@ -0,0 +1,19 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import java.util.Collection +import java.util.List +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm + +interface Logic2VampireLanguageMapper_TypeMapper { + def void transformTypes(Collection types, Collection elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace); + //samples below 2 lines + def List transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) + def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) + + def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace) + def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace) + + def VampireModelInterpretation_TypeInterpretation getTypeInterpreter() +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend new file mode 100644 index 00000000..a0f0edda --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend @@ -0,0 +1,21 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import java.util.ArrayList +import java.util.HashMap +import java.util.List +import java.util.Map + +class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace{ + +// public var VLSFofFormula objectSuperClass + public val Map type2Predicate = new HashMap; + public val Map definedElement2Declaration = new HashMap //Not Yet Used + public val Map type2PossibleNot = new HashMap + public val Map type2And = new HashMap + +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..7221f3ff --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend @@ -0,0 +1,158 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import java.util.ArrayList +import java.util.Collection + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + + new() { + LogicproblemPackage.eINSTANCE.class + } + + override transformTypes(Collection types, Collection elements, + Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { + val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes + trace.typeMapperTrace = typeTrace + + val VLSVariable variable = createVLSVariable => [it.name = "A"] // did not work + // 1. store predicates for declarations in trace + for (type : types) { + val typePred = createVLSFunction => [ + it.constant = support.toIDMultiple("type", type.name) + it.terms += createVLSVariable => [it.name = variable.name] + ] + typeTrace.type2Predicate.put(type, typePred) + } + + // 2. Map each type definition to fof formula + for (type : types.filter(TypeDefinition)) { + + val res = createVLSFofFormula => [ + it.name = support.toIDMultiple("typeDef", type.name) + // below is temporary solution + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += createVLSVariable => [it.name = variable.name] + it.operand = createVLSEquivalent => [ + it.left = createVLSFunction => [ + it.constant = type.lookup(typeTrace.type2Predicate).constant + it.terms += createVLSVariable => [it.name = "A"] + ] + + type.lookup(typeTrace.type2Predicate) + it.right = support.unfoldOr(type.elements.map [ e | + createVLSEquality => [ + it.left = createVLSVariable => [it.name = variable.name] +// it.right = createVLSDoubleQuote => [ +// it.value = "\"" + e.name + "\"" +// ] + it.right = createVLSDoubleQuote => [ + it.value = "\"a" + e.name + "\"" + ] + ] + ]) + ] + ] + + ] + trace.specification.formulas += res + } + // 2.5. Currently allowing duplicate types. Not problematic cuz strings are by def unique + // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates + // and store in a map +// val List type2PossibleNot = new ArrayList +// val List type2And = new ArrayList + for (type : types.filter[!isIsAbstract]) { + for (type2 : types) { + // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes + if (type == type2 || dfsSupertypeCheck(type, type2)) { + typeTrace.type2PossibleNot.put(type2, createVLSFunction => [ + it.constant = type2.lookup(typeTrace.type2Predicate).constant + it.terms += createVLSVariable => [it.name = "A"] + ]) + } else { + typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [ + it.operand = createVLSFunction => [ + it.constant = type2.lookup(typeTrace.type2Predicate).constant + it.terms += createVLSVariable => [it.name = "A"] + ] + ]) + } +// typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate)) + } + typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList(typeTrace.type2PossibleNot.values))) +// typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) ) + typeTrace.type2PossibleNot.clear + } + + // 5. create fof function that is an or with all the elements in map + val hierarch = createVLSFofFormula => [ + it.name = "hierarchyHandler" + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += createVLSVariable => [it.name = "A"] + it.operand = createVLSEquivalent => [ + it.left = createVLSFunction => [ + it.constant = "Object" + it.terms += createVLSVariable => [ + it.name = "A" + ] + ] + it.right = support.unfoldOr(new ArrayList(typeTrace.type2And.values)) + ] + ] + ] + + trace.specification.formulas += hierarch + } + + def boolean dfsSupertypeCheck(Type type, Type type2) { + // There is surely a better way to do this + if (type.supertypes.isEmpty) + return false + else { + if (type.supertypes.contains(type2)) + return true + else { + for (supertype : type.supertypes) { + if(dfsSupertypeCheck(supertype, type2)) return true + } + } + } + } + + override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, + Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { + createVLSDoubleQuote => [ + it.value = "\"a" + referred.name + "\"" + ] + } + + override getTypeInterpreter() { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend new file mode 100644 index 00000000..66f4fb06 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend @@ -0,0 +1,5 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +interface VampireModelInterpretation_TypeInterpretation { + +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend new file mode 100644 index 00000000..863ec783 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend @@ -0,0 +1,5 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation { + //TODO +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf