Merge pull request #67 from LiliNemes/subsetting

Implement subsetting for references and predicates.

CONTRIBUTORS.md

@@ -16,6 +16,7 @@ Other contributors (in alphabetical order):
 * Garami, Bence <85867500+garamibence@users.noreply.github.com>
 * Golej, Márton Marcell <golejmarci@gmail.com>
 * Marussy, Kristóf <marussy@mit.bme.hu>
+* Nemes, Lili <lili.nemes@outlook.com>
 * Semeráth, Oszkár <semerath@mit.bme.hu>
 
 ## Support

subprojects/frontend/src/language/problem.grammar

@@ -54,6 +54,7 @@ statement {
   PredicateDefinition {
     ((kw<"error"> | kw<"partial"> | ckw<"shadow">)* kw<"pred"> | kw<"error">)
     RelationName ParameterList<Parameter>?
+    (kw<"subsets"> sep1<",", RelationName>)*
     PredicateBody { ("<->" sep<OrOp, Conjunction>)? "." }
   } |
   // FunctionDefinition {
@@ -89,7 +90,10 @@ FeatureDeclaration {
   RelationName
   ("[" Multiplicity? "]")?
   RelationName
-  (kw<"opposite"> RelationName)?
+  (
+    kw<"opposite"> RelationName |
+    kw<"subsets"> sep1<",", RelationName>
+  )*
   ";"?
 }
 

subprojects/frontend/src/language/problemLanguageSupport.ts

@@ -36,7 +36,8 @@ const parserWithMetadata = parser.configure({
       'import as declare atom multi': t.definitionKeyword,
       'extern datatype aggregator': t.definitionKeyword,
       rule: t.definitionKeyword,
-      'abstract extends refers contains container partial opposite': t.modifier,
+      'abstract extends refers contains container partial': t.modifier,
+      'opposite subsets': t.modifier,
       default: t.modifier,
       'shadow propagation decision concretization': t.modifier,
       'true false unknown error': t.keyword,

subprojects/generator/src/test/resources/tools/refinery/generator/concretization/predicateSubsetting.problem

@@ -0,0 +1,30 @@
+% Copyright (c) 2024 The Refinery Authors <https://refinery.tools/>
+%
+% SPDX-License-Identifier: EPL-2.0
+
+class A {
+    partial A[] foo
+}
+
+pred hasCommonFoo(A a1, A a2) <->
+    a1 != a2,
+    a1 != a3,
+    a2 != a3,
+    foo(a1, a3),
+    foo(a2, a3).
+
+pred noCommonFoo(A a1, A a2) subsets foo <->
+    a1 != a2,
+    !hasCommonFoo(a1, a2).
+
+!exists(A::new).
+atom x, y, z.
+A(x).
+A(y).
+A(z).
+concretization rule addNoFoo() ==> !foo(x, z).
+
+% EXPECT CANDIDATE:
+foo(x, y).
+foo(y, x).
+!noCommonFoo(x, z).

subprojects/generator/src/test/resources/tools/refinery/generator/semantics/crossreference/basePredicateSuperset.problem

@@ -0,0 +1,38 @@
+% Copyright (c) 2024 The Refinery Authors <https://refinery.tools/>
+%
+% SPDX-License-Identifier: EPL-2.0
+
+class Definition.
+
+class Usage.
+
+class PartDefinition extends Definition.
+
+class PartUsage extends Usage.
+
+class FeatureTyping {
+    Usage[1] typedFeature
+    Definition[1] featureType
+}
+
+pred def(Usage u, Definition d) <->
+    typedFeature(t, u),
+    featureType(t, d).
+
+pred partDef(PartUsage u, PartDefinition d) subsets def.
+
+% TEST: subset not allowed
+
+PartUsage(part1).
+PartDefinition(partDef1).
+!exists(FeatureTyping::new).
+
+% EXPECT:
+!partDef(part1, partDef1).
+
+% TEST: superset forced
+
+partDef(part1, partDef1).
+
+% EXPECT:
+def(part1, partDef1).

subprojects/generator/src/test/resources/tools/refinery/generator/semantics/crossreference/containerSuperset.problem

@@ -0,0 +1,53 @@
+% Copyright (c) 2024 The Refinery Authors <https://refinery.tools/>
+%
+% SPDX-License-Identifier: EPL-2.0
+
+class Definition {
+    Usage[] usages opposite def
+}
+
+class Usage {
+    Definition[] def opposite usages
+}
+
+class PartDefinition extends Definition {
+    container PartUsage partUsages opposite partDef subsets usages
+}
+
+class PartUsage extends Usage {
+    contains PartDefinition[] partDef opposite partUsages
+}
+
+% TEST: subset not allowed
+
+PartUsage(part1).
+PartDefinition(partDef1).
+!def(part1, partDef1).
+
+% EXPECT:
+!partDef(part1, partDef1).
+
+% TEST: superset forced
+
+partDef(part1, partDef1).
+
+% EXPECT:
+def(part1, partDef1).
+
+% TEST: superset forced with default false
+
+default !def(*, *).
+partDef(part1, partDef1).
+?def(part1, partDef1).
+
+% EXPECT:
+def(part1, partDef1).
+
+% TEST WITH ERRORS: inconsistency with default false
+
+default !def(*, *).
+partDef(part1, partDef1).
+
+% EXPECT:
+def(part1, partDef1): error.
+partDef(part1, partDef1): error.

subprojects/generator/src/test/resources/tools/refinery/generator/semantics/crossreference/containmentSuperset.problem

@@ -0,0 +1,49 @@
+% Copyright (c) 2024 The Refinery Authors <https://refinery.tools/>
+%
+% SPDX-License-Identifier: EPL-2.0
+
+class Definition.
+
+class Usage {
+    Definition[] def
+}
+
+class PartDefinition extends Definition.
+
+class PartUsage extends Usage {
+    contains PartDefinition[] partDef subsets def
+}
+
+% TEST: subset not allowed
+
+PartUsage(part1).
+PartDefinition(partDef1).
+!def(part1, partDef1).
+
+% EXPECT:
+!partDef(part1, partDef1).
+
+% TEST: superset forced
+
+partDef(part1, partDef1).
+
+% EXPECT:
+def(part1, partDef1).
+
+% TEST: superset forced with default false
+
+default !def(*, *).
+partDef(part1, partDef1).
+?def(part1, partDef1).
+
+% EXPECT:
+def(part1, partDef1).
+
+% TEST WITH ERRORS: inconsistency with default false
+
+default !def(*, *).
+partDef(part1, partDef1).
+
+% EXPECT:
+def(part1, partDef1): error.
+partDef(part1, partDef1): error.

subprojects/generator/src/test/resources/tools/refinery/generator/semantics/crossreference/directedSuperset.problem

@@ -0,0 +1,31 @@
+% Copyright (c) 2024 The Refinery Authors <https://refinery.tools/>
+%
+% SPDX-License-Identifier: EPL-2.0
+
+class Definition.
+
+class Usage {
+    Definition[] def
+}
+
+class PartDefinition extends Definition.
+
+class PartUsage extends Usage {
+    PartDefinition[] partDef subsets def
+}
+
+% TEST: subset not allowed
+
+PartUsage(part1).
+PartDefinition(partDef1).
+!def(part1, partDef1).
+
+% EXPECT:
+!partDef(part1, partDef1).
+
+% TEST: superset forced
+
+partDef(part1, partDef1).
+
+% EXPECT:
+def(part1, partDef1).

subprojects/generator/src/test/resources/tools/refinery/generator/semantics/crossreference/undirectedSuperset.problem

@@ -0,0 +1,29 @@
+% Copyright (c) 2024 The Refinery Authors <https://refinery.tools/>
+%
+% SPDX-License-Identifier: EPL-2.0
+
+class Usage {
+    Usage[] usage
+}
+
+class PartUsage extends Usage {
+    PartUsage[] partUsage opposite partUsage subsets usage
+}
+
+% TEST: subset not allowed
+
+PartUsage(part1).
+PartUsage(part2).
+!usage(part1, part2).
+
+% EXPECT:
+!partUsage(part1, part2).
+!partUsage(part2, part1).
+
+% TEST: superset forced
+
+partUsage(part1, part2).
+
+% EXPECT:
+usage(part1, part2).
+usage(part2, part1).

subprojects/generator/src/test/resources/tools/refinery/generator/semantics/predicateSubsetting.problem

@@ -0,0 +1,39 @@
+% Copyright (c) 2024 The Refinery Authors <https://refinery.tools/>
+%
+% SPDX-License-Identifier: EPL-2.0
+
+class A {
+    A[] foo
+}
+
+pred hasCommonFoo(A a1, A a2) <->
+    a1 != a2,
+    a1 != a3,
+    a2 != a3,
+    foo(a1, a3),
+    foo(a2, a3).
+
+pred noCommonFoo(A a1, A a2) subsets foo <->
+    a1 != a2,
+    !hasCommonFoo(a1, a2).
+
+!exists(A::new).
+A(x).
+A(y).
+A(z).
+
+% TEST: no propagation without assertion
+
+% EXPECT EXACTLY:
+?foo(x, y).
+?foo(y, x).
+?noCommonFoo(x, z).
+
+% TEST: with negative assertion
+
+!foo(x, z).
+
+% EXPECT:
+foo(x, y).
+foo(y, x).
+!noCommonFoo(x, z).