diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-21 17:14:25 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:21 -0400 |
commit | 7379cc66fc3cc3b635df45072afc3dec42997c76 (patch) | |
tree | bd95befcd89d1e2fccc49630b2ecdf4f2b683f11 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner | |
parent | VAMPIRE: complete data collection and code setup (diff) | |
download | VIATRA-Generator-7379cc66fc3cc3b635df45072afc3dec42997c76.tar.gz VIATRA-Generator-7379cc66fc3cc3b635df45072afc3dec42997c76.tar.zst VIATRA-Generator-7379cc66fc3cc3b635df45072afc3dec42997c76.zip |
mid-measurement push
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner')
19 files changed, 129 insertions, 22 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 4c2f1952..1fda24d9 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 | |||
@@ -24,7 +24,8 @@ enum BackendSolver { | |||
24 | IPROVER, | 24 | IPROVER, |
25 | PARADOX, | 25 | PARADOX, |
26 | VAMPIRE, | 26 | VAMPIRE, |
27 | Z3 | 27 | Z3, |
28 | LOCVAMP | ||
28 | //add needed things | 29 | //add needed things |
29 | } | 30 | } |
30 | 31 | ||
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 9ec08163..042caa86 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 | |||
@@ -20,6 +20,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | |||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
22 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 22 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl | ||
23 | 24 | ||
24 | class VampireSolver extends LogicReasoner { | 25 | class VampireSolver extends LogicReasoner { |
25 | 26 | ||
@@ -128,17 +129,17 @@ class VampireSolver extends LogicReasoner { | |||
128 | it.name = "satOut" | 129 | it.name = "satOut" |
129 | it.value = satOut | 130 | it.value = satOut |
130 | ] | 131 | ] |
131 | it.entries += createRealStatisticEntry => [ | 132 | it.entries += createStringStatisticEntry => [ |
132 | it.name = "satTime" | 133 | it.name = "satTime" |
133 | it.value = Double.parseDouble(satTime) | 134 | it.value = satTime |
134 | ] | 135 | ] |
135 | it.entries += createStringStatisticEntry => [ | 136 | it.entries += createStringStatisticEntry => [ |
136 | it.name = "modOut" | 137 | it.name = "modOut" |
137 | it.value = modOut | 138 | it.value = modOut |
138 | ] | 139 | ] |
139 | it.entries += createRealStatisticEntry => [ | 140 | it.entries += createStringStatisticEntry => [ |
140 | it.name = "modTime" | 141 | it.name = "modTime" |
141 | it.value = Double.parseDouble(modTime) | 142 | it.value = modTime |
142 | ] | 143 | ] |
143 | 144 | ||
144 | ] | 145 | ] |
@@ -148,6 +149,7 @@ class VampireSolver extends LogicReasoner { | |||
148 | } else { | 149 | } else { |
149 | 150 | ||
150 | // Start: Solving .tptp problem | 151 | // Start: Solving .tptp problem |
152 | println() | ||
151 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | 153 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) |
152 | // Finish: Solving .tptp problem | 154 | // Finish: Solving .tptp problem |
153 | // Start: Vampire -> Logic mapping | 155 | // Start: Vampire -> Logic mapping |
@@ -159,7 +161,44 @@ class VampireSolver extends LogicReasoner { | |||
159 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | 161 | val backTransformationTime = System.currentTimeMillis - backTransformationStart |
160 | // Finish: Vampire -> Logic Mapping | 162 | // Finish: Vampire -> Logic Mapping |
161 | // print(vampSol.generatedModel.tfformulas.size) | 163 | // print(vampSol.generatedModel.tfformulas.size) |
162 | return logicResult // currently only a ModelResult | 164 | |
165 | // return logicResult // currently only a ModelResult | ||
166 | |||
167 | var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl] | ||
168 | // | ||
169 | var modOut = "no" | ||
170 | if(model.length >0){ | ||
171 | modOut = "FiniteModel" | ||
172 | } | ||
173 | |||
174 | val realModOut=modOut | ||
175 | |||
176 | |||
177 | return createModelResult => [ | ||
178 | it.problem = null | ||
179 | it.representation += createVampireModel => [] | ||
180 | it.trace = trace | ||
181 | it.statistics = createStatistics => [ | ||
182 | it.transformationTime = transformationTime as int | ||
183 | it.entries += createStringStatisticEntry => [ | ||
184 | it.name = "satOut" | ||
185 | it.value = "-" | ||
186 | ] | ||
187 | it.entries += createStringStatisticEntry => [ | ||
188 | it.name = "satTime" | ||
189 | it.value = "-" | ||
190 | ] | ||
191 | it.entries += createStringStatisticEntry => [ | ||
192 | it.name = "modOut" | ||
193 | it.value = realModOut | ||
194 | ] | ||
195 | it.entries += createStringStatisticEntry => [ | ||
196 | it.name = "modTime" | ||
197 | it.value = (vampSol.solverTime/1000.0).toString | ||
198 | ] | ||
199 | |||
200 | ] | ||
201 | ] | ||
163 | } | 202 | } |
164 | } | 203 | } |
165 | return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, | 204 | 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/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend index 6d301442..c277759a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | |||
@@ -54,7 +54,7 @@ class VampireHandler { | |||
54 | val TEMPNAME = "TEMP.tptp" | 54 | val TEMPNAME = "TEMP.tptp" |
55 | // val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + | 55 | // val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + |
56 | // "_" + configuration.iteration + ".tptp" | 56 | // "_" + configuration.iteration + ".tptp" |
57 | val SOLNNAME = "solution" + "_" + configuration.typeScopes.maxNewElements + "_" + configuration.iteration + | 57 | val SOLNNAME = "solution" + "_" + configuration.typeScopes.minNewElements + "_" + configuration.iteration + |
58 | ".tptp" | 58 | ".tptp" |
59 | val PATH = "C:/cygwin64/bin" | 59 | val PATH = "C:/cygwin64/bin" |
60 | 60 | ||
@@ -70,7 +70,7 @@ class VampireHandler { | |||
70 | var long startTime = -1 as long | 70 | var long startTime = -1 as long |
71 | var long solverTime = -1 as long | 71 | var long solverTime = -1 as long |
72 | var Process p = null | 72 | var Process p = null |
73 | if (configuration.solver == BackendSolver::VAMPIRE) { | 73 | if (configuration.solver == BackendSolver::LOCVAMP) { |
74 | 74 | ||
75 | var OPTION = " --mode casc_sat " | 75 | var OPTION = " --mode casc_sat " |
76 | if (configuration.runtimeLimit != -1) { | 76 | if (configuration.runtimeLimit != -1) { |
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 index b26c1ded..5c40d767 100644 --- 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 | |||
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 index 7fedcc30..2d4d0741 100644 --- 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 | |||
Binary files differ | |||
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 index 3e3bd688..4f554956 100644 --- 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 | |||
@@ -10,9 +10,11 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolut | |||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; |
11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | 11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; |
12 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; | 12 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl; | ||
16 | import com.google.common.base.Objects; | 18 | import com.google.common.base.Objects; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; |
@@ -24,7 +26,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | |||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; | 27 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; |
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 28 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; | 29 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; |
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; | 30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; |
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; | 31 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; |
@@ -34,10 +35,12 @@ import java.util.List; | |||
34 | import org.eclipse.emf.common.util.EList; | 35 | import org.eclipse.emf.common.util.EList; |
35 | import org.eclipse.xtend2.lib.StringConcatenation; | 36 | import org.eclipse.xtend2.lib.StringConcatenation; |
36 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
38 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
37 | import org.eclipse.xtext.xbase.lib.Exceptions; | 39 | import org.eclipse.xtext.xbase.lib.Exceptions; |
38 | import org.eclipse.xtext.xbase.lib.Extension; | 40 | import org.eclipse.xtext.xbase.lib.Extension; |
39 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 41 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
40 | import org.eclipse.xtext.xbase.lib.InputOutput; | 42 | import org.eclipse.xtext.xbase.lib.InputOutput; |
43 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
41 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 44 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
42 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 45 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
43 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 46 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
@@ -149,28 +152,28 @@ public class VampireSolver extends LogicReasoner { | |||
149 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3); | 152 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3); |
150 | _entries.add(_doubleArrow_1); | 153 | _entries.add(_doubleArrow_1); |
151 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); | 154 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); |
152 | RealStatisticEntry _createRealStatisticEntry = this.resultFactory.createRealStatisticEntry(); | 155 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); |
153 | final Procedure1<RealStatisticEntry> _function_4 = (RealStatisticEntry it_2) -> { | 156 | final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> { |
154 | it_2.setName("satTime"); | 157 | it_2.setName("satTime"); |
155 | it_2.setValue(Double.parseDouble(satTime)); | 158 | it_2.setValue(satTime); |
156 | }; | 159 | }; |
157 | RealStatisticEntry _doubleArrow_2 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry, _function_4); | 160 | StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_4); |
158 | _entries_1.add(_doubleArrow_2); | 161 | _entries_1.add(_doubleArrow_2); |
159 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); | 162 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); |
160 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); | 163 | StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); |
161 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { | 164 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { |
162 | it_2.setName("modOut"); | 165 | it_2.setName("modOut"); |
163 | it_2.setValue(modOut); | 166 | it_2.setValue(modOut); |
164 | }; | 167 | }; |
165 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5); | 168 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_5); |
166 | _entries_2.add(_doubleArrow_3); | 169 | _entries_2.add(_doubleArrow_3); |
167 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); | 170 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); |
168 | RealStatisticEntry _createRealStatisticEntry_1 = this.resultFactory.createRealStatisticEntry(); | 171 | StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); |
169 | final Procedure1<RealStatisticEntry> _function_6 = (RealStatisticEntry it_2) -> { | 172 | final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> { |
170 | it_2.setName("modTime"); | 173 | it_2.setName("modTime"); |
171 | it_2.setValue(Double.parseDouble(modTime)); | 174 | it_2.setValue(modTime); |
172 | }; | 175 | }; |
173 | RealStatisticEntry _doubleArrow_4 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry_1, _function_6); | 176 | StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_6); |
174 | _entries_3.add(_doubleArrow_4); | 177 | _entries_3.add(_doubleArrow_4); |
175 | }; | 178 | }; |
176 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2); | 179 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2); |
@@ -178,13 +181,77 @@ public class VampireSolver extends LogicReasoner { | |||
178 | }; | 181 | }; |
179 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function); | 182 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function); |
180 | } else { | 183 | } else { |
184 | InputOutput.println(); | ||
181 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | 185 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); |
182 | final long backTransformationStart = System.currentTimeMillis(); | 186 | final long backTransformationStart = System.currentTimeMillis(); |
183 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, | 187 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, |
184 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | 188 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); |
185 | long _currentTimeMillis_1 = System.currentTimeMillis(); | 189 | long _currentTimeMillis_1 = System.currentTimeMillis(); |
186 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | 190 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); |
187 | return logicResult; | 191 | final Function1<VLSConfirmations, Boolean> _function_1 = (VLSConfirmations it) -> { |
192 | Class<? extends VLSConfirmations> _class = it.getClass(); | ||
193 | return Boolean.valueOf(Objects.equal(_class, VLSFiniteModelImpl.class)); | ||
194 | }; | ||
195 | Iterable<VLSConfirmations> model = IterableExtensions.<VLSConfirmations>filter(vampSol.getGeneratedModel().getConfirmations(), _function_1); | ||
196 | String modOut_1 = "no"; | ||
197 | final Iterable<VLSConfirmations> _converted_model = (Iterable<VLSConfirmations>)model; | ||
198 | int _length = ((Object[])Conversions.unwrapArray(_converted_model, Object.class)).length; | ||
199 | boolean _greaterThan = (_length > 0); | ||
200 | if (_greaterThan) { | ||
201 | modOut_1 = "FiniteModel"; | ||
202 | } | ||
203 | final String realModOut = modOut_1; | ||
204 | ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); | ||
205 | final Procedure1<ModelResult> _function_2 = (ModelResult it) -> { | ||
206 | it.setProblem(null); | ||
207 | EList<Object> _representation = it.getRepresentation(); | ||
208 | VampireModel _createVampireModel = this.factory.createVampireModel(); | ||
209 | final Procedure1<VampireModel> _function_3 = (VampireModel it_1) -> { | ||
210 | }; | ||
211 | VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_3); | ||
212 | _representation.add(_doubleArrow); | ||
213 | it.setTrace(it.getTrace()); | ||
214 | Statistics _createStatistics = this.resultFactory.createStatistics(); | ||
215 | final Procedure1<Statistics> _function_4 = (Statistics it_1) -> { | ||
216 | it_1.setTransformationTime(((int) transformationTime)); | ||
217 | EList<StatisticEntry> _entries = it_1.getEntries(); | ||
218 | StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); | ||
219 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { | ||
220 | it_2.setName("satOut"); | ||
221 | it_2.setValue("-"); | ||
222 | }; | ||
223 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_5); | ||
224 | _entries.add(_doubleArrow_1); | ||
225 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); | ||
226 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); | ||
227 | final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> { | ||
228 | it_2.setName("satTime"); | ||
229 | it_2.setValue("-"); | ||
230 | }; | ||
231 | StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_6); | ||
232 | _entries_1.add(_doubleArrow_2); | ||
233 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); | ||
234 | StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); | ||
235 | final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> { | ||
236 | it_2.setName("modOut"); | ||
237 | it_2.setValue(realModOut); | ||
238 | }; | ||
239 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_7); | ||
240 | _entries_2.add(_doubleArrow_3); | ||
241 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); | ||
242 | StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); | ||
243 | final Procedure1<StringStatisticEntry> _function_8 = (StringStatisticEntry it_2) -> { | ||
244 | it_2.setName("modTime"); | ||
245 | long _solverTime = vampSol.getSolverTime(); | ||
246 | it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString()); | ||
247 | }; | ||
248 | StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_8); | ||
249 | _entries_3.add(_doubleArrow_4); | ||
250 | }; | ||
251 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_4); | ||
252 | it.setStatistics(_doubleArrow_1); | ||
253 | }; | ||
254 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_2); | ||
188 | } | 255 | } |
189 | } | 256 | } |
190 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); | 257 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); |
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 index 8b7f031e..887a3a31 100644 --- 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 | |||
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 index 1b6e8f80..b4943b57 100644 --- 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 | |||
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 index f523f1af..e3b29572 100644 --- 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 | |||
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 index 30ba1843..50ff7011 100644 --- 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 | |||
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 index 174c7362..337edcba 100644 --- 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 | |||
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 index affa3754..c32ba83f 100644 --- 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 | |||
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 index 9caad4ea..75e60f21 100644 --- 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 | |||
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 index 5be67889..d69b41ea 100644 --- 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 | |||
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 index 192c9d1a..6b91ff7b 100644 --- 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 | |||
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 index 0495ab53..f23063ea 100644 --- 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 | |||
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 index c438f1e5..0de59fdb 100644 --- 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 | |||
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 index 5fb9b455..6176aca5 100644 --- 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 | |||
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.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java index e32530cb..e9073d82 100644 --- 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 | |||
@@ -30,7 +30,7 @@ public class VampireHandler { | |||
30 | final String CVC4LOC = (CVC4DIR + CVC4NAME); | 30 | final String CVC4LOC = (CVC4DIR + CVC4NAME); |
31 | final String CMD = "cmd /c "; | 31 | final String CMD = "cmd /c "; |
32 | final String TEMPNAME = "TEMP.tptp"; | 32 | final String TEMPNAME = "TEMP.tptp"; |
33 | final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + | 33 | final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.minNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + |
34 | ".tptp"); | 34 | ".tptp"); |
35 | final String PATH = "C:/cygwin64/bin"; | 35 | final String PATH = "C:/cygwin64/bin"; |
36 | final URI wsURI = workspace.getWorkspaceURI(); | 36 | final URI wsURI = workspace.getWorkspaceURI(); |
@@ -41,7 +41,7 @@ public class VampireHandler { | |||
41 | long startTime = (-((long) 1)); | 41 | long startTime = (-((long) 1)); |
42 | long solverTime = (-((long) 1)); | 42 | long solverTime = (-((long) 1)); |
43 | Process p = null; | 43 | Process p = null; |
44 | boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMPIRE); | 44 | boolean _equals = Objects.equal(configuration.solver, BackendSolver.LOCVAMP); |
45 | if (_equals) { | 45 | if (_equals) { |
46 | String OPTION = " --mode casc_sat "; | 46 | String OPTION = " --mode casc_sat "; |
47 | if ((configuration.runtimeLimit != (-1))) { | 47 | if ((configuration.runtimeLimit != (-1))) { |