From 17d6aa5028bff14c80f0be6a042c6a68fe8b61b0 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 11 Oct 2019 15:51:49 -0400 Subject: VAMPIRE: complete testing setup --- .../ide/.VampireLanguageIdeModule.xtendbin | Bin 1685 -> 1685 bytes .../ide/.VampireLanguageIdeSetup.xtendbin | Bin 2500 -> 2500 bytes .../ui/.VampireLanguageUiModule.xtendbin | Bin 2342 -> 2342 bytes .../.VampireLanguageProposalProvider.xtendbin | Bin 1792 -> 1792 bytes ...ampireLanguageDescriptionLabelProvider.xtendbin | Bin 1965 -> 1965 bytes .../.VampireLanguageLabelProvider.xtendbin | Bin 2405 -> 2405 bytes .../.VampireLanguageOutlineTreeProvider.xtendbin | Bin 1819 -> 1819 bytes .../.VampireLanguageQuickfixProvider.xtendbin | Bin 1786 -> 1786 bytes .../.VampireLanguageRuntimeModule.xtendbin | Bin 1706 -> 1706 bytes .../.VampireLanguageStandaloneSetup.xtendbin | Bin 1980 -> 1980 bytes .../formatting2/.VampireLanguageFormatter.xtendbin | Bin 3759 -> 3759 bytes .../generator/.VampireLanguageGenerator.xtendbin | Bin 2338 -> 2338 bytes .../scoping/.VampireLanguageScopeProvider.xtendbin | Bin 1751 -> 1751 bytes .../validation/.VampireLanguageValidator.xtendbin | Bin 1736 -> 1736 bytes .../.classpath | 6 + .../reasoner/VampireAnalyzerConfiguration.xtend | 16 +- .../vampire/reasoner/VampireSolver.xtend | 116 ++++++++-- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 6 +- .../Logic2VampireLanguageMapper_Support.xtend | 95 +++++++- .../vampire/reasoner/builder/VampireHandler.xtend | 2 +- .../.VampireAnalyzerConfiguration.xtendbin | Bin 3161 -> 3418 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 6885 -> 10151 bytes .../vampire/reasoner/VampireSolver.java | 175 ++++++++++++--- .../reasoner/VampireSolverConfiguration.java | 4 +- .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 19565 -> 19566 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 5080 -> 5080 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11807 -> 11807 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 7880 -> 7880 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10660 -> 10682 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13060 -> 17151 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11037 -> 11037 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3997 -> 3997 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 7803 -> 7804 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../Logic2VampireLanguageMapper_ScopeMapper.java | 6 +- .../Logic2VampireLanguageMapper_Support.java | 88 ++++++++ .../vampire/reasoner/builder/VampireHandler.java | 2 +- .../dslreasoner/vampire/icse/GeneralTest.xtend | 59 ----- .../dslreasoner/vampire/icse/YakinduTest.xtend | 214 +++++++++++------- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 4552 -> 4545 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 6632 -> 6626 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 6207 -> 6201 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 10182 -> 6625 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 8484 -> 8992 bytes .../ecse/dslreasoner/vampire/icse/GeneralTest.java | 68 ------ .../ecse/dslreasoner/vampire/icse/YakinduTest.java | 250 ++++++++++++--------- .../vampire/test/.MedicalSystem.xtendbin | Bin 4997 -> 4997 bytes .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 687 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6500 -> 6500 bytes 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin 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 @@ + + + + + + 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 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration -class VampireSolverConfiguration extends LogicSolverConfiguration { +class VampireSolverConfiguration + extends LogicSolverConfiguration { public var int contCycleLevel = 0 public var boolean uniquenessDuplicates = false public var int iteration = -1 - public var BackendSolver solver = BackendSolver::VAMP + public var BackendSolver solver = BackendSolver::VAMPIRE public var genModel = true + public var server = false //choose needed backend solver // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J } enum BackendSolver { - VAMP, - CVC4 + CVC4, + DARWINFM, + EDARWIN, + GEOIII, + IPROVER, + PARADOX, + VAMPIRE, + Z3 //add needed things } 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 import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel -import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace @@ -30,18 +32,20 @@ class VampireSolver extends LogicReasoner { val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper val VampireHandler handler = new VampireHandler + val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE // var fileName = "problem.tptp" - // def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { // fileName = location + fileName // solve(problem, config, workspace) // } - override solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace) throws LogicReasonerException { val vampireConfig = config.asConfig - var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + vampireConfig.typeScopes.maxNewElements + ".tptp" + var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + + vampireConfig.typeScopes.maxNewElements + ".tptp" // Start: Logic -> Vampire mapping val transformationStart = System.currentTimeMillis @@ -55,8 +59,6 @@ class VampireSolver extends LogicReasoner { var String fileURI = null; var String vampireCode = null; vampireCode = workspace.writeModelToString(vampireProblem, fileName) - - val writeFile = ( vampireConfig.documentationLevel === DocumentationLevel::NORMAL || @@ -73,24 +75,94 @@ class VampireSolver extends LogicReasoner { // println(model) // Finish: Logic -> Vampire mapping if (vampireConfig.genModel) { - - // Start: Solving .tptp problem - val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) - // Finish: Solving .tptp problem - // Start: Vampire -> Logic mapping - val backTransformationStart = System.currentTimeMillis - // Backwards Mapper - val logicResult = backwardMapper.transformOutput(problem, - vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) - - val backTransformationTime = System.currentTimeMillis - backTransformationStart - // Finish: Vampire -> Logic Mapping + if (vampireConfig.server) { + val form = support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit) + var response = newArrayList + var ind = 0 + var done = false + print(" ") + while (!done) { + print("(x)") + done = false + response = support.sendPost(form) + + var responseFound = false + ind = 0 + while (!responseFound) { + var line = response.get(ind) + if (line.length >= 5 && line.substring(0, 5) == "ERROR") { + done = false + responseFound = true + } else { + if (line == "") { + done = true + responseFound = true + } + } + ind++ + } + } + val satRaw = response.get(ind - 3) + val modRaw = response.get(ind - 2) + + val sat = newArrayList(satRaw.split(" ")) + val mod = newArrayList(modRaw.split(" ")) + + val satOut = sat.get(1) + val modOut = mod.get(1) + val satTime = sat.get(2) + val modTime = mod.get(2) + + println() + println(sat) + println(mod) + + return createModelResult => [ + it.problem = null + it.representation += createVampireModel => [] + it.trace = trace + it.statistics = createStatistics => [ + it.transformationTime = transformationTime as int + it.entries += createStringStatisticEntry => [ + it.name = "satOut" + it.value = satOut + ] + it.entries += createRealStatisticEntry => [ + it.name = "satTime" + it.value = Double.parseDouble(satTime) + ] + it.entries += createStringStatisticEntry => [ + it.name = "modOut" + it.value = modOut + ] + it.entries += createRealStatisticEntry => [ + it.name = "modTime" + it.value = Double.parseDouble(modTime) + ] + + ] + ] + +// return newArrayList(line1, line2) + } else { + + // Start: Solving .tptp problem + val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) + // Finish: Solving .tptp problem + // Start: Vampire -> Logic mapping + val backTransformationStart = System.currentTimeMillis + // Backwards Mapper + val logicResult = backwardMapper.transformOutput(problem, + vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime) + + val backTransformationTime = System.currentTimeMillis - backTransformationStart + // Finish: Vampire -> Logic Mapping // print(vampSol.generatedModel.tfformulas.size) - return logicResult // currently only a ModelResult + return logicResult // currently only a ModelResult + } } - - return backwardMapper.transformOutput(problem, - vampireConfig.solutionScope.numberOfRequiredSolution, new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) + return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, + new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime) } 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 { // Equals the number of elements in te initial model var elemsInIM = trace.definedElement2String.size val ABSOLUTE_MIN = 0 - val ABSOLUTE_MAX = -1-elemsInIM + val ABSOLUTE_MAX = Integer.MAX_VALUE-elemsInIM // var elemsInIM = 0 // // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { @@ -60,7 +60,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { // Handling Minimum_General if (GLOBAL_MIN != ABSOLUTE_MIN) { - getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant) + getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant)//may make not consistent here if (consistant) { for (i : trace.uniqueInstances) { localInstances.add(support.duplicate(i)) @@ -73,7 +73,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { // Handling Maximum_General if (GLOBAL_MAX != ABSOLUTE_MAX) { - getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant) + getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, !consistant) if (consistant) { makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) } 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 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm @@ -16,6 +17,12 @@ import java.util.ArrayList import java.util.HashMap import java.util.List import java.util.Map +import java.util.concurrent.TimeUnit +import okhttp3.MediaType +import okhttp3.OkHttpClient +import okhttp3.Request +import okhttp3.RequestBody +import okhttp3.Response import org.eclipse.emf.common.util.EList import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* @@ -77,13 +84,13 @@ class Logic2VampireLanguageMapper_Support { it.terms += duplicate(v) ] } - + def protected List duplicate(List vars) { - var newList = newArrayList - for (v : vars) { - newList.add(duplicate(v)) - } - return newList + var newList = newArrayList + for (v : vars) { + newList.add(duplicate(v)) + } + return newList } def protected VLSConstant toConstant(VLSFunctionAsTerm term) { @@ -117,7 +124,7 @@ class Logic2VampireLanguageMapper_Support { // TODO Make more general def establishUniqueness(List terms, VLSConstant t2) { - + // OLD // val List eqs = newArrayList // for (t1 : terms.subList(1, terms.length)) { @@ -133,7 +140,6 @@ class Logic2VampireLanguageMapper_Support { // } // return unfoldAnd(eqs) // END OLD - val List eqs = newArrayList for (t1 : terms) { if (t1 != t2) { @@ -257,7 +263,8 @@ class Logic2VampireLanguageMapper_Support { } } } - //TODO rewrite such that it uses "listSubTypes" + + // TODO rewrite such that it uses "listSubTypes" def protected boolean dfsSubtypeCheck(Type type, Type type2) { // There is surely a better way to do this if (type.subtypes.isEmpty) @@ -284,4 +291,74 @@ class Logic2VampireLanguageMapper_Support { new HashMap(map1) => [putAll(map2)] } + // SERVERS + def makeForm(String formula, BackendSolver solver, int time) { + return header + formula + addOptions + addSolver(solver, time) + addEnd + } + + def getSolverSpecs(BackendSolver solver) { + switch (solver) { + case BackendSolver::CVC4: return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT") + case BackendSolver::DARWINFM: return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s") + case BackendSolver::EDARWIN: return newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s") + case BackendSolver::GEOIII: return newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s") + case BackendSolver::IPROVER: return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s") + case BackendSolver::PARADOX: return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s") + case BackendSolver::VAMPIRE: return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s") + case BackendSolver::Z3: return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s") + } + } + + def getHeader() { + 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" + } + + def addSpec(String spec) { + return spec.replace("\n", "\\r\\n") + } + + def addOptions() { + 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" + } + + def addSolver(BackendSolver solver, int time) { + val solverSpecs = getSolverSpecs(solver) + val ID = solverSpecs.get(0) + val cmd = solverSpecs.get(1) + + 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.replace("%d", time.toString) + "\r\n" + } + + def addEnd() { + return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--" + } + + def sendPost(String formData) throws Exception { + + val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build() + + val MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") + val RequestBody body = RequestBody.create(mediaType, formData) + val 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", + "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", + "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("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"). + addHeader("Accept", + "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", + "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", + "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", + "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build() + + val Response response = client.newCall(request).execute() +// TimeUnit.SECONDS.sleep(5) + return newArrayList(response.body.string.split("\n")) +// return response.body.string + // case 1: + } + } 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 { var long startTime = -1 as long var long solverTime = -1 as long var Process p = null - if (configuration.solver == BackendSolver::VAMP) { + if (configuration.solver == BackendSolver::VAMPIRE) { var OPTION = " --mode casc_sat " 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin 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; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; +import com.google.common.base.Objects; import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; @@ -19,13 +22,25 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; +import java.util.ArrayList; import java.util.List; import org.eclipse.emf.common.util.EList; import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; +import org.eclipse.xtext.xbase.lib.Exceptions; +import org.eclipse.xtext.xbase.lib.Extension; import org.eclipse.xtext.xbase.lib.Functions.Function1; +import org.eclipse.xtext.xbase.lib.InputOutput; import org.eclipse.xtext.xbase.lib.ListExtensions; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @SuppressWarnings("all") public class VampireSolver extends LogicReasoner { @@ -41,36 +56,142 @@ public class VampireSolver extends LogicReasoner { private final VampireHandler handler = new VampireHandler(); + private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); + + @Extension + private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE; + + @Extension + private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; + @Override public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { - final VampireSolverConfiguration vampireConfig = this.asConfig(config); - String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp"); - final long transformationStart = System.currentTimeMillis(); - final TracedOutput result = this.forwardMapper.transformProblem(problem, vampireConfig); - long _currentTimeMillis = System.currentTimeMillis(); - final long transformationTime = (_currentTimeMillis - transformationStart); - final VampireModel vampireProblem = result.getOutput(); - final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); - String fileURI = null; - String vampireCode = null; - vampireCode = workspace.writeModelToString(vampireProblem, fileName); - final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || - (vampireConfig.documentationLevel == DocumentationLevel.FULL)); - if (writeFile) { - fileURI = workspace.writeModel(vampireProblem, fileName).toFileString(); - } - if (vampireConfig.genModel) { - final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); - final long backTransformationStart = System.currentTimeMillis(); - final ModelResult logicResult = this.backwardMapper.transformOutput(problem, - vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); - long _currentTimeMillis_1 = System.currentTimeMillis(); - final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); - return logicResult; + try { + final VampireSolverConfiguration vampireConfig = this.asConfig(config); + String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + + Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp"); + final long transformationStart = System.currentTimeMillis(); + final TracedOutput result = this.forwardMapper.transformProblem(problem, vampireConfig); + long _currentTimeMillis = System.currentTimeMillis(); + final long transformationTime = (_currentTimeMillis - transformationStart); + final VampireModel vampireProblem = result.getOutput(); + final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); + String fileURI = null; + String vampireCode = null; + vampireCode = workspace.writeModelToString(vampireProblem, fileName); + final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || + (vampireConfig.documentationLevel == DocumentationLevel.FULL)); + if (writeFile) { + fileURI = workspace.writeModel(vampireProblem, fileName).toFileString(); + } + if (vampireConfig.genModel) { + if (vampireConfig.server) { + final String form = this.support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit); + ArrayList response = CollectionLiterals.newArrayList(); + int ind = 0; + boolean done = false; + InputOutput.print(" "); + while ((!done)) { + { + InputOutput.print("(x)"); + done = false; + response = this.support.sendPost(form); + boolean responseFound = false; + ind = 0; + while ((!responseFound)) { + { + String line = response.get(ind); + if (((line.length() >= 5) && Objects.equal(line.substring(0, 5), "ERROR"))) { + done = false; + responseFound = true; + } else { + boolean _equals = Objects.equal(line, ""); + if (_equals) { + done = true; + responseFound = true; + } + } + ind++; + } + } + } + } + final String satRaw = response.get((ind - 3)); + final String modRaw = response.get((ind - 2)); + final ArrayList sat = CollectionLiterals.newArrayList(satRaw.split(" ")); + final ArrayList mod = CollectionLiterals.newArrayList(modRaw.split(" ")); + final String satOut = sat.get(1); + final String modOut = mod.get(1); + final String satTime = sat.get(2); + final String modTime = mod.get(2); + InputOutput.println(); + InputOutput.>println(sat); + InputOutput.>println(mod); + ModelResult _createModelResult = this.resultFactory.createModelResult(); + final Procedure1 _function = (ModelResult it) -> { + it.setProblem(null); + EList _representation = it.getRepresentation(); + VampireModel _createVampireModel = this.factory.createVampireModel(); + final Procedure1 _function_1 = (VampireModel it_1) -> { + }; + VampireModel _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVampireModel, _function_1); + _representation.add(_doubleArrow); + it.setTrace(it.getTrace()); + Statistics _createStatistics = this.resultFactory.createStatistics(); + final Procedure1 _function_2 = (Statistics it_1) -> { + it_1.setTransformationTime(((int) transformationTime)); + EList _entries = it_1.getEntries(); + StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_3 = (StringStatisticEntry it_2) -> { + it_2.setName("satOut"); + it_2.setValue(satOut); + }; + StringStatisticEntry _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry, _function_3); + _entries.add(_doubleArrow_1); + EList _entries_1 = it_1.getEntries(); + RealStatisticEntry _createRealStatisticEntry = this.resultFactory.createRealStatisticEntry(); + final Procedure1 _function_4 = (RealStatisticEntry it_2) -> { + it_2.setName("satTime"); + it_2.setValue(Double.parseDouble(satTime)); + }; + RealStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createRealStatisticEntry, _function_4); + _entries_1.add(_doubleArrow_2); + EList _entries_2 = it_1.getEntries(); + StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_5 = (StringStatisticEntry it_2) -> { + it_2.setName("modOut"); + it_2.setValue(modOut); + }; + StringStatisticEntry _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_1, _function_5); + _entries_2.add(_doubleArrow_3); + EList _entries_3 = it_1.getEntries(); + RealStatisticEntry _createRealStatisticEntry_1 = this.resultFactory.createRealStatisticEntry(); + final Procedure1 _function_6 = (RealStatisticEntry it_2) -> { + it_2.setName("modTime"); + it_2.setValue(Double.parseDouble(modTime)); + }; + RealStatisticEntry _doubleArrow_4 = ObjectExtensions.operator_doubleArrow(_createRealStatisticEntry_1, _function_6); + _entries_3.add(_doubleArrow_4); + }; + Statistics _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStatistics, _function_2); + it.setStatistics(_doubleArrow_1); + }; + return ObjectExtensions.operator_doubleArrow(_createModelResult, _function); + } else { + final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); + final long backTransformationStart = System.currentTimeMillis(); + final ModelResult logicResult = this.backwardMapper.transformOutput(problem, + vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime); + long _currentTimeMillis_1 = System.currentTimeMillis(); + final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart); + return logicResult; + } + } + MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); + return this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); } - MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); - return this.backwardMapper.transformOutput(problem, - vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime); } 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 { public int iteration = (-1); - public BackendSolver solver = BackendSolver.VAMP; + public BackendSolver solver = BackendSolver.VAMPIRE; public boolean genModel = true; + + public boolean server = false; } 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin 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 { public void _transformScope(final List types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { int elemsInIM = trace.definedElement2String.size(); final int ABSOLUTE_MIN = 0; - final int ABSOLUTE_MAX = ((-1) - elemsInIM); + final int ABSOLUTE_MAX = (Integer.MAX_VALUE - elemsInIM); final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); final ArrayList localInstances = CollectionLiterals.newArrayList(); final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); if ((GLOBAL_MIN != ABSOLUTE_MIN)) { - this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant)); + this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant); if (consistant) { for (final VLSConstant i : trace.uniqueInstances) { localInstances.add(this.support.duplicate(i)); @@ -72,7 +72,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { } } if ((GLOBAL_MAX != ABSOLUTE_MAX)) { - this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant); + this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, (!consistant)); if (consistant) { this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); } 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 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; @@ -29,6 +30,12 @@ import java.util.Collection; import java.util.HashMap; import java.util.List; import java.util.Map; +import java.util.concurrent.TimeUnit; +import okhttp3.MediaType; +import okhttp3.OkHttpClient; +import okhttp3.Request; +import okhttp3.RequestBody; +import okhttp3.Response; import org.eclipse.emf.common.util.EList; import org.eclipse.xtend2.lib.StringConcatenation; import org.eclipse.xtext.xbase.lib.CollectionLiterals; @@ -421,4 +428,85 @@ public class Logic2VampireLanguageMapper_Support { }; return ObjectExtensions.>operator_doubleArrow(_hashMap, _function); } + + public String makeForm(final String formula, final BackendSolver solver, final int time) { + String _header = this.getHeader(); + String _plus = (_header + formula); + String _addOptions = this.addOptions(); + String _plus_1 = (_plus + _addOptions); + String _addSolver = this.addSolver(solver, time); + String _plus_2 = (_plus_1 + _addSolver); + String _addEnd = this.addEnd(); + return (_plus_2 + _addEnd); + } + + public ArrayList getSolverSpecs(final BackendSolver solver) { + if (solver != null) { + switch (solver) { + case CVC4: + return CollectionLiterals.newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT"); + case DARWINFM: + return CollectionLiterals.newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s"); + case EDARWIN: + return CollectionLiterals.newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s"); + case GEOIII: + return CollectionLiterals.newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s"); + case IPROVER: + return CollectionLiterals.newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s"); + case PARADOX: + return CollectionLiterals.newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s"); + case VAMPIRE: + return CollectionLiterals.newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s"); + case Z3: + return CollectionLiterals.newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s"); + default: + break; + } + } + return null; + } + + public String getHeader() { + 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"; + } + + public String addSpec(final String spec) { + return spec.replace("\n", "\\r\\n"); + } + + public String addOptions() { + 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"; + } + + public String addSolver(final BackendSolver solver, final int time) { + final ArrayList solverSpecs = this.getSolverSpecs(solver); + final String ID = solverSpecs.get(0); + final String cmd = solverSpecs.get(1); + String _replace = cmd.replace("%d", Integer.valueOf(time).toString()); + String _plus = ((((((("------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") + _replace); + return (_plus + "\r\n"); + } + + public String addEnd() { + return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"; + } + + public ArrayList sendPost(final String formData) throws Exception { + final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build(); + final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); + final RequestBody body = RequestBody.create(mediaType, formData); + 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", + "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", + "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("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").addHeader("Accept", + "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", + "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", + "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", + "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build(); + final Response response = client.newCall(request).execute(); + return CollectionLiterals.newArrayList(response.body().string().split("\n")); + } } 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 { long startTime = (-((long) 1)); long solverTime = (-((long) 1)); Process p = null; - boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMP); + boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMPIRE); if (_equals) { String OPTION = " --mode casc_sat "; 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 import org.eclipse.viatra.query.runtime.api.IQueryGroup class GeneralTest { - 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" - - def static void main(String[] args) { - val form = makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300) - -// 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 -// -//\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 -// -//------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--") - val x = sendPost(form) - print(x.toString) - } - - def static makeForm(String formula, String solver, String cmd, int time) { - return header + addSpec(formula) + addOptions + addSolver(solver, cmd.replace("%d", time.toString)) + addEnd - } - - def static sendPost(String formData ) throws Exception { - - val OkHttpClient client = new OkHttpClient() - - val MediaType mediaType = MediaType.parse( - "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") - val RequestBody body = RequestBody.create(mediaType, formData) - val 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", - "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", - "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("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"). - addHeader("Accept", - "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", - "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", - "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", - "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build() - - val Response response = client.newCall(request).execute() -// TimeUnit.SECONDS.sleep(5) -// return newArrayList( response.body.string.split("\n")) -return response.body.string - - // case 1: - } - def static getHeader() { - 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" - } - def static addSpec(String spec) { - return spec.replace("\n", "\r\n") - } - def static addOptions() { - 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" - } - def static addSolver(String ID, String cmd) { - 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" - } - def static addEnd() { - return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--" - } def static Map getTypeMap(Map classMap, EcoreMetamodelDescriptor metamodel, 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 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement @@ -11,6 +12,8 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration @@ -32,10 +35,11 @@ class YakinduTest { // Workspace setup val Date date = new Date(System.currentTimeMillis) - val SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss"); + val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm"); val formattedDate = format.format(date) val inputs = new FileSystemWorkspace('''initialModels/''', "") + val dataWorkspace = new FileSystemWorkspace('''output/YakinduTest/''', "") val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "") workspace.initAndClear @@ -55,89 +59,120 @@ class YakinduTest { // val queries = null println("DSL loaded") - var SZ_TOP = 10 - var SZ_BOT = 126 - var INC = 1 + var SZ_TOP = 30 + var SZ_BOT = 5 + var INC = 5 var REPS = 1 - - val RANGE = 3 - val EXACT = 10 + val RUNTIME = 20 + + val EXACT = -1 if (EXACT != -1) { SZ_TOP = EXACT SZ_BOT = EXACT INC = 1 - REPS = 1 + REPS = 10 } + val BACKENDSOLVERS = newArrayList( +// BackendSolver::CVC4 +// , +// BackendSolver::DARWINFM +// , +// BackendSolver::EDARWIN +// , +// BackendSolver::GEOIII +// , + BackendSolver::IPROVER +// , +// BackendSolver::PARADOX +// , +// BackendSolver::VAMPIRE +// , +// BackendSolver::Z3 + ) + - var writer = new PrintWriter(workspace.workspaceURI + "//_yakinduStats.csv") - writer.append("size,") - for (var x = 0; x < REPS; x++) { - writer.append("tTransf" + x + "," + "tSolv" + x + ",") + var str = "" + + for (solver : BACKENDSOLVERS) { + str += solver.name.substring(0, 1) } - writer.append("medSolv,medTransf\n") + + var writer = new PrintWriter( + dataWorkspace.workspaceURI + "//_stats" + formattedDate + "-" + str + SZ_BOT + "to" + SZ_TOP + "by" + INC + + "x" + REPS + ".csv") + writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n") var solverTimes = newArrayList var transformationTimes = newArrayList - var modelFound = true var LogicResult solution = null - for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { - val num = (i - SZ_BOT) / INC - print("Generation " + num + ": SIZE=" + i + " Attempt: ") - writer.append(i + ",") - solverTimes.clear - transformationTimes.clear - modelFound = true - for (var j = 0; j < REPS; j++) { - print(j) + for (BESOLVER : BACKENDSOLVERS) { - val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) - var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel) - var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, - new Viatra2LogicConfiguration) + for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { + val num = (i - SZ_BOT) / INC + println() + println("SOLVER: " + BESOLVER.name + ", SIZE=" + i) + println() - var problem = modelGenerationProblem.output - workspace.writeModel(problem, "Yakindu.logicproblem") + solverTimes.clear + transformationTimes.clear + for (var j = 0; j < REPS; j++) { + print("<> :") + + val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, + new Ecore2LogicConfiguration()) + var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel) + var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, + new Viatra2LogicConfiguration) + + var problem = modelGenerationProblem.output +// workspace.writeModel(problem, "Yakindu.logicproblem") // println("Problem created") // Start Time - var startTime = System.currentTimeMillis - - var VampireSolver reasoner - // * - reasoner = new VampireSolver - - // ///////////////////////////////////////////////////// - // Minimum Scope - val classMapMin = new HashMap - classMapMin.put(Region, 1) - classMapMin.put(Transition, 2) - classMapMin.put(CompositeElement, 3) - val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) - // Maximum Scope - val classMapMax = new HashMap - classMapMax.put(Region, 5) - classMapMax.put(Transition, 2) - val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) - // Define Config File - val size = i - val inc = INC - val iter = j - val vampireConfig = new VampireSolverConfiguration => [ - // add configuration things, in config file first - it.documentationLevel = DocumentationLevel::FULL - it.iteration = iter - it.runtimeLimit = 60 - it.typeScopes.maxNewElements = -1 - it.typeScopes.minNewElements = size - it.genModel = false - if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin - if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax - it.contCycleLevel = 5 - it.uniquenessDuplicates = false - ] - - solution = reasoner.solve(problem, vampireConfig, workspace) + var startTime = System.currentTimeMillis + + var VampireSolver reasoner + // * + reasoner = new VampireSolver + + // ///////////////////////////////////////////////////// + // Minimum Scope + val classMapMin = new HashMap + classMapMin.put(Region, 1) + classMapMin.put(Transition, 2) + classMapMin.put(CompositeElement, 3) + val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, + modelGenerationProblem.trace) + // Maximum Scope + val classMapMax = new HashMap + classMapMax.put(Region, 5) + classMapMax.put(Transition, 2) + val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, + modelGenerationProblem.trace) + // Define Config File + val size = i + val inc = INC + val iter = j + val vampireConfig = new VampireSolverConfiguration => [ + // add configuration things, in config file first + it.documentationLevel = DocumentationLevel::FULL + it.iteration = iter + it.runtimeLimit = RUNTIME +// it.typeScopes.maxNewElements = size + it.typeScopes.minNewElements = size + + it.genModel = true + it.server = true + it.solver = BESOLVER + +// if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin +// if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax + it.contCycleLevel = 5 + it.uniquenessDuplicates = false + ] + + solution = reasoner.solve(problem, vampireConfig, workspace) // print((solution as ModelResult).representation.get(0)) // val soln = ((solution as ModelResult).representation.get(0) as VampireModel) // println(soln.confirmations) @@ -145,20 +180,35 @@ class YakinduTest { // modelFound = !soln.confirmations.filter [ // class == VLSFiniteModelImpl // ].isEmpty -// -// if (modelFound) { - val tTime = solution.statistics.transformationTime / 1000.0 - val sTime = solution.statistics.solverTime / 1000.0 - writer.append(tTime + "," + sTime + ",") - print("(" + tTime + "/" + sTime + "s)..") - solverTimes.add(sTime) - transformationTimes.add(tTime) +// ADD TO CSV + writer.append(vampireConfig.solver.name + ",") + writer.append(size + ",") + writer.append(solution.statistics.transformationTime / 1000.0 + ",") + + val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry). + value + val satTime = (solution.statistics.entries.filter[name == "satTime"].get(0) as RealStatisticEntry). + value + val modOut = (solution.statistics.entries.filter[name == "modOut"].get(0) as StringStatisticEntry). + value + val modTime = (solution.statistics.entries.filter[name == "modTime"].get(0) as RealStatisticEntry). + value + + writer.append(satOut + ",") + writer.append(satTime + ",") + writer.append(modOut + ",") + writer.append(modTime + ",") + writer.append("\n") + +// print("(" + tTime + "/" + sTime + "s)..") +// solverTimes.add(sTime) +// transformationTimes.add(tTime) // } else { // writer.append("MNF" + ",") //// print("MNF") // } - // println("Problem solved") - // visualisation, see + // println("Problem solved") + // visualisation, see // var interpretations = reasoner.getInterpretations(solution as ModelResult) // for (interpretation : interpretations) { // val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) @@ -168,15 +218,15 @@ class YakinduTest { // var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 // println("Problem solved") // println("Time was: " + totalTimeMin + ":" + totalTimeSec) + } +// println() +// var solverMed = solverTimes.sort.get(REPS / 2) +// var transformationMed = transformationTimes.sort.get(REPS / 2) +// writer.append(solverMed.toString + "," + transformationMed.toString) } - println() - var solverMed = solverTimes.sort.get(REPS / 2) - var transformationMed = transformationTimes.sort.get(REPS / 2) - writer.append(solverMed.toString + "," + transformationMed.toString) - writer.append("\n") + } writer.close - } } 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin 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; import java.util.List; import java.util.Map; import java.util.Set; -import okhttp3.MediaType; -import okhttp3.OkHttpClient; -import okhttp3.Request; -import okhttp3.RequestBody; -import okhttp3.Response; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.ecore.EAttribute; import org.eclipse.emf.ecore.EClass; @@ -33,75 +28,12 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup; import org.eclipse.viatra.query.runtime.api.IQuerySpecification; import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Exceptions; import org.eclipse.xtext.xbase.lib.Functions.Function1; -import org.eclipse.xtext.xbase.lib.InputOutput; import org.eclipse.xtext.xbase.lib.IterableExtensions; import org.eclipse.xtext.xbase.lib.ListExtensions; @SuppressWarnings("all") public class GeneralTest { - 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"; - - public static void main(final String[] args) { - try { - 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); - final String x = GeneralTest.sendPost(form); - InputOutput.print(x.toString()); - } catch (Throwable _e) { - throw Exceptions.sneakyThrow(_e); - } - } - - public static String makeForm(final String formula, final String solver, final String cmd, final int time) { - String _header = GeneralTest.getHeader(); - String _addSpec = GeneralTest.addSpec(formula); - String _plus = (_header + _addSpec); - String _addOptions = GeneralTest.addOptions(); - String _plus_1 = (_plus + _addOptions); - String _addSolver = GeneralTest.addSolver(solver, cmd.replace("%d", Integer.valueOf(time).toString())); - String _plus_2 = (_plus_1 + _addSolver); - String _addEnd = GeneralTest.addEnd(); - return (_plus_2 + _addEnd); - } - - public static String sendPost(final String formData) throws Exception { - final OkHttpClient client = new OkHttpClient(); - final MediaType mediaType = MediaType.parse( - "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); - final RequestBody body = RequestBody.create(mediaType, formData); - 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", - "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", - "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("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").addHeader("Accept", - "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", - "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", - "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", - "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build(); - final Response response = client.newCall(request).execute(); - return response.body().string(); - } - - public static String getHeader() { - 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"; - } - - public static String addSpec(final String spec) { - return spec.replace("\n", "\r\n"); - } - - public static String addOptions() { - 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"; - } - - public static String addSolver(final String ID, final String cmd) { - 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"); - } - - public static String addEnd() { - return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"; - } - public static Map getTypeMap(final Map classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { final HashMap typeMap = new HashMap(); final Function1 _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; import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement; import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region; import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition; import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; +import com.google.common.base.Objects; import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; @@ -17,6 +19,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; @@ -37,7 +42,9 @@ import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; import org.eclipse.xtend2.lib.StringConcatenation; import org.eclipse.xtext.xbase.lib.CollectionLiterals; +import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.Exceptions; +import org.eclipse.xtext.xbase.lib.Functions.Function1; import org.eclipse.xtext.xbase.lib.InputOutput; import org.eclipse.xtext.xbase.lib.IterableExtensions; import org.eclipse.xtext.xbase.lib.ObjectExtensions; @@ -53,17 +60,20 @@ public class YakinduTest { final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); long _currentTimeMillis = System.currentTimeMillis(); final Date date = new Date(_currentTimeMillis); - final SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss"); + final SimpleDateFormat format = new SimpleDateFormat("dd-HHmm"); final String formattedDate = format.format(date); StringConcatenation _builder = new StringConcatenation(); _builder.append("initialModels/"); final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); StringConcatenation _builder_1 = new StringConcatenation(); _builder_1.append("output/YakinduTest/"); - String _plus = (_builder_1.toString() + formattedDate); + final FileSystemWorkspace dataWorkspace = new FileSystemWorkspace(_builder_1.toString(), ""); StringConcatenation _builder_2 = new StringConcatenation(); - _builder_2.append("/"); - String _plus_1 = (_plus + _builder_2); + _builder_2.append("output/YakinduTest/"); + String _plus = (_builder_2.toString() + formattedDate); + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.append("/"); + String _plus_1 = (_plus + _builder_3); final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, ""); workspace.initAndClear(); final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; @@ -75,117 +85,149 @@ public class YakinduTest { final EList partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); InputOutput.println("DSL loaded"); - int SZ_TOP = 10; - int SZ_BOT = 126; - int INC = 1; + int SZ_TOP = 30; + int SZ_BOT = 5; + int INC = 5; int REPS = 1; - final int RANGE = 3; - final int EXACT = 10; + final int RUNTIME = 20; + final int EXACT = (-1); if ((EXACT != (-1))) { SZ_TOP = EXACT; SZ_BOT = EXACT; INC = 1; - REPS = 1; + REPS = 10; } - URI _workspaceURI = workspace.getWorkspaceURI(); - String _plus_2 = (_workspaceURI + "//_yakinduStats.csv"); - PrintWriter writer = new PrintWriter(_plus_2); - writer.append("size,"); - for (int x = 0; (x < REPS); x++) { - writer.append(((((("tTransf" + Integer.valueOf(x)) + ",") + "tSolv") + Integer.valueOf(x)) + ",")); + final ArrayList BACKENDSOLVERS = CollectionLiterals.newArrayList( + BackendSolver.IPROVER); + String str = ""; + for (final BackendSolver solver : BACKENDSOLVERS) { + String _str = str; + String _substring = solver.name().substring(0, 1); + str = (_str + _substring); } - writer.append("medSolv,medTransf\n"); - ArrayList solverTimes = CollectionLiterals.newArrayList(); - ArrayList transformationTimes = CollectionLiterals.newArrayList(); - boolean modelFound = true; + URI _workspaceURI = dataWorkspace.getWorkspaceURI(); + String _plus_2 = (_workspaceURI + "//_stats"); + String _plus_3 = (_plus_2 + formattedDate); + String _plus_4 = (_plus_3 + "-"); + String _plus_5 = (_plus_4 + str); + String _plus_6 = (_plus_5 + Integer.valueOf(SZ_BOT)); + String _plus_7 = (_plus_6 + "to"); + String _plus_8 = (_plus_7 + Integer.valueOf(SZ_TOP)); + String _plus_9 = (_plus_8 + "by"); + String _plus_10 = (_plus_9 + Integer.valueOf(INC)); + String _plus_11 = (_plus_10 + + "x"); + String _plus_12 = (_plus_11 + Integer.valueOf(REPS)); + String _plus_13 = (_plus_12 + ".csv"); + PrintWriter writer = new PrintWriter(_plus_13); + writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n"); + ArrayList solverTimes = CollectionLiterals.newArrayList(); + ArrayList transformationTimes = CollectionLiterals.newArrayList(); LogicResult solution = null; - { - int i = SZ_BOT; - boolean _while = (i <= SZ_TOP); - while (_while) { - { - final int num = ((i - SZ_BOT) / INC); - InputOutput.print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); - String _plus_3 = (Integer.valueOf(i) + ","); - writer.append(_plus_3); - solverTimes.clear(); - transformationTimes.clear(); - modelFound = true; - for (int j = 0; (j < REPS); j++) { - { - InputOutput.print(Integer.valueOf(j)); - Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); - final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); - TracedOutput modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); - Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); - TracedOutput validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration); - LogicProblem problem = modelGenerationProblem.getOutput(); - workspace.writeModel(problem, "Yakindu.logicproblem"); - long startTime = System.currentTimeMillis(); - VampireSolver reasoner = null; - VampireSolver _vampireSolver = new VampireSolver(); - reasoner = _vampireSolver; - final HashMap classMapMin = new HashMap(); - classMapMin.put(Region.class, Integer.valueOf(1)); - classMapMin.put(Transition.class, Integer.valueOf(2)); - classMapMin.put(CompositeElement.class, Integer.valueOf(3)); - final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); - final HashMap classMapMax = new HashMap(); - classMapMax.put(Region.class, Integer.valueOf(5)); - classMapMax.put(Transition.class, Integer.valueOf(2)); - final Map typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); - final int size = i; - final int inc = INC; - final int iter = j; - VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); - final Procedure1 _function = (VampireSolverConfiguration it) -> { - it.documentationLevel = DocumentationLevel.FULL; - it.iteration = iter; - it.runtimeLimit = 60; - it.typeScopes.maxNewElements = (-1); - it.typeScopes.minNewElements = size; - it.genModel = false; - int _size = typeMapMin.size(); - boolean _notEquals = (_size != 0); - if (_notEquals) { - it.typeScopes.minNewElementsByType = typeMapMin; - } - int _size_1 = typeMapMin.size(); - boolean _notEquals_1 = (_size_1 != 0); - if (_notEquals_1) { - it.typeScopes.maxNewElementsByType = typeMapMax; - } - it.contCycleLevel = 5; - it.uniquenessDuplicates = false; - }; - final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); - solution = reasoner.solve(problem, vampireConfig, workspace); - int _transformationTime = solution.getStatistics().getTransformationTime(); - final double tTime = (_transformationTime / 1000.0); - int _solverTime = solution.getStatistics().getSolverTime(); - final double sTime = (_solverTime / 1000.0); - String _plus_4 = (Double.valueOf(tTime) + ","); - String _plus_5 = (_plus_4 + Double.valueOf(sTime)); - String _plus_6 = (_plus_5 + ","); - writer.append(_plus_6); - InputOutput.print((((("(" + Double.valueOf(tTime)) + "/") + Double.valueOf(sTime)) + "s)..")); - solverTimes.add(Double.valueOf(sTime)); - transformationTimes.add(Double.valueOf(tTime)); + for (final BackendSolver BESOLVER : BACKENDSOLVERS) { + { + int i = SZ_BOT; + boolean _while = (i <= SZ_TOP); + while (_while) { + { + final int num = ((i - SZ_BOT) / INC); + InputOutput.println(); + String _name = BESOLVER.name(); + String _plus_14 = ("SOLVER: " + _name); + String _plus_15 = (_plus_14 + ", SIZE="); + String _plus_16 = (_plus_15 + Integer.valueOf(i)); + InputOutput.println(_plus_16); + InputOutput.println(); + solverTimes.clear(); + transformationTimes.clear(); + for (int j = 0; (j < REPS); j++) { + { + InputOutput.print((("<> :")); + Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); + final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); + TracedOutput modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); + Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); + TracedOutput validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration); + LogicProblem problem = modelGenerationProblem.getOutput(); + long startTime = System.currentTimeMillis(); + VampireSolver reasoner = null; + VampireSolver _vampireSolver = new VampireSolver(); + reasoner = _vampireSolver; + final HashMap classMapMin = new HashMap(); + classMapMin.put(Region.class, Integer.valueOf(1)); + classMapMin.put(Transition.class, Integer.valueOf(2)); + classMapMin.put(CompositeElement.class, Integer.valueOf(3)); + final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, + modelGenerationProblem.getTrace()); + final HashMap classMapMax = new HashMap(); + classMapMax.put(Region.class, Integer.valueOf(5)); + classMapMax.put(Transition.class, Integer.valueOf(2)); + final Map typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, + modelGenerationProblem.getTrace()); + final int size = i; + final int inc = INC; + final int iter = j; + VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); + final Procedure1 _function = (VampireSolverConfiguration it) -> { + it.documentationLevel = DocumentationLevel.FULL; + it.iteration = iter; + it.runtimeLimit = RUNTIME; + it.typeScopes.minNewElements = size; + it.genModel = true; + it.server = true; + it.solver = BESOLVER; + it.contCycleLevel = 5; + it.uniquenessDuplicates = false; + }; + final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); + solution = reasoner.solve(problem, vampireConfig, workspace); + String _name_1 = vampireConfig.solver.name(); + String _plus_17 = (_name_1 + ","); + writer.append(_plus_17); + String _plus_18 = (Integer.valueOf(size) + ","); + writer.append(_plus_18); + int _transformationTime = solution.getStatistics().getTransformationTime(); + double _divide = (_transformationTime / 1000.0); + String _plus_19 = (Double.valueOf(_divide) + ","); + writer.append(_plus_19); + final Function1 _function_1 = (StatisticEntry it) -> { + String _name_2 = it.getName(); + return Boolean.valueOf(Objects.equal(_name_2, "satOut")); + }; + StatisticEntry _get = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.filter(solution.getStatistics().getEntries(), _function_1), StatisticEntry.class))[0]; + final String satOut = ((StringStatisticEntry) _get).getValue(); + final Function1 _function_2 = (StatisticEntry it) -> { + String _name_2 = it.getName(); + return Boolean.valueOf(Objects.equal(_name_2, "satTime")); + }; + StatisticEntry _get_1 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.filter(solution.getStatistics().getEntries(), _function_2), StatisticEntry.class))[0]; + final double satTime = ((RealStatisticEntry) _get_1).getValue(); + final Function1 _function_3 = (StatisticEntry it) -> { + String _name_2 = it.getName(); + return Boolean.valueOf(Objects.equal(_name_2, "modOut")); + }; + StatisticEntry _get_2 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.filter(solution.getStatistics().getEntries(), _function_3), StatisticEntry.class))[0]; + final String modOut = ((StringStatisticEntry) _get_2).getValue(); + final Function1 _function_4 = (StatisticEntry it) -> { + String _name_2 = it.getName(); + return Boolean.valueOf(Objects.equal(_name_2, "modTime")); + }; + StatisticEntry _get_3 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.filter(solution.getStatistics().getEntries(), _function_4), StatisticEntry.class))[0]; + final double modTime = ((RealStatisticEntry) _get_3).getValue(); + writer.append((satOut + ",")); + String _plus_20 = (Double.valueOf(satTime) + ","); + writer.append(_plus_20); + writer.append((modOut + ",")); + String _plus_21 = (Double.valueOf(modTime) + ","); + writer.append(_plus_21); + writer.append("\n"); + } } } - InputOutput.println(); - Double solverMed = IterableExtensions.sort(solverTimes).get((REPS / 2)); - Double transformationMed = IterableExtensions.sort(transformationTimes).get((REPS / 2)); - String _string = solverMed.toString(); - String _plus_4 = (_string + ","); - String _string_1 = transformationMed.toString(); - String _plus_5 = (_plus_4 + _string_1); - writer.append(_plus_5); - writer.append("\n"); + int _i = i; + i = (_i + INC); + _while = (i <= SZ_TOP); } - int _i = i; - i = (_i + INC); - _while = (i <= SZ_TOP); } } 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin differ -- cgit v1.2.3-54-g00ecf