diff options
52 files changed, 387 insertions, 228 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin index ef511dca..1eaefbda 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin index c9ed86f5..05c29aff 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin index e24f55b7..12f063b1 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin index af221451..88a713db 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin index 1f1241ce..31d3dbf6 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin index e89f2182..ca30b3d0 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin index 9c0c7969..0d75d237 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin index fe289357..a8d38a91 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin index 6cb28d31..0192cd3c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin index 7e8ae1ab..07f4c611 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin index 81de0171..01c9f74f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin index c5672cca..b4bd4155 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin index 2b96a53a..5dd72d15 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin index 5faad94e..db384a64 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin | |||
Binary files differ | |||
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)); |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath index 3f0838b6..7618afdf 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath | |||
@@ -5,5 +5,11 @@ | |||
5 | <classpathentry kind="src" path="src"/> | 5 | <classpathentry kind="src" path="src"/> |
6 | <classpathentry kind="src" path="src-gen"/> | 6 | <classpathentry kind="src" path="src-gen"/> |
7 | <classpathentry kind="src" path="xtend-gen"/> | 7 | <classpathentry kind="src" path="xtend-gen"/> |
8 | <classpathentry kind="lib" path="InputLPs/unirest-java-1.4.9.jar"/> | ||
9 | <classpathentry kind="lib" path="InputLPs/annotations-13.0.jar"/> | ||
10 | <classpathentry kind="lib" path="InputLPs/kotlin-stdlib-1.3.50.jar"/> | ||
11 | <classpathentry kind="lib" path="InputLPs/kotlin-stdlib-common-1.3.50.jar"/> | ||
12 | <classpathentry kind="lib" path="InputLPs/okhttp-4.2.0.jar"/> | ||
13 | <classpathentry kind="lib" path="InputLPs/okio-2.2.2.jar"/> | ||
8 | <classpathentry kind="output" path="bin"/> | 14 | <classpathentry kind="output" path="bin"/> |
9 | </classpath> | 15 | </classpath> |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF index 0af80e6c..dead7622 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF | |||
@@ -6,48 +6,44 @@ Bundle-Version: 1.0.0.qualifier | |||
6 | Bundle-ClassPath: . | 6 | Bundle-ClassPath: . |
7 | Bundle-Vendor: %providerName | 7 | Bundle-Vendor: %providerName |
8 | Bundle-Localization: plugin | 8 | Bundle-Localization: plugin |
9 | Export-Package: ca.mcgill.ecse.dslreasoner.vamipre.yakindumm, | 9 | Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries, |
10 | ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.impl, | 10 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm, |
11 | ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.util, | 11 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl, |
12 | ca.mcgill.ecse.dslreasoner.vampire.queries, | 12 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util |
13 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm, | ||
14 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl, | ||
15 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util, | ||
16 | yakindumm, | ||
17 | yakindumm.impl, | ||
18 | yakindumm.util, | ||
19 | yakindumm.yakindumm, | ||
20 | yakindumm.yakindumm.impl, | ||
21 | yakindumm.yakindumm.util | ||
22 | Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime, | 13 | Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime, |
23 | org.eclipse.core.runtime, | 14 | org.eclipse.core.runtime, |
24 | org.eclipse.emf.ecore;visibility:=reexport, | 15 | org.eclipse.emf.ecore;visibility:=reexport, |
25 | org.eclipse.viatra.query.runtime.rete, | 16 | org.eclipse.viatra.query.runtime.rete, |
26 | org.eclipse.viatra.query.runtime.localsearch, | 17 | org.eclipse.viatra.query.runtime.localsearch, |
27 | com.google.guava, | 18 | com.google.guava, |
28 | org.eclipse.xtext.xbase.lib, | 19 | org.eclipse.xtext.xbase.lib, |
29 | org.eclipse.xtend.lib, | 20 | org.eclipse.xtend.lib, |
30 | org.eclipse.xtend.lib.macro, | 21 | org.eclipse.xtend.lib.macro, |
31 | ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", | 22 | ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", |
32 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | 23 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", |
33 | ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", | 24 | ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", |
34 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | 25 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", |
35 | hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", | 26 | hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", |
36 | org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", | 27 | org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", |
37 | hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", | 28 | hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", |
38 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", | 29 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", |
39 | hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", | 30 | hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", |
40 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", | 31 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", |
41 | hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0", | 32 | hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0", |
42 | hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0", | 33 | hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0", |
43 | ModelGenExampleFAM_plugin;bundle-version="1.0.0", | 34 | ModelGenExampleFAM_plugin;bundle-version="1.0.0", |
44 | ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1", | 35 | ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1", |
45 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", | 36 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", |
46 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1", | 37 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1", |
47 | org.eclipse.viatra.query.runtime;bundle-version="2.1.0", | 38 | org.eclipse.viatra.query.runtime;bundle-version="2.1.0", |
48 | org.eclipse.collections;bundle-version="9.2.0", | 39 | org.eclipse.collections;bundle-version="9.2.0", |
49 | hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", | 40 | hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", |
50 | ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0" | 41 | ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0", |
42 | org.apache.httpcomponents.httpcore;bundle-version="4.4.6", | ||
43 | org.apache.httpcomponents.httpclient;bundle-version="4.5.2", | ||
44 | org.apache.httpcomponents.httpclient.source;bundle-version="4.5.2", | ||
45 | org.apache.httpcomponents.httpclient.win;bundle-version="4.5.2", | ||
46 | org.apache.httpcomponents.httpcore.source;bundle-version="4.4.6" | ||
51 | Import-Package: org.apache.log4j | 47 | Import-Package: org.apache.log4j |
52 | Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test | 48 | Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test |
53 | Bundle-ActivationPolicy: lazy | 49 | Bundle-ActivationPolicy: lazy |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend index 2495ab77..5289371f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend | |||
@@ -86,7 +86,7 @@ class FileSystemTest { | |||
86 | it.uniquenessDuplicates = false | 86 | it.uniquenessDuplicates = false |
87 | ] | 87 | ] |
88 | 88 | ||
89 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS") | 89 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) |
90 | 90 | ||
91 | /*/ | 91 | /*/ |
92 | * | 92 | * |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend index 89375801..5225fb89 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend | |||
@@ -9,6 +9,11 @@ import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | |||
9 | import java.util.HashMap | 9 | import java.util.HashMap |
10 | import java.util.List | 10 | import java.util.List |
11 | import java.util.Map | 11 | import java.util.Map |
12 | import okhttp3.MediaType | ||
13 | import okhttp3.OkHttpClient | ||
14 | import okhttp3.Request | ||
15 | import okhttp3.RequestBody | ||
16 | import okhttp3.Response | ||
12 | import org.eclipse.emf.ecore.EAttribute | 17 | import org.eclipse.emf.ecore.EAttribute |
13 | import org.eclipse.emf.ecore.EClass | 18 | import org.eclipse.emf.ecore.EClass |
14 | import org.eclipse.emf.ecore.EEnum | 19 | import org.eclipse.emf.ecore.EEnum |
@@ -20,15 +25,77 @@ import org.eclipse.emf.ecore.resource.Resource | |||
20 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 25 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
21 | import org.eclipse.viatra.query.runtime.api.IQueryGroup | 26 | import org.eclipse.viatra.query.runtime.api.IQueryGroup |
22 | 27 | ||
23 | class GeneralTest { | 28 | class GeneralTest { |
24 | def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) { | 29 | val static USER_AGENT = "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36" |
30 | |||
31 | def static void main(String[] args) { | ||
32 | val form = makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300) | ||
33 | |||
34 | // val x =sendPost("------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\ntester | ||
35 | // | ||
36 | //\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 | ||
37 | // | ||
38 | //------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___Paradox---4.0\"\r\n\r\nParadox---4.0\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___Paradox---4.0\"\r\n\r\nparadox --no-progress --time %d --tstp --model %s\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--") | ||
39 | val x = sendPost(form) | ||
40 | print(x.toString) | ||
41 | } | ||
42 | |||
43 | def static makeForm(String formula, String solver, String cmd, int time) { | ||
44 | return header + addSpec(formula) + addOptions + addSolver(solver, cmd.replace("%d", time.toString)) + addEnd | ||
45 | } | ||
46 | |||
47 | def static sendPost(String formData ) throws Exception { | ||
48 | |||
49 | val OkHttpClient client = new OkHttpClient() | ||
50 | |||
51 | val MediaType mediaType = MediaType.parse( | ||
52 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") | ||
53 | val RequestBody body = RequestBody.create(mediaType, formData) | ||
54 | val Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body). | ||
55 | addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", | ||
56 | "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", | ||
57 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", | ||
58 | "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36"). | ||
59 | addHeader("Accept", | ||
60 | "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3"). | ||
61 | addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", | ||
62 | "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", | ||
63 | "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", | ||
64 | "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build() | ||
65 | |||
66 | val Response response = client.newCall(request).execute() | ||
67 | // TimeUnit.SECONDS.sleep(5) | ||
68 | // return newArrayList( response.body.string.split("\n")) | ||
69 | return response.body.string | ||
70 | |||
71 | // case 1: | ||
72 | } | ||
73 | def static getHeader() { | ||
74 | 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" | ||
75 | } | ||
76 | def static addSpec(String spec) { | ||
77 | return spec.replace("\n", "\r\n") | ||
78 | } | ||
79 | def static addOptions() { | ||
80 | 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" | ||
81 | } | ||
82 | def static addSolver(String ID, String cmd) { | ||
83 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + "\"\r\n\r\n" + ID + "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + "\"\r\n\r\n" + cmd + "\r\n" | ||
84 | } | ||
85 | def static addEnd() { | ||
86 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--" | ||
87 | } | ||
88 | |||
89 | def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, | ||
90 | Ecore2Logic e2l, Ecore2Logic_Trace trace) { | ||
25 | val typeMap = new HashMap<Type, Integer> | 91 | val typeMap = new HashMap<Type, Integer> |
26 | val listMap = metamodel.classes.toMap[s|s.name] | 92 | val listMap = metamodel.classes.toMap[s|s.name] |
27 | 93 | ||
28 | for (Class elem : classMap.keySet) { | 94 | for (Class elem : classMap.keySet) { |
29 | typeMap.put(e2l.TypeofEClass( | 95 | typeMap.put(e2l.TypeofEClass( |
30 | trace, listMap.get(elem.simpleName) | 96 | trace, |
31 | ), classMap.get(elem)) | 97 | listMap.get(elem.simpleName) |
98 | ), classMap.get(elem)) | ||
32 | } | 99 | } |
33 | return typeMap | 100 | return typeMap |
34 | } | 101 | } |
@@ -43,7 +110,7 @@ class GeneralTest { | |||
43 | } | 110 | } |
44 | 111 | ||
45 | def static loadPartialModel(ReasonerWorkspace inputs, String path) { | 112 | def static loadPartialModel(ReasonerWorkspace inputs, String path) { |
46 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); | 113 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()) |
47 | inputs.readModel(EObject, path).eResource.contents | 114 | inputs.readModel(EObject, path).eResource.contents |
48 | // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList | 115 | // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList |
49 | } | 116 | } |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend index 28e3e685..c35b200e 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend | |||
@@ -3,13 +3,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns | 3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
6 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage | 9 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
13 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | 14 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore |
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | 15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic |
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | 16 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration |
@@ -17,8 +18,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.Insta | |||
17 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 18 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
18 | import java.io.PrintWriter | 19 | import java.io.PrintWriter |
19 | import java.text.SimpleDateFormat | 20 | import java.text.SimpleDateFormat |
20 | import java.time.LocalDate | ||
21 | import java.util.Date | 21 | import java.util.Date |
22 | import java.util.HashMap | ||
22 | import org.eclipse.emf.ecore.resource.Resource | 23 | import org.eclipse.emf.ecore.resource.Resource |
23 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 24 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
24 | 25 | ||
@@ -54,16 +55,18 @@ class YakinduTest { | |||
54 | // val queries = null | 55 | // val queries = null |
55 | println("DSL loaded") | 56 | println("DSL loaded") |
56 | 57 | ||
57 | var MAX = 80 | 58 | var SZ_TOP = 10 |
58 | var START = 79 | 59 | var SZ_BOT = 126 |
59 | var INC = 1 | 60 | var INC = 1 |
60 | var REPS = 3 | 61 | var REPS = 1 |
62 | |||
63 | val RANGE = 3 | ||
61 | 64 | ||
62 | val EXACT = 130 | 65 | val EXACT = 10 |
63 | if (EXACT != -1) { | 66 | if (EXACT != -1) { |
64 | MAX = EXACT | 67 | SZ_TOP = EXACT |
65 | START = EXACT | 68 | SZ_BOT = EXACT |
66 | INC = 5 | 69 | INC = 1 |
67 | REPS = 1 | 70 | REPS = 1 |
68 | } | 71 | } |
69 | 72 | ||
@@ -77,8 +80,8 @@ class YakinduTest { | |||
77 | var transformationTimes = newArrayList | 80 | var transformationTimes = newArrayList |
78 | var modelFound = true | 81 | var modelFound = true |
79 | var LogicResult solution = null | 82 | var LogicResult solution = null |
80 | for (var i = START; i <= MAX; i += INC) { | 83 | for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { |
81 | val num = (i - START) / INC | 84 | val num = (i - SZ_BOT) / INC |
82 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") | 85 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") |
83 | writer.append(i + ",") | 86 | writer.append(i + ",") |
84 | solverTimes.clear | 87 | solverTimes.clear |
@@ -106,17 +109,16 @@ class YakinduTest { | |||
106 | 109 | ||
107 | // ///////////////////////////////////////////////////// | 110 | // ///////////////////////////////////////////////////// |
108 | // Minimum Scope | 111 | // Minimum Scope |
109 | // val classMapMin = new HashMap<Class, Integer> | 112 | val classMapMin = new HashMap<Class, Integer> |
110 | // classMapMin.put(Region, 1) | 113 | classMapMin.put(Region, 1) |
111 | // classMapMin.put(Transition, 2) | 114 | classMapMin.put(Transition, 2) |
112 | // classMapMin.put(CompositeElement, 3) | 115 | classMapMin.put(CompositeElement, 3) |
113 | // val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) | 116 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) |
114 | // Maximum Scope | 117 | // Maximum Scope |
115 | // val classMapMax = new HashMap<Class, Integer> | 118 | val classMapMax = new HashMap<Class, Integer> |
116 | // classMapMax.put(Region, 5) | 119 | classMapMax.put(Region, 5) |
117 | // classMapMax.put(Transition, 2) | 120 | classMapMax.put(Transition, 2) |
118 | // classMapMax.put(Synchronization, 4) | 121 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) |
119 | // val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | ||
120 | // Define Config File | 122 | // Define Config File |
121 | val size = i | 123 | val size = i |
122 | val inc = INC | 124 | val inc = INC |
@@ -126,18 +128,18 @@ class YakinduTest { | |||
126 | it.documentationLevel = DocumentationLevel::FULL | 128 | it.documentationLevel = DocumentationLevel::FULL |
127 | it.iteration = iter | 129 | it.iteration = iter |
128 | it.runtimeLimit = 60 | 130 | it.runtimeLimit = 60 |
129 | it.typeScopes.maxNewElements = size | 131 | it.typeScopes.maxNewElements = -1 |
130 | it.typeScopes.minNewElements = size - 5 | 132 | it.typeScopes.minNewElements = size |
131 | 133 | it.genModel = false | |
132 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 134 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
133 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 135 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
134 | it.contCycleLevel = 5 | 136 | it.contCycleLevel = 5 |
135 | it.uniquenessDuplicates = false | 137 | it.uniquenessDuplicates = false |
136 | ] | 138 | ] |
137 | 139 | ||
138 | solution = reasoner.solve(problem, vampireConfig, workspace) | 140 | solution = reasoner.solve(problem, vampireConfig, workspace) |
139 | // print((solution as ModelResult).representation.get(0)) | 141 | // print((solution as ModelResult).representation.get(0)) |
140 | val soln = ((solution as ModelResult).representation.get(0) as VampireModel) | 142 | // val soln = ((solution as ModelResult).representation.get(0) as VampireModel) |
141 | // println(soln.confirmations) | 143 | // println(soln.confirmations) |
142 | // println((solution as ModelResult).representation) | 144 | // println((solution as ModelResult).representation) |
143 | // modelFound = !soln.confirmations.filter [ | 145 | // modelFound = !soln.confirmations.filter [ |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin index 084503b5..93d27b4d 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin index 2315cd50..bc2bae6f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin index a3386941..5687258f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin index dee6f742..de68a908 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin index f54cd3a0..16a3cd03 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java index 7579bd98..8c7923be 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java | |||
@@ -25,6 +25,7 @@ import org.eclipse.emf.ecore.EObject; | |||
25 | import org.eclipse.emf.ecore.resource.Resource; | 25 | import org.eclipse.emf.ecore.resource.Resource; |
26 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; | 26 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; |
27 | import org.eclipse.xtend2.lib.StringConcatenation; | 27 | import org.eclipse.xtend2.lib.StringConcatenation; |
28 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
28 | import org.eclipse.xtext.xbase.lib.InputOutput; | 29 | import org.eclipse.xtext.xbase.lib.InputOutput; |
29 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 30 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
30 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 31 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
@@ -32,70 +33,74 @@ import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | |||
32 | @SuppressWarnings("all") | 33 | @SuppressWarnings("all") |
33 | public class FileSystemTest { | 34 | public class FileSystemTest { |
34 | public static void main(final String[] args) { | 35 | public static void main(final String[] args) { |
35 | final Ecore2Logic ecore2Logic = new Ecore2Logic(); | 36 | try { |
36 | final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); | 37 | final Ecore2Logic ecore2Logic = new Ecore2Logic(); |
37 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); | 38 | final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); |
38 | StringConcatenation _builder = new StringConcatenation(); | 39 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); |
39 | _builder.append("initialModels/"); | 40 | StringConcatenation _builder = new StringConcatenation(); |
40 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); | 41 | _builder.append("initialModels/"); |
41 | StringConcatenation _builder_1 = new StringConcatenation(); | 42 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); |
42 | _builder_1.append("output/FileSystemTest/"); | 43 | StringConcatenation _builder_1 = new StringConcatenation(); |
43 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); | 44 | _builder_1.append("output/FileSystemTest/"); |
44 | workspace.initAndClear(); | 45 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); |
45 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; | 46 | workspace.initAndClear(); |
46 | final Map<String, Object> map = reg.getExtensionToFactoryMap(); | 47 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; |
47 | XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); | 48 | final Map<String, Object> map = reg.getExtensionToFactoryMap(); |
48 | map.put("logicproblem", _xMIResourceFactoryImpl); | 49 | XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); |
49 | InputOutput.<String>println("Input and output workspaces are created"); | 50 | map.put("logicproblem", _xMIResourceFactoryImpl); |
50 | final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); | 51 | InputOutput.<String>println("Input and output workspaces are created"); |
51 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); | 52 | final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); |
52 | InputOutput.<String>println("DSL loaded"); | 53 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); |
53 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); | 54 | InputOutput.<String>println("DSL loaded"); |
54 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); | 55 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); |
55 | LogicProblem problem = modelGenerationProblem.getOutput(); | 56 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); |
56 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); | 57 | LogicProblem problem = modelGenerationProblem.getOutput(); |
57 | workspace.writeModel(problem, "FileSystem.logicproblem"); | 58 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); |
58 | InputOutput.<String>println("Problem created"); | 59 | workspace.writeModel(problem, "FileSystem.logicproblem"); |
59 | long startTime = System.currentTimeMillis(); | 60 | InputOutput.<String>println("Problem created"); |
60 | VampireSolver reasoner = null; | 61 | long startTime = System.currentTimeMillis(); |
61 | VampireSolver _vampireSolver = new VampireSolver(); | 62 | VampireSolver reasoner = null; |
62 | reasoner = _vampireSolver; | 63 | VampireSolver _vampireSolver = new VampireSolver(); |
63 | final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); | 64 | reasoner = _vampireSolver; |
64 | classMapMin.put(Dir.class, Integer.valueOf(10)); | 65 | final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); |
65 | classMapMin.put(File.class, Integer.valueOf(5)); | 66 | classMapMin.put(Dir.class, Integer.valueOf(10)); |
66 | final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); | 67 | classMapMin.put(File.class, Integer.valueOf(5)); |
67 | final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); | 68 | final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); |
68 | classMapMax.put(File.class, Integer.valueOf(15)); | 69 | final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); |
69 | classMapMax.put(Dir.class, Integer.valueOf(15)); | 70 | classMapMax.put(File.class, Integer.valueOf(15)); |
70 | final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); | 71 | classMapMax.put(Dir.class, Integer.valueOf(15)); |
71 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); | 72 | final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); |
72 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { | 73 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); |
73 | it.documentationLevel = DocumentationLevel.FULL; | 74 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { |
74 | it.typeScopes.minNewElements = 10; | 75 | it.documentationLevel = DocumentationLevel.FULL; |
75 | it.typeScopes.maxNewElements = 25; | 76 | it.typeScopes.minNewElements = 10; |
76 | int _size = typeMapMin.size(); | 77 | it.typeScopes.maxNewElements = 25; |
77 | boolean _notEquals = (_size != 0); | 78 | int _size = typeMapMin.size(); |
78 | if (_notEquals) { | 79 | boolean _notEquals = (_size != 0); |
79 | it.typeScopes.minNewElementsByType = typeMapMin; | 80 | if (_notEquals) { |
80 | } | 81 | it.typeScopes.minNewElementsByType = typeMapMin; |
81 | int _size_1 = typeMapMin.size(); | 82 | } |
82 | boolean _notEquals_1 = (_size_1 != 0); | 83 | int _size_1 = typeMapMin.size(); |
83 | if (_notEquals_1) { | 84 | boolean _notEquals_1 = (_size_1 != 0); |
84 | it.typeScopes.maxNewElementsByType = typeMapMax; | 85 | if (_notEquals_1) { |
85 | } | 86 | it.typeScopes.maxNewElementsByType = typeMapMax; |
86 | it.contCycleLevel = 5; | 87 | } |
87 | it.uniquenessDuplicates = false; | 88 | it.contCycleLevel = 5; |
88 | }; | 89 | it.uniquenessDuplicates = false; |
89 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | 90 | }; |
90 | LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS"); | 91 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); |
91 | long _currentTimeMillis = System.currentTimeMillis(); | 92 | LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); |
92 | long _minus = (_currentTimeMillis - startTime); | 93 | long _currentTimeMillis = System.currentTimeMillis(); |
93 | long totalTimeMin = (_minus / 60000); | 94 | long _minus = (_currentTimeMillis - startTime); |
94 | long _currentTimeMillis_1 = System.currentTimeMillis(); | 95 | long totalTimeMin = (_minus / 60000); |
95 | long _minus_1 = (_currentTimeMillis_1 - startTime); | 96 | long _currentTimeMillis_1 = System.currentTimeMillis(); |
96 | long _divide = (_minus_1 / 1000); | 97 | long _minus_1 = (_currentTimeMillis_1 - startTime); |
97 | long totalTimeSec = (_divide % 60); | 98 | long _divide = (_minus_1 / 1000); |
98 | InputOutput.<String>println("Problem solved"); | 99 | long totalTimeSec = (_divide % 60); |
99 | InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); | 100 | InputOutput.<String>println("Problem solved"); |
101 | InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); | ||
102 | } catch (Throwable _e) { | ||
103 | throw Exceptions.sneakyThrow(_e); | ||
104 | } | ||
100 | } | 105 | } |
101 | } | 106 | } |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java index 0bb8f76e..ce057092 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java | |||
@@ -13,6 +13,11 @@ import java.util.HashMap; | |||
13 | import java.util.List; | 13 | import java.util.List; |
14 | import java.util.Map; | 14 | import java.util.Map; |
15 | import java.util.Set; | 15 | import java.util.Set; |
16 | import okhttp3.MediaType; | ||
17 | import okhttp3.OkHttpClient; | ||
18 | import okhttp3.Request; | ||
19 | import okhttp3.RequestBody; | ||
20 | import okhttp3.Response; | ||
16 | import org.eclipse.emf.common.util.EList; | 21 | import org.eclipse.emf.common.util.EList; |
17 | import org.eclipse.emf.ecore.EAttribute; | 22 | import org.eclipse.emf.ecore.EAttribute; |
18 | import org.eclipse.emf.ecore.EClass; | 23 | import org.eclipse.emf.ecore.EClass; |
@@ -28,12 +33,75 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup; | |||
28 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; | 33 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; |
29 | import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; | 34 | import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; |
30 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 35 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
36 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 37 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
38 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | 39 | import org.eclipse.xtext.xbase.lib.IterableExtensions; |
33 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 40 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
34 | 41 | ||
35 | @SuppressWarnings("all") | 42 | @SuppressWarnings("all") |
36 | public class GeneralTest { | 43 | public class GeneralTest { |
44 | private final static String USER_AGENT = "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36"; | ||
45 | |||
46 | public static void main(final String[] args) { | ||
47 | try { | ||
48 | final String form = GeneralTest.makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300); | ||
49 | final String x = GeneralTest.sendPost(form); | ||
50 | InputOutput.<String>print(x.toString()); | ||
51 | } catch (Throwable _e) { | ||
52 | throw Exceptions.sneakyThrow(_e); | ||
53 | } | ||
54 | } | ||
55 | |||
56 | public static String makeForm(final String formula, final String solver, final String cmd, final int time) { | ||
57 | String _header = GeneralTest.getHeader(); | ||
58 | String _addSpec = GeneralTest.addSpec(formula); | ||
59 | String _plus = (_header + _addSpec); | ||
60 | String _addOptions = GeneralTest.addOptions(); | ||
61 | String _plus_1 = (_plus + _addOptions); | ||
62 | String _addSolver = GeneralTest.addSolver(solver, cmd.replace("%d", Integer.valueOf(time).toString())); | ||
63 | String _plus_2 = (_plus_1 + _addSolver); | ||
64 | String _addEnd = GeneralTest.addEnd(); | ||
65 | return (_plus_2 + _addEnd); | ||
66 | } | ||
67 | |||
68 | public static String sendPost(final String formData) throws Exception { | ||
69 | final OkHttpClient client = new OkHttpClient(); | ||
70 | final MediaType mediaType = MediaType.parse( | ||
71 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); | ||
72 | final RequestBody body = RequestBody.create(mediaType, formData); | ||
73 | final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", | ||
74 | "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", | ||
75 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", | ||
76 | "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").addHeader("Accept", | ||
77 | "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", | ||
78 | "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", | ||
79 | "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", | ||
80 | "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build(); | ||
81 | final Response response = client.newCall(request).execute(); | ||
82 | return response.body().string(); | ||
83 | } | ||
84 | |||
85 | public static String getHeader() { | ||
86 | 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"; | ||
87 | } | ||
88 | |||
89 | public static String addSpec(final String spec) { | ||
90 | return spec.replace("\n", "\r\n"); | ||
91 | } | ||
92 | |||
93 | public static String addOptions() { | ||
94 | 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"; | ||
95 | } | ||
96 | |||
97 | public static String addSolver(final String ID, final String cmd) { | ||
98 | return (((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID) + "\"\r\n\r\n") + ID) + "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + "\"\r\n\r\n") + cmd) + "\r\n"); | ||
99 | } | ||
100 | |||
101 | public static String addEnd() { | ||
102 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"; | ||
103 | } | ||
104 | |||
37 | public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { | 105 | public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { |
38 | final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>(); | 106 | final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>(); |
39 | final Function1<EClass, String> _function = (EClass s) -> { | 107 | final Function1<EClass, String> _function = (EClass s) -> { |
@@ -43,7 +111,8 @@ public class GeneralTest { | |||
43 | Set<Class> _keySet = classMap.keySet(); | 111 | Set<Class> _keySet = classMap.keySet(); |
44 | for (final Class elem : _keySet) { | 112 | for (final Class elem : _keySet) { |
45 | typeMap.put( | 113 | typeMap.put( |
46 | e2l.TypeofEClass(trace, listMap.get(elem.getSimpleName())), classMap.get(elem)); | 114 | e2l.TypeofEClass(trace, |
115 | listMap.get(elem.getSimpleName())), classMap.get(elem)); | ||
47 | } | 116 | } |
48 | return typeMap; | 117 | return typeMap; |
49 | } | 118 | } |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java index b18ede4f..3a8f3fb4 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java | |||
@@ -4,17 +4,19 @@ import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; | |||
4 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; | 11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; |
10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; | 12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; |
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; | 13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; |
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; | 14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | 20 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; |
19 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; | 21 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; |
20 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; | 22 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; |
@@ -26,6 +28,7 @@ import java.io.PrintWriter; | |||
26 | import java.text.SimpleDateFormat; | 28 | import java.text.SimpleDateFormat; |
27 | import java.util.ArrayList; | 29 | import java.util.ArrayList; |
28 | import java.util.Date; | 30 | import java.util.Date; |
31 | import java.util.HashMap; | ||
29 | import java.util.Map; | 32 | import java.util.Map; |
30 | import org.eclipse.emf.common.util.EList; | 33 | import org.eclipse.emf.common.util.EList; |
31 | import org.eclipse.emf.common.util.URI; | 34 | import org.eclipse.emf.common.util.URI; |
@@ -72,15 +75,16 @@ public class YakinduTest { | |||
72 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); | 75 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); |
73 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); | 76 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); |
74 | InputOutput.<String>println("DSL loaded"); | 77 | InputOutput.<String>println("DSL loaded"); |
75 | int MAX = 80; | 78 | int SZ_TOP = 10; |
76 | int START = 79; | 79 | int SZ_BOT = 126; |
77 | int INC = 1; | 80 | int INC = 1; |
78 | int REPS = 3; | 81 | int REPS = 1; |
79 | final int EXACT = 130; | 82 | final int RANGE = 3; |
83 | final int EXACT = 10; | ||
80 | if ((EXACT != (-1))) { | 84 | if ((EXACT != (-1))) { |
81 | MAX = EXACT; | 85 | SZ_TOP = EXACT; |
82 | START = EXACT; | 86 | SZ_BOT = EXACT; |
83 | INC = 5; | 87 | INC = 1; |
84 | REPS = 1; | 88 | REPS = 1; |
85 | } | 89 | } |
86 | URI _workspaceURI = workspace.getWorkspaceURI(); | 90 | URI _workspaceURI = workspace.getWorkspaceURI(); |
@@ -96,11 +100,11 @@ public class YakinduTest { | |||
96 | boolean modelFound = true; | 100 | boolean modelFound = true; |
97 | LogicResult solution = null; | 101 | LogicResult solution = null; |
98 | { | 102 | { |
99 | int i = START; | 103 | int i = SZ_BOT; |
100 | boolean _while = (i <= MAX); | 104 | boolean _while = (i <= SZ_TOP); |
101 | while (_while) { | 105 | while (_while) { |
102 | { | 106 | { |
103 | final int num = ((i - START) / INC); | 107 | final int num = ((i - SZ_BOT) / INC); |
104 | InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); | 108 | InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); |
105 | String _plus_3 = (Integer.valueOf(i) + ","); | 109 | String _plus_3 = (Integer.valueOf(i) + ","); |
106 | writer.append(_plus_3); | 110 | writer.append(_plus_3); |
@@ -121,6 +125,15 @@ public class YakinduTest { | |||
121 | VampireSolver reasoner = null; | 125 | VampireSolver reasoner = null; |
122 | VampireSolver _vampireSolver = new VampireSolver(); | 126 | VampireSolver _vampireSolver = new VampireSolver(); |
123 | reasoner = _vampireSolver; | 127 | reasoner = _vampireSolver; |
128 | final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); | ||
129 | classMapMin.put(Region.class, Integer.valueOf(1)); | ||
130 | classMapMin.put(Transition.class, Integer.valueOf(2)); | ||
131 | classMapMin.put(CompositeElement.class, Integer.valueOf(3)); | ||
132 | final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); | ||
133 | final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); | ||
134 | classMapMax.put(Region.class, Integer.valueOf(5)); | ||
135 | classMapMax.put(Transition.class, Integer.valueOf(2)); | ||
136 | final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); | ||
124 | final int size = i; | 137 | final int size = i; |
125 | final int inc = INC; | 138 | final int inc = INC; |
126 | final int iter = j; | 139 | final int iter = j; |
@@ -129,15 +142,24 @@ public class YakinduTest { | |||
129 | it.documentationLevel = DocumentationLevel.FULL; | 142 | it.documentationLevel = DocumentationLevel.FULL; |
130 | it.iteration = iter; | 143 | it.iteration = iter; |
131 | it.runtimeLimit = 60; | 144 | it.runtimeLimit = 60; |
132 | it.typeScopes.maxNewElements = size; | 145 | it.typeScopes.maxNewElements = (-1); |
133 | it.typeScopes.minNewElements = (size - 5); | 146 | it.typeScopes.minNewElements = size; |
147 | it.genModel = false; | ||
148 | int _size = typeMapMin.size(); | ||
149 | boolean _notEquals = (_size != 0); | ||
150 | if (_notEquals) { | ||
151 | it.typeScopes.minNewElementsByType = typeMapMin; | ||
152 | } | ||
153 | int _size_1 = typeMapMin.size(); | ||
154 | boolean _notEquals_1 = (_size_1 != 0); | ||
155 | if (_notEquals_1) { | ||
156 | it.typeScopes.maxNewElementsByType = typeMapMax; | ||
157 | } | ||
134 | it.contCycleLevel = 5; | 158 | it.contCycleLevel = 5; |
135 | it.uniquenessDuplicates = false; | 159 | it.uniquenessDuplicates = false; |
136 | }; | 160 | }; |
137 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | 161 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); |
138 | solution = reasoner.solve(problem, vampireConfig, workspace); | 162 | solution = reasoner.solve(problem, vampireConfig, workspace); |
139 | Object _get = ((ModelResult) solution).getRepresentation().get(0); | ||
140 | final VampireModel soln = ((VampireModel) _get); | ||
141 | int _transformationTime = solution.getStatistics().getTransformationTime(); | 163 | int _transformationTime = solution.getStatistics().getTransformationTime(); |
142 | final double tTime = (_transformationTime / 1000.0); | 164 | final double tTime = (_transformationTime / 1000.0); |
143 | int _solverTime = solution.getStatistics().getSolverTime(); | 165 | int _solverTime = solution.getStatistics().getSolverTime(); |
@@ -163,7 +185,7 @@ public class YakinduTest { | |||
163 | } | 185 | } |
164 | int _i = i; | 186 | int _i = i; |
165 | i = (_i + INC); | 187 | i = (_i + INC); |
166 | _while = (i <= MAX); | 188 | _while = (i <= SZ_TOP); |
167 | } | 189 | } |
168 | } | 190 | } |
169 | writer.close(); | 191 | writer.close(); |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin index e77449e7..96f343fa 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin index 97f29b0c..1ca8223d 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin index 0e320f18..5d6a9ee2 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin | |||
Binary files differ | |||