diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-11 15:51:49 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:17 -0400 |
commit | 606f6965f3ccec837aa216cbb3f56fdcf943a59b (patch) | |
tree | e9d1283f60b335de331b5e8abd93f040636f871b | |
parent | implement http requests for the TPTP server (diff) | |
download | VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.tar.gz VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.tar.zst VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.zip |
VAMPIRE: complete testing setup
51 files changed, 723 insertions, 384 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 1eaefbda..8225ed58 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 05c29aff..5d455790 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 12f063b1..db1a37c4 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 88a713db..32d2213b 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 31d3dbf6..24c6eca6 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 ca30b3d0..422fad02 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 0d75d237..d6bf1d6f 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 a8d38a91..d341af67 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 0192cd3c..2f552529 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 07f4c611..f73dadba 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 01c9f74f..0b18e8e6 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 b4bd4155..8dac584b 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 5dd72d15..ee3df0a3 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 db384a64..96ae5822 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/.classpath b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath index 2a126610..f6de9681 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath | |||
@@ -6,5 +6,11 @@ | |||
6 | <classpathentry kind="src" path="xtend-gen"/> | 6 | <classpathentry kind="src" path="xtend-gen"/> |
7 | <classpathentry kind="src" path="queries"/> | 7 | <classpathentry kind="src" path="queries"/> |
8 | <classpathentry kind="src" path="src-gen"/> | 8 | <classpathentry kind="src" path="src-gen"/> |
9 | <classpathentry kind="lib" path="lib/annotations-13.0.jar"/> | ||
10 | <classpathentry kind="lib" path="lib/kotlin-stdlib-1.3.50.jar"/> | ||
11 | <classpathentry kind="lib" path="lib/kotlin-stdlib-common-1.3.50.jar"/> | ||
12 | <classpathentry kind="lib" path="lib/okhttp-4.2.0.jar"/> | ||
13 | <classpathentry kind="lib" path="lib/okio-2.2.2.jar"/> | ||
14 | <classpathentry kind="lib" path="lib/unirest-java-1.4.9.jar"/> | ||
9 | <classpathentry kind="output" path="bin"/> | 15 | <classpathentry kind="output" path="bin"/> |
10 | </classpath> | 16 | </classpath> |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend index 4e9737cb..4c2f1952 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend | |||
@@ -2,21 +2,29 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner | |||
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
4 | 4 | ||
5 | class VampireSolverConfiguration extends LogicSolverConfiguration { | 5 | class VampireSolverConfiguration |
6 | extends LogicSolverConfiguration { | ||
6 | 7 | ||
7 | public var int contCycleLevel = 0 | 8 | public var int contCycleLevel = 0 |
8 | public var boolean uniquenessDuplicates = false | 9 | public var boolean uniquenessDuplicates = false |
9 | public var int iteration = -1 | 10 | public var int iteration = -1 |
10 | public var BackendSolver solver = BackendSolver::VAMP | 11 | public var BackendSolver solver = BackendSolver::VAMPIRE |
11 | public var genModel = true | 12 | public var genModel = true |
13 | public var server = false | ||
12 | //choose needed backend solver | 14 | //choose needed backend solver |
13 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J | 15 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J |
14 | } | 16 | } |
15 | 17 | ||
16 | 18 | ||
17 | enum BackendSolver { | 19 | enum BackendSolver { |
18 | VAMP, | 20 | CVC4, |
19 | CVC4 | 21 | DARWINFM, |
22 | EDARWIN, | ||
23 | GEOIII, | ||
24 | IPROVER, | ||
25 | PARADOX, | ||
26 | VAMPIRE, | ||
27 | Z3 | ||
20 | //add needed things | 28 | //add needed things |
21 | } | 29 | } |
22 | 30 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend index 85b81a8c..31aa091c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend | |||
@@ -4,18 +4,20 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | |||
4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated | 4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution | 8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper | 9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper |
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler | 10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler |
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation | 11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
20 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 22 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
21 | 23 | ||
@@ -30,18 +32,20 @@ class VampireSolver extends LogicReasoner { | |||
30 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper | 32 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper |
31 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | 33 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper |
32 | val VampireHandler handler = new VampireHandler | 34 | val VampireHandler handler = new VampireHandler |
35 | val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
36 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | ||
37 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
33 | 38 | ||
34 | // var fileName = "problem.tptp" | 39 | // var fileName = "problem.tptp" |
35 | |||
36 | // def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { | 40 | // def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { |
37 | // fileName = location + fileName | 41 | // fileName = location + fileName |
38 | // solve(problem, config, workspace) | 42 | // solve(problem, config, workspace) |
39 | // } | 43 | // } |
40 | |||
41 | override solve(LogicProblem problem, LogicSolverConfiguration config, | 44 | override solve(LogicProblem problem, LogicSolverConfiguration config, |
42 | ReasonerWorkspace workspace) throws LogicReasonerException { | 45 | ReasonerWorkspace workspace) throws LogicReasonerException { |
43 | val vampireConfig = config.asConfig | 46 | val vampireConfig = config.asConfig |
44 | var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + vampireConfig.typeScopes.maxNewElements + ".tptp" | 47 | var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + |
48 | vampireConfig.typeScopes.maxNewElements + ".tptp" | ||
45 | 49 | ||
46 | // Start: Logic -> Vampire mapping | 50 | // Start: Logic -> Vampire mapping |
47 | val transformationStart = System.currentTimeMillis | 51 | val transformationStart = System.currentTimeMillis |
@@ -55,8 +59,6 @@ class VampireSolver extends LogicReasoner { | |||
55 | var String fileURI = null; | 59 | var String fileURI = null; |
56 | var String vampireCode = null; | 60 | var String vampireCode = null; |
57 | vampireCode = workspace.writeModelToString(vampireProblem, fileName) | 61 | vampireCode = workspace.writeModelToString(vampireProblem, fileName) |
58 | |||
59 | |||
60 | 62 | ||
61 | val writeFile = ( | 63 | val writeFile = ( |
62 | vampireConfig.documentationLevel === DocumentationLevel::NORMAL || | 64 | vampireConfig.documentationLevel === DocumentationLevel::NORMAL || |
@@ -73,24 +75,94 @@ class VampireSolver extends LogicReasoner { | |||
73 | // println(model) | 75 | // println(model) |
74 | // Finish: Logic -> Vampire mapping | 76 | // Finish: Logic -> Vampire mapping |
75 | if (vampireConfig.genModel) { | 77 | if (vampireConfig.genModel) { |
76 | 78 | if (vampireConfig.server) { | |
77 | // Start: Solving .tptp problem | 79 | val form = support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit) |
78 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | 80 | var response = newArrayList |
79 | // Finish: Solving .tptp problem | 81 | var ind = 0 |
80 | // Start: Vampire -> Logic mapping | 82 | var done = false |
81 | val backTransformationStart = System.currentTimeMillis | 83 | print(" ") |
82 | // Backwards Mapper | 84 | while (!done) { |
83 | val logicResult = backwardMapper.transformOutput(problem, | 85 | print("(x)") |
84 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) | 86 | done = false |
85 | 87 | response = support.sendPost(form) | |
86 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | 88 | |
87 | // Finish: Vampire -> Logic Mapping | 89 | var responseFound = false |
90 | ind = 0 | ||
91 | while (!responseFound) { | ||
92 | var line = response.get(ind) | ||
93 | if (line.length >= 5 && line.substring(0, 5) == "ERROR") { | ||
94 | done = false | ||
95 | responseFound = true | ||
96 | } else { | ||
97 | if (line == "</PRE>") { | ||
98 | done = true | ||
99 | responseFound = true | ||
100 | } | ||
101 | } | ||
102 | ind++ | ||
103 | } | ||
104 | } | ||
105 | val satRaw = response.get(ind - 3) | ||
106 | val modRaw = response.get(ind - 2) | ||
107 | |||
108 | val sat = newArrayList(satRaw.split(" ")) | ||
109 | val mod = newArrayList(modRaw.split(" ")) | ||
110 | |||
111 | val satOut = sat.get(1) | ||
112 | val modOut = mod.get(1) | ||
113 | val satTime = sat.get(2) | ||
114 | val modTime = mod.get(2) | ||
115 | |||
116 | println() | ||
117 | println(sat) | ||
118 | println(mod) | ||
119 | |||
120 | return createModelResult => [ | ||
121 | it.problem = null | ||
122 | it.representation += createVampireModel => [] | ||
123 | it.trace = trace | ||
124 | it.statistics = createStatistics => [ | ||
125 | it.transformationTime = transformationTime as int | ||
126 | it.entries += createStringStatisticEntry => [ | ||
127 | it.name = "satOut" | ||
128 | it.value = satOut | ||
129 | ] | ||
130 | it.entries += createRealStatisticEntry => [ | ||
131 | it.name = "satTime" | ||
132 | it.value = Double.parseDouble(satTime) | ||
133 | ] | ||
134 | it.entries += createStringStatisticEntry => [ | ||
135 | it.name = "modOut" | ||
136 | it.value = modOut | ||
137 | ] | ||
138 | it.entries += createRealStatisticEntry => [ | ||
139 | it.name = "modTime" | ||
140 | it.value = Double.parseDouble(modTime) | ||
141 | ] | ||
142 | |||
143 | ] | ||
144 | ] | ||
145 | |||
146 | // return newArrayList(line1, line2) | ||
147 | } else { | ||
148 | |||
149 | // Start: Solving .tptp problem | ||
150 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | ||
151 | // Finish: Solving .tptp problem | ||
152 | // Start: Vampire -> Logic mapping | ||
153 | val backTransformationStart = System.currentTimeMillis | ||
154 | // Backwards Mapper | ||
155 | val logicResult = backwardMapper.transformOutput(problem, | ||
156 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) | ||
157 | |||
158 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | ||
159 | // Finish: Vampire -> Logic Mapping | ||
88 | // print(vampSol.generatedModel.tfformulas.size) | 160 | // print(vampSol.generatedModel.tfformulas.size) |
89 | return logicResult // currently only a ModelResult | 161 | return logicResult // currently only a ModelResult |
162 | } | ||
90 | } | 163 | } |
91 | 164 | return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, | |
92 | return backwardMapper.transformOutput(problem, | 165 | new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) |
93 | vampireConfig.solutionScope.numberOfRequiredSolution, new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) | ||
94 | } | 166 | } |
95 | 167 | ||
96 | def asConfig(LogicSolverConfiguration configuration) { | 168 | def asConfig(LogicSolverConfiguration configuration) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index 39862c65..a9516cc4 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend | |||
@@ -40,7 +40,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
40 | // Equals the number of elements in te initial model | 40 | // Equals the number of elements in te initial model |
41 | var elemsInIM = trace.definedElement2String.size | 41 | var elemsInIM = trace.definedElement2String.size |
42 | val ABSOLUTE_MIN = 0 | 42 | val ABSOLUTE_MIN = 0 |
43 | val ABSOLUTE_MAX = -1-elemsInIM | 43 | val ABSOLUTE_MAX = Integer.MAX_VALUE-elemsInIM |
44 | // var elemsInIM = 0 | 44 | // var elemsInIM = 0 |
45 | // | 45 | // |
46 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { | 46 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { |
@@ -60,7 +60,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
60 | 60 | ||
61 | // Handling Minimum_General | 61 | // Handling Minimum_General |
62 | if (GLOBAL_MIN != ABSOLUTE_MIN) { | 62 | if (GLOBAL_MIN != ABSOLUTE_MIN) { |
63 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant) | 63 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant)//may make not consistent here |
64 | if (consistant) { | 64 | if (consistant) { |
65 | for (i : trace.uniqueInstances) { | 65 | for (i : trace.uniqueInstances) { |
66 | localInstances.add(support.duplicate(i)) | 66 | localInstances.add(support.duplicate(i)) |
@@ -73,7 +73,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
73 | 73 | ||
74 | // Handling Maximum_General | 74 | // Handling Maximum_General |
75 | if (GLOBAL_MAX != ABSOLUTE_MAX) { | 75 | if (GLOBAL_MAX != ABSOLUTE_MAX) { |
76 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant) | 76 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, !consistant) |
77 | if (consistant) { | 77 | if (consistant) { |
78 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) | 78 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) |
79 | } else { | 79 | } else { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index 680213ab..7b1c7d9a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | |||
@@ -1,5 +1,6 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm |
@@ -16,6 +17,12 @@ import java.util.ArrayList | |||
16 | import java.util.HashMap | 17 | import java.util.HashMap |
17 | import java.util.List | 18 | import java.util.List |
18 | import java.util.Map | 19 | import java.util.Map |
20 | import java.util.concurrent.TimeUnit | ||
21 | import okhttp3.MediaType | ||
22 | import okhttp3.OkHttpClient | ||
23 | import okhttp3.Request | ||
24 | import okhttp3.RequestBody | ||
25 | import okhttp3.Response | ||
19 | import org.eclipse.emf.common.util.EList | 26 | import org.eclipse.emf.common.util.EList |
20 | 27 | ||
21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
@@ -77,13 +84,13 @@ class Logic2VampireLanguageMapper_Support { | |||
77 | it.terms += duplicate(v) | 84 | it.terms += duplicate(v) |
78 | ] | 85 | ] |
79 | } | 86 | } |
80 | 87 | ||
81 | def protected List<VLSVariable> duplicate(List<VLSVariable> vars) { | 88 | def protected List<VLSVariable> duplicate(List<VLSVariable> vars) { |
82 | var newList = newArrayList | 89 | var newList = newArrayList |
83 | for (v : vars) { | 90 | for (v : vars) { |
84 | newList.add(duplicate(v)) | 91 | newList.add(duplicate(v)) |
85 | } | 92 | } |
86 | return newList | 93 | return newList |
87 | } | 94 | } |
88 | 95 | ||
89 | def protected VLSConstant toConstant(VLSFunctionAsTerm term) { | 96 | def protected VLSConstant toConstant(VLSFunctionAsTerm term) { |
@@ -117,7 +124,7 @@ class Logic2VampireLanguageMapper_Support { | |||
117 | 124 | ||
118 | // TODO Make more general | 125 | // TODO Make more general |
119 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { | 126 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { |
120 | 127 | ||
121 | // OLD | 128 | // OLD |
122 | // val List<VLSInequality> eqs = newArrayList | 129 | // val List<VLSInequality> eqs = newArrayList |
123 | // for (t1 : terms.subList(1, terms.length)) { | 130 | // for (t1 : terms.subList(1, terms.length)) { |
@@ -133,7 +140,6 @@ class Logic2VampireLanguageMapper_Support { | |||
133 | // } | 140 | // } |
134 | // return unfoldAnd(eqs) | 141 | // return unfoldAnd(eqs) |
135 | // END OLD | 142 | // END OLD |
136 | |||
137 | val List<VLSInequality> eqs = newArrayList | 143 | val List<VLSInequality> eqs = newArrayList |
138 | for (t1 : terms) { | 144 | for (t1 : terms) { |
139 | if (t1 != t2) { | 145 | if (t1 != t2) { |
@@ -257,7 +263,8 @@ class Logic2VampireLanguageMapper_Support { | |||
257 | } | 263 | } |
258 | } | 264 | } |
259 | } | 265 | } |
260 | //TODO rewrite such that it uses "listSubTypes" | 266 | |
267 | // TODO rewrite such that it uses "listSubTypes" | ||
261 | def protected boolean dfsSubtypeCheck(Type type, Type type2) { | 268 | def protected boolean dfsSubtypeCheck(Type type, Type type2) { |
262 | // There is surely a better way to do this | 269 | // There is surely a better way to do this |
263 | if (type.subtypes.isEmpty) | 270 | if (type.subtypes.isEmpty) |
@@ -284,4 +291,74 @@ class Logic2VampireLanguageMapper_Support { | |||
284 | new HashMap(map1) => [putAll(map2)] | 291 | new HashMap(map1) => [putAll(map2)] |
285 | } | 292 | } |
286 | 293 | ||
294 | // SERVERS | ||
295 | def makeForm(String formula, BackendSolver solver, int time) { | ||
296 | return header + formula + addOptions + addSolver(solver, time) + addEnd | ||
297 | } | ||
298 | |||
299 | def getSolverSpecs(BackendSolver solver) { | ||
300 | switch (solver) { | ||
301 | case BackendSolver::CVC4: return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") | ||
302 | case BackendSolver::DARWINFM: return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") | ||
303 | case BackendSolver::EDARWIN: return newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") | ||
304 | case BackendSolver::GEOIII: return newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") | ||
305 | case BackendSolver::IPROVER: return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") | ||
306 | case BackendSolver::PARADOX: return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") | ||
307 | case BackendSolver::VAMPIRE: return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") | ||
308 | case BackendSolver::Z3: return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s") | ||
309 | } | ||
310 | } | ||
311 | |||
312 | def getHeader() { | ||
313 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n" | ||
314 | } | ||
315 | |||
316 | def addSpec(String spec) { | ||
317 | return spec.replace("\n", "\\r\\n") | ||
318 | } | ||
319 | |||
320 | def addOptions() { | ||
321 | return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n" | ||
322 | } | ||
323 | |||
324 | def addSolver(BackendSolver solver, int time) { | ||
325 | val solverSpecs = getSolverSpecs(solver) | ||
326 | val ID = solverSpecs.get(0) | ||
327 | val cmd = solverSpecs.get(1) | ||
328 | |||
329 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + | ||
330 | "\"\r\n\r\n" + ID + | ||
331 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + | ||
332 | "\"\r\n\r\n" + cmd.replace("%d", time.toString) + "\r\n" | ||
333 | } | ||
334 | |||
335 | def addEnd() { | ||
336 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--" | ||
337 | } | ||
338 | |||
339 | def sendPost(String formData) throws Exception { | ||
340 | |||
341 | val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build() | ||
342 | |||
343 | val MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") | ||
344 | val RequestBody body = RequestBody.create(mediaType, formData) | ||
345 | val Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body). | ||
346 | addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", | ||
347 | "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", | ||
348 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", | ||
349 | "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36"). | ||
350 | addHeader("Accept", | ||
351 | "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3"). | ||
352 | addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", | ||
353 | "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", | ||
354 | "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", | ||
355 | "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build() | ||
356 | |||
357 | val Response response = client.newCall(request).execute() | ||
358 | // TimeUnit.SECONDS.sleep(5) | ||
359 | return newArrayList(response.body.string.split("\n")) | ||
360 | // return response.body.string | ||
361 | // case 1: | ||
362 | } | ||
363 | |||
287 | } | 364 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend index 47eae807..6d301442 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | |||
@@ -70,7 +70,7 @@ class VampireHandler { | |||
70 | var long startTime = -1 as long | 70 | var long startTime = -1 as long |
71 | var long solverTime = -1 as long | 71 | var long solverTime = -1 as long |
72 | var Process p = null | 72 | var Process p = null |
73 | if (configuration.solver == BackendSolver::VAMP) { | 73 | if (configuration.solver == BackendSolver::VAMPIRE) { |
74 | 74 | ||
75 | var OPTION = " --mode casc_sat " | 75 | var OPTION = " --mode casc_sat " |
76 | if (configuration.runtimeLimit != -1) { | 76 | if (configuration.runtimeLimit != -1) { |
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 e50e6812..b26c1ded 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 e4925e24..fb8f872d 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 432b14c3..3e3bd688 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 | |||
@@ -5,12 +5,15 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated; | |||
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.reasoner.builder.Logic2VampireLanguageMapper; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; | 9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; |
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; |
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | 11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; |
11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; | 12 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
16 | import com.google.common.base.Objects; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; |
@@ -19,13 +22,25 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | |||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; | ||
23 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 31 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
32 | import java.util.ArrayList; | ||
24 | import java.util.List; | 33 | import java.util.List; |
25 | import org.eclipse.emf.common.util.EList; | 34 | import org.eclipse.emf.common.util.EList; |
26 | import org.eclipse.xtend2.lib.StringConcatenation; | 35 | import org.eclipse.xtend2.lib.StringConcatenation; |
36 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
37 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
38 | import org.eclipse.xtext.xbase.lib.Extension; | ||
27 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 39 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
40 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
28 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 41 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
42 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
43 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
29 | 44 | ||
30 | @SuppressWarnings("all") | 45 | @SuppressWarnings("all") |
31 | public class VampireSolver extends LogicReasoner { | 46 | public class VampireSolver extends LogicReasoner { |
@@ -41,36 +56,142 @@ public class VampireSolver extends LogicReasoner { | |||
41 | 56 | ||
42 | private final VampireHandler handler = new VampireHandler(); | 57 | private final VampireHandler handler = new VampireHandler(); |
43 | 58 | ||
59 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
60 | |||
61 | @Extension | ||
62 | private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE; | ||
63 | |||
64 | @Extension | ||
65 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
66 | |||
44 | @Override | 67 | @Override |
45 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { | 68 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { |
46 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); | 69 | try { |
47 | String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp"); | 70 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); |
48 | final long transformationStart = System.currentTimeMillis(); | 71 | String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + |
49 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | 72 | Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp"); |
50 | long _currentTimeMillis = System.currentTimeMillis(); | 73 | final long transformationStart = System.currentTimeMillis(); |
51 | final long transformationTime = (_currentTimeMillis - transformationStart); | 74 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); |
52 | final VampireModel vampireProblem = result.getOutput(); | 75 | long _currentTimeMillis = System.currentTimeMillis(); |
53 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | 76 | final long transformationTime = (_currentTimeMillis - transformationStart); |
54 | String fileURI = null; | 77 | final VampireModel vampireProblem = result.getOutput(); |
55 | String vampireCode = null; | 78 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); |
56 | vampireCode = workspace.writeModelToString(vampireProblem, fileName); | 79 | String fileURI = null; |
57 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || | 80 | String vampireCode = null; |
58 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); | 81 | vampireCode = workspace.writeModelToString(vampireProblem, fileName); |
59 | if (writeFile) { | 82 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || |
60 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString(); | 83 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); |
61 | } | 84 | if (writeFile) { |
62 | if (vampireConfig.genModel) { | 85 | fileURI = workspace.writeModel(vampireProblem, fileName).toFileString(); |
63 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | 86 | } |
64 | final long backTransformationStart = System.currentTimeMillis(); | 87 | if (vampireConfig.genModel) { |
65 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, | 88 | if (vampireConfig.server) { |
66 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | 89 | final String form = this.support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit); |
67 | long _currentTimeMillis_1 = System.currentTimeMillis(); | 90 | ArrayList<String> response = CollectionLiterals.<String>newArrayList(); |
68 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | 91 | int ind = 0; |
69 | return logicResult; | 92 | boolean done = false; |
93 | InputOutput.<String>print(" "); | ||
94 | while ((!done)) { | ||
95 | { | ||
96 | InputOutput.<String>print("(x)"); | ||
97 | done = false; | ||
98 | response = this.support.sendPost(form); | ||
99 | boolean responseFound = false; | ||
100 | ind = 0; | ||
101 | while ((!responseFound)) { | ||
102 | { | ||
103 | String line = response.get(ind); | ||
104 | if (((line.length() >= 5) && Objects.equal(line.substring(0, 5), "ERROR"))) { | ||
105 | done = false; | ||
106 | responseFound = true; | ||
107 | } else { | ||
108 | boolean _equals = Objects.equal(line, "</PRE>"); | ||
109 | if (_equals) { | ||
110 | done = true; | ||
111 | responseFound = true; | ||
112 | } | ||
113 | } | ||
114 | ind++; | ||
115 | } | ||
116 | } | ||
117 | } | ||
118 | } | ||
119 | final String satRaw = response.get((ind - 3)); | ||
120 | final String modRaw = response.get((ind - 2)); | ||
121 | final ArrayList<String> sat = CollectionLiterals.<String>newArrayList(satRaw.split(" ")); | ||
122 | final ArrayList<String> mod = CollectionLiterals.<String>newArrayList(modRaw.split(" ")); | ||
123 | final String satOut = sat.get(1); | ||
124 | final String modOut = mod.get(1); | ||
125 | final String satTime = sat.get(2); | ||
126 | final String modTime = mod.get(2); | ||
127 | InputOutput.println(); | ||
128 | InputOutput.<ArrayList<String>>println(sat); | ||
129 | InputOutput.<ArrayList<String>>println(mod); | ||
130 | ModelResult _createModelResult = this.resultFactory.createModelResult(); | ||
131 | final Procedure1<ModelResult> _function = (ModelResult it) -> { | ||
132 | it.setProblem(null); | ||
133 | EList<Object> _representation = it.getRepresentation(); | ||
134 | VampireModel _createVampireModel = this.factory.createVampireModel(); | ||
135 | final Procedure1<VampireModel> _function_1 = (VampireModel it_1) -> { | ||
136 | }; | ||
137 | VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1); | ||
138 | _representation.add(_doubleArrow); | ||
139 | it.setTrace(it.getTrace()); | ||
140 | Statistics _createStatistics = this.resultFactory.createStatistics(); | ||
141 | final Procedure1<Statistics> _function_2 = (Statistics it_1) -> { | ||
142 | it_1.setTransformationTime(((int) transformationTime)); | ||
143 | EList<StatisticEntry> _entries = it_1.getEntries(); | ||
144 | StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); | ||
145 | final Procedure1<StringStatisticEntry> _function_3 = (StringStatisticEntry it_2) -> { | ||
146 | it_2.setName("satOut"); | ||
147 | it_2.setValue(satOut); | ||
148 | }; | ||
149 | StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3); | ||
150 | _entries.add(_doubleArrow_1); | ||
151 | EList<StatisticEntry> _entries_1 = it_1.getEntries(); | ||
152 | RealStatisticEntry _createRealStatisticEntry = this.resultFactory.createRealStatisticEntry(); | ||
153 | final Procedure1<RealStatisticEntry> _function_4 = (RealStatisticEntry it_2) -> { | ||
154 | it_2.setName("satTime"); | ||
155 | it_2.setValue(Double.parseDouble(satTime)); | ||
156 | }; | ||
157 | RealStatisticEntry _doubleArrow_2 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry, _function_4); | ||
158 | _entries_1.add(_doubleArrow_2); | ||
159 | EList<StatisticEntry> _entries_2 = it_1.getEntries(); | ||
160 | StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); | ||
161 | final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> { | ||
162 | it_2.setName("modOut"); | ||
163 | it_2.setValue(modOut); | ||
164 | }; | ||
165 | StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5); | ||
166 | _entries_2.add(_doubleArrow_3); | ||
167 | EList<StatisticEntry> _entries_3 = it_1.getEntries(); | ||
168 | RealStatisticEntry _createRealStatisticEntry_1 = this.resultFactory.createRealStatisticEntry(); | ||
169 | final Procedure1<RealStatisticEntry> _function_6 = (RealStatisticEntry it_2) -> { | ||
170 | it_2.setName("modTime"); | ||
171 | it_2.setValue(Double.parseDouble(modTime)); | ||
172 | }; | ||
173 | RealStatisticEntry _doubleArrow_4 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry_1, _function_6); | ||
174 | _entries_3.add(_doubleArrow_4); | ||
175 | }; | ||
176 | Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2); | ||
177 | it.setStatistics(_doubleArrow_1); | ||
178 | }; | ||
179 | return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function); | ||
180 | } else { | ||
181 | final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); | ||
182 | final long backTransformationStart = System.currentTimeMillis(); | ||
183 | final ModelResult logicResult = this.backwardMapper.transformOutput(problem, | ||
184 | vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); | ||
185 | long _currentTimeMillis_1 = System.currentTimeMillis(); | ||
186 | final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); | ||
187 | return logicResult; | ||
188 | } | ||
189 | } | ||
190 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); | ||
191 | return this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); | ||
192 | } catch (Throwable _e) { | ||
193 | throw Exceptions.sneakyThrow(_e); | ||
70 | } | 194 | } |
71 | MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); | ||
72 | return this.backwardMapper.transformOutput(problem, | ||
73 | vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); | ||
74 | } | 195 | } |
75 | 196 | ||
76 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | 197 | 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 dd66e910..c094872e 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 | |||
@@ -11,7 +11,9 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration { | |||
11 | 11 | ||
12 | public int iteration = (-1); | 12 | public int iteration = (-1); |
13 | 13 | ||
14 | public BackendSolver solver = BackendSolver.VAMP; | 14 | public BackendSolver solver = BackendSolver.VAMPIRE; |
15 | 15 | ||
16 | public boolean genModel = true; | 16 | public boolean genModel = true; |
17 | |||
18 | public boolean server = false; | ||
17 | } | 19 | } |
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 8d2ec6ab..8b7f031e 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 515b4b3c..1b6e8f80 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 46ad8c79..f523f1af 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 169aedc2..30ba1843 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 699ce6e2..174c7362 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 799515d4..affa3754 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 2a112ae7..6c7c7522 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 7f32e055..5be67889 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 a2dd469b..192c9d1a 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 98c355ab..0495ab53 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 246c08c8..c438f1e5 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 9e55bac4..5fb9b455 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 bc39a068..c09d929e 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 | |||
@@ -55,13 +55,13 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
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 | int elemsInIM = trace.definedElement2String.size(); | 56 | int elemsInIM = trace.definedElement2String.size(); |
57 | final int ABSOLUTE_MIN = 0; | 57 | final int ABSOLUTE_MIN = 0; |
58 | final int ABSOLUTE_MAX = ((-1) - elemsInIM); | 58 | final int ABSOLUTE_MAX = (Integer.MAX_VALUE - 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(); |
62 | final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); | 62 | final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); |
63 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { | 63 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { |
64 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant)); | 64 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant); |
65 | if (consistant) { | 65 | if (consistant) { |
66 | for (final VLSConstant i : trace.uniqueInstances) { | 66 | for (final VLSConstant i : trace.uniqueInstances) { |
67 | localInstances.add(this.support.duplicate(i)); | 67 | localInstances.add(this.support.duplicate(i)); |
@@ -72,7 +72,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
72 | } | 72 | } |
73 | } | 73 | } |
74 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { | 74 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { |
75 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant); | 75 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, (!consistant)); |
76 | if (consistant) { | 76 | if (consistant) { |
77 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); | 77 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); |
78 | } else { | 78 | } else { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index dae0df6e..1255b25c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |||
@@ -1,5 +1,6 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver; | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; |
@@ -29,6 +30,12 @@ import java.util.Collection; | |||
29 | import java.util.HashMap; | 30 | import java.util.HashMap; |
30 | import java.util.List; | 31 | import java.util.List; |
31 | import java.util.Map; | 32 | import java.util.Map; |
33 | import java.util.concurrent.TimeUnit; | ||
34 | import okhttp3.MediaType; | ||
35 | import okhttp3.OkHttpClient; | ||
36 | import okhttp3.Request; | ||
37 | import okhttp3.RequestBody; | ||
38 | import okhttp3.Response; | ||
32 | import org.eclipse.emf.common.util.EList; | 39 | import org.eclipse.emf.common.util.EList; |
33 | import org.eclipse.xtend2.lib.StringConcatenation; | 40 | import org.eclipse.xtend2.lib.StringConcatenation; |
34 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 41 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
@@ -421,4 +428,85 @@ public class Logic2VampireLanguageMapper_Support { | |||
421 | }; | 428 | }; |
422 | return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function); | 429 | return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function); |
423 | } | 430 | } |
431 | |||
432 | public String makeForm(final String formula, final BackendSolver solver, final int time) { | ||
433 | String _header = this.getHeader(); | ||
434 | String _plus = (_header + formula); | ||
435 | String _addOptions = this.addOptions(); | ||
436 | String _plus_1 = (_plus + _addOptions); | ||
437 | String _addSolver = this.addSolver(solver, time); | ||
438 | String _plus_2 = (_plus_1 + _addSolver); | ||
439 | String _addEnd = this.addEnd(); | ||
440 | return (_plus_2 + _addEnd); | ||
441 | } | ||
442 | |||
443 | public ArrayList<String> getSolverSpecs(final BackendSolver solver) { | ||
444 | if (solver != null) { | ||
445 | switch (solver) { | ||
446 | case CVC4: | ||
447 | return CollectionLiterals.<String>newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT"); | ||
448 | case DARWINFM: | ||
449 | return CollectionLiterals.<String>newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s"); | ||
450 | case EDARWIN: | ||
451 | return CollectionLiterals.<String>newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s"); | ||
452 | case GEOIII: | ||
453 | return CollectionLiterals.<String>newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s"); | ||
454 | case IPROVER: | ||
455 | return CollectionLiterals.<String>newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s"); | ||
456 | case PARADOX: | ||
457 | return CollectionLiterals.<String>newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s"); | ||
458 | case VAMPIRE: | ||
459 | return CollectionLiterals.<String>newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s"); | ||
460 | case Z3: | ||
461 | return CollectionLiterals.<String>newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s"); | ||
462 | default: | ||
463 | break; | ||
464 | } | ||
465 | } | ||
466 | return null; | ||
467 | } | ||
468 | |||
469 | public String getHeader() { | ||
470 | 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"; | ||
471 | } | ||
472 | |||
473 | public String addSpec(final String spec) { | ||
474 | return spec.replace("\n", "\\r\\n"); | ||
475 | } | ||
476 | |||
477 | public String addOptions() { | ||
478 | 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"; | ||
479 | } | ||
480 | |||
481 | public String addSolver(final BackendSolver solver, final int time) { | ||
482 | final ArrayList<String> solverSpecs = this.getSolverSpecs(solver); | ||
483 | final String ID = solverSpecs.get(0); | ||
484 | final String cmd = solverSpecs.get(1); | ||
485 | String _replace = cmd.replace("%d", Integer.valueOf(time).toString()); | ||
486 | String _plus = ((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID) + | ||
487 | "\"\r\n\r\n") + ID) + | ||
488 | "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + | ||
489 | "\"\r\n\r\n") + _replace); | ||
490 | return (_plus + "\r\n"); | ||
491 | } | ||
492 | |||
493 | public String addEnd() { | ||
494 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"; | ||
495 | } | ||
496 | |||
497 | public ArrayList<String> sendPost(final String formData) throws Exception { | ||
498 | final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build(); | ||
499 | final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); | ||
500 | final RequestBody body = RequestBody.create(mediaType, formData); | ||
501 | 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", | ||
502 | "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", | ||
503 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", | ||
504 | "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", | ||
505 | "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", | ||
506 | "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", | ||
507 | "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", | ||
508 | "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build(); | ||
509 | final Response response = client.newCall(request).execute(); | ||
510 | return CollectionLiterals.<String>newArrayList(response.body().string().split("\n")); | ||
511 | } | ||
424 | } | 512 | } |
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 fcbdfde7..e32530cb 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 | |||
@@ -41,7 +41,7 @@ public class VampireHandler { | |||
41 | long startTime = (-((long) 1)); | 41 | long startTime = (-((long) 1)); |
42 | long solverTime = (-((long) 1)); | 42 | long solverTime = (-((long) 1)); |
43 | Process p = null; | 43 | Process p = null; |
44 | boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMP); | 44 | boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMPIRE); |
45 | if (_equals) { | 45 | if (_equals) { |
46 | String OPTION = " --mode casc_sat "; | 46 | String OPTION = " --mode casc_sat "; |
47 | if ((configuration.runtimeLimit != (-1))) { | 47 | if ((configuration.runtimeLimit != (-1))) { |
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 5225fb89..26ed10e3 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 | |||
@@ -26,65 +26,6 @@ import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | |||
26 | import org.eclipse.viatra.query.runtime.api.IQueryGroup | 26 | import org.eclipse.viatra.query.runtime.api.IQueryGroup |
27 | 27 | ||
28 | class GeneralTest { | 28 | class GeneralTest { |
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 | 29 | ||
89 | def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, | 30 | def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, |
90 | Ecore2Logic e2l, Ecore2Logic_Trace trace) { | 31 | Ecore2Logic e2l, Ecore2Logic_Trace trace) { |
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 c35b200e..9121367b 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 | |||
@@ -1,6 +1,7 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
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.BackendSolver | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 6 | 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.CompositeElement |
@@ -11,6 +12,8 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | |||
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry | ||
14 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | 17 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore |
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | 18 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic |
16 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | 19 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration |
@@ -32,10 +35,11 @@ class YakinduTest { | |||
32 | 35 | ||
33 | // Workspace setup | 36 | // Workspace setup |
34 | val Date date = new Date(System.currentTimeMillis) | 37 | val Date date = new Date(System.currentTimeMillis) |
35 | val SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss"); | 38 | val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm"); |
36 | val formattedDate = format.format(date) | 39 | val formattedDate = format.format(date) |
37 | 40 | ||
38 | val inputs = new FileSystemWorkspace('''initialModels/''', "") | 41 | val inputs = new FileSystemWorkspace('''initialModels/''', "") |
42 | val dataWorkspace = new FileSystemWorkspace('''output/YakinduTest/''', "") | ||
39 | val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "") | 43 | val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "") |
40 | workspace.initAndClear | 44 | workspace.initAndClear |
41 | 45 | ||
@@ -55,89 +59,120 @@ class YakinduTest { | |||
55 | // val queries = null | 59 | // val queries = null |
56 | println("DSL loaded") | 60 | println("DSL loaded") |
57 | 61 | ||
58 | var SZ_TOP = 10 | 62 | var SZ_TOP = 30 |
59 | var SZ_BOT = 126 | 63 | var SZ_BOT = 5 |
60 | var INC = 1 | 64 | var INC = 5 |
61 | var REPS = 1 | 65 | var REPS = 1 |
62 | |||
63 | val RANGE = 3 | ||
64 | 66 | ||
65 | val EXACT = 10 | 67 | val RUNTIME = 20 |
68 | |||
69 | val EXACT = -1 | ||
66 | if (EXACT != -1) { | 70 | if (EXACT != -1) { |
67 | SZ_TOP = EXACT | 71 | SZ_TOP = EXACT |
68 | SZ_BOT = EXACT | 72 | SZ_BOT = EXACT |
69 | INC = 1 | 73 | INC = 1 |
70 | REPS = 1 | 74 | REPS = 10 |
71 | } | 75 | } |
76 | val BACKENDSOLVERS = newArrayList( | ||
77 | // BackendSolver::CVC4 | ||
78 | // , | ||
79 | // BackendSolver::DARWINFM | ||
80 | // , | ||
81 | // BackendSolver::EDARWIN | ||
82 | // , | ||
83 | // BackendSolver::GEOIII | ||
84 | // , | ||
85 | BackendSolver::IPROVER | ||
86 | // , | ||
87 | // BackendSolver::PARADOX | ||
88 | // , | ||
89 | // BackendSolver::VAMPIRE | ||
90 | // , | ||
91 | // BackendSolver::Z3 | ||
92 | ) | ||
93 | |||
72 | 94 | ||
73 | var writer = new PrintWriter(workspace.workspaceURI + "//_yakinduStats.csv") | 95 | var str = "" |
74 | writer.append("size,") | 96 | |
75 | for (var x = 0; x < REPS; x++) { | 97 | for (solver : BACKENDSOLVERS) { |
76 | writer.append("tTransf" + x + "," + "tSolv" + x + ",") | 98 | str += solver.name.substring(0, 1) |
77 | } | 99 | } |
78 | writer.append("medSolv,medTransf\n") | 100 | |
101 | var writer = new PrintWriter( | ||
102 | dataWorkspace.workspaceURI + "//_stats" + formattedDate + "-" + str + SZ_BOT + "to" + SZ_TOP + "by" + INC + | ||
103 | "x" + REPS + ".csv") | ||
104 | writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n") | ||
79 | var solverTimes = newArrayList | 105 | var solverTimes = newArrayList |
80 | var transformationTimes = newArrayList | 106 | var transformationTimes = newArrayList |
81 | var modelFound = true | ||
82 | var LogicResult solution = null | 107 | var LogicResult solution = null |
83 | for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { | ||
84 | val num = (i - SZ_BOT) / INC | ||
85 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") | ||
86 | writer.append(i + ",") | ||
87 | solverTimes.clear | ||
88 | transformationTimes.clear | ||
89 | modelFound = true | ||
90 | for (var j = 0; j < REPS; j++) { | ||
91 | 108 | ||
92 | print(j) | 109 | for (BESOLVER : BACKENDSOLVERS) { |
93 | 110 | ||
94 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) | 111 | for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { |
95 | var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel) | 112 | val num = (i - SZ_BOT) / INC |
96 | var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, | 113 | println() |
97 | new Viatra2LogicConfiguration) | 114 | println("SOLVER: " + BESOLVER.name + ", SIZE=" + i) |
115 | println() | ||
98 | 116 | ||
99 | var problem = modelGenerationProblem.output | 117 | solverTimes.clear |
100 | workspace.writeModel(problem, "Yakindu.logicproblem") | 118 | transformationTimes.clear |
119 | for (var j = 0; j < REPS; j++) { | ||
101 | 120 | ||
121 | print("<<Run number " + j + ">> :") | ||
122 | |||
123 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, | ||
124 | new Ecore2LogicConfiguration()) | ||
125 | var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel) | ||
126 | var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, | ||
127 | new Viatra2LogicConfiguration) | ||
128 | |||
129 | var problem = modelGenerationProblem.output | ||
130 | // workspace.writeModel(problem, "Yakindu.logicproblem") | ||
102 | // println("Problem created") | 131 | // println("Problem created") |
103 | // Start Time | 132 | // Start Time |
104 | var startTime = System.currentTimeMillis | 133 | var startTime = System.currentTimeMillis |
105 | 134 | ||
106 | var VampireSolver reasoner | 135 | var VampireSolver reasoner |
107 | // * | 136 | // * |
108 | reasoner = new VampireSolver | 137 | reasoner = new VampireSolver |
109 | 138 | ||
110 | // ///////////////////////////////////////////////////// | 139 | // ///////////////////////////////////////////////////// |
111 | // Minimum Scope | 140 | // Minimum Scope |
112 | val classMapMin = new HashMap<Class, Integer> | 141 | val classMapMin = new HashMap<Class, Integer> |
113 | classMapMin.put(Region, 1) | 142 | classMapMin.put(Region, 1) |
114 | classMapMin.put(Transition, 2) | 143 | classMapMin.put(Transition, 2) |
115 | classMapMin.put(CompositeElement, 3) | 144 | classMapMin.put(CompositeElement, 3) |
116 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) | 145 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, |
117 | // Maximum Scope | 146 | modelGenerationProblem.trace) |
118 | val classMapMax = new HashMap<Class, Integer> | 147 | // Maximum Scope |
119 | classMapMax.put(Region, 5) | 148 | val classMapMax = new HashMap<Class, Integer> |
120 | classMapMax.put(Transition, 2) | 149 | classMapMax.put(Region, 5) |
121 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | 150 | classMapMax.put(Transition, 2) |
122 | // Define Config File | 151 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, |
123 | val size = i | 152 | modelGenerationProblem.trace) |
124 | val inc = INC | 153 | // Define Config File |
125 | val iter = j | 154 | val size = i |
126 | val vampireConfig = new VampireSolverConfiguration => [ | 155 | val inc = INC |
127 | // add configuration things, in config file first | 156 | val iter = j |
128 | it.documentationLevel = DocumentationLevel::FULL | 157 | val vampireConfig = new VampireSolverConfiguration => [ |
129 | it.iteration = iter | 158 | // add configuration things, in config file first |
130 | it.runtimeLimit = 60 | 159 | it.documentationLevel = DocumentationLevel::FULL |
131 | it.typeScopes.maxNewElements = -1 | 160 | it.iteration = iter |
132 | it.typeScopes.minNewElements = size | 161 | it.runtimeLimit = RUNTIME |
133 | it.genModel = false | 162 | // it.typeScopes.maxNewElements = size |
134 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 163 | it.typeScopes.minNewElements = size |
135 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 164 | |
136 | it.contCycleLevel = 5 | 165 | it.genModel = true |
137 | it.uniquenessDuplicates = false | 166 | it.server = true |
138 | ] | 167 | it.solver = BESOLVER |
139 | 168 | ||
140 | solution = reasoner.solve(problem, vampireConfig, workspace) | 169 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
170 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | ||
171 | it.contCycleLevel = 5 | ||
172 | it.uniquenessDuplicates = false | ||
173 | ] | ||
174 | |||
175 | solution = reasoner.solve(problem, vampireConfig, workspace) | ||
141 | // print((solution as ModelResult).representation.get(0)) | 176 | // print((solution as ModelResult).representation.get(0)) |
142 | // val soln = ((solution as ModelResult).representation.get(0) as VampireModel) | 177 | // val soln = ((solution as ModelResult).representation.get(0) as VampireModel) |
143 | // println(soln.confirmations) | 178 | // println(soln.confirmations) |
@@ -145,20 +180,35 @@ class YakinduTest { | |||
145 | // modelFound = !soln.confirmations.filter [ | 180 | // modelFound = !soln.confirmations.filter [ |
146 | // class == VLSFiniteModelImpl | 181 | // class == VLSFiniteModelImpl |
147 | // ].isEmpty | 182 | // ].isEmpty |
148 | // | 183 | // ADD TO CSV |
149 | // if (modelFound) { | 184 | writer.append(vampireConfig.solver.name + ",") |
150 | val tTime = solution.statistics.transformationTime / 1000.0 | 185 | writer.append(size + ",") |
151 | val sTime = solution.statistics.solverTime / 1000.0 | 186 | writer.append(solution.statistics.transformationTime / 1000.0 + ",") |
152 | writer.append(tTime + "," + sTime + ",") | 187 | |
153 | print("(" + tTime + "/" + sTime + "s)..") | 188 | val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry). |
154 | solverTimes.add(sTime) | 189 | value |
155 | transformationTimes.add(tTime) | 190 | val satTime = (solution.statistics.entries.filter[name == "satTime"].get(0) as RealStatisticEntry). |
191 | value | ||
192 | val modOut = (solution.statistics.entries.filter[name == "modOut"].get(0) as StringStatisticEntry). | ||
193 | value | ||
194 | val modTime = (solution.statistics.entries.filter[name == "modTime"].get(0) as RealStatisticEntry). | ||
195 | value | ||
196 | |||
197 | writer.append(satOut + ",") | ||
198 | writer.append(satTime + ",") | ||
199 | writer.append(modOut + ",") | ||
200 | writer.append(modTime + ",") | ||
201 | writer.append("\n") | ||
202 | |||
203 | // print("(" + tTime + "/" + sTime + "s)..") | ||
204 | // solverTimes.add(sTime) | ||
205 | // transformationTimes.add(tTime) | ||
156 | // } else { | 206 | // } else { |
157 | // writer.append("MNF" + ",") | 207 | // writer.append("MNF" + ",") |
158 | //// print("MNF") | 208 | //// print("MNF") |
159 | // } | 209 | // } |
160 | // println("Problem solved") | 210 | // println("Problem solved") |
161 | // visualisation, see | 211 | // visualisation, see |
162 | // var interpretations = reasoner.getInterpretations(solution as ModelResult) | 212 | // var interpretations = reasoner.getInterpretations(solution as ModelResult) |
163 | // for (interpretation : interpretations) { | 213 | // for (interpretation : interpretations) { |
164 | // val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) | 214 | // val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) |
@@ -168,15 +218,15 @@ class YakinduTest { | |||
168 | // var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 | 218 | // var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 |
169 | // println("Problem solved") | 219 | // println("Problem solved") |
170 | // println("Time was: " + totalTimeMin + ":" + totalTimeSec) | 220 | // println("Time was: " + totalTimeMin + ":" + totalTimeSec) |
221 | } | ||
222 | // println() | ||
223 | // var solverMed = solverTimes.sort.get(REPS / 2) | ||
224 | // var transformationMed = transformationTimes.sort.get(REPS / 2) | ||
225 | // writer.append(solverMed.toString + "," + transformationMed.toString) | ||
171 | } | 226 | } |
172 | println() | 227 | |
173 | var solverMed = solverTimes.sort.get(REPS / 2) | ||
174 | var transformationMed = transformationTimes.sort.get(REPS / 2) | ||
175 | writer.append(solverMed.toString + "," + transformationMed.toString) | ||
176 | writer.append("\n") | ||
177 | } | 228 | } |
178 | writer.close | 229 | writer.close |
179 | |||
180 | } | 230 | } |
181 | 231 | ||
182 | } | 232 | } |
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 93d27b4d..5dc01040 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 bc2bae6f..e96cf904 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 5687258f..688908b9 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 de68a908..0d18615c 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 16a3cd03..cf52d6a6 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/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java index ce057092..bdea5746 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,11 +13,6 @@ 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; | ||
21 | import org.eclipse.emf.common.util.EList; | 16 | import org.eclipse.emf.common.util.EList; |
22 | import org.eclipse.emf.ecore.EAttribute; | 17 | import org.eclipse.emf.ecore.EAttribute; |
23 | import org.eclipse.emf.ecore.EClass; | 18 | import org.eclipse.emf.ecore.EClass; |
@@ -33,75 +28,12 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup; | |||
33 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; | 28 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; |
34 | import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; | 29 | import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; |
35 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 30 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
36 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
37 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
38 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
39 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | 32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; |
40 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 33 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
41 | 34 | ||
42 | @SuppressWarnings("all") | 35 | @SuppressWarnings("all") |
43 | public class GeneralTest { | 36 | 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 | |||
105 | public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { | 37 | public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { |
106 | final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>(); | 38 | final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>(); |
107 | final Function1<EClass, String> _function = (EClass s) -> { | 39 | final Function1<EClass, String> _function = (EClass s) -> { |
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 3a8f3fb4..1837b768 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 | |||
@@ -2,12 +2,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; | |||
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; | 3 | 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.BackendSolver; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 7 | 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.CompositeElement; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region; | 9 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region; |
9 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition; |
10 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; | 11 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; |
12 | import com.google.common.base.Objects; | ||
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; | 13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; |
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; | 14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; |
13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; | 15 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; |
@@ -17,6 +19,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | |||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | 25 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; |
21 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; | 26 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; |
22 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; | 27 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; |
@@ -37,7 +42,9 @@ import org.eclipse.emf.ecore.resource.Resource; | |||
37 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; | 42 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; |
38 | import org.eclipse.xtend2.lib.StringConcatenation; | 43 | import org.eclipse.xtend2.lib.StringConcatenation; |
39 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 44 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
45 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
40 | import org.eclipse.xtext.xbase.lib.Exceptions; | 46 | import org.eclipse.xtext.xbase.lib.Exceptions; |
47 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
41 | import org.eclipse.xtext.xbase.lib.InputOutput; | 48 | import org.eclipse.xtext.xbase.lib.InputOutput; |
42 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | 49 | import org.eclipse.xtext.xbase.lib.IterableExtensions; |
43 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 50 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
@@ -53,17 +60,20 @@ public class YakinduTest { | |||
53 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); | 60 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); |
54 | long _currentTimeMillis = System.currentTimeMillis(); | 61 | long _currentTimeMillis = System.currentTimeMillis(); |
55 | final Date date = new Date(_currentTimeMillis); | 62 | final Date date = new Date(_currentTimeMillis); |
56 | final SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss"); | 63 | final SimpleDateFormat format = new SimpleDateFormat("dd-HHmm"); |
57 | final String formattedDate = format.format(date); | 64 | final String formattedDate = format.format(date); |
58 | StringConcatenation _builder = new StringConcatenation(); | 65 | StringConcatenation _builder = new StringConcatenation(); |
59 | _builder.append("initialModels/"); | 66 | _builder.append("initialModels/"); |
60 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); | 67 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); |
61 | StringConcatenation _builder_1 = new StringConcatenation(); | 68 | StringConcatenation _builder_1 = new StringConcatenation(); |
62 | _builder_1.append("output/YakinduTest/"); | 69 | _builder_1.append("output/YakinduTest/"); |
63 | String _plus = (_builder_1.toString() + formattedDate); | 70 | final FileSystemWorkspace dataWorkspace = new FileSystemWorkspace(_builder_1.toString(), ""); |
64 | StringConcatenation _builder_2 = new StringConcatenation(); | 71 | StringConcatenation _builder_2 = new StringConcatenation(); |
65 | _builder_2.append("/"); | 72 | _builder_2.append("output/YakinduTest/"); |
66 | String _plus_1 = (_plus + _builder_2); | 73 | String _plus = (_builder_2.toString() + formattedDate); |
74 | StringConcatenation _builder_3 = new StringConcatenation(); | ||
75 | _builder_3.append("/"); | ||
76 | String _plus_1 = (_plus + _builder_3); | ||
67 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, ""); | 77 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, ""); |
68 | workspace.initAndClear(); | 78 | workspace.initAndClear(); |
69 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; | 79 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; |
@@ -75,117 +85,149 @@ public class YakinduTest { | |||
75 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); | 85 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); |
76 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); | 86 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); |
77 | InputOutput.<String>println("DSL loaded"); | 87 | InputOutput.<String>println("DSL loaded"); |
78 | int SZ_TOP = 10; | 88 | int SZ_TOP = 30; |
79 | int SZ_BOT = 126; | 89 | int SZ_BOT = 5; |
80 | int INC = 1; | 90 | int INC = 5; |
81 | int REPS = 1; | 91 | int REPS = 1; |
82 | final int RANGE = 3; | 92 | final int RUNTIME = 20; |
83 | final int EXACT = 10; | 93 | final int EXACT = (-1); |
84 | if ((EXACT != (-1))) { | 94 | if ((EXACT != (-1))) { |
85 | SZ_TOP = EXACT; | 95 | SZ_TOP = EXACT; |
86 | SZ_BOT = EXACT; | 96 | SZ_BOT = EXACT; |
87 | INC = 1; | 97 | INC = 1; |
88 | REPS = 1; | 98 | REPS = 10; |
89 | } | 99 | } |
90 | URI _workspaceURI = workspace.getWorkspaceURI(); | 100 | final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList( |
91 | String _plus_2 = (_workspaceURI + "//_yakinduStats.csv"); | 101 | BackendSolver.IPROVER); |
92 | PrintWriter writer = new PrintWriter(_plus_2); | 102 | String str = ""; |
93 | writer.append("size,"); | 103 | for (final BackendSolver solver : BACKENDSOLVERS) { |
94 | for (int x = 0; (x < REPS); x++) { | 104 | String _str = str; |
95 | writer.append(((((("tTransf" + Integer.valueOf(x)) + ",") + "tSolv") + Integer.valueOf(x)) + ",")); | 105 | String _substring = solver.name().substring(0, 1); |
106 | str = (_str + _substring); | ||
96 | } | 107 | } |
97 | writer.append("medSolv,medTransf\n"); | 108 | URI _workspaceURI = dataWorkspace.getWorkspaceURI(); |
98 | ArrayList<Double> solverTimes = CollectionLiterals.<Double>newArrayList(); | 109 | String _plus_2 = (_workspaceURI + "//_stats"); |
99 | ArrayList<Double> transformationTimes = CollectionLiterals.<Double>newArrayList(); | 110 | String _plus_3 = (_plus_2 + formattedDate); |
100 | boolean modelFound = true; | 111 | String _plus_4 = (_plus_3 + "-"); |
112 | String _plus_5 = (_plus_4 + str); | ||
113 | String _plus_6 = (_plus_5 + Integer.valueOf(SZ_BOT)); | ||
114 | String _plus_7 = (_plus_6 + "to"); | ||
115 | String _plus_8 = (_plus_7 + Integer.valueOf(SZ_TOP)); | ||
116 | String _plus_9 = (_plus_8 + "by"); | ||
117 | String _plus_10 = (_plus_9 + Integer.valueOf(INC)); | ||
118 | String _plus_11 = (_plus_10 + | ||
119 | "x"); | ||
120 | String _plus_12 = (_plus_11 + Integer.valueOf(REPS)); | ||
121 | String _plus_13 = (_plus_12 + ".csv"); | ||
122 | PrintWriter writer = new PrintWriter(_plus_13); | ||
123 | writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n"); | ||
124 | ArrayList<Object> solverTimes = CollectionLiterals.<Object>newArrayList(); | ||
125 | ArrayList<Object> transformationTimes = CollectionLiterals.<Object>newArrayList(); | ||
101 | LogicResult solution = null; | 126 | LogicResult solution = null; |
102 | { | 127 | for (final BackendSolver BESOLVER : BACKENDSOLVERS) { |
103 | int i = SZ_BOT; | 128 | { |
104 | boolean _while = (i <= SZ_TOP); | 129 | int i = SZ_BOT; |
105 | while (_while) { | 130 | boolean _while = (i <= SZ_TOP); |
106 | { | 131 | while (_while) { |
107 | final int num = ((i - SZ_BOT) / INC); | 132 | { |
108 | InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); | 133 | final int num = ((i - SZ_BOT) / INC); |
109 | String _plus_3 = (Integer.valueOf(i) + ","); | 134 | InputOutput.println(); |
110 | writer.append(_plus_3); | 135 | String _name = BESOLVER.name(); |
111 | solverTimes.clear(); | 136 | String _plus_14 = ("SOLVER: " + _name); |
112 | transformationTimes.clear(); | 137 | String _plus_15 = (_plus_14 + ", SIZE="); |
113 | modelFound = true; | 138 | String _plus_16 = (_plus_15 + Integer.valueOf(i)); |
114 | for (int j = 0; (j < REPS); j++) { | 139 | InputOutput.<String>println(_plus_16); |
115 | { | 140 | InputOutput.println(); |
116 | InputOutput.<Integer>print(Integer.valueOf(j)); | 141 | solverTimes.clear(); |
117 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); | 142 | transformationTimes.clear(); |
118 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); | 143 | for (int j = 0; (j < REPS); j++) { |
119 | TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); | 144 | { |
120 | Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); | 145 | InputOutput.<String>print((("<<Run number " + Integer.valueOf(j)) + ">> :")); |
121 | TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration); | 146 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); |
122 | LogicProblem problem = modelGenerationProblem.getOutput(); | 147 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); |
123 | workspace.writeModel(problem, "Yakindu.logicproblem"); | 148 | TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); |
124 | long startTime = System.currentTimeMillis(); | 149 | Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); |
125 | VampireSolver reasoner = null; | 150 | TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration); |
126 | VampireSolver _vampireSolver = new VampireSolver(); | 151 | LogicProblem problem = modelGenerationProblem.getOutput(); |
127 | reasoner = _vampireSolver; | 152 | long startTime = System.currentTimeMillis(); |
128 | final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); | 153 | VampireSolver reasoner = null; |
129 | classMapMin.put(Region.class, Integer.valueOf(1)); | 154 | VampireSolver _vampireSolver = new VampireSolver(); |
130 | classMapMin.put(Transition.class, Integer.valueOf(2)); | 155 | reasoner = _vampireSolver; |
131 | classMapMin.put(CompositeElement.class, Integer.valueOf(3)); | 156 | final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); |
132 | final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); | 157 | classMapMin.put(Region.class, Integer.valueOf(1)); |
133 | final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); | 158 | classMapMin.put(Transition.class, Integer.valueOf(2)); |
134 | classMapMax.put(Region.class, Integer.valueOf(5)); | 159 | classMapMin.put(CompositeElement.class, Integer.valueOf(3)); |
135 | classMapMax.put(Transition.class, Integer.valueOf(2)); | 160 | final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, |
136 | final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); | 161 | modelGenerationProblem.getTrace()); |
137 | final int size = i; | 162 | final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); |
138 | final int inc = INC; | 163 | classMapMax.put(Region.class, Integer.valueOf(5)); |
139 | final int iter = j; | 164 | classMapMax.put(Transition.class, Integer.valueOf(2)); |
140 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); | 165 | final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, |
141 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { | 166 | modelGenerationProblem.getTrace()); |
142 | it.documentationLevel = DocumentationLevel.FULL; | 167 | final int size = i; |
143 | it.iteration = iter; | 168 | final int inc = INC; |
144 | it.runtimeLimit = 60; | 169 | final int iter = j; |
145 | it.typeScopes.maxNewElements = (-1); | 170 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); |
146 | it.typeScopes.minNewElements = size; | 171 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { |
147 | it.genModel = false; | 172 | it.documentationLevel = DocumentationLevel.FULL; |
148 | int _size = typeMapMin.size(); | 173 | it.iteration = iter; |
149 | boolean _notEquals = (_size != 0); | 174 | it.runtimeLimit = RUNTIME; |
150 | if (_notEquals) { | 175 | it.typeScopes.minNewElements = size; |
151 | it.typeScopes.minNewElementsByType = typeMapMin; | 176 | it.genModel = true; |
152 | } | 177 | it.server = true; |
153 | int _size_1 = typeMapMin.size(); | 178 | it.solver = BESOLVER; |
154 | boolean _notEquals_1 = (_size_1 != 0); | 179 | it.contCycleLevel = 5; |
155 | if (_notEquals_1) { | 180 | it.uniquenessDuplicates = false; |
156 | it.typeScopes.maxNewElementsByType = typeMapMax; | 181 | }; |
157 | } | 182 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); |
158 | it.contCycleLevel = 5; | 183 | solution = reasoner.solve(problem, vampireConfig, workspace); |
159 | it.uniquenessDuplicates = false; | 184 | String _name_1 = vampireConfig.solver.name(); |
160 | }; | 185 | String _plus_17 = (_name_1 + ","); |
161 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | 186 | writer.append(_plus_17); |
162 | solution = reasoner.solve(problem, vampireConfig, workspace); | 187 | String _plus_18 = (Integer.valueOf(size) + ","); |
163 | int _transformationTime = solution.getStatistics().getTransformationTime(); | 188 | writer.append(_plus_18); |
164 | final double tTime = (_transformationTime / 1000.0); | 189 | int _transformationTime = solution.getStatistics().getTransformationTime(); |
165 | int _solverTime = solution.getStatistics().getSolverTime(); | 190 | double _divide = (_transformationTime / 1000.0); |
166 | final double sTime = (_solverTime / 1000.0); | 191 | String _plus_19 = (Double.valueOf(_divide) + ","); |
167 | String _plus_4 = (Double.valueOf(tTime) + ","); | 192 | writer.append(_plus_19); |
168 | String _plus_5 = (_plus_4 + Double.valueOf(sTime)); | 193 | final Function1<StatisticEntry, Boolean> _function_1 = (StatisticEntry it) -> { |
169 | String _plus_6 = (_plus_5 + ","); | 194 | String _name_2 = it.getName(); |
170 | writer.append(_plus_6); | 195 | return Boolean.valueOf(Objects.equal(_name_2, "satOut")); |
171 | InputOutput.<String>print((((("(" + Double.valueOf(tTime)) + "/") + Double.valueOf(sTime)) + "s)..")); | 196 | }; |
172 | solverTimes.add(Double.valueOf(sTime)); | 197 | StatisticEntry _get = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_1), StatisticEntry.class))[0]; |
173 | transformationTimes.add(Double.valueOf(tTime)); | 198 | final String satOut = ((StringStatisticEntry) _get).getValue(); |
199 | final Function1<StatisticEntry, Boolean> _function_2 = (StatisticEntry it) -> { | ||
200 | String _name_2 = it.getName(); | ||
201 | return Boolean.valueOf(Objects.equal(_name_2, "satTime")); | ||
202 | }; | ||
203 | StatisticEntry _get_1 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_2), StatisticEntry.class))[0]; | ||
204 | final double satTime = ((RealStatisticEntry) _get_1).getValue(); | ||
205 | final Function1<StatisticEntry, Boolean> _function_3 = (StatisticEntry it) -> { | ||
206 | String _name_2 = it.getName(); | ||
207 | return Boolean.valueOf(Objects.equal(_name_2, "modOut")); | ||
208 | }; | ||
209 | StatisticEntry _get_2 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_3), StatisticEntry.class))[0]; | ||
210 | final String modOut = ((StringStatisticEntry) _get_2).getValue(); | ||
211 | final Function1<StatisticEntry, Boolean> _function_4 = (StatisticEntry it) -> { | ||
212 | String _name_2 = it.getName(); | ||
213 | return Boolean.valueOf(Objects.equal(_name_2, "modTime")); | ||
214 | }; | ||
215 | StatisticEntry _get_3 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_4), StatisticEntry.class))[0]; | ||
216 | final double modTime = ((RealStatisticEntry) _get_3).getValue(); | ||
217 | writer.append((satOut + ",")); | ||
218 | String _plus_20 = (Double.valueOf(satTime) + ","); | ||
219 | writer.append(_plus_20); | ||
220 | writer.append((modOut + ",")); | ||
221 | String _plus_21 = (Double.valueOf(modTime) + ","); | ||
222 | writer.append(_plus_21); | ||
223 | writer.append("\n"); | ||
224 | } | ||
174 | } | 225 | } |
175 | } | 226 | } |
176 | InputOutput.println(); | 227 | int _i = i; |
177 | Double solverMed = IterableExtensions.<Double>sort(solverTimes).get((REPS / 2)); | 228 | i = (_i + INC); |
178 | Double transformationMed = IterableExtensions.<Double>sort(transformationTimes).get((REPS / 2)); | 229 | _while = (i <= SZ_TOP); |
179 | String _string = solverMed.toString(); | ||
180 | String _plus_4 = (_string + ","); | ||
181 | String _string_1 = transformationMed.toString(); | ||
182 | String _plus_5 = (_plus_4 + _string_1); | ||
183 | writer.append(_plus_5); | ||
184 | writer.append("\n"); | ||
185 | } | 230 | } |
186 | int _i = i; | ||
187 | i = (_i + INC); | ||
188 | _while = (i <= SZ_TOP); | ||
189 | } | 231 | } |
190 | } | 232 | } |
191 | writer.close(); | 233 | 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 96f343fa..b596dc1f 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 1ca8223d..e1434d74 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 5d6a9ee2..50068d97 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 | |||