From 012e1cbb107110ff0d6381ed186163e399f1dd55 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 21 Oct 2019 17:14:25 -0400 Subject: mid-measurement push --- .../model/Statechart.xmi | 4 + .../model/Statechart1.xmi | 10 + .../model/yakindu_simplified.aird | 448 ++++++++++++--------- .../model/yakindu_simplified.ecore | 5 + .../model/yakindummTPTP.png | Bin 0 -> 1085629 bytes .../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 | 3 +- .../vampire/reasoner/VampireSolver.xtend | 49 ++- .../vampire/reasoner/builder/VampireHandler.xtend | 4 +- .../.VampireAnalyzerConfiguration.xtendbin | Bin 3418 -> 3449 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 10151 -> 10862 bytes .../vampire/reasoner/VampireSolver.java | 91 ++++- .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 19566 -> 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 10682 -> 10682 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 17151 -> 17151 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11037 -> 11037 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3997 -> 3997 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 7804 -> 7782 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../vampire/reasoner/builder/VampireHandler.java | 4 +- .../dslreasoner/vampire/icse/YakinduTest.xtend | 29 +- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 4545 -> 4545 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 6626 -> 6626 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 6201 -> 6201 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 6625 -> 6625 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 8997 -> 8995 bytes .../ecse/dslreasoner/vampire/icse/YakinduTest.java | 32 +- .../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 48 files changed, 439 insertions(+), 240 deletions(-) create mode 100644 Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/Statechart.xmi create mode 100644 Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/Statechart1.xmi create mode 100644 Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindummTPTP.png diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/Statechart.xmi b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/Statechart.xmi new file mode 100644 index 00000000..d76b3929 --- /dev/null +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/Statechart.xmi @@ -0,0 +1,4 @@ + + diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/Statechart1.xmi b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/Statechart1.xmi new file mode 100644 index 00000000..6368cea9 --- /dev/null +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/Statechart1.xmi @@ -0,0 +1,10 @@ + + + + + diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.aird b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.aird index 12aa0f9e..b2216e24 100644 --- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.aird +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.aird @@ -1,31 +1,31 @@ - + yakindu_simplified.ecore - + - + - + - + - + - + - - - + + + @@ -46,7 +46,7 @@ - + @@ -55,7 +55,7 @@ - + @@ -64,7 +64,7 @@ - + @@ -73,7 +73,7 @@ - + @@ -82,7 +82,7 @@ - + @@ -91,16 +91,20 @@ - + + + + + - + @@ -109,7 +113,7 @@ - + @@ -118,7 +122,7 @@ - + @@ -127,7 +131,7 @@ - + @@ -136,7 +140,7 @@ - + @@ -145,7 +149,7 @@ - + @@ -154,7 +158,28 @@ - + + + + + + + + + + + + + + + + + + + + + + @@ -217,8 +242,8 @@ - - + + @@ -234,7 +259,7 @@ - + @@ -287,17 +312,17 @@ - + - + - + - + @@ -330,7 +355,7 @@ - + @@ -346,7 +371,7 @@ - + @@ -361,31 +386,31 @@ - - + + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + italic - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + labelFormat backgroundColor italic @@ -393,26 +418,26 @@ - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + labelFormat backgroundColor foregroundColor @@ -420,290 +445,331 @@ - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor + + + + + + + + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + italic - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + italic - + - - + + labelSize - + labelSize - + - - + + labelSize - + labelSize - + - - + + - + italic - + - + - - + + routingStyle - + italic - + - + - - + + - + italic - + - + - - - + + - + italic - + - + - - - + + - + italic - + - + - - + + - + italic - + - + - + strokeColor size - + labelFormat - + labelFormat - + - + strokeColor size - + labelFormat - + labelFormat - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - - + + - + italic - + - + - - + + - + italic - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - - + + routingStyle - + italic - + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - - - + + + @@ -724,7 +790,7 @@ - + @@ -995,25 +1061,25 @@ - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + italic - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + labelFormat backgroundColor foregroundColor @@ -1022,26 +1088,26 @@ - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + labelFormat backgroundColor foregroundColor @@ -1049,39 +1115,39 @@ - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + labelFormat backgroundColor foregroundColor @@ -1089,190 +1155,190 @@ - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + italic - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + italic - + - - + + labelSize - + labelSize - + - - + + labelSize - + labelSize - + - + - + italic - + - + - + - + italic - + - + - + - + italic - + - + - + - + italic - + - + - + - + italic - + - + - + - + italic - + - + - + - + italic - + - + - + strokeColor size - + labelFormat - + labelFormat - + - + strokeColor size - + labelFormat - + labelFormat - + diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.ecore b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.ecore index 51b0ca5b..5999c4c7 100644 --- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.ecore +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.ecore @@ -37,4 +37,9 @@ + + + + + diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindummTPTP.png b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindummTPTP.png new file mode 100644 index 00000000..cfa34e77 Binary files /dev/null and b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindummTPTP.png differ 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 8225ed58..4e0689cf 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 5d455790..050aa53c 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 db1a37c4..d96ec303 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 32d2213b..e2a84938 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 24c6eca6..04d1d9f3 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 422fad02..94728db2 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 d6bf1d6f..a6531f1c 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 d341af67..d90a1d5f 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 2f552529..7343916e 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 f73dadba..864e293f 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 0b18e8e6..51e6a1c6 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 8dac584b..094211cc 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 ee3df0a3..175c556b 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 96ae5822..dc97888c 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 4c2f1952..1fda24d9 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 @@ -24,7 +24,8 @@ enum BackendSolver { IPROVER, PARADOX, VAMPIRE, - Z3 + Z3, + LOCVAMP //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 9ec08163..042caa86 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 @@ -20,6 +20,7 @@ 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 +import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl class VampireSolver extends LogicReasoner { @@ -128,17 +129,17 @@ class VampireSolver extends LogicReasoner { it.name = "satOut" it.value = satOut ] - it.entries += createRealStatisticEntry => [ + it.entries += createStringStatisticEntry => [ it.name = "satTime" - it.value = Double.parseDouble(satTime) + it.value = satTime ] it.entries += createStringStatisticEntry => [ it.name = "modOut" it.value = modOut ] - it.entries += createRealStatisticEntry => [ + it.entries += createStringStatisticEntry => [ it.name = "modTime" - it.value = Double.parseDouble(modTime) + it.value = modTime ] ] @@ -148,6 +149,7 @@ class VampireSolver extends LogicReasoner { } else { // Start: Solving .tptp problem + println() val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) // Finish: Solving .tptp problem // Start: Vampire -> Logic mapping @@ -159,7 +161,44 @@ class VampireSolver extends LogicReasoner { 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 + + var model = vampSol.generatedModel.confirmations.filter[class == VLSFiniteModelImpl] +// + var modOut = "no" + if(model.length >0){ + modOut = "FiniteModel" + } + + val realModOut=modOut + + + 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 = "-" + ] + it.entries += createStringStatisticEntry => [ + it.name = "satTime" + it.value = "-" + ] + it.entries += createStringStatisticEntry => [ + it.name = "modOut" + it.value = realModOut + ] + it.entries += createStringStatisticEntry => [ + it.name = "modTime" + it.value = (vampSol.solverTime/1000.0).toString + ] + + ] + ] } } return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, 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 6d301442..c277759a 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 @@ -54,7 +54,7 @@ class VampireHandler { val TEMPNAME = "TEMP.tptp" // val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + // "_" + configuration.iteration + ".tptp" - val SOLNNAME = "solution" + "_" + configuration.typeScopes.maxNewElements + "_" + configuration.iteration + + val SOLNNAME = "solution" + "_" + configuration.typeScopes.minNewElements + "_" + configuration.iteration + ".tptp" val PATH = "C:/cygwin64/bin" @@ -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::VAMPIRE) { + if (configuration.solver == BackendSolver::LOCVAMP) { 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 b26c1ded..5c40d767 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 7fedcc30..2d4d0741 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 3e3bd688..4f554956 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 @@ -10,9 +10,11 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolut 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.VLSConfirmations; 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 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; @@ -24,7 +26,6 @@ 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; @@ -34,10 +35,12 @@ 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.Conversions; 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.IterableExtensions; import org.eclipse.xtext.xbase.lib.ListExtensions; import org.eclipse.xtext.xbase.lib.ObjectExtensions; import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @@ -149,28 +152,28 @@ public class VampireSolver extends LogicReasoner { 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) -> { + StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_4 = (StringStatisticEntry it_2) -> { it_2.setName("satTime"); - it_2.setValue(Double.parseDouble(satTime)); + it_2.setValue(satTime); }; - RealStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createRealStatisticEntry, _function_4); + StringStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_1, _function_4); _entries_1.add(_doubleArrow_2); EList _entries_2 = it_1.getEntries(); - StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); + StringStatisticEntry _createStringStatisticEntry_2 = 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); + StringStatisticEntry _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_2, _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) -> { + StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_6 = (StringStatisticEntry it_2) -> { it_2.setName("modTime"); - it_2.setValue(Double.parseDouble(modTime)); + it_2.setValue(modTime); }; - RealStatisticEntry _doubleArrow_4 = ObjectExtensions.operator_doubleArrow(_createRealStatisticEntry_1, _function_6); + StringStatisticEntry _doubleArrow_4 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_3, _function_6); _entries_3.add(_doubleArrow_4); }; Statistics _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStatistics, _function_2); @@ -178,13 +181,77 @@ public class VampireSolver extends LogicReasoner { }; return ObjectExtensions.operator_doubleArrow(_createModelResult, _function); } else { + InputOutput.println(); 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 Function1 _function_1 = (VLSConfirmations it) -> { + Class _class = it.getClass(); + return Boolean.valueOf(Objects.equal(_class, VLSFiniteModelImpl.class)); + }; + Iterable model = IterableExtensions.filter(vampSol.getGeneratedModel().getConfirmations(), _function_1); + String modOut_1 = "no"; + final Iterable _converted_model = (Iterable)model; + int _length = ((Object[])Conversions.unwrapArray(_converted_model, Object.class)).length; + boolean _greaterThan = (_length > 0); + if (_greaterThan) { + modOut_1 = "FiniteModel"; + } + final String realModOut = modOut_1; + ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); + final Procedure1 _function_2 = (ModelResult it) -> { + it.setProblem(null); + EList _representation = it.getRepresentation(); + VampireModel _createVampireModel = this.factory.createVampireModel(); + final Procedure1 _function_3 = (VampireModel it_1) -> { + }; + VampireModel _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVampireModel, _function_3); + _representation.add(_doubleArrow); + it.setTrace(it.getTrace()); + Statistics _createStatistics = this.resultFactory.createStatistics(); + final Procedure1 _function_4 = (Statistics it_1) -> { + it_1.setTransformationTime(((int) transformationTime)); + EList _entries = it_1.getEntries(); + StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_5 = (StringStatisticEntry it_2) -> { + it_2.setName("satOut"); + it_2.setValue("-"); + }; + StringStatisticEntry _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry, _function_5); + _entries.add(_doubleArrow_1); + EList _entries_1 = it_1.getEntries(); + StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_6 = (StringStatisticEntry it_2) -> { + it_2.setName("satTime"); + it_2.setValue("-"); + }; + StringStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_1, _function_6); + _entries_1.add(_doubleArrow_2); + EList _entries_2 = it_1.getEntries(); + StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_7 = (StringStatisticEntry it_2) -> { + it_2.setName("modOut"); + it_2.setValue(realModOut); + }; + StringStatisticEntry _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_2, _function_7); + _entries_2.add(_doubleArrow_3); + EList _entries_3 = it_1.getEntries(); + StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); + final Procedure1 _function_8 = (StringStatisticEntry it_2) -> { + it_2.setName("modTime"); + long _solverTime = vampSol.getSolverTime(); + it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString()); + }; + StringStatisticEntry _doubleArrow_4 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_3, _function_8); + _entries_3.add(_doubleArrow_4); + }; + Statistics _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStatistics, _function_4); + it.setStatistics(_doubleArrow_1); + }; + return ObjectExtensions.operator_doubleArrow(_createModelResult_1, _function_2); } } MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null); 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 8b7f031e..887a3a31 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 1b6e8f80..b4943b57 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 f523f1af..e3b29572 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 30ba1843..50ff7011 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 174c7362..337edcba 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 affa3754..c32ba83f 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 9caad4ea..75e60f21 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 5be67889..d69b41ea 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 192c9d1a..6b91ff7b 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 0495ab53..f23063ea 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 c438f1e5..0de59fdb 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 5fb9b455..6176aca5 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/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java index e32530cb..e9073d82 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,7 +30,7 @@ public class VampireHandler { final String CVC4LOC = (CVC4DIR + CVC4NAME); final String CMD = "cmd /c "; final String TEMPNAME = "TEMP.tptp"; - final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + + final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.minNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + ".tptp"); final String PATH = "C:/cygwin64/bin"; final URI wsURI = workspace.getWorkspaceURI(); @@ -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.VAMPIRE); + boolean _equals = Objects.equal(configuration.solver, BackendSolver.LOCVAMP); 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/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend index 26b91525..f26a1c91 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 @@ -59,12 +59,12 @@ class YakinduTest { // val queries = null println("DSL loaded") - var SZ_TOP = 150 - var SZ_BOT = 150 - var INC = 10 - var REPS = 10 + var SZ_TOP = 25 + var SZ_BOT = 5 + var INC = 5 + var REPS = 5 - val RUNTIME = 300 + val RUNTIME = 60 val EXACT = -1 if (EXACT != -1) { @@ -88,7 +88,9 @@ class YakinduTest { // , // BackendSolver::VAMPIRE // , - BackendSolver::Z3 +// BackendSolver::Z3 +// , + BackendSolver::LOCVAMP ) @@ -163,12 +165,17 @@ class YakinduTest { it.typeScopes.minNewElements = size it.genModel = true - it.server = true - it.solver = BESOLVER + it.server = false + if(it.server){ + it.solver = BESOLVER + } else{ + it.solver = BackendSolver::LOCVAMP + } + // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax - it.contCycleLevel = 5 +// it.contCycleLevel = 5 it.uniquenessDuplicates = false ] @@ -187,11 +194,11 @@ class YakinduTest { 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). + val satTime = (solution.statistics.entries.filter[name == "satTime"].get(0) as StringStatisticEntry). 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). + val modTime = (solution.statistics.entries.filter[name == "modTime"].get(0) as StringStatisticEntry). value writer.append(satOut + ",") 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 5dc01040..1174c9aa 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 e96cf904..369ae25b 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 688908b9..d66e9ca0 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 0d18615c..19872b6a 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 b29e18b1..1e5c3981 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/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java index c2aaee03..c46f75d2 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 @@ -19,7 +19,6 @@ 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; @@ -85,11 +84,11 @@ 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 = 150; - int SZ_BOT = 150; - int INC = 10; - int REPS = 10; - final int RUNTIME = 300; + int SZ_TOP = 25; + int SZ_BOT = 5; + int INC = 5; + int REPS = 5; + final int RUNTIME = 60; final int EXACT = (-1); if ((EXACT != (-1))) { SZ_TOP = EXACT; @@ -98,7 +97,7 @@ public class YakinduTest { REPS = 10; } final ArrayList BACKENDSOLVERS = CollectionLiterals.newArrayList( - BackendSolver.Z3); + BackendSolver.LOCVAMP); String str = ""; for (final BackendSolver solver : BACKENDSOLVERS) { String _str = str; @@ -174,9 +173,12 @@ public class YakinduTest { it.runtimeLimit = RUNTIME; it.typeScopes.minNewElements = size; it.genModel = true; - it.server = true; - it.solver = BESOLVER; - it.contCycleLevel = 5; + it.server = false; + if (it.server) { + it.solver = BESOLVER; + } else { + it.solver = BackendSolver.LOCVAMP; + } it.uniquenessDuplicates = false; }; final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); @@ -201,7 +203,7 @@ public class YakinduTest { 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 String satTime = ((StringStatisticEntry) _get_1).getValue(); final Function1 _function_3 = (StatisticEntry it) -> { String _name_2 = it.getName(); return Boolean.valueOf(Objects.equal(_name_2, "modOut")); @@ -213,13 +215,11 @@ public class YakinduTest { 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(); + final String modTime = ((StringStatisticEntry) _get_3).getValue(); writer.append((satOut + ",")); - String _plus_20 = (Double.valueOf(satTime) + ","); - writer.append(_plus_20); + writer.append((satTime + ",")); writer.append((modOut + ",")); - String _plus_21 = (Double.valueOf(modTime) + ""); - writer.append(_plus_21); + writer.append((modTime + "")); writer.append("\n"); } } 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 b596dc1f..41df0b2f 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 e1434d74..9bf38940 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 50068d97..54f2770d 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