diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca')
3 files changed, 65 insertions, 14 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 | ||