aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend2
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend61
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend16
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
generated by cgit v1.2.3-54-g00ecf (git 2.45.1) at 2024-05-25 17:56:08 +0000