From b3f7c4d7707435803921c4fec2c4d95b3dd45c53 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 20 Feb 2023 20:23:27 +0100 Subject: refactor: split query and partial from store Allows more complicated dependency hiearchies (e.g., use store-query-viatra for testing store-partial) and better separation of test fixtures. --- settings.gradle | 2 + subprojects/store-partial/build.gradle | 7 + .../partial/AnyPartialSymbolInterpretation.java | 13 ++ .../tools/refinery/store/partial/MergeResult.java | 15 ++ .../store/partial/PartialInterpretation.java | 24 +++ .../partial/PartialInterpretationAdapter.java | 20 ++ .../partial/PartialInterpretationBuilder.java | 28 +++ .../partial/PartialInterpretationStoreAdapter.java | 17 ++ .../store/partial/PartialSymbolInterpretation.java | 22 +++ .../internal/PartialInterpretationAdapterImpl.java | 38 ++++ .../internal/PartialInterpretationBuilderImpl.java | 29 +++ .../PartialInterpretationStoreAdapterImpl.java | 37 ++++ .../refinery/store/partial/lifting/DnfLifter.java | 107 +++++++++++ .../refinery/store/partial/lifting/ModalDnf.java | 11 ++ .../store/partial/literal/ModalDnfCallLiteral.java | 37 ++++ .../store/partial/literal/ModalLiteral.java | 45 +++++ .../partial/literal/ModalRelationLiteral.java | 31 ++++ .../refinery/store/partial/literal/Modality.java | 31 ++++ .../store/partial/literal/PartialLiterals.java | 33 ++++ .../partial/literal/PartialRelationLiteral.java | 27 +++ .../partial/representation/AnyPartialFunction.java | 4 + .../partial/representation/AnyPartialSymbol.java | 11 ++ .../partial/representation/PartialFunction.java | 32 ++++ .../partial/representation/PartialRelation.java | 66 +++++++ .../partial/representation/PartialSymbol.java | 12 ++ .../partial/rule/RelationRefinementAction.java | 36 ++++ .../tools/refinery/store/partial/rule/Rule.java | 38 ++++ .../refinery/store/partial/rule/RuleAction.java | 12 ++ .../store/partial/rule/RuleActionExecutor.java | 9 + .../refinery/store/partial/rule/RuleExecutor.java | 34 ++++ .../refinery/store/partial/translator/Advice.java | 155 ++++++++++++++++ .../store/partial/translator/AdviceSlot.java | 25 +++ .../refinery/store/partial/translator/Seed.java | 12 ++ .../store/partial/translator/TranslationUnit.java | 48 +++++ .../translator/typehierarchy/EliminatedType.java | 6 + .../translator/typehierarchy/ExtendedTypeInfo.java | 101 ++++++++++ .../typehierarchy/InferredMayTypeRelationView.java | 19 ++ .../InferredMustTypeRelationView.java | 19 ++ .../translator/typehierarchy/InferredType.java | 30 +++ .../translator/typehierarchy/PreservedType.java | 136 ++++++++++++++ .../typehierarchy/TypeAnalysisResult.java | 4 + .../translator/typehierarchy/TypeAnalyzer.java | 202 ++++++++++++++++++++ .../TypeHierarchyTranslationUnit.java | 52 ++++++ .../partial/translator/typehierarchy/TypeInfo.java | 46 +++++ .../translator/typehierarchy/InferredTypeTest.java | 32 ++++ .../TypeAnalyzerExampleHierarchyTest.java | 204 +++++++++++++++++++++ .../translator/typehierarchy/TypeAnalyzerTest.java | 201 ++++++++++++++++++++ .../typehierarchy/TypeAnalyzerTester.java | 51 ++++++ subprojects/store-query-viatra/build.gradle | 2 +- subprojects/store-query/build.gradle | 7 + .../main/java/tools/refinery/store/query/Dnf.java | 112 +++++++++++ .../tools/refinery/store/query/DnfBuilder.java | 108 +++++++++++ .../java/tools/refinery/store/query/DnfClause.java | 9 + .../java/tools/refinery/store/query/DnfUtils.java | 24 +++ .../refinery/store/query/FunctionalDependency.java | 15 ++ .../tools/refinery/store/query/ModelQuery.java | 11 ++ .../refinery/store/query/ModelQueryAdapter.java | 13 ++ .../refinery/store/query/ModelQueryBuilder.java | 23 +++ .../store/query/ModelQueryStoreAdapter.java | 16 ++ .../tools/refinery/store/query/RelationLike.java | 11 ++ .../java/tools/refinery/store/query/ResultSet.java | 25 +++ .../java/tools/refinery/store/query/Variable.java | 58 ++++++ .../store/query/literal/BooleanLiteral.java | 37 ++++ .../refinery/store/query/literal/CallLiteral.java | 66 +++++++ .../refinery/store/query/literal/CallPolarity.java | 32 ++++ .../store/query/literal/ConstantLiteral.java | 19 ++ .../store/query/literal/DnfCallLiteral.java | 29 +++ .../store/query/literal/EquivalenceLiteral.java | 35 ++++ .../refinery/store/query/literal/Literal.java | 16 ++ .../store/query/literal/LiteralReduction.java | 26 +++ .../refinery/store/query/literal/Literals.java | 11 ++ .../refinery/store/query/literal/PolarLiteral.java | 5 + .../store/query/literal/RelationViewLiteral.java | 24 +++ .../refinery/store/query/view/AnyRelationView.java | 24 +++ .../store/query/view/FilteredRelationView.java | 49 +++++ .../store/query/view/FunctionalRelationView.java | 71 +++++++ .../store/query/view/KeyOnlyRelationView.java | 36 ++++ .../refinery/store/query/view/RelationView.java | 82 +++++++++ .../store/query/view/RelationViewImplication.java | 19 ++ .../query/view/TuplePreservingRelationView.java | 44 +++++ .../store/partial/PartialInterpretation.java | 19 -- .../partial/PartialInterpretationAdapter.java | 9 - .../partial/PartialInterpretationBuilder.java | 9 - .../partial/PartialInterpretationStoreAdapter.java | 9 - .../internal/PartialInterpretationAdapterImpl.java | 24 --- .../internal/PartialInterpretationBuilderImpl.java | 17 -- .../PartialInterpretationStoreAdapterImpl.java | 23 --- .../store/partial/literal/ModalDnfCallLiteral.java | 30 --- .../store/partial/literal/ModalLiteral.java | 45 ----- .../partial/literal/ModalRelationLiteral.java | 31 ---- .../refinery/store/partial/literal/Modality.java | 31 ---- .../store/partial/literal/PartialLiterals.java | 33 ---- .../partial/literal/PartialRelationLiteral.java | 27 --- .../partial/representation/AnyPartialFunction.java | 4 - .../partial/representation/AnyPartialSymbol.java | 11 -- .../partial/representation/PartialFunction.java | 32 ---- .../partial/representation/PartialRelation.java | 66 ------- .../partial/representation/PartialSymbol.java | 12 -- .../translator/typehierarchy/EliminatedType.java | 6 - .../translator/typehierarchy/ExtendedTypeInfo.java | 101 ---------- .../translator/typehierarchy/InferredType.java | 30 --- .../translator/typehierarchy/PreservedType.java | 136 -------------- .../typehierarchy/TypeAnalysisResult.java | 4 - .../translator/typehierarchy/TypeAnalyzer.java | 202 -------------------- .../partial/translator/typehierarchy/TypeInfo.java | 46 ----- .../main/java/tools/refinery/store/query/Dnf.java | 187 ------------------- .../java/tools/refinery/store/query/DnfClause.java | 9 - .../java/tools/refinery/store/query/DnfUtils.java | 24 --- .../refinery/store/query/FunctionalDependency.java | 15 -- .../tools/refinery/store/query/ModelQuery.java | 11 -- .../refinery/store/query/ModelQueryAdapter.java | 13 -- .../refinery/store/query/ModelQueryBuilder.java | 23 --- .../store/query/ModelQueryStoreAdapter.java | 16 -- .../tools/refinery/store/query/RelationLike.java | 11 -- .../java/tools/refinery/store/query/ResultSet.java | 25 --- .../java/tools/refinery/store/query/Variable.java | 58 ------ .../refinery/store/query/literal/CallLiteral.java | 66 ------- .../refinery/store/query/literal/CallPolarity.java | 32 ---- .../store/query/literal/ConstantLiteral.java | 19 -- .../store/query/literal/DnfCallLiteral.java | 23 --- .../store/query/literal/EquivalenceLiteral.java | 27 --- .../refinery/store/query/literal/Literal.java | 12 -- .../refinery/store/query/literal/Literals.java | 11 -- .../refinery/store/query/literal/PolarLiteral.java | 5 - .../store/query/literal/RelationViewLiteral.java | 24 --- .../refinery/store/query/view/AnyRelationView.java | 24 --- .../store/query/view/FilteredRelationView.java | 49 ----- .../store/query/view/FunctionalRelationView.java | 71 ------- .../store/query/view/KeyOnlyRelationView.java | 36 ---- .../refinery/store/query/view/RelationView.java | 82 --------- .../store/query/view/RelationViewImplication.java | 19 -- .../query/view/TuplePreservingRelationView.java | 44 ----- .../translator/typehierarchy/InferredTypeTest.java | 32 ---- .../TypeAnalyzerExampleHierarchyTest.java | 203 -------------------- .../translator/typehierarchy/TypeAnalyzerTest.java | 200 -------------------- .../typehierarchy/TypeAnalyzerTester.java | 51 ------ 136 files changed, 3229 insertions(+), 2380 deletions(-) create mode 100644 subprojects/store-partial/build.gradle create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java create mode 100644 subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java create mode 100644 subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java create mode 100644 subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java create mode 100644 subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java create mode 100644 subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java create mode 100644 subprojects/store-query/build.gradle create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/FunctionalDependency.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretation.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/DnfClause.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/FunctionalDependency.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/ModelQuery.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/RelationLike.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/ResultSet.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/Variable.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/view/AnyRelationView.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java delete mode 100644 subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java delete mode 100644 subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java delete mode 100644 subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java delete mode 100644 subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java diff --git a/settings.gradle b/settings.gradle index 3149380d..94a3c2e6 100644 --- a/settings.gradle +++ b/settings.gradle @@ -7,6 +7,8 @@ include 'language-model' include 'language-semantics' include 'language-web' include 'store' +include 'store-partial' +include 'store-query' include 'store-query-viatra' for (project in rootProject.children) { diff --git a/subprojects/store-partial/build.gradle b/subprojects/store-partial/build.gradle new file mode 100644 index 00000000..cb440d9f --- /dev/null +++ b/subprojects/store-partial/build.gradle @@ -0,0 +1,7 @@ +plugins { + id 'refinery-java-library' +} + +dependencies { + api project(':refinery-store-query') +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java new file mode 100644 index 00000000..b6b1f2be --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java @@ -0,0 +1,13 @@ +package tools.refinery.store.partial; + +import tools.refinery.store.partial.representation.AnyPartialSymbol; + +public sealed interface AnyPartialSymbolInterpretation permits PartialSymbolInterpretation { + PartialInterpretationAdapter getAdapter(); + + AnyPartialSymbol getPartialSymbol(); + + int countUnfinished(); + + int countErrors(); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java new file mode 100644 index 00000000..82414d87 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java @@ -0,0 +1,15 @@ +package tools.refinery.store.partial; + +public enum MergeResult { + UNCHANGED, + REFINED, + REJECTED; + + public MergeResult andAlso(MergeResult other) { + return switch (this) { + case UNCHANGED -> other; + case REFINED -> other == REJECTED ? REJECTED : REFINED; + case REJECTED -> REJECTED; + }; + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java new file mode 100644 index 00000000..d76f8728 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java @@ -0,0 +1,24 @@ +package tools.refinery.store.partial; + +import tools.refinery.store.partial.internal.PartialInterpretationBuilderImpl; +import tools.refinery.store.adapter.ModelAdapterBuilderFactory; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.partial.representation.PartialRelation; + +public final class PartialInterpretation extends ModelAdapterBuilderFactory { + public static final PartialInterpretation ADAPTER = new PartialInterpretation(); + + public static final PartialRelation EXISTS = new PartialRelation("exists", 1); + + public static final PartialRelation EQUALS = new PartialRelation("equals", 1); + + private PartialInterpretation() { + super(PartialInterpretationAdapter.class, PartialInterpretationStoreAdapter.class, PartialInterpretationBuilder.class); + } + + @Override + public PartialInterpretationBuilder createBuilder(ModelStoreBuilder storeBuilder) { + return new PartialInterpretationBuilderImpl(storeBuilder); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java new file mode 100644 index 00000000..b811ae7a --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java @@ -0,0 +1,20 @@ +package tools.refinery.store.partial; + +import tools.refinery.store.adapter.ModelAdapter; +import tools.refinery.store.partial.representation.AnyPartialSymbol; +import tools.refinery.store.partial.representation.PartialSymbol; +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.ResultSet; + +public interface PartialInterpretationAdapter extends ModelAdapter { + @Override + PartialInterpretationStoreAdapter getStoreAdapter(); + + default AnyPartialSymbolInterpretation getPartialInterpretation(AnyPartialSymbol partialSymbol) { + return getPartialInterpretation((PartialSymbol) partialSymbol); + } + + PartialSymbolInterpretation getPartialInterpretation(PartialSymbol partialSymbol); + + ResultSet getLiftedResultSet(Dnf query); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java new file mode 100644 index 00000000..db042466 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java @@ -0,0 +1,28 @@ +package tools.refinery.store.partial; + +import tools.refinery.store.adapter.ModelAdapterBuilder; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.query.Dnf; +import tools.refinery.store.partial.literal.Modality; + +import java.util.Collection; +import java.util.List; + +@SuppressWarnings("UnusedReturnValue") +public interface PartialInterpretationBuilder extends ModelAdapterBuilder { + default PartialInterpretationBuilder liftedQueries(Dnf... liftedQueries) { + return liftedQueries(List.of(liftedQueries)); + } + + default PartialInterpretationBuilder liftedQueries(Collection liftedQueries) { + liftedQueries.forEach(this::liftedQuery); + return this; + } + + PartialInterpretationBuilder liftedQuery(Dnf liftedQuery); + + Dnf lift(Modality modality, Dnf query); + + @Override + PartialInterpretationStoreAdapter createStoreAdapter(ModelStore store); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java new file mode 100644 index 00000000..a1813671 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java @@ -0,0 +1,17 @@ +package tools.refinery.store.partial; + +import tools.refinery.store.adapter.ModelStoreAdapter; +import tools.refinery.store.model.Model; +import tools.refinery.store.partial.representation.AnyPartialSymbol; +import tools.refinery.store.query.Dnf; + +import java.util.Collection; + +public interface PartialInterpretationStoreAdapter extends ModelStoreAdapter { + Collection getPartialSymbols(); + + Collection getLiftedQueries(); + + @Override + PartialInterpretationAdapter createModelAdapter(Model model); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java new file mode 100644 index 00000000..fa9e9216 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java @@ -0,0 +1,22 @@ +package tools.refinery.store.partial; + +import tools.refinery.store.partial.representation.PartialSymbol; +import tools.refinery.store.map.Cursor; +import tools.refinery.store.tuple.Tuple; + +public non-sealed interface PartialSymbolInterpretation extends AnyPartialSymbolInterpretation { + @Override + PartialSymbol getPartialSymbol(); + + A get(Tuple key); + + Cursor getAll(); + + Cursor getAllErrors(); + + MergeResult merge(Tuple key, A value); + + C getConcrete(Tuple key); + + Cursor getAllConcrete(); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java new file mode 100644 index 00000000..c482d8a2 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java @@ -0,0 +1,38 @@ +package tools.refinery.store.partial.internal; + +import tools.refinery.store.model.Model; +import tools.refinery.store.partial.PartialInterpretationAdapter; +import tools.refinery.store.partial.PartialSymbolInterpretation; +import tools.refinery.store.partial.representation.PartialSymbol; +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.ResultSet; + +public class PartialInterpretationAdapterImpl implements PartialInterpretationAdapter { + private final Model model; + private final PartialInterpretationStoreAdapterImpl storeAdapter; + + PartialInterpretationAdapterImpl(Model model, PartialInterpretationStoreAdapterImpl storeAdapter) { + this.model = model; + this.storeAdapter = storeAdapter; + } + + @Override + public Model getModel() { + return model; + } + + @Override + public PartialInterpretationStoreAdapterImpl getStoreAdapter() { + return storeAdapter; + } + + @Override + public PartialSymbolInterpretation getPartialInterpretation(PartialSymbol partialSymbol) { + return null; + } + + @Override + public ResultSet getLiftedResultSet(Dnf query) { + return null; + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java new file mode 100644 index 00000000..5853aeaf --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java @@ -0,0 +1,29 @@ +package tools.refinery.store.partial.internal; + +import tools.refinery.store.adapter.AbstractModelAdapterBuilder; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.partial.PartialInterpretationBuilder; +import tools.refinery.store.partial.literal.Modality; +import tools.refinery.store.query.Dnf; + +public class PartialInterpretationBuilderImpl extends AbstractModelAdapterBuilder implements PartialInterpretationBuilder { + public PartialInterpretationBuilderImpl(ModelStoreBuilder storeBuilder) { + super(storeBuilder); + } + + @Override + public PartialInterpretationBuilder liftedQuery(Dnf liftedQuery) { + return null; + } + + @Override + public Dnf lift(Modality modality, Dnf query) { + return null; + } + + @Override + public PartialInterpretationStoreAdapterImpl createStoreAdapter(ModelStore store) { + return null; + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java new file mode 100644 index 00000000..0486af6e --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java @@ -0,0 +1,37 @@ +package tools.refinery.store.partial.internal; + +import tools.refinery.store.partial.PartialInterpretationStoreAdapter; +import tools.refinery.store.model.Model; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.partial.representation.AnyPartialSymbol; +import tools.refinery.store.query.Dnf; + +import java.util.Collection; + +public class PartialInterpretationStoreAdapterImpl implements PartialInterpretationStoreAdapter { + private final ModelStore store; + + PartialInterpretationStoreAdapterImpl(ModelStore store) { + this.store = store; + } + + @Override + public ModelStore getStore() { + return store; + } + + @Override + public Collection getPartialSymbols() { + return null; + } + + @Override + public Collection getLiftedQueries() { + return null; + } + + @Override + public PartialInterpretationAdapterImpl createModelAdapter(Model model) { + return new PartialInterpretationAdapterImpl(model, this); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java new file mode 100644 index 00000000..1c35b925 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java @@ -0,0 +1,107 @@ +package tools.refinery.store.partial.lifting; + +import org.jetbrains.annotations.Nullable; +import tools.refinery.store.partial.literal.ModalDnfCallLiteral; +import tools.refinery.store.partial.PartialInterpretation; +import tools.refinery.store.partial.literal.ModalRelationLiteral; +import tools.refinery.store.partial.literal.PartialRelationLiteral; +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.DnfBuilder; +import tools.refinery.store.query.DnfClause; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.DnfCallLiteral; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.partial.literal.Modality; +import tools.refinery.store.util.CycleDetectingMapper; + +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; + +public class DnfLifter { + private final CycleDetectingMapper mapper = new CycleDetectingMapper<>(ModalDnf::toString, + this::doLift); + + public Dnf lift(Modality modality, Dnf query) { + return mapper.map(new ModalDnf(modality, query)); + } + + private Dnf doLift(ModalDnf modalDnf) { + var modality = modalDnf.modality(); + var dnf = modalDnf.dnf(); + var builder = Dnf.builder(); + builder.parameters(dnf.getParameters()); + boolean changed = false; + for (var clause : dnf.getClauses()) { + if (liftClause(modality, clause, builder)) { + changed = true; + } + } + if (changed) { + return builder.build(); + } + return dnf; + } + + private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) { + boolean changed = false; + var quantifiedVariables = new HashSet<>(clause.quantifiedVariables()); + var literals = clause.literals(); + var liftedLiterals = new ArrayList(literals.size()); + for (var literal : literals) { + Literal liftedLiteral = liftLiteral(modality, literal); + if (liftedLiteral == null) { + liftedLiteral = literal; + } else { + changed = true; + } + liftedLiterals.add(liftedLiteral); + var variable = isExistsLiteralForVariable(modality, liftedLiteral); + if (variable != null) { + // If we already quantify over the existence of the variable with the expected modality, + // we don't need to insert quantification manually. + quantifiedVariables.remove(variable); + } + } + for (var quantifiedVariable : quantifiedVariables) { + // Quantify over variables that are not already quantified with the expected modality. + liftedLiterals.add(PartialInterpretation.EXISTS.call(CallPolarity.POSITIVE, modality, + List.of(quantifiedVariable))); + } + builder.clause(liftedLiterals); + return changed || !quantifiedVariables.isEmpty(); + } + + @Nullable + private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { + if (literal instanceof ModalRelationLiteral modalRelationLiteral && + modalRelationLiteral.getPolarity() == CallPolarity.POSITIVE && + modalRelationLiteral.getModality() == modality && + modalRelationLiteral.getTarget().equals(PartialInterpretation.EXISTS)) { + return modalRelationLiteral.getArguments().get(0); + } + return null; + } + + @Nullable + private Literal liftLiteral(Modality modality, Literal literal) { + if (literal instanceof PartialRelationLiteral partialRelationLiteral) { + return new ModalRelationLiteral(modality, partialRelationLiteral); + } else if (literal instanceof DnfCallLiteral dnfCallLiteral) { + var polarity = dnfCallLiteral.getPolarity(); + var target = dnfCallLiteral.getTarget(); + var liftedTarget = lift(modality.commute(polarity), target); + if (target.equals(liftedTarget)) { + return null; + } + return new DnfCallLiteral(polarity, liftedTarget, dnfCallLiteral.getArguments()); + } else if (literal instanceof ModalDnfCallLiteral modalDnfCallLiteral) { + var liftedTarget = lift(modalDnfCallLiteral.getModality(), modalDnfCallLiteral.getTarget()); + return new DnfCallLiteral(modalDnfCallLiteral.getPolarity(), liftedTarget, + modalDnfCallLiteral.getArguments()); + } else { + return null; + } + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java new file mode 100644 index 00000000..6fe54ad9 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java @@ -0,0 +1,11 @@ +package tools.refinery.store.partial.lifting; + +import tools.refinery.store.query.Dnf; +import tools.refinery.store.partial.literal.Modality; + +public record ModalDnf(Modality modality, Dnf dnf) { + @Override + public String toString() { + return "%s %s".formatted(modality, dnf.name()); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java new file mode 100644 index 00000000..a49e0625 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java @@ -0,0 +1,37 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.DnfCallLiteral; +import tools.refinery.store.query.literal.LiteralReduction; +import tools.refinery.store.query.literal.PolarLiteral; + +import java.util.List; +import java.util.Map; + +public class ModalDnfCallLiteral extends ModalLiteral implements PolarLiteral { + public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List arguments) { + super(polarity, modality, target, arguments); + } + + public ModalDnfCallLiteral(Modality modality, DnfCallLiteral baseLiteral) { + super(modality.commute(baseLiteral.getPolarity()), baseLiteral); + } + + @Override + public ModalDnfCallLiteral substitute(Map substitution) { + return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); + } + + @Override + public ModalDnfCallLiteral negate() { + return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); + } + + @Override + public LiteralReduction getReduction() { + var dnfReduction = getTarget().getReduction(); + return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate(); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java new file mode 100644 index 00000000..a1b6c83e --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java @@ -0,0 +1,45 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.query.RelationLike; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallLiteral; +import tools.refinery.store.query.literal.CallPolarity; + +import java.util.List; +import java.util.Objects; + +public abstract class ModalLiteral extends CallLiteral { + private final Modality modality; + + protected ModalLiteral(CallPolarity polarity, Modality modality, T target, List arguments) { + super(polarity, target, arguments); + this.modality = modality; + } + + protected ModalLiteral(Modality modality, CallLiteral baseLiteral) { + this(baseLiteral.getPolarity(), commute(modality, baseLiteral.getPolarity()), baseLiteral.getTarget(), + baseLiteral.getArguments()); + } + + public Modality getModality() { + return modality; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + if (!super.equals(o)) return false; + ModalLiteral that = (ModalLiteral) o; + return modality == that.modality; + } + + @Override + public int hashCode() { + return Objects.hash(super.hashCode(), modality); + } + + private static Modality commute(Modality modality, CallPolarity polarity) { + return polarity.isPositive() ? modality : modality.negate(); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java new file mode 100644 index 00000000..dbaa524f --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java @@ -0,0 +1,31 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.PolarLiteral; + +import java.util.List; +import java.util.Map; + +public final class ModalRelationLiteral extends ModalLiteral + implements PolarLiteral { + public ModalRelationLiteral(CallPolarity polarity, Modality modality, PartialRelation target, + List arguments) { + super(polarity, modality, target, arguments); + } + + public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) { + super(modality, baseLiteral); + } + + @Override + public ModalRelationLiteral substitute(Map substitution) { + return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); + } + + @Override + public ModalRelationLiteral negate() { + return new ModalRelationLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java new file mode 100644 index 00000000..d647ef0a --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java @@ -0,0 +1,31 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.query.literal.CallPolarity; + +import java.util.Locale; + +public enum Modality { + MUST, + MAY, + CURRENT; + + public Modality negate() { + return switch(this) { + case MUST -> MAY; + case MAY -> MUST; + case CURRENT -> CURRENT; + }; + } + + public Modality commute(CallPolarity polarity) { + if (polarity.isPositive()) { + return this; + } + return this.negate(); + } + + @Override + public String toString() { + return name().toLowerCase(Locale.ROOT); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java new file mode 100644 index 00000000..51d388d3 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java @@ -0,0 +1,33 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.query.literal.DnfCallLiteral; + +public final class PartialLiterals { + private PartialLiterals() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public ModalRelationLiteral may(PartialRelationLiteral literal) { + return new ModalRelationLiteral(Modality.MAY, literal); + } + + public ModalRelationLiteral must(PartialRelationLiteral literal) { + return new ModalRelationLiteral(Modality.MUST, literal); + } + + public ModalRelationLiteral current(PartialRelationLiteral literal) { + return new ModalRelationLiteral(Modality.CURRENT, literal); + } + + public ModalDnfCallLiteral may(DnfCallLiteral literal) { + return new ModalDnfCallLiteral(Modality.MAY, literal); + } + + public ModalDnfCallLiteral must(DnfCallLiteral literal) { + return new ModalDnfCallLiteral(Modality.MUST, literal); + } + + public ModalDnfCallLiteral current(DnfCallLiteral literal) { + return new ModalDnfCallLiteral(Modality.CURRENT, literal); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java new file mode 100644 index 00000000..dc1a1da3 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java @@ -0,0 +1,27 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallLiteral; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.PolarLiteral; + +import java.util.List; +import java.util.Map; + +public final class PartialRelationLiteral extends CallLiteral + implements PolarLiteral { + public PartialRelationLiteral(CallPolarity polarity, PartialRelation target, List substitution) { + super(polarity, target, substitution); + } + + @Override + public PartialRelationLiteral substitute(Map substitution) { + return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); + } + + @Override + public PartialRelationLiteral negate() { + return new PartialRelationLiteral(getPolarity().negate(), getTarget(), getArguments()); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java new file mode 100644 index 00000000..1113245e --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java @@ -0,0 +1,4 @@ +package tools.refinery.store.partial.representation; + +public sealed interface AnyPartialFunction extends AnyPartialSymbol permits PartialFunction { +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java new file mode 100644 index 00000000..25096e74 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java @@ -0,0 +1,11 @@ +package tools.refinery.store.partial.representation; + +import tools.refinery.store.representation.AnyAbstractDomain; + +public sealed interface AnyPartialSymbol permits AnyPartialFunction, PartialSymbol { + String name(); + + int arity(); + + AnyAbstractDomain abstractDomain(); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java new file mode 100644 index 00000000..3c186f6f --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java @@ -0,0 +1,32 @@ +package tools.refinery.store.partial.representation; + +import tools.refinery.store.representation.AbstractDomain; + +public record PartialFunction(String name, int arity, AbstractDomain abstractDomain) + implements AnyPartialFunction, PartialSymbol { + @Override + public A defaultValue() { + return null; + } + + @Override + public C defaultConcreteValue() { + return null; + } + + @Override + public boolean equals(Object o) { + return this == o; + } + + @Override + public int hashCode() { + // Compare by identity to make hash table lookups more efficient. + return System.identityHashCode(this); + } + + @Override + public String toString() { + return "%s/%d".formatted(name, arity); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java new file mode 100644 index 00000000..51c2f28d --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java @@ -0,0 +1,66 @@ +package tools.refinery.store.partial.representation; + +import tools.refinery.store.partial.literal.Modality; +import tools.refinery.store.partial.literal.PartialRelationLiteral; +import tools.refinery.store.partial.literal.ModalRelationLiteral; +import tools.refinery.store.query.RelationLike; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.representation.AbstractDomain; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.representation.TruthValueDomain; + +import java.util.List; + +public record PartialRelation(String name, int arity) implements PartialSymbol, RelationLike { + @Override + public AbstractDomain abstractDomain() { + return TruthValueDomain.INSTANCE; + } + + @Override + public TruthValue defaultValue() { + return TruthValue.FALSE; + } + + @Override + public Boolean defaultConcreteValue() { + return false; + } + + public ModalRelationLiteral call(CallPolarity polarity, Modality modality, List arguments) { + return new ModalRelationLiteral(polarity, modality, this, arguments); + } + + public PartialRelationLiteral call(CallPolarity polarity, List arguments) { + return new PartialRelationLiteral(polarity, this, arguments); + } + + public PartialRelationLiteral call(CallPolarity polarity, Variable... arguments) { + return call(polarity, List.of(arguments)); + } + + public PartialRelationLiteral call(Variable... arguments) { + return call(CallPolarity.POSITIVE, arguments); + } + + public PartialRelationLiteral callTransitive(Variable left, Variable right) { + return call(CallPolarity.TRANSITIVE, List.of(left, right)); + } + + @Override + public boolean equals(Object o) { + return this == o; + } + + @Override + public int hashCode() { + // Compare by identity to make hash table lookups more efficient. + return System.identityHashCode(this); + } + + @Override + public String toString() { + return "%s/%d".formatted(name, arity); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java new file mode 100644 index 00000000..38533fa9 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java @@ -0,0 +1,12 @@ +package tools.refinery.store.partial.representation; + +import tools.refinery.store.representation.AbstractDomain; + +public sealed interface PartialSymbol extends AnyPartialSymbol permits PartialFunction, PartialRelation { + @Override + AbstractDomain abstractDomain(); + + A defaultValue(); + + C defaultConcreteValue(); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java new file mode 100644 index 00000000..6c89653d --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java @@ -0,0 +1,36 @@ +package tools.refinery.store.partial.rule; + +import tools.refinery.store.partial.PartialInterpretation; +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.Variable; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.tuple.Tuple; + +import java.util.List; + +public record RelationRefinementAction(PartialRelation target, List arguments, TruthValue value) + implements RuleAction { + public RelationRefinementAction { + if (arguments.size() != target.arity()) { + throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(), + target.arity(), arguments.size())); + } + if (value == TruthValue.UNKNOWN) { + throw new IllegalArgumentException("Refining with UNKNOWN has no effect"); + } + } + + @Override + public RuleActionExecutor createExecutor(int[] argumentIndices, Model model) { + var targetInterpretation = model.getAdapter(PartialInterpretation.ADAPTER).getPartialInterpretation(target); + return activationTuple -> { + int arity = argumentIndices.length; + var arguments = new int[arity]; + for (int i = 0; i < arity; i++) { + arguments[i] = activationTuple.get(argumentIndices[i]); + } + return targetInterpretation.merge(Tuple.of(arguments), value); + }; + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java new file mode 100644 index 00000000..c114b8cf --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java @@ -0,0 +1,38 @@ +package tools.refinery.store.partial.rule; + +import tools.refinery.store.model.Model; +import tools.refinery.store.query.Dnf; + +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; + +public record Rule(Dnf precondition, List actions) { + public Rule { + var parameterSet = new HashSet<>(precondition.getParameters()); + for (var action : actions) { + for (var argument : action.arguments()) { + if (!parameterSet.contains(argument)) { + throw new IllegalArgumentException( + "Argument %s of action %s does not appear in the parameter list %s of %s" + .formatted(argument, action, precondition.getParameters(), precondition.name())); + } + } + } + } + + public RuleExecutor createExecutor(Model model) { + var parameters = precondition.getParameters(); + var actionExecutors = new ArrayList(actions.size()); + for (var action : actions) { + var arguments = action.arguments(); + int arity = arguments.size(); + var argumentIndices = new int[arity]; + for (int i = 0; i < arity; i++) { + argumentIndices[i] = parameters.indexOf(arguments.get(i)); + } + actionExecutors.add(action.createExecutor(argumentIndices, model)); + } + return new RuleExecutor(this, model, actionExecutors); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java new file mode 100644 index 00000000..7a8ede40 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java @@ -0,0 +1,12 @@ +package tools.refinery.store.partial.rule; + +import tools.refinery.store.model.Model; +import tools.refinery.store.query.Variable; + +import java.util.List; + +public interface RuleAction { + List arguments(); + + RuleActionExecutor createExecutor(int[] argumentIndices, Model model); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java new file mode 100644 index 00000000..1c2db5f1 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java @@ -0,0 +1,9 @@ +package tools.refinery.store.partial.rule; + +import tools.refinery.store.partial.MergeResult; +import tools.refinery.store.tuple.TupleLike; + +@FunctionalInterface +public interface RuleActionExecutor { + MergeResult execute(TupleLike activationTuple); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java new file mode 100644 index 00000000..41d79306 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java @@ -0,0 +1,34 @@ +package tools.refinery.store.partial.rule; + +import tools.refinery.store.partial.MergeResult; +import tools.refinery.store.model.Model; +import tools.refinery.store.tuple.TupleLike; + +import java.util.List; + +public final class RuleExecutor { + private final Rule rule; + private final Model model; + private final List actionExecutors; + + RuleExecutor(Rule rule, Model model, List actionExecutors) { + this.rule = rule; + this.model = model; + this.actionExecutors = actionExecutors; + } + + public Rule getRule() { + return rule; + } + + public Model getModel() { + return model; + } + public MergeResult execute(TupleLike activationTuple) { + MergeResult mergeResult = MergeResult.UNCHANGED; + for (var actionExecutor : actionExecutors) { + mergeResult = mergeResult.andAlso(actionExecutor.execute(activationTuple)); + } + return mergeResult; + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java new file mode 100644 index 00000000..65040a8e --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java @@ -0,0 +1,155 @@ +package tools.refinery.store.partial.translator; + +import tools.refinery.store.partial.representation.AnyPartialSymbol; +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.Literal; + +import java.util.*; + +public final class Advice { + private final AnyPartialSymbol source; + private final PartialRelation target; + private final AdviceSlot slot; + private final boolean mandatory; + private final List parameters; + private final List literals; + private boolean processed; + + public Advice(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot, boolean mandatory, List parameters, List literals) { + if (mandatory && !slot.isMonotonic()) { + throw new IllegalArgumentException("Only monotonic advice can be mandatory"); + } + this.source = source; + this.target = target; + this.slot = slot; + this.mandatory = mandatory; + checkArity(parameters); + this.parameters = parameters; + this.literals = literals; + } + + public AnyPartialSymbol source() { + return source; + } + + public PartialRelation target() { + return target; + } + + public AdviceSlot slot() { + return slot; + } + + public boolean mandatory() { + return mandatory; + } + + public List parameters() { + return parameters; + } + + public List literals() { + return literals; + } + + public boolean processed() { + return processed; + } + + public List substitute(List substituteParameters) { + checkArity(substituteParameters); + markProcessed(); + int arity = parameters.size(); + var substitution = new HashMap(arity); + for (int i = 0; i < arity; i++) { + substitution.put(parameters.get(i), substituteParameters.get(i)); + } + return literals.stream().map(literal -> literal.substitute(substitution)).toList(); + } + + private void markProcessed() { + processed = true; + } + + public void checkProcessed() { + if (mandatory && !processed) { + throw new IllegalStateException("Mandatory advice %s was not processed".formatted(this)); + } + } + + private void checkArity(List toCheck) { + if (toCheck.size() != target.arity()) { + throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(), + target.arity(), parameters.size())); + } + } + + public static Builder builderFor(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) { + return new Builder(source, target, slot); + } + + + @Override + public String toString() { + return "Advice[source=%s, target=%s, slot=%s, mandatory=%s, parameters=%s, literals=%s]".formatted(source, + target, slot, mandatory, parameters, literals); + } + + public static class Builder { + private final AnyPartialSymbol source; + private final PartialRelation target; + private final AdviceSlot slot; + private boolean mandatory; + private final List parameters = new ArrayList<>(); + private final List literals = new ArrayList<>(); + + private Builder(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) { + this.source = source; + this.target = target; + this.slot = slot; + } + + public Builder mandatory(boolean mandatory) { + this.mandatory = mandatory; + return this; + } + + public Builder mandatory() { + return mandatory(false); + } + + public Builder parameters(List variables) { + parameters.addAll(variables); + return this; + } + + public Builder parameters(Variable... variables) { + return parameters(List.of(variables)); + } + + public Builder parameter(Variable variable) { + parameters.add(variable); + return this; + } + + public Builder literals(Collection literals) { + this.literals.addAll(literals); + return this; + } + + public Builder literals(Literal... literals) { + return literals(List.of(literals)); + } + + public Builder literal(Literal literal) { + literals.add(literal); + return this; + } + + public Advice build() { + return new Advice(source, target, slot, mandatory, Collections.unmodifiableList(parameters), + Collections.unmodifiableList(literals)); + } + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java new file mode 100644 index 00000000..3702a8ac --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java @@ -0,0 +1,25 @@ +package tools.refinery.store.partial.translator; + +import tools.refinery.store.representation.TruthValue; + +public enum AdviceSlot { + EXTEND_MUST(true), + + RESTRICT_MAY(true), + + /** + * Same as {@link #RESTRICT_MAY}, but only active if the value of the relation is not {@link TruthValue#TRUE} or + * {@link TruthValue#ERROR}. + */ + RESTRICT_NEW(false); + + private final boolean monotonic; + + AdviceSlot(boolean monotonic) { + this.monotonic = monotonic; + } + + public boolean isMonotonic() { + return monotonic; + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java new file mode 100644 index 00000000..c56b06ed --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java @@ -0,0 +1,12 @@ +package tools.refinery.store.partial.translator; + +import tools.refinery.store.map.Cursor; +import tools.refinery.store.tuple.Tuple; + +public interface Seed { + int arity(); + + T get(Tuple key); + + Cursor getCursor(T defaultValue, int nodeCount); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java new file mode 100644 index 00000000..26bd909b --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java @@ -0,0 +1,48 @@ +package tools.refinery.store.partial.translator; + +import tools.refinery.store.partial.PartialInterpretationBuilder; +import tools.refinery.store.model.Model; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.partial.AnyPartialSymbolInterpretation; +import tools.refinery.store.partial.literal.Modality; +import tools.refinery.store.partial.representation.AnyPartialSymbol; +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.Literal; + +import java.util.Collection; +import java.util.List; +import java.util.Map; + +public abstract class TranslationUnit { + private PartialInterpretationBuilder partialInterpretationBuilder; + + protected PartialInterpretationBuilder getPartialInterpretationBuilder() { + return partialInterpretationBuilder; + } + + public void setPartialInterpretationBuilder(PartialInterpretationBuilder partialInterpretationBuilder) { + this.partialInterpretationBuilder = partialInterpretationBuilder; + } + + protected ModelStoreBuilder getModelStoreBuilder() { + return partialInterpretationBuilder.getStoreBuilder(); + } + + public abstract Collection getTranslatedPartialSymbols(); + + public Collection computeAdvices() { + // No advices to give by default. + return List.of(); + } + + public abstract void configure(Collection advices); + + public abstract List call(CallPolarity polarity, Modality modality, PartialRelation target, + List arguments); + + public abstract Map createPartialInterpretations(Model model); + + public abstract void initializeModel(Model model, int nodeCount); +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java new file mode 100644 index 00000000..9adf6bc8 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java @@ -0,0 +1,6 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import tools.refinery.store.partial.representation.PartialRelation; + +record EliminatedType(PartialRelation replacement) implements TypeAnalysisResult { +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java new file mode 100644 index 00000000..d3f66a4c --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java @@ -0,0 +1,101 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import org.jetbrains.annotations.NotNull; +import tools.refinery.store.partial.representation.PartialRelation; + +import java.util.HashSet; +import java.util.LinkedHashSet; +import java.util.Objects; +import java.util.Set; + +final class ExtendedTypeInfo implements Comparable { + private final int index; + private final PartialRelation type; + private final TypeInfo typeInfo; + private final Set allSubtypes = new LinkedHashSet<>(); + private final Set allSupertypes; + private final Set concreteSubtypesAndSelf = new LinkedHashSet<>(); + private Set directSubtypes; + private final Set unsortedDirectSupertypes = new HashSet<>(); + + public ExtendedTypeInfo(int index, PartialRelation type, TypeInfo typeInfo) { + this.index = index; + this.type = type; + this.typeInfo = typeInfo; + this.allSupertypes = new LinkedHashSet<>(typeInfo.supertypes()); + } + + public PartialRelation getType() { + return type; + } + + public TypeInfo getTypeInfo() { + return typeInfo; + } + + public boolean isAbstractType() { + return getTypeInfo().abstractType(); + } + + public Set getAllSubtypes() { + return allSubtypes; + } + + public Set getAllSupertypes() { + return allSupertypes; + } + + public Set getAllSupertypesAndSelf() { + var allSubtypesAndSelf = new HashSet(allSupertypes.size() + 1); + addMust(allSubtypesAndSelf); + return allSubtypesAndSelf; + } + + public Set getConcreteSubtypesAndSelf() { + return concreteSubtypesAndSelf; + } + + public Set getDirectSubtypes() { + return directSubtypes; + } + + public Set getUnsortedDirectSupertypes() { + return unsortedDirectSupertypes; + } + + public void setDirectSubtypes(Set directSubtypes) { + this.directSubtypes = directSubtypes; + } + + public boolean allowsAllConcreteTypes(Set concreteTypes) { + for (var concreteType : concreteTypes) { + if (!concreteSubtypesAndSelf.contains(concreteType)) { + return false; + } + } + return true; + } + + public void addMust(Set mustTypes) { + mustTypes.add(type); + mustTypes.addAll(allSupertypes); + } + + @Override + public int compareTo(@NotNull ExtendedTypeInfo extendedTypeInfo) { + return Integer.compare(index, extendedTypeInfo.index); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + ExtendedTypeInfo that = (ExtendedTypeInfo) o; + return index == that.index; + } + + @Override + public int hashCode() { + return Objects.hash(index); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java new file mode 100644 index 00000000..ff761936 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java @@ -0,0 +1,19 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.query.view.TuplePreservingRelationView; +import tools.refinery.store.tuple.Tuple; + +class InferredMayTypeRelationView extends TuplePreservingRelationView { + private final PartialRelation type; + + InferredMayTypeRelationView(PartialRelation type) { + super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#may".formatted(type)); + this.type = type; + } + + @Override + public boolean filter(Tuple key, InferredType value) { + return value.mayConcreteTypes().contains(type); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java new file mode 100644 index 00000000..4eca0a1c --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java @@ -0,0 +1,19 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.query.view.TuplePreservingRelationView; +import tools.refinery.store.tuple.Tuple; + +class InferredMustTypeRelationView extends TuplePreservingRelationView { + private final PartialRelation type; + + InferredMustTypeRelationView(PartialRelation type) { + super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#must".formatted(type)); + this.type = type; + } + + @Override + public boolean filter(Tuple key, InferredType value) { + return value.mustTypes().contains(type); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java new file mode 100644 index 00000000..729b1fb5 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java @@ -0,0 +1,30 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import tools.refinery.store.partial.representation.PartialRelation; + +import java.util.Collections; +import java.util.Set; + +record InferredType(Set mustTypes, Set mayConcreteTypes, + PartialRelation currentType) { + public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null); + + public InferredType(Set mustTypes, Set mayConcreteTypes, + PartialRelation currentType) { + this.mustTypes = Collections.unmodifiableSet(mustTypes); + this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes); + this.currentType = currentType; + } + + public boolean isConsistent() { + return currentType != null || mustTypes.isEmpty(); + } + + public boolean isMust(PartialRelation partialRelation) { + return mustTypes.contains(partialRelation); + } + + public boolean isMayConcrete(PartialRelation partialRelation) { + return mayConcreteTypes.contains(partialRelation); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java new file mode 100644 index 00000000..0299ae03 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java @@ -0,0 +1,136 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.representation.TruthValue; + +import java.util.*; + +final class PreservedType implements TypeAnalysisResult { + private final ExtendedTypeInfo extendedTypeInfo; + private final List directSubtypes; + private final List allExternalTypeInfoList; + private final InferredType inferredType; + + public PreservedType(ExtendedTypeInfo extendedTypeInfo, List allExternalTypeInfoList) { + this.extendedTypeInfo = extendedTypeInfo; + directSubtypes = List.copyOf(extendedTypeInfo.getDirectSubtypes()); + this.allExternalTypeInfoList = allExternalTypeInfoList; + inferredType = propagateMust(extendedTypeInfo.getAllSupertypesAndSelf(), + extendedTypeInfo.getConcreteSubtypesAndSelf()); + } + + public PartialRelation type() { + return extendedTypeInfo.getType(); + } + + public List getDirectSubtypes() { + return directSubtypes; + } + + public boolean isAbstractType() { + return extendedTypeInfo.isAbstractType(); + } + + public boolean isVacuous() { + return isAbstractType() && directSubtypes.isEmpty(); + } + + public InferredType asInferredType() { + return inferredType; + } + + public InferredType merge(InferredType inferredType, TruthValue value) { + return switch (value) { + case UNKNOWN -> inferredType; + case TRUE -> addMust(inferredType); + case FALSE -> removeMay(inferredType); + case ERROR -> addError(inferredType); + }; + } + + private InferredType addMust(InferredType inferredType) { + var originalMustTypes = inferredType.mustTypes(); + if (originalMustTypes.contains(type())) { + return inferredType; + } + var mustTypes = new HashSet<>(originalMustTypes); + extendedTypeInfo.addMust(mustTypes); + var originalMayConcreteTypes = inferredType.mayConcreteTypes(); + var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); + Set mayConcreteTypesResult; + if (mayConcreteTypes.retainAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { + mayConcreteTypesResult = mayConcreteTypes; + } else { + mayConcreteTypesResult = originalMayConcreteTypes; + } + return propagateMust(mustTypes, mayConcreteTypesResult); + } + + private InferredType removeMay(InferredType inferredType) { + var originalMayConcreteTypes = inferredType.mayConcreteTypes(); + var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); + if (!mayConcreteTypes.removeAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { + return inferredType; + } + return propagateMust(inferredType.mustTypes(), mayConcreteTypes); + } + + private InferredType addError(InferredType inferredType) { + var originalMustTypes = inferredType.mustTypes(); + if (originalMustTypes.contains(type())) { + if (inferredType.mayConcreteTypes().isEmpty()) { + return inferredType; + } + return new InferredType(originalMustTypes, Set.of(), null); + } + var mustTypes = new HashSet<>(originalMustTypes); + extendedTypeInfo.addMust(mustTypes); + return new InferredType(mustTypes, Set.of(), null); + } + + private InferredType propagateMust(Set originalMustTypes, + Set mayConcreteTypes) { + // It is possible that there is not type at all, do not force one by propagation. + var maybeUntyped = originalMustTypes.isEmpty(); + // Para-consistent case, do not propagate must types to avoid logical explosion. + var paraConsistentOrSurelyUntyped = mayConcreteTypes.isEmpty(); + if (maybeUntyped || paraConsistentOrSurelyUntyped) { + return new InferredType(originalMustTypes, mayConcreteTypes, null); + } + var currentType = computeCurrentType(mayConcreteTypes); + var mustTypes = new HashSet<>(originalMustTypes); + boolean changed = false; + for (var newMustExtendedTypeInfo : allExternalTypeInfoList) { + var newMustType = newMustExtendedTypeInfo.getType(); + if (mustTypes.contains(newMustType)) { + continue; + } + if (newMustExtendedTypeInfo.allowsAllConcreteTypes(mayConcreteTypes)) { + newMustExtendedTypeInfo.addMust(mustTypes); + changed = true; + } + } + if (!changed) { + return new InferredType(originalMustTypes, mayConcreteTypes, currentType); + } + return new InferredType(mustTypes, mayConcreteTypes, currentType); + } + + /** + * Returns a concrete type that is allowed by a (consistent, i.e., nonempty) set of may concrete types. + * + * @param mayConcreteTypes The set of allowed concrete types. Must not be empty. + * @return The first concrete type that is allowed by {@code matConcreteTypes}. + */ + private PartialRelation computeCurrentType(Set mayConcreteTypes) { + for (var concreteExtendedTypeInfo : allExternalTypeInfoList) { + var concreteType = concreteExtendedTypeInfo.getType(); + if (!concreteExtendedTypeInfo.isAbstractType() && mayConcreteTypes.contains(concreteType)) { + return concreteType; + } + } + // We have already filtered out the para-consistent case in {@link #propagateMust(Set, + // Set}. + throw new AssertionError("No concrete type in %s".formatted(mayConcreteTypes)); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java new file mode 100644 index 00000000..0745f84e --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java @@ -0,0 +1,4 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +sealed interface TypeAnalysisResult permits EliminatedType, PreservedType { +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java new file mode 100644 index 00000000..062b4c49 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java @@ -0,0 +1,202 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import tools.refinery.store.partial.representation.PartialRelation; + +import java.util.*; + +class TypeAnalyzer { + private final Map extendedTypeInfoMap; + private final Map replacements = new LinkedHashMap<>(); + private final InferredType unknownType; + private final Map analysisResults; + + public TypeAnalyzer(Map typeInfoMap) { + int size = typeInfoMap.size(); + extendedTypeInfoMap = new LinkedHashMap<>(size); + var concreteTypes = new LinkedHashSet(); + int index = 0; + for (var entry : typeInfoMap.entrySet()) { + var type = entry.getKey(); + var typeInfo = entry.getValue(); + extendedTypeInfoMap.put(type, new ExtendedTypeInfo(index, type, typeInfo)); + if (!typeInfo.abstractType()) { + concreteTypes.add(type); + } + index++; + } + unknownType = new InferredType(Set.of(), concreteTypes, null); + computeAllSupertypes(); + computeAllAndConcreteSubtypes(); + computeDirectSubtypes(); + eliminateTrivialSupertypes(); + analysisResults = computeAnalysisResults(); + } + + public InferredType getUnknownType() { + return unknownType; + } + + public Map getAnalysisResults() { + return analysisResults; + } + + private void computeAllSupertypes() { + boolean changed; + do { + changed = false; + for (var extendedTypeInfo : extendedTypeInfoMap.values()) { + var found = new HashSet(); + var allSupertypes = extendedTypeInfo.getAllSupertypes(); + for (var supertype : allSupertypes) { + found.addAll(extendedTypeInfoMap.get(supertype).getAllSupertypes()); + } + if (allSupertypes.addAll(found)) { + changed = true; + } + } + } while (changed); + } + + private void computeAllAndConcreteSubtypes() { + for (var extendedTypeInfo : extendedTypeInfoMap.values()) { + var type = extendedTypeInfo.getType(); + if (!extendedTypeInfo.isAbstractType()) { + extendedTypeInfo.getConcreteSubtypesAndSelf().add(type); + } + for (var supertype : extendedTypeInfo.getAllSupertypes()) { + if (type.equals(supertype)) { + throw new IllegalArgumentException("%s cannot be a supertype of itself".formatted(type)); + } + var supertypeInfo = extendedTypeInfoMap.get(supertype); + supertypeInfo.getAllSubtypes().add(type); + if (!extendedTypeInfo.isAbstractType()) { + supertypeInfo.getConcreteSubtypesAndSelf().add(type); + } + } + } + } + + private void computeDirectSubtypes() { + for (var extendedTypeInfo : extendedTypeInfoMap.values()) { + var allSubtypes = extendedTypeInfo.getAllSubtypes(); + var directSubtypes = new LinkedHashSet<>(allSubtypes); + var indirectSubtypes = new LinkedHashSet(allSubtypes.size()); + for (var subtype : allSubtypes) { + indirectSubtypes.addAll(extendedTypeInfoMap.get(subtype).getAllSubtypes()); + } + directSubtypes.removeAll(indirectSubtypes); + extendedTypeInfo.setDirectSubtypes(directSubtypes); + } + } + + private void eliminateTrivialSupertypes() { + boolean changed; + do { + var toRemove = new ArrayList(); + for (var entry : extendedTypeInfoMap.entrySet()) { + var extendedTypeInfo = entry.getValue(); + boolean isAbstract = extendedTypeInfo.isAbstractType(); + // Do not eliminate abstract types with 0 subtypes, because they can be used para-consistently, i.e., + // an object determined to must have an abstract type with 0 subtypes may not ever exist. + boolean hasSingleDirectSubtype = extendedTypeInfo.getDirectSubtypes().size() == 1; + if (isAbstract && hasSingleDirectSubtype) { + toRemove.add(entry.getKey()); + } + } + toRemove.forEach(this::removeTrivialType); + changed = !toRemove.isEmpty(); + } while (changed); + } + + private void removeTrivialType(PartialRelation trivialType) { + var extendedTypeInfo = extendedTypeInfoMap.get(trivialType); + var iterator = extendedTypeInfo.getDirectSubtypes().iterator(); + if (!iterator.hasNext()) { + throw new AssertionError("Expected trivial supertype %s to have a direct subtype" + .formatted(trivialType)); + } + PartialRelation replacement = setReplacement(trivialType, iterator.next()); + if (iterator.hasNext()) { + throw new AssertionError("Expected trivial supertype %s to have at most 1 direct subtype" + .formatted(trivialType)); + } + replacements.put(trivialType, replacement); + for (var supertype : extendedTypeInfo.getAllSupertypes()) { + var extendedSupertypeInfo = extendedTypeInfoMap.get(supertype); + if (!extendedSupertypeInfo.getAllSubtypes().remove(trivialType)) { + throw new AssertionError("Expected %s to be subtype of %s".formatted(trivialType, supertype)); + } + var directSubtypes = extendedSupertypeInfo.getDirectSubtypes(); + if (directSubtypes.remove(trivialType)) { + directSubtypes.add(replacement); + } + } + for (var subtype : extendedTypeInfo.getAllSubtypes()) { + var extendedSubtypeInfo = extendedTypeInfoMap.get(subtype); + if (!extendedSubtypeInfo.getAllSupertypes().remove(trivialType)) { + throw new AssertionError("Expected %s to be supertype of %s".formatted(trivialType, subtype)); + } + } + extendedTypeInfoMap.remove(trivialType); + } + + private PartialRelation setReplacement(PartialRelation trivialRelation, PartialRelation replacement) { + if (replacement == null) { + return trivialRelation; + } + var resolved = setReplacement(replacement, replacements.get(replacement)); + replacements.put(trivialRelation, resolved); + return resolved; + } + + private Map computeAnalysisResults() { + var allExtendedTypeInfoList = sortTypes(); + var results = new LinkedHashMap( + allExtendedTypeInfoList.size() + replacements.size()); + for (var extendedTypeInfo : allExtendedTypeInfoList) { + var type = extendedTypeInfo.getType(); + results.put(type, new PreservedType(extendedTypeInfo, allExtendedTypeInfoList)); + } + for (var entry : replacements.entrySet()) { + var type = entry.getKey(); + results.put(type, new EliminatedType(entry.getValue())); + } + return Collections.unmodifiableMap(results); + } + + private List sortTypes() { + // Invert {@code directSubtypes} to keep track of the out-degree of types. + for (var extendedTypeInfo : extendedTypeInfoMap.values()) { + for (var directSubtype : extendedTypeInfo.getDirectSubtypes()) { + var extendedDirectSubtypeInfo = extendedTypeInfoMap.get(directSubtype); + extendedDirectSubtypeInfo.getUnsortedDirectSupertypes().add(extendedTypeInfo.getType()); + } + } + // Build a inverse topological order ({@code extends} edges always points to earlier nodes in the order, + // breaking ties according to the original order ({@link ExtendedTypeInfo#index}) to form a 'stable' sort. + // See, e.g., https://stackoverflow.com/a/11236027. + var priorityQueue = new PriorityQueue(); + for (var extendedTypeInfo : extendedTypeInfoMap.values()) { + if (extendedTypeInfo.getUnsortedDirectSupertypes().isEmpty()) { + priorityQueue.add(extendedTypeInfo); + } + } + var sorted = new ArrayList(extendedTypeInfoMap.size()); + while (!priorityQueue.isEmpty()) { + var extendedTypeInfo = priorityQueue.remove(); + sorted.add(extendedTypeInfo); + for (var directSubtype : extendedTypeInfo.getDirectSubtypes()) { + var extendedDirectSubtypeInfo = extendedTypeInfoMap.get(directSubtype); + var unsortedDirectSupertypes = extendedDirectSubtypeInfo.getUnsortedDirectSupertypes(); + if (!unsortedDirectSupertypes.remove(extendedTypeInfo.getType())) { + throw new AssertionError("Expected %s to be a direct supertype of %s" + .formatted(extendedTypeInfo.getType(), directSubtype)); + } + if (unsortedDirectSupertypes.isEmpty()) { + priorityQueue.add(extendedDirectSubtypeInfo); + } + } + } + return Collections.unmodifiableList(sorted); + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java new file mode 100644 index 00000000..7f438f71 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java @@ -0,0 +1,52 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import tools.refinery.store.partial.AnyPartialSymbolInterpretation; +import tools.refinery.store.partial.literal.Modality; +import tools.refinery.store.partial.representation.AnyPartialSymbol; +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.partial.translator.Advice; +import tools.refinery.store.partial.translator.TranslationUnit; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.Literal; +import tools.refinery.store.representation.Symbol; + +import java.util.*; + +public class TypeHierarchyTranslationUnit extends TranslationUnit { + static final Symbol INFERRED_TYPE_SYMBOL = new Symbol<>("inferredType", 1, + InferredType.class, InferredType.UNTYPED); + + private final Map typeInfoMap; + + public TypeHierarchyTranslationUnit(Map typeInfoMap) { + this.typeInfoMap = new LinkedHashMap<>(typeInfoMap); + } + + @Override + public Collection getTranslatedPartialSymbols() { + return null; + } + + @Override + public void configure(Collection advices) { + + } + + @Override + public List call(CallPolarity polarity, Modality modality, PartialRelation target, + List arguments) { + return null; + } + + @Override + public Map createPartialInterpretations(Model model) { + return null; + } + + @Override + public void initializeModel(Model model, int nodeCount) { + + } +} diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java new file mode 100644 index 00000000..1b0922fe --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java @@ -0,0 +1,46 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import tools.refinery.store.partial.representation.PartialRelation; + +import java.util.*; + +public record TypeInfo(Collection supertypes, boolean abstractType) { + public static Builder builder() { + return new Builder(); + } + + public static class Builder { + private final Set supertypes = new LinkedHashSet<>(); + private boolean abstractType; + + private Builder() { + } + + public Builder supertypes(Collection supertypes) { + this.supertypes.addAll(supertypes); + return this; + } + + public Builder supertypes(PartialRelation... supertypes) { + return supertypes(List.of(supertypes)); + } + + public Builder supertype(PartialRelation supertype) { + supertypes.add(supertype); + return this; + } + + public Builder abstractType(boolean abstractType) { + this.abstractType = abstractType; + return this; + } + + public Builder abstractType() { + return abstractType(true); + } + + public TypeInfo build() { + return new TypeInfo(Collections.unmodifiableSet(supertypes), abstractType); + } + } +} diff --git a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java new file mode 100644 index 00000000..9efa76ef --- /dev/null +++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java @@ -0,0 +1,32 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import org.junit.jupiter.api.Test; +import tools.refinery.store.partial.representation.PartialRelation; + +import java.util.Set; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; + +class InferredTypeTest { + private final PartialRelation c1 = new PartialRelation("C1", 1); + private final PartialRelation c2 = new PartialRelation("C2", 1); + + @Test + void untypedIsConsistentTest() { + var sut = new InferredType(Set.of(), Set.of(c1, c2), null); + assertThat(sut.isConsistent(), is(true)); + } + + @Test + void typedIsConsistentTest() { + var sut = new InferredType(Set.of(c1), Set.of(c1, c2), c1); + assertThat(sut.isConsistent(), is(true)); + } + + @Test + void typedIsInconsistentTest() { + var sut = new InferredType(Set.of(c1), Set.of(), null); + assertThat(sut.isConsistent(), is(false)); + } +} diff --git a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java new file mode 100644 index 00000000..ad81e28f --- /dev/null +++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java @@ -0,0 +1,204 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import org.hamcrest.Matchers; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.representation.TruthValue; + +import java.util.LinkedHashMap; +import java.util.Set; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; +import static org.junit.jupiter.api.Assertions.assertAll; + +class TypeAnalyzerExampleHierarchyTest { + private final PartialRelation a1 = new PartialRelation("A1", 1); + private final PartialRelation a2 = new PartialRelation("A2", 1); + private final PartialRelation a3 = new PartialRelation("A3", 1); + private final PartialRelation a4 = new PartialRelation("A4", 1); + private final PartialRelation a5 = new PartialRelation("A5", 1); + private final PartialRelation c1 = new PartialRelation("C1", 1); + private final PartialRelation c2 = new PartialRelation("C2", 1); + private final PartialRelation c3 = new PartialRelation("C3", 1); + private final PartialRelation c4 = new PartialRelation("C4", 1); + + private TypeAnalyzer sut; + private TypeAnalyzerTester tester; + + @BeforeEach + void beforeEach() { + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(a2, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(a4, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(a5, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(c1, TypeInfo.builder().supertypes(a1, a4).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertypes(a1, a2, a3, a4).build()); + typeInfoMap.put(c3, TypeInfo.builder().supertype(a3).build()); + typeInfoMap.put(c4, TypeInfo.builder().supertype(a4).build()); + sut = new TypeAnalyzer(typeInfoMap); + tester = new TypeAnalyzerTester(sut); + } + + @Test + void analysisResultsTest() { + assertAll( + () -> tester.assertAbstractType(a1, c1, c2), + () -> tester.assertEliminatedType(a2, c2), + () -> tester.assertAbstractType(a3, c2, c3), + () -> tester.assertAbstractType(a4, c1, c2, c4), + () -> tester.assertVacuousType(a5), + () -> tester.assertConcreteType(c1), + () -> tester.assertConcreteType(c2), + () -> tester.assertConcreteType(c3), + () -> tester.assertConcreteType(c4) + ); + } + + @Test + void inferredTypesTest() { + assertAll( + () -> assertThat(sut.getUnknownType(), Matchers.is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))), + () -> assertThat(tester.getInferredType(a1), Matchers.is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))), + () -> assertThat(tester.getInferredType(a3), Matchers.is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))), + () -> assertThat(tester.getInferredType(a4), Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))), + () -> assertThat(tester.getInferredType(a5), Matchers.is(new InferredType(Set.of(a5), Set.of(), null))), + () -> assertThat(tester.getInferredType(c1), Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), + () -> assertThat(tester.getInferredType(c2), + Matchers.is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))), + () -> assertThat(tester.getInferredType(c3), Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), + () -> assertThat(tester.getInferredType(c4), Matchers.is(new InferredType(Set.of(a4, c4), Set.of(c4), c4))) + ); + } + + @Test + void consistentMustTest() { + var a1Result = tester.getPreservedType(a1); + var a3Result = tester.getPreservedType(a3); + var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2); + assertAll( + () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)), + () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)), + () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())), + () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())), + () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE), + is(a1Result.asInferredType())) + ); + } + + @Test + void consistentMayNotTest() { + var a1Result = tester.getPreservedType(a1); + var a3Result = tester.getPreservedType(a3); + var a4Result = tester.getPreservedType(a4); + assertAll( + () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), + () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), + () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), + () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))), + () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(), Set.of(c3, c4), null))), + () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(), Set.of(c1, c4), null))), + () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(), Set.of(c3), null))) + ); + } + + @Test + void consistentErrorTest() { + var c1Result = tester.getPreservedType(c1); + var a4Result = tester.getPreservedType(a4); + var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null); + assertAll( + () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)), + () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)) + ); + } + + @Test + void consistentUnknownTest() { + var c1Result = tester.getPreservedType(c1); + var a4Result = tester.getPreservedType(a4); + assertAll( + () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.UNKNOWN), + is(a4Result.asInferredType())), + () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.UNKNOWN), + is(c1Result.asInferredType())) + ); + } + + @Test + void inconsistentMustTest() { + var a1Result = tester.getPreservedType(a1); + var c3Result = tester.getPreservedType(c3); + assertAll( + () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE), + Matchers.is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))), + () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), + Matchers.is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null))) + ); + } + + @Test + void inconsistentMayNotTest() { + var a1Result = tester.getPreservedType(a1); + var a4Result = tester.getPreservedType(a4); + var c1Result = tester.getPreservedType(c1); + assertAll( + () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))), + () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), + () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), + () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))) + ); + } + + @Test + void vacuousMustTest() { + var c1Result = tester.getPreservedType(c1); + var a5Result = tester.getPreservedType(a5); + assertAll( + () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE), + Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), + () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE), + Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))) + ); + } + + @Test + void vacuousMayNotTest() { + var c1Result = tester.getPreservedType(c1); + var a5Result = tester.getPreservedType(a5); + assertAll( + () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.FALSE), + is(a5Result.asInferredType())), + () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.FALSE), + is(c1Result.asInferredType())) + ); + } + + @Test + void vacuousErrorTest() { + var c1Result = tester.getPreservedType(c1); + var a5Result = tester.getPreservedType(a5); + assertAll( + () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR), + Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), + () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR), + Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), + () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR), + is(a5Result.asInferredType())) + ); + } +} diff --git a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java new file mode 100644 index 00000000..1aab75bb --- /dev/null +++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java @@ -0,0 +1,201 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import org.hamcrest.Matchers; +import org.junit.jupiter.api.Test; +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.representation.TruthValue; + +import java.util.LinkedHashMap; +import java.util.Set; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; +import static org.junit.jupiter.api.Assertions.assertAll; +import static org.junit.jupiter.api.Assertions.assertThrows; + +class TypeAnalyzerTest { + @Test + void directSupertypesTest() { + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var c3 = new PartialRelation("C3", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertypes(c2, c3).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build()); + typeInfoMap.put(c3, TypeInfo.builder().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + + assertAll( + () -> tester.assertConcreteType(c1), + () -> tester.assertConcreteType(c2, c1), + () -> tester.assertConcreteType(c3, c2) + ); + } + + @Test + void typeEliminationAbstractToConcreteTest() { + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var a11 = new PartialRelation("A11", 1); + var a12 = new PartialRelation("A12", 1); + var a21 = new PartialRelation("A21", 1); + var a22 = new PartialRelation("A22", 1); + var a3 = new PartialRelation("A3", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); + typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build()); + typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build()); + typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); + typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); + typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + + assertAll( + () -> tester.assertConcreteType(c1), + () -> tester.assertConcreteType(c2), + () -> tester.assertEliminatedType(a11, c1), + () -> tester.assertEliminatedType(a12, c1), + () -> tester.assertEliminatedType(a21, c1), + () -> tester.assertEliminatedType(a22, c1), + () -> tester.assertAbstractType(a3, c1, c2) + ); + } + + @Test + void typeEliminationConcreteToAbstractTest() { + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var a11 = new PartialRelation("A11", 1); + var a12 = new PartialRelation("A12", 1); + var a21 = new PartialRelation("A21", 1); + var a22 = new PartialRelation("A22", 1); + var a3 = new PartialRelation("A3", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build()); + typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); + typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); + typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build()); + typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build()); + typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + + assertAll( + () -> tester.assertConcreteType(c1), + () -> tester.assertConcreteType(c2), + () -> tester.assertEliminatedType(a11, c1), + () -> tester.assertEliminatedType(a12, c1), + () -> tester.assertEliminatedType(a21, c1), + () -> tester.assertEliminatedType(a22, c1), + () -> tester.assertAbstractType(a3, c1, c2) + ); + } + + @Test + void preserveConcreteTypeTest() { + var c1 = new PartialRelation("C1", 1); + var a1 = new PartialRelation("A1", 1); + var c2 = new PartialRelation("C2", 1); + var a2 = new PartialRelation("A2", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(a1, TypeInfo.builder().abstractType().supertype(c2).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(a2).build()); + typeInfoMap.put(a2, TypeInfo.builder().abstractType().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + + assertAll( + () -> tester.assertConcreteType(c1), + () -> tester.assertEliminatedType(a1, c1), + () -> tester.assertConcreteType(c2, c1), + () -> tester.assertEliminatedType(a2, c2) + ); + } + + @Test + void mostGeneralCurrentTypeTest() { + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var c3 = new PartialRelation("C3", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertype(c3).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build()); + typeInfoMap.put(c3, TypeInfo.builder().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + var c3Result = tester.getPreservedType(c3); + + var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); + assertAll( + () -> assertThat(tester.getInferredType(c3), Matchers.is(expected)), + () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), Matchers.is(expected)) + ); + } + + @Test + void preferFirstConcreteTypeTest() { + var a1 = new PartialRelation("A1", 1); + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var c3 = new PartialRelation("C3", 1); + var c4 = new PartialRelation("C4", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build()); + typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + var c1Result = tester.getPreservedType(c1); + var a1Result = tester.getPreservedType(a1); + + assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2))); + } + + @Test + void preferFirstMostGeneralConcreteTypeTest() { + var a1 = new PartialRelation("A1", 1); + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var c3 = new PartialRelation("C3", 1); + var c4 = new PartialRelation("C4", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build()); + typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); + typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); + + var sut = new TypeAnalyzer(typeInfoMap); + var tester = new TypeAnalyzerTester(sut); + var c1Result = tester.getPreservedType(c1); + var a1Result = tester.getPreservedType(a1); + + assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), + Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3))); + } + + @Test + void circularTypeHierarchyTest() { + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + var typeInfoMap = new LinkedHashMap(); + typeInfoMap.put(c1, TypeInfo.builder().supertype(c2).build()); + typeInfoMap.put(c2, TypeInfo.builder().supertype(c1).build()); + + assertThrows(IllegalArgumentException.class, () -> new TypeAnalyzer(typeInfoMap)); + } +} diff --git a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java new file mode 100644 index 00000000..ce600ea6 --- /dev/null +++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java @@ -0,0 +1,51 @@ +package tools.refinery.store.partial.translator.typehierarchy; + +import tools.refinery.store.partial.representation.PartialRelation; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.*; +import static org.hamcrest.Matchers.is; + +class TypeAnalyzerTester { + private final TypeAnalyzer sut; + + public TypeAnalyzerTester(TypeAnalyzer sut) { + this.sut = sut; + } + + public void assertAbstractType(PartialRelation partialRelation, PartialRelation... directSubtypes) { + assertPreservedType(partialRelation, true, false, directSubtypes); + } + + public void assertVacuousType(PartialRelation partialRelation) { + assertPreservedType(partialRelation, true, true); + } + + public void assertConcreteType(PartialRelation partialRelation, PartialRelation... directSubtypes) { + assertPreservedType(partialRelation, false, false, directSubtypes); + } + + private void assertPreservedType(PartialRelation partialRelation, boolean isAbstract, boolean isVacuous, + PartialRelation... directSubtypes) { + var result = sut.getAnalysisResults().get(partialRelation); + assertThat(result, is(instanceOf(PreservedType.class))); + var preservedResult = (PreservedType) result; + assertThat(preservedResult.isAbstractType(), is(isAbstract)); + assertThat(preservedResult.isVacuous(), is(isVacuous)); + assertThat(preservedResult.getDirectSubtypes(), hasItems(directSubtypes)); + } + + public void assertEliminatedType(PartialRelation partialRelation, PartialRelation replacement) { + var result = sut.getAnalysisResults().get(partialRelation); + assertThat(result, is(instanceOf(EliminatedType.class))); + assertThat(((EliminatedType) result).replacement(), is(replacement)); + } + + public PreservedType getPreservedType(PartialRelation partialRelation) { + return (PreservedType) sut.getAnalysisResults().get(partialRelation); + } + + public InferredType getInferredType(PartialRelation partialRelation) { + return getPreservedType(partialRelation).asInferredType(); + } +} diff --git a/subprojects/store-query-viatra/build.gradle b/subprojects/store-query-viatra/build.gradle index c12b48fe..13a7544f 100644 --- a/subprojects/store-query-viatra/build.gradle +++ b/subprojects/store-query-viatra/build.gradle @@ -10,7 +10,7 @@ configurations.testRuntimeClasspath { dependencies { implementation libs.ecore api libs.viatra - api project(':refinery-store') + api project(':refinery-store-query') testImplementation libs.slf4j.simple testImplementation libs.slf4j.log4j } diff --git a/subprojects/store-query/build.gradle b/subprojects/store-query/build.gradle new file mode 100644 index 00000000..2b76e608 --- /dev/null +++ b/subprojects/store-query/build.gradle @@ -0,0 +1,7 @@ +plugins { + id 'refinery-java-library' +} + +dependencies { + api project(':refinery-store') +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java new file mode 100644 index 00000000..760b264b --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java @@ -0,0 +1,112 @@ +package tools.refinery.store.query; + +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.DnfCallLiteral; +import tools.refinery.store.query.literal.LiteralReduction; + +import java.util.*; + +public final class Dnf implements RelationLike { + private final String name; + + private final String uniqueName; + + private final List parameters; + + private final List> functionalDependencies; + + private final List clauses; + + Dnf(String name, List parameters, List> functionalDependencies, + List clauses) { + validateFunctionalDependencies(parameters, functionalDependencies); + this.name = name; + this.uniqueName = DnfUtils.generateUniqueName(name); + this.parameters = parameters; + this.functionalDependencies = functionalDependencies; + this.clauses = clauses; + } + + private static void validateFunctionalDependencies( + Collection parameters, Collection> functionalDependencies) { + var parameterSet = new HashSet<>(parameters); + for (var functionalDependency : functionalDependencies) { + validateParameters(parameters, parameterSet, functionalDependency.forEach(), functionalDependency); + validateParameters(parameters, parameterSet, functionalDependency.unique(), functionalDependency); + } + } + + private static void validateParameters(Collection parameters, Set parameterSet, + Collection toValidate, + FunctionalDependency functionalDependency) { + for (var variable : toValidate) { + if (!parameterSet.contains(variable)) { + throw new IllegalArgumentException( + "Variable %s of functional dependency %s does not appear in the parameter list %s" + .formatted(variable, functionalDependency, parameters)); + } + } + } + + @Override + public String name() { + return name; + } + + public String getUniqueName() { + return uniqueName; + } + + public List getParameters() { + return parameters; + } + + public List> getFunctionalDependencies() { + return functionalDependencies; + } + + @Override + public int arity() { + return parameters.size(); + } + + public List getClauses() { + return clauses; + } + + public LiteralReduction getReduction() { + if (clauses.isEmpty()) { + return LiteralReduction.ALWAYS_FALSE; + } + for (var clause : clauses) { + if (clause.literals().isEmpty()) { + return LiteralReduction.ALWAYS_TRUE; + } + } + return LiteralReduction.NOT_REDUCIBLE; + } + + public DnfCallLiteral call(CallPolarity polarity, List arguments) { + return new DnfCallLiteral(polarity, this, arguments); + } + + public DnfCallLiteral call(CallPolarity polarity, Variable... arguments) { + return call(polarity, List.of(arguments)); + } + + public DnfCallLiteral call(Variable... arguments) { + return call(CallPolarity.POSITIVE, arguments); + } + + public DnfCallLiteral callTransitive(Variable left, Variable right) { + return call(CallPolarity.TRANSITIVE, List.of(left, right)); + } + + public static DnfBuilder builder() { + return builder(null); + } + + public static DnfBuilder builder(String name) { + return new DnfBuilder(name); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java new file mode 100644 index 00000000..b18b5177 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java @@ -0,0 +1,108 @@ +package tools.refinery.store.query; + +import tools.refinery.store.query.literal.Literal; + +import java.util.*; + +@SuppressWarnings("UnusedReturnValue") +public class DnfBuilder { + private final String name; + + private final List parameters = new ArrayList<>(); + + private final List> functionalDependencies = new ArrayList<>(); + + private final List> clauses = new ArrayList<>(); + + DnfBuilder(String name) { + this.name = name; + } + + public DnfBuilder parameter(Variable variable) { + parameters.add(variable); + return this; + } + + public DnfBuilder parameters(Variable... variables) { + return parameters(List.of(variables)); + } + + public DnfBuilder parameters(Collection variables) { + parameters.addAll(variables); + return this; + } + + public DnfBuilder functionalDependencies(Collection> functionalDependencies) { + this.functionalDependencies.addAll(functionalDependencies); + return this; + } + + public DnfBuilder functionalDependency(FunctionalDependency functionalDependency) { + functionalDependencies.add(functionalDependency); + return this; + } + + public DnfBuilder functionalDependency(Set forEach, Set unique) { + return functionalDependency(new FunctionalDependency<>(forEach, unique)); + } + + public DnfBuilder clause(Literal... literals) { + clause(List.of(literals)); + return this; + } + + public DnfBuilder clause(Collection literals) { + var filteredLiterals = new ArrayList(literals.size()); + for (var literal : literals) { + var reduction = literal.getReduction(); + switch (reduction) { + case NOT_REDUCIBLE -> filteredLiterals.add(literal); + case ALWAYS_TRUE -> { + // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at + // least on object. + } + case ALWAYS_FALSE -> { + // Clauses with {@code false} literals can be omitted entirely. + return this; + } + default -> throw new IllegalStateException("Invalid reduction %s".formatted(reduction)); + } + } + clauses.add(Collections.unmodifiableList(filteredLiterals)); + return this; + } + + public DnfBuilder clause(DnfClause clause) { + return clause(clause.literals()); + } + + public DnfBuilder clauses(DnfClause... clauses) { + for (var clause : clauses) { + this.clause(clause); + } + return this; + } + + public DnfBuilder clauses(Collection clauses) { + for (var clause : clauses) { + this.clause(clause); + } + return this; + } + + public Dnf build() { + var postProcessedClauses = new ArrayList(clauses.size()); + for (var constraints : clauses) { + var variables = new HashSet(); + for (var constraint : constraints) { + constraint.collectAllVariables(variables); + } + parameters.forEach(variables::remove); + postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables), + Collections.unmodifiableList(constraints))); + } + return new Dnf(name, Collections.unmodifiableList(parameters), + Collections.unmodifiableList(functionalDependencies), + Collections.unmodifiableList(postProcessedClauses)); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java new file mode 100644 index 00000000..2ba6becc --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java @@ -0,0 +1,9 @@ +package tools.refinery.store.query; + +import tools.refinery.store.query.literal.Literal; + +import java.util.List; +import java.util.Set; + +public record DnfClause(Set quantifiedVariables, List literals) { +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java new file mode 100644 index 00000000..17564d43 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java @@ -0,0 +1,24 @@ +package tools.refinery.store.query; + +import java.util.Map; +import java.util.UUID; + +public final class DnfUtils { + private DnfUtils() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static String generateUniqueName(String originalName) { + UUID uuid = UUID.randomUUID(); + String uniqueString = "_" + uuid.toString().replace('-', '_'); + if (originalName == null) { + return uniqueString; + } else { + return originalName + uniqueString; + } + } + + public static Variable maybeSubstitute(Variable variable, Map substitution) { + return substitution.getOrDefault(variable, variable); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/FunctionalDependency.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/FunctionalDependency.java new file mode 100644 index 00000000..63a81713 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/FunctionalDependency.java @@ -0,0 +1,15 @@ +package tools.refinery.store.query; + +import java.util.HashSet; +import java.util.Set; + +public record FunctionalDependency(Set forEach, Set unique) { + public FunctionalDependency { + var uniqueForEach = new HashSet<>(unique); + uniqueForEach.retainAll(forEach); + if (!uniqueForEach.isEmpty()) { + throw new IllegalArgumentException("Variables %s appear on both sides of the functional dependency" + .formatted(uniqueForEach)); + } + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java new file mode 100644 index 00000000..6a1aeabb --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java @@ -0,0 +1,11 @@ +package tools.refinery.store.query; + +import tools.refinery.store.adapter.ModelAdapterType; + +public final class ModelQuery extends ModelAdapterType { + public static final ModelQuery ADAPTER = new ModelQuery(); + + private ModelQuery() { + super(ModelQueryAdapter.class, ModelQueryStoreAdapter.class, ModelQueryBuilder.class); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java new file mode 100644 index 00000000..f7762444 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java @@ -0,0 +1,13 @@ +package tools.refinery.store.query; + +import tools.refinery.store.adapter.ModelAdapter; + +public interface ModelQueryAdapter extends ModelAdapter { + ModelQueryStoreAdapter getStoreAdapter(); + + ResultSet getResultSet(Dnf query); + + boolean hasPendingChanges(); + + void flushChanges(); +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java new file mode 100644 index 00000000..b3cfb4b4 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java @@ -0,0 +1,23 @@ +package tools.refinery.store.query; + +import tools.refinery.store.adapter.ModelAdapterBuilder; +import tools.refinery.store.model.ModelStore; + +import java.util.Collection; +import java.util.List; + +public interface ModelQueryBuilder extends ModelAdapterBuilder { + default ModelQueryBuilder queries(Dnf... queries) { + return queries(List.of(queries)); + } + + default ModelQueryBuilder queries(Collection queries) { + queries.forEach(this::query); + return this; + } + + ModelQueryBuilder query(Dnf query); + + @Override + ModelQueryStoreAdapter createStoreAdapter(ModelStore store); +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java new file mode 100644 index 00000000..091d6d06 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java @@ -0,0 +1,16 @@ +package tools.refinery.store.query; + +import tools.refinery.store.query.view.AnyRelationView; +import tools.refinery.store.adapter.ModelStoreAdapter; +import tools.refinery.store.model.Model; + +import java.util.Collection; + +public interface ModelQueryStoreAdapter extends ModelStoreAdapter { + Collection getRelationViews(); + + Collection getQueries(); + + @Override + ModelQueryAdapter createModelAdapter(Model model); +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java new file mode 100644 index 00000000..8c784d8b --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java @@ -0,0 +1,11 @@ +package tools.refinery.store.query; + +public interface RelationLike { + String name(); + + int arity(); + + default boolean invalidIndex(int i) { + return i < 0 || i >= arity(); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java new file mode 100644 index 00000000..3542e252 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java @@ -0,0 +1,25 @@ +package tools.refinery.store.query; + +import tools.refinery.store.tuple.Tuple; +import tools.refinery.store.tuple.TupleLike; + +import java.util.Optional; +import java.util.stream.Stream; + +public interface ResultSet { + boolean hasResult(); + + boolean hasResult(Tuple parameters); + + Optional oneResult(); + + Optional oneResult(Tuple parameters); + + Stream allResults(); + + Stream allResults(Tuple parameters); + + int countResults(); + + int countResults(Tuple parameters); +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java new file mode 100644 index 00000000..2eb87649 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java @@ -0,0 +1,58 @@ +package tools.refinery.store.query; + +import tools.refinery.store.query.literal.ConstantLiteral; +import tools.refinery.store.query.literal.EquivalenceLiteral; + +import java.util.Objects; + +public class Variable { + private final String name; + private final String uniqueName; + + public Variable() { + this(null); + } + + public Variable(String name) { + super(); + this.name = name; + this.uniqueName = DnfUtils.generateUniqueName(name); + + } + public String getName() { + return name; + } + + public String getUniqueName() { + return uniqueName; + } + + public boolean isNamed() { + return name != null; + } + + public ConstantLiteral isConstant(int value) { + return new ConstantLiteral(this, value); + } + + public EquivalenceLiteral isEquivalent(Variable other) { + return new EquivalenceLiteral(true, this, other); + } + + public EquivalenceLiteral notEquivalent(Variable other) { + return new EquivalenceLiteral(false, this, other); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + Variable variable = (Variable) o; + return Objects.equals(uniqueName, variable.uniqueName); + } + + @Override + public int hashCode() { + return Objects.hash(uniqueName); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java new file mode 100644 index 00000000..fd2f1eec --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java @@ -0,0 +1,37 @@ +package tools.refinery.store.query.literal; + +import tools.refinery.store.query.Variable; + +import java.util.Map; +import java.util.Set; + +public class BooleanLiteral implements Literal { + public static final BooleanLiteral TRUE = new BooleanLiteral(LiteralReduction.ALWAYS_TRUE); + public static final BooleanLiteral FALSE = new BooleanLiteral(LiteralReduction.ALWAYS_FALSE); + + private final LiteralReduction reduction; + + private BooleanLiteral(LiteralReduction reduction) { + this.reduction = reduction; + } + + @Override + public void collectAllVariables(Set variables) { + // No variables to collect. + } + + @Override + public Literal substitute(Map substitution) { + // No variables to substitute. + return this; + } + + @Override + public LiteralReduction getReduction() { + return reduction; + } + + public static BooleanLiteral fromBoolean(boolean value) { + return value ? TRUE : FALSE; + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java new file mode 100644 index 00000000..5e1ae94d --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java @@ -0,0 +1,66 @@ +package tools.refinery.store.query.literal; + +import tools.refinery.store.query.DnfUtils; +import tools.refinery.store.query.RelationLike; +import tools.refinery.store.query.Variable; + +import java.util.List; +import java.util.Map; +import java.util.Objects; +import java.util.Set; + +public abstract class CallLiteral implements Literal { + private final CallPolarity polarity; + private final T target; + private final List arguments; + + protected CallLiteral(CallPolarity polarity, T target, List arguments) { + if (arguments.size() != target.arity()) { + throw new IllegalArgumentException("%s needs %d arguments, but got %s".formatted(target.name(), + target.arity(), arguments.size())); + } + if (polarity.isTransitive() && target.arity() != 2) { + throw new IllegalArgumentException("Transitive closures can only take binary relations"); + } + this.polarity = polarity; + this.target = target; + this.arguments = arguments; + } + + public CallPolarity getPolarity() { + return polarity; + } + + public T getTarget() { + return target; + } + + public List getArguments() { + return arguments; + } + + @Override + public void collectAllVariables(Set variables) { + if (polarity.isPositive()) { + variables.addAll(arguments); + } + } + + protected List substituteArguments(Map substitution) { + return arguments.stream().map(variable -> DnfUtils.maybeSubstitute(variable, substitution)).toList(); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + CallLiteral callAtom = (CallLiteral) o; + return polarity == callAtom.polarity && Objects.equals(target, callAtom.target) && + Objects.equals(arguments, callAtom.arguments); + } + + @Override + public int hashCode() { + return Objects.hash(polarity, target, arguments); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java new file mode 100644 index 00000000..84b4b771 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java @@ -0,0 +1,32 @@ +package tools.refinery.store.query.literal; + +public enum CallPolarity { + POSITIVE(true, false), + NEGATIVE(false, false), + TRANSITIVE(true, true); + + private final boolean positive; + + private final boolean transitive; + + CallPolarity(boolean positive, boolean transitive) { + this.positive = positive; + this.transitive = transitive; + } + + public boolean isPositive() { + return positive; + } + + public boolean isTransitive() { + return transitive; + } + + public CallPolarity negate() { + return switch (this) { + case POSITIVE -> NEGATIVE; + case NEGATIVE -> POSITIVE; + case TRANSITIVE -> throw new IllegalArgumentException("Transitive polarity cannot be negated"); + }; + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java new file mode 100644 index 00000000..746d23af --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java @@ -0,0 +1,19 @@ +package tools.refinery.store.query.literal; + +import tools.refinery.store.query.DnfUtils; +import tools.refinery.store.query.Variable; + +import java.util.Map; +import java.util.Set; + +public record ConstantLiteral(Variable variable, int nodeId) implements Literal { + @Override + public void collectAllVariables(Set variables) { + variables.add(variable); + } + + @Override + public ConstantLiteral substitute(Map substitution) { + return new ConstantLiteral(DnfUtils.maybeSubstitute(variable, substitution), nodeId); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java new file mode 100644 index 00000000..de6c6005 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java @@ -0,0 +1,29 @@ +package tools.refinery.store.query.literal; + +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.Variable; + +import java.util.List; +import java.util.Map; + +public final class DnfCallLiteral extends CallLiteral implements PolarLiteral { + public DnfCallLiteral(CallPolarity polarity, Dnf target, List arguments) { + super(polarity, target, arguments); + } + + @Override + public DnfCallLiteral substitute(Map substitution) { + return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); + } + + @Override + public DnfCallLiteral negate() { + return new DnfCallLiteral(getPolarity().negate(), getTarget(), getArguments()); + } + + @Override + public LiteralReduction getReduction() { + var dnfReduction = getTarget().getReduction(); + return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate(); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java new file mode 100644 index 00000000..f30179b2 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java @@ -0,0 +1,35 @@ +package tools.refinery.store.query.literal; + +import tools.refinery.store.query.DnfUtils; +import tools.refinery.store.query.Variable; + +import java.util.Map; +import java.util.Set; + +public record EquivalenceLiteral(boolean positive, Variable left, Variable right) + implements PolarLiteral { + @Override + public void collectAllVariables(Set variables) { + variables.add(left); + variables.add(right); + } + + @Override + public EquivalenceLiteral negate() { + return new EquivalenceLiteral(!positive, left, right); + } + + @Override + public EquivalenceLiteral substitute(Map substitution) { + return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution), + DnfUtils.maybeSubstitute(right, substitution)); + } + + @Override + public LiteralReduction getReduction() { + if (left.equals(right)) { + return positive ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE; + } + return LiteralReduction.NOT_REDUCIBLE; + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java new file mode 100644 index 00000000..a6893acf --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java @@ -0,0 +1,16 @@ +package tools.refinery.store.query.literal; + +import tools.refinery.store.query.Variable; + +import java.util.Map; +import java.util.Set; + +public interface Literal { + void collectAllVariables(Set variables); + + Literal substitute(Map substitution); + + default LiteralReduction getReduction() { + return LiteralReduction.NOT_REDUCIBLE; + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java new file mode 100644 index 00000000..146089f6 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java @@ -0,0 +1,26 @@ +package tools.refinery.store.query.literal; + +public enum LiteralReduction { + /** + * Signifies that a literal should be preserved in the clause. + */ + NOT_REDUCIBLE, + + /** + * Signifies that the literal may be omitted from the cause (if the model being queried is nonempty). + */ + ALWAYS_TRUE, + + /** + * Signifies that the clause with the literal may be omitted entirely. + */ + ALWAYS_FALSE; + + public LiteralReduction negate() { + return switch (this) { + case NOT_REDUCIBLE -> NOT_REDUCIBLE; + case ALWAYS_TRUE -> ALWAYS_FALSE; + case ALWAYS_FALSE -> ALWAYS_TRUE; + }; + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java new file mode 100644 index 00000000..2c7e893f --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java @@ -0,0 +1,11 @@ +package tools.refinery.store.query.literal; + +public final class Literals { + private Literals() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static > T not(PolarLiteral literal) { + return literal.negate(); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java new file mode 100644 index 00000000..32523675 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java @@ -0,0 +1,5 @@ +package tools.refinery.store.query.literal; + +public interface PolarLiteral> extends Literal { + T negate(); +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java new file mode 100644 index 00000000..4718b550 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java @@ -0,0 +1,24 @@ +package tools.refinery.store.query.literal; + +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.view.AnyRelationView; + +import java.util.List; +import java.util.Map; + +public final class RelationViewLiteral extends CallLiteral + implements PolarLiteral { + public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List arguments) { + super(polarity, target, arguments); + } + + @Override + public RelationViewLiteral substitute(Map substitution) { + return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); + } + + @Override + public RelationViewLiteral negate() { + return new RelationViewLiteral(getPolarity().negate(), getTarget(), getArguments()); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java new file mode 100644 index 00000000..328cde3a --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java @@ -0,0 +1,24 @@ +package tools.refinery.store.query.view; + +import tools.refinery.store.model.Model; +import tools.refinery.store.query.FunctionalDependency; +import tools.refinery.store.representation.AnySymbol; +import tools.refinery.store.query.RelationLike; + +import java.util.Set; + +public sealed interface AnyRelationView extends RelationLike permits RelationView { + AnySymbol getSymbol(); + + default Set> getFunctionalDependencies() { + return Set.of(); + } + + default Set getImpliedRelationViews() { + return Set.of(); + } + + boolean get(Model model, Object[] tuple); + + Iterable getAll(Model model); +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java new file mode 100644 index 00000000..64c601bb --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java @@ -0,0 +1,49 @@ +package tools.refinery.store.query.view; + +import tools.refinery.store.tuple.Tuple; +import tools.refinery.store.representation.Symbol; + +import java.util.Objects; +import java.util.function.BiPredicate; +import java.util.function.Predicate; + +public class FilteredRelationView extends TuplePreservingRelationView { + private final BiPredicate predicate; + + public FilteredRelationView(Symbol symbol, String name, BiPredicate predicate) { + super(symbol, name); + this.predicate = predicate; + } + + public FilteredRelationView(Symbol symbol, BiPredicate predicate) { + super(symbol); + this.predicate = predicate; + } + + public FilteredRelationView(Symbol symbol, String name, Predicate predicate) { + this(symbol, name, (k, v) -> predicate.test(v)); + } + + public FilteredRelationView(Symbol symbol, Predicate predicate) { + this(symbol, (k, v) -> predicate.test(v)); + } + + @Override + public boolean filter(Tuple key, T value) { + return this.predicate.test(key, value); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + if (!super.equals(o)) return false; + FilteredRelationView that = (FilteredRelationView) o; + return Objects.equals(predicate, that.predicate); + } + + @Override + public int hashCode() { + return Objects.hash(super.hashCode(), predicate); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java new file mode 100644 index 00000000..3d278a8b --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java @@ -0,0 +1,71 @@ +package tools.refinery.store.query.view; + +import tools.refinery.store.model.Model; +import tools.refinery.store.query.FunctionalDependency; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; +import tools.refinery.store.tuple.Tuple1; + +import java.util.Set; +import java.util.stream.Collectors; +import java.util.stream.IntStream; + +public final class FunctionalRelationView extends RelationView { + public FunctionalRelationView(Symbol symbol, String name) { + super(symbol, name); + } + + public FunctionalRelationView(Symbol symbol) { + super(symbol); + } + + @Override + public Set> getFunctionalDependencies() { + var arity = getSymbol().arity(); + var forEach = IntStream.range(0, arity).boxed().collect(Collectors.toUnmodifiableSet()); + var unique = Set.of(arity); + return Set.of(new FunctionalDependency<>(forEach, unique)); + } + + @Override + public Set getImpliedRelationViews() { + var symbol = getSymbol(); + var impliedIndices = IntStream.range(0, symbol.arity()).boxed().toList(); + var keyOnlyRelationView = new KeyOnlyRelationView<>(symbol); + return Set.of(new RelationViewImplication(this, keyOnlyRelationView, impliedIndices)); + } + + @Override + public boolean filter(Tuple key, T value) { + return true; + } + + @Override + public Object[] forwardMap(Tuple key, T value) { + int size = key.getSize(); + Object[] result = new Object[size + 1]; + for (int i = 0; i < size; i++) { + result[i] = Tuple.of(key.get(i)); + } + result[key.getSize()] = value; + return result; + } + + @Override + public boolean get(Model model, Object[] tuple) { + int[] content = new int[tuple.length - 1]; + for (int i = 0; i < tuple.length - 1; i++) { + content[i] = ((Tuple1) tuple[i]).value0(); + } + Tuple key = Tuple.of(content); + @SuppressWarnings("unchecked") + T valueInTuple = (T) tuple[tuple.length - 1]; + T valueInMap = model.getInterpretation(getSymbol()).get(key); + return valueInTuple.equals(valueInMap); + } + + @Override + public int arity() { + return getSymbol().arity() + 1; + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java new file mode 100644 index 00000000..e1b2e45b --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java @@ -0,0 +1,36 @@ +package tools.refinery.store.query.view; + +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; + +import java.util.Objects; + +public final class KeyOnlyRelationView extends TuplePreservingRelationView { + public static final String VIEW_NAME = "key"; + + private final T defaultValue; + + public KeyOnlyRelationView(Symbol symbol) { + super(symbol, VIEW_NAME); + defaultValue = symbol.defaultValue(); + } + + @Override + public boolean filter(Tuple key, T value) { + return !Objects.equals(value, defaultValue); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + if (!super.equals(o)) return false; + KeyOnlyRelationView that = (KeyOnlyRelationView) o; + return Objects.equals(defaultValue, that.defaultValue); + } + + @Override + public int hashCode() { + return Objects.hash(super.hashCode(), defaultValue); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java new file mode 100644 index 00000000..2714a8c5 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java @@ -0,0 +1,82 @@ +package tools.refinery.store.query.view; + +import tools.refinery.store.query.Variable; +import tools.refinery.store.map.CursorAsIterator; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.RelationViewLiteral; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; + +import java.util.List; +import java.util.Objects; +import java.util.UUID; + +/** + * Represents a view of a {@link Symbol} that can be queried. + * + * @param + * @author Oszkar Semerath + */ +public abstract non-sealed class RelationView implements AnyRelationView { + private final Symbol symbol; + + private final String name; + + protected RelationView(Symbol symbol, String name) { + this.symbol = symbol; + this.name = name; + } + + protected RelationView(Symbol representation) { + this(representation, UUID.randomUUID().toString()); + } + + @Override + public Symbol getSymbol() { + return symbol; + } + + @Override + public String name() { + return symbol.name() + "#" + name; + } + + public abstract boolean filter(Tuple key, T value); + + public abstract Object[] forwardMap(Tuple key, T value); + + @Override + public Iterable getAll(Model model) { + return (() -> new CursorAsIterator<>(model.getInterpretation(symbol).getAll(), this::forwardMap, this::filter)); + } + + public RelationViewLiteral call(CallPolarity polarity, List arguments) { + return new RelationViewLiteral(polarity, this, arguments); + } + + public RelationViewLiteral call(CallPolarity polarity, Variable... arguments) { + return call(polarity, List.of(arguments)); + } + + public RelationViewLiteral call(Variable... arguments) { + return call(CallPolarity.POSITIVE, arguments); + } + + public RelationViewLiteral callTransitive(Variable left, Variable right) { + return call(CallPolarity.TRANSITIVE, List.of(left, right)); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + RelationView that = (RelationView) o; + return Objects.equals(symbol, that.symbol) && Objects.equals(name, that.name); + } + + @Override + public int hashCode() { + return Objects.hash(symbol, name); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java new file mode 100644 index 00000000..2ba1fcc4 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java @@ -0,0 +1,19 @@ +package tools.refinery.store.query.view; + +import java.util.List; + +public record RelationViewImplication(AnyRelationView implyingRelationView, AnyRelationView impliedRelationView, + List impliedIndices) { + public RelationViewImplication { + if (impliedIndices.size() != impliedRelationView.arity()) { + throw new IllegalArgumentException("Expected %d implied indices for %s, but %d are provided" + .formatted(impliedRelationView.arity(), impliedRelationView, impliedIndices.size())); + } + for (var index : impliedIndices) { + if (impliedRelationView.invalidIndex(index)) { + throw new IllegalArgumentException("%d is not a valid index for %s".formatted(index, + implyingRelationView)); + } + } + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java new file mode 100644 index 00000000..8cc4986e --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java @@ -0,0 +1,44 @@ +package tools.refinery.store.query.view; + +import tools.refinery.store.model.Model; +import tools.refinery.store.tuple.Tuple; +import tools.refinery.store.tuple.Tuple1; +import tools.refinery.store.representation.Symbol; + +public abstract class TuplePreservingRelationView extends RelationView { + protected TuplePreservingRelationView(Symbol symbol, String name) { + super(symbol, name); + } + + protected TuplePreservingRelationView(Symbol symbol) { + super(symbol); + } + + public Object[] forwardMap(Tuple key) { + Object[] result = new Object[key.getSize()]; + for (int i = 0; i < key.getSize(); i++) { + result[i] = Tuple.of(key.get(i)); + } + return result; + } + + @Override + public Object[] forwardMap(Tuple key, T value) { + return forwardMap(key); + } + + @Override + public boolean get(Model model, Object[] tuple) { + int[] content = new int[tuple.length]; + for (int i = 0; i < tuple.length; i++) { + content[i] = ((Tuple1) tuple[i]).value0(); + } + Tuple key = Tuple.of(content); + T value = model.getInterpretation(getSymbol()).get(key); + return filter(key, value); + } + + public int arity() { + return this.getSymbol().arity(); + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretation.java b/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretation.java deleted file mode 100644 index 331fa294..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretation.java +++ /dev/null @@ -1,19 +0,0 @@ -package tools.refinery.store.partial; - -import tools.refinery.store.adapter.ModelAdapterBuilderFactory; -import tools.refinery.store.model.ModelStoreBuilder; -import tools.refinery.store.partial.internal.PartialInterpretationBuilderImpl; - -public final class PartialInterpretation extends ModelAdapterBuilderFactory { - public static final PartialInterpretation ADAPTER = new PartialInterpretation(); - - private PartialInterpretation() { - super(PartialInterpretationAdapter.class, PartialInterpretationStoreAdapter.class, PartialInterpretationBuilder.class); - } - - @Override - public PartialInterpretationBuilder createBuilder(ModelStoreBuilder storeBuilder) { - return new PartialInterpretationBuilderImpl(storeBuilder); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java b/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java deleted file mode 100644 index 2c83a200..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java +++ /dev/null @@ -1,9 +0,0 @@ -package tools.refinery.store.partial; - -import tools.refinery.store.adapter.ModelAdapter; - -public interface PartialInterpretationAdapter extends ModelAdapter { - @Override - PartialInterpretationStoreAdapter getStoreAdapter(); -} - diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java b/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java deleted file mode 100644 index 0ec13836..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java +++ /dev/null @@ -1,9 +0,0 @@ -package tools.refinery.store.partial; - -import tools.refinery.store.adapter.ModelAdapterBuilder; -import tools.refinery.store.model.ModelStore; - -public interface PartialInterpretationBuilder extends ModelAdapterBuilder { - @Override - PartialInterpretationStoreAdapter createStoreAdapter(ModelStore store); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java b/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java deleted file mode 100644 index d4eb770d..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java +++ /dev/null @@ -1,9 +0,0 @@ -package tools.refinery.store.partial; - -import tools.refinery.store.adapter.ModelStoreAdapter; -import tools.refinery.store.model.Model; - -public interface PartialInterpretationStoreAdapter extends ModelStoreAdapter { - @Override - PartialInterpretationAdapter createModelAdapter(Model model); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java b/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java deleted file mode 100644 index 4b3977c0..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java +++ /dev/null @@ -1,24 +0,0 @@ -package tools.refinery.store.partial.internal; - -import tools.refinery.store.model.Model; -import tools.refinery.store.partial.PartialInterpretationAdapter; - -public class PartialInterpretationAdapterImpl implements PartialInterpretationAdapter { - private final Model model; - private final PartialInterpretationStoreAdapterImpl storeAdapter; - - PartialInterpretationAdapterImpl(Model model, PartialInterpretationStoreAdapterImpl storeAdapter) { - this.model = model; - this.storeAdapter = storeAdapter; - } - - @Override - public Model getModel() { - return model; - } - - @Override - public PartialInterpretationStoreAdapterImpl getStoreAdapter() { - return storeAdapter; - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java b/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java deleted file mode 100644 index 4609dc32..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java +++ /dev/null @@ -1,17 +0,0 @@ -package tools.refinery.store.partial.internal; - -import tools.refinery.store.adapter.AbstractModelAdapterBuilder; -import tools.refinery.store.model.ModelStore; -import tools.refinery.store.model.ModelStoreBuilder; -import tools.refinery.store.partial.PartialInterpretationBuilder; - -public class PartialInterpretationBuilderImpl extends AbstractModelAdapterBuilder implements PartialInterpretationBuilder { - public PartialInterpretationBuilderImpl(ModelStoreBuilder storeBuilder) { - super(storeBuilder); - } - - @Override - public PartialInterpretationStoreAdapterImpl createStoreAdapter(ModelStore store) { - return null; - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java b/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java deleted file mode 100644 index 970b802b..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java +++ /dev/null @@ -1,23 +0,0 @@ -package tools.refinery.store.partial.internal; - -import tools.refinery.store.model.Model; -import tools.refinery.store.model.ModelStore; -import tools.refinery.store.partial.PartialInterpretationStoreAdapter; - -public class PartialInterpretationStoreAdapterImpl implements PartialInterpretationStoreAdapter { - private final ModelStore store; - - PartialInterpretationStoreAdapterImpl(ModelStore store) { - this.store = store; - } - - @Override - public ModelStore getStore() { - return store; - } - - @Override - public PartialInterpretationAdapterImpl createModelAdapter(Model model) { - return new PartialInterpretationAdapterImpl(model, this); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java deleted file mode 100644 index 8070726a..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java +++ /dev/null @@ -1,30 +0,0 @@ -package tools.refinery.store.partial.literal; - -import tools.refinery.store.query.Dnf; -import tools.refinery.store.query.Variable; -import tools.refinery.store.query.literal.CallPolarity; -import tools.refinery.store.query.literal.DnfCallLiteral; -import tools.refinery.store.query.literal.PolarLiteral; - -import java.util.List; -import java.util.Map; - -public class ModalDnfCallLiteral extends ModalLiteral implements PolarLiteral { - public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List arguments) { - super(polarity, modality, target, arguments); - } - - public ModalDnfCallLiteral(Modality modality, DnfCallLiteral baseLiteral) { - super(modality.commute(baseLiteral.getPolarity()), baseLiteral); - } - - @Override - public ModalDnfCallLiteral substitute(Map substitution) { - return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); - } - - @Override - public ModalDnfCallLiteral negate() { - return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java deleted file mode 100644 index a1b6c83e..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java +++ /dev/null @@ -1,45 +0,0 @@ -package tools.refinery.store.partial.literal; - -import tools.refinery.store.query.RelationLike; -import tools.refinery.store.query.Variable; -import tools.refinery.store.query.literal.CallLiteral; -import tools.refinery.store.query.literal.CallPolarity; - -import java.util.List; -import java.util.Objects; - -public abstract class ModalLiteral extends CallLiteral { - private final Modality modality; - - protected ModalLiteral(CallPolarity polarity, Modality modality, T target, List arguments) { - super(polarity, target, arguments); - this.modality = modality; - } - - protected ModalLiteral(Modality modality, CallLiteral baseLiteral) { - this(baseLiteral.getPolarity(), commute(modality, baseLiteral.getPolarity()), baseLiteral.getTarget(), - baseLiteral.getArguments()); - } - - public Modality getModality() { - return modality; - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - if (!super.equals(o)) return false; - ModalLiteral that = (ModalLiteral) o; - return modality == that.modality; - } - - @Override - public int hashCode() { - return Objects.hash(super.hashCode(), modality); - } - - private static Modality commute(Modality modality, CallPolarity polarity) { - return polarity.isPositive() ? modality : modality.negate(); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java deleted file mode 100644 index dbaa524f..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java +++ /dev/null @@ -1,31 +0,0 @@ -package tools.refinery.store.partial.literal; - -import tools.refinery.store.partial.representation.PartialRelation; -import tools.refinery.store.query.Variable; -import tools.refinery.store.query.literal.CallPolarity; -import tools.refinery.store.query.literal.PolarLiteral; - -import java.util.List; -import java.util.Map; - -public final class ModalRelationLiteral extends ModalLiteral - implements PolarLiteral { - public ModalRelationLiteral(CallPolarity polarity, Modality modality, PartialRelation target, - List arguments) { - super(polarity, modality, target, arguments); - } - - public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) { - super(modality, baseLiteral); - } - - @Override - public ModalRelationLiteral substitute(Map substitution) { - return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); - } - - @Override - public ModalRelationLiteral negate() { - return new ModalRelationLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java deleted file mode 100644 index d647ef0a..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java +++ /dev/null @@ -1,31 +0,0 @@ -package tools.refinery.store.partial.literal; - -import tools.refinery.store.query.literal.CallPolarity; - -import java.util.Locale; - -public enum Modality { - MUST, - MAY, - CURRENT; - - public Modality negate() { - return switch(this) { - case MUST -> MAY; - case MAY -> MUST; - case CURRENT -> CURRENT; - }; - } - - public Modality commute(CallPolarity polarity) { - if (polarity.isPositive()) { - return this; - } - return this.negate(); - } - - @Override - public String toString() { - return name().toLowerCase(Locale.ROOT); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java deleted file mode 100644 index 51d388d3..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java +++ /dev/null @@ -1,33 +0,0 @@ -package tools.refinery.store.partial.literal; - -import tools.refinery.store.query.literal.DnfCallLiteral; - -public final class PartialLiterals { - private PartialLiterals() { - throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); - } - - public ModalRelationLiteral may(PartialRelationLiteral literal) { - return new ModalRelationLiteral(Modality.MAY, literal); - } - - public ModalRelationLiteral must(PartialRelationLiteral literal) { - return new ModalRelationLiteral(Modality.MUST, literal); - } - - public ModalRelationLiteral current(PartialRelationLiteral literal) { - return new ModalRelationLiteral(Modality.CURRENT, literal); - } - - public ModalDnfCallLiteral may(DnfCallLiteral literal) { - return new ModalDnfCallLiteral(Modality.MAY, literal); - } - - public ModalDnfCallLiteral must(DnfCallLiteral literal) { - return new ModalDnfCallLiteral(Modality.MUST, literal); - } - - public ModalDnfCallLiteral current(DnfCallLiteral literal) { - return new ModalDnfCallLiteral(Modality.CURRENT, literal); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java deleted file mode 100644 index dc1a1da3..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java +++ /dev/null @@ -1,27 +0,0 @@ -package tools.refinery.store.partial.literal; - -import tools.refinery.store.partial.representation.PartialRelation; -import tools.refinery.store.query.Variable; -import tools.refinery.store.query.literal.CallLiteral; -import tools.refinery.store.query.literal.CallPolarity; -import tools.refinery.store.query.literal.PolarLiteral; - -import java.util.List; -import java.util.Map; - -public final class PartialRelationLiteral extends CallLiteral - implements PolarLiteral { - public PartialRelationLiteral(CallPolarity polarity, PartialRelation target, List substitution) { - super(polarity, target, substitution); - } - - @Override - public PartialRelationLiteral substitute(Map substitution) { - return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); - } - - @Override - public PartialRelationLiteral negate() { - return new PartialRelationLiteral(getPolarity().negate(), getTarget(), getArguments()); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java deleted file mode 100644 index 1113245e..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java +++ /dev/null @@ -1,4 +0,0 @@ -package tools.refinery.store.partial.representation; - -public sealed interface AnyPartialFunction extends AnyPartialSymbol permits PartialFunction { -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java deleted file mode 100644 index 25096e74..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java +++ /dev/null @@ -1,11 +0,0 @@ -package tools.refinery.store.partial.representation; - -import tools.refinery.store.representation.AnyAbstractDomain; - -public sealed interface AnyPartialSymbol permits AnyPartialFunction, PartialSymbol { - String name(); - - int arity(); - - AnyAbstractDomain abstractDomain(); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java deleted file mode 100644 index 3c186f6f..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java +++ /dev/null @@ -1,32 +0,0 @@ -package tools.refinery.store.partial.representation; - -import tools.refinery.store.representation.AbstractDomain; - -public record PartialFunction(String name, int arity, AbstractDomain abstractDomain) - implements AnyPartialFunction, PartialSymbol { - @Override - public A defaultValue() { - return null; - } - - @Override - public C defaultConcreteValue() { - return null; - } - - @Override - public boolean equals(Object o) { - return this == o; - } - - @Override - public int hashCode() { - // Compare by identity to make hash table lookups more efficient. - return System.identityHashCode(this); - } - - @Override - public String toString() { - return "%s/%d".formatted(name, arity); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java deleted file mode 100644 index 127355ca..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java +++ /dev/null @@ -1,66 +0,0 @@ -package tools.refinery.store.partial.representation; - -import tools.refinery.store.partial.literal.ModalRelationLiteral; -import tools.refinery.store.partial.literal.PartialRelationLiteral; -import tools.refinery.store.query.RelationLike; -import tools.refinery.store.query.Variable; -import tools.refinery.store.query.literal.CallPolarity; -import tools.refinery.store.partial.literal.Modality; -import tools.refinery.store.representation.AbstractDomain; -import tools.refinery.store.representation.TruthValue; -import tools.refinery.store.representation.TruthValueDomain; - -import java.util.List; - -public record PartialRelation(String name, int arity) implements PartialSymbol, RelationLike { - @Override - public AbstractDomain abstractDomain() { - return TruthValueDomain.INSTANCE; - } - - @Override - public TruthValue defaultValue() { - return TruthValue.FALSE; - } - - @Override - public Boolean defaultConcreteValue() { - return false; - } - - public ModalRelationLiteral call(CallPolarity polarity, Modality modality, List arguments) { - return new ModalRelationLiteral(polarity, modality, this, arguments); - } - - public PartialRelationLiteral call(CallPolarity polarity, List arguments) { - return new PartialRelationLiteral(polarity, this, arguments); - } - - public PartialRelationLiteral call(CallPolarity polarity, Variable... arguments) { - return call(polarity, List.of(arguments)); - } - - public PartialRelationLiteral call(Variable... arguments) { - return call(CallPolarity.POSITIVE, arguments); - } - - public PartialRelationLiteral callTransitive(Variable left, Variable right) { - return call(CallPolarity.TRANSITIVE, List.of(left, right)); - } - - @Override - public boolean equals(Object o) { - return this == o; - } - - @Override - public int hashCode() { - // Compare by identity to make hash table lookups more efficient. - return System.identityHashCode(this); - } - - @Override - public String toString() { - return "%s/%d".formatted(name, arity); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java deleted file mode 100644 index 38533fa9..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java +++ /dev/null @@ -1,12 +0,0 @@ -package tools.refinery.store.partial.representation; - -import tools.refinery.store.representation.AbstractDomain; - -public sealed interface PartialSymbol extends AnyPartialSymbol permits PartialFunction, PartialRelation { - @Override - AbstractDomain abstractDomain(); - - A defaultValue(); - - C defaultConcreteValue(); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java b/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java deleted file mode 100644 index 9adf6bc8..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java +++ /dev/null @@ -1,6 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -import tools.refinery.store.partial.representation.PartialRelation; - -record EliminatedType(PartialRelation replacement) implements TypeAnalysisResult { -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java b/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java deleted file mode 100644 index d3f66a4c..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java +++ /dev/null @@ -1,101 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -import org.jetbrains.annotations.NotNull; -import tools.refinery.store.partial.representation.PartialRelation; - -import java.util.HashSet; -import java.util.LinkedHashSet; -import java.util.Objects; -import java.util.Set; - -final class ExtendedTypeInfo implements Comparable { - private final int index; - private final PartialRelation type; - private final TypeInfo typeInfo; - private final Set allSubtypes = new LinkedHashSet<>(); - private final Set allSupertypes; - private final Set concreteSubtypesAndSelf = new LinkedHashSet<>(); - private Set directSubtypes; - private final Set unsortedDirectSupertypes = new HashSet<>(); - - public ExtendedTypeInfo(int index, PartialRelation type, TypeInfo typeInfo) { - this.index = index; - this.type = type; - this.typeInfo = typeInfo; - this.allSupertypes = new LinkedHashSet<>(typeInfo.supertypes()); - } - - public PartialRelation getType() { - return type; - } - - public TypeInfo getTypeInfo() { - return typeInfo; - } - - public boolean isAbstractType() { - return getTypeInfo().abstractType(); - } - - public Set getAllSubtypes() { - return allSubtypes; - } - - public Set getAllSupertypes() { - return allSupertypes; - } - - public Set getAllSupertypesAndSelf() { - var allSubtypesAndSelf = new HashSet(allSupertypes.size() + 1); - addMust(allSubtypesAndSelf); - return allSubtypesAndSelf; - } - - public Set getConcreteSubtypesAndSelf() { - return concreteSubtypesAndSelf; - } - - public Set getDirectSubtypes() { - return directSubtypes; - } - - public Set getUnsortedDirectSupertypes() { - return unsortedDirectSupertypes; - } - - public void setDirectSubtypes(Set directSubtypes) { - this.directSubtypes = directSubtypes; - } - - public boolean allowsAllConcreteTypes(Set concreteTypes) { - for (var concreteType : concreteTypes) { - if (!concreteSubtypesAndSelf.contains(concreteType)) { - return false; - } - } - return true; - } - - public void addMust(Set mustTypes) { - mustTypes.add(type); - mustTypes.addAll(allSupertypes); - } - - @Override - public int compareTo(@NotNull ExtendedTypeInfo extendedTypeInfo) { - return Integer.compare(index, extendedTypeInfo.index); - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - ExtendedTypeInfo that = (ExtendedTypeInfo) o; - return index == that.index; - } - - @Override - public int hashCode() { - return Objects.hash(index); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java b/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java deleted file mode 100644 index 729b1fb5..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java +++ /dev/null @@ -1,30 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -import tools.refinery.store.partial.representation.PartialRelation; - -import java.util.Collections; -import java.util.Set; - -record InferredType(Set mustTypes, Set mayConcreteTypes, - PartialRelation currentType) { - public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null); - - public InferredType(Set mustTypes, Set mayConcreteTypes, - PartialRelation currentType) { - this.mustTypes = Collections.unmodifiableSet(mustTypes); - this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes); - this.currentType = currentType; - } - - public boolean isConsistent() { - return currentType != null || mustTypes.isEmpty(); - } - - public boolean isMust(PartialRelation partialRelation) { - return mustTypes.contains(partialRelation); - } - - public boolean isMayConcrete(PartialRelation partialRelation) { - return mayConcreteTypes.contains(partialRelation); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java b/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java deleted file mode 100644 index 0299ae03..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java +++ /dev/null @@ -1,136 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -import tools.refinery.store.partial.representation.PartialRelation; -import tools.refinery.store.representation.TruthValue; - -import java.util.*; - -final class PreservedType implements TypeAnalysisResult { - private final ExtendedTypeInfo extendedTypeInfo; - private final List directSubtypes; - private final List allExternalTypeInfoList; - private final InferredType inferredType; - - public PreservedType(ExtendedTypeInfo extendedTypeInfo, List allExternalTypeInfoList) { - this.extendedTypeInfo = extendedTypeInfo; - directSubtypes = List.copyOf(extendedTypeInfo.getDirectSubtypes()); - this.allExternalTypeInfoList = allExternalTypeInfoList; - inferredType = propagateMust(extendedTypeInfo.getAllSupertypesAndSelf(), - extendedTypeInfo.getConcreteSubtypesAndSelf()); - } - - public PartialRelation type() { - return extendedTypeInfo.getType(); - } - - public List getDirectSubtypes() { - return directSubtypes; - } - - public boolean isAbstractType() { - return extendedTypeInfo.isAbstractType(); - } - - public boolean isVacuous() { - return isAbstractType() && directSubtypes.isEmpty(); - } - - public InferredType asInferredType() { - return inferredType; - } - - public InferredType merge(InferredType inferredType, TruthValue value) { - return switch (value) { - case UNKNOWN -> inferredType; - case TRUE -> addMust(inferredType); - case FALSE -> removeMay(inferredType); - case ERROR -> addError(inferredType); - }; - } - - private InferredType addMust(InferredType inferredType) { - var originalMustTypes = inferredType.mustTypes(); - if (originalMustTypes.contains(type())) { - return inferredType; - } - var mustTypes = new HashSet<>(originalMustTypes); - extendedTypeInfo.addMust(mustTypes); - var originalMayConcreteTypes = inferredType.mayConcreteTypes(); - var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); - Set mayConcreteTypesResult; - if (mayConcreteTypes.retainAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { - mayConcreteTypesResult = mayConcreteTypes; - } else { - mayConcreteTypesResult = originalMayConcreteTypes; - } - return propagateMust(mustTypes, mayConcreteTypesResult); - } - - private InferredType removeMay(InferredType inferredType) { - var originalMayConcreteTypes = inferredType.mayConcreteTypes(); - var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); - if (!mayConcreteTypes.removeAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { - return inferredType; - } - return propagateMust(inferredType.mustTypes(), mayConcreteTypes); - } - - private InferredType addError(InferredType inferredType) { - var originalMustTypes = inferredType.mustTypes(); - if (originalMustTypes.contains(type())) { - if (inferredType.mayConcreteTypes().isEmpty()) { - return inferredType; - } - return new InferredType(originalMustTypes, Set.of(), null); - } - var mustTypes = new HashSet<>(originalMustTypes); - extendedTypeInfo.addMust(mustTypes); - return new InferredType(mustTypes, Set.of(), null); - } - - private InferredType propagateMust(Set originalMustTypes, - Set mayConcreteTypes) { - // It is possible that there is not type at all, do not force one by propagation. - var maybeUntyped = originalMustTypes.isEmpty(); - // Para-consistent case, do not propagate must types to avoid logical explosion. - var paraConsistentOrSurelyUntyped = mayConcreteTypes.isEmpty(); - if (maybeUntyped || paraConsistentOrSurelyUntyped) { - return new InferredType(originalMustTypes, mayConcreteTypes, null); - } - var currentType = computeCurrentType(mayConcreteTypes); - var mustTypes = new HashSet<>(originalMustTypes); - boolean changed = false; - for (var newMustExtendedTypeInfo : allExternalTypeInfoList) { - var newMustType = newMustExtendedTypeInfo.getType(); - if (mustTypes.contains(newMustType)) { - continue; - } - if (newMustExtendedTypeInfo.allowsAllConcreteTypes(mayConcreteTypes)) { - newMustExtendedTypeInfo.addMust(mustTypes); - changed = true; - } - } - if (!changed) { - return new InferredType(originalMustTypes, mayConcreteTypes, currentType); - } - return new InferredType(mustTypes, mayConcreteTypes, currentType); - } - - /** - * Returns a concrete type that is allowed by a (consistent, i.e., nonempty) set of may concrete types. - * - * @param mayConcreteTypes The set of allowed concrete types. Must not be empty. - * @return The first concrete type that is allowed by {@code matConcreteTypes}. - */ - private PartialRelation computeCurrentType(Set mayConcreteTypes) { - for (var concreteExtendedTypeInfo : allExternalTypeInfoList) { - var concreteType = concreteExtendedTypeInfo.getType(); - if (!concreteExtendedTypeInfo.isAbstractType() && mayConcreteTypes.contains(concreteType)) { - return concreteType; - } - } - // We have already filtered out the para-consistent case in {@link #propagateMust(Set, - // Set}. - throw new AssertionError("No concrete type in %s".formatted(mayConcreteTypes)); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java deleted file mode 100644 index 0745f84e..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java +++ /dev/null @@ -1,4 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -sealed interface TypeAnalysisResult permits EliminatedType, PreservedType { -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java b/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java deleted file mode 100644 index 062b4c49..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java +++ /dev/null @@ -1,202 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -import tools.refinery.store.partial.representation.PartialRelation; - -import java.util.*; - -class TypeAnalyzer { - private final Map extendedTypeInfoMap; - private final Map replacements = new LinkedHashMap<>(); - private final InferredType unknownType; - private final Map analysisResults; - - public TypeAnalyzer(Map typeInfoMap) { - int size = typeInfoMap.size(); - extendedTypeInfoMap = new LinkedHashMap<>(size); - var concreteTypes = new LinkedHashSet(); - int index = 0; - for (var entry : typeInfoMap.entrySet()) { - var type = entry.getKey(); - var typeInfo = entry.getValue(); - extendedTypeInfoMap.put(type, new ExtendedTypeInfo(index, type, typeInfo)); - if (!typeInfo.abstractType()) { - concreteTypes.add(type); - } - index++; - } - unknownType = new InferredType(Set.of(), concreteTypes, null); - computeAllSupertypes(); - computeAllAndConcreteSubtypes(); - computeDirectSubtypes(); - eliminateTrivialSupertypes(); - analysisResults = computeAnalysisResults(); - } - - public InferredType getUnknownType() { - return unknownType; - } - - public Map getAnalysisResults() { - return analysisResults; - } - - private void computeAllSupertypes() { - boolean changed; - do { - changed = false; - for (var extendedTypeInfo : extendedTypeInfoMap.values()) { - var found = new HashSet(); - var allSupertypes = extendedTypeInfo.getAllSupertypes(); - for (var supertype : allSupertypes) { - found.addAll(extendedTypeInfoMap.get(supertype).getAllSupertypes()); - } - if (allSupertypes.addAll(found)) { - changed = true; - } - } - } while (changed); - } - - private void computeAllAndConcreteSubtypes() { - for (var extendedTypeInfo : extendedTypeInfoMap.values()) { - var type = extendedTypeInfo.getType(); - if (!extendedTypeInfo.isAbstractType()) { - extendedTypeInfo.getConcreteSubtypesAndSelf().add(type); - } - for (var supertype : extendedTypeInfo.getAllSupertypes()) { - if (type.equals(supertype)) { - throw new IllegalArgumentException("%s cannot be a supertype of itself".formatted(type)); - } - var supertypeInfo = extendedTypeInfoMap.get(supertype); - supertypeInfo.getAllSubtypes().add(type); - if (!extendedTypeInfo.isAbstractType()) { - supertypeInfo.getConcreteSubtypesAndSelf().add(type); - } - } - } - } - - private void computeDirectSubtypes() { - for (var extendedTypeInfo : extendedTypeInfoMap.values()) { - var allSubtypes = extendedTypeInfo.getAllSubtypes(); - var directSubtypes = new LinkedHashSet<>(allSubtypes); - var indirectSubtypes = new LinkedHashSet(allSubtypes.size()); - for (var subtype : allSubtypes) { - indirectSubtypes.addAll(extendedTypeInfoMap.get(subtype).getAllSubtypes()); - } - directSubtypes.removeAll(indirectSubtypes); - extendedTypeInfo.setDirectSubtypes(directSubtypes); - } - } - - private void eliminateTrivialSupertypes() { - boolean changed; - do { - var toRemove = new ArrayList(); - for (var entry : extendedTypeInfoMap.entrySet()) { - var extendedTypeInfo = entry.getValue(); - boolean isAbstract = extendedTypeInfo.isAbstractType(); - // Do not eliminate abstract types with 0 subtypes, because they can be used para-consistently, i.e., - // an object determined to must have an abstract type with 0 subtypes may not ever exist. - boolean hasSingleDirectSubtype = extendedTypeInfo.getDirectSubtypes().size() == 1; - if (isAbstract && hasSingleDirectSubtype) { - toRemove.add(entry.getKey()); - } - } - toRemove.forEach(this::removeTrivialType); - changed = !toRemove.isEmpty(); - } while (changed); - } - - private void removeTrivialType(PartialRelation trivialType) { - var extendedTypeInfo = extendedTypeInfoMap.get(trivialType); - var iterator = extendedTypeInfo.getDirectSubtypes().iterator(); - if (!iterator.hasNext()) { - throw new AssertionError("Expected trivial supertype %s to have a direct subtype" - .formatted(trivialType)); - } - PartialRelation replacement = setReplacement(trivialType, iterator.next()); - if (iterator.hasNext()) { - throw new AssertionError("Expected trivial supertype %s to have at most 1 direct subtype" - .formatted(trivialType)); - } - replacements.put(trivialType, replacement); - for (var supertype : extendedTypeInfo.getAllSupertypes()) { - var extendedSupertypeInfo = extendedTypeInfoMap.get(supertype); - if (!extendedSupertypeInfo.getAllSubtypes().remove(trivialType)) { - throw new AssertionError("Expected %s to be subtype of %s".formatted(trivialType, supertype)); - } - var directSubtypes = extendedSupertypeInfo.getDirectSubtypes(); - if (directSubtypes.remove(trivialType)) { - directSubtypes.add(replacement); - } - } - for (var subtype : extendedTypeInfo.getAllSubtypes()) { - var extendedSubtypeInfo = extendedTypeInfoMap.get(subtype); - if (!extendedSubtypeInfo.getAllSupertypes().remove(trivialType)) { - throw new AssertionError("Expected %s to be supertype of %s".formatted(trivialType, subtype)); - } - } - extendedTypeInfoMap.remove(trivialType); - } - - private PartialRelation setReplacement(PartialRelation trivialRelation, PartialRelation replacement) { - if (replacement == null) { - return trivialRelation; - } - var resolved = setReplacement(replacement, replacements.get(replacement)); - replacements.put(trivialRelation, resolved); - return resolved; - } - - private Map computeAnalysisResults() { - var allExtendedTypeInfoList = sortTypes(); - var results = new LinkedHashMap( - allExtendedTypeInfoList.size() + replacements.size()); - for (var extendedTypeInfo : allExtendedTypeInfoList) { - var type = extendedTypeInfo.getType(); - results.put(type, new PreservedType(extendedTypeInfo, allExtendedTypeInfoList)); - } - for (var entry : replacements.entrySet()) { - var type = entry.getKey(); - results.put(type, new EliminatedType(entry.getValue())); - } - return Collections.unmodifiableMap(results); - } - - private List sortTypes() { - // Invert {@code directSubtypes} to keep track of the out-degree of types. - for (var extendedTypeInfo : extendedTypeInfoMap.values()) { - for (var directSubtype : extendedTypeInfo.getDirectSubtypes()) { - var extendedDirectSubtypeInfo = extendedTypeInfoMap.get(directSubtype); - extendedDirectSubtypeInfo.getUnsortedDirectSupertypes().add(extendedTypeInfo.getType()); - } - } - // Build a inverse topological order ({@code extends} edges always points to earlier nodes in the order, - // breaking ties according to the original order ({@link ExtendedTypeInfo#index}) to form a 'stable' sort. - // See, e.g., https://stackoverflow.com/a/11236027. - var priorityQueue = new PriorityQueue(); - for (var extendedTypeInfo : extendedTypeInfoMap.values()) { - if (extendedTypeInfo.getUnsortedDirectSupertypes().isEmpty()) { - priorityQueue.add(extendedTypeInfo); - } - } - var sorted = new ArrayList(extendedTypeInfoMap.size()); - while (!priorityQueue.isEmpty()) { - var extendedTypeInfo = priorityQueue.remove(); - sorted.add(extendedTypeInfo); - for (var directSubtype : extendedTypeInfo.getDirectSubtypes()) { - var extendedDirectSubtypeInfo = extendedTypeInfoMap.get(directSubtype); - var unsortedDirectSupertypes = extendedDirectSubtypeInfo.getUnsortedDirectSupertypes(); - if (!unsortedDirectSupertypes.remove(extendedTypeInfo.getType())) { - throw new AssertionError("Expected %s to be a direct supertype of %s" - .formatted(extendedTypeInfo.getType(), directSubtype)); - } - if (unsortedDirectSupertypes.isEmpty()) { - priorityQueue.add(extendedDirectSubtypeInfo); - } - } - } - return Collections.unmodifiableList(sorted); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java b/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java deleted file mode 100644 index 1b0922fe..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java +++ /dev/null @@ -1,46 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -import tools.refinery.store.partial.representation.PartialRelation; - -import java.util.*; - -public record TypeInfo(Collection supertypes, boolean abstractType) { - public static Builder builder() { - return new Builder(); - } - - public static class Builder { - private final Set supertypes = new LinkedHashSet<>(); - private boolean abstractType; - - private Builder() { - } - - public Builder supertypes(Collection supertypes) { - this.supertypes.addAll(supertypes); - return this; - } - - public Builder supertypes(PartialRelation... supertypes) { - return supertypes(List.of(supertypes)); - } - - public Builder supertype(PartialRelation supertype) { - supertypes.add(supertype); - return this; - } - - public Builder abstractType(boolean abstractType) { - this.abstractType = abstractType; - return this; - } - - public Builder abstractType() { - return abstractType(true); - } - - public TypeInfo build() { - return new TypeInfo(Collections.unmodifiableSet(supertypes), abstractType); - } - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java deleted file mode 100644 index b080094f..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java +++ /dev/null @@ -1,187 +0,0 @@ -package tools.refinery.store.query; - -import tools.refinery.store.query.literal.CallPolarity; -import tools.refinery.store.query.literal.DnfCallLiteral; -import tools.refinery.store.query.literal.Literal; - -import java.util.*; - -public final class Dnf implements RelationLike { - private final String name; - - private final String uniqueName; - - private final List parameters; - - private final List> functionalDependencies; - - private final List clauses; - - private Dnf(String name, List parameters, List> functionalDependencies, - List clauses) { - validateFunctionalDependencies(parameters, functionalDependencies); - this.name = name; - this.uniqueName = DnfUtils.generateUniqueName(name); - this.parameters = parameters; - this.functionalDependencies = functionalDependencies; - this.clauses = clauses; - } - - private static void validateFunctionalDependencies( - Collection parameters, Collection> functionalDependencies) { - var parameterSet = new HashSet<>(parameters); - for (var functionalDependency : functionalDependencies) { - validateParameters(parameters, parameterSet, functionalDependency.forEach(), functionalDependency); - validateParameters(parameters, parameterSet, functionalDependency.unique(), functionalDependency); - } - } - - private static void validateParameters(Collection parameters, Set parameterSet, - Collection toValidate, - FunctionalDependency functionalDependency) { - for (var variable : toValidate) { - if (!parameterSet.contains(variable)) { - throw new IllegalArgumentException( - "Variable %s of functional dependency %s does not appear in the parameter list %s" - .formatted(variable, functionalDependency, parameters)); - } - } - } - - @Override - public String name() { - return name; - } - - public String getUniqueName() { - return uniqueName; - } - - public List getParameters() { - return parameters; - } - - public List> getFunctionalDependencies() { - return functionalDependencies; - } - - @Override - public int arity() { - return parameters.size(); - } - - public List getClauses() { - return clauses; - } - - public DnfCallLiteral call(CallPolarity polarity, List arguments) { - return new DnfCallLiteral(polarity, this, arguments); - } - - public DnfCallLiteral call(CallPolarity polarity, Variable... arguments) { - return call(polarity, List.of(arguments)); - } - - public DnfCallLiteral call(Variable... arguments) { - return call(CallPolarity.POSITIVE, arguments); - } - - public DnfCallLiteral callTransitive(Variable left, Variable right) { - return call(CallPolarity.TRANSITIVE, List.of(left, right)); - } - - public static Builder builder() { - return builder(null); - } - - public static Builder builder(String name) { - return new Builder(name); - } - - @SuppressWarnings("UnusedReturnValue") - public static class Builder { - private final String name; - - private final List parameters = new ArrayList<>(); - - private final List> functionalDependencies = new ArrayList<>(); - - private final List> clauses = new ArrayList<>(); - - private Builder(String name) { - this.name = name; - } - - public Builder parameter(Variable variable) { - parameters.add(variable); - return this; - } - - public Builder parameters(Variable... variables) { - return parameters(List.of(variables)); - } - - public Builder parameters(Collection variables) { - parameters.addAll(variables); - return this; - } - - public Builder functionalDependencies(Collection> functionalDependencies) { - this.functionalDependencies.addAll(functionalDependencies); - return this; - } - - public Builder functionalDependency(FunctionalDependency functionalDependency) { - functionalDependencies.add(functionalDependency); - return this; - } - - public Builder functionalDependency(Set forEach, Set unique) { - return functionalDependency(new FunctionalDependency<>(forEach, unique)); - } - - public Builder clause(Literal... atoms) { - clauses.add(List.of(atoms)); - return this; - } - - public Builder clause(Collection atoms) { - clauses.add(List.copyOf(atoms)); - return this; - } - - public Builder clause(DnfClause clause) { - return clause(clause.literals()); - } - - public Builder clauses(DnfClause... clauses) { - for (var clause : clauses) { - this.clause(clause); - } - return this; - } - - public Builder clauses(Collection clauses) { - for (var clause : clauses) { - this.clause(clause); - } - return this; - } - - public Dnf build() { - var postProcessedClauses = new ArrayList(); - for (var constraints : clauses) { - var variables = new HashSet(); - for (var constraint : constraints) { - constraint.collectAllVariables(variables); - } - parameters.forEach(variables::remove); - postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables), - Collections.unmodifiableList(constraints))); - } - return new Dnf(name, Collections.unmodifiableList(parameters), - Collections.unmodifiableList(functionalDependencies), - Collections.unmodifiableList(postProcessedClauses)); - } - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DnfClause.java b/subprojects/store/src/main/java/tools/refinery/store/query/DnfClause.java deleted file mode 100644 index 2ba6becc..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/DnfClause.java +++ /dev/null @@ -1,9 +0,0 @@ -package tools.refinery.store.query; - -import tools.refinery.store.query.literal.Literal; - -import java.util.List; -import java.util.Set; - -public record DnfClause(Set quantifiedVariables, List literals) { -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java deleted file mode 100644 index 17564d43..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java +++ /dev/null @@ -1,24 +0,0 @@ -package tools.refinery.store.query; - -import java.util.Map; -import java.util.UUID; - -public final class DnfUtils { - private DnfUtils() { - throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); - } - - public static String generateUniqueName(String originalName) { - UUID uuid = UUID.randomUUID(); - String uniqueString = "_" + uuid.toString().replace('-', '_'); - if (originalName == null) { - return uniqueString; - } else { - return originalName + uniqueString; - } - } - - public static Variable maybeSubstitute(Variable variable, Map substitution) { - return substitution.getOrDefault(variable, variable); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/FunctionalDependency.java b/subprojects/store/src/main/java/tools/refinery/store/query/FunctionalDependency.java deleted file mode 100644 index 63a81713..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/FunctionalDependency.java +++ /dev/null @@ -1,15 +0,0 @@ -package tools.refinery.store.query; - -import java.util.HashSet; -import java.util.Set; - -public record FunctionalDependency(Set forEach, Set unique) { - public FunctionalDependency { - var uniqueForEach = new HashSet<>(unique); - uniqueForEach.retainAll(forEach); - if (!uniqueForEach.isEmpty()) { - throw new IllegalArgumentException("Variables %s appear on both sides of the functional dependency" - .formatted(uniqueForEach)); - } - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQuery.java b/subprojects/store/src/main/java/tools/refinery/store/query/ModelQuery.java deleted file mode 100644 index 6a1aeabb..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQuery.java +++ /dev/null @@ -1,11 +0,0 @@ -package tools.refinery.store.query; - -import tools.refinery.store.adapter.ModelAdapterType; - -public final class ModelQuery extends ModelAdapterType { - public static final ModelQuery ADAPTER = new ModelQuery(); - - private ModelQuery() { - super(ModelQueryAdapter.class, ModelQueryStoreAdapter.class, ModelQueryBuilder.class); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java b/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java deleted file mode 100644 index f7762444..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java +++ /dev/null @@ -1,13 +0,0 @@ -package tools.refinery.store.query; - -import tools.refinery.store.adapter.ModelAdapter; - -public interface ModelQueryAdapter extends ModelAdapter { - ModelQueryStoreAdapter getStoreAdapter(); - - ResultSet getResultSet(Dnf query); - - boolean hasPendingChanges(); - - void flushChanges(); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java b/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java deleted file mode 100644 index b3cfb4b4..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java +++ /dev/null @@ -1,23 +0,0 @@ -package tools.refinery.store.query; - -import tools.refinery.store.adapter.ModelAdapterBuilder; -import tools.refinery.store.model.ModelStore; - -import java.util.Collection; -import java.util.List; - -public interface ModelQueryBuilder extends ModelAdapterBuilder { - default ModelQueryBuilder queries(Dnf... queries) { - return queries(List.of(queries)); - } - - default ModelQueryBuilder queries(Collection queries) { - queries.forEach(this::query); - return this; - } - - ModelQueryBuilder query(Dnf query); - - @Override - ModelQueryStoreAdapter createStoreAdapter(ModelStore store); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java b/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java deleted file mode 100644 index 3efeacaa..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java +++ /dev/null @@ -1,16 +0,0 @@ -package tools.refinery.store.query; - -import tools.refinery.store.adapter.ModelStoreAdapter; -import tools.refinery.store.model.Model; -import tools.refinery.store.query.view.AnyRelationView; - -import java.util.Collection; - -public interface ModelQueryStoreAdapter extends ModelStoreAdapter { - Collection getRelationViews(); - - Collection getQueries(); - - @Override - ModelQueryAdapter createModelAdapter(Model model); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/RelationLike.java b/subprojects/store/src/main/java/tools/refinery/store/query/RelationLike.java deleted file mode 100644 index 8c784d8b..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/RelationLike.java +++ /dev/null @@ -1,11 +0,0 @@ -package tools.refinery.store.query; - -public interface RelationLike { - String name(); - - int arity(); - - default boolean invalidIndex(int i) { - return i < 0 || i >= arity(); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ResultSet.java b/subprojects/store/src/main/java/tools/refinery/store/query/ResultSet.java deleted file mode 100644 index 3542e252..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/ResultSet.java +++ /dev/null @@ -1,25 +0,0 @@ -package tools.refinery.store.query; - -import tools.refinery.store.tuple.Tuple; -import tools.refinery.store.tuple.TupleLike; - -import java.util.Optional; -import java.util.stream.Stream; - -public interface ResultSet { - boolean hasResult(); - - boolean hasResult(Tuple parameters); - - Optional oneResult(); - - Optional oneResult(Tuple parameters); - - Stream allResults(); - - Stream allResults(Tuple parameters); - - int countResults(); - - int countResults(Tuple parameters); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java deleted file mode 100644 index 2eb87649..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java +++ /dev/null @@ -1,58 +0,0 @@ -package tools.refinery.store.query; - -import tools.refinery.store.query.literal.ConstantLiteral; -import tools.refinery.store.query.literal.EquivalenceLiteral; - -import java.util.Objects; - -public class Variable { - private final String name; - private final String uniqueName; - - public Variable() { - this(null); - } - - public Variable(String name) { - super(); - this.name = name; - this.uniqueName = DnfUtils.generateUniqueName(name); - - } - public String getName() { - return name; - } - - public String getUniqueName() { - return uniqueName; - } - - public boolean isNamed() { - return name != null; - } - - public ConstantLiteral isConstant(int value) { - return new ConstantLiteral(this, value); - } - - public EquivalenceLiteral isEquivalent(Variable other) { - return new EquivalenceLiteral(true, this, other); - } - - public EquivalenceLiteral notEquivalent(Variable other) { - return new EquivalenceLiteral(false, this, other); - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - Variable variable = (Variable) o; - return Objects.equals(uniqueName, variable.uniqueName); - } - - @Override - public int hashCode() { - return Objects.hash(uniqueName); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java deleted file mode 100644 index 5e1ae94d..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java +++ /dev/null @@ -1,66 +0,0 @@ -package tools.refinery.store.query.literal; - -import tools.refinery.store.query.DnfUtils; -import tools.refinery.store.query.RelationLike; -import tools.refinery.store.query.Variable; - -import java.util.List; -import java.util.Map; -import java.util.Objects; -import java.util.Set; - -public abstract class CallLiteral implements Literal { - private final CallPolarity polarity; - private final T target; - private final List arguments; - - protected CallLiteral(CallPolarity polarity, T target, List arguments) { - if (arguments.size() != target.arity()) { - throw new IllegalArgumentException("%s needs %d arguments, but got %s".formatted(target.name(), - target.arity(), arguments.size())); - } - if (polarity.isTransitive() && target.arity() != 2) { - throw new IllegalArgumentException("Transitive closures can only take binary relations"); - } - this.polarity = polarity; - this.target = target; - this.arguments = arguments; - } - - public CallPolarity getPolarity() { - return polarity; - } - - public T getTarget() { - return target; - } - - public List getArguments() { - return arguments; - } - - @Override - public void collectAllVariables(Set variables) { - if (polarity.isPositive()) { - variables.addAll(arguments); - } - } - - protected List substituteArguments(Map substitution) { - return arguments.stream().map(variable -> DnfUtils.maybeSubstitute(variable, substitution)).toList(); - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - CallLiteral callAtom = (CallLiteral) o; - return polarity == callAtom.polarity && Objects.equals(target, callAtom.target) && - Objects.equals(arguments, callAtom.arguments); - } - - @Override - public int hashCode() { - return Objects.hash(polarity, target, arguments); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java deleted file mode 100644 index 84b4b771..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java +++ /dev/null @@ -1,32 +0,0 @@ -package tools.refinery.store.query.literal; - -public enum CallPolarity { - POSITIVE(true, false), - NEGATIVE(false, false), - TRANSITIVE(true, true); - - private final boolean positive; - - private final boolean transitive; - - CallPolarity(boolean positive, boolean transitive) { - this.positive = positive; - this.transitive = transitive; - } - - public boolean isPositive() { - return positive; - } - - public boolean isTransitive() { - return transitive; - } - - public CallPolarity negate() { - return switch (this) { - case POSITIVE -> NEGATIVE; - case NEGATIVE -> POSITIVE; - case TRANSITIVE -> throw new IllegalArgumentException("Transitive polarity cannot be negated"); - }; - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java deleted file mode 100644 index 746d23af..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java +++ /dev/null @@ -1,19 +0,0 @@ -package tools.refinery.store.query.literal; - -import tools.refinery.store.query.DnfUtils; -import tools.refinery.store.query.Variable; - -import java.util.Map; -import java.util.Set; - -public record ConstantLiteral(Variable variable, int nodeId) implements Literal { - @Override - public void collectAllVariables(Set variables) { - variables.add(variable); - } - - @Override - public ConstantLiteral substitute(Map substitution) { - return new ConstantLiteral(DnfUtils.maybeSubstitute(variable, substitution), nodeId); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java deleted file mode 100644 index 40499222..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java +++ /dev/null @@ -1,23 +0,0 @@ -package tools.refinery.store.query.literal; - -import tools.refinery.store.query.Dnf; -import tools.refinery.store.query.Variable; - -import java.util.List; -import java.util.Map; - -public final class DnfCallLiteral extends CallLiteral implements PolarLiteral { - public DnfCallLiteral(CallPolarity polarity, Dnf target, List arguments) { - super(polarity, target, arguments); - } - - @Override - public DnfCallLiteral substitute(Map substitution) { - return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); - } - - @Override - public DnfCallLiteral negate() { - return new DnfCallLiteral(getPolarity().negate(), getTarget(), getArguments()); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java deleted file mode 100644 index 5fee54b1..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java +++ /dev/null @@ -1,27 +0,0 @@ -package tools.refinery.store.query.literal; - -import tools.refinery.store.query.DnfUtils; -import tools.refinery.store.query.Variable; - -import java.util.Map; -import java.util.Set; - -public record EquivalenceLiteral(boolean positive, Variable left, Variable right) - implements PolarLiteral { - @Override - public void collectAllVariables(Set variables) { - variables.add(left); - variables.add(right); - } - - @Override - public EquivalenceLiteral negate() { - return new EquivalenceLiteral(!positive, left, right); - } - - @Override - public EquivalenceLiteral substitute(Map substitution) { - return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution), - DnfUtils.maybeSubstitute(right, substitution)); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java deleted file mode 100644 index e0f5f605..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java +++ /dev/null @@ -1,12 +0,0 @@ -package tools.refinery.store.query.literal; - -import tools.refinery.store.query.Variable; - -import java.util.Map; -import java.util.Set; - -public interface Literal { - void collectAllVariables(Set variables); - - Literal substitute(Map substitution); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java deleted file mode 100644 index 2c7e893f..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java +++ /dev/null @@ -1,11 +0,0 @@ -package tools.refinery.store.query.literal; - -public final class Literals { - private Literals() { - throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); - } - - public static > T not(PolarLiteral literal) { - return literal.negate(); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java deleted file mode 100644 index 32523675..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java +++ /dev/null @@ -1,5 +0,0 @@ -package tools.refinery.store.query.literal; - -public interface PolarLiteral> extends Literal { - T negate(); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java deleted file mode 100644 index 4718b550..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java +++ /dev/null @@ -1,24 +0,0 @@ -package tools.refinery.store.query.literal; - -import tools.refinery.store.query.Variable; -import tools.refinery.store.query.view.AnyRelationView; - -import java.util.List; -import java.util.Map; - -public final class RelationViewLiteral extends CallLiteral - implements PolarLiteral { - public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List arguments) { - super(polarity, target, arguments); - } - - @Override - public RelationViewLiteral substitute(Map substitution) { - return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); - } - - @Override - public RelationViewLiteral negate() { - return new RelationViewLiteral(getPolarity().negate(), getTarget(), getArguments()); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/AnyRelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/AnyRelationView.java deleted file mode 100644 index 328cde3a..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/AnyRelationView.java +++ /dev/null @@ -1,24 +0,0 @@ -package tools.refinery.store.query.view; - -import tools.refinery.store.model.Model; -import tools.refinery.store.query.FunctionalDependency; -import tools.refinery.store.representation.AnySymbol; -import tools.refinery.store.query.RelationLike; - -import java.util.Set; - -public sealed interface AnyRelationView extends RelationLike permits RelationView { - AnySymbol getSymbol(); - - default Set> getFunctionalDependencies() { - return Set.of(); - } - - default Set getImpliedRelationViews() { - return Set.of(); - } - - boolean get(Model model, Object[] tuple); - - Iterable getAll(Model model); -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java deleted file mode 100644 index 64c601bb..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java +++ /dev/null @@ -1,49 +0,0 @@ -package tools.refinery.store.query.view; - -import tools.refinery.store.tuple.Tuple; -import tools.refinery.store.representation.Symbol; - -import java.util.Objects; -import java.util.function.BiPredicate; -import java.util.function.Predicate; - -public class FilteredRelationView extends TuplePreservingRelationView { - private final BiPredicate predicate; - - public FilteredRelationView(Symbol symbol, String name, BiPredicate predicate) { - super(symbol, name); - this.predicate = predicate; - } - - public FilteredRelationView(Symbol symbol, BiPredicate predicate) { - super(symbol); - this.predicate = predicate; - } - - public FilteredRelationView(Symbol symbol, String name, Predicate predicate) { - this(symbol, name, (k, v) -> predicate.test(v)); - } - - public FilteredRelationView(Symbol symbol, Predicate predicate) { - this(symbol, (k, v) -> predicate.test(v)); - } - - @Override - public boolean filter(Tuple key, T value) { - return this.predicate.test(key, value); - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - if (!super.equals(o)) return false; - FilteredRelationView that = (FilteredRelationView) o; - return Objects.equals(predicate, that.predicate); - } - - @Override - public int hashCode() { - return Objects.hash(super.hashCode(), predicate); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java deleted file mode 100644 index 3d278a8b..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java +++ /dev/null @@ -1,71 +0,0 @@ -package tools.refinery.store.query.view; - -import tools.refinery.store.model.Model; -import tools.refinery.store.query.FunctionalDependency; -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.tuple.Tuple; -import tools.refinery.store.tuple.Tuple1; - -import java.util.Set; -import java.util.stream.Collectors; -import java.util.stream.IntStream; - -public final class FunctionalRelationView extends RelationView { - public FunctionalRelationView(Symbol symbol, String name) { - super(symbol, name); - } - - public FunctionalRelationView(Symbol symbol) { - super(symbol); - } - - @Override - public Set> getFunctionalDependencies() { - var arity = getSymbol().arity(); - var forEach = IntStream.range(0, arity).boxed().collect(Collectors.toUnmodifiableSet()); - var unique = Set.of(arity); - return Set.of(new FunctionalDependency<>(forEach, unique)); - } - - @Override - public Set getImpliedRelationViews() { - var symbol = getSymbol(); - var impliedIndices = IntStream.range(0, symbol.arity()).boxed().toList(); - var keyOnlyRelationView = new KeyOnlyRelationView<>(symbol); - return Set.of(new RelationViewImplication(this, keyOnlyRelationView, impliedIndices)); - } - - @Override - public boolean filter(Tuple key, T value) { - return true; - } - - @Override - public Object[] forwardMap(Tuple key, T value) { - int size = key.getSize(); - Object[] result = new Object[size + 1]; - for (int i = 0; i < size; i++) { - result[i] = Tuple.of(key.get(i)); - } - result[key.getSize()] = value; - return result; - } - - @Override - public boolean get(Model model, Object[] tuple) { - int[] content = new int[tuple.length - 1]; - for (int i = 0; i < tuple.length - 1; i++) { - content[i] = ((Tuple1) tuple[i]).value0(); - } - Tuple key = Tuple.of(content); - @SuppressWarnings("unchecked") - T valueInTuple = (T) tuple[tuple.length - 1]; - T valueInMap = model.getInterpretation(getSymbol()).get(key); - return valueInTuple.equals(valueInMap); - } - - @Override - public int arity() { - return getSymbol().arity() + 1; - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java deleted file mode 100644 index e1b2e45b..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java +++ /dev/null @@ -1,36 +0,0 @@ -package tools.refinery.store.query.view; - -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.tuple.Tuple; - -import java.util.Objects; - -public final class KeyOnlyRelationView extends TuplePreservingRelationView { - public static final String VIEW_NAME = "key"; - - private final T defaultValue; - - public KeyOnlyRelationView(Symbol symbol) { - super(symbol, VIEW_NAME); - defaultValue = symbol.defaultValue(); - } - - @Override - public boolean filter(Tuple key, T value) { - return !Objects.equals(value, defaultValue); - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - if (!super.equals(o)) return false; - KeyOnlyRelationView that = (KeyOnlyRelationView) o; - return Objects.equals(defaultValue, that.defaultValue); - } - - @Override - public int hashCode() { - return Objects.hash(super.hashCode(), defaultValue); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java deleted file mode 100644 index 6accd27a..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java +++ /dev/null @@ -1,82 +0,0 @@ -package tools.refinery.store.query.view; - -import tools.refinery.store.map.CursorAsIterator; -import tools.refinery.store.model.Model; -import tools.refinery.store.query.Variable; -import tools.refinery.store.query.literal.CallPolarity; -import tools.refinery.store.query.literal.RelationViewLiteral; -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.tuple.Tuple; - -import java.util.List; -import java.util.Objects; -import java.util.UUID; - -/** - * Represents a view of a {@link Symbol} that can be queried. - * - * @param - * @author Oszkar Semerath - */ -public abstract non-sealed class RelationView implements AnyRelationView { - private final Symbol symbol; - - private final String name; - - protected RelationView(Symbol symbol, String name) { - this.symbol = symbol; - this.name = name; - } - - protected RelationView(Symbol representation) { - this(representation, UUID.randomUUID().toString()); - } - - @Override - public Symbol getSymbol() { - return symbol; - } - - @Override - public String name() { - return symbol.name() + "#" + name; - } - - public abstract boolean filter(Tuple key, T value); - - public abstract Object[] forwardMap(Tuple key, T value); - - @Override - public Iterable getAll(Model model) { - return (() -> new CursorAsIterator<>(model.getInterpretation(symbol).getAll(), this::forwardMap, this::filter)); - } - - public RelationViewLiteral call(CallPolarity polarity, List arguments) { - return new RelationViewLiteral(polarity, this, arguments); - } - - public RelationViewLiteral call(CallPolarity polarity, Variable... arguments) { - return call(polarity, List.of(arguments)); - } - - public RelationViewLiteral call(Variable... arguments) { - return call(CallPolarity.POSITIVE, arguments); - } - - public RelationViewLiteral callTransitive(Variable left, Variable right) { - return call(CallPolarity.TRANSITIVE, List.of(left, right)); - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - RelationView that = (RelationView) o; - return Objects.equals(symbol, that.symbol) && Objects.equals(name, that.name); - } - - @Override - public int hashCode() { - return Objects.hash(symbol, name); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java deleted file mode 100644 index 2ba1fcc4..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java +++ /dev/null @@ -1,19 +0,0 @@ -package tools.refinery.store.query.view; - -import java.util.List; - -public record RelationViewImplication(AnyRelationView implyingRelationView, AnyRelationView impliedRelationView, - List impliedIndices) { - public RelationViewImplication { - if (impliedIndices.size() != impliedRelationView.arity()) { - throw new IllegalArgumentException("Expected %d implied indices for %s, but %d are provided" - .formatted(impliedRelationView.arity(), impliedRelationView, impliedIndices.size())); - } - for (var index : impliedIndices) { - if (impliedRelationView.invalidIndex(index)) { - throw new IllegalArgumentException("%d is not a valid index for %s".formatted(index, - implyingRelationView)); - } - } - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java deleted file mode 100644 index 8cc4986e..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java +++ /dev/null @@ -1,44 +0,0 @@ -package tools.refinery.store.query.view; - -import tools.refinery.store.model.Model; -import tools.refinery.store.tuple.Tuple; -import tools.refinery.store.tuple.Tuple1; -import tools.refinery.store.representation.Symbol; - -public abstract class TuplePreservingRelationView extends RelationView { - protected TuplePreservingRelationView(Symbol symbol, String name) { - super(symbol, name); - } - - protected TuplePreservingRelationView(Symbol symbol) { - super(symbol); - } - - public Object[] forwardMap(Tuple key) { - Object[] result = new Object[key.getSize()]; - for (int i = 0; i < key.getSize(); i++) { - result[i] = Tuple.of(key.get(i)); - } - return result; - } - - @Override - public Object[] forwardMap(Tuple key, T value) { - return forwardMap(key); - } - - @Override - public boolean get(Model model, Object[] tuple) { - int[] content = new int[tuple.length]; - for (int i = 0; i < tuple.length; i++) { - content[i] = ((Tuple1) tuple[i]).value0(); - } - Tuple key = Tuple.of(content); - T value = model.getInterpretation(getSymbol()).get(key); - return filter(key, value); - } - - public int arity() { - return this.getSymbol().arity(); - } -} diff --git a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java b/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java deleted file mode 100644 index 9efa76ef..00000000 --- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java +++ /dev/null @@ -1,32 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -import org.junit.jupiter.api.Test; -import tools.refinery.store.partial.representation.PartialRelation; - -import java.util.Set; - -import static org.hamcrest.MatcherAssert.assertThat; -import static org.hamcrest.Matchers.is; - -class InferredTypeTest { - private final PartialRelation c1 = new PartialRelation("C1", 1); - private final PartialRelation c2 = new PartialRelation("C2", 1); - - @Test - void untypedIsConsistentTest() { - var sut = new InferredType(Set.of(), Set.of(c1, c2), null); - assertThat(sut.isConsistent(), is(true)); - } - - @Test - void typedIsConsistentTest() { - var sut = new InferredType(Set.of(c1), Set.of(c1, c2), c1); - assertThat(sut.isConsistent(), is(true)); - } - - @Test - void typedIsInconsistentTest() { - var sut = new InferredType(Set.of(c1), Set.of(), null); - assertThat(sut.isConsistent(), is(false)); - } -} diff --git a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java deleted file mode 100644 index 5f528328..00000000 --- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java +++ /dev/null @@ -1,203 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -import org.junit.jupiter.api.BeforeEach; -import org.junit.jupiter.api.Test; -import tools.refinery.store.partial.representation.PartialRelation; -import tools.refinery.store.representation.TruthValue; - -import java.util.LinkedHashMap; -import java.util.Set; - -import static org.hamcrest.MatcherAssert.assertThat; -import static org.hamcrest.Matchers.is; -import static org.junit.jupiter.api.Assertions.assertAll; - -class TypeAnalyzerExampleHierarchyTest { - private final PartialRelation a1 = new PartialRelation("A1", 1); - private final PartialRelation a2 = new PartialRelation("A2", 1); - private final PartialRelation a3 = new PartialRelation("A3", 1); - private final PartialRelation a4 = new PartialRelation("A4", 1); - private final PartialRelation a5 = new PartialRelation("A5", 1); - private final PartialRelation c1 = new PartialRelation("C1", 1); - private final PartialRelation c2 = new PartialRelation("C2", 1); - private final PartialRelation c3 = new PartialRelation("C3", 1); - private final PartialRelation c4 = new PartialRelation("C4", 1); - - private TypeAnalyzer sut; - private TypeAnalyzerTester tester; - - @BeforeEach - void beforeEach() { - var typeInfoMap = new LinkedHashMap(); - typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); - typeInfoMap.put(a2, TypeInfo.builder().abstractType().build()); - typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); - typeInfoMap.put(a4, TypeInfo.builder().abstractType().build()); - typeInfoMap.put(a5, TypeInfo.builder().abstractType().build()); - typeInfoMap.put(c1, TypeInfo.builder().supertypes(a1, a4).build()); - typeInfoMap.put(c2, TypeInfo.builder().supertypes(a1, a2, a3, a4).build()); - typeInfoMap.put(c3, TypeInfo.builder().supertype(a3).build()); - typeInfoMap.put(c4, TypeInfo.builder().supertype(a4).build()); - sut = new TypeAnalyzer(typeInfoMap); - tester = new TypeAnalyzerTester(sut); - } - - @Test - void analysisResultsTest() { - assertAll( - () -> tester.assertAbstractType(a1, c1, c2), - () -> tester.assertEliminatedType(a2, c2), - () -> tester.assertAbstractType(a3, c2, c3), - () -> tester.assertAbstractType(a4, c1, c2, c4), - () -> tester.assertVacuousType(a5), - () -> tester.assertConcreteType(c1), - () -> tester.assertConcreteType(c2), - () -> tester.assertConcreteType(c3), - () -> tester.assertConcreteType(c4) - ); - } - - @Test - void inferredTypesTest() { - assertAll( - () -> assertThat(sut.getUnknownType(), is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))), - () -> assertThat(tester.getInferredType(a1), is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))), - () -> assertThat(tester.getInferredType(a3), is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))), - () -> assertThat(tester.getInferredType(a4), is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))), - () -> assertThat(tester.getInferredType(a5), is(new InferredType(Set.of(a5), Set.of(), null))), - () -> assertThat(tester.getInferredType(c1), is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), - () -> assertThat(tester.getInferredType(c2), - is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))), - () -> assertThat(tester.getInferredType(c3), is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), - () -> assertThat(tester.getInferredType(c4), is(new InferredType(Set.of(a4, c4), Set.of(c4), c4))) - ); - } - - @Test - void consistentMustTest() { - var a1Result = tester.getPreservedType(a1); - var a3Result = tester.getPreservedType(a3); - var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2); - assertAll( - () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), is(expected)), - () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), is(expected)), - () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())), - () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())), - () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE), - is(a1Result.asInferredType())) - ); - } - - @Test - void consistentMayNotTest() { - var a1Result = tester.getPreservedType(a1); - var a3Result = tester.getPreservedType(a3); - var a4Result = tester.getPreservedType(a4); - assertAll( - () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE), - is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), - () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE), - is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), - () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE), - is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), - () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE), - is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))), - () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE), - is(new InferredType(Set.of(), Set.of(c3, c4), null))), - () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE), - is(new InferredType(Set.of(), Set.of(c1, c4), null))), - () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE), - is(new InferredType(Set.of(), Set.of(c3), null))) - ); - } - - @Test - void consistentErrorTest() { - var c1Result = tester.getPreservedType(c1); - var a4Result = tester.getPreservedType(a4); - var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null); - assertAll( - () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), is(expected)), - () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), is(expected)) - ); - } - - @Test - void consistentUnknownTest() { - var c1Result = tester.getPreservedType(c1); - var a4Result = tester.getPreservedType(a4); - assertAll( - () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.UNKNOWN), - is(a4Result.asInferredType())), - () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.UNKNOWN), - is(c1Result.asInferredType())) - ); - } - - @Test - void inconsistentMustTest() { - var a1Result = tester.getPreservedType(a1); - var c3Result = tester.getPreservedType(c3); - assertAll( - () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE), - is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))), - () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), - is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null))) - ); - } - - @Test - void inconsistentMayNotTest() { - var a1Result = tester.getPreservedType(a1); - var a4Result = tester.getPreservedType(a4); - var c1Result = tester.getPreservedType(c1); - assertAll( - () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE), - is(new InferredType(Set.of(a1, a4), Set.of(), null))), - () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE), - is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), - () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE), - is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), - () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), - is(new InferredType(Set.of(a1, a4), Set.of(), null))) - ); - } - - @Test - void vacuousMustTest() { - var c1Result = tester.getPreservedType(c1); - var a5Result = tester.getPreservedType(a5); - assertAll( - () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE), - is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), - () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE), - is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))) - ); - } - - @Test - void vacuousMayNotTest() { - var c1Result = tester.getPreservedType(c1); - var a5Result = tester.getPreservedType(a5); - assertAll( - () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.FALSE), - is(a5Result.asInferredType())), - () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.FALSE), - is(c1Result.asInferredType())) - ); - } - - @Test - void vacuousErrorTest() { - var c1Result = tester.getPreservedType(c1); - var a5Result = tester.getPreservedType(a5); - assertAll( - () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR), - is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), - () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR), - is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), - () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR), - is(a5Result.asInferredType())) - ); - } -} diff --git a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java deleted file mode 100644 index 02903026..00000000 --- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java +++ /dev/null @@ -1,200 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -import org.junit.jupiter.api.Test; -import tools.refinery.store.partial.representation.PartialRelation; -import tools.refinery.store.representation.TruthValue; - -import java.util.LinkedHashMap; -import java.util.Set; - -import static org.hamcrest.MatcherAssert.assertThat; -import static org.hamcrest.Matchers.is; -import static org.junit.jupiter.api.Assertions.assertAll; -import static org.junit.jupiter.api.Assertions.assertThrows; - -class TypeAnalyzerTest { - @Test - void directSupertypesTest() { - var c1 = new PartialRelation("C1", 1); - var c2 = new PartialRelation("C2", 1); - var c3 = new PartialRelation("C3", 1); - var typeInfoMap = new LinkedHashMap(); - typeInfoMap.put(c1, TypeInfo.builder().supertypes(c2, c3).build()); - typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build()); - typeInfoMap.put(c3, TypeInfo.builder().build()); - - var sut = new TypeAnalyzer(typeInfoMap); - var tester = new TypeAnalyzerTester(sut); - - assertAll( - () -> tester.assertConcreteType(c1), - () -> tester.assertConcreteType(c2, c1), - () -> tester.assertConcreteType(c3, c2) - ); - } - - @Test - void typeEliminationAbstractToConcreteTest() { - var c1 = new PartialRelation("C1", 1); - var c2 = new PartialRelation("C2", 1); - var a11 = new PartialRelation("A11", 1); - var a12 = new PartialRelation("A12", 1); - var a21 = new PartialRelation("A21", 1); - var a22 = new PartialRelation("A22", 1); - var a3 = new PartialRelation("A3", 1); - var typeInfoMap = new LinkedHashMap(); - typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); - typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build()); - typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build()); - typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); - typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); - typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build()); - typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build()); - - var sut = new TypeAnalyzer(typeInfoMap); - var tester = new TypeAnalyzerTester(sut); - - assertAll( - () -> tester.assertConcreteType(c1), - () -> tester.assertConcreteType(c2), - () -> tester.assertEliminatedType(a11, c1), - () -> tester.assertEliminatedType(a12, c1), - () -> tester.assertEliminatedType(a21, c1), - () -> tester.assertEliminatedType(a22, c1), - () -> tester.assertAbstractType(a3, c1, c2) - ); - } - - @Test - void typeEliminationConcreteToAbstractTest() { - var c1 = new PartialRelation("C1", 1); - var c2 = new PartialRelation("C2", 1); - var a11 = new PartialRelation("A11", 1); - var a12 = new PartialRelation("A12", 1); - var a21 = new PartialRelation("A21", 1); - var a22 = new PartialRelation("A22", 1); - var a3 = new PartialRelation("A3", 1); - var typeInfoMap = new LinkedHashMap(); - typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build()); - typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build()); - typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); - typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); - typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build()); - typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build()); - typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); - - var sut = new TypeAnalyzer(typeInfoMap); - var tester = new TypeAnalyzerTester(sut); - - assertAll( - () -> tester.assertConcreteType(c1), - () -> tester.assertConcreteType(c2), - () -> tester.assertEliminatedType(a11, c1), - () -> tester.assertEliminatedType(a12, c1), - () -> tester.assertEliminatedType(a21, c1), - () -> tester.assertEliminatedType(a22, c1), - () -> tester.assertAbstractType(a3, c1, c2) - ); - } - - @Test - void preserveConcreteTypeTest() { - var c1 = new PartialRelation("C1", 1); - var a1 = new PartialRelation("A1", 1); - var c2 = new PartialRelation("C2", 1); - var a2 = new PartialRelation("A2", 1); - var typeInfoMap = new LinkedHashMap(); - typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); - typeInfoMap.put(a1, TypeInfo.builder().abstractType().supertype(c2).build()); - typeInfoMap.put(c2, TypeInfo.builder().supertype(a2).build()); - typeInfoMap.put(a2, TypeInfo.builder().abstractType().build()); - - var sut = new TypeAnalyzer(typeInfoMap); - var tester = new TypeAnalyzerTester(sut); - - assertAll( - () -> tester.assertConcreteType(c1), - () -> tester.assertEliminatedType(a1, c1), - () -> tester.assertConcreteType(c2, c1), - () -> tester.assertEliminatedType(a2, c2) - ); - } - - @Test - void mostGeneralCurrentTypeTest() { - var c1 = new PartialRelation("C1", 1); - var c2 = new PartialRelation("C2", 1); - var c3 = new PartialRelation("C3", 1); - var typeInfoMap = new LinkedHashMap(); - typeInfoMap.put(c1, TypeInfo.builder().supertype(c3).build()); - typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build()); - typeInfoMap.put(c3, TypeInfo.builder().build()); - - var sut = new TypeAnalyzer(typeInfoMap); - var tester = new TypeAnalyzerTester(sut); - var c3Result = tester.getPreservedType(c3); - - var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); - assertAll( - () -> assertThat(tester.getInferredType(c3), is(expected)), - () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(expected)) - ); - } - - @Test - void preferFirstConcreteTypeTest() { - var a1 = new PartialRelation("A1", 1); - var c1 = new PartialRelation("C1", 1); - var c2 = new PartialRelation("C2", 1); - var c3 = new PartialRelation("C3", 1); - var c4 = new PartialRelation("C4", 1); - var typeInfoMap = new LinkedHashMap(); - typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); - typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build()); - typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build()); - typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build()); - typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); - - var sut = new TypeAnalyzer(typeInfoMap); - var tester = new TypeAnalyzerTester(sut); - var c1Result = tester.getPreservedType(c1); - var a1Result = tester.getPreservedType(a1); - - assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), - is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2))); - } - - @Test - void preferFirstMostGeneralConcreteTypeTest() { - var a1 = new PartialRelation("A1", 1); - var c1 = new PartialRelation("C1", 1); - var c2 = new PartialRelation("C2", 1); - var c3 = new PartialRelation("C3", 1); - var c4 = new PartialRelation("C4", 1); - var typeInfoMap = new LinkedHashMap(); - typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build()); - typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build()); - typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build()); - typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); - typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); - - var sut = new TypeAnalyzer(typeInfoMap); - var tester = new TypeAnalyzerTester(sut); - var c1Result = tester.getPreservedType(c1); - var a1Result = tester.getPreservedType(a1); - - assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), - is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3))); - } - - @Test - void circularTypeHierarchyTest() { - var c1 = new PartialRelation("C1", 1); - var c2 = new PartialRelation("C2", 1); - var typeInfoMap = new LinkedHashMap(); - typeInfoMap.put(c1, TypeInfo.builder().supertype(c2).build()); - typeInfoMap.put(c2, TypeInfo.builder().supertype(c1).build()); - - assertThrows(IllegalArgumentException.class, () -> new TypeAnalyzer(typeInfoMap)); - } -} diff --git a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java b/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java deleted file mode 100644 index ce600ea6..00000000 --- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java +++ /dev/null @@ -1,51 +0,0 @@ -package tools.refinery.store.partial.translator.typehierarchy; - -import tools.refinery.store.partial.representation.PartialRelation; - -import static org.hamcrest.MatcherAssert.assertThat; -import static org.hamcrest.Matchers.*; -import static org.hamcrest.Matchers.is; - -class TypeAnalyzerTester { - private final TypeAnalyzer sut; - - public TypeAnalyzerTester(TypeAnalyzer sut) { - this.sut = sut; - } - - public void assertAbstractType(PartialRelation partialRelation, PartialRelation... directSubtypes) { - assertPreservedType(partialRelation, true, false, directSubtypes); - } - - public void assertVacuousType(PartialRelation partialRelation) { - assertPreservedType(partialRelation, true, true); - } - - public void assertConcreteType(PartialRelation partialRelation, PartialRelation... directSubtypes) { - assertPreservedType(partialRelation, false, false, directSubtypes); - } - - private void assertPreservedType(PartialRelation partialRelation, boolean isAbstract, boolean isVacuous, - PartialRelation... directSubtypes) { - var result = sut.getAnalysisResults().get(partialRelation); - assertThat(result, is(instanceOf(PreservedType.class))); - var preservedResult = (PreservedType) result; - assertThat(preservedResult.isAbstractType(), is(isAbstract)); - assertThat(preservedResult.isVacuous(), is(isVacuous)); - assertThat(preservedResult.getDirectSubtypes(), hasItems(directSubtypes)); - } - - public void assertEliminatedType(PartialRelation partialRelation, PartialRelation replacement) { - var result = sut.getAnalysisResults().get(partialRelation); - assertThat(result, is(instanceOf(EliminatedType.class))); - assertThat(((EliminatedType) result).replacement(), is(replacement)); - } - - public PreservedType getPreservedType(PartialRelation partialRelation) { - return (PreservedType) sut.getAnalysisResults().get(partialRelation); - } - - public InferredType getInferredType(PartialRelation partialRelation) { - return getPreservedType(partialRelation).asInferredType(); - } -} -- cgit v1.2.3-70-g09d2