diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-01-15 12:44:33 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:06:26 -0400 |
commit | f87b4233437f0900c19f462b5e443a3c81b27b6e (patch) | |
tree | fa5af86016db54e24f54e3d801424eb1216efc2f /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner | |
parent | Fix numeric-solver-at-end (diff) | |
download | VIATRA-Generator-f87b4233437f0900c19f462b5e443a3c81b27b6e.tar.gz VIATRA-Generator-f87b4233437f0900c19f462b5e443a3c81b27b6e.tar.zst VIATRA-Generator-f87b4233437f0900c19f462b5e443a3c81b27b6e.zip |
Initial workspace setup
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner')
49 files changed, 2718 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath new file mode 100644 index 00000000..a1e0140b --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath | |||
@@ -0,0 +1,9 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <classpath> | ||
3 | <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/> | ||
4 | <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> | ||
5 | <classpathentry kind="src" path="src"/> | ||
6 | <classpathentry kind="src" path="xtend-gen"/> | ||
7 | <classpathentry kind="src" path="queries"/> | ||
8 | <classpathentry kind="output" path="bin"/> | ||
9 | </classpath> | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.gitignore new file mode 100644 index 00000000..ae3c1726 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.gitignore | |||
@@ -0,0 +1 @@ | |||
/bin/ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project new file mode 100644 index 00000000..2221f39c --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project | |||
@@ -0,0 +1,34 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <projectDescription> | ||
3 | <name>ca.mcgill.ecse.dslreasoner.vampire.reasoner</name> | ||
4 | <comment></comment> | ||
5 | <projects> | ||
6 | </projects> | ||
7 | <buildSpec> | ||
8 | <buildCommand> | ||
9 | <name>org.eclipse.xtext.ui.shared.xtextBuilder</name> | ||
10 | <arguments> | ||
11 | </arguments> | ||
12 | </buildCommand> | ||
13 | <buildCommand> | ||
14 | <name>org.eclipse.jdt.core.javabuilder</name> | ||
15 | <arguments> | ||
16 | </arguments> | ||
17 | </buildCommand> | ||
18 | <buildCommand> | ||
19 | <name>org.eclipse.pde.ManifestBuilder</name> | ||
20 | <arguments> | ||
21 | </arguments> | ||
22 | </buildCommand> | ||
23 | <buildCommand> | ||
24 | <name>org.eclipse.pde.SchemaBuilder</name> | ||
25 | <arguments> | ||
26 | </arguments> | ||
27 | </buildCommand> | ||
28 | </buildSpec> | ||
29 | <natures> | ||
30 | <nature>org.eclipse.pde.PluginNature</nature> | ||
31 | <nature>org.eclipse.jdt.core.javanature</nature> | ||
32 | <nature>org.eclipse.xtext.ui.shared.xtextNature</nature> | ||
33 | </natures> | ||
34 | </projectDescription> | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.settings/org.eclipse.jdt.core.prefs b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..295926d9 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.settings/org.eclipse.jdt.core.prefs | |||
@@ -0,0 +1,7 @@ | |||
1 | eclipse.preferences.version=1 | ||
2 | org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled | ||
3 | org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 | ||
4 | org.eclipse.jdt.core.compiler.compliance=1.8 | ||
5 | org.eclipse.jdt.core.compiler.problem.assertIdentifier=error | ||
6 | org.eclipse.jdt.core.compiler.problem.enumIdentifier=error | ||
7 | org.eclipse.jdt.core.compiler.source=1.8 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF new file mode 100644 index 00000000..2eb4f151 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF | |||
@@ -0,0 +1,17 @@ | |||
1 | Manifest-Version: 1.0 | ||
2 | Bundle-ManifestVersion: 2 | ||
3 | Bundle-Name: Reasoner | ||
4 | Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.reasoner;singleton:=true | ||
5 | Bundle-Version: 1.0.0.qualifier | ||
6 | Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.reasoner | ||
7 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | ||
8 | Require-Bundle: org.eclipse.xtend.lib, | ||
9 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | ||
10 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | ||
11 | ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", | ||
12 | org.eclipse.viatra.query.runtime;bundle-version="2.1.0", | ||
13 | org.eclipse.viatra.query.runtime.base.itc;bundle-version="2.1.0" | ||
14 | Export-Package: ca.mcgill.ecse.dslreasoner.vampire.reasoner, | ||
15 | ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
16 | |||
17 | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties new file mode 100644 index 00000000..41eb6ade --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties | |||
@@ -0,0 +1,4 @@ | |||
1 | source.. = src/ | ||
2 | output.. = bin/ | ||
3 | bin.includes = META-INF/,\ | ||
4 | . | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/signatureQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/signatureQueries.vql new file mode 100644 index 00000000..754b5ac7 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/signatureQueries.vql | |||
@@ -0,0 +1 @@ | |||
package ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries \ No newline at end of file | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/typeQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/typeQueries.vql new file mode 100644 index 00000000..754b5ac7 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/typeQueries.vql | |||
@@ -0,0 +1 @@ | |||
package ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries \ 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/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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
4 | |||
5 | class VampireSolverConfiguration extends LogicSolverConfiguration { | ||
6 | |||
7 | public var int symmetry = 0 // by default | ||
8 | //choose needed backend solver | ||
9 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J | ||
10 | public var boolean writeToFile = false | ||
11 | } | ||
12 | |||
13 | |||
14 | enum VampireBackendSolver { | ||
15 | //add needed things | ||
16 | } | ||
17 | |||
18 | |||
19 | enum TypeMappingTechnique { | ||
20 | //default | ||
21 | FilteredTypes | ||
22 | } \ 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage | ||
11 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
12 | import java.io.PrintWriter | ||
13 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | ||
14 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper | ||
15 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes | ||
16 | |||
17 | class VampireSolver extends LogicReasoner{ | ||
18 | |||
19 | new() { | ||
20 | VampireLanguagePackage.eINSTANCE.eClass | ||
21 | val x = new VampireLanguageStandaloneSetupGenerated | ||
22 | VampireLanguageStandaloneSetup::doSetup() | ||
23 | } | ||
24 | |||
25 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) | ||
26 | // //not for now | ||
27 | // val VampireHandler handler = new VampireHandler | ||
28 | // val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | ||
29 | |||
30 | val fileName = "problem.tptp" | ||
31 | |||
32 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | ||
33 | val vampireConfig = configuration.asConfig | ||
34 | |||
35 | // Start: Logic -> Vampire mapping | ||
36 | val transformationStart = System.currentTimeMillis | ||
37 | //TODO | ||
38 | val result = forwardMapper.transformProblem(problem,vampireConfig) | ||
39 | val vampireProblem = result.output | ||
40 | val forwardTrace = result.trace | ||
41 | |||
42 | var String fileURI = null; | ||
43 | var String vampireCode = null; | ||
44 | if(vampireConfig.writeToFile) { | ||
45 | fileURI = workspace.writeModel(vampireProblem,fileName).toFileString | ||
46 | } else { | ||
47 | vampireCode = workspace.writeModelToString(vampireProblem,fileName) | ||
48 | } | ||
49 | val transformationTime = System.currentTimeMillis - transformationStart | ||
50 | // Finish: Logic -> Vampire mapping | ||
51 | |||
52 | //Creates a file containing the tptp code after transformation | ||
53 | val out = new PrintWriter("output/files/vampireCode.tptp") | ||
54 | out.println(vampireCode) | ||
55 | out.close() | ||
56 | |||
57 | |||
58 | /* | ||
59 | * not for now -> Start: Solving Alloy problem | ||
60 | * | ||
61 | // Start: Solving Alloy problem | ||
62 | val solverStart = System.currentTimeMillis | ||
63 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode) | ||
64 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | ||
65 | val solverFinish = System.currentTimeMillis-solverStart | ||
66 | // Finish: Solving Alloy problem | ||
67 | |||
68 | if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) | ||
69 | |||
70 | return logicResult | ||
71 | */ | ||
72 | |||
73 | return null // for now | ||
74 | } | ||
75 | |||
76 | def asConfig(LogicSolverConfiguration configuration){ | ||
77 | if(configuration instanceof VampireSolverConfiguration) { | ||
78 | return configuration | ||
79 | } else { | ||
80 | throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''') | ||
81 | } | ||
82 | } | ||
83 | |||
84 | // /* | ||
85 | // * not for now | ||
86 | // * | ||
87 | override getInterpretations(ModelResult modelResult) { | ||
88 | //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] | ||
89 | // val sols = modelResult.representation// as List<A4Solution> | ||
90 | // //val res = answers.map | ||
91 | // sols.map[ | ||
92 | // new VampireModelInterpretation( | ||
93 | // forwardMapper.typeMapper.typeInterpreter, | ||
94 | // it as A4Solution, | ||
95 | // forwardMapper, | ||
96 | // modelResult.trace as Logic2AlloyLanguageMapperTrace | ||
97 | // ) | ||
98 | // ] | ||
99 | } | ||
100 | // */ | ||
101 | |||
102 | } \ 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
31 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
32 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
33 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
34 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
35 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
36 | import java.util.Collections | ||
37 | import java.util.HashMap | ||
38 | import java.util.List | ||
39 | import java.util.Map | ||
40 | import org.eclipse.xtend.lib.annotations.Accessors | ||
41 | |||
42 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
43 | |||
44 | class Logic2VampireLanguageMapper { | ||
45 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
46 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support; | ||
47 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper( | ||
48 | this) | ||
49 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( | ||
50 | this) | ||
51 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper | ||
52 | |||
53 | public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) { | ||
54 | this.typeMapper = typeMapper | ||
55 | } | ||
56 | |||
57 | public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem, | ||
58 | VampireSolverConfiguration configuration) { | ||
59 | // create model bases | ||
60 | // TODO | ||
61 | val initialComment = createVLSComment => [ | ||
62 | it.comment = "%This is an initial Test Comment \r" | ||
63 | ] | ||
64 | |||
65 | val specification = createVampireModel => [ | ||
66 | it.comments += initialComment | ||
67 | ] | ||
68 | |||
69 | val trace = new Logic2VampireLanguageMapperTrace => [ | ||
70 | it.specification = specification | ||
71 | |||
72 | // it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem)) | ||
73 | ] | ||
74 | |||
75 | // call mappers | ||
76 | if (!problem.types.isEmpty) { | ||
77 | typeMapper.transformTypes(problem.types, problem.elements, this, trace) | ||
78 | } | ||
79 | |||
80 | trace.constantDefinitions = problem.collectConstantDefinitions | ||
81 | trace.relationDefinitions = problem.collectRelationDefinitions | ||
82 | |||
83 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] | ||
84 | |||
85 | // only transforms definitions | ||
86 | // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)] | ||
87 | problem.constants.filter(ConstantDefinition).forEach [ | ||
88 | this.constantMapper.transformConstantDefinitionSpecification(it, trace) | ||
89 | ] | ||
90 | |||
91 | // ////////////////// | ||
92 | // Transform Assertions | ||
93 | // ////////////////// | ||
94 | for (assertion : problem.assertions) { | ||
95 | transformAssertion(assertion, trace) | ||
96 | } | ||
97 | |||
98 | return new TracedOutput(specification, trace) | ||
99 | } | ||
100 | |||
101 | // End of transformProblem | ||
102 | // //////////// | ||
103 | // Type References | ||
104 | // //////////// | ||
105 | def dispatch protected VLSTerm transformTypeReference(BoolTypeReference boolTypeReference, | ||
106 | Logic2VampireLanguageMapperTrace trace) { | ||
107 | // TODO, Not Now | ||
108 | // return createALSReference => [ it.referred = support.getBooleanType(trace) ] | ||
109 | } | ||
110 | |||
111 | // //////////// | ||
112 | // Collectors | ||
113 | // //////////// | ||
114 | // exact Same as for Alloy | ||
115 | private def collectConstantDefinitions(LogicProblem problem) { | ||
116 | val res = new HashMap | ||
117 | problem.constants.filter(ConstantDefinition).filter[it.defines !== null].forEach [ | ||
118 | res.put(it.defines, it) | ||
119 | ] | ||
120 | return res | ||
121 | } | ||
122 | |||
123 | private def collectRelationDefinitions(LogicProblem problem) { | ||
124 | val res = new HashMap | ||
125 | problem.relations.filter(RelationDefinition).filter[it.defines !== null].forEach [ | ||
126 | res.put(it.defines, it) | ||
127 | ] | ||
128 | return res | ||
129 | } | ||
130 | |||
131 | // //////////// | ||
132 | // Assertions + Terms | ||
133 | // //////////// | ||
134 | def protected transformAssertion(Assertion assertion, Logic2VampireLanguageMapperTrace trace) { | ||
135 | val res = createVLSFofFormula => [ | ||
136 | it.name = support.toID(assertion.name) | ||
137 | // below is temporary solution | ||
138 | it.fofRole = "axiom" | ||
139 | it.fofFormula = assertion.value.transformTerm(trace, Collections.EMPTY_MAP) | ||
140 | // it.annotation = nothing | ||
141 | ] | ||
142 | trace.specification.formulas += res | ||
143 | } | ||
144 | |||
145 | def dispatch protected VLSTerm transformTerm(BoolLiteral literal, Logic2VampireLanguageMapperTrace trace, | ||
146 | Map<Variable, VLSVariable> variables) { | ||
147 | if (literal.value == true) { | ||
148 | createVLSTrue | ||
149 | } else { | ||
150 | createVLSFalse | ||
151 | } | ||
152 | } | ||
153 | |||
154 | def dispatch protected VLSTerm transformTerm(IntLiteral literal, Logic2VampireLanguageMapperTrace trace, | ||
155 | Map<Variable, VLSVariable> variables) { | ||
156 | createVLSInt => [it.value = literal.value.toString()] | ||
157 | } | ||
158 | |||
159 | def dispatch protected VLSTerm transformTerm(RealLiteral literal, Logic2VampireLanguageMapperTrace trace, | ||
160 | Map<Variable, VLSVariable> variables) { | ||
161 | createVLSReal => [it.value = literal.value.toString()] | ||
162 | } | ||
163 | |||
164 | def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace, | ||
165 | Map<Variable, VLSVariable> variables) { | ||
166 | createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)] | ||
167 | } | ||
168 | |||
169 | def dispatch protected VLSTerm transformTerm(And and, Logic2VampireLanguageMapperTrace trace, | ||
170 | Map<Variable, VLSVariable> variables) { support.unfoldAnd(and.operands.map[transformTerm(trace, variables)]) } | ||
171 | |||
172 | def dispatch protected VLSTerm transformTerm(Or or, Logic2VampireLanguageMapperTrace trace, | ||
173 | Map<Variable, VLSVariable> variables) { support.unfoldOr(or.operands.map[transformTerm(trace, variables)]) } | ||
174 | |||
175 | def dispatch protected VLSTerm transformTerm(Impl impl, Logic2VampireLanguageMapperTrace trace, | ||
176 | Map<Variable, VLSVariable> variables) { | ||
177 | createVLSImplies => [ | ||
178 | left = impl.leftOperand.transformTerm(trace, variables) | ||
179 | right = impl.rightOperand.transformTerm(trace, variables) | ||
180 | ] | ||
181 | } | ||
182 | |||
183 | def dispatch protected VLSTerm transformTerm(Iff iff, Logic2VampireLanguageMapperTrace trace, | ||
184 | Map<Variable, VLSVariable> variables) { | ||
185 | createVLSEquivalent => [ | ||
186 | left = iff.leftOperand.transformTerm(trace, variables) | ||
187 | right = iff.rightOperand.transformTerm(trace, variables) | ||
188 | ] | ||
189 | } | ||
190 | |||
191 | // def dispatch protected VLSTerm transformTerm(MoreThan moreThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
192 | // createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } | ||
193 | // def dispatch protected VLSTerm transformTerm(LessThan lessThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
194 | // createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } | ||
195 | // def dispatch protected VLSTerm transformTerm(MoreOrEqualThan moreThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
196 | // createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } | ||
197 | // def dispatch protected VLSTerm transformTerm(LessOrEqualThan lessThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
198 | // createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } | ||
199 | def dispatch protected VLSTerm transformTerm(Equals equals, Logic2VampireLanguageMapperTrace trace, | ||
200 | Map<Variable, VLSVariable> variables) { | ||
201 | createVLSEquality => [ | ||
202 | left = equals.leftOperand.transformTerm(trace, variables) | ||
203 | right = equals.rightOperand.transformTerm(trace, variables) | ||
204 | ] | ||
205 | } | ||
206 | |||
207 | def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
208 | support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } | ||
209 | // | ||
210 | // def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
211 | // createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] } | ||
212 | // def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
213 | // createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] } | ||
214 | // def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
215 | // createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] } | ||
216 | // def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
217 | // createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] } | ||
218 | // def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
219 | // createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] } | ||
220 | // | ||
221 | def dispatch protected VLSTerm transformTerm(Forall forall, Logic2VampireLanguageMapperTrace trace, | ||
222 | Map<Variable, VLSVariable> variables) { | ||
223 | support.createUniversallyQuantifiedExpression(this, forall, trace, variables) | ||
224 | } | ||
225 | |||
226 | def dispatch protected VLSTerm transformTerm(Exists exists, Logic2VampireLanguageMapperTrace trace, | ||
227 | Map<Variable, VLSVariable> variables) { | ||
228 | support.createExistentiallyQuantifiedExpression(this, exists, trace, variables) | ||
229 | } | ||
230 | |||
231 | def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
232 | return createVLSFunction => [ | ||
233 | it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name ) | ||
234 | it.terms += instanceOf.value.transformTerm(trace, variables) | ||
235 | ] | ||
236 | } | ||
237 | // | ||
238 | // def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
239 | // return this.relationMapper.transformTransitiveRelationReference( | ||
240 | // tc.relation, | ||
241 | // tc.leftOperand.transformTerm(trace,variables), | ||
242 | // tc.rightOperand.transformTerm(trace,variables), | ||
243 | // trace | ||
244 | // ) | ||
245 | // } | ||
246 | // | ||
247 | def dispatch protected VLSTerm transformTerm(SymbolicValue symbolicValue, Logic2VampireLanguageMapperTrace trace, | ||
248 | Map<Variable, VLSVariable> variables) { | ||
249 | symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions, trace, | ||
250 | variables) | ||
251 | } | ||
252 | |||
253 | def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, | ||
254 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
255 | Map<Variable, VLSVariable> variables) { | ||
256 | typeMapper.transformReference(referred, trace) | ||
257 | } | ||
258 | |||
259 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, | ||
260 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
261 | Map<Variable, VLSVariable> variables) { | ||
262 | // might need to make sure that only declared csts get transformed. see for Alloy | ||
263 | val res = createVLSConstant => [ | ||
264 | // ask if necessary VLSConstantDeclaration and not just directly strng | ||
265 | it.name = support.toID(constant.name) | ||
266 | ] | ||
267 | // no postprocessing cuz booleans are accepted | ||
268 | return res | ||
269 | } | ||
270 | |||
271 | // NOT NEEDED FOR NOW | ||
272 | // TODO | ||
273 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant, | ||
274 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
275 | Map<Variable, VLSVariable> variables) { | ||
276 | // val res = createVLSFunctionCall => [ | ||
277 | // it.referredDefinition = constant.lookup(trace.constantDefinition2Function) | ||
278 | // ] | ||
279 | // return support.postprocessResultOfSymbolicReference(constant.type,res,trace) | ||
280 | } | ||
281 | |||
282 | def dispatch protected VLSTerm transformSymbolicReference(Variable variable, | ||
283 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
284 | Map<Variable, VLSVariable> variables) { | ||
285 | |||
286 | // cannot treat variable as function (constant) because of name ID not being the same | ||
287 | // below does not work | ||
288 | val res = createVLSVariable => [ | ||
289 | // it.name = support.toIDMultiple("Var", variable.lookup(variables).name) | ||
290 | it.name = support.toID(variable.lookup(variables).name) | ||
291 | ] | ||
292 | // no need for potprocessing cuz booleans are supported | ||
293 | return res | ||
294 | } | ||
295 | |||
296 | // TODO | ||
297 | def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function, | ||
298 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
299 | Map<Variable, VLSVariable> variables) { | ||
300 | // if(trace.functionDefinitions.containsKey(function)) { | ||
301 | // return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) | ||
302 | // } else { | ||
303 | // if(functionMapper.transformedToHostedField(function,trace)) { | ||
304 | // val param = parameterSubstitutions.get(0).transformTerm(trace,variables) | ||
305 | // val res = createVLSJoin => [ | ||
306 | // leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace) | ||
307 | // rightOperand = createVLSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)] | ||
308 | // ] | ||
309 | // return support.postprocessResultOfSymbolicReference(function.range,res,trace) | ||
310 | // } else { | ||
311 | // val functionExpression = createVLSJoin=>[ | ||
312 | // leftOperand = createVLSReference => [referred = trace.logicLanguage] | ||
313 | // rightOperand = createVLSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)] | ||
314 | // ] | ||
315 | // val res = support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables) | ||
316 | // return support.postprocessResultOfSymbolicReference(function.range,res,trace) | ||
317 | // } | ||
318 | // } | ||
319 | } | ||
320 | |||
321 | // TODO | ||
322 | def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function, | ||
323 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
324 | Map<Variable, VLSVariable> variables) { | ||
325 | // val result = createVLSFunctionCall => [ | ||
326 | // it.referredDefinition = function.lookup(trace.functionDefinition2Function) | ||
327 | // it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] | ||
328 | // ] | ||
329 | // return support.postprocessResultOfSymbolicReference(function.range,result,trace) | ||
330 | } | ||
331 | |||
332 | // TODO | ||
333 | /* | ||
334 | def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | ||
335 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
336 | Map<Variable, VLSVariable> variables) { | ||
337 | if (trace.relationDefinitions.containsKey(relation)) { | ||
338 | this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), | ||
339 | parameterSubstitutions, trace, variables) | ||
340 | } | ||
341 | else { | ||
342 | // if (relationMapper.transformToHostedField(relation, trace)) { | ||
343 | // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) | ||
344 | // // R(a,b) => | ||
345 | // // b in a.R | ||
346 | // return createVLSSubset => [ | ||
347 | // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) | ||
348 | // it.rightOperand = createVLSJoin => [ | ||
349 | // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) | ||
350 | // it.rightOperand = createVLSReference => [it.referred = VLSRelation] | ||
351 | // ] | ||
352 | // ] | ||
353 | // } else { | ||
354 | // val target = createVLSJoin => [ | ||
355 | // leftOperand = createVLSReference => [referred = trace.logicLanguage] | ||
356 | // rightOperand = createVLSReference => [ | ||
357 | // referred = relation.lookup(trace.relationDeclaration2Global) | ||
358 | // ] | ||
359 | // ] | ||
360 | // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) | ||
361 | // | ||
362 | // return createVLSSubset => [ | ||
363 | // leftOperand = source | ||
364 | // rightOperand = target | ||
365 | // ] | ||
366 | // } | ||
367 | } | ||
368 | } | ||
369 | */ | ||
370 | |||
371 | // TODO | ||
372 | def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | ||
373 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
374 | Map<Variable, VLSVariable> variables) { | ||
375 | // createVLSFunction => [ | ||
376 | // it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) | ||
377 | // it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] | ||
378 | // ] | ||
379 | return createVLSFunction => [ | ||
380 | it.constant = support.toIDMultiple("rel", relation.name) | ||
381 | it.terms += parameterSubstitutions.map[p | p.transformTerm(trace,variables)] | ||
382 | ] | ||
383 | } | ||
384 | |||
385 | } | ||
386 | \ 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
13 | import java.util.HashMap | ||
14 | import java.util.Map | ||
15 | |||
16 | interface Logic2VampireLanguageMapper_TypeMapperTrace {} | ||
17 | |||
18 | class Logic2VampireLanguageMapperTrace { | ||
19 | // public var ViatraQueryEngine incQueryEngine; | ||
20 | |||
21 | //list of needed VLS components | ||
22 | public var VampireModel specification | ||
23 | public var VLSFofFormula logicLanguageBody | ||
24 | public var VLSTerm formula | ||
25 | //NOT NEEDED //public var VLSFunction constantDec | ||
26 | |||
27 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace | ||
28 | |||
29 | |||
30 | //NOT NEEDED //public val Map<ConstantDeclaration, VLSFunctionDeclaration> constantDeclaration2LanguageField = new HashMap | ||
31 | //public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap | ||
32 | |||
33 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | ||
34 | |||
35 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | ||
36 | public val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | ||
37 | public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap | ||
38 | |||
39 | } \ 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
6 | |||
7 | class Logic2VampireLanguageMapper_ConstantMapper { | ||
8 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
9 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
10 | val Logic2VampireLanguageMapper base | ||
11 | |||
12 | public new(Logic2VampireLanguageMapper base) { | ||
13 | this.base = base | ||
14 | } | ||
15 | |||
16 | //NOT NEEDED | ||
17 | // def protected dispatch transformConstant(ConstantDeclaration constant, Logic2VampireLanguageMapperTrace trace) { | ||
18 | // val c = createVLSFunctionDeclaration=> [ | ||
19 | // it.name = support.toID(constant.name) | ||
20 | // ] | ||
21 | // trace.constantDec.constant = c | ||
22 | // trace.constantDeclaration2LanguageField.put(constant, c); | ||
23 | // | ||
24 | // } | ||
25 | |||
26 | //NOT Used In Sample | ||
27 | def protected dispatch transformConstant(ConstantDefinition constant, Logic2VampireLanguageMapperTrace trace) { | ||
28 | //error | ||
29 | //TODO | ||
30 | // val c = createVLSFofFormula=> [ | ||
31 | // name = support.toID(constant.name) | ||
32 | // fofRole = "axiom" | ||
33 | // fofFormula = base.transformTypeReference() | ||
34 | // ] | ||
35 | } | ||
36 | |||
37 | def protected transformConstantDefinitionSpecification(ConstantDefinition constant, Logic2VampireLanguageMapperTrace trace) { | ||
38 | //TODO | ||
39 | } | ||
40 | |||
41 | |||
42 | } \ 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
11 | import java.util.ArrayList | ||
12 | import java.util.HashMap | ||
13 | import java.util.List | ||
14 | import java.util.Map | ||
15 | |||
16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
17 | |||
18 | class Logic2VampireLanguageMapper_RelationMapper { | ||
19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
20 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
21 | val Logic2VampireLanguageMapper base | ||
22 | |||
23 | public new(Logic2VampireLanguageMapper base) { | ||
24 | this.base = base | ||
25 | } | ||
26 | |||
27 | def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace) { | ||
28 | |||
29 | // 1. store all variables in support wrt their name | ||
30 | // 1.1 if variable has type, creating list of type declarations | ||
31 | val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | ||
32 | val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap | ||
33 | val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap | ||
34 | val typedefs = new ArrayList<VLSTerm> | ||
35 | for (variable : r.variables) { | ||
36 | val v = createVLSVariable => [ | ||
37 | it.name = support.toIDMultiple("Var", variable.name) | ||
38 | ] | ||
39 | relationVar2VLS.put(variable, v) | ||
40 | |||
41 | val varTypeComply = createVLSFunction => [ | ||
42 | it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | ||
43 | it.terms += createVLSVariable => [ | ||
44 | it.name = support.toIDMultiple("Var", variable.name) | ||
45 | ] | ||
46 | ] | ||
47 | relationVar2TypeDecComply.put(variable, varTypeComply) | ||
48 | |||
49 | val varTypeRes = createVLSFunction => [ | ||
50 | it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | ||
51 | it.terms += createVLSVariable => [ | ||
52 | it.name = support.toIDMultiple("Var", variable.name) | ||
53 | ] | ||
54 | ] | ||
55 | relationVar2TypeDecRes.put(variable, varTypeRes) | ||
56 | } | ||
57 | |||
58 | val comply = createVLSFofFormula => [ | ||
59 | it.name = support.toIDMultiple("compliance", r.name) | ||
60 | it.fofRole = "axiom" | ||
61 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
62 | for (variable : r.variables) { | ||
63 | val v = createVLSVariable => [ | ||
64 | it.name = variable.lookup(relationVar2VLS).name | ||
65 | ] | ||
66 | it.variables += v | ||
67 | |||
68 | } | ||
69 | it.operand = createVLSImplies => [ | ||
70 | it.left = createVLSFunction => [ | ||
71 | it.constant = support.toIDMultiple("rel", r.name) | ||
72 | for (variable : r.variables) { | ||
73 | val v = createVLSVariable => [ | ||
74 | it.name = variable.lookup(relationVar2VLS).name | ||
75 | ] | ||
76 | it.terms += v | ||
77 | } | ||
78 | ] | ||
79 | it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values)) | ||
80 | ] | ||
81 | ] | ||
82 | ] | ||
83 | |||
84 | val res = createVLSFofFormula => [ | ||
85 | it.name = support.toIDMultiple("relation", r.name) | ||
86 | it.fofRole = "axiom" | ||
87 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
88 | for (variable : r.variables) { | ||
89 | val v = createVLSVariable => [ | ||
90 | it.name = variable.lookup(relationVar2VLS).name | ||
91 | ] | ||
92 | it.variables += v | ||
93 | |||
94 | } | ||
95 | it.operand = createVLSImplies => [ | ||
96 | it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) | ||
97 | it.right = createVLSEquivalent => [ | ||
98 | it.left = createVLSFunction => [ | ||
99 | it.constant = support.toIDMultiple("rel", r.name) | ||
100 | for (variable : r.variables) { | ||
101 | val v = createVLSVariable => [ | ||
102 | it.name = variable.lookup(relationVar2VLS).name | ||
103 | ] | ||
104 | it.terms += v | ||
105 | |||
106 | } | ||
107 | ] | ||
108 | it.right = base.transformTerm(r.value, trace, relationVar2VLS) | ||
109 | ] | ||
110 | |||
111 | ] | ||
112 | |||
113 | ] | ||
114 | |||
115 | ] | ||
116 | |||
117 | // trace.relationDefinition2Predicate.put(r,res) | ||
118 | trace.specification.formulas += comply; | ||
119 | trace.specification.formulas += res; | ||
120 | |||
121 | } | ||
122 | |||
123 | def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) { | ||
124 | |||
125 | // 1. store all variables in support wrt their name | ||
126 | // 1.1 if variable has type, creating list of type declarations | ||
127 | val List<VLSVariable> relationVar2VLS = new ArrayList | ||
128 | val List<VLSFunction> relationVar2TypeDecComply = new ArrayList | ||
129 | val typedefs = new ArrayList<VLSTerm> | ||
130 | |||
131 | for (i : 0..<r.parameters.length) { | ||
132 | |||
133 | val v = createVLSVariable => [ | ||
134 | it.name = support.toIDMultiple("Var", i.toString) | ||
135 | ] | ||
136 | relationVar2VLS.add(v) | ||
137 | |||
138 | val varTypeComply = createVLSFunction => [ | ||
139 | it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name) | ||
140 | it.terms += createVLSVariable => [ | ||
141 | it.name = support.toIDMultiple("Var", i.toString) | ||
142 | ] | ||
143 | ] | ||
144 | relationVar2TypeDecComply.add(varTypeComply) | ||
145 | |||
146 | } | ||
147 | |||
148 | |||
149 | val comply = createVLSFofFormula => [ | ||
150 | it.name = support.toIDMultiple("compliance", r.name) | ||
151 | it.fofRole = "axiom" | ||
152 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
153 | |||
154 | for (i : 0..<r.parameters.length) { | ||
155 | val v = createVLSVariable => [ | ||
156 | it.name = relationVar2VLS.get(i).name | ||
157 | ] | ||
158 | it.variables += v | ||
159 | |||
160 | } | ||
161 | |||
162 | it.operand = createVLSImplies => [ | ||
163 | it.left = createVLSFunction => [ | ||
164 | it.constant = support.toIDMultiple("rel", r.name) | ||
165 | |||
166 | for (i : 0..<r.parameters.length) { | ||
167 | val v = createVLSVariable => [ | ||
168 | it.name = relationVar2VLS.get(i).name | ||
169 | ] | ||
170 | it.terms += v | ||
171 | } | ||
172 | |||
173 | ] | ||
174 | it.right = support.unfoldAnd(relationVar2TypeDecComply) | ||
175 | ] | ||
176 | ] | ||
177 | ] | ||
178 | |||
179 | // trace.relationDefinition2Predicate.put(r,res) | ||
180 | trace.specification.formulas += comply | ||
181 | } | ||
182 | |||
183 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
8 | import java.util.ArrayList | ||
9 | import java.util.HashMap | ||
10 | import java.util.List | ||
11 | import java.util.Map | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
13 | import org.eclipse.emf.common.util.EList | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
15 | |||
16 | class Logic2VampireLanguageMapper_Support { | ||
17 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
18 | |||
19 | // ID Handler | ||
20 | def protected String toIDMultiple(String... ids) { | ||
21 | ids.map[it.split("\\s+").join("_")].join("_") | ||
22 | } | ||
23 | |||
24 | def protected String toID(String ids) { | ||
25 | ids.split("\\s+").join("_") | ||
26 | } | ||
27 | |||
28 | // Support Functions | ||
29 | // booleans | ||
30 | // AND and OR | ||
31 | def protected VLSTerm unfoldAnd(List<? extends VLSTerm> operands) { | ||
32 | if (operands.size == 1) { | ||
33 | return operands.head | ||
34 | } else if (operands.size > 1) { | ||
35 | return createVLSAnd => [ | ||
36 | left = operands.head | ||
37 | right = operands.subList(1, operands.size).unfoldAnd | ||
38 | ] | ||
39 | } else | ||
40 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') | ||
41 | } | ||
42 | |||
43 | def protected VLSTerm unfoldOr(List<? extends VLSTerm> operands) { | ||
44 | |||
45 | // if(operands.size == 0) {basically return true} | ||
46 | /*else*/ if (operands.size == 1) { | ||
47 | return operands.head | ||
48 | } else if (operands.size > 1) { | ||
49 | return createVLSOr => [ | ||
50 | left = operands.head | ||
51 | right = operands.subList(1, operands.size).unfoldOr | ||
52 | ] | ||
53 | } else | ||
54 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP | ||
55 | } | ||
56 | |||
57 | def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands, | ||
58 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
59 | if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) } | ||
60 | else if(operands.size > 1) { | ||
61 | val notEquals = new ArrayList<VLSTerm>(operands.size*operands.size/2) | ||
62 | for(i:0..<operands.size) { | ||
63 | for(j: i+1..<operands.size) { | ||
64 | notEquals+=createVLSInequality=>[ | ||
65 | it.left= m.transformTerm(operands.get(i),trace,variables) | ||
66 | it.right = m.transformTerm(operands.get(j),trace,variables) | ||
67 | ] | ||
68 | } | ||
69 | } | ||
70 | return notEquals.unfoldAnd | ||
71 | } | ||
72 | else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') | ||
73 | } | ||
74 | |||
75 | // Symbolic | ||
76 | // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) { | ||
77 | // if(type instanceof BoolTypeReference) { | ||
78 | // return booleanToLogicValue(term ,trace) | ||
79 | // } | ||
80 | // else return term | ||
81 | // } | ||
82 | // def booleanToLogicValue(VLSTerm term, Logic2VampireLanguageMapperTrace trace) { | ||
83 | // throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
84 | // } | ||
85 | /* | ||
86 | * def protected String toID(List<String> ids) { | ||
87 | * ids.map[it.split("\\s+").join("'")].join("'") | ||
88 | * } | ||
89 | */ | ||
90 | // QUANTIFIERS + VARIABLES | ||
91 | def protected VLSTerm createUniversallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, | ||
92 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
93 | val variableMap = expression.quantifiedVariables.toInvertedMap [ v | | ||
94 | createVLSVariable => [it.name = toIDMultiple("Var", v.name)] | ||
95 | ] | ||
96 | |||
97 | val typedefs = new ArrayList<VLSTerm> | ||
98 | for (variable : expression.quantifiedVariables) { | ||
99 | val eq = createVLSFunction => [ | ||
100 | it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | ||
101 | it.terms += createVLSVariable => [ | ||
102 | it.name = toIDMultiple("Var", variable.name) | ||
103 | ] | ||
104 | |||
105 | ] | ||
106 | typedefs.add(eq) | ||
107 | } | ||
108 | |||
109 | |||
110 | createVLSUniversalQuantifier => [ | ||
111 | it.variables += variableMap.values | ||
112 | it.operand = createVLSImplies => [ | ||
113 | it.left = unfoldAnd(typedefs) | ||
114 | it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)) | ||
115 | ] | ||
116 | ] | ||
117 | } | ||
118 | |||
119 | def protected VLSTerm createExistentiallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, | ||
120 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
121 | val variableMap = expression.quantifiedVariables.toInvertedMap [ v | | ||
122 | createVLSVariable => [it.name = toIDMultiple("Var", v.name)] | ||
123 | ] | ||
124 | |||
125 | val typedefs = new ArrayList<VLSTerm> | ||
126 | for (variable : expression.quantifiedVariables) { | ||
127 | val eq = createVLSFunction => [ | ||
128 | it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | ||
129 | it.terms += createVLSVariable => [ | ||
130 | it.name = toIDMultiple("Var", variable.name) | ||
131 | ] | ||
132 | ] | ||
133 | typedefs.add(eq) | ||
134 | } | ||
135 | |||
136 | typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))) | ||
137 | createVLSExistentialQuantifier => [ | ||
138 | it.variables += variableMap.values | ||
139 | it.operand = unfoldAnd(typedefs) | ||
140 | |||
141 | ] | ||
142 | } | ||
143 | |||
144 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | ||
145 | new HashMap(map1) => [putAll(map2)] | ||
146 | } | ||
147 | |||
148 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import java.util.Collection | ||
6 | import java.util.List | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
8 | |||
9 | interface Logic2VampireLanguageMapper_TypeMapper { | ||
10 | def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace); | ||
11 | //samples below 2 lines | ||
12 | def List<VLSTerm> transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) | ||
13 | def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) | ||
14 | |||
15 | def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace) | ||
16 | def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace) | ||
17 | |||
18 | def VampireModelInterpretation_TypeInterpretation getTypeInterpreter() | ||
19 | } \ 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
8 | import java.util.ArrayList | ||
9 | import java.util.HashMap | ||
10 | import java.util.List | ||
11 | import java.util.Map | ||
12 | |||
13 | class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace{ | ||
14 | |||
15 | // public var VLSFofFormula objectSuperClass | ||
16 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; | ||
17 | public val Map<DefinedElement, VLSEquality> definedElement2Declaration = new HashMap //Not Yet Used | ||
18 | public val Map<Type, VLSTerm> type2PossibleNot = new HashMap | ||
19 | public val Map<Type, VLSTerm> type2And = new HashMap | ||
20 | |||
21 | } \ 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
10 | import java.util.ArrayList | ||
11 | import java.util.Collection | ||
12 | |||
13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
14 | |||
15 | class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { | ||
16 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
17 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
18 | |||
19 | new() { | ||
20 | LogicproblemPackage.eINSTANCE.class | ||
21 | } | ||
22 | |||
23 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, | ||
24 | Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { | ||
25 | val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes | ||
26 | trace.typeMapperTrace = typeTrace | ||
27 | |||
28 | val VLSVariable variable = createVLSVariable => [it.name = "A"] // did not work | ||
29 | // 1. store predicates for declarations in trace | ||
30 | for (type : types) { | ||
31 | val typePred = createVLSFunction => [ | ||
32 | it.constant = support.toIDMultiple("type", type.name) | ||
33 | it.terms += createVLSVariable => [it.name = variable.name] | ||
34 | ] | ||
35 | typeTrace.type2Predicate.put(type, typePred) | ||
36 | } | ||
37 | |||
38 | // 2. Map each type definition to fof formula | ||
39 | for (type : types.filter(TypeDefinition)) { | ||
40 | |||
41 | val res = createVLSFofFormula => [ | ||
42 | it.name = support.toIDMultiple("typeDef", type.name) | ||
43 | // below is temporary solution | ||
44 | it.fofRole = "axiom" | ||
45 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
46 | it.variables += createVLSVariable => [it.name = variable.name] | ||
47 | it.operand = createVLSEquivalent => [ | ||
48 | it.left = createVLSFunction => [ | ||
49 | it.constant = type.lookup(typeTrace.type2Predicate).constant | ||
50 | it.terms += createVLSVariable => [it.name = "A"] | ||
51 | ] | ||
52 | |||
53 | type.lookup(typeTrace.type2Predicate) | ||
54 | it.right = support.unfoldOr(type.elements.map [ e | | ||
55 | createVLSEquality => [ | ||
56 | it.left = createVLSVariable => [it.name = variable.name] | ||
57 | // it.right = createVLSDoubleQuote => [ | ||
58 | // it.value = "\"" + e.name + "\"" | ||
59 | // ] | ||
60 | it.right = createVLSDoubleQuote => [ | ||
61 | it.value = "\"a" + e.name + "\"" | ||
62 | ] | ||
63 | ] | ||
64 | ]) | ||
65 | ] | ||
66 | ] | ||
67 | |||
68 | ] | ||
69 | trace.specification.formulas += res | ||
70 | } | ||
71 | // 2.5. Currently allowing duplicate types. Not problematic cuz strings are by def unique | ||
72 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates | ||
73 | // and store in a map | ||
74 | // val List<VLSTerm> type2PossibleNot = new ArrayList | ||
75 | // val List<VLSTerm> type2And = new ArrayList | ||
76 | for (type : types.filter[!isIsAbstract]) { | ||
77 | for (type2 : types) { | ||
78 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes | ||
79 | if (type == type2 || dfsSupertypeCheck(type, type2)) { | ||
80 | typeTrace.type2PossibleNot.put(type2, createVLSFunction => [ | ||
81 | it.constant = type2.lookup(typeTrace.type2Predicate).constant | ||
82 | it.terms += createVLSVariable => [it.name = "A"] | ||
83 | ]) | ||
84 | } else { | ||
85 | typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [ | ||
86 | it.operand = createVLSFunction => [ | ||
87 | it.constant = type2.lookup(typeTrace.type2Predicate).constant | ||
88 | it.terms += createVLSVariable => [it.name = "A"] | ||
89 | ] | ||
90 | ]) | ||
91 | } | ||
92 | // typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate)) | ||
93 | } | ||
94 | typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values))) | ||
95 | // typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) ) | ||
96 | typeTrace.type2PossibleNot.clear | ||
97 | } | ||
98 | |||
99 | // 5. create fof function that is an or with all the elements in map | ||
100 | val hierarch = createVLSFofFormula => [ | ||
101 | it.name = "hierarchyHandler" | ||
102 | it.fofRole = "axiom" | ||
103 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
104 | it.variables += createVLSVariable => [it.name = "A"] | ||
105 | it.operand = createVLSEquivalent => [ | ||
106 | it.left = createVLSFunction => [ | ||
107 | it.constant = "Object" | ||
108 | it.terms += createVLSVariable => [ | ||
109 | it.name = "A" | ||
110 | ] | ||
111 | ] | ||
112 | it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values)) | ||
113 | ] | ||
114 | ] | ||
115 | ] | ||
116 | |||
117 | trace.specification.formulas += hierarch | ||
118 | } | ||
119 | |||
120 | def boolean dfsSupertypeCheck(Type type, Type type2) { | ||
121 | // There is surely a better way to do this | ||
122 | if (type.supertypes.isEmpty) | ||
123 | return false | ||
124 | else { | ||
125 | if (type.supertypes.contains(type2)) | ||
126 | return true | ||
127 | else { | ||
128 | for (supertype : type.supertypes) { | ||
129 | if(dfsSupertypeCheck(supertype, type2)) return true | ||
130 | } | ||
131 | } | ||
132 | } | ||
133 | } | ||
134 | |||
135 | override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, | ||
136 | Logic2VampireLanguageMapperTrace trace) { | ||
137 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
138 | } | ||
139 | |||
140 | override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) { | ||
141 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
142 | } | ||
143 | |||
144 | override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) { | ||
145 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
146 | } | ||
147 | |||
148 | override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { | ||
149 | createVLSDoubleQuote => [ | ||
150 | it.value = "\"a" + referred.name + "\"" | ||
151 | ] | ||
152 | } | ||
153 | |||
154 | override getTypeInterpreter() { | ||
155 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
156 | } | ||
157 | |||
158 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | interface VampireModelInterpretation_TypeInterpretation { | ||
4 | |||
5 | } \ 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation { | ||
4 | //TODO | ||
5 | } \ No newline at end of file | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin new file mode 100644 index 00000000..e8e82269 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin new file mode 100644 index 00000000..dee2a0a8 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore new file mode 100644 index 00000000..9efd2ac5 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore | |||
@@ -0,0 +1,4 @@ | |||
1 | /.VampireSolver.java._trace | ||
2 | /.TypeMappingTechnique.java._trace | ||
3 | /.VampireBackendSolver.java._trace | ||
4 | /.VampireSolverConfiguration.java._trace | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java new file mode 100644 index 00000000..8ffba2f1 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java | |||
@@ -0,0 +1,6 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public enum TypeMappingTechnique { | ||
5 | FilteredTypes; | ||
6 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java new file mode 100644 index 00000000..91e9bed0 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java | |||
@@ -0,0 +1,5 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public enum VampireBackendSolver { | ||
5 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java new file mode 100644 index 00000000..81cae109 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java | |||
@@ -0,0 +1,80 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup; | ||
4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | ||
19 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | ||
20 | import java.io.PrintWriter; | ||
21 | import java.util.List; | ||
22 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
23 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
24 | |||
25 | @SuppressWarnings("all") | ||
26 | public class VampireSolver extends LogicReasoner { | ||
27 | public VampireSolver() { | ||
28 | VampireLanguagePackage.eINSTANCE.eClass(); | ||
29 | final VampireLanguageStandaloneSetupGenerated x = new VampireLanguageStandaloneSetupGenerated(); | ||
30 | VampireLanguageStandaloneSetup.doSetup(); | ||
31 | } | ||
32 | |||
33 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); | ||
34 | |||
35 | private final String fileName = "problem.tptp"; | ||
36 | |||
37 | @Override | ||
38 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration configuration, final ReasonerWorkspace workspace) throws LogicReasonerException { | ||
39 | try { | ||
40 | final VampireSolverConfiguration vampireConfig = this.asConfig(configuration); | ||
41 | final long transformationStart = System.currentTimeMillis(); | ||
42 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | ||
43 | final VampireModel vampireProblem = result.getOutput(); | ||
44 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | ||
45 | String fileURI = null; | ||
46 | String vampireCode = null; | ||
47 | if (vampireConfig.writeToFile) { | ||
48 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); | ||
49 | } else { | ||
50 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); | ||
51 | } | ||
52 | long _currentTimeMillis = System.currentTimeMillis(); | ||
53 | final long transformationTime = (_currentTimeMillis - transformationStart); | ||
54 | final PrintWriter out = new PrintWriter("output/files/vampireCode.tptp"); | ||
55 | out.println(vampireCode); | ||
56 | out.close(); | ||
57 | return null; | ||
58 | } catch (Throwable _e) { | ||
59 | throw Exceptions.sneakyThrow(_e); | ||
60 | } | ||
61 | } | ||
62 | |||
63 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | ||
64 | if ((configuration instanceof VampireSolverConfiguration)) { | ||
65 | return ((VampireSolverConfiguration)configuration); | ||
66 | } else { | ||
67 | StringConcatenation _builder = new StringConcatenation(); | ||
68 | _builder.append("The configuration have to be an "); | ||
69 | String _simpleName = VampireSolverConfiguration.class.getSimpleName(); | ||
70 | _builder.append(_simpleName); | ||
71 | _builder.append("!"); | ||
72 | throw new IllegalArgumentException(_builder.toString()); | ||
73 | } | ||
74 | } | ||
75 | |||
76 | @Override | ||
77 | public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) { | ||
78 | return null; | ||
79 | } | ||
80 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java new file mode 100644 index 00000000..d392016e --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java | |||
@@ -0,0 +1,10 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner; | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
4 | |||
5 | @SuppressWarnings("all") | ||
6 | public class VampireSolverConfiguration extends LogicSolverConfiguration { | ||
7 | public int symmetry = 0; | ||
8 | |||
9 | public boolean writeToFile = false; | ||
10 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin new file mode 100644 index 00000000..10edee94 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin new file mode 100644 index 00000000..50c1d625 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin new file mode 100644 index 00000000..f331beac --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin new file mode 100644 index 00000000..e929e637 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin new file mode 100644 index 00000000..cc7aea7c --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin new file mode 100644 index 00000000..1b6cf5d1 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin new file mode 100644 index 00000000..7a4d5bc7 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin new file mode 100644 index 00000000..7b6b2f9a --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin new file mode 100644 index 00000000..f8b3c54e --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin new file mode 100644 index 00000000..52b870a3 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore new file mode 100644 index 00000000..d27ff186 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore | |||
@@ -0,0 +1,11 @@ | |||
1 | /.Logic2VampireLanguageMapper_ConstantMapper.java._trace | ||
2 | /.Logic2VampireLanguageMapper.java._trace | ||
3 | /.Logic2VampireLanguageMapperTrace.java._trace | ||
4 | /.Logic2VampireLanguageMapper_TypeMapperTrace.java._trace | ||
5 | /.VampireModelInterpretation_TypeInterpretation.java._trace | ||
6 | /.VampireModelInterpretation_TypeInterpretation_FilteredTypes.java._trace | ||
7 | /.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java._trace | ||
8 | /.Logic2VampireLanguageMapper_TypeMapper.java._trace | ||
9 | /.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java._trace | ||
10 | /.Logic2VampireLanguageMapper_Support.java._trace | ||
11 | /.Logic2VampireLanguageMapper_RelationMapper.java._trace | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java new file mode 100644 index 00000000..390a6b10 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java | |||
@@ -0,0 +1,442 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
20 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
23 | import com.google.common.collect.Iterables; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference; | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct; | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals; | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall; | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration; | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition; | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl; | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf; | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral; | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral; | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
54 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
55 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
56 | import java.util.Arrays; | ||
57 | import java.util.Collections; | ||
58 | import java.util.HashMap; | ||
59 | import java.util.List; | ||
60 | import java.util.Map; | ||
61 | import java.util.function.Consumer; | ||
62 | import org.eclipse.emf.common.util.EList; | ||
63 | import org.eclipse.xtend.lib.annotations.AccessorType; | ||
64 | import org.eclipse.xtend.lib.annotations.Accessors; | ||
65 | import org.eclipse.xtext.xbase.lib.Extension; | ||
66 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
67 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
68 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
69 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
70 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
71 | import org.eclipse.xtext.xbase.lib.Pure; | ||
72 | |||
73 | @SuppressWarnings("all") | ||
74 | public class Logic2VampireLanguageMapper { | ||
75 | @Extension | ||
76 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
77 | |||
78 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
79 | |||
80 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
81 | private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); | ||
82 | |||
83 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
84 | private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); | ||
85 | |||
86 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
87 | private final Logic2VampireLanguageMapper_TypeMapper typeMapper; | ||
88 | |||
89 | public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) { | ||
90 | this.typeMapper = typeMapper; | ||
91 | } | ||
92 | |||
93 | public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration configuration) { | ||
94 | VLSComment _createVLSComment = this.factory.createVLSComment(); | ||
95 | final Procedure1<VLSComment> _function = (VLSComment it) -> { | ||
96 | it.setComment("%This is an initial Test Comment \r"); | ||
97 | }; | ||
98 | final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function); | ||
99 | VampireModel _createVampireModel = this.factory.createVampireModel(); | ||
100 | final Procedure1<VampireModel> _function_1 = (VampireModel it) -> { | ||
101 | EList<VLSComment> _comments = it.getComments(); | ||
102 | _comments.add(initialComment); | ||
103 | }; | ||
104 | final VampireModel specification = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1); | ||
105 | Logic2VampireLanguageMapperTrace _logic2VampireLanguageMapperTrace = new Logic2VampireLanguageMapperTrace(); | ||
106 | final Procedure1<Logic2VampireLanguageMapperTrace> _function_2 = (Logic2VampireLanguageMapperTrace it) -> { | ||
107 | it.specification = specification; | ||
108 | }; | ||
109 | final Logic2VampireLanguageMapperTrace trace = ObjectExtensions.<Logic2VampireLanguageMapperTrace>operator_doubleArrow(_logic2VampireLanguageMapperTrace, _function_2); | ||
110 | boolean _isEmpty = problem.getTypes().isEmpty(); | ||
111 | boolean _not = (!_isEmpty); | ||
112 | if (_not) { | ||
113 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); | ||
114 | } | ||
115 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | ||
116 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | ||
117 | final Consumer<Relation> _function_3 = (Relation it) -> { | ||
118 | this.relationMapper.transformRelation(it, trace); | ||
119 | }; | ||
120 | problem.getRelations().forEach(_function_3); | ||
121 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { | ||
122 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); | ||
123 | }; | ||
124 | Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_4); | ||
125 | EList<Assertion> _assertions = problem.getAssertions(); | ||
126 | for (final Assertion assertion : _assertions) { | ||
127 | this.transformAssertion(assertion, trace); | ||
128 | } | ||
129 | return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace); | ||
130 | } | ||
131 | |||
132 | protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { | ||
133 | return null; | ||
134 | } | ||
135 | |||
136 | private HashMap<ConstantDeclaration, ConstantDefinition> collectConstantDefinitions(final LogicProblem problem) { | ||
137 | final HashMap<ConstantDeclaration, ConstantDefinition> res = new HashMap<ConstantDeclaration, ConstantDefinition>(); | ||
138 | final Function1<ConstantDefinition, Boolean> _function = (ConstantDefinition it) -> { | ||
139 | ConstantDeclaration _defines = it.getDefines(); | ||
140 | return Boolean.valueOf((_defines != null)); | ||
141 | }; | ||
142 | final Consumer<ConstantDefinition> _function_1 = (ConstantDefinition it) -> { | ||
143 | res.put(it.getDefines(), it); | ||
144 | }; | ||
145 | IterableExtensions.<ConstantDefinition>filter(Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class), _function).forEach(_function_1); | ||
146 | return res; | ||
147 | } | ||
148 | |||
149 | private HashMap<RelationDeclaration, RelationDefinition> collectRelationDefinitions(final LogicProblem problem) { | ||
150 | final HashMap<RelationDeclaration, RelationDefinition> res = new HashMap<RelationDeclaration, RelationDefinition>(); | ||
151 | final Function1<RelationDefinition, Boolean> _function = (RelationDefinition it) -> { | ||
152 | RelationDeclaration _defines = it.getDefines(); | ||
153 | return Boolean.valueOf((_defines != null)); | ||
154 | }; | ||
155 | final Consumer<RelationDefinition> _function_1 = (RelationDefinition it) -> { | ||
156 | res.put(it.getDefines(), it); | ||
157 | }; | ||
158 | IterableExtensions.<RelationDefinition>filter(Iterables.<RelationDefinition>filter(problem.getRelations(), RelationDefinition.class), _function).forEach(_function_1); | ||
159 | return res; | ||
160 | } | ||
161 | |||
162 | protected boolean transformAssertion(final Assertion assertion, final Logic2VampireLanguageMapperTrace trace) { | ||
163 | boolean _xblockexpression = false; | ||
164 | { | ||
165 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
166 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
167 | it.setName(this.support.toID(assertion.getName())); | ||
168 | it.setFofRole("axiom"); | ||
169 | it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); | ||
170 | }; | ||
171 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
172 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
173 | _xblockexpression = _formulas.add(res); | ||
174 | } | ||
175 | return _xblockexpression; | ||
176 | } | ||
177 | |||
178 | protected VLSTerm _transformTerm(final BoolLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
179 | VLSTerm _xifexpression = null; | ||
180 | boolean _isValue = literal.isValue(); | ||
181 | boolean _equals = (_isValue == true); | ||
182 | if (_equals) { | ||
183 | _xifexpression = this.factory.createVLSTrue(); | ||
184 | } else { | ||
185 | _xifexpression = this.factory.createVLSFalse(); | ||
186 | } | ||
187 | return _xifexpression; | ||
188 | } | ||
189 | |||
190 | protected VLSTerm _transformTerm(final IntLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
191 | VLSInt _createVLSInt = this.factory.createVLSInt(); | ||
192 | final Procedure1<VLSInt> _function = (VLSInt it) -> { | ||
193 | it.setValue(Integer.valueOf(literal.getValue()).toString()); | ||
194 | }; | ||
195 | return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function); | ||
196 | } | ||
197 | |||
198 | protected VLSTerm _transformTerm(final RealLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
199 | VLSReal _createVLSReal = this.factory.createVLSReal(); | ||
200 | final Procedure1<VLSReal> _function = (VLSReal it) -> { | ||
201 | it.setValue(literal.getValue().toString()); | ||
202 | }; | ||
203 | return ObjectExtensions.<VLSReal>operator_doubleArrow(_createVLSReal, _function); | ||
204 | } | ||
205 | |||
206 | protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
207 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
208 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { | ||
209 | it.setOperand(this.transformTerm(not.getOperand(), trace, variables)); | ||
210 | }; | ||
211 | return ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function); | ||
212 | } | ||
213 | |||
214 | protected VLSTerm _transformTerm(final And and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
215 | final Function1<Term, VLSTerm> _function = (Term it) -> { | ||
216 | return this.transformTerm(it, trace, variables); | ||
217 | }; | ||
218 | return this.support.unfoldAnd(ListExtensions.<Term, VLSTerm>map(and.getOperands(), _function)); | ||
219 | } | ||
220 | |||
221 | protected VLSTerm _transformTerm(final Or or, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
222 | final Function1<Term, VLSTerm> _function = (Term it) -> { | ||
223 | return this.transformTerm(it, trace, variables); | ||
224 | }; | ||
225 | return this.support.unfoldOr(ListExtensions.<Term, VLSTerm>map(or.getOperands(), _function)); | ||
226 | } | ||
227 | |||
228 | protected VLSTerm _transformTerm(final Impl impl, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
229 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
230 | final Procedure1<VLSImplies> _function = (VLSImplies it) -> { | ||
231 | it.setLeft(this.transformTerm(impl.getLeftOperand(), trace, variables)); | ||
232 | it.setRight(this.transformTerm(impl.getRightOperand(), trace, variables)); | ||
233 | }; | ||
234 | return ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function); | ||
235 | } | ||
236 | |||
237 | protected VLSTerm _transformTerm(final Iff iff, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
238 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
239 | final Procedure1<VLSEquivalent> _function = (VLSEquivalent it) -> { | ||
240 | it.setLeft(this.transformTerm(iff.getLeftOperand(), trace, variables)); | ||
241 | it.setRight(this.transformTerm(iff.getRightOperand(), trace, variables)); | ||
242 | }; | ||
243 | return ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function); | ||
244 | } | ||
245 | |||
246 | protected VLSTerm _transformTerm(final Equals equals, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
247 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
248 | final Procedure1<VLSEquality> _function = (VLSEquality it) -> { | ||
249 | it.setLeft(this.transformTerm(equals.getLeftOperand(), trace, variables)); | ||
250 | it.setRight(this.transformTerm(equals.getRightOperand(), trace, variables)); | ||
251 | }; | ||
252 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function); | ||
253 | } | ||
254 | |||
255 | protected VLSTerm _transformTerm(final Distinct distinct, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
256 | return this.support.unfoldDistinctTerms(this, distinct.getOperands(), trace, variables); | ||
257 | } | ||
258 | |||
259 | protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
260 | return this.support.createUniversallyQuantifiedExpression(this, forall, trace, variables); | ||
261 | } | ||
262 | |||
263 | protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
264 | return this.support.createExistentiallyQuantifiedExpression(this, exists, trace, variables); | ||
265 | } | ||
266 | |||
267 | protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
268 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
269 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
270 | TypeReference _range = instanceOf.getRange(); | ||
271 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | ||
272 | EList<VLSTerm> _terms = it.getTerms(); | ||
273 | VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); | ||
274 | _terms.add(_transformTerm); | ||
275 | }; | ||
276 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
277 | } | ||
278 | |||
279 | protected VLSTerm _transformTerm(final SymbolicValue symbolicValue, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
280 | return this.transformSymbolicReference(symbolicValue.getSymbolicReference(), symbolicValue.getParameterSubstitutions(), trace, variables); | ||
281 | } | ||
282 | |||
283 | protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
284 | return this.typeMapper.transformReference(referred, trace); | ||
285 | } | ||
286 | |||
287 | protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
288 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
289 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
290 | it.setName(this.support.toID(constant.getName())); | ||
291 | }; | ||
292 | final VLSConstant res = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
293 | return res; | ||
294 | } | ||
295 | |||
296 | protected VLSTerm _transformSymbolicReference(final ConstantDefinition constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
297 | return null; | ||
298 | } | ||
299 | |||
300 | protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
301 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
302 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
303 | it.setName(this.support.toID(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables).getName())); | ||
304 | }; | ||
305 | final VLSVariable res = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
306 | return res; | ||
307 | } | ||
308 | |||
309 | protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
310 | return null; | ||
311 | } | ||
312 | |||
313 | protected VLSTerm _transformSymbolicReference(final FunctionDefinition function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
314 | return null; | ||
315 | } | ||
316 | |||
317 | /** | ||
318 | * def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | ||
319 | * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
320 | * Map<Variable, VLSVariable> variables) { | ||
321 | * if (trace.relationDefinitions.containsKey(relation)) { | ||
322 | * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), | ||
323 | * parameterSubstitutions, trace, variables) | ||
324 | * } | ||
325 | * else { | ||
326 | * // if (relationMapper.transformToHostedField(relation, trace)) { | ||
327 | * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) | ||
328 | * // // R(a,b) => | ||
329 | * // // b in a.R | ||
330 | * // return createVLSSubset => [ | ||
331 | * // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) | ||
332 | * // it.rightOperand = createVLSJoin => [ | ||
333 | * // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) | ||
334 | * // it.rightOperand = createVLSReference => [it.referred = VLSRelation] | ||
335 | * // ] | ||
336 | * // ] | ||
337 | * // } else { | ||
338 | * // val target = createVLSJoin => [ | ||
339 | * // leftOperand = createVLSReference => [referred = trace.logicLanguage] | ||
340 | * // rightOperand = createVLSReference => [ | ||
341 | * // referred = relation.lookup(trace.relationDeclaration2Global) | ||
342 | * // ] | ||
343 | * // ] | ||
344 | * // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) | ||
345 | * // | ||
346 | * // return createVLSSubset => [ | ||
347 | * // leftOperand = source | ||
348 | * // rightOperand = target | ||
349 | * // ] | ||
350 | * // } | ||
351 | * } | ||
352 | * } | ||
353 | */ | ||
354 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
355 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
356 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
357 | it.setConstant(this.support.toIDMultiple("rel", relation.getName())); | ||
358 | EList<VLSTerm> _terms = it.getTerms(); | ||
359 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { | ||
360 | return this.transformTerm(p, trace, variables); | ||
361 | }; | ||
362 | List<VLSTerm> _map = ListExtensions.<Term, VLSTerm>map(parameterSubstitutions, _function_1); | ||
363 | Iterables.<VLSTerm>addAll(_terms, _map); | ||
364 | }; | ||
365 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
366 | } | ||
367 | |||
368 | protected VLSTerm transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { | ||
369 | return _transformTypeReference(boolTypeReference, trace); | ||
370 | } | ||
371 | |||
372 | protected VLSTerm transformTerm(final Term and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
373 | if (and instanceof And) { | ||
374 | return _transformTerm((And)and, trace, variables); | ||
375 | } else if (and instanceof BoolLiteral) { | ||
376 | return _transformTerm((BoolLiteral)and, trace, variables); | ||
377 | } else if (and instanceof Distinct) { | ||
378 | return _transformTerm((Distinct)and, trace, variables); | ||
379 | } else if (and instanceof Equals) { | ||
380 | return _transformTerm((Equals)and, trace, variables); | ||
381 | } else if (and instanceof Exists) { | ||
382 | return _transformTerm((Exists)and, trace, variables); | ||
383 | } else if (and instanceof Forall) { | ||
384 | return _transformTerm((Forall)and, trace, variables); | ||
385 | } else if (and instanceof Iff) { | ||
386 | return _transformTerm((Iff)and, trace, variables); | ||
387 | } else if (and instanceof Impl) { | ||
388 | return _transformTerm((Impl)and, trace, variables); | ||
389 | } else if (and instanceof IntLiteral) { | ||
390 | return _transformTerm((IntLiteral)and, trace, variables); | ||
391 | } else if (and instanceof Not) { | ||
392 | return _transformTerm((Not)and, trace, variables); | ||
393 | } else if (and instanceof Or) { | ||
394 | return _transformTerm((Or)and, trace, variables); | ||
395 | } else if (and instanceof RealLiteral) { | ||
396 | return _transformTerm((RealLiteral)and, trace, variables); | ||
397 | } else if (and instanceof InstanceOf) { | ||
398 | return _transformTerm((InstanceOf)and, trace, variables); | ||
399 | } else if (and instanceof SymbolicValue) { | ||
400 | return _transformTerm((SymbolicValue)and, trace, variables); | ||
401 | } else { | ||
402 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
403 | Arrays.<Object>asList(and, trace, variables).toString()); | ||
404 | } | ||
405 | } | ||
406 | |||
407 | protected VLSTerm transformSymbolicReference(final SymbolicDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
408 | if (constant instanceof ConstantDeclaration) { | ||
409 | return _transformSymbolicReference((ConstantDeclaration)constant, parameterSubstitutions, trace, variables); | ||
410 | } else if (constant instanceof ConstantDefinition) { | ||
411 | return _transformSymbolicReference((ConstantDefinition)constant, parameterSubstitutions, trace, variables); | ||
412 | } else if (constant instanceof FunctionDeclaration) { | ||
413 | return _transformSymbolicReference((FunctionDeclaration)constant, parameterSubstitutions, trace, variables); | ||
414 | } else if (constant instanceof FunctionDefinition) { | ||
415 | return _transformSymbolicReference((FunctionDefinition)constant, parameterSubstitutions, trace, variables); | ||
416 | } else if (constant instanceof DefinedElement) { | ||
417 | return _transformSymbolicReference((DefinedElement)constant, parameterSubstitutions, trace, variables); | ||
418 | } else if (constant instanceof Relation) { | ||
419 | return _transformSymbolicReference((Relation)constant, parameterSubstitutions, trace, variables); | ||
420 | } else if (constant instanceof Variable) { | ||
421 | return _transformSymbolicReference((Variable)constant, parameterSubstitutions, trace, variables); | ||
422 | } else { | ||
423 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
424 | Arrays.<Object>asList(constant, parameterSubstitutions, trace, variables).toString()); | ||
425 | } | ||
426 | } | ||
427 | |||
428 | @Pure | ||
429 | public Logic2VampireLanguageMapper_ConstantMapper getConstantMapper() { | ||
430 | return this.constantMapper; | ||
431 | } | ||
432 | |||
433 | @Pure | ||
434 | public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { | ||
435 | return this.relationMapper; | ||
436 | } | ||
437 | |||
438 | @Pure | ||
439 | public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() { | ||
440 | return this.typeMapper; | ||
441 | } | ||
442 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java new file mode 100644 index 00000000..855815f8 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java | |||
@@ -0,0 +1,34 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
14 | import java.util.HashMap; | ||
15 | import java.util.Map; | ||
16 | |||
17 | @SuppressWarnings("all") | ||
18 | public class Logic2VampireLanguageMapperTrace { | ||
19 | public VampireModel specification; | ||
20 | |||
21 | public VLSFofFormula logicLanguageBody; | ||
22 | |||
23 | public VLSTerm formula; | ||
24 | |||
25 | public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; | ||
26 | |||
27 | public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions; | ||
28 | |||
29 | public Map<RelationDeclaration, RelationDefinition> relationDefinitions; | ||
30 | |||
31 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
32 | |||
33 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); | ||
34 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java new file mode 100644 index 00000000..e5f42e73 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java | |||
@@ -0,0 +1,34 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
8 | import org.eclipse.xtext.xbase.lib.Extension; | ||
9 | |||
10 | @SuppressWarnings("all") | ||
11 | public class Logic2VampireLanguageMapper_ConstantMapper { | ||
12 | @Extension | ||
13 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
14 | |||
15 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
16 | |||
17 | private final Logic2VampireLanguageMapper base; | ||
18 | |||
19 | public Logic2VampireLanguageMapper_ConstantMapper(final Logic2VampireLanguageMapper base) { | ||
20 | this.base = base; | ||
21 | } | ||
22 | |||
23 | protected Object _transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { | ||
24 | return null; | ||
25 | } | ||
26 | |||
27 | protected Object transformConstantDefinitionSpecification(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { | ||
28 | return null; | ||
29 | } | ||
30 | |||
31 | protected Object transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { | ||
32 | return _transformConstant(constant, trace); | ||
33 | } | ||
34 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java new file mode 100644 index 00000000..561402a7 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | |||
@@ -0,0 +1,296 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
20 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
21 | import java.util.ArrayList; | ||
22 | import java.util.Arrays; | ||
23 | import java.util.Collection; | ||
24 | import java.util.HashMap; | ||
25 | import java.util.List; | ||
26 | import java.util.Map; | ||
27 | import org.eclipse.emf.common.util.EList; | ||
28 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
29 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
30 | import org.eclipse.xtext.xbase.lib.Extension; | ||
31 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
32 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
33 | |||
34 | @SuppressWarnings("all") | ||
35 | public class Logic2VampireLanguageMapper_RelationMapper { | ||
36 | @Extension | ||
37 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
38 | |||
39 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
40 | |||
41 | private final Logic2VampireLanguageMapper base; | ||
42 | |||
43 | public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) { | ||
44 | this.base = base; | ||
45 | } | ||
46 | |||
47 | public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace) { | ||
48 | final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
49 | final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>(); | ||
50 | final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>(); | ||
51 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
52 | EList<Variable> _variables = r.getVariables(); | ||
53 | for (final Variable variable : _variables) { | ||
54 | { | ||
55 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
56 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
57 | it.setName(this.support.toIDMultiple("Var", variable.getName())); | ||
58 | }; | ||
59 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
60 | relationVar2VLS.put(variable, v); | ||
61 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
62 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
63 | TypeReference _range = variable.getRange(); | ||
64 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | ||
65 | EList<VLSTerm> _terms = it.getTerms(); | ||
66 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
67 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
68 | it_1.setName(this.support.toIDMultiple("Var", variable.getName())); | ||
69 | }; | ||
70 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
71 | _terms.add(_doubleArrow); | ||
72 | }; | ||
73 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
74 | relationVar2TypeDecComply.put(variable, varTypeComply); | ||
75 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); | ||
76 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { | ||
77 | TypeReference _range = variable.getRange(); | ||
78 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | ||
79 | EList<VLSTerm> _terms = it.getTerms(); | ||
80 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
81 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> { | ||
82 | it_1.setName(this.support.toIDMultiple("Var", variable.getName())); | ||
83 | }; | ||
84 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3); | ||
85 | _terms.add(_doubleArrow); | ||
86 | }; | ||
87 | final VLSFunction varTypeRes = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_2); | ||
88 | relationVar2TypeDecRes.put(variable, varTypeRes); | ||
89 | } | ||
90 | } | ||
91 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
92 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
93 | it.setName(this.support.toIDMultiple("compliance", r.getName())); | ||
94 | it.setFofRole("axiom"); | ||
95 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
96 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
97 | EList<Variable> _variables_1 = r.getVariables(); | ||
98 | for (final Variable variable_1 : _variables_1) { | ||
99 | { | ||
100 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
101 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> { | ||
102 | it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName()); | ||
103 | }; | ||
104 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
105 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
106 | _variables_2.add(v); | ||
107 | } | ||
108 | } | ||
109 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
110 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
111 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
112 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
113 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | ||
114 | EList<Variable> _variables_2 = r.getVariables(); | ||
115 | for (final Variable variable_2 : _variables_2) { | ||
116 | { | ||
117 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
118 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
119 | it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
120 | }; | ||
121 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
122 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
123 | _terms.add(v); | ||
124 | } | ||
125 | } | ||
126 | }; | ||
127 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
128 | it_2.setLeft(_doubleArrow); | ||
129 | Collection<VLSFunction> _values = relationVar2TypeDecComply.values(); | ||
130 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
131 | it_2.setRight(this.support.unfoldAnd(_arrayList)); | ||
132 | }; | ||
133 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
134 | it_1.setOperand(_doubleArrow); | ||
135 | }; | ||
136 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
137 | it.setFofFormula(_doubleArrow); | ||
138 | }; | ||
139 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
140 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
141 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
142 | it.setName(this.support.toIDMultiple("relation", r.getName())); | ||
143 | it.setFofRole("axiom"); | ||
144 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
145 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
146 | EList<Variable> _variables_1 = r.getVariables(); | ||
147 | for (final Variable variable_1 : _variables_1) { | ||
148 | { | ||
149 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
150 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> { | ||
151 | it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName()); | ||
152 | }; | ||
153 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3); | ||
154 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
155 | _variables_2.add(v); | ||
156 | } | ||
157 | } | ||
158 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
159 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
160 | Collection<VLSFunction> _values = relationVar2TypeDecRes.values(); | ||
161 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
162 | it_2.setLeft(this.support.unfoldAnd(_arrayList)); | ||
163 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
164 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> { | ||
165 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
166 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> { | ||
167 | it_4.setConstant(this.support.toIDMultiple("rel", r.getName())); | ||
168 | EList<Variable> _variables_2 = r.getVariables(); | ||
169 | for (final Variable variable_2 : _variables_2) { | ||
170 | { | ||
171 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
172 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_5) -> { | ||
173 | it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
174 | }; | ||
175 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); | ||
176 | EList<VLSTerm> _terms = it_4.getTerms(); | ||
177 | _terms.add(v); | ||
178 | } | ||
179 | } | ||
180 | }; | ||
181 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | ||
182 | it_3.setLeft(_doubleArrow); | ||
183 | it_3.setRight(this.base.transformTerm(r.getValue(), trace, relationVar2VLS)); | ||
184 | }; | ||
185 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
186 | it_2.setRight(_doubleArrow); | ||
187 | }; | ||
188 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
189 | it_1.setOperand(_doubleArrow); | ||
190 | }; | ||
191 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
192 | it.setFofFormula(_doubleArrow); | ||
193 | }; | ||
194 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_1); | ||
195 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
196 | _formulas.add(comply); | ||
197 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
198 | _formulas_1.add(res); | ||
199 | } | ||
200 | |||
201 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { | ||
202 | final List<VLSVariable> relationVar2VLS = new ArrayList<VLSVariable>(); | ||
203 | final List<VLSFunction> relationVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
204 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
205 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
206 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
207 | for (final Integer i : _doubleDotLessThan) { | ||
208 | { | ||
209 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
210 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
211 | it.setName(this.support.toIDMultiple("Var", i.toString())); | ||
212 | }; | ||
213 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
214 | relationVar2VLS.add(v); | ||
215 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
216 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
217 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
218 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _get).getReferred().getName())); | ||
219 | EList<VLSTerm> _terms = it.getTerms(); | ||
220 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
221 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
222 | it_1.setName(this.support.toIDMultiple("Var", i.toString())); | ||
223 | }; | ||
224 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
225 | _terms.add(_doubleArrow); | ||
226 | }; | ||
227 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
228 | relationVar2TypeDecComply.add(varTypeComply); | ||
229 | } | ||
230 | } | ||
231 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
232 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
233 | it.setName(this.support.toIDMultiple("compliance", r.getName())); | ||
234 | it.setFofRole("axiom"); | ||
235 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
236 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
237 | int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
238 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); | ||
239 | for (final Integer i_1 : _doubleDotLessThan_1) { | ||
240 | { | ||
241 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
242 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> { | ||
243 | it_2.setName(relationVar2VLS.get((i_1).intValue()).getName()); | ||
244 | }; | ||
245 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
246 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
247 | _variables.add(v); | ||
248 | } | ||
249 | } | ||
250 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
251 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
252 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
253 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
254 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | ||
255 | int _length_2 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
256 | ExclusiveRange _doubleDotLessThan_2 = new ExclusiveRange(0, _length_2, true); | ||
257 | for (final Integer i_2 : _doubleDotLessThan_2) { | ||
258 | { | ||
259 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
260 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
261 | it_4.setName(relationVar2VLS.get((i_2).intValue()).getName()); | ||
262 | }; | ||
263 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
264 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
265 | _terms.add(v); | ||
266 | } | ||
267 | } | ||
268 | }; | ||
269 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
270 | it_2.setLeft(_doubleArrow); | ||
271 | it_2.setRight(this.support.unfoldAnd(relationVar2TypeDecComply)); | ||
272 | }; | ||
273 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
274 | it_1.setOperand(_doubleArrow); | ||
275 | }; | ||
276 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
277 | it.setFofFormula(_doubleArrow); | ||
278 | }; | ||
279 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
280 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
281 | _formulas.add(comply); | ||
282 | } | ||
283 | |||
284 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { | ||
285 | if (r instanceof RelationDeclaration) { | ||
286 | _transformRelation((RelationDeclaration)r, trace); | ||
287 | return; | ||
288 | } else if (r instanceof RelationDefinition) { | ||
289 | _transformRelation((RelationDefinition)r, trace); | ||
290 | return; | ||
291 | } else { | ||
292 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
293 | Arrays.<Object>asList(r, trace).toString()); | ||
294 | } | ||
295 | } | ||
296 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java new file mode 100644 index 00000000..e1be7df5 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |||
@@ -0,0 +1,242 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
15 | import com.google.common.collect.Iterables; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
21 | import java.util.ArrayList; | ||
22 | import java.util.Collection; | ||
23 | import java.util.HashMap; | ||
24 | import java.util.List; | ||
25 | import java.util.Map; | ||
26 | import org.eclipse.emf.common.util.EList; | ||
27 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
28 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
29 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
30 | import org.eclipse.xtext.xbase.lib.Extension; | ||
31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
33 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
34 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
35 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
36 | |||
37 | @SuppressWarnings("all") | ||
38 | public class Logic2VampireLanguageMapper_Support { | ||
39 | @Extension | ||
40 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
41 | |||
42 | protected String toIDMultiple(final String... ids) { | ||
43 | final Function1<String, String> _function = (String it) -> { | ||
44 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(it.split("\\s+"))), "_"); | ||
45 | }; | ||
46 | return IterableExtensions.join(ListExtensions.<String, String>map(((List<String>)Conversions.doWrapArray(ids)), _function), "_"); | ||
47 | } | ||
48 | |||
49 | protected String toID(final String ids) { | ||
50 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_"); | ||
51 | } | ||
52 | |||
53 | protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) { | ||
54 | int _size = operands.size(); | ||
55 | boolean _equals = (_size == 1); | ||
56 | if (_equals) { | ||
57 | return IterableExtensions.head(operands); | ||
58 | } else { | ||
59 | int _size_1 = operands.size(); | ||
60 | boolean _greaterThan = (_size_1 > 1); | ||
61 | if (_greaterThan) { | ||
62 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
63 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
64 | it.setLeft(IterableExtensions.head(operands)); | ||
65 | it.setRight(this.unfoldAnd(operands.subList(1, operands.size()))); | ||
66 | }; | ||
67 | return ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
68 | } else { | ||
69 | StringConcatenation _builder = new StringConcatenation(); | ||
70 | _builder.append("Logic operator with 0 operands!"); | ||
71 | throw new UnsupportedOperationException(_builder.toString()); | ||
72 | } | ||
73 | } | ||
74 | } | ||
75 | |||
76 | protected VLSTerm unfoldOr(final List<? extends VLSTerm> operands) { | ||
77 | int _size = operands.size(); | ||
78 | boolean _equals = (_size == 1); | ||
79 | if (_equals) { | ||
80 | return IterableExtensions.head(operands); | ||
81 | } else { | ||
82 | int _size_1 = operands.size(); | ||
83 | boolean _greaterThan = (_size_1 > 1); | ||
84 | if (_greaterThan) { | ||
85 | VLSOr _createVLSOr = this.factory.createVLSOr(); | ||
86 | final Procedure1<VLSOr> _function = (VLSOr it) -> { | ||
87 | it.setLeft(IterableExtensions.head(operands)); | ||
88 | it.setRight(this.unfoldOr(operands.subList(1, operands.size()))); | ||
89 | }; | ||
90 | return ObjectExtensions.<VLSOr>operator_doubleArrow(_createVLSOr, _function); | ||
91 | } else { | ||
92 | StringConcatenation _builder = new StringConcatenation(); | ||
93 | _builder.append("Logic operator with 0 operands!"); | ||
94 | throw new UnsupportedOperationException(_builder.toString()); | ||
95 | } | ||
96 | } | ||
97 | } | ||
98 | |||
99 | protected VLSTerm unfoldDistinctTerms(final Logic2VampireLanguageMapper m, final EList<Term> operands, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
100 | int _size = operands.size(); | ||
101 | boolean _equals = (_size == 1); | ||
102 | if (_equals) { | ||
103 | return m.transformTerm(IterableExtensions.<Term>head(operands), trace, variables); | ||
104 | } else { | ||
105 | int _size_1 = operands.size(); | ||
106 | boolean _greaterThan = (_size_1 > 1); | ||
107 | if (_greaterThan) { | ||
108 | int _size_2 = operands.size(); | ||
109 | int _size_3 = operands.size(); | ||
110 | int _multiply = (_size_2 * _size_3); | ||
111 | int _divide = (_multiply / 2); | ||
112 | final ArrayList<VLSTerm> notEquals = new ArrayList<VLSTerm>(_divide); | ||
113 | int _size_4 = operands.size(); | ||
114 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _size_4, true); | ||
115 | for (final Integer i : _doubleDotLessThan) { | ||
116 | int _size_5 = operands.size(); | ||
117 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(((i).intValue() + 1), _size_5, true); | ||
118 | for (final Integer j : _doubleDotLessThan_1) { | ||
119 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); | ||
120 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { | ||
121 | it.setLeft(m.transformTerm(operands.get((i).intValue()), trace, variables)); | ||
122 | it.setRight(m.transformTerm(operands.get((j).intValue()), trace, variables)); | ||
123 | }; | ||
124 | VLSInequality _doubleArrow = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | ||
125 | notEquals.add(_doubleArrow); | ||
126 | } | ||
127 | } | ||
128 | return this.unfoldAnd(notEquals); | ||
129 | } else { | ||
130 | StringConcatenation _builder = new StringConcatenation(); | ||
131 | _builder.append("Logic operator with 0 operands!"); | ||
132 | throw new UnsupportedOperationException(_builder.toString()); | ||
133 | } | ||
134 | } | ||
135 | } | ||
136 | |||
137 | /** | ||
138 | * def protected String toID(List<String> ids) { | ||
139 | * ids.map[it.split("\\s+").join("'")].join("'") | ||
140 | * } | ||
141 | */ | ||
142 | protected VLSTerm createUniversallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
143 | VLSUniversalQuantifier _xblockexpression = null; | ||
144 | { | ||
145 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { | ||
146 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
147 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
148 | it.setName(this.toIDMultiple("Var", v.getName())); | ||
149 | }; | ||
150 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
151 | }; | ||
152 | final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function); | ||
153 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
154 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); | ||
155 | for (final Variable variable : _quantifiedVariables) { | ||
156 | { | ||
157 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
158 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
159 | TypeReference _range = variable.getRange(); | ||
160 | it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | ||
161 | EList<VLSTerm> _terms = it.getTerms(); | ||
162 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
163 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
164 | it_1.setName(this.toIDMultiple("Var", variable.getName())); | ||
165 | }; | ||
166 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
167 | _terms.add(_doubleArrow); | ||
168 | }; | ||
169 | final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
170 | typedefs.add(eq); | ||
171 | } | ||
172 | } | ||
173 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
174 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> { | ||
175 | EList<VLSVariable> _variables = it.getVariables(); | ||
176 | Collection<VLSVariable> _values = variableMap.values(); | ||
177 | Iterables.<VLSVariable>addAll(_variables, _values); | ||
178 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
179 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> { | ||
180 | it_1.setLeft(this.unfoldAnd(typedefs)); | ||
181 | it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | ||
182 | }; | ||
183 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
184 | it.setOperand(_doubleArrow); | ||
185 | }; | ||
186 | _xblockexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
187 | } | ||
188 | return _xblockexpression; | ||
189 | } | ||
190 | |||
191 | protected VLSTerm createExistentiallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
192 | VLSExistentialQuantifier _xblockexpression = null; | ||
193 | { | ||
194 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { | ||
195 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
196 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
197 | it.setName(this.toIDMultiple("Var", v.getName())); | ||
198 | }; | ||
199 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
200 | }; | ||
201 | final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function); | ||
202 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
203 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); | ||
204 | for (final Variable variable : _quantifiedVariables) { | ||
205 | { | ||
206 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
207 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
208 | TypeReference _range = variable.getRange(); | ||
209 | it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | ||
210 | EList<VLSTerm> _terms = it.getTerms(); | ||
211 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
212 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
213 | it_1.setName(this.toIDMultiple("Var", variable.getName())); | ||
214 | }; | ||
215 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
216 | _terms.add(_doubleArrow); | ||
217 | }; | ||
218 | final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
219 | typedefs.add(eq); | ||
220 | } | ||
221 | } | ||
222 | typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | ||
223 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
224 | final Procedure1<VLSExistentialQuantifier> _function_1 = (VLSExistentialQuantifier it) -> { | ||
225 | EList<VLSVariable> _variables = it.getVariables(); | ||
226 | Collection<VLSVariable> _values = variableMap.values(); | ||
227 | Iterables.<VLSVariable>addAll(_variables, _values); | ||
228 | it.setOperand(this.unfoldAnd(typedefs)); | ||
229 | }; | ||
230 | _xblockexpression = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_1); | ||
231 | } | ||
232 | return _xblockexpression; | ||
233 | } | ||
234 | |||
235 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { | ||
236 | HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1); | ||
237 | final Procedure1<HashMap<Variable, VLSVariable>> _function = (HashMap<Variable, VLSVariable> it) -> { | ||
238 | it.putAll(map2); | ||
239 | }; | ||
240 | return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function); | ||
241 | } | ||
242 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java new file mode 100644 index 00000000..c55e2421 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java | |||
@@ -0,0 +1,25 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
9 | import java.util.Collection; | ||
10 | import java.util.List; | ||
11 | |||
12 | @SuppressWarnings("all") | ||
13 | public interface Logic2VampireLanguageMapper_TypeMapper { | ||
14 | public abstract void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); | ||
15 | |||
16 | public abstract List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); | ||
17 | |||
18 | public abstract VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace); | ||
19 | |||
20 | public abstract int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace); | ||
21 | |||
22 | public abstract VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace); | ||
23 | |||
24 | public abstract VampireModelInterpretation_TypeInterpretation getTypeInterpreter(); | ||
25 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java new file mode 100644 index 00000000..1e08c8ad --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java | |||
@@ -0,0 +1,5 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public interface Logic2VampireLanguageMapper_TypeMapperTrace { | ||
5 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java new file mode 100644 index 00000000..d674ac71 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java | |||
@@ -0,0 +1,21 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
9 | import java.util.HashMap; | ||
10 | import java.util.Map; | ||
11 | |||
12 | @SuppressWarnings("all") | ||
13 | public class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace { | ||
14 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); | ||
15 | |||
16 | public final Map<DefinedElement, VLSEquality> definedElement2Declaration = new HashMap<DefinedElement, VLSEquality>(); | ||
17 | |||
18 | public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>(); | ||
19 | |||
20 | public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>(); | ||
21 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java new file mode 100644 index 00000000..38ff37cd --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java | |||
@@ -0,0 +1,287 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
19 | import com.google.common.base.Objects; | ||
20 | import com.google.common.collect.Iterables; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; | ||
25 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
26 | import java.util.ArrayList; | ||
27 | import java.util.Collection; | ||
28 | import java.util.List; | ||
29 | import org.eclipse.emf.common.util.EList; | ||
30 | import org.eclipse.xtext.xbase.lib.Extension; | ||
31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
33 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
34 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
35 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
36 | |||
37 | @SuppressWarnings("all") | ||
38 | public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { | ||
39 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
40 | |||
41 | @Extension | ||
42 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
43 | |||
44 | public Logic2VampireLanguageMapper_TypeMapper_FilteredTypes() { | ||
45 | LogicproblemPackage.eINSTANCE.getClass(); | ||
46 | } | ||
47 | |||
48 | @Override | ||
49 | public void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | ||
50 | final Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes(); | ||
51 | trace.typeMapperTrace = typeTrace; | ||
52 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
53 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
54 | it.setName("A"); | ||
55 | }; | ||
56 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
57 | for (final Type type : types) { | ||
58 | { | ||
59 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
60 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
61 | it.setConstant(this.support.toIDMultiple("type", type.getName())); | ||
62 | EList<VLSTerm> _terms = it.getTerms(); | ||
63 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
64 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
65 | it_1.setName(variable.getName()); | ||
66 | }; | ||
67 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
68 | _terms.add(_doubleArrow); | ||
69 | }; | ||
70 | final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
71 | typeTrace.type2Predicate.put(type, typePred); | ||
72 | } | ||
73 | } | ||
74 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); | ||
75 | for (final TypeDefinition type_1 : _filter) { | ||
76 | { | ||
77 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
78 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
79 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName())); | ||
80 | it.setFofRole("axiom"); | ||
81 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
82 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
83 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
84 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
85 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> { | ||
86 | it_2.setName(variable.getName()); | ||
87 | }; | ||
88 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3); | ||
89 | _variables.add(_doubleArrow); | ||
90 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
91 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | ||
92 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
93 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_3) -> { | ||
94 | it_3.setConstant(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate).getConstant()); | ||
95 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
96 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
97 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { | ||
98 | it_4.setName("A"); | ||
99 | }; | ||
100 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_6); | ||
101 | _terms.add(_doubleArrow_1); | ||
102 | }; | ||
103 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | ||
104 | it_2.setLeft(_doubleArrow_1); | ||
105 | CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate); | ||
106 | final Function1<DefinedElement, VLSEquality> _function_6 = (DefinedElement e) -> { | ||
107 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
108 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { | ||
109 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
110 | final Procedure1<VLSVariable> _function_8 = (VLSVariable it_4) -> { | ||
111 | it_4.setName(variable.getName()); | ||
112 | }; | ||
113 | VLSVariable _doubleArrow_2 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_8); | ||
114 | it_3.setLeft(_doubleArrow_2); | ||
115 | VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); | ||
116 | final Procedure1<VLSDoubleQuote> _function_9 = (VLSDoubleQuote it_4) -> { | ||
117 | String _name = e.getName(); | ||
118 | String _plus = ("\"a" + _name); | ||
119 | String _plus_1 = (_plus + "\""); | ||
120 | it_4.setValue(_plus_1); | ||
121 | }; | ||
122 | VLSDoubleQuote _doubleArrow_3 = ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function_9); | ||
123 | it_3.setRight(_doubleArrow_3); | ||
124 | }; | ||
125 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); | ||
126 | }; | ||
127 | it_2.setRight(this.support.unfoldOr(ListExtensions.<DefinedElement, VLSEquality>map(type_1.getElements(), _function_6))); | ||
128 | }; | ||
129 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
130 | it_1.setOperand(_doubleArrow_1); | ||
131 | }; | ||
132 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
133 | it.setFofFormula(_doubleArrow); | ||
134 | }; | ||
135 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
136 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
137 | _formulas.add(res); | ||
138 | } | ||
139 | } | ||
140 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | ||
141 | boolean _isIsAbstract = it.isIsAbstract(); | ||
142 | return Boolean.valueOf((!_isIsAbstract)); | ||
143 | }; | ||
144 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); | ||
145 | for (final Type type_2 : _filter_1) { | ||
146 | { | ||
147 | for (final Type type2 : types) { | ||
148 | if ((Objects.equal(type_2, type2) || this.dfsSupertypeCheck(type_2, type2))) { | ||
149 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
150 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { | ||
151 | it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant()); | ||
152 | EList<VLSTerm> _terms = it.getTerms(); | ||
153 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
154 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> { | ||
155 | it_1.setName("A"); | ||
156 | }; | ||
157 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3); | ||
158 | _terms.add(_doubleArrow); | ||
159 | }; | ||
160 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2); | ||
161 | typeTrace.type2PossibleNot.put(type2, _doubleArrow); | ||
162 | } else { | ||
163 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
164 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { | ||
165 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); | ||
166 | final Procedure1<VLSFunction> _function_4 = (VLSFunction it_1) -> { | ||
167 | it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant()); | ||
168 | EList<VLSTerm> _terms = it_1.getTerms(); | ||
169 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
170 | final Procedure1<VLSVariable> _function_5 = (VLSVariable it_2) -> { | ||
171 | it_2.setName("A"); | ||
172 | }; | ||
173 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_5); | ||
174 | _terms.add(_doubleArrow_1); | ||
175 | }; | ||
176 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_4); | ||
177 | it.setOperand(_doubleArrow_1); | ||
178 | }; | ||
179 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); | ||
180 | typeTrace.type2PossibleNot.put(type2, _doubleArrow_1); | ||
181 | } | ||
182 | } | ||
183 | Collection<VLSTerm> _values = typeTrace.type2PossibleNot.values(); | ||
184 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
185 | typeTrace.type2And.put(type_2, this.support.unfoldAnd(_arrayList)); | ||
186 | typeTrace.type2PossibleNot.clear(); | ||
187 | } | ||
188 | } | ||
189 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
190 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | ||
191 | it.setName("hierarchyHandler"); | ||
192 | it.setFofRole("axiom"); | ||
193 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
194 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | ||
195 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
196 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
197 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_2) -> { | ||
198 | it_2.setName("A"); | ||
199 | }; | ||
200 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_4); | ||
201 | _variables.add(_doubleArrow); | ||
202 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
203 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | ||
204 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
205 | final Procedure1<VLSFunction> _function_6 = (VLSFunction it_3) -> { | ||
206 | it_3.setConstant("Object"); | ||
207 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
208 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
209 | final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> { | ||
210 | it_4.setName("A"); | ||
211 | }; | ||
212 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_7); | ||
213 | _terms.add(_doubleArrow_1); | ||
214 | }; | ||
215 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_6); | ||
216 | it_2.setLeft(_doubleArrow_1); | ||
217 | Collection<VLSTerm> _values = typeTrace.type2And.values(); | ||
218 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
219 | it_2.setRight(this.support.unfoldOr(_arrayList)); | ||
220 | }; | ||
221 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | ||
222 | it_1.setOperand(_doubleArrow_1); | ||
223 | }; | ||
224 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); | ||
225 | it.setFofFormula(_doubleArrow); | ||
226 | }; | ||
227 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | ||
228 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
229 | _formulas.add(hierarch); | ||
230 | } | ||
231 | |||
232 | public boolean dfsSupertypeCheck(final Type type, final Type type2) { | ||
233 | boolean _xifexpression = false; | ||
234 | boolean _isEmpty = type.getSupertypes().isEmpty(); | ||
235 | if (_isEmpty) { | ||
236 | return false; | ||
237 | } else { | ||
238 | boolean _xifexpression_1 = false; | ||
239 | boolean _contains = type.getSupertypes().contains(type2); | ||
240 | if (_contains) { | ||
241 | return true; | ||
242 | } else { | ||
243 | EList<Type> _supertypes = type.getSupertypes(); | ||
244 | for (final Type supertype : _supertypes) { | ||
245 | boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2); | ||
246 | if (_dfsSupertypeCheck) { | ||
247 | return true; | ||
248 | } | ||
249 | } | ||
250 | } | ||
251 | _xifexpression = _xifexpression_1; | ||
252 | } | ||
253 | return _xifexpression; | ||
254 | } | ||
255 | |||
256 | @Override | ||
257 | public List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | ||
258 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
259 | } | ||
260 | |||
261 | @Override | ||
262 | public VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { | ||
263 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
264 | } | ||
265 | |||
266 | @Override | ||
267 | public int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { | ||
268 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
269 | } | ||
270 | |||
271 | @Override | ||
272 | public VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { | ||
273 | VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); | ||
274 | final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> { | ||
275 | String _name = referred.getName(); | ||
276 | String _plus = ("\"a" + _name); | ||
277 | String _plus_1 = (_plus + "\""); | ||
278 | it.setValue(_plus_1); | ||
279 | }; | ||
280 | return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function); | ||
281 | } | ||
282 | |||
283 | @Override | ||
284 | public VampireModelInterpretation_TypeInterpretation getTypeInterpreter() { | ||
285 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
286 | } | ||
287 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java new file mode 100644 index 00000000..507831fa --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java | |||
@@ -0,0 +1,5 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public interface VampireModelInterpretation_TypeInterpretation { | ||
5 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java new file mode 100644 index 00000000..aff0dc9d --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java | |||
@@ -0,0 +1,7 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; | ||
4 | |||
5 | @SuppressWarnings("all") | ||
6 | public class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation { | ||
7 | } | ||