diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend')
| -rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend | 61 |
1 files changed, 56 insertions, 5 deletions
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, |