diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-10 22:25:07 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:14 -0400 |
commit | b97501f5f1cdce51ead750e806dc16013f59ec38 (patch) | |
tree | 4e8f60623112320eaece09b7854063d02ff93259 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner | |
parent | VAMPIRE: Further develop testing fo r Vampire solver (diff) | |
download | VIATRA-Generator-b97501f5f1cdce51ead750e806dc16013f59ec38.tar.gz VIATRA-Generator-b97501f5f1cdce51ead750e806dc16013f59ec38.tar.zst VIATRA-Generator-b97501f5f1cdce51ead750e806dc16013f59ec38.zip |
implement http requests for the TPTP server
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner')
22 files changed, 61 insertions, 69 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 b223dbe5..4e9737cb 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,6 +8,7 @@ class VampireSolverConfiguration extends LogicSolverConfiguration { | |||
8 | public var boolean uniquenessDuplicates = false | 8 | public var boolean uniquenessDuplicates = false |
9 | public var int iteration = -1 | 9 | public var int iteration = -1 |
10 | public var BackendSolver solver = BackendSolver::VAMP | 10 | public var BackendSolver solver = BackendSolver::VAMP |
11 | public var genModel = true | ||
11 | //choose needed backend solver | 12 | //choose needed backend solver |
12 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J | 13 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J |
13 | } | 14 | } |
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 3281a196..85b81a8c 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 | |||
@@ -31,29 +31,32 @@ class VampireSolver extends LogicReasoner { | |||
31 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | 31 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper |
32 | val VampireHandler handler = new VampireHandler | 32 | val VampireHandler handler = new VampireHandler |
33 | 33 | ||
34 | var fileName = "problem.tptp" | 34 | // var fileName = "problem.tptp" |
35 | 35 | ||
36 | def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { | 36 | // def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { |
37 | fileName = location + fileName | 37 | // fileName = location + fileName |
38 | solve(problem, config, workspace) | 38 | // solve(problem, config, workspace) |
39 | } | 39 | // } |
40 | 40 | ||
41 | override solve(LogicProblem problem, LogicSolverConfiguration config, | 41 | override solve(LogicProblem problem, LogicSolverConfiguration config, |
42 | ReasonerWorkspace workspace) throws LogicReasonerException { | 42 | ReasonerWorkspace workspace) throws LogicReasonerException { |
43 | val vampireConfig = config.asConfig | 43 | val vampireConfig = config.asConfig |
44 | var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + vampireConfig.typeScopes.maxNewElements + ".tptp" | ||
44 | 45 | ||
45 | // Start: Logic -> Vampire mapping | 46 | // Start: Logic -> Vampire mapping |
46 | val transformationStart = System.currentTimeMillis | 47 | val transformationStart = System.currentTimeMillis |
47 | // TODO | 48 | // TODO |
48 | val result = forwardMapper.transformProblem(problem, vampireConfig) | 49 | val result = forwardMapper.transformProblem(problem, vampireConfig) |
49 | val transformationTime = System.currentTimeMillis - transformationStart | 50 | val transformationTime = System.currentTimeMillis - transformationStart |
50 | 51 | ||
51 | val vampireProblem = result.output | 52 | val vampireProblem = result.output |
52 | val forwardTrace = result.trace | 53 | val forwardTrace = result.trace |
53 | 54 | ||
54 | var String fileURI = null; | 55 | var String fileURI = null; |
55 | var String vampireCode = null; | 56 | var String vampireCode = null; |
56 | vampireCode = workspace.writeModelToString(vampireProblem, fileName) | 57 | vampireCode = workspace.writeModelToString(vampireProblem, fileName) |
58 | |||
59 | |||
57 | 60 | ||
58 | val writeFile = ( | 61 | val writeFile = ( |
59 | vampireConfig.documentationLevel === DocumentationLevel::NORMAL || | 62 | vampireConfig.documentationLevel === DocumentationLevel::NORMAL || |
@@ -61,35 +64,33 @@ class VampireSolver extends LogicReasoner { | |||
61 | if (writeFile) { | 64 | if (writeFile) { |
62 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString | 65 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString |
63 | } | 66 | } |
64 | 67 | ||
65 | |||
66 | |||
67 | // Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("tptp", new VampireLanguageFactoryImpl) | 68 | // Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("tptp", new VampireLanguageFactoryImpl) |
68 | //// val Resource resource = Resource. | 69 | //// val Resource resource = Resource. |
69 | //// Resource.getResource(wsURI+"problem.tptp") as Resource | 70 | //// Resource.getResource(wsURI+"problem.tptp") as Resource |
70 | //// resource | 71 | //// resource |
71 | // val model = workspace.readModel(VampireModel, "problem.tptp").eResource.contents | 72 | // val model = workspace.readModel(VampireModel, "problem.tptp").eResource.contents |
72 | // println(model) | 73 | // println(model) |
73 | |||
74 | |||
75 | // Result as String | ||
76 | |||
77 | // Finish: Logic -> Vampire mapping | 74 | // Finish: Logic -> Vampire mapping |
78 | 75 | if (vampireConfig.genModel) { | |
79 | // Start: Solving .tptp problem | ||
80 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | ||
81 | // Finish: Solving .tptp problem | ||
82 | |||
83 | // Start: Vampire -> Logic mapping | ||
84 | val backTransformationStart = System.currentTimeMillis | ||
85 | // Backwards Mapper | ||
86 | val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime) | ||
87 | 76 | ||
88 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | 77 | // Start: Solving .tptp problem |
89 | // Finish: Vampire -> Logic Mapping | 78 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) |
90 | 79 | // Finish: Solving .tptp problem | |
80 | // Start: Vampire -> Logic mapping | ||
81 | val backTransformationStart = System.currentTimeMillis | ||
82 | // Backwards Mapper | ||
83 | val logicResult = backwardMapper.transformOutput(problem, | ||
84 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) | ||
85 | |||
86 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | ||
87 | // Finish: Vampire -> Logic Mapping | ||
91 | // print(vampSol.generatedModel.tfformulas.size) | 88 | // print(vampSol.generatedModel.tfformulas.size) |
92 | return logicResult //currently only a ModelResult | 89 | return logicResult // currently only a ModelResult |
90 | } | ||
91 | |||
92 | return backwardMapper.transformOutput(problem, | ||
93 | vampireConfig.solutionScope.numberOfRequiredSolution, new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) | ||
93 | } | 94 | } |
94 | 95 | ||
95 | def asConfig(LogicSolverConfiguration configuration) { | 96 | def asConfig(LogicSolverConfiguration configuration) { |
@@ -105,9 +106,9 @@ class VampireSolver extends LogicReasoner { | |||
105 | // * | 106 | // * |
106 | override getInterpretations(ModelResult modelResult) { | 107 | override getInterpretations(ModelResult modelResult) { |
107 | // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] | 108 | // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] |
108 | val sols = modelResult.representation// as List<A4Solution> | 109 | val sols = modelResult.representation // as List<A4Solution> |
109 | //val res = answers.map | 110 | // val res = answers.map |
110 | sols.map[ | 111 | sols.map [ |
111 | new VampireModelInterpretation( | 112 | new VampireModelInterpretation( |
112 | // forwardMapper.typeMapper.typeInterpreter, | 113 | // forwardMapper.typeMapper.typeInterpreter, |
113 | it as VampireModel, | 114 | it as VampireModel, |
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 df3cfd82..39862c65 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 | |||
@@ -25,8 +25,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
25 | 25 | ||
26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, | 26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, |
27 | Logic2VampireLanguageMapperTrace trace) { | 27 | Logic2VampireLanguageMapperTrace trace) { |
28 | val ABSOLUTE_MIN = 0 | 28 | |
29 | val ABSOLUTE_MAX = Integer.MAX_VALUE | ||
30 | 29 | ||
31 | // TODO HANDLE ERRORS RELATED TO MAX > MIN | 30 | // TODO HANDLE ERRORS RELATED TO MAX > MIN |
32 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS | 31 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS |
@@ -40,6 +39,8 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
40 | // Number of defined non-abstract elements that are not enum elements | 39 | // Number of defined non-abstract elements that are not enum elements |
41 | // Equals the number of elements in te initial model | 40 | // Equals the number of elements in te initial model |
42 | var elemsInIM = trace.definedElement2String.size | 41 | var elemsInIM = trace.definedElement2String.size |
42 | val ABSOLUTE_MIN = 0 | ||
43 | val ABSOLUTE_MAX = -1-elemsInIM | ||
43 | // var elemsInIM = 0 | 44 | // var elemsInIM = 0 |
44 | // | 45 | // |
45 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { | 46 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { |
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 c1eb3382..47eae807 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 | |||
@@ -52,8 +52,10 @@ class VampireHandler { | |||
52 | 52 | ||
53 | val CMD = "cmd /c " | 53 | val CMD = "cmd /c " |
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 + | ||
58 | ".tptp" | ||
57 | val PATH = "C:/cygwin64/bin" | 59 | val PATH = "C:/cygwin64/bin" |
58 | 60 | ||
59 | val wsURI = workspace.workspaceURI | 61 | val wsURI = workspace.workspaceURI |
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 85f3773c..e50e6812 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 77dc060f..e4925e24 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 c3e185f5..432b14c3 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 | |||
@@ -24,7 +24,6 @@ import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | |||
24 | import java.util.List; | 24 | import java.util.List; |
25 | import org.eclipse.emf.common.util.EList; | 25 | import org.eclipse.emf.common.util.EList; |
26 | import org.eclipse.xtend2.lib.StringConcatenation; | 26 | import org.eclipse.xtend2.lib.StringConcatenation; |
27 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
28 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 27 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
29 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 28 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
30 | 29 | ||
@@ -42,24 +41,10 @@ public class VampireSolver extends LogicReasoner { | |||
42 | 41 | ||
43 | private final VampireHandler handler = new VampireHandler(); | 42 | private final VampireHandler handler = new VampireHandler(); |
44 | 43 | ||
45 | private String fileName = "problem.tptp"; | ||
46 | |||
47 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace, final String location) { | ||
48 | try { | ||
49 | LogicResult _xblockexpression = null; | ||
50 | { | ||
51 | this.fileName = (location + this.fileName); | ||
52 | _xblockexpression = this.solve(problem, config, workspace); | ||
53 | } | ||
54 | return _xblockexpression; | ||
55 | } catch (Throwable _e) { | ||
56 | throw Exceptions.sneakyThrow(_e); | ||
57 | } | ||
58 | } | ||
59 | |||
60 | @Override | 44 | @Override |
61 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { | 45 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { |
62 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); | 46 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); |
47 | String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp"); | ||
63 | final long transformationStart = System.currentTimeMillis(); | 48 | final long transformationStart = System.currentTimeMillis(); |
64 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | 49 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); |
65 | long _currentTimeMillis = System.currentTimeMillis(); | 50 | long _currentTimeMillis = System.currentTimeMillis(); |
@@ -68,18 +53,24 @@ public class VampireSolver extends LogicReasoner { | |||
68 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | 53 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); |
69 | String fileURI = null; | 54 | String fileURI = null; |
70 | String vampireCode = null; | 55 | String vampireCode = null; |
71 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); | 56 | vampireCode = workspace.writeModelToString(vampireProblem, fileName); |
72 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || | 57 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || |
73 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); | 58 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); |
74 | if (writeFile) { | 59 | if (writeFile) { |
75 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); | 60 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString(); |
61 | } | ||
62 | if (vampireConfig.genModel) { | ||
63 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | ||
64 | final long backTransformationStart = System.currentTimeMillis(); | ||
65 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, | ||
66 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | ||
67 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
68 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | ||
69 | return logicResult; | ||
76 | } | 70 | } |
77 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | 71 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); |
78 | final long backTransformationStart = System.currentTimeMillis(); | 72 | return this.backwardMapper.transformOutput(problem, |
79 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | 73 | vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); |
80 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
81 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | ||
82 | return logicResult; | ||
83 | } | 74 | } |
84 | 75 | ||
85 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | 76 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java index 7bb17b59..dd66e910 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java | |||
@@ -12,4 +12,6 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration { | |||
12 | public int iteration = (-1); | 12 | public int iteration = (-1); |
13 | 13 | ||
14 | public BackendSolver solver = BackendSolver.VAMP; | 14 | public BackendSolver solver = BackendSolver.VAMP; |
15 | |||
16 | public boolean genModel = true; | ||
15 | } | 17 | } |
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 eb1685d1..8d2ec6ab 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 3ddf9cfc..515b4b3c 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 66f9d9e8..46ad8c79 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 bafcfab6..169aedc2 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 a4af882f..699ce6e2 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 08f9fd96..799515d4 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 dc25e3be..2a112ae7 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 37b0c7a5..7f32e055 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 6d562aa8..a2dd469b 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 5ed9ac3b..98c355ab 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 111053a4..246c08c8 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 f33599f9..9e55bac4 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/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index 6da75271..bc39a068 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |||
@@ -53,9 +53,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
53 | } | 53 | } |
54 | 54 | ||
55 | public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 55 | public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
56 | final int ABSOLUTE_MIN = 0; | ||
57 | final int ABSOLUTE_MAX = Integer.MAX_VALUE; | ||
58 | int elemsInIM = trace.definedElement2String.size(); | 56 | int elemsInIM = trace.definedElement2String.size(); |
57 | final int ABSOLUTE_MIN = 0; | ||
58 | final int ABSOLUTE_MAX = ((-1) - elemsInIM); | ||
59 | final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); | 59 | final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); |
60 | final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); | 60 | final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); |
61 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); | 61 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); |
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 7906c5fb..fcbdfde7 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,19 +30,13 @@ 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 | String _string = configuration.solver.toString(); | 33 | final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + |
34 | String _plus = ("solution" + _string); | 34 | ".tptp"); |
35 | String _plus_1 = (_plus + "_"); | ||
36 | String _plus_2 = (_plus_1 + Integer.valueOf(configuration.typeScopes.maxNewElements)); | ||
37 | String _plus_3 = (_plus_2 + | ||
38 | "_"); | ||
39 | String _plus_4 = (_plus_3 + Integer.valueOf(configuration.iteration)); | ||
40 | final String SOLNNAME = (_plus_4 + ".tptp"); | ||
41 | final String PATH = "C:/cygwin64/bin"; | 35 | final String PATH = "C:/cygwin64/bin"; |
42 | final URI wsURI = workspace.getWorkspaceURI(); | 36 | final URI wsURI = workspace.getWorkspaceURI(); |
43 | final String tempLoc = (wsURI + TEMPNAME); | 37 | final String tempLoc = (wsURI + TEMPNAME); |
44 | String _plus_5 = (wsURI + SOLNNAME); | 38 | String _plus = (wsURI + SOLNNAME); |
45 | final String solnLoc = (_plus_5 + " "); | 39 | final String solnLoc = (_plus + " "); |
46 | String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); | 40 | String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); |
47 | long startTime = (-((long) 1)); | 41 | long startTime = (-((long) 1)); |
48 | long solverTime = (-((long) 1)); | 42 | long solverTime = (-((long) 1)); |