From 16f9cd46474a4934c1afd733d687f3c382fbdf56 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 10 Oct 2019 22:25:07 -0400 Subject: implement http requests for the TPTP server --- .../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 .../reasoner/VampireAnalyzerConfiguration.xtend | 1 + .../vampire/reasoner/VampireSolver.xtend | 59 ++++----- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 5 +- .../vampire/reasoner/builder/VampireHandler.xtend | 6 +- .../.VampireAnalyzerConfiguration.xtendbin | Bin 3082 -> 3161 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 6973 -> 6885 bytes .../vampire/reasoner/VampireSolver.java | 39 +++--- .../reasoner/VampireSolverConfiguration.java | 2 + .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 19565 -> 19565 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 10676 -> 10660 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13060 -> 13060 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11037 -> 11037 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3997 -> 3997 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 7838 -> 7803 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../Logic2VampireLanguageMapper_ScopeMapper.java | 4 +- .../vampire/reasoner/builder/VampireHandler.java | 14 +-- .../.classpath | 6 + .../META-INF/MANIFEST.MF | 78 ++++++------ .../dslreasoner/vampire/icse/FileSystemTest.xtend | 2 +- .../dslreasoner/vampire/icse/GeneralTest.xtend | 79 +++++++++++- .../dslreasoner/vampire/icse/YakinduTest.xtend | 58 ++++----- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 4545 -> 4552 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 6624 -> 6632 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 6204 -> 6207 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 6456 -> 10182 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 7958 -> 8484 bytes .../dslreasoner/vampire/icse/FileSystemTest.java | 135 +++++++++++---------- .../ecse/dslreasoner/vampire/icse/GeneralTest.java | 71 ++++++++++- .../ecse/dslreasoner/vampire/icse/YakinduTest.java | 56 ++++++--- .../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 52 files changed, 387 insertions(+), 228 deletions(-) diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin index ef511dca..1eaefbda 100644 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 c9ed86f5..05c29aff 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 e24f55b7..12f063b1 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 af221451..88a713db 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 1f1241ce..31d3dbf6 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 e89f2182..ca30b3d0 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 9c0c7969..0d75d237 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 fe289357..a8d38a91 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 6cb28d31..0192cd3c 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 7e8ae1ab..07f4c611 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 81de0171..01c9f74f 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 c5672cca..b4bd4155 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 2b96a53a..5dd72d15 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 5faad94e..db384a64 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/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend index b223dbe5..4e9737cb 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend @@ -8,6 +8,7 @@ class VampireSolverConfiguration extends LogicSolverConfiguration { public var boolean uniquenessDuplicates = false public var int iteration = -1 public var BackendSolver solver = BackendSolver::VAMP + public var genModel = true //choose needed backend solver // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend index 3281a196..85b81a8c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend @@ -31,29 +31,32 @@ class VampireSolver extends LogicReasoner { val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper val VampireHandler handler = new VampireHandler - var fileName = "problem.tptp" +// var fileName = "problem.tptp" - def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) { - fileName = location + fileName - solve(problem, config, workspace) - } +// 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" // Start: Logic -> Vampire mapping val transformationStart = System.currentTimeMillis // TODO val result = forwardMapper.transformProblem(problem, vampireConfig) val transformationTime = System.currentTimeMillis - transformationStart - + val vampireProblem = result.output val forwardTrace = result.trace var String fileURI = null; var String vampireCode = null; vampireCode = workspace.writeModelToString(vampireProblem, fileName) + + val writeFile = ( vampireConfig.documentationLevel === DocumentationLevel::NORMAL || @@ -61,35 +64,33 @@ class VampireSolver extends LogicReasoner { if (writeFile) { fileURI = workspace.writeModel(vampireProblem, fileName).toFileString } - - - + // Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("tptp", new VampireLanguageFactoryImpl) //// val Resource resource = Resource. //// Resource.getResource(wsURI+"problem.tptp") as Resource //// resource // val model = workspace.readModel(VampireModel, "problem.tptp").eResource.contents // println(model) - - - // Result as String - // Finish: Logic -> Vampire mapping - - // 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) + if (vampireConfig.genModel) { - val backTransformationTime = System.currentTimeMillis - backTransformationStart - // Finish: Vampire -> Logic Mapping - + // 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) } def asConfig(LogicSolverConfiguration configuration) { @@ -105,9 +106,9 @@ class VampireSolver extends LogicReasoner { // * override getInterpretations(ModelResult modelResult) { // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] - val sols = modelResult.representation// as List - //val res = answers.map - sols.map[ + val sols = modelResult.representation // as List + // val res = answers.map + sols.map [ new VampireModelInterpretation( // forwardMapper.typeMapper.typeInterpreter, it as VampireModel, diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index df3cfd82..39862c65 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend @@ -25,8 +25,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { def dispatch public void transformScope(List types, VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { - val ABSOLUTE_MIN = 0 - val ABSOLUTE_MAX = Integer.MAX_VALUE + // TODO HANDLE ERRORS RELATED TO MAX > MIN // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS @@ -40,6 +39,8 @@ class Logic2VampireLanguageMapper_ScopeMapper { // Number of defined non-abstract elements that are not enum elements // Equals the number of elements in te initial model var elemsInIM = trace.definedElement2String.size + val ABSOLUTE_MIN = 0 + val ABSOLUTE_MAX = -1-elemsInIM // var elemsInIM = 0 // // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend index c1eb3382..47eae807 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend @@ -52,8 +52,10 @@ class VampireHandler { val CMD = "cmd /c " val TEMPNAME = "TEMP.tptp" - val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + - "_" + configuration.iteration + ".tptp" +// val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + +// "_" + configuration.iteration + ".tptp" + val SOLNNAME = "solution" + "_" + configuration.typeScopes.maxNewElements + "_" + configuration.iteration + + ".tptp" val PATH = "C:/cygwin64/bin" val wsURI = workspace.workspaceURI diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 85f3773c..e50e6812 100644 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 77dc060f..e4925e24 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 c3e185f5..432b14c3 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java @@ -24,7 +24,6 @@ import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; import java.util.List; import org.eclipse.emf.common.util.EList; import org.eclipse.xtend2.lib.StringConcatenation; -import org.eclipse.xtext.xbase.lib.Exceptions; import org.eclipse.xtext.xbase.lib.Functions.Function1; import org.eclipse.xtext.xbase.lib.ListExtensions; @@ -42,24 +41,10 @@ public class VampireSolver extends LogicReasoner { private final VampireHandler handler = new VampireHandler(); - private String fileName = "problem.tptp"; - - public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace, final String location) { - try { - LogicResult _xblockexpression = null; - { - this.fileName = (location + this.fileName); - _xblockexpression = this.solve(problem, config, workspace); - } - return _xblockexpression; - } catch (Throwable _e) { - throw Exceptions.sneakyThrow(_e); - } - } - @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(); @@ -68,18 +53,24 @@ public class VampireSolver extends LogicReasoner { final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); String fileURI = null; String vampireCode = null; - vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); + vampireCode = workspace.writeModelToString(vampireProblem, fileName); final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || (vampireConfig.documentationLevel == DocumentationLevel.FULL)); if (writeFile) { - fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); + 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; } - 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); } public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java index 7bb17b59..dd66e910 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java @@ -12,4 +12,6 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration { public int iteration = (-1); public BackendSolver solver = BackendSolver.VAMP; + + public boolean genModel = true; } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index eb1685d1..8d2ec6ab 100644 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 3ddf9cfc..515b4b3c 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 66f9d9e8..46ad8c79 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 bafcfab6..169aedc2 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 a4af882f..699ce6e2 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 08f9fd96..799515d4 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 dc25e3be..2a112ae7 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 37b0c7a5..7f32e055 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 6d562aa8..a2dd469b 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 5ed9ac3b..98c355ab 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 111053a4..246c08c8 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 f33599f9..9e55bac4 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 6da75271..bc39a068 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java @@ -53,9 +53,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper { } public void _transformScope(final List types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { - final int ABSOLUTE_MIN = 0; - final int ABSOLUTE_MAX = Integer.MAX_VALUE; int elemsInIM = trace.definedElement2String.size(); + final int ABSOLUTE_MIN = 0; + final int ABSOLUTE_MAX = ((-1) - elemsInIM); final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); final ArrayList localInstances = CollectionLiterals.newArrayList(); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java index 7906c5fb..fcbdfde7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java @@ -30,19 +30,13 @@ public class VampireHandler { final String CVC4LOC = (CVC4DIR + CVC4NAME); final String CMD = "cmd /c "; final String TEMPNAME = "TEMP.tptp"; - String _string = configuration.solver.toString(); - String _plus = ("solution" + _string); - String _plus_1 = (_plus + "_"); - String _plus_2 = (_plus_1 + Integer.valueOf(configuration.typeScopes.maxNewElements)); - String _plus_3 = (_plus_2 + - "_"); - String _plus_4 = (_plus_3 + Integer.valueOf(configuration.iteration)); - final String SOLNNAME = (_plus_4 + ".tptp"); + final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + + ".tptp"); final String PATH = "C:/cygwin64/bin"; final URI wsURI = workspace.getWorkspaceURI(); final String tempLoc = (wsURI + TEMPNAME); - String _plus_5 = (wsURI + SOLNNAME); - final String solnLoc = (_plus_5 + " "); + String _plus = (wsURI + SOLNNAME); + final String solnLoc = (_plus + " "); String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); long startTime = (-((long) 1)); long solverTime = (-((long) 1)); diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath index 3f0838b6..7618afdf 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath @@ -5,5 +5,11 @@ + + + + + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF index 0af80e6c..dead7622 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF @@ -6,48 +6,44 @@ Bundle-Version: 1.0.0.qualifier Bundle-ClassPath: . Bundle-Vendor: %providerName Bundle-Localization: plugin -Export-Package: ca.mcgill.ecse.dslreasoner.vamipre.yakindumm, - ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.impl, - ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.util, - ca.mcgill.ecse.dslreasoner.vampire.queries, - ca.mcgill.ecse.dslreasoner.vampire.yakindumm, - ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl, - ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util, - yakindumm, - yakindumm.impl, - yakindumm.util, - yakindumm.yakindumm, - yakindumm.yakindumm.impl, - yakindumm.yakindumm.util +Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries, + ca.mcgill.ecse.dslreasoner.vampire.yakindumm, + ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl, + ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime, - org.eclipse.core.runtime, - org.eclipse.emf.ecore;visibility:=reexport, - org.eclipse.viatra.query.runtime.rete, - org.eclipse.viatra.query.runtime.localsearch, - com.google.guava, - org.eclipse.xtext.xbase.lib, - org.eclipse.xtend.lib, - org.eclipse.xtend.lib.macro, - ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", - ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", - org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", - hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0", - ModelGenExampleFAM_plugin;bundle-version="1.0.0", - ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1", - hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1", - org.eclipse.viatra.query.runtime;bundle-version="2.1.0", - org.eclipse.collections;bundle-version="9.2.0", - hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", - ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0" + org.eclipse.core.runtime, + org.eclipse.emf.ecore;visibility:=reexport, + org.eclipse.viatra.query.runtime.rete, + org.eclipse.viatra.query.runtime.localsearch, + com.google.guava, + org.eclipse.xtext.xbase.lib, + org.eclipse.xtend.lib, + org.eclipse.xtend.lib.macro, + ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", + ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", + org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", + hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0", + ModelGenExampleFAM_plugin;bundle-version="1.0.0", + ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1", + hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1", + org.eclipse.viatra.query.runtime;bundle-version="2.1.0", + org.eclipse.collections;bundle-version="9.2.0", + hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", + ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0", + org.apache.httpcomponents.httpcore;bundle-version="4.4.6", + org.apache.httpcomponents.httpclient;bundle-version="4.5.2", + org.apache.httpcomponents.httpclient.source;bundle-version="4.5.2", + org.apache.httpcomponents.httpclient.win;bundle-version="4.5.2", + org.apache.httpcomponents.httpcore.source;bundle-version="4.4.6" Import-Package: org.apache.log4j Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test Bundle-ActivationPolicy: lazy diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend index 2495ab77..5289371f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend @@ -86,7 +86,7 @@ class FileSystemTest { it.uniquenessDuplicates = false ] - var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS") + var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) /*/ * diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend index 89375801..5225fb89 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend @@ -9,6 +9,11 @@ import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace import java.util.HashMap import java.util.List import java.util.Map +import okhttp3.MediaType +import okhttp3.OkHttpClient +import okhttp3.Request +import okhttp3.RequestBody +import okhttp3.Response import org.eclipse.emf.ecore.EAttribute import org.eclipse.emf.ecore.EClass import org.eclipse.emf.ecore.EEnum @@ -20,15 +25,77 @@ import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl import org.eclipse.viatra.query.runtime.api.IQueryGroup -class GeneralTest { - def static Map getTypeMap(Map classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) { +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) { val typeMap = new HashMap val listMap = metamodel.classes.toMap[s|s.name] - + for (Class elem : classMap.keySet) { typeMap.put(e2l.TypeofEClass( - trace, listMap.get(elem.simpleName) - ), classMap.get(elem)) + trace, + listMap.get(elem.simpleName) + ), classMap.get(elem)) } return typeMap } @@ -43,7 +110,7 @@ class GeneralTest { } def static loadPartialModel(ReasonerWorkspace inputs, String path) { - Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); + Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()) inputs.readModel(EObject, path).eResource.contents // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend index 28e3e685..c35b200e 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend @@ -3,13 +3,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns 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 ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel 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.ModelResult import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration @@ -17,8 +18,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.Insta import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace import java.io.PrintWriter import java.text.SimpleDateFormat -import java.time.LocalDate import java.util.Date +import java.util.HashMap import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl @@ -54,16 +55,18 @@ class YakinduTest { // val queries = null println("DSL loaded") - var MAX = 80 - var START = 79 + var SZ_TOP = 10 + var SZ_BOT = 126 var INC = 1 - var REPS = 3 + var REPS = 1 + + val RANGE = 3 - val EXACT = 130 + val EXACT = 10 if (EXACT != -1) { - MAX = EXACT - START = EXACT - INC = 5 + SZ_TOP = EXACT + SZ_BOT = EXACT + INC = 1 REPS = 1 } @@ -77,8 +80,8 @@ class YakinduTest { var transformationTimes = newArrayList var modelFound = true var LogicResult solution = null - for (var i = START; i <= MAX; i += INC) { - val num = (i - START) / INC + 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 @@ -106,17 +109,16 @@ class YakinduTest { // ///////////////////////////////////////////////////// // 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) + 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) -// classMapMax.put(Synchronization, 4) -// val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) + 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 @@ -126,18 +128,18 @@ class YakinduTest { it.documentationLevel = DocumentationLevel::FULL it.iteration = iter it.runtimeLimit = 60 - it.typeScopes.maxNewElements = size - it.typeScopes.minNewElements = size - 5 - -// if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin -// if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax + 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) // print((solution as ModelResult).representation.get(0)) - val soln = ((solution as ModelResult).representation.get(0) as VampireModel) +// val soln = ((solution as ModelResult).representation.get(0) as VampireModel) // println(soln.confirmations) // println((solution as ModelResult).representation) // modelFound = !soln.confirmations.filter [ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin index 084503b5..93d27b4d 100644 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 2315cd50..bc2bae6f 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 a3386941..5687258f 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 dee6f742..de68a908 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 f54cd3a0..16a3cd03 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/FileSystemTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java index 7579bd98..8c7923be 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java @@ -25,6 +25,7 @@ import org.eclipse.emf.ecore.EObject; 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.Exceptions; import org.eclipse.xtext.xbase.lib.InputOutput; import org.eclipse.xtext.xbase.lib.ObjectExtensions; import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @@ -32,70 +33,74 @@ import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @SuppressWarnings("all") public class FileSystemTest { public static void main(final String[] args) { - final Ecore2Logic ecore2Logic = new Ecore2Logic(); - final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); - final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); - StringConcatenation _builder = new StringConcatenation(); - _builder.append("initialModels/"); - final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("output/FileSystemTest/"); - final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); - workspace.initAndClear(); - final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; - final Map map = reg.getExtensionToFactoryMap(); - XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); - map.put("logicproblem", _xMIResourceFactoryImpl); - InputOutput.println("Input and output workspaces are created"); - final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); - final EList partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); - InputOutput.println("DSL loaded"); - Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); - final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); - LogicProblem problem = modelGenerationProblem.getOutput(); - problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); - workspace.writeModel(problem, "FileSystem.logicproblem"); - InputOutput.println("Problem created"); - long startTime = System.currentTimeMillis(); - VampireSolver reasoner = null; - VampireSolver _vampireSolver = new VampireSolver(); - reasoner = _vampireSolver; - final HashMap classMapMin = new HashMap(); - classMapMin.put(Dir.class, Integer.valueOf(10)); - classMapMin.put(File.class, Integer.valueOf(5)); - final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); - final HashMap classMapMax = new HashMap(); - classMapMax.put(File.class, Integer.valueOf(15)); - classMapMax.put(Dir.class, Integer.valueOf(15)); - final Map typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); - VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); - final Procedure1 _function = (VampireSolverConfiguration it) -> { - it.documentationLevel = DocumentationLevel.FULL; - it.typeScopes.minNewElements = 10; - it.typeScopes.maxNewElements = 25; - 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); - LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS"); - long _currentTimeMillis = System.currentTimeMillis(); - long _minus = (_currentTimeMillis - startTime); - long totalTimeMin = (_minus / 60000); - long _currentTimeMillis_1 = System.currentTimeMillis(); - long _minus_1 = (_currentTimeMillis_1 - startTime); - long _divide = (_minus_1 / 1000); - long totalTimeSec = (_divide % 60); - InputOutput.println("Problem solved"); - InputOutput.println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); + try { + final Ecore2Logic ecore2Logic = new Ecore2Logic(); + final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); + final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("initialModels/"); + final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("output/FileSystemTest/"); + final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); + workspace.initAndClear(); + final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; + final Map map = reg.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); + map.put("logicproblem", _xMIResourceFactoryImpl); + InputOutput.println("Input and output workspaces are created"); + final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); + final EList partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); + InputOutput.println("DSL loaded"); + Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); + final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); + LogicProblem problem = modelGenerationProblem.getOutput(); + problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); + workspace.writeModel(problem, "FileSystem.logicproblem"); + InputOutput.println("Problem created"); + long startTime = System.currentTimeMillis(); + VampireSolver reasoner = null; + VampireSolver _vampireSolver = new VampireSolver(); + reasoner = _vampireSolver; + final HashMap classMapMin = new HashMap(); + classMapMin.put(Dir.class, Integer.valueOf(10)); + classMapMin.put(File.class, Integer.valueOf(5)); + final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + final HashMap classMapMax = new HashMap(); + classMapMax.put(File.class, Integer.valueOf(15)); + classMapMax.put(Dir.class, Integer.valueOf(15)); + final Map typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); + final Procedure1 _function = (VampireSolverConfiguration it) -> { + it.documentationLevel = DocumentationLevel.FULL; + it.typeScopes.minNewElements = 10; + it.typeScopes.maxNewElements = 25; + 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); + LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); + long _currentTimeMillis = System.currentTimeMillis(); + long _minus = (_currentTimeMillis - startTime); + long totalTimeMin = (_minus / 60000); + long _currentTimeMillis_1 = System.currentTimeMillis(); + long _minus_1 = (_currentTimeMillis_1 - startTime); + long _divide = (_minus_1 / 1000); + long totalTimeSec = (_divide % 60); + InputOutput.println("Problem solved"); + InputOutput.println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); + } } } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java index 0bb8f76e..ce057092 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java @@ -13,6 +13,11 @@ import java.util.HashMap; 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; @@ -28,12 +33,75 @@ 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) -> { @@ -43,7 +111,8 @@ public class GeneralTest { Set _keySet = classMap.keySet(); for (final Class elem : _keySet) { typeMap.put( - e2l.TypeofEClass(trace, listMap.get(elem.getSimpleName())), classMap.get(elem)); + e2l.TypeofEClass(trace, + listMap.get(elem.getSimpleName())), classMap.get(elem)); } return typeMap; } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java index b18ede4f..3a8f3fb4 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java @@ -4,17 +4,19 @@ import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns; 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 ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; 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; import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; 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.ModelResult; import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; @@ -26,6 +28,7 @@ import java.io.PrintWriter; import java.text.SimpleDateFormat; import java.util.ArrayList; import java.util.Date; +import java.util.HashMap; import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.common.util.URI; @@ -72,15 +75,16 @@ 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 MAX = 80; - int START = 79; + int SZ_TOP = 10; + int SZ_BOT = 126; int INC = 1; - int REPS = 3; - final int EXACT = 130; + int REPS = 1; + final int RANGE = 3; + final int EXACT = 10; if ((EXACT != (-1))) { - MAX = EXACT; - START = EXACT; - INC = 5; + SZ_TOP = EXACT; + SZ_BOT = EXACT; + INC = 1; REPS = 1; } URI _workspaceURI = workspace.getWorkspaceURI(); @@ -96,11 +100,11 @@ public class YakinduTest { boolean modelFound = true; LogicResult solution = null; { - int i = START; - boolean _while = (i <= MAX); + int i = SZ_BOT; + boolean _while = (i <= SZ_TOP); while (_while) { { - final int num = ((i - START) / INC); + 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); @@ -121,6 +125,15 @@ public class YakinduTest { 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; @@ -129,15 +142,24 @@ public class YakinduTest { it.documentationLevel = DocumentationLevel.FULL; it.iteration = iter; it.runtimeLimit = 60; - it.typeScopes.maxNewElements = size; - it.typeScopes.minNewElements = (size - 5); + 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); - Object _get = ((ModelResult) solution).getRepresentation().get(0); - final VampireModel soln = ((VampireModel) _get); int _transformationTime = solution.getStatistics().getTransformationTime(); final double tTime = (_transformationTime / 1000.0); int _solverTime = solution.getStatistics().getSolverTime(); @@ -163,7 +185,7 @@ public class YakinduTest { } int _i = i; i = (_i + INC); - _while = (i <= MAX); + _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 e77449e7..96f343fa 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 97f29b0c..1ca8223d 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 0e320f18..5d6a9ee2 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