diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-11 15:51:49 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:17 -0400 |
commit | 606f6965f3ccec837aa216cbb3f56fdcf943a59b (patch) | |
tree | e9d1283f60b335de331b5e8abd93f040636f871b /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src | |
parent | implement http requests for the TPTP server (diff) | |
download | VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.tar.gz VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.tar.zst VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.zip |
VAMPIRE: complete testing setup
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src')
5 files changed, 196 insertions, 39 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 4e9737cb..4c2f1952 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 | |||
@@ -2,21 +2,29 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner | |||
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
4 | 4 | ||
5 | class VampireSolverConfiguration extends LogicSolverConfiguration { | 5 | class VampireSolverConfiguration |
6 | extends LogicSolverConfiguration { | ||
6 | 7 | ||
7 | public var int contCycleLevel = 0 | 8 | public var int contCycleLevel = 0 |
8 | public var boolean uniquenessDuplicates = false | 9 | public var boolean uniquenessDuplicates = false |
9 | public var int iteration = -1 | 10 | public var int iteration = -1 |
10 | public var BackendSolver solver = BackendSolver::VAMP | 11 | public var BackendSolver solver = BackendSolver::VAMPIRE |
11 | public var genModel = true | 12 | public var genModel = true |
13 | public var server = false | ||
12 | //choose needed backend solver | 14 | //choose needed backend solver |
13 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J | 15 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J |
14 | } | 16 | } |
15 | 17 | ||
16 | 18 | ||
17 | enum BackendSolver { | 19 | enum BackendSolver { |
18 | VAMP, | 20 | CVC4, |
19 | CVC4 | 21 | DARWINFM, |
22 | EDARWIN, | ||
23 | GEOIII, | ||
24 | IPROVER, | ||
25 | PARADOX, | ||
26 | VAMPIRE, | ||
27 | Z3 | ||
20 | //add needed things | 28 | //add needed things |
21 | } | 29 | } |
22 | 30 | ||
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 85b81a8c..31aa091c 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 | |||
@@ -4,18 +4,20 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | |||
4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated | 4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution | 8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper | 9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper |
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler | 10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler |
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation | 11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
20 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 22 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
21 | 23 | ||
@@ -30,18 +32,20 @@ class VampireSolver extends LogicReasoner { | |||
30 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper | 32 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper |
31 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | 33 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper |
32 | val VampireHandler handler = new VampireHandler | 34 | val VampireHandler handler = new VampireHandler |
35 | val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
36 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | ||
37 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
33 | 38 | ||
34 | // var fileName = "problem.tptp" | 39 | // var fileName = "problem.tptp" |
35 | |||
36 | // def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { | 40 | // def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { |
37 | // fileName = location + fileName | 41 | // fileName = location + fileName |
38 | // solve(problem, config, workspace) | 42 | // solve(problem, config, workspace) |
39 | // } | 43 | // } |
40 | |||
41 | override solve(LogicProblem problem, LogicSolverConfiguration config, | 44 | override solve(LogicProblem problem, LogicSolverConfiguration config, |
42 | ReasonerWorkspace workspace) throws LogicReasonerException { | 45 | ReasonerWorkspace workspace) throws LogicReasonerException { |
43 | val vampireConfig = config.asConfig | 46 | val vampireConfig = config.asConfig |
44 | var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + vampireConfig.typeScopes.maxNewElements + ".tptp" | 47 | var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + |
48 | vampireConfig.typeScopes.maxNewElements + ".tptp" | ||
45 | 49 | ||
46 | // Start: Logic -> Vampire mapping | 50 | // Start: Logic -> Vampire mapping |
47 | val transformationStart = System.currentTimeMillis | 51 | val transformationStart = System.currentTimeMillis |
@@ -55,8 +59,6 @@ class VampireSolver extends LogicReasoner { | |||
55 | var String fileURI = null; | 59 | var String fileURI = null; |
56 | var String vampireCode = null; | 60 | var String vampireCode = null; |
57 | vampireCode = workspace.writeModelToString(vampireProblem, fileName) | 61 | vampireCode = workspace.writeModelToString(vampireProblem, fileName) |
58 | |||
59 | |||
60 | 62 | ||
61 | val writeFile = ( | 63 | val writeFile = ( |
62 | vampireConfig.documentationLevel === DocumentationLevel::NORMAL || | 64 | vampireConfig.documentationLevel === DocumentationLevel::NORMAL || |
@@ -73,24 +75,94 @@ class VampireSolver extends LogicReasoner { | |||
73 | // println(model) | 75 | // println(model) |
74 | // Finish: Logic -> Vampire mapping | 76 | // Finish: Logic -> Vampire mapping |
75 | if (vampireConfig.genModel) { | 77 | if (vampireConfig.genModel) { |
76 | 78 | if (vampireConfig.server) { | |
77 | // Start: Solving .tptp problem | 79 | val form = support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit) |
78 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | 80 | var response = newArrayList |
79 | // Finish: Solving .tptp problem | 81 | var ind = 0 |
80 | // Start: Vampire -> Logic mapping | 82 | var done = false |
81 | val backTransformationStart = System.currentTimeMillis | 83 | print(" ") |
82 | // Backwards Mapper | 84 | while (!done) { |
83 | val logicResult = backwardMapper.transformOutput(problem, | 85 | print("(x)") |
84 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) | 86 | done = false |
85 | 87 | response = support.sendPost(form) | |
86 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | 88 | |
87 | // Finish: Vampire -> Logic Mapping | 89 | var responseFound = false |
90 | ind = 0 | ||
91 | while (!responseFound) { | ||
92 | var line = response.get(ind) | ||
93 | if (line.length >= 5 && line.substring(0, 5) == "ERROR") { | ||
94 | done = false | ||
95 | responseFound = true | ||
96 | } else { | ||
97 | if (line == "</PRE>") { | ||
98 | done = true | ||
99 | responseFound = true | ||
100 | } | ||
101 | } | ||
102 | ind++ | ||
103 | } | ||
104 | } | ||
105 | val satRaw = response.get(ind - 3) | ||
106 | val modRaw = response.get(ind - 2) | ||
107 | |||
108 | val sat = newArrayList(satRaw.split(" ")) | ||
109 | val mod = newArrayList(modRaw.split(" ")) | ||
110 | |||
111 | val satOut = sat.get(1) | ||
112 | val modOut = mod.get(1) | ||
113 | val satTime = sat.get(2) | ||
114 | val modTime = mod.get(2) | ||
115 | |||
116 | println() | ||
117 | println(sat) | ||
118 | println(mod) | ||
119 | |||
120 | return createModelResult => [ | ||
121 | it.problem = null | ||
122 | it.representation += createVampireModel => [] | ||
123 | it.trace = trace | ||
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 += createRealStatisticEntry => [ | ||
131 | it.name = "satTime" | ||
132 | it.value = Double.parseDouble(satTime) | ||
133 | ] | ||
134 | it.entries += createStringStatisticEntry => [ | ||
135 | it.name = "modOut" | ||
136 | it.value = modOut | ||
137 | ] | ||
138 | it.entries += createRealStatisticEntry => [ | ||
139 | it.name = "modTime" | ||
140 | it.value = Double.parseDouble(modTime) | ||
141 | ] | ||
142 | |||
143 | ] | ||
144 | ] | ||
145 | |||
146 | // return newArrayList(line1, line2) | ||
147 | } else { | ||
148 | |||
149 | // Start: Solving .tptp problem | ||
150 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | ||
151 | // Finish: Solving .tptp problem | ||
152 | // Start: Vampire -> Logic mapping | ||
153 | val backTransformationStart = System.currentTimeMillis | ||
154 | // Backwards Mapper | ||
155 | val logicResult = backwardMapper.transformOutput(problem, | ||
156 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) | ||
157 | |||
158 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | ||
159 | // Finish: Vampire -> Logic Mapping | ||
88 | // print(vampSol.generatedModel.tfformulas.size) | 160 | // print(vampSol.generatedModel.tfformulas.size) |
89 | return logicResult // currently only a ModelResult | 161 | return logicResult // currently only a ModelResult |
162 | } | ||
90 | } | 163 | } |
91 | 164 | return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, | |
92 | return backwardMapper.transformOutput(problem, | 165 | new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) |
93 | vampireConfig.solutionScope.numberOfRequiredSolution, new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) | ||
94 | } | 166 | } |
95 | 167 | ||
96 | def asConfig(LogicSolverConfiguration configuration) { | 168 | def asConfig(LogicSolverConfiguration configuration) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index 39862c65..a9516cc4 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend | |||
@@ -40,7 +40,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
40 | // Equals the number of elements in te initial model | 40 | // Equals the number of elements in te initial model |
41 | var elemsInIM = trace.definedElement2String.size | 41 | var elemsInIM = trace.definedElement2String.size |
42 | val ABSOLUTE_MIN = 0 | 42 | val ABSOLUTE_MIN = 0 |
43 | val ABSOLUTE_MAX = -1-elemsInIM | 43 | val ABSOLUTE_MAX = Integer.MAX_VALUE-elemsInIM |
44 | // var elemsInIM = 0 | 44 | // var elemsInIM = 0 |
45 | // | 45 | // |
46 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { | 46 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { |
@@ -60,7 +60,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
60 | 60 | ||
61 | // Handling Minimum_General | 61 | // Handling Minimum_General |
62 | if (GLOBAL_MIN != ABSOLUTE_MIN) { | 62 | if (GLOBAL_MIN != ABSOLUTE_MIN) { |
63 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant) | 63 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant)//may make not consistent here |
64 | if (consistant) { | 64 | if (consistant) { |
65 | for (i : trace.uniqueInstances) { | 65 | for (i : trace.uniqueInstances) { |
66 | localInstances.add(support.duplicate(i)) | 66 | localInstances.add(support.duplicate(i)) |
@@ -73,7 +73,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
73 | 73 | ||
74 | // Handling Maximum_General | 74 | // Handling Maximum_General |
75 | if (GLOBAL_MAX != ABSOLUTE_MAX) { | 75 | if (GLOBAL_MAX != ABSOLUTE_MAX) { |
76 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant) | 76 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, !consistant) |
77 | if (consistant) { | 77 | if (consistant) { |
78 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) | 78 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) |
79 | } else { | 79 | } else { |
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 680213ab..7b1c7d9a 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 | |||
@@ -1,5 +1,6 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm |
@@ -16,6 +17,12 @@ import java.util.ArrayList | |||
16 | import java.util.HashMap | 17 | import java.util.HashMap |
17 | import java.util.List | 18 | import java.util.List |
18 | import java.util.Map | 19 | import java.util.Map |
20 | import java.util.concurrent.TimeUnit | ||
21 | import okhttp3.MediaType | ||
22 | import okhttp3.OkHttpClient | ||
23 | import okhttp3.Request | ||
24 | import okhttp3.RequestBody | ||
25 | import okhttp3.Response | ||
19 | import org.eclipse.emf.common.util.EList | 26 | import org.eclipse.emf.common.util.EList |
20 | 27 | ||
21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
@@ -77,13 +84,13 @@ class Logic2VampireLanguageMapper_Support { | |||
77 | it.terms += duplicate(v) | 84 | it.terms += duplicate(v) |
78 | ] | 85 | ] |
79 | } | 86 | } |
80 | 87 | ||
81 | def protected List<VLSVariable> duplicate(List<VLSVariable> vars) { | 88 | def protected List<VLSVariable> duplicate(List<VLSVariable> vars) { |
82 | var newList = newArrayList | 89 | var newList = newArrayList |
83 | for (v : vars) { | 90 | for (v : vars) { |
84 | newList.add(duplicate(v)) | 91 | newList.add(duplicate(v)) |
85 | } | 92 | } |
86 | return newList | 93 | return newList |
87 | } | 94 | } |
88 | 95 | ||
89 | def protected VLSConstant toConstant(VLSFunctionAsTerm term) { | 96 | def protected VLSConstant toConstant(VLSFunctionAsTerm term) { |
@@ -117,7 +124,7 @@ class Logic2VampireLanguageMapper_Support { | |||
117 | 124 | ||
118 | // TODO Make more general | 125 | // TODO Make more general |
119 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { | 126 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { |
120 | 127 | ||
121 | // OLD | 128 | // OLD |
122 | // val List<VLSInequality> eqs = newArrayList | 129 | // val List<VLSInequality> eqs = newArrayList |
123 | // for (t1 : terms.subList(1, terms.length)) { | 130 | // for (t1 : terms.subList(1, terms.length)) { |
@@ -133,7 +140,6 @@ class Logic2VampireLanguageMapper_Support { | |||
133 | // } | 140 | // } |
134 | // return unfoldAnd(eqs) | 141 | // return unfoldAnd(eqs) |
135 | // END OLD | 142 | // END OLD |
136 | |||
137 | val List<VLSInequality> eqs = newArrayList | 143 | val List<VLSInequality> eqs = newArrayList |
138 | for (t1 : terms) { | 144 | for (t1 : terms) { |
139 | if (t1 != t2) { | 145 | if (t1 != t2) { |
@@ -257,7 +263,8 @@ class Logic2VampireLanguageMapper_Support { | |||
257 | } | 263 | } |
258 | } | 264 | } |
259 | } | 265 | } |
260 | //TODO rewrite such that it uses "listSubTypes" | 266 | |
267 | // TODO rewrite such that it uses "listSubTypes" | ||
261 | def protected boolean dfsSubtypeCheck(Type type, Type type2) { | 268 | def protected boolean dfsSubtypeCheck(Type type, Type type2) { |
262 | // There is surely a better way to do this | 269 | // There is surely a better way to do this |
263 | if (type.subtypes.isEmpty) | 270 | if (type.subtypes.isEmpty) |
@@ -284,4 +291,74 @@ class Logic2VampireLanguageMapper_Support { | |||
284 | new HashMap(map1) => [putAll(map2)] | 291 | new HashMap(map1) => [putAll(map2)] |
285 | } | 292 | } |
286 | 293 | ||
294 | // SERVERS | ||
295 | def makeForm(String formula, BackendSolver solver, int time) { | ||
296 | return header + formula + addOptions + addSolver(solver, time) + addEnd | ||
297 | } | ||
298 | |||
299 | def getSolverSpecs(BackendSolver solver) { | ||
300 | switch (solver) { | ||
301 | case BackendSolver::CVC4: return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") | ||
302 | case BackendSolver::DARWINFM: return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") | ||
303 | case BackendSolver::EDARWIN: return newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") | ||
304 | case BackendSolver::GEOIII: return newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") | ||
305 | case BackendSolver::IPROVER: return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") | ||
306 | case BackendSolver::PARADOX: return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") | ||
307 | case BackendSolver::VAMPIRE: return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") | ||
308 | case BackendSolver::Z3: return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s") | ||
309 | } | ||
310 | } | ||
311 | |||
312 | def getHeader() { | ||
313 | 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" | ||
314 | } | ||
315 | |||
316 | def addSpec(String spec) { | ||
317 | return spec.replace("\n", "\\r\\n") | ||
318 | } | ||
319 | |||
320 | def addOptions() { | ||
321 | 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" | ||
322 | } | ||
323 | |||
324 | def addSolver(BackendSolver solver, int time) { | ||
325 | val solverSpecs = getSolverSpecs(solver) | ||
326 | val ID = solverSpecs.get(0) | ||
327 | val cmd = solverSpecs.get(1) | ||
328 | |||
329 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + | ||
330 | "\"\r\n\r\n" + ID + | ||
331 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + | ||
332 | "\"\r\n\r\n" + cmd.replace("%d", time.toString) + "\r\n" | ||
333 | } | ||
334 | |||
335 | def addEnd() { | ||
336 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--" | ||
337 | } | ||
338 | |||
339 | def sendPost(String formData) throws Exception { | ||
340 | |||
341 | val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build() | ||
342 | |||
343 | val MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") | ||
344 | val RequestBody body = RequestBody.create(mediaType, formData) | ||
345 | val Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body). | ||
346 | addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", | ||
347 | "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", | ||
348 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", | ||
349 | "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36"). | ||
350 | addHeader("Accept", | ||
351 | "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3"). | ||
352 | addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", | ||
353 | "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", | ||
354 | "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", | ||
355 | "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build() | ||
356 | |||
357 | val Response response = client.newCall(request).execute() | ||
358 | // TimeUnit.SECONDS.sleep(5) | ||
359 | return newArrayList(response.body.string.split("\n")) | ||
360 | // return response.body.string | ||
361 | // case 1: | ||
362 | } | ||
363 | |||
287 | } | 364 | } |
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 47eae807..6d301442 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 | |||
@@ -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::VAMP) { | 73 | if (configuration.solver == BackendSolver::VAMPIRE) { |
74 | 74 | ||
75 | var OPTION = " --mode casc_sat " | 75 | var OPTION = " --mode casc_sat " |
76 | if (configuration.runtimeLimit != -1) { | 76 | if (configuration.runtimeLimit != -1) { |