diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-14 19:38:40 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-14 19:38:40 -0400 |
commit | 3997c2408f192e22f809cd96faa5bc552530289d (patch) | |
tree | 6d9134700977b29a5d67206c1e3f587d468e34fa /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner | |
parent | remove Alloy solver copy (diff) | |
download | VIATRA-Generator-3997c2408f192e22f809cd96faa5bc552530289d.tar.gz VIATRA-Generator-3997c2408f192e22f809cd96faa5bc552530289d.tar.zst VIATRA-Generator-3997c2408f192e22f809cd96faa5bc552530289d.zip |
This branch is ready to be merged into masterVampire-New
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner')
36 files changed, 65 insertions, 2882 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend index 1fda24d9..c3b344eb 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend | |||
@@ -8,7 +8,7 @@ class VampireSolverConfiguration | |||
8 | public var int contCycleLevel = 0 | 8 | public var int contCycleLevel = 0 |
9 | public var boolean uniquenessDuplicates = false | 9 | public var boolean uniquenessDuplicates = false |
10 | public var int iteration = -1 | 10 | public var int iteration = -1 |
11 | public var BackendSolver solver = BackendSolver::VAMPIRE | 11 | public var BackendSolver solver = BackendSolver::LOCVAMP |
12 | public var genModel = true | 12 | public var genModel = true |
13 | public var server = false | 13 | public var server = false |
14 | //choose needed backend solver | 14 | //choose needed backend solver |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend index 59084843..4b8b10a9 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend | |||
@@ -83,26 +83,27 @@ class VampireSolver extends LogicReasoner { | |||
83 | var done = false | 83 | var done = false |
84 | print(" ") | 84 | print(" ") |
85 | while (!done) { | 85 | while (!done) { |
86 | print("(x)") | 86 | // print("(x)") |
87 | done = false | 87 | done = false |
88 | response = support.sendPost(form) | 88 | response = support.sendPost(form) |
89 | 89 | ||
90 | var responseFound = false | 90 | var responseFound = false |
91 | ind = 0 | 91 | ind = 0 |
92 | while (!responseFound) { | 92 | while (!responseFound && ind<response.length) { |
93 | var line = response.get(ind) | 93 | var line = response.get(ind) |
94 | // println(line) | 94 | // println(line) |
95 | if (line.length >= 5 && line.substring(0, 5) == "ERROR") { | 95 | if (line.length >= 5 && line.substring(0, 5) == "ERROR") { |
96 | done = false | 96 | done = false |
97 | responseFound = true | 97 | responseFound = true |
98 | } else { | 98 | } else { |
99 | if (line == "</PRE>") { | 99 | if (line == "</PRE>" && response.get(ind-1) != "<PRE>") { |
100 | done = true | 100 | done = true |
101 | responseFound = true | 101 | responseFound = true |
102 | } | 102 | } |
103 | } | 103 | } |
104 | ind++ | 104 | ind++ |
105 | } | 105 | } |
106 | if (!done) println("(Server call failed. Trying again...)") | ||
106 | } | 107 | } |
107 | val satRaw = response.get(ind - 3) | 108 | val satRaw = response.get(ind - 3) |
108 | val modRaw = response.get(ind - 2) | 109 | val modRaw = response.get(ind - 2) |
@@ -118,10 +119,35 @@ class VampireSolver extends LogicReasoner { | |||
118 | println() | 119 | println() |
119 | println(sat) | 120 | println(sat) |
120 | println(mod) | 121 | println(mod) |
122 | |||
123 | return createUndecidableResult => [ | ||
124 | it.statistics = createStatistics => [ | ||
125 | it.transformationTime = transformationTime as int | ||
126 | it.entries += createStringStatisticEntry => [ | ||
127 | it.name = "satOut" | ||
128 | it.value = satOut | ||
129 | ] | ||
130 | it.entries += createStringStatisticEntry => [ | ||
131 | it.name = "satTime" | ||
132 | it.value = satTime | ||
133 | ] | ||
134 | it.entries += createStringStatisticEntry => [ | ||
135 | it.name = "modOut" | ||
136 | it.value = modOut | ||
137 | ] | ||
138 | it.entries += createStringStatisticEntry => [ | ||
139 | it.name = "modTime" | ||
140 | it.value = modTime | ||
141 | ] | ||
121 | 142 | ||
143 | ] | ||
144 | ] | ||
145 | |||
146 | /* | ||
147 | * TODO | ||
122 | return createModelResult => [ | 148 | return createModelResult => [ |
123 | it.problem = null | 149 | it.problem = null |
124 | it.representation += createVampireModel => [] | 150 | it.representation += createVampireModel => []//TODO Add something here |
125 | it.trace = trace | 151 | it.trace = trace |
126 | it.statistics = createStatistics => [ | 152 | it.statistics = createStatistics => [ |
127 | it.transformationTime = transformationTime as int | 153 | it.transformationTime = transformationTime as int |
@@ -144,6 +170,7 @@ class VampireSolver extends LogicReasoner { | |||
144 | 170 | ||
145 | ] | 171 | ] |
146 | ] | 172 | ] |
173 | */ | ||
147 | 174 | ||
148 | // return newArrayList(line1, line2) | 175 | // return newArrayList(line1, line2) |
149 | } else { | 176 | } else { |
@@ -172,8 +199,31 @@ class VampireSolver extends LogicReasoner { | |||
172 | } | 199 | } |
173 | 200 | ||
174 | val realModOut=modOut | 201 | val realModOut=modOut |
175 | |||
176 | 202 | ||
203 | return createUndecidableResult => [ | ||
204 | it.statistics = createStatistics => [ | ||
205 | it.transformationTime = transformationTime as int | ||
206 | it.entries += createStringStatisticEntry => [ | ||
207 | it.name = "satOut" | ||
208 | it.value = "-" | ||
209 | ] | ||
210 | it.entries += createStringStatisticEntry => [ | ||
211 | it.name = "satTime" | ||
212 | it.value = "-" | ||
213 | ] | ||
214 | it.entries += createStringStatisticEntry => [ | ||
215 | it.name = "modOut" | ||
216 | it.value = realModOut | ||
217 | ] | ||
218 | it.entries += createStringStatisticEntry => [ | ||
219 | it.name = "modTime" | ||
220 | it.value = (vampSol.solverTime/1000.0).toString | ||
221 | ] | ||
222 | |||
223 | ] | ||
224 | ] | ||
225 | |||
226 | /* | ||
177 | return createModelResult => [ | 227 | return createModelResult => [ |
178 | it.problem = null | 228 | it.problem = null |
179 | it.representation += createVampireModel => [] | 229 | it.representation += createVampireModel => [] |
@@ -199,6 +249,7 @@ class VampireSolver extends LogicReasoner { | |||
199 | 249 | ||
200 | ] | 250 | ] |
201 | ] | 251 | ] |
252 | */ | ||
202 | } | 253 | } |
203 | } | 254 | } |
204 | // return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, | 255 | // return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, |
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 index 44efd84e..fa334322 100644 --- 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 | |||
@@ -299,23 +299,23 @@ class Logic2VampireLanguageMapper_Support { | |||
299 | def getSolverSpecs(BackendSolver solver) { | 299 | def getSolverSpecs(BackendSolver solver) { |
300 | switch (solver) { | 300 | switch (solver) { |
301 | case BackendSolver::CVC4: | 301 | case BackendSolver::CVC4: |
302 | return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") | 302 | return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT")//TODO Update |
303 | case BackendSolver::DARWINFM: | 303 | case BackendSolver::DARWINFM: |
304 | return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") | 304 | return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s")//TODO Update |
305 | case BackendSolver::EDARWIN: | 305 | case BackendSolver::EDARWIN: |
306 | return newArrayList("E-Darwin---1.5", | 306 | return newArrayList("E-Darwin---1.5", |
307 | "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") | 307 | "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s")//TODO Update |
308 | case BackendSolver::GEOIII: | 308 | case BackendSolver::GEOIII: |
309 | return newArrayList("Geo-III---2018C", | 309 | return newArrayList("Geo-III---2018C", |
310 | "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") | 310 | "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s")//TODO Update |
311 | case BackendSolver::IPROVER: | 311 | case BackendSolver::IPROVER: |
312 | return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") | 312 | return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s")//TODO Update |
313 | case BackendSolver::PARADOX: | 313 | case BackendSolver::PARADOX: |
314 | return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") | 314 | return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s")//TODO Update |
315 | case BackendSolver::VAMPIRE: | 315 | case BackendSolver::VAMPIRE: |
316 | return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") | 316 | return newArrayList("Vampire---SAT-4.5", "vampire --mode casc_sat -t %d %s") |
317 | case BackendSolver::Z3: | 317 | case BackendSolver::Z3: |
318 | return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s") | 318 | return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s")//TODO Update |
319 | } | 319 | } |
320 | } | 320 | } |
321 | 321 | ||
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 deleted file mode 100644 index e999bce6..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin +++ /dev/null | |||
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 deleted file mode 100644 index 28154d14..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin +++ /dev/null | |||
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 deleted file mode 100644 index 70f60102..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore +++ /dev/null | |||
@@ -1,10 +0,0 @@ | |||
1 | /.VampireSolver.java._trace | ||
2 | /.TypeMappingTechnique.java._trace | ||
3 | /.VampireBackendSolver.java._trace | ||
4 | /.VampireSolverConfiguration.java._trace | ||
5 | /.VampireAnalyzerConfiguration.xtendbin | ||
6 | /.VampireSolver.xtendbin | ||
7 | /TypeMappingTechnique.java | ||
8 | /VampireBackendSolver.java | ||
9 | /VampireSolver.java | ||
10 | /VampireSolverConfiguration.java | ||
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 deleted file mode 100644 index 8ffba2f1..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java +++ /dev/null | |||
@@ -1,6 +0,0 @@ | |||
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/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java deleted file mode 100644 index eb6007ec..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java +++ /dev/null | |||
@@ -1,275 +0,0 @@ | |||
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_Support; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
16 | import com.google.common.base.Objects; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; | ||
30 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | ||
31 | import java.util.ArrayList; | ||
32 | import java.util.List; | ||
33 | import org.eclipse.emf.common.util.EList; | ||
34 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
35 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
36 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
37 | import org.eclipse.xtext.xbase.lib.Extension; | ||
38 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
39 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
40 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
41 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
42 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
43 | |||
44 | @SuppressWarnings("all") | ||
45 | public class VampireSolver extends LogicReasoner { | ||
46 | public VampireSolver() { | ||
47 | VampireLanguagePackage.eINSTANCE.eClass(); | ||
48 | final VampireLanguageStandaloneSetupGenerated x = new VampireLanguageStandaloneSetupGenerated(); | ||
49 | VampireLanguageStandaloneSetup.doSetup(); | ||
50 | } | ||
51 | |||
52 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(); | ||
53 | |||
54 | private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper(); | ||
55 | |||
56 | private final VampireHandler handler = new VampireHandler(); | ||
57 | |||
58 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
59 | |||
60 | @Extension | ||
61 | private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE; | ||
62 | |||
63 | @Extension | ||
64 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
65 | |||
66 | @Override | ||
67 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { | ||
68 | try { | ||
69 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); | ||
70 | String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + | ||
71 | Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp"); | ||
72 | final long transformationStart = System.currentTimeMillis(); | ||
73 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | ||
74 | long _currentTimeMillis = System.currentTimeMillis(); | ||
75 | final long transformationTime = (_currentTimeMillis - transformationStart); | ||
76 | final VampireModel vampireProblem = result.getOutput(); | ||
77 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | ||
78 | String fileURI = null; | ||
79 | String vampireCode = null; | ||
80 | vampireCode = workspace.writeModelToString(vampireProblem, fileName); | ||
81 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || | ||
82 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); | ||
83 | if (writeFile) { | ||
84 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString(); | ||
85 | } | ||
86 | if (vampireConfig.genModel) { | ||
87 | if (vampireConfig.server) { | ||
88 | final String form = this.support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit); | ||
89 | ArrayList<String> response = CollectionLiterals.<String>newArrayList(); | ||
90 | int ind = 0; | ||
91 | boolean done = false; | ||
92 | InputOutput.<String>print(" "); | ||
93 | while ((!done)) { | ||
94 | { | ||
95 | InputOutput.<String>print("(x)"); | ||
96 | done = false; | ||
97 | response = this.support.sendPost(form); | ||
98 | boolean responseFound = false; | ||
99 | ind = 0; | ||
100 | while ((!responseFound)) { | ||
101 | { | ||
102 | String line = response.get(ind); | ||
103 | if (((line.length() >= 5) && Objects.equal(line.substring(0, 5), "ERROR"))) { | ||
104 | done = false; | ||
105 | responseFound = true; | ||
106 | } else { | ||
107 | boolean _equals = Objects.equal(line, "</PRE>"); | ||
108 | if (_equals) { | ||
109 | done = true; | ||
110 | responseFound = true; | ||
111 | } | ||
112 | } | ||
113 | ind++; | ||
114 | } | ||
115 | } | ||
116 | } | ||
117 | } | ||
118 | final String satRaw = response.get((ind - 3)); | ||
119 | final String modRaw = response.get((ind - 2)); | ||
120 | final ArrayList<String> sat = CollectionLiterals.<String>newArrayList(satRaw.split(" ")); | ||
121 | final ArrayList<String> mod = CollectionLiterals.<String>newArrayList(modRaw.split(" ")); | ||
122 | final String satOut = sat.get(1); | ||
123 | final String modOut = mod.get(1); | ||
124 | final String satTime = sat.get(2); | ||
125 | final String modTime = mod.get(2); | ||
126 | InputOutput.println(); | ||
127 | InputOutput.<ArrayList<String>>println(sat); | ||
128 | InputOutput.<ArrayList<String>>println(mod); | ||
129 | ModelResult _createModelResult = this.resultFactory.createModelResult(); | ||
130 | final Procedure1<ModelResult> _function = (ModelResult it) -> { | ||
131 | it.setProblem(null); | ||
132 | EList<Object> _representation = it.getRepresentation(); | ||
133 | VampireModel _createVampireModel = this.factory.createVampireModel(); | ||
134 | final Procedure1<VampireModel> _function_1 = (VampireModel it_1) -> { | ||
135 | }; | ||
136 | VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1); | ||
137 | _representation.add(_doubleArrow); | ||
138 | it.setTrace(it.getTrace()); | ||
139 | Statistics _createStatistics = this.resultFactory.createStatistics(); | ||
140 | final Procedure1<Statistics> _function_2 = (Statistics it_1) -> { | ||
141 | it_1.setTransformationTime(((int) transformationTime)); | ||
142 | EList<StatisticEntry> _entries = it_1.getEntries(); | ||
143 | StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); | ||
144 | final Procedure1<StringStatisticEntry> _function_3 = (StringStatisticEntry it_2) -> { | ||
145 | it_2.setName("satOut"); | ||
146 | it_2.setValue(satOut); | ||
147 | }; | ||
148 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3); | ||
149 | _entries.add(_doubleArrow_1); | ||
150 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); | ||
151 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); | ||
152 | final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> { | ||
153 | it_2.setName("satTime"); | ||
154 | it_2.setValue(satTime); | ||
155 | }; | ||
156 | StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_4); | ||
157 | _entries_1.add(_doubleArrow_2); | ||
158 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); | ||
159 | StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); | ||
160 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { | ||
161 | it_2.setName("modOut"); | ||
162 | it_2.setValue(modOut); | ||
163 | }; | ||
164 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_5); | ||
165 | _entries_2.add(_doubleArrow_3); | ||
166 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); | ||
167 | StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); | ||
168 | final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> { | ||
169 | it_2.setName("modTime"); | ||
170 | it_2.setValue(modTime); | ||
171 | }; | ||
172 | StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_6); | ||
173 | _entries_3.add(_doubleArrow_4); | ||
174 | }; | ||
175 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2); | ||
176 | it.setStatistics(_doubleArrow_1); | ||
177 | }; | ||
178 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function); | ||
179 | } else { | ||
180 | InputOutput.println(); | ||
181 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | ||
182 | String modOut_1 = "no"; | ||
183 | boolean _isFiniteModelGenerated = vampSol.isFiniteModelGenerated(); | ||
184 | if (_isFiniteModelGenerated) { | ||
185 | modOut_1 = "FiniteModel"; | ||
186 | } | ||
187 | final String realModOut = modOut_1; | ||
188 | ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); | ||
189 | final Procedure1<ModelResult> _function_1 = (ModelResult it) -> { | ||
190 | it.setProblem(null); | ||
191 | EList<Object> _representation = it.getRepresentation(); | ||
192 | VampireModel _createVampireModel = this.factory.createVampireModel(); | ||
193 | final Procedure1<VampireModel> _function_2 = (VampireModel it_1) -> { | ||
194 | }; | ||
195 | VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_2); | ||
196 | _representation.add(_doubleArrow); | ||
197 | it.setTrace(it.getTrace()); | ||
198 | Statistics _createStatistics = this.resultFactory.createStatistics(); | ||
199 | final Procedure1<Statistics> _function_3 = (Statistics it_1) -> { | ||
200 | it_1.setTransformationTime(((int) transformationTime)); | ||
201 | EList<StatisticEntry> _entries = it_1.getEntries(); | ||
202 | StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); | ||
203 | final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> { | ||
204 | it_2.setName("satOut"); | ||
205 | it_2.setValue("-"); | ||
206 | }; | ||
207 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_4); | ||
208 | _entries.add(_doubleArrow_1); | ||
209 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); | ||
210 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); | ||
211 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { | ||
212 | it_2.setName("satTime"); | ||
213 | it_2.setValue("-"); | ||
214 | }; | ||
215 | StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5); | ||
216 | _entries_1.add(_doubleArrow_2); | ||
217 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); | ||
218 | StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); | ||
219 | final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> { | ||
220 | it_2.setName("modOut"); | ||
221 | it_2.setValue(realModOut); | ||
222 | }; | ||
223 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_6); | ||
224 | _entries_2.add(_doubleArrow_3); | ||
225 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); | ||
226 | StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); | ||
227 | final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> { | ||
228 | it_2.setName("modTime"); | ||
229 | long _solverTime = vampSol.getSolverTime(); | ||
230 | it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString()); | ||
231 | }; | ||
232 | StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_7); | ||
233 | _entries_3.add(_doubleArrow_4); | ||
234 | }; | ||
235 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_3); | ||
236 | it.setStatistics(_doubleArrow_1); | ||
237 | }; | ||
238 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_1); | ||
239 | } | ||
240 | } | ||
241 | return null; | ||
242 | } catch (Throwable _e) { | ||
243 | throw Exceptions.sneakyThrow(_e); | ||
244 | } | ||
245 | } | ||
246 | |||
247 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | ||
248 | if ((configuration instanceof VampireSolverConfiguration)) { | ||
249 | return ((VampireSolverConfiguration)configuration); | ||
250 | } else { | ||
251 | StringConcatenation _builder = new StringConcatenation(); | ||
252 | _builder.append("The configuration have to be an "); | ||
253 | String _simpleName = VampireSolverConfiguration.class.getSimpleName(); | ||
254 | _builder.append(_simpleName); | ||
255 | _builder.append("!"); | ||
256 | throw new IllegalArgumentException(_builder.toString()); | ||
257 | } | ||
258 | } | ||
259 | |||
260 | @Override | ||
261 | public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) { | ||
262 | List<VampireModelInterpretation> _xblockexpression = null; | ||
263 | { | ||
264 | final EList<Object> sols = modelResult.getRepresentation(); | ||
265 | final Function1<Object, VampireModelInterpretation> _function = (Object it) -> { | ||
266 | Object _trace = modelResult.getTrace(); | ||
267 | return new VampireModelInterpretation( | ||
268 | ((VampireModel) it), | ||
269 | ((Logic2VampireLanguageMapperTrace) _trace)); | ||
270 | }; | ||
271 | _xblockexpression = ListExtensions.<Object, VampireModelInterpretation>map(sols, _function); | ||
272 | } | ||
273 | return _xblockexpression; | ||
274 | } | ||
275 | } | ||
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 deleted file mode 100644 index c094872e..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java +++ /dev/null | |||
@@ -1,19 +0,0 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver; | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
5 | |||
6 | @SuppressWarnings("all") | ||
7 | public class VampireSolverConfiguration extends LogicSolverConfiguration { | ||
8 | public int contCycleLevel = 0; | ||
9 | |||
10 | public boolean uniquenessDuplicates = false; | ||
11 | |||
12 | public int iteration = (-1); | ||
13 | |||
14 | public BackendSolver solver = BackendSolver.VAMPIRE; | ||
15 | |||
16 | public boolean genModel = true; | ||
17 | |||
18 | public boolean server = false; | ||
19 | } | ||
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 deleted file mode 100644 index 18da19a9..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin +++ /dev/null | |||
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 deleted file mode 100644 index 37c845cd..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin +++ /dev/null | |||
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 deleted file mode 100644 index d8c61adc..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin +++ /dev/null | |||
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_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin deleted file mode 100644 index 1a86a55f..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin +++ /dev/null | |||
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 deleted file mode 100644 index 216b3a4b..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin +++ /dev/null | |||
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_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin deleted file mode 100644 index 8733e530..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin +++ /dev/null | |||
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 deleted file mode 100644 index 634dab6a..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin +++ /dev/null | |||
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 deleted file mode 100644 index 28c93f34..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin +++ /dev/null | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin deleted file mode 100644 index faef07c1..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin +++ /dev/null | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin deleted file mode 100644 index 3d96efbf..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin +++ /dev/null | |||
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 deleted file mode 100644 index b3756706..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin +++ /dev/null | |||
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 deleted file mode 100644 index f75b4eaf..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ /dev/null | |||
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 deleted file mode 100644 index 8a9aa4bb..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore +++ /dev/null | |||
@@ -1,42 +0,0 @@ | |||
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 | ||
12 | /.Logic2VampireLanguageMapper.xtendbin | ||
13 | /.Logic2VampireLanguageMapperTrace.xtendbin | ||
14 | /.Logic2VampireLanguageMapper_ConstantMapper.xtendbin | ||
15 | /.Logic2VampireLanguageMapper_RelationMapper.xtendbin | ||
16 | /.Logic2VampireLanguageMapper_Support.xtendbin | ||
17 | /.Logic2VampireLanguageMapper_TypeMapper.xtendbin | ||
18 | /.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin | ||
19 | /.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin | ||
20 | /.VampireModelInterpretation_TypeInterpretation.xtendbin | ||
21 | /.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin | ||
22 | /Logic2VampireLanguageMapper.java | ||
23 | /Logic2VampireLanguageMapperTrace.java | ||
24 | /Logic2VampireLanguageMapper_ConstantMapper.java | ||
25 | /Logic2VampireLanguageMapper_RelationMapper.java | ||
26 | /Logic2VampireLanguageMapper_Support.java | ||
27 | /Logic2VampireLanguageMapper_TypeMapper.java | ||
28 | /Logic2VampireLanguageMapper_TypeMapperTrace.java | ||
29 | /Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java | ||
30 | /Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java | ||
31 | /VampireModelInterpretation_TypeInterpretation.java | ||
32 | /VampireModelInterpretation_TypeInterpretation_FilteredTypes.java | ||
33 | /.Vampire2LogicMapper.java._trace | ||
34 | /.VampireHandler.java._trace | ||
35 | /.MonitoredVampireSolution.java._trace | ||
36 | /.SolverConfiguration.java._trace | ||
37 | /.VampireSolverException.java._trace | ||
38 | /.VampireSolutionModel.java._trace | ||
39 | /.VampireCallerWithTimeout.java._trace | ||
40 | /.Logic2VampireLanguageMapper_ScopeMapper.java._trace | ||
41 | /.Logic2VampireLanguageMapper_Containment.java._trace | ||
42 | /.Logic2VampireLanguageMapper_ContainmentMapper.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 deleted file mode 100644 index dc5ec788..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ /dev/null | |||
@@ -1,510 +0,0 @@ | |||
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_ContainmentMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; | ||
19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
20 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
24 | import com.google.common.base.Objects; | ||
25 | import com.google.common.collect.Iterables; | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral; | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference; | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct; | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals; | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall; | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration; | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition; | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl; | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf; | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral; | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; | ||
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; | ||
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
55 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
56 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl; | ||
57 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl; | ||
58 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
59 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
60 | import java.util.Arrays; | ||
61 | import java.util.Collections; | ||
62 | import java.util.HashMap; | ||
63 | import java.util.List; | ||
64 | import java.util.Map; | ||
65 | import java.util.function.Consumer; | ||
66 | import org.eclipse.emf.common.util.EList; | ||
67 | import org.eclipse.xtend.lib.annotations.AccessorType; | ||
68 | import org.eclipse.xtend.lib.annotations.Accessors; | ||
69 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
70 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
71 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
72 | import org.eclipse.xtext.xbase.lib.Extension; | ||
73 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
74 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
75 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
76 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
77 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
78 | import org.eclipse.xtext.xbase.lib.Pure; | ||
79 | |||
80 | @SuppressWarnings("all") | ||
81 | public class Logic2VampireLanguageMapper { | ||
82 | @Extension | ||
83 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
84 | |||
85 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
86 | |||
87 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
88 | private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); | ||
89 | |||
90 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
91 | private final Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(this); | ||
92 | |||
93 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
94 | private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); | ||
95 | |||
96 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
97 | private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this); | ||
98 | |||
99 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
100 | private final Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(this); | ||
101 | |||
102 | public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) { | ||
103 | VLSComment _createVLSComment = this.factory.createVLSComment(); | ||
104 | final Procedure1<VLSComment> _function = (VLSComment it) -> { | ||
105 | it.setComment("%This is an initial Test Comment"); | ||
106 | }; | ||
107 | final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function); | ||
108 | VampireModel _createVampireModel = this.factory.createVampireModel(); | ||
109 | final Procedure1<VampireModel> _function_1 = (VampireModel it) -> { | ||
110 | EList<VLSComment> _comments = it.getComments(); | ||
111 | _comments.add(initialComment); | ||
112 | }; | ||
113 | final VampireModel specification = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1); | ||
114 | Logic2VampireLanguageMapperTrace _logic2VampireLanguageMapperTrace = new Logic2VampireLanguageMapperTrace(); | ||
115 | final Procedure1<Logic2VampireLanguageMapperTrace> _function_2 = (Logic2VampireLanguageMapperTrace it) -> { | ||
116 | it.specification = specification; | ||
117 | }; | ||
118 | final Logic2VampireLanguageMapperTrace trace = ObjectExtensions.<Logic2VampireLanguageMapperTrace>operator_doubleArrow(_logic2VampireLanguageMapperTrace, _function_2); | ||
119 | boolean _isEmpty = problem.getTypes().isEmpty(); | ||
120 | boolean _not = (!_isEmpty); | ||
121 | if (_not) { | ||
122 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); | ||
123 | } | ||
124 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | ||
125 | final Function1<Relation, Boolean> _function_3 = (Relation it) -> { | ||
126 | Class<? extends Relation> _class = it.getClass(); | ||
127 | return Boolean.valueOf(Objects.equal(_class, RelationDefinitionImpl.class)); | ||
128 | }; | ||
129 | this.toTrace(IterableExtensions.<Relation>filter(problem.getRelations(), _function_3), trace); | ||
130 | final Consumer<Relation> _function_4 = (Relation it) -> { | ||
131 | Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper(); | ||
132 | this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper); | ||
133 | }; | ||
134 | problem.getRelations().forEach(_function_4); | ||
135 | this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); | ||
136 | this.scopeMapper.transformScope(problem.getTypes(), config, trace); | ||
137 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | ||
138 | final Consumer<ConstantDefinition> _function_5 = (ConstantDefinition it) -> { | ||
139 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); | ||
140 | }; | ||
141 | Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_5); | ||
142 | EList<Assertion> _assertions = problem.getAssertions(); | ||
143 | for (final Assertion assertion : _assertions) { | ||
144 | this.transformAssertion(assertion, trace); | ||
145 | } | ||
146 | return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace); | ||
147 | } | ||
148 | |||
149 | public void toTrace(final Iterable<Relation> relations, final Logic2VampireLanguageMapperTrace trace) { | ||
150 | final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList(); | ||
151 | for (final Relation rel : relations) { | ||
152 | { | ||
153 | final String[] nameArray = rel.getName().split(" "); | ||
154 | String relNameVar = ""; | ||
155 | int _length = nameArray.length; | ||
156 | boolean _equals = (_length == 3); | ||
157 | if (_equals) { | ||
158 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
159 | } else { | ||
160 | relNameVar = rel.getName(); | ||
161 | } | ||
162 | final String relName = relNameVar; | ||
163 | final RelationDefinition relDef = ((RelationDefinition) rel); | ||
164 | int _length_1 = ((Object[])Conversions.unwrapArray(rel.getParameters(), Object.class)).length; | ||
165 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length_1, true); | ||
166 | for (final Integer i : _doubleDotLessThan) { | ||
167 | { | ||
168 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
169 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
170 | it.setName(this.support.toIDMultiple("V", i.toString())); | ||
171 | }; | ||
172 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
173 | vars.add(v); | ||
174 | } | ||
175 | } | ||
176 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
177 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
178 | it.setConstant(this.support.toIDMultiple("r", relName)); | ||
179 | for (final VLSVariable v : vars) { | ||
180 | EList<VLSTerm> _terms = it.getTerms(); | ||
181 | VLSVariable _duplicate = this.support.duplicate(v); | ||
182 | _terms.add(_duplicate); | ||
183 | } | ||
184 | }; | ||
185 | final VLSFunction relFunc = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
186 | trace.relDef2Predicate.put(relDef, relFunc); | ||
187 | trace.predicate2RelDef.put(relFunc, relDef); | ||
188 | } | ||
189 | } | ||
190 | } | ||
191 | |||
192 | protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { | ||
193 | return null; | ||
194 | } | ||
195 | |||
196 | private HashMap<ConstantDeclaration, ConstantDefinition> collectConstantDefinitions(final LogicProblem problem) { | ||
197 | final HashMap<ConstantDeclaration, ConstantDefinition> res = new HashMap<ConstantDeclaration, ConstantDefinition>(); | ||
198 | final Function1<ConstantDefinition, Boolean> _function = (ConstantDefinition it) -> { | ||
199 | ConstantDeclaration _defines = it.getDefines(); | ||
200 | return Boolean.valueOf((_defines != null)); | ||
201 | }; | ||
202 | final Consumer<ConstantDefinition> _function_1 = (ConstantDefinition it) -> { | ||
203 | res.put(it.getDefines(), it); | ||
204 | }; | ||
205 | IterableExtensions.<ConstantDefinition>filter(Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class), _function).forEach(_function_1); | ||
206 | return res; | ||
207 | } | ||
208 | |||
209 | private HashMap<RelationDeclaration, RelationDefinition> collectRelationDefinitions(final LogicProblem problem) { | ||
210 | final HashMap<RelationDeclaration, RelationDefinition> res = new HashMap<RelationDeclaration, RelationDefinition>(); | ||
211 | final Function1<RelationDefinition, Boolean> _function = (RelationDefinition it) -> { | ||
212 | RelationDeclaration _defines = it.getDefines(); | ||
213 | return Boolean.valueOf((_defines != null)); | ||
214 | }; | ||
215 | final Consumer<RelationDefinition> _function_1 = (RelationDefinition it) -> { | ||
216 | res.put(it.getDefines(), it); | ||
217 | }; | ||
218 | IterableExtensions.<RelationDefinition>filter(Iterables.<RelationDefinition>filter(problem.getRelations(), RelationDefinition.class), _function).forEach(_function_1); | ||
219 | return res; | ||
220 | } | ||
221 | |||
222 | protected boolean transformAssertion(final Assertion assertion, final Logic2VampireLanguageMapperTrace trace) { | ||
223 | boolean _xblockexpression = false; | ||
224 | { | ||
225 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
226 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
227 | String _name = assertion.getName(); | ||
228 | String _plus = ("assertion_" + _name); | ||
229 | it.setName(this.support.toID(_plus)); | ||
230 | it.setFofRole("axiom"); | ||
231 | it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); | ||
232 | }; | ||
233 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
234 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
235 | _xblockexpression = _formulas.add(res); | ||
236 | } | ||
237 | return _xblockexpression; | ||
238 | } | ||
239 | |||
240 | protected VLSTerm _transformTerm(final BoolLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
241 | VLSTerm _xifexpression = null; | ||
242 | boolean _isValue = literal.isValue(); | ||
243 | boolean _equals = (_isValue == true); | ||
244 | if (_equals) { | ||
245 | _xifexpression = this.factory.createVLSTrue(); | ||
246 | } else { | ||
247 | _xifexpression = this.factory.createVLSFalse(); | ||
248 | } | ||
249 | return _xifexpression; | ||
250 | } | ||
251 | |||
252 | protected VLSTerm _transformTerm(final IntLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
253 | VLSInt _createVLSInt = this.factory.createVLSInt(); | ||
254 | final Procedure1<VLSInt> _function = (VLSInt it) -> { | ||
255 | it.setValue(Integer.valueOf(literal.getValue()).toString()); | ||
256 | }; | ||
257 | return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function); | ||
258 | } | ||
259 | |||
260 | protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
261 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
262 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { | ||
263 | it.setOperand(this.transformTerm(not.getOperand(), trace, variables)); | ||
264 | }; | ||
265 | return ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function); | ||
266 | } | ||
267 | |||
268 | protected VLSTerm _transformTerm(final And and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
269 | final Function1<Term, VLSTerm> _function = (Term it) -> { | ||
270 | return this.transformTerm(it, trace, variables); | ||
271 | }; | ||
272 | return this.support.unfoldAnd(ListExtensions.<Term, VLSTerm>map(and.getOperands(), _function)); | ||
273 | } | ||
274 | |||
275 | protected VLSTerm _transformTerm(final Or or, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
276 | final Function1<Term, VLSTerm> _function = (Term it) -> { | ||
277 | return this.transformTerm(it, trace, variables); | ||
278 | }; | ||
279 | return this.support.unfoldOr(ListExtensions.<Term, VLSTerm>map(or.getOperands(), _function)); | ||
280 | } | ||
281 | |||
282 | protected VLSTerm _transformTerm(final Impl impl, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
283 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
284 | final Procedure1<VLSImplies> _function = (VLSImplies it) -> { | ||
285 | it.setLeft(this.transformTerm(impl.getLeftOperand(), trace, variables)); | ||
286 | it.setRight(this.transformTerm(impl.getRightOperand(), trace, variables)); | ||
287 | }; | ||
288 | return ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function); | ||
289 | } | ||
290 | |||
291 | protected VLSTerm _transformTerm(final Iff iff, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
292 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
293 | final Procedure1<VLSEquivalent> _function = (VLSEquivalent it) -> { | ||
294 | it.setLeft(this.transformTerm(iff.getLeftOperand(), trace, variables)); | ||
295 | it.setRight(this.transformTerm(iff.getRightOperand(), trace, variables)); | ||
296 | }; | ||
297 | return ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function); | ||
298 | } | ||
299 | |||
300 | protected VLSTerm _transformTerm(final Equals equals, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
301 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
302 | final Procedure1<VLSEquality> _function = (VLSEquality it) -> { | ||
303 | it.setLeft(this.transformTerm(equals.getLeftOperand(), trace, variables)); | ||
304 | it.setRight(this.transformTerm(equals.getRightOperand(), trace, variables)); | ||
305 | }; | ||
306 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function); | ||
307 | } | ||
308 | |||
309 | protected VLSTerm _transformTerm(final Distinct distinct, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
310 | return this.support.unfoldDistinctTerms(this, distinct.getOperands(), trace, variables); | ||
311 | } | ||
312 | |||
313 | protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
314 | return this.support.createQuantifiedExpression(this, forall, trace, variables, true); | ||
315 | } | ||
316 | |||
317 | protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
318 | return this.support.createQuantifiedExpression(this, exists, trace, variables, false); | ||
319 | } | ||
320 | |||
321 | protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
322 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
323 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
324 | TypeReference _range = instanceOf.getRange(); | ||
325 | it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate).getConstant()); | ||
326 | EList<VLSTerm> _terms = it.getTerms(); | ||
327 | VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); | ||
328 | _terms.add(_transformTerm); | ||
329 | }; | ||
330 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
331 | } | ||
332 | |||
333 | protected VLSTerm _transformTerm(final SymbolicValue symbolicValue, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
334 | return this.transformSymbolicReference(symbolicValue.getSymbolicReference(), symbolicValue.getParameterSubstitutions(), trace, variables); | ||
335 | } | ||
336 | |||
337 | protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
338 | final String name = CollectionsUtil.<DefinedElement, String>lookup(referred, trace.definedElement2String); | ||
339 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
340 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
341 | it.setName(name); | ||
342 | }; | ||
343 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
344 | } | ||
345 | |||
346 | protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
347 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
348 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
349 | it.setName(this.support.toID(constant.getName())); | ||
350 | }; | ||
351 | final VLSConstant res = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
352 | return res; | ||
353 | } | ||
354 | |||
355 | protected VLSTerm _transformSymbolicReference(final ConstantDefinition constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
356 | return null; | ||
357 | } | ||
358 | |||
359 | protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
360 | return this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables)); | ||
361 | } | ||
362 | |||
363 | protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
364 | return null; | ||
365 | } | ||
366 | |||
367 | protected VLSTerm _transformSymbolicReference(final FunctionDefinition function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
368 | return null; | ||
369 | } | ||
370 | |||
371 | /** | ||
372 | * def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | ||
373 | * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
374 | * Map<Variable, VLSVariable> variables) { | ||
375 | * if (trace.relationDefinitions.containsKey(relation)) { | ||
376 | * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), | ||
377 | * parameterSubstitutions, trace, variables) | ||
378 | * } | ||
379 | * else { | ||
380 | * // if (relationMapper.transformToHostedField(relation, trace)) { | ||
381 | * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) | ||
382 | * // // R(a,b) => | ||
383 | * // // b in a.R | ||
384 | * // return createVLSSubset => [ | ||
385 | * // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) | ||
386 | * // it.rightOperand = createVLSJoin => [ | ||
387 | * // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) | ||
388 | * // it.rightOperand = createVLSReference => [it.referred = VLSRelation] | ||
389 | * // ] | ||
390 | * // ] | ||
391 | * // } else { | ||
392 | * // val target = createVLSJoin => [ | ||
393 | * // leftOperand = createVLSReference => [referred = trace.logicLanguage] | ||
394 | * // rightOperand = createVLSReference => [ | ||
395 | * // referred = relation.lookup(trace.relationDeclaration2Global) | ||
396 | * // ] | ||
397 | * // ] | ||
398 | * // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) | ||
399 | * // | ||
400 | * // return createVLSSubset => [ | ||
401 | * // leftOperand = source | ||
402 | * // rightOperand = target | ||
403 | * // ] | ||
404 | * // } | ||
405 | * } | ||
406 | * } | ||
407 | */ | ||
408 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
409 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
410 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
411 | Class<? extends Relation> _class = relation.getClass(); | ||
412 | boolean _equals = Objects.equal(_class, RelationDeclarationImpl.class); | ||
413 | if (_equals) { | ||
414 | it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); | ||
415 | } else { | ||
416 | it.setConstant(CollectionsUtil.<RelationDefinition, VLSFunction>lookup(((RelationDefinition) relation), trace.relDef2Predicate).getConstant()); | ||
417 | } | ||
418 | EList<VLSTerm> _terms = it.getTerms(); | ||
419 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { | ||
420 | return this.transformTerm(p, trace, variables); | ||
421 | }; | ||
422 | List<VLSTerm> _map = ListExtensions.<Term, VLSTerm>map(parameterSubstitutions, _function_1); | ||
423 | Iterables.<VLSTerm>addAll(_terms, _map); | ||
424 | }; | ||
425 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
426 | } | ||
427 | |||
428 | protected VLSTerm transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { | ||
429 | return _transformTypeReference(boolTypeReference, trace); | ||
430 | } | ||
431 | |||
432 | protected VLSTerm transformTerm(final Term and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
433 | if (and instanceof And) { | ||
434 | return _transformTerm((And)and, trace, variables); | ||
435 | } else if (and instanceof BoolLiteral) { | ||
436 | return _transformTerm((BoolLiteral)and, trace, variables); | ||
437 | } else if (and instanceof Distinct) { | ||
438 | return _transformTerm((Distinct)and, trace, variables); | ||
439 | } else if (and instanceof Equals) { | ||
440 | return _transformTerm((Equals)and, trace, variables); | ||
441 | } else if (and instanceof Exists) { | ||
442 | return _transformTerm((Exists)and, trace, variables); | ||
443 | } else if (and instanceof Forall) { | ||
444 | return _transformTerm((Forall)and, trace, variables); | ||
445 | } else if (and instanceof Iff) { | ||
446 | return _transformTerm((Iff)and, trace, variables); | ||
447 | } else if (and instanceof Impl) { | ||
448 | return _transformTerm((Impl)and, trace, variables); | ||
449 | } else if (and instanceof IntLiteral) { | ||
450 | return _transformTerm((IntLiteral)and, trace, variables); | ||
451 | } else if (and instanceof Not) { | ||
452 | return _transformTerm((Not)and, trace, variables); | ||
453 | } else if (and instanceof Or) { | ||
454 | return _transformTerm((Or)and, trace, variables); | ||
455 | } else if (and instanceof InstanceOf) { | ||
456 | return _transformTerm((InstanceOf)and, trace, variables); | ||
457 | } else if (and instanceof SymbolicValue) { | ||
458 | return _transformTerm((SymbolicValue)and, trace, variables); | ||
459 | } else { | ||
460 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
461 | Arrays.<Object>asList(and, trace, variables).toString()); | ||
462 | } | ||
463 | } | ||
464 | |||
465 | protected VLSTerm transformSymbolicReference(final SymbolicDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
466 | if (constant instanceof ConstantDeclaration) { | ||
467 | return _transformSymbolicReference((ConstantDeclaration)constant, parameterSubstitutions, trace, variables); | ||
468 | } else if (constant instanceof ConstantDefinition) { | ||
469 | return _transformSymbolicReference((ConstantDefinition)constant, parameterSubstitutions, trace, variables); | ||
470 | } else if (constant instanceof FunctionDeclaration) { | ||
471 | return _transformSymbolicReference((FunctionDeclaration)constant, parameterSubstitutions, trace, variables); | ||
472 | } else if (constant instanceof FunctionDefinition) { | ||
473 | return _transformSymbolicReference((FunctionDefinition)constant, parameterSubstitutions, trace, variables); | ||
474 | } else if (constant instanceof DefinedElement) { | ||
475 | return _transformSymbolicReference((DefinedElement)constant, parameterSubstitutions, trace, variables); | ||
476 | } else if (constant instanceof Relation) { | ||
477 | return _transformSymbolicReference((Relation)constant, parameterSubstitutions, trace, variables); | ||
478 | } else if (constant instanceof Variable) { | ||
479 | return _transformSymbolicReference((Variable)constant, parameterSubstitutions, trace, variables); | ||
480 | } else { | ||
481 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
482 | Arrays.<Object>asList(constant, parameterSubstitutions, trace, variables).toString()); | ||
483 | } | ||
484 | } | ||
485 | |||
486 | @Pure | ||
487 | public Logic2VampireLanguageMapper_ConstantMapper getConstantMapper() { | ||
488 | return this.constantMapper; | ||
489 | } | ||
490 | |||
491 | @Pure | ||
492 | public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() { | ||
493 | return this.containmentMapper; | ||
494 | } | ||
495 | |||
496 | @Pure | ||
497 | public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { | ||
498 | return this.relationMapper; | ||
499 | } | ||
500 | |||
501 | @Pure | ||
502 | public Logic2VampireLanguageMapper_ScopeMapper getScopeMapper() { | ||
503 | return this.scopeMapper; | ||
504 | } | ||
505 | |||
506 | @Pure | ||
507 | public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() { | ||
508 | return this.typeMapper; | ||
509 | } | ||
510 | } | ||
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 deleted file mode 100644 index 22df456b..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ /dev/null | |||
@@ -1,65 +0,0 @@ | |||
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.VLSConstant; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
17 | import java.util.HashMap; | ||
18 | import java.util.List; | ||
19 | import java.util.Map; | ||
20 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
21 | |||
22 | @SuppressWarnings("all") | ||
23 | public class Logic2VampireLanguageMapperTrace { | ||
24 | public VampireModel specification; | ||
25 | |||
26 | public VLSFofFormula logicLanguageBody; | ||
27 | |||
28 | public VLSTerm formula; | ||
29 | |||
30 | public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; | ||
31 | |||
32 | public Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>(); | ||
33 | |||
34 | public Object topLvlElementIsInInitialModel = null; | ||
35 | |||
36 | public Object topLevelType = null; | ||
37 | |||
38 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); | ||
39 | |||
40 | public final Map<VLSFunction, Type> predicate2Type = new HashMap<VLSFunction, Type>(); | ||
41 | |||
42 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); | ||
43 | |||
44 | public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>(); | ||
45 | |||
46 | public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>(); | ||
47 | |||
48 | public final List<VLSConstant> uniqueInstances = CollectionLiterals.<VLSConstant>newArrayList(); | ||
49 | |||
50 | public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions; | ||
51 | |||
52 | public Map<RelationDeclaration, RelationDefinition> relationDefinitions; | ||
53 | |||
54 | public Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap<RelationDeclaration, VLSFunction>(); | ||
55 | |||
56 | public Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap<VLSFunction, RelationDeclaration>(); | ||
57 | |||
58 | public Map<RelationDefinition, VLSFunction> relDef2Predicate = new HashMap<RelationDefinition, VLSFunction>(); | ||
59 | |||
60 | public Map<VLSFunction, RelationDefinition> predicate2RelDef = new HashMap<VLSFunction, RelationDefinition>(); | ||
61 | |||
62 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
63 | |||
64 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); | ||
65 | } | ||
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 deleted file mode 100644 index e5f42e73..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java +++ /dev/null | |||
@@ -1,34 +0,0 @@ | |||
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_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java deleted file mode 100644 index 2100b92f..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ /dev/null | |||
@@ -1,386 +0,0 @@ | |||
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.Logic2VampireLanguageMapper; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
20 | import com.google.common.base.Objects; | ||
21 | import com.google.common.collect.Iterables; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl; | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | ||
31 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
32 | import java.util.ArrayList; | ||
33 | import java.util.HashMap; | ||
34 | import java.util.List; | ||
35 | import java.util.Map; | ||
36 | import java.util.Set; | ||
37 | import org.eclipse.emf.common.util.EList; | ||
38 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
39 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
40 | import org.eclipse.xtext.xbase.lib.Extension; | ||
41 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
42 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
43 | |||
44 | @SuppressWarnings("all") | ||
45 | public class Logic2VampireLanguageMapper_ContainmentMapper { | ||
46 | @Extension | ||
47 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
48 | |||
49 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
50 | |||
51 | private final Logic2VampireLanguageMapper base; | ||
52 | |||
53 | private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> { | ||
54 | it.setName("A"); | ||
55 | })); | ||
56 | |||
57 | public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) { | ||
58 | this.base = base; | ||
59 | } | ||
60 | |||
61 | public void transformContainment(final VampireSolverConfiguration config, final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) { | ||
62 | final ContainmentHierarchy hierarchy = hierarchies.get(0); | ||
63 | final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); | ||
64 | final EList<Relation> relationsList = hierarchy.getContainmentRelations(); | ||
65 | final ArrayList<Object> toRemove = CollectionLiterals.<Object>newArrayList(); | ||
66 | for (final Relation l : relationsList) { | ||
67 | { | ||
68 | TypeReference _get = l.getParameters().get(1); | ||
69 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
70 | Type pointingTo = ((Type) _referred); | ||
71 | containmentListCopy.remove(pointingTo); | ||
72 | List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList(); | ||
73 | this.support.listSubtypes(pointingTo, allSubtypes); | ||
74 | for (final Type c : allSubtypes) { | ||
75 | containmentListCopy.remove(c); | ||
76 | } | ||
77 | } | ||
78 | } | ||
79 | Type topTermVar = containmentListCopy.get(0); | ||
80 | for (final Relation l_1 : relationsList) { | ||
81 | { | ||
82 | TypeReference _get = l_1.getParameters().get(0); | ||
83 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
84 | Type pointingFrom = ((Type) _referred); | ||
85 | boolean _contains = containmentListCopy.contains(pointingFrom); | ||
86 | if (_contains) { | ||
87 | topTermVar = pointingFrom; | ||
88 | } | ||
89 | } | ||
90 | } | ||
91 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString(); | ||
92 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); | ||
93 | trace.topLevelType = topTermVar; | ||
94 | boolean topLvlIsInInitModel = false; | ||
95 | String topLvlString = ""; | ||
96 | ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar); | ||
97 | listToCheck.addAll(topTermVar.getSubtypes()); | ||
98 | for (final Type c : listToCheck) { | ||
99 | Class<? extends Type> _class = c.getClass(); | ||
100 | boolean _equals = Objects.equal(_class, TypeDefinitionImpl.class); | ||
101 | if (_equals) { | ||
102 | int _length = ((Object[])Conversions.unwrapArray(((TypeDefinition) c).getElements(), Object.class)).length; | ||
103 | boolean _greaterThan = (_length > 1); | ||
104 | if (_greaterThan) { | ||
105 | throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model"); | ||
106 | } | ||
107 | EList<DefinedElement> _elements = ((TypeDefinition) c).getElements(); | ||
108 | for (final DefinedElement d : _elements) { | ||
109 | boolean _containsKey = trace.definedElement2String.containsKey(d); | ||
110 | if (_containsKey) { | ||
111 | topLvlIsInInitModel = true; | ||
112 | topLvlString = CollectionsUtil.<DefinedElement, String>lookup(d, trace.definedElement2String); | ||
113 | } | ||
114 | } | ||
115 | } | ||
116 | } | ||
117 | trace.topLvlElementIsInInitialModel = Boolean.valueOf(topLvlIsInInitModel); | ||
118 | final boolean topInIM = topLvlIsInInitModel; | ||
119 | final String topStr = topLvlString; | ||
120 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
121 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
122 | it.setName(this.support.toIDMultiple("containment_topLevel", topName)); | ||
123 | it.setFofRole("axiom"); | ||
124 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
125 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
126 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
127 | VLSVariable _duplicate = this.support.duplicate(this.variable); | ||
128 | _variables.add(_duplicate); | ||
129 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
130 | final Procedure1<VLSEquivalent> _function_2 = (VLSEquivalent it_2) -> { | ||
131 | it_2.setLeft(topTerm); | ||
132 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
133 | final Procedure1<VLSEquality> _function_3 = (VLSEquality it_3) -> { | ||
134 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
135 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
136 | final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> { | ||
137 | String _xifexpression = null; | ||
138 | if (topInIM) { | ||
139 | _xifexpression = topStr; | ||
140 | } else { | ||
141 | _xifexpression = "o1"; | ||
142 | } | ||
143 | it_4.setName(_xifexpression); | ||
144 | }; | ||
145 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4); | ||
146 | it_3.setRight(_doubleArrow); | ||
147 | }; | ||
148 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_3); | ||
149 | it_2.setRight(_doubleArrow); | ||
150 | }; | ||
151 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_2); | ||
152 | it_1.setOperand(_doubleArrow); | ||
153 | }; | ||
154 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
155 | it.setFofFormula(_doubleArrow); | ||
156 | }; | ||
157 | final VLSFofFormula contTop = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
158 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
159 | _formulas.add(contTop); | ||
160 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
161 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
162 | it.setName("A"); | ||
163 | }; | ||
164 | final VLSVariable varA = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
165 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
166 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it) -> { | ||
167 | it.setName("B"); | ||
168 | }; | ||
169 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
170 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
171 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it) -> { | ||
172 | it.setName("C"); | ||
173 | }; | ||
174 | final VLSVariable varC = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_3); | ||
175 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); | ||
176 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); | ||
177 | for (final Relation l_2 : relationsList) { | ||
178 | { | ||
179 | final VLSFunction rel = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate); | ||
180 | TypeReference _get = l_2.getParameters().get(1); | ||
181 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
182 | final Type toType = ((Type) _referred); | ||
183 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); | ||
184 | this.addToMap(type2cont, this.support.duplicate(toFunc), this.support.duplicate(rel, varList)); | ||
185 | ArrayList<Type> subTypes = CollectionLiterals.<Type>newArrayList(); | ||
186 | this.support.listSubtypes(toType, subTypes); | ||
187 | for (final Type c_1 : subTypes) { | ||
188 | this.addToMap(type2cont, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(c_1, trace.type2Predicate)), this.support.duplicate(rel, varList)); | ||
189 | } | ||
190 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
191 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
192 | it.setName(this.support.toIDMultiple("containment_noDup", rel.getConstant().toString())); | ||
193 | it.setFofRole("axiom"); | ||
194 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
195 | final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> { | ||
196 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
197 | VLSVariable _duplicate = this.support.duplicate(varA); | ||
198 | _variables.add(_duplicate); | ||
199 | EList<VLSTffTerm> _variables_1 = it_1.getVariables(); | ||
200 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | ||
201 | _variables_1.add(_duplicate_1); | ||
202 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
203 | final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> { | ||
204 | it_2.setLeft(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varA, varB))); | ||
205 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
206 | final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> { | ||
207 | VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier(); | ||
208 | final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> { | ||
209 | EList<VLSTffTerm> _variables_2 = it_4.getVariables(); | ||
210 | VLSVariable _duplicate_2 = this.support.duplicate(varC); | ||
211 | _variables_2.add(_duplicate_2); | ||
212 | EList<VLSTffTerm> _variables_3 = it_4.getVariables(); | ||
213 | VLSVariable _duplicate_3 = this.support.duplicate(varB); | ||
214 | _variables_3.add(_duplicate_3); | ||
215 | it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB))); | ||
216 | }; | ||
217 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier_1, _function_8); | ||
218 | it_3.setOperand(_doubleArrow); | ||
219 | }; | ||
220 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_7); | ||
221 | it_2.setRight(_doubleArrow); | ||
222 | }; | ||
223 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6); | ||
224 | it_1.setOperand(_doubleArrow); | ||
225 | }; | ||
226 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_5); | ||
227 | it.setFofFormula(_doubleArrow); | ||
228 | }; | ||
229 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); | ||
230 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
231 | _formulas_1.add(relFormula); | ||
232 | } | ||
233 | } | ||
234 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); | ||
235 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { | ||
236 | { | ||
237 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
238 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
239 | it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); | ||
240 | it.setFofRole("axiom"); | ||
241 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
242 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | ||
243 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
244 | VLSVariable _duplicate = this.support.duplicate(varA); | ||
245 | _variables.add(_duplicate); | ||
246 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
247 | final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> { | ||
248 | it_2.setLeft(this.support.duplicate(e.getKey(), varA)); | ||
249 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
250 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> { | ||
251 | EList<VLSTffTerm> _variables_1 = it_3.getVariables(); | ||
252 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | ||
253 | _variables_1.add(_duplicate_1); | ||
254 | int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; | ||
255 | boolean _greaterThan_1 = (_length_1 > 1); | ||
256 | if (_greaterThan_1) { | ||
257 | it_3.setOperand(this.makeUnique(e.getValue())); | ||
258 | } else { | ||
259 | it_3.setOperand(e.getValue().get(0)); | ||
260 | } | ||
261 | }; | ||
262 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); | ||
263 | it_2.setRight(_doubleArrow); | ||
264 | }; | ||
265 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6); | ||
266 | it_1.setOperand(_doubleArrow); | ||
267 | }; | ||
268 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); | ||
269 | it.setFofFormula(_doubleArrow); | ||
270 | }; | ||
271 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); | ||
272 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
273 | _formulas_1.add(relFormula); | ||
274 | } | ||
275 | } | ||
276 | final ArrayList<VLSVariable> variables = CollectionLiterals.<VLSVariable>newArrayList(); | ||
277 | final ArrayList<VLSFunction> disjunctionList = CollectionLiterals.<VLSFunction>newArrayList(); | ||
278 | final ArrayList<VLSTerm> conjunctionList = CollectionLiterals.<VLSTerm>newArrayList(); | ||
279 | for (int i = 1; (i <= config.contCycleLevel); i++) { | ||
280 | { | ||
281 | final int ind = i; | ||
282 | VLSVariable _createVLSVariable_3 = this.factory.createVLSVariable(); | ||
283 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it) -> { | ||
284 | String _string = Integer.toString(ind); | ||
285 | String _plus = ("V" + _string); | ||
286 | it.setName(_plus); | ||
287 | }; | ||
288 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_3, _function_4); | ||
289 | variables.add(_doubleArrow); | ||
290 | for (int j = 0; (j < i); j++) { | ||
291 | { | ||
292 | for (final Relation l_3 : relationsList) { | ||
293 | { | ||
294 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), | ||
295 | CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i)))); | ||
296 | disjunctionList.add(rel); | ||
297 | } | ||
298 | } | ||
299 | conjunctionList.add(this.support.unfoldOr(disjunctionList)); | ||
300 | disjunctionList.clear(); | ||
301 | } | ||
302 | } | ||
303 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
304 | final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> { | ||
305 | it.setName(this.support.toIDMultiple("containment_noCycle", Integer.toString(ind))); | ||
306 | it.setFofRole("axiom"); | ||
307 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
308 | final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_1) -> { | ||
309 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
310 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_2) -> { | ||
311 | EList<VLSTffTerm> _variables = it_2.getVariables(); | ||
312 | List<VLSVariable> _duplicate = this.support.duplicate(variables); | ||
313 | Iterables.<VLSTffTerm>addAll(_variables, _duplicate); | ||
314 | it_2.setOperand(this.support.unfoldAnd(conjunctionList)); | ||
315 | }; | ||
316 | VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); | ||
317 | it_1.setOperand(_doubleArrow_1); | ||
318 | }; | ||
319 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_6); | ||
320 | it.setFofFormula(_doubleArrow_1); | ||
321 | }; | ||
322 | final VLSFofFormula contCycleForm = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5); | ||
323 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
324 | _formulas_1.add(contCycleForm); | ||
325 | conjunctionList.clear(); | ||
326 | } | ||
327 | } | ||
328 | } | ||
329 | |||
330 | protected VLSTerm makeUnique(final List<VLSFunction> list) { | ||
331 | final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList(); | ||
332 | final List<VLSTerm> uniqueRels = CollectionLiterals.<VLSTerm>newArrayList(); | ||
333 | for (final VLSFunction t1 : list) { | ||
334 | { | ||
335 | for (final VLSFunction t2 : list) { | ||
336 | boolean _equals = Objects.equal(t1, t2); | ||
337 | if (_equals) { | ||
338 | final VLSFunction fct = this.support.duplicate(t2); | ||
339 | possibleNots.add(fct); | ||
340 | } else { | ||
341 | final VLSFunction op = this.support.duplicate(t2); | ||
342 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
343 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { | ||
344 | it.setOperand(op); | ||
345 | }; | ||
346 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function); | ||
347 | possibleNots.add(negFct); | ||
348 | } | ||
349 | } | ||
350 | uniqueRels.add(this.support.unfoldAnd(possibleNots)); | ||
351 | possibleNots.clear(); | ||
352 | } | ||
353 | } | ||
354 | return this.support.unfoldOr(uniqueRels); | ||
355 | } | ||
356 | |||
357 | protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) { | ||
358 | Object _xblockexpression = null; | ||
359 | { | ||
360 | boolean keyInMap = false; | ||
361 | VLSFunction existingKey = this.factory.createVLSFunction(); | ||
362 | Set<VLSFunction> _keySet = type2cont.keySet(); | ||
363 | for (final VLSFunction k : _keySet) { | ||
364 | boolean _equals = k.getConstant().equals(toFunc.getConstant()); | ||
365 | if (_equals) { | ||
366 | keyInMap = true; | ||
367 | existingKey = k; | ||
368 | } | ||
369 | } | ||
370 | Object _xifexpression = null; | ||
371 | if ((!keyInMap)) { | ||
372 | _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel)); | ||
373 | } else { | ||
374 | boolean _xifexpression_1 = false; | ||
375 | boolean _contains = type2cont.get(existingKey).contains(rel); | ||
376 | boolean _not = (!_contains); | ||
377 | if (_not) { | ||
378 | _xifexpression_1 = type2cont.get(existingKey).add(rel); | ||
379 | } | ||
380 | _xifexpression = Boolean.valueOf(_xifexpression_1); | ||
381 | } | ||
382 | _xblockexpression = _xifexpression; | ||
383 | } | ||
384 | return _xblockexpression; | ||
385 | } | ||
386 | } | ||
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 deleted file mode 100644 index 4c14e93e..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ /dev/null | |||
@@ -1,205 +0,0 @@ | |||
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.VLSAnd; | ||
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.VLSTffTerm; | ||
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 hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
22 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
23 | import java.util.ArrayList; | ||
24 | import java.util.Arrays; | ||
25 | import java.util.HashMap; | ||
26 | import java.util.List; | ||
27 | import java.util.Map; | ||
28 | import org.eclipse.emf.common.util.EList; | ||
29 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
30 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
31 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
32 | import org.eclipse.xtext.xbase.lib.Extension; | ||
33 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
34 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
35 | |||
36 | @SuppressWarnings("all") | ||
37 | public class Logic2VampireLanguageMapper_RelationMapper { | ||
38 | @Extension | ||
39 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
40 | |||
41 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
42 | |||
43 | private final Logic2VampireLanguageMapper base; | ||
44 | |||
45 | public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) { | ||
46 | this.base = base; | ||
47 | } | ||
48 | |||
49 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { | ||
50 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); | ||
51 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
52 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
53 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
54 | for (final Integer i : _doubleDotLessThan) { | ||
55 | { | ||
56 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
57 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
58 | it.setName(this.support.toIDMultiple("V", i.toString())); | ||
59 | }; | ||
60 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
61 | relVar2VLS.add(v); | ||
62 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
63 | final Type relType = ((ComplexTypeReference) _get).getReferred(); | ||
64 | final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v); | ||
65 | relVar2TypeDecComply.add(varTypeComply); | ||
66 | } | ||
67 | } | ||
68 | final String[] nameArray = r.getName().split(" "); | ||
69 | String relNameVar = ""; | ||
70 | int _length_1 = nameArray.length; | ||
71 | boolean _equals = (_length_1 == 3); | ||
72 | if (_equals) { | ||
73 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
74 | } else { | ||
75 | relNameVar = r.getName(); | ||
76 | } | ||
77 | final String relName = relNameVar; | ||
78 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
79 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
80 | it.setName(this.support.toIDMultiple("compliance", relName)); | ||
81 | it.setFofRole("axiom"); | ||
82 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
83 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
84 | for (final VLSVariable v : relVar2VLS) { | ||
85 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
86 | VLSVariable _duplicate = this.support.duplicate(v); | ||
87 | _variables.add(_duplicate); | ||
88 | } | ||
89 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
90 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
91 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
92 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
93 | it_3.setConstant(this.support.toIDMultiple("r", relName)); | ||
94 | for (final VLSVariable v_1 : relVar2VLS) { | ||
95 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
96 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); | ||
97 | _terms.add(_duplicate_1); | ||
98 | } | ||
99 | }; | ||
100 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
101 | trace.rel2Predicate.put(r, rel); | ||
102 | trace.predicate2Relation.put(rel, r); | ||
103 | it_2.setLeft(this.support.duplicate(rel)); | ||
104 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); | ||
105 | }; | ||
106 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
107 | it_1.setOperand(_doubleArrow); | ||
108 | }; | ||
109 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
110 | it.setFofFormula(_doubleArrow); | ||
111 | }; | ||
112 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
113 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
114 | _formulas.add(comply); | ||
115 | } | ||
116 | |||
117 | public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { | ||
118 | final Map<Variable, VLSVariable> relVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
119 | final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList(); | ||
120 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
121 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
122 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
123 | for (final Integer i : _doubleDotLessThan) { | ||
124 | { | ||
125 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
126 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
127 | it.setName(this.support.toIDMultiple("V", i.toString())); | ||
128 | }; | ||
129 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
130 | relVar2VLS.put(r.getVariables().get((i).intValue()), v); | ||
131 | vars.add(v); | ||
132 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
133 | final Type relType = ((ComplexTypeReference) _get).getReferred(); | ||
134 | final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v); | ||
135 | relVar2TypeDecComply.add(varTypeComply); | ||
136 | } | ||
137 | } | ||
138 | final String[] nameArray = r.getName().split(" "); | ||
139 | String relNameVar = ""; | ||
140 | int _length_1 = nameArray.length; | ||
141 | boolean _equals = (_length_1 == 3); | ||
142 | if (_equals) { | ||
143 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
144 | } else { | ||
145 | relNameVar = r.getName(); | ||
146 | } | ||
147 | final String relName = relNameVar; | ||
148 | final VLSTerm definition = mapper.transformTerm(r.getValue(), trace, relVar2VLS); | ||
149 | final VLSTerm compliance = this.support.unfoldAnd(relVar2TypeDecComply); | ||
150 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
151 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
152 | it.setLeft(compliance); | ||
153 | it.setRight(definition); | ||
154 | }; | ||
155 | final VLSAnd compDefn = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
156 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
157 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
158 | it.setName(this.support.toID(relName)); | ||
159 | it.setFofRole("axiom"); | ||
160 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
161 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
162 | for (final VLSVariable v : vars) { | ||
163 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
164 | VLSVariable _duplicate = this.support.duplicate(v); | ||
165 | _variables.add(_duplicate); | ||
166 | } | ||
167 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
168 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
169 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
170 | final Procedure1<VLSFunction> _function_4 = (VLSFunction it_3) -> { | ||
171 | it_3.setConstant(this.support.toIDMultiple("r", relName)); | ||
172 | for (final VLSVariable v_1 : vars) { | ||
173 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
174 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); | ||
175 | _terms.add(_duplicate_1); | ||
176 | } | ||
177 | }; | ||
178 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_4); | ||
179 | it_2.setLeft(this.support.duplicate(rel)); | ||
180 | it_2.setRight(compDefn); | ||
181 | }; | ||
182 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
183 | it_1.setOperand(_doubleArrow); | ||
184 | }; | ||
185 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
186 | it.setFofFormula(_doubleArrow); | ||
187 | }; | ||
188 | final VLSFofFormula relDef = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
189 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
190 | _formulas.add(relDef); | ||
191 | } | ||
192 | |||
193 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { | ||
194 | if (r instanceof RelationDeclaration) { | ||
195 | _transformRelation((RelationDeclaration)r, trace, mapper); | ||
196 | return; | ||
197 | } else if (r instanceof RelationDefinition) { | ||
198 | _transformRelation((RelationDefinition)r, trace, mapper); | ||
199 | return; | ||
200 | } else { | ||
201 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
202 | Arrays.<Object>asList(r, trace, mapper).toString()); | ||
203 | } | ||
204 | } | ||
205 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java deleted file mode 100644 index d6c90484..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ /dev/null | |||
@@ -1,302 +0,0 @@ | |||
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.Logic2VampireLanguageMapper; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
18 | import com.google.common.base.Objects; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
22 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
23 | import java.util.ArrayList; | ||
24 | import java.util.HashMap; | ||
25 | import java.util.List; | ||
26 | import java.util.Map; | ||
27 | import java.util.Set; | ||
28 | import org.eclipse.emf.common.util.EList; | ||
29 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
30 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
31 | import org.eclipse.xtext.xbase.lib.Extension; | ||
32 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
33 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
34 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
35 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
36 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
37 | |||
38 | @SuppressWarnings("all") | ||
39 | public class Logic2VampireLanguageMapper_ScopeMapper { | ||
40 | @Extension | ||
41 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
42 | |||
43 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
44 | |||
45 | private final Logic2VampireLanguageMapper base; | ||
46 | |||
47 | private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> { | ||
48 | it.setName("A"); | ||
49 | })); | ||
50 | |||
51 | public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) { | ||
52 | this.base = base; | ||
53 | } | ||
54 | |||
55 | public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | ||
56 | int elemsInIM = trace.definedElement2String.size(); | ||
57 | final int ABSOLUTE_MIN = 0; | ||
58 | final int ABSOLUTE_MAX = (Integer.MAX_VALUE - elemsInIM); | ||
59 | final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); | ||
60 | final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); | ||
61 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); | ||
62 | final boolean consistant = (GLOBAL_MAX >= GLOBAL_MIN); | ||
63 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { | ||
64 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant)); | ||
65 | if (consistant) { | ||
66 | for (final VLSConstant i : trace.uniqueInstances) { | ||
67 | localInstances.add(this.support.duplicate(i)); | ||
68 | } | ||
69 | this.makeFofFormula(localInstances, trace, true, null); | ||
70 | } else { | ||
71 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, true, null); | ||
72 | } | ||
73 | } | ||
74 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { | ||
75 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant); | ||
76 | if (consistant) { | ||
77 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); | ||
78 | } else { | ||
79 | this.makeFofFormula(localInstances, trace, false, null); | ||
80 | } | ||
81 | } | ||
82 | int i_1 = 1; | ||
83 | if ((((Boolean) trace.topLvlElementIsInInitialModel)).booleanValue()) { | ||
84 | i_1 = 0; | ||
85 | } | ||
86 | int minNum = (-1); | ||
87 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); | ||
88 | final Function1<Type, Boolean> _function = (Type it) -> { | ||
89 | boolean _equals = it.equals(trace.topLevelType); | ||
90 | return Boolean.valueOf((!_equals)); | ||
91 | }; | ||
92 | Iterable<Type> _filter = IterableExtensions.<Type>filter(config.typeScopes.minNewElementsByType.keySet(), _function); | ||
93 | for (final Type t : _filter) { | ||
94 | { | ||
95 | int numIniIntModel = 0; | ||
96 | Set<DefinedElement> _keySet = trace.definedElement2String.keySet(); | ||
97 | for (final DefinedElement elem : _keySet) { | ||
98 | EList<TypeDefinition> _definedInType = elem.getDefinedInType(); | ||
99 | for (final TypeDefinition tDefined : _definedInType) { | ||
100 | boolean _dfsSubtypeCheck = this.support.dfsSubtypeCheck(t, tDefined); | ||
101 | if (_dfsSubtypeCheck) { | ||
102 | int _numIniIntModel = numIniIntModel; | ||
103 | numIniIntModel = (_numIniIntModel + 1); | ||
104 | } | ||
105 | } | ||
106 | } | ||
107 | Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType); | ||
108 | int _minus = ((_lookup).intValue() - numIniIntModel); | ||
109 | minNum = _minus; | ||
110 | if ((minNum != 0)) { | ||
111 | this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); | ||
112 | startPoints.put(t, Integer.valueOf(i_1)); | ||
113 | int _i = i_1; | ||
114 | i_1 = (_i + minNum); | ||
115 | this.makeFofFormula(localInstances, trace, true, t); | ||
116 | } | ||
117 | } | ||
118 | } | ||
119 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | ||
120 | boolean _equals = it.equals(trace.topLevelType); | ||
121 | return Boolean.valueOf((!_equals)); | ||
122 | }; | ||
123 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(config.typeScopes.maxNewElementsByType.keySet(), _function_1); | ||
124 | for (final Type t_1 : _filter_1) { | ||
125 | { | ||
126 | int numIniIntModel = 0; | ||
127 | Set<DefinedElement> _keySet = trace.definedElement2String.keySet(); | ||
128 | for (final DefinedElement elem : _keySet) { | ||
129 | EList<TypeDefinition> _definedInType = elem.getDefinedInType(); | ||
130 | boolean _equals = Objects.equal(_definedInType, t_1); | ||
131 | if (_equals) { | ||
132 | int _numIniIntModel = numIniIntModel; | ||
133 | numIniIntModel = (_numIniIntModel + 1); | ||
134 | } | ||
135 | } | ||
136 | Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); | ||
137 | int maxNum = ((_lookup).intValue() - numIniIntModel); | ||
138 | boolean _contains = config.typeScopes.minNewElementsByType.keySet().contains(t_1); | ||
139 | if (_contains) { | ||
140 | Integer _lookup_1 = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType); | ||
141 | int _minus = ((_lookup_1).intValue() - numIniIntModel); | ||
142 | minNum = _minus; | ||
143 | } else { | ||
144 | minNum = 0; | ||
145 | } | ||
146 | if ((minNum != 0)) { | ||
147 | Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints); | ||
148 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); | ||
149 | } else { | ||
150 | localInstances.clear(); | ||
151 | } | ||
152 | int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + maxNum) - minNum)); | ||
153 | this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); | ||
154 | this.makeFofFormula(localInstances, trace, false, t_1); | ||
155 | } | ||
156 | } | ||
157 | final boolean DUPLICATES = config.uniquenessDuplicates; | ||
158 | final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; | ||
159 | int ind = 1; | ||
160 | if ((numInst != 0)) { | ||
161 | if (DUPLICATES) { | ||
162 | for (final VLSConstant e : trace.uniqueInstances) { | ||
163 | { | ||
164 | final int x = ind; | ||
165 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
166 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | ||
167 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); | ||
168 | it.setFofRole("axiom"); | ||
169 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); | ||
170 | }; | ||
171 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | ||
172 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
173 | _formulas.add(uniqueness); | ||
174 | ind++; | ||
175 | } | ||
176 | } | ||
177 | } else { | ||
178 | List<VLSConstant> _subList = trace.uniqueInstances.subList(0, (numInst - 1)); | ||
179 | for (final VLSConstant e_1 : _subList) { | ||
180 | { | ||
181 | final int x = ind; | ||
182 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
183 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | ||
184 | it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName())); | ||
185 | it.setFofRole("axiom"); | ||
186 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1)); | ||
187 | }; | ||
188 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | ||
189 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
190 | _formulas.add(uniqueness); | ||
191 | ind++; | ||
192 | } | ||
193 | } | ||
194 | } | ||
195 | } | ||
196 | } | ||
197 | |||
198 | protected void getInstanceConstants(final int endInd, final int startInd, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean clear, final boolean addToTrace) { | ||
199 | if (clear) { | ||
200 | list.clear(); | ||
201 | } | ||
202 | for (int i = startInd; (i < endInd); i++) { | ||
203 | { | ||
204 | final int num = (i + 1); | ||
205 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
206 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
207 | it.setName(("o" + Integer.valueOf(num))); | ||
208 | }; | ||
209 | final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
210 | if (addToTrace) { | ||
211 | trace.uniqueInstances.add(cst); | ||
212 | } | ||
213 | list.add(cst); | ||
214 | } | ||
215 | } | ||
216 | } | ||
217 | |||
218 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { | ||
219 | String nm = ""; | ||
220 | VLSTerm tm = null; | ||
221 | if ((type == null)) { | ||
222 | nm = "object"; | ||
223 | tm = this.support.topLevelTypeFunc(); | ||
224 | } else { | ||
225 | nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString(); | ||
226 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
227 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
228 | it.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate))); | ||
229 | it.setRight(this.support.topLevelTypeFunc()); | ||
230 | }; | ||
231 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
232 | tm = _doubleArrow; | ||
233 | } | ||
234 | final String name = nm; | ||
235 | final VLSTerm term = tm; | ||
236 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
237 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
238 | String _xifexpression = null; | ||
239 | if (minimum) { | ||
240 | _xifexpression = "min"; | ||
241 | } else { | ||
242 | _xifexpression = "max"; | ||
243 | } | ||
244 | it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); | ||
245 | it.setFofRole("axiom"); | ||
246 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
247 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
248 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
249 | VLSVariable _duplicate = this.support.duplicate(this.variable); | ||
250 | _variables.add(_duplicate); | ||
251 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
252 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
253 | if (minimum) { | ||
254 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { | ||
255 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
256 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { | ||
257 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
258 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { | ||
259 | it_4.setName(this.variable.getName()); | ||
260 | }; | ||
261 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); | ||
262 | it_3.setLeft(_doubleArrow_1); | ||
263 | it_3.setRight(i); | ||
264 | }; | ||
265 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); | ||
266 | }; | ||
267 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); | ||
268 | it_2.setRight(term); | ||
269 | } else { | ||
270 | it_2.setLeft(term); | ||
271 | final Function1<VLSTerm, VLSEquality> _function_5 = (VLSTerm i) -> { | ||
272 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
273 | final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> { | ||
274 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
275 | final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> { | ||
276 | it_4.setName(this.variable.getName()); | ||
277 | }; | ||
278 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_7); | ||
279 | it_3.setLeft(_doubleArrow_1); | ||
280 | it_3.setRight(i); | ||
281 | }; | ||
282 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6); | ||
283 | }; | ||
284 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_5))); | ||
285 | } | ||
286 | }; | ||
287 | VLSImplies _doubleArrow_1 = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
288 | it_1.setOperand(_doubleArrow_1); | ||
289 | }; | ||
290 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
291 | it.setFofFormula(_doubleArrow_1); | ||
292 | }; | ||
293 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
294 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
295 | _formulas.add(cstDec); | ||
296 | } | ||
297 | |||
298 | public void transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | ||
299 | _transformScope(types, config, trace); | ||
300 | return; | ||
301 | } | ||
302 | } | ||
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 deleted file mode 100644 index d757212a..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ /dev/null | |||
@@ -1,515 +0,0 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; | ||
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.ComplexTypeReference; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
27 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
28 | import java.util.ArrayList; | ||
29 | import java.util.Collection; | ||
30 | import java.util.HashMap; | ||
31 | import java.util.List; | ||
32 | import java.util.Map; | ||
33 | import java.util.concurrent.TimeUnit; | ||
34 | import okhttp3.MediaType; | ||
35 | import okhttp3.OkHttpClient; | ||
36 | import okhttp3.Request; | ||
37 | import okhttp3.RequestBody; | ||
38 | import okhttp3.Response; | ||
39 | import org.eclipse.emf.common.util.EList; | ||
40 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
41 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
42 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
43 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
44 | import org.eclipse.xtext.xbase.lib.Extension; | ||
45 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
46 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
47 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
48 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
49 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
50 | |||
51 | @SuppressWarnings("all") | ||
52 | public class Logic2VampireLanguageMapper_Support { | ||
53 | @Extension | ||
54 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
55 | |||
56 | protected String toIDMultiple(final String... ids) { | ||
57 | final Function1<String, String> _function = (String it) -> { | ||
58 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(it.split("\\s+"))), "_"); | ||
59 | }; | ||
60 | return IterableExtensions.join(ListExtensions.<String, String>map(((List<String>)Conversions.doWrapArray(ids)), _function), "_"); | ||
61 | } | ||
62 | |||
63 | protected String toID(final String ids) { | ||
64 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_"); | ||
65 | } | ||
66 | |||
67 | protected VLSVariable duplicate(final VLSVariable term) { | ||
68 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
69 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
70 | it.setName(term.getName()); | ||
71 | }; | ||
72 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
73 | } | ||
74 | |||
75 | protected VLSFunctionAsTerm duplicate(final VLSFunctionAsTerm term) { | ||
76 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | ||
77 | final Procedure1<VLSFunctionAsTerm> _function = (VLSFunctionAsTerm it) -> { | ||
78 | it.setFunctor(term.getFunctor()); | ||
79 | }; | ||
80 | return ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function); | ||
81 | } | ||
82 | |||
83 | protected VLSConstant duplicate(final VLSConstant term) { | ||
84 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
85 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
86 | it.setName(term.getName()); | ||
87 | }; | ||
88 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
89 | } | ||
90 | |||
91 | protected VLSFunction duplicate(final VLSFunction term) { | ||
92 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
93 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
94 | it.setConstant(term.getConstant()); | ||
95 | EList<VLSTerm> _terms = term.getTerms(); | ||
96 | for (final VLSTerm v : _terms) { | ||
97 | EList<VLSTerm> _terms_1 = it.getTerms(); | ||
98 | VLSVariable _duplicate = this.duplicate(((VLSVariable) v)); | ||
99 | _terms_1.add(_duplicate); | ||
100 | } | ||
101 | }; | ||
102 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
103 | } | ||
104 | |||
105 | protected VLSFunction duplicate(final VLSFunction term, final VLSVariable v) { | ||
106 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
107 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
108 | it.setConstant(term.getConstant()); | ||
109 | EList<VLSTerm> _terms = it.getTerms(); | ||
110 | VLSVariable _duplicate = this.duplicate(v); | ||
111 | _terms.add(_duplicate); | ||
112 | }; | ||
113 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
114 | } | ||
115 | |||
116 | protected VLSFunction duplicate(final VLSFunction term, final List<VLSVariable> vars) { | ||
117 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
118 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
119 | it.setConstant(term.getConstant()); | ||
120 | for (final VLSVariable v : vars) { | ||
121 | EList<VLSTerm> _terms = it.getTerms(); | ||
122 | VLSVariable _duplicate = this.duplicate(v); | ||
123 | _terms.add(_duplicate); | ||
124 | } | ||
125 | }; | ||
126 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
127 | } | ||
128 | |||
129 | protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { | ||
130 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
131 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
132 | it.setConstant(term.getConstant()); | ||
133 | EList<VLSTerm> _terms = it.getTerms(); | ||
134 | VLSFunctionAsTerm _duplicate = this.duplicate(v); | ||
135 | _terms.add(_duplicate); | ||
136 | }; | ||
137 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
138 | } | ||
139 | |||
140 | protected List<VLSVariable> duplicate(final List<VLSVariable> vars) { | ||
141 | ArrayList<VLSVariable> newList = CollectionLiterals.<VLSVariable>newArrayList(); | ||
142 | for (final VLSVariable v : vars) { | ||
143 | newList.add(this.duplicate(v)); | ||
144 | } | ||
145 | return newList; | ||
146 | } | ||
147 | |||
148 | protected VLSConstant toConstant(final VLSFunctionAsTerm term) { | ||
149 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
150 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
151 | it.setName(term.getFunctor()); | ||
152 | }; | ||
153 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
154 | } | ||
155 | |||
156 | protected VLSFunction topLevelTypeFunc() { | ||
157 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
158 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
159 | it.setConstant("object"); | ||
160 | EList<VLSTerm> _terms = it.getTerms(); | ||
161 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
162 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it_1) -> { | ||
163 | it_1.setName("A"); | ||
164 | }; | ||
165 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
166 | _terms.add(_doubleArrow); | ||
167 | }; | ||
168 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
169 | } | ||
170 | |||
171 | protected VLSFunction topLevelTypeFunc(final VLSVariable v) { | ||
172 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
173 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
174 | it.setConstant("object"); | ||
175 | EList<VLSTerm> _terms = it.getTerms(); | ||
176 | VLSVariable _duplicate = this.duplicate(v); | ||
177 | _terms.add(_duplicate); | ||
178 | }; | ||
179 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
180 | } | ||
181 | |||
182 | protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { | ||
183 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
184 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
185 | it.setConstant("object"); | ||
186 | EList<VLSTerm> _terms = it.getTerms(); | ||
187 | VLSFunctionAsTerm _duplicate = this.duplicate(v); | ||
188 | _terms.add(_duplicate); | ||
189 | }; | ||
190 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
191 | } | ||
192 | |||
193 | public VLSTerm establishUniqueness(final List<VLSConstant> terms, final VLSConstant t2) { | ||
194 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); | ||
195 | for (final VLSConstant t1 : terms) { | ||
196 | boolean _notEquals = (!Objects.equal(t1, t2)); | ||
197 | if (_notEquals) { | ||
198 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); | ||
199 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { | ||
200 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
201 | final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> { | ||
202 | it_1.setName(t2.getName()); | ||
203 | }; | ||
204 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); | ||
205 | it.setLeft(_doubleArrow); | ||
206 | VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); | ||
207 | final Procedure1<VLSConstant> _function_2 = (VLSConstant it_1) -> { | ||
208 | it_1.setName(t1.getName()); | ||
209 | }; | ||
210 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2); | ||
211 | it.setRight(_doubleArrow_1); | ||
212 | }; | ||
213 | final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | ||
214 | eqs.add(eq); | ||
215 | } | ||
216 | } | ||
217 | return this.unfoldAnd(eqs); | ||
218 | } | ||
219 | |||
220 | protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) { | ||
221 | int _size = operands.size(); | ||
222 | boolean _equals = (_size == 1); | ||
223 | if (_equals) { | ||
224 | return IterableExtensions.head(operands); | ||
225 | } else { | ||
226 | int _size_1 = operands.size(); | ||
227 | boolean _greaterThan = (_size_1 > 1); | ||
228 | if (_greaterThan) { | ||
229 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
230 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
231 | it.setLeft(IterableExtensions.head(operands)); | ||
232 | it.setRight(this.unfoldAnd(operands.subList(1, operands.size()))); | ||
233 | }; | ||
234 | return ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
235 | } else { | ||
236 | StringConcatenation _builder = new StringConcatenation(); | ||
237 | _builder.append("Logic operator with 0 operands!"); | ||
238 | throw new UnsupportedOperationException(_builder.toString()); | ||
239 | } | ||
240 | } | ||
241 | } | ||
242 | |||
243 | protected VLSTerm unfoldOr(final List<? extends VLSTerm> operands) { | ||
244 | int _size = operands.size(); | ||
245 | boolean _equals = (_size == 1); | ||
246 | if (_equals) { | ||
247 | return IterableExtensions.head(operands); | ||
248 | } else { | ||
249 | int _size_1 = operands.size(); | ||
250 | boolean _greaterThan = (_size_1 > 1); | ||
251 | if (_greaterThan) { | ||
252 | VLSOr _createVLSOr = this.factory.createVLSOr(); | ||
253 | final Procedure1<VLSOr> _function = (VLSOr it) -> { | ||
254 | it.setLeft(IterableExtensions.head(operands)); | ||
255 | it.setRight(this.unfoldOr(operands.subList(1, operands.size()))); | ||
256 | }; | ||
257 | return ObjectExtensions.<VLSOr>operator_doubleArrow(_createVLSOr, _function); | ||
258 | } else { | ||
259 | StringConcatenation _builder = new StringConcatenation(); | ||
260 | _builder.append("Logic operator with 0 operands!"); | ||
261 | throw new UnsupportedOperationException(_builder.toString()); | ||
262 | } | ||
263 | } | ||
264 | } | ||
265 | |||
266 | protected VLSTerm unfoldDistinctTerms(final Logic2VampireLanguageMapper m, final EList<Term> operands, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
267 | int _size = operands.size(); | ||
268 | boolean _equals = (_size == 1); | ||
269 | if (_equals) { | ||
270 | return m.transformTerm(IterableExtensions.<Term>head(operands), trace, variables); | ||
271 | } else { | ||
272 | int _size_1 = operands.size(); | ||
273 | boolean _greaterThan = (_size_1 > 1); | ||
274 | if (_greaterThan) { | ||
275 | int _size_2 = operands.size(); | ||
276 | int _size_3 = operands.size(); | ||
277 | int _multiply = (_size_2 * _size_3); | ||
278 | int _divide = (_multiply / 2); | ||
279 | final ArrayList<VLSTerm> notEquals = new ArrayList<VLSTerm>(_divide); | ||
280 | int _size_4 = operands.size(); | ||
281 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _size_4, true); | ||
282 | for (final Integer i : _doubleDotLessThan) { | ||
283 | int _size_5 = operands.size(); | ||
284 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(((i).intValue() + 1), _size_5, true); | ||
285 | for (final Integer j : _doubleDotLessThan_1) { | ||
286 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); | ||
287 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { | ||
288 | it.setLeft(m.transformTerm(operands.get((i).intValue()), trace, variables)); | ||
289 | it.setRight(m.transformTerm(operands.get((j).intValue()), trace, variables)); | ||
290 | }; | ||
291 | VLSInequality _doubleArrow = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | ||
292 | notEquals.add(_doubleArrow); | ||
293 | } | ||
294 | } | ||
295 | return this.unfoldAnd(notEquals); | ||
296 | } else { | ||
297 | StringConcatenation _builder = new StringConcatenation(); | ||
298 | _builder.append("Logic operator with 0 operands!"); | ||
299 | throw new UnsupportedOperationException(_builder.toString()); | ||
300 | } | ||
301 | } | ||
302 | } | ||
303 | |||
304 | /** | ||
305 | * def protected String toID(List<String> ids) { | ||
306 | * ids.map[it.split("\\s+").join("'")].join("'") | ||
307 | * } | ||
308 | */ | ||
309 | protected VLSTerm createQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables, final boolean isUniversal) { | ||
310 | VLSTerm _xblockexpression = null; | ||
311 | { | ||
312 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { | ||
313 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
314 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
315 | it.setName(this.toIDMultiple("V", v.getName())); | ||
316 | }; | ||
317 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
318 | }; | ||
319 | final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function); | ||
320 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
321 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); | ||
322 | for (final Variable variable : _quantifiedVariables) { | ||
323 | { | ||
324 | TypeReference _range = variable.getRange(); | ||
325 | final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), | ||
326 | CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap)); | ||
327 | typedefs.add(eq); | ||
328 | } | ||
329 | } | ||
330 | VLSTerm _xifexpression = null; | ||
331 | if (isUniversal) { | ||
332 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
333 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> { | ||
334 | EList<VLSTffTerm> _variables = it.getVariables(); | ||
335 | Collection<VLSVariable> _values = variableMap.values(); | ||
336 | Iterables.<VLSTffTerm>addAll(_variables, _values); | ||
337 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
338 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> { | ||
339 | it_1.setLeft(this.unfoldAnd(typedefs)); | ||
340 | it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | ||
341 | }; | ||
342 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
343 | it.setOperand(_doubleArrow); | ||
344 | }; | ||
345 | _xifexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
346 | } else { | ||
347 | VLSExistentialQuantifier _xblockexpression_1 = null; | ||
348 | { | ||
349 | typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | ||
350 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
351 | final Procedure1<VLSExistentialQuantifier> _function_2 = (VLSExistentialQuantifier it) -> { | ||
352 | EList<VLSTffTerm> _variables = it.getVariables(); | ||
353 | Collection<VLSVariable> _values = variableMap.values(); | ||
354 | Iterables.<VLSTffTerm>addAll(_variables, _values); | ||
355 | it.setOperand(this.unfoldAnd(typedefs)); | ||
356 | }; | ||
357 | _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2); | ||
358 | } | ||
359 | _xifexpression = _xblockexpression_1; | ||
360 | } | ||
361 | _xblockexpression = _xifexpression; | ||
362 | } | ||
363 | return _xblockexpression; | ||
364 | } | ||
365 | |||
366 | protected boolean dfsSupertypeCheck(final Type type, final Type type2) { | ||
367 | boolean _xifexpression = false; | ||
368 | boolean _isEmpty = type.getSupertypes().isEmpty(); | ||
369 | if (_isEmpty) { | ||
370 | return false; | ||
371 | } else { | ||
372 | boolean _xifexpression_1 = false; | ||
373 | boolean _contains = type.getSupertypes().contains(type2); | ||
374 | if (_contains) { | ||
375 | return true; | ||
376 | } else { | ||
377 | EList<Type> _supertypes = type.getSupertypes(); | ||
378 | for (final Type supertype : _supertypes) { | ||
379 | boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2); | ||
380 | if (_dfsSupertypeCheck) { | ||
381 | return true; | ||
382 | } | ||
383 | } | ||
384 | } | ||
385 | _xifexpression = _xifexpression_1; | ||
386 | } | ||
387 | return _xifexpression; | ||
388 | } | ||
389 | |||
390 | protected boolean dfsSubtypeCheck(final Type type, final Type type2) { | ||
391 | boolean _xifexpression = false; | ||
392 | boolean _isEmpty = type.getSubtypes().isEmpty(); | ||
393 | if (_isEmpty) { | ||
394 | return false; | ||
395 | } else { | ||
396 | boolean _xifexpression_1 = false; | ||
397 | boolean _contains = type.getSubtypes().contains(type2); | ||
398 | if (_contains) { | ||
399 | return true; | ||
400 | } else { | ||
401 | EList<Type> _subtypes = type.getSubtypes(); | ||
402 | for (final Type subtype : _subtypes) { | ||
403 | boolean _dfsSubtypeCheck = this.dfsSubtypeCheck(subtype, type2); | ||
404 | if (_dfsSubtypeCheck) { | ||
405 | return true; | ||
406 | } | ||
407 | } | ||
408 | } | ||
409 | _xifexpression = _xifexpression_1; | ||
410 | } | ||
411 | return _xifexpression; | ||
412 | } | ||
413 | |||
414 | protected void listSubtypes(final Type t, final List<Type> allSubtypes) { | ||
415 | EList<Type> _subtypes = t.getSubtypes(); | ||
416 | for (final Type subt : _subtypes) { | ||
417 | { | ||
418 | allSubtypes.add(subt); | ||
419 | this.listSubtypes(subt, allSubtypes); | ||
420 | } | ||
421 | } | ||
422 | } | ||
423 | |||
424 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { | ||
425 | HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1); | ||
426 | final Procedure1<HashMap<Variable, VLSVariable>> _function = (HashMap<Variable, VLSVariable> it) -> { | ||
427 | it.putAll(map2); | ||
428 | }; | ||
429 | return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function); | ||
430 | } | ||
431 | |||
432 | public String makeForm(final String formula, final BackendSolver solver, final int time) { | ||
433 | String _header = this.getHeader(); | ||
434 | String _plus = (_header + formula); | ||
435 | String _addOptions = this.addOptions(); | ||
436 | String _plus_1 = (_plus + _addOptions); | ||
437 | String _addSolver = this.addSolver(solver, time); | ||
438 | String _plus_2 = (_plus_1 + _addSolver); | ||
439 | String _addEnd = this.addEnd(); | ||
440 | return (_plus_2 + _addEnd); | ||
441 | } | ||
442 | |||
443 | public ArrayList<String> getSolverSpecs(final BackendSolver solver) { | ||
444 | if (solver != null) { | ||
445 | switch (solver) { | ||
446 | case CVC4: | ||
447 | return CollectionLiterals.<String>newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT"); | ||
448 | case DARWINFM: | ||
449 | return CollectionLiterals.<String>newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s"); | ||
450 | case EDARWIN: | ||
451 | return CollectionLiterals.<String>newArrayList("E-Darwin---1.5", | ||
452 | "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s"); | ||
453 | case GEOIII: | ||
454 | return CollectionLiterals.<String>newArrayList("Geo-III---2018C", | ||
455 | "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s"); | ||
456 | case IPROVER: | ||
457 | return CollectionLiterals.<String>newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s"); | ||
458 | case PARADOX: | ||
459 | return CollectionLiterals.<String>newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s"); | ||
460 | case VAMPIRE: | ||
461 | return CollectionLiterals.<String>newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s"); | ||
462 | case Z3: | ||
463 | return CollectionLiterals.<String>newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s"); | ||
464 | default: | ||
465 | break; | ||
466 | } | ||
467 | } | ||
468 | return null; | ||
469 | } | ||
470 | |||
471 | public String getHeader() { | ||
472 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n"; | ||
473 | } | ||
474 | |||
475 | public String addSpec(final String spec) { | ||
476 | return spec.replace("\n", "\\r\\n"); | ||
477 | } | ||
478 | |||
479 | public String addOptions() { | ||
480 | return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n"; | ||
481 | } | ||
482 | |||
483 | public String addSolver(final BackendSolver solver, final int time) { | ||
484 | final ArrayList<String> solverSpecs = this.getSolverSpecs(solver); | ||
485 | final String ID = solverSpecs.get(0); | ||
486 | final String cmd = solverSpecs.get(1); | ||
487 | return (((((((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"TimeLimit___" + ID) + | ||
488 | "\"\r\n\r\n") + Integer.valueOf(time)) + | ||
489 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___") + ID) + | ||
490 | "\"\r\n\r\n") + ID) + | ||
491 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + | ||
492 | "\"\r\n\r\n") + cmd) + "\r\n"); | ||
493 | } | ||
494 | |||
495 | public String addEnd() { | ||
496 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"; | ||
497 | } | ||
498 | |||
499 | public ArrayList<String> sendPost(final String formData) throws Exception { | ||
500 | final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(600, TimeUnit.SECONDS).readTimeout(350, | ||
501 | TimeUnit.SECONDS).build(); | ||
502 | final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); | ||
503 | final RequestBody body = RequestBody.create(mediaType, formData); | ||
504 | final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", | ||
505 | "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", | ||
506 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", | ||
507 | "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").addHeader("Accept", | ||
508 | "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", | ||
509 | "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", | ||
510 | "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", | ||
511 | "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build(); | ||
512 | final Response response = client.newCall(request).execute(); | ||
513 | return CollectionLiterals.<String>newArrayList(response.body().string().split("\n")); | ||
514 | } | ||
515 | } | ||
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 deleted file mode 100644 index 72fea6d3..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java +++ /dev/null | |||
@@ -1,339 +0,0 @@ | |||
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.VLSAnd; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; | ||
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.CollectionLiterals; | ||
31 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
32 | import org.eclipse.xtext.xbase.lib.Extension; | ||
33 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
34 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
35 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
36 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
37 | |||
38 | @SuppressWarnings("all") | ||
39 | public class Logic2VampireLanguageMapper_TypeMapper { | ||
40 | @Extension | ||
41 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
42 | |||
43 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
44 | |||
45 | private final Logic2VampireLanguageMapper base; | ||
46 | |||
47 | public Logic2VampireLanguageMapper_TypeMapper(final Logic2VampireLanguageMapper base) { | ||
48 | LogicproblemPackage.eINSTANCE.getClass(); | ||
49 | this.base = base; | ||
50 | } | ||
51 | |||
52 | protected boolean transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | ||
53 | boolean _xblockexpression = false; | ||
54 | { | ||
55 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
56 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
57 | it.setName("A"); | ||
58 | }; | ||
59 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
60 | int globalCounter = 0; | ||
61 | for (final Type type : types) { | ||
62 | { | ||
63 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
64 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
65 | int _length = type.getName().split(" ").length; | ||
66 | boolean _equals = (_length == 3); | ||
67 | if (_equals) { | ||
68 | it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0], type.getName().split(" ")[2])); | ||
69 | } else { | ||
70 | it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); | ||
71 | } | ||
72 | EList<VLSTerm> _terms = it.getTerms(); | ||
73 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
74 | _terms.add(_duplicate); | ||
75 | }; | ||
76 | final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
77 | trace.type2Predicate.put(type, typePred); | ||
78 | trace.predicate2Type.put(typePred, type); | ||
79 | } | ||
80 | } | ||
81 | final Function1<TypeDefinition, Boolean> _function_1 = (TypeDefinition it) -> { | ||
82 | boolean _isIsAbstract = it.isIsAbstract(); | ||
83 | return Boolean.valueOf((!_isIsAbstract)); | ||
84 | }; | ||
85 | Iterable<TypeDefinition> _filter = IterableExtensions.<TypeDefinition>filter(Iterables.<TypeDefinition>filter(types, TypeDefinition.class), _function_1); | ||
86 | for (final TypeDefinition type_1 : _filter) { | ||
87 | { | ||
88 | final int len = type_1.getName().length(); | ||
89 | boolean _equals = type_1.getName().substring((len - 4), len).equals("enum"); | ||
90 | final boolean isNotEnum = (!_equals); | ||
91 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); | ||
92 | EList<DefinedElement> _elements = type_1.getElements(); | ||
93 | for (final DefinedElement e : _elements) { | ||
94 | { | ||
95 | final String[] nameArray = e.getName().split(" "); | ||
96 | String relNameVar = ""; | ||
97 | int _length = nameArray.length; | ||
98 | boolean _equals_1 = (_length == 3); | ||
99 | if (_equals_1) { | ||
100 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
101 | } else { | ||
102 | relNameVar = e.getName(); | ||
103 | } | ||
104 | final String relName = relNameVar; | ||
105 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
106 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { | ||
107 | it.setConstant(this.support.toIDMultiple("e", relName)); | ||
108 | EList<VLSTerm> _terms = it.getTerms(); | ||
109 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
110 | _terms.add(_duplicate); | ||
111 | }; | ||
112 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2); | ||
113 | trace.element2Predicate.put(e, enumElemPred); | ||
114 | } | ||
115 | } | ||
116 | final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList(); | ||
117 | final List<VLSTerm> typeDefs = CollectionLiterals.<VLSTerm>newArrayList(); | ||
118 | EList<DefinedElement> _elements_1 = type_1.getElements(); | ||
119 | for (final DefinedElement t1 : _elements_1) { | ||
120 | { | ||
121 | EList<DefinedElement> _elements_2 = type_1.getElements(); | ||
122 | for (final DefinedElement t2 : _elements_2) { | ||
123 | boolean _equals_1 = Objects.equal(t1, t2); | ||
124 | if (_equals_1) { | ||
125 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | ||
126 | possibleNots.add(fct); | ||
127 | } else { | ||
128 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | ||
129 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
130 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | ||
131 | it.setOperand(op); | ||
132 | }; | ||
133 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | ||
134 | possibleNots.add(negFct); | ||
135 | } | ||
136 | } | ||
137 | typeDefs.add(this.support.unfoldAnd(possibleNots)); | ||
138 | possibleNots.clear(); | ||
139 | } | ||
140 | } | ||
141 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
142 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | ||
143 | it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString())); | ||
144 | it.setFofRole("axiom"); | ||
145 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
146 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | ||
147 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
148 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
149 | _variables.add(_duplicate); | ||
150 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
151 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | ||
152 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); | ||
153 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
154 | final Procedure1<VLSAnd> _function_5 = (VLSAnd it_3) -> { | ||
155 | it_3.setLeft(this.support.topLevelTypeFunc(variable)); | ||
156 | it_3.setRight(this.support.unfoldOr(typeDefs)); | ||
157 | }; | ||
158 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_5); | ||
159 | it_2.setRight(_doubleArrow); | ||
160 | }; | ||
161 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
162 | it_1.setOperand(_doubleArrow); | ||
163 | }; | ||
164 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); | ||
165 | it.setFofFormula(_doubleArrow); | ||
166 | }; | ||
167 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | ||
168 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
169 | _formulas.add(res); | ||
170 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { | ||
171 | { | ||
172 | final int num = (i + 1); | ||
173 | final int index = (i - globalCounter); | ||
174 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | ||
175 | final Procedure1<VLSFunctionAsTerm> _function_3 = (VLSFunctionAsTerm it) -> { | ||
176 | it.setFunctor(("eo" + Integer.valueOf(num))); | ||
177 | }; | ||
178 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3); | ||
179 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); | ||
180 | final VLSConstant cst = this.support.toConstant(cstTerm); | ||
181 | trace.uniqueInstances.add(cst); | ||
182 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
183 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
184 | String _xifexpression = null; | ||
185 | if (isNotEnum) { | ||
186 | _xifexpression = "definedType"; | ||
187 | } else { | ||
188 | _xifexpression = "enumScope"; | ||
189 | } | ||
190 | it.setName(this.support.toIDMultiple(_xifexpression, CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), | ||
191 | type_1.getElements().get(index).getName().split(" ")[0])); | ||
192 | it.setFofRole("axiom"); | ||
193 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
194 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | ||
195 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
196 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
197 | _variables.add(_duplicate); | ||
198 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
199 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { | ||
200 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
201 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { | ||
202 | it_3.setLeft(this.support.duplicate(variable)); | ||
203 | it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); | ||
204 | }; | ||
205 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); | ||
206 | it_2.setLeft(_doubleArrow); | ||
207 | it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); | ||
208 | }; | ||
209 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); | ||
210 | it_1.setOperand(_doubleArrow); | ||
211 | }; | ||
212 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); | ||
213 | it.setFofFormula(_doubleArrow); | ||
214 | }; | ||
215 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); | ||
216 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
217 | _formulas_1.add(enumScope); | ||
218 | } | ||
219 | } | ||
220 | int _globalCounter = globalCounter; | ||
221 | int _size = type_1.getElements().size(); | ||
222 | globalCounter = (_globalCounter + _size); | ||
223 | } | ||
224 | } | ||
225 | final Function1<Type, Boolean> _function_2 = (Type it) -> { | ||
226 | boolean _isIsAbstract = it.isIsAbstract(); | ||
227 | return Boolean.valueOf((!_isIsAbstract)); | ||
228 | }; | ||
229 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_2); | ||
230 | for (final Type t1 : _filter_1) { | ||
231 | { | ||
232 | for (final Type t2 : types) { | ||
233 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { | ||
234 | trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | ||
235 | } else { | ||
236 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
237 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { | ||
238 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | ||
239 | }; | ||
240 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); | ||
241 | trace.type2PossibleNot.put(t2, _doubleArrow); | ||
242 | } | ||
243 | } | ||
244 | Collection<VLSTerm> _values = trace.type2PossibleNot.values(); | ||
245 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
246 | trace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); | ||
247 | trace.type2PossibleNot.clear(); | ||
248 | } | ||
249 | } | ||
250 | final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList(); | ||
251 | for (final Type t : types) { | ||
252 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
253 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { | ||
254 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate))); | ||
255 | }; | ||
256 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); | ||
257 | type2Not.add(_doubleArrow); | ||
258 | } | ||
259 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
260 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
261 | it.setName("notObjectHandler"); | ||
262 | it.setFofRole("axiom"); | ||
263 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
264 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | ||
265 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
266 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
267 | _variables.add(_duplicate); | ||
268 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
269 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { | ||
270 | VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); | ||
271 | final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> { | ||
272 | it_3.setOperand(this.support.topLevelTypeFunc()); | ||
273 | }; | ||
274 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_7); | ||
275 | it_2.setLeft(_doubleArrow_1); | ||
276 | it_2.setRight(this.support.unfoldAnd(type2Not)); | ||
277 | }; | ||
278 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); | ||
279 | it_1.setOperand(_doubleArrow_1); | ||
280 | }; | ||
281 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); | ||
282 | it.setFofFormula(_doubleArrow_1); | ||
283 | }; | ||
284 | final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_4); | ||
285 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
286 | _formulas.add(notObj); | ||
287 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
288 | final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> { | ||
289 | it.setName("inheritanceHierarchyHandler"); | ||
290 | it.setFofRole("axiom"); | ||
291 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
292 | final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> { | ||
293 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
294 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
295 | _variables.add(_duplicate); | ||
296 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
297 | final Procedure1<VLSEquivalent> _function_7 = (VLSEquivalent it_2) -> { | ||
298 | it_2.setLeft(this.support.topLevelTypeFunc()); | ||
299 | Collection<VLSTerm> _values = trace.type2And.values(); | ||
300 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); | ||
301 | it_2.setRight(this.support.unfoldOr(reversedList)); | ||
302 | }; | ||
303 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_7); | ||
304 | it_1.setOperand(_doubleArrow_1); | ||
305 | }; | ||
306 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_6); | ||
307 | it.setFofFormula(_doubleArrow_1); | ||
308 | }; | ||
309 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5); | ||
310 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
311 | _xblockexpression = _formulas_1.add(hierarch); | ||
312 | } | ||
313 | return _xblockexpression; | ||
314 | } | ||
315 | |||
316 | protected void transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | ||
317 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
318 | } | ||
319 | |||
320 | protected void getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { | ||
321 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
322 | } | ||
323 | |||
324 | protected void getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { | ||
325 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
326 | } | ||
327 | |||
328 | protected VLSConstant transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { | ||
329 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
330 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
331 | it.setName(referred.getName()); | ||
332 | }; | ||
333 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
334 | } | ||
335 | |||
336 | protected void getTypeInterpreter() { | ||
337 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
338 | } | ||
339 | } | ||
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 deleted file mode 100644 index 1e08c8ad..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java +++ /dev/null | |||
@@ -1,5 +0,0 @@ | |||
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/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java deleted file mode 100644 index 9fb23c71..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java +++ /dev/null | |||
@@ -1,42 +0,0 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; | ||
10 | import org.eclipse.emf.common.util.EList; | ||
11 | import org.eclipse.xtext.xbase.lib.Extension; | ||
12 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
13 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
14 | |||
15 | @SuppressWarnings("all") | ||
16 | public class Vampire2LogicMapper { | ||
17 | @Extension | ||
18 | private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE; | ||
19 | |||
20 | public ModelResult transformOutput(final LogicProblem problem, final int requiredNumberOfSolution, final MonitoredVampireSolution monitoredVampireSolution, final Logic2VampireLanguageMapperTrace trace, final long transformationTime) { | ||
21 | ModelResult _createModelResult = this.resultFactory.createModelResult(); | ||
22 | final Procedure1<ModelResult> _function = (ModelResult it) -> { | ||
23 | it.setProblem(problem); | ||
24 | EList<Object> _representation = it.getRepresentation(); | ||
25 | VampireModel _generatedModel = monitoredVampireSolution.getGeneratedModel(); | ||
26 | _representation.add(_generatedModel); | ||
27 | it.setTrace(trace); | ||
28 | it.setStatistics(this.transformStatistics(monitoredVampireSolution, transformationTime)); | ||
29 | }; | ||
30 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function); | ||
31 | } | ||
32 | |||
33 | public Statistics transformStatistics(final MonitoredVampireSolution solution, final long transformationTime) { | ||
34 | Statistics _createStatistics = this.resultFactory.createStatistics(); | ||
35 | final Procedure1<Statistics> _function = (Statistics it) -> { | ||
36 | long _solverTime = solution.getSolverTime(); | ||
37 | it.setSolverTime(((int) _solverTime)); | ||
38 | it.setTransformationTime(((int) transformationTime)); | ||
39 | }; | ||
40 | return ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function); | ||
41 | } | ||
42 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java deleted file mode 100644 index 39773357..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java +++ /dev/null | |||
@@ -1,82 +0,0 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
7 | import com.google.common.base.Objects; | ||
8 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | ||
9 | import java.io.BufferedReader; | ||
10 | import java.io.FileReader; | ||
11 | import java.util.List; | ||
12 | import org.eclipse.emf.common.util.URI; | ||
13 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
14 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
15 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
16 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
17 | |||
18 | @SuppressWarnings("all") | ||
19 | public class VampireHandler { | ||
20 | public MonitoredVampireSolution callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) { | ||
21 | try { | ||
22 | final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; | ||
23 | final String VAMPNAME = "vampire.exe"; | ||
24 | final String VAMPLOC = (VAMPDIR + VAMPNAME); | ||
25 | final String CVC4DIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; | ||
26 | final String CVC4NAME = "vampire.exe"; | ||
27 | final String CVC4LOC = (CVC4DIR + CVC4NAME); | ||
28 | final String CMD = "cmd /c "; | ||
29 | final String TEMPNAME = "TEMP.tptp"; | ||
30 | final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.minNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + | ||
31 | ".tptp"); | ||
32 | final String PATH = "C:/cygwin64/bin"; | ||
33 | final URI wsURI = workspace.getWorkspaceURI(); | ||
34 | final String tempLoc = (wsURI + TEMPNAME); | ||
35 | String _plus = (wsURI + SOLNNAME); | ||
36 | final String solnLoc = (_plus + " "); | ||
37 | String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); | ||
38 | long startTime = (-((long) 1)); | ||
39 | long solverTime = (-((long) 1)); | ||
40 | Process p = null; | ||
41 | boolean _equals = Objects.equal(configuration.solver, BackendSolver.LOCVAMP); | ||
42 | if (_equals) { | ||
43 | String OPTION = " --mode casc_sat "; | ||
44 | if ((configuration.runtimeLimit != (-1))) { | ||
45 | OPTION = (((OPTION + "-t ") + Integer.valueOf(configuration.runtimeLimit)) + " "); | ||
46 | } | ||
47 | startTime = System.currentTimeMillis(); | ||
48 | p = Runtime.getRuntime().exec((((((CMD + VAMPLOC) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class))); | ||
49 | p.waitFor(); | ||
50 | long _currentTimeMillis = System.currentTimeMillis(); | ||
51 | long _minus = (_currentTimeMillis - startTime); | ||
52 | solverTime = _minus; | ||
53 | } | ||
54 | boolean _equals_1 = Objects.equal(configuration.solver, BackendSolver.CVC4); | ||
55 | if (_equals_1) { | ||
56 | String OPTION_1 = " SAT "; | ||
57 | if ((configuration.runtimeLimit != (-1))) { | ||
58 | OPTION_1 = ((" " + Integer.valueOf(configuration.runtimeLimit)) + OPTION_1); | ||
59 | } | ||
60 | InputOutput.<String>println((((((CMD + CVC4LOC) + tempLoc) + OPTION_1) + " > ") + solnLoc)); | ||
61 | p = Runtime.getRuntime().exec((((((CMD + CVC4LOC) + tempLoc) + OPTION_1) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class))); | ||
62 | p.waitFor(); | ||
63 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
64 | long _minus_1 = (_currentTimeMillis_1 - startTime); | ||
65 | solverTime = _minus_1; | ||
66 | } | ||
67 | FileReader _fileReader = new FileReader(solnLoc); | ||
68 | final BufferedReader reader = new BufferedReader(_fileReader); | ||
69 | final List<String> output = CollectionLiterals.<String>newArrayList(); | ||
70 | String line = ""; | ||
71 | while ((!Objects.equal((line = reader.readLine()), null))) { | ||
72 | boolean _equals_2 = Objects.equal(line, "Finite Model Found!"); | ||
73 | if (_equals_2) { | ||
74 | return new MonitoredVampireSolution(solverTime, null, true); | ||
75 | } | ||
76 | } | ||
77 | return new MonitoredVampireSolution(solverTime, null, false); | ||
78 | } catch (Throwable _e) { | ||
79 | throw Exceptions.sneakyThrow(_e); | ||
80 | } | ||
81 | } | ||
82 | } | ||
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 deleted file mode 100644 index 507831fa..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java +++ /dev/null | |||
@@ -1,5 +0,0 @@ | |||
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 deleted file mode 100644 index aff0dc9d..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java +++ /dev/null | |||
@@ -1,7 +0,0 @@ | |||
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 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java deleted file mode 100644 index b96df82a..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java +++ /dev/null | |||
@@ -1,19 +0,0 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import java.util.List; | ||
4 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
5 | |||
6 | @SuppressWarnings("all") | ||
7 | public class VampireSolverException extends Exception { | ||
8 | public VampireSolverException(final String s) { | ||
9 | super(s); | ||
10 | } | ||
11 | |||
12 | public VampireSolverException(final String s, final Exception e) { | ||
13 | super(s, e); | ||
14 | } | ||
15 | |||
16 | public VampireSolverException(final String s, final List<String> errors, final Exception e) { | ||
17 | super(((s + "\n") + IterableExtensions.join(errors, "\n")), e); | ||
18 | } | ||
19 | } | ||