Merge pull request #63 from kris7t/base-preds

Base predicates

gradle/libs.versions.toml

@@ -39,7 +39,7 @@ jdt-core = "3.38.0"
 jdt-debug = "3.21.400"
 jdt-launching = "3.22.0"
 jetbrainsAnnotations = "24.1.0"
-jetty = "12.0.11"
+jetty = "12.0.12"
 jmh = "1.37"
 jna = "5.14.0"
 junit = "5.10.3"

package.json

@@ -36,10 +36,10 @@
   },
   "devDependencies": {
     "@types/eslint": "^8.56.11",
-    "@types/node": "^20.14.12",
+    "@types/node": "^20.14.14",
     "@types/react": "^18.3.3",
-    "@typescript-eslint/eslint-plugin": "^7.17.0",
-    "@typescript-eslint/parser": "^7.17.0",
+    "@typescript-eslint/eslint-plugin": "^7.18.0",
+    "@typescript-eslint/parser": "^7.18.0",
     "corepack": "^0.29.3",
     "eslint": "^8.57.0",
     "eslint-config-airbnb": "^19.0.4",

subprojects/docs/package.json

@@ -44,7 +44,7 @@
     "@fontsource/open-sans": "^5.0.28",
     "@material-icons/svg": "^1.0.33",
     "@mdx-js/react": "^3.0.1",
-    "@swc/core": "^1.7.2",
+    "@swc/core": "^1.7.5",
     "clsx": "^2.1.1",
     "java-properties": "^1.0.2",
     "mdast-util-mdx": "^3.0.0",
@@ -68,7 +68,7 @@
     "@docusaurus/types": "^3.4.0",
     "@types/babel__core": "^7.20.5",
     "@types/mdast": "^4.0.4",
-    "@types/node": "^20.14.12",
+    "@types/node": "^20.14.14",
     "@types/react": "^18.3.3",
     "@types/react-dom": "^18.3.0",
     "@types/unist": "^3.0.2"

subprojects/frontend/package.json

@@ -34,7 +34,7 @@
     "@codemirror/lint": "^6.8.1",
     "@codemirror/search": "^6.5.6",
     "@codemirror/state": "^6.4.1",
-    "@codemirror/view": "^6.29.0",
+    "@codemirror/view": "^6.29.1",
     "@emotion/cache": "^11.13.1",
     "@emotion/react": "^11.13.0",
     "@emotion/serialize": "^1.3.0",
@@ -46,12 +46,12 @@
     "@hpcc-js/wasm": "^2.18.0",
     "@lezer/common": "^1.2.1",
     "@lezer/highlight": "^1.2.0",
-    "@lezer/lr": "^1.4.1",
+    "@lezer/lr": "^1.4.2",
     "@material-icons/svg": "^1.0.33",
-    "@mui/icons-material": "^5.16.5",
-    "@mui/material": "^5.16.5",
-    "@mui/system": "^5.16.5",
-    "@mui/x-data-grid": "^7.11.1",
+    "@mui/icons-material": "^5.16.6",
+    "@mui/material": "^5.16.6",
+    "@mui/system": "^5.16.6",
+    "@mui/x-data-grid": "^7.12.0",
     "ansi-styles": "^6.2.1",
     "csstype": "^3.1.3",
     "d3": "^7.9.0",
@@ -88,7 +88,7 @@
     "@types/lodash-es": "^4.17.12",
     "@types/micromatch": "^4.0.9",
     "@types/ms": "^0.7.34",
-    "@types/node": "^20.14.12",
+    "@types/node": "^20.14.14",
     "@types/pnpapi": "^0.0.5",
     "@types/react": "^18.3.3",
     "@types/react-dom": "^18.3.0",

subprojects/frontend/src/graph/GraphStore.ts

@@ -25,6 +25,7 @@ export function getDefaultVisibility(
     case 'class':
     case 'reference':
     case 'opposite':
+    case 'base':
       return 'all';
     case 'predicate':
       return detail.error ? 'must' : 'none';

subprojects/frontend/src/language/problem.grammar

@@ -52,8 +52,7 @@ statement {
     kw<"extern"> ckw<"aggregator"> AggregatorName "."
   } |
   PredicateDefinition {
-    ckw<"shadow">?
-    (kw<"error">? kw<"pred"> | kw<"error">)
+    ((kw<"error"> | kw<"partial"> | ckw<"shadow">)* kw<"pred"> | kw<"error">)
     RelationName ParameterList<Parameter>?
     PredicateBody { ("<->" sep<OrOp, Conjunction>)? "." }
   } |

subprojects/frontend/src/xtext/xtextServiceResults.ts

@@ -156,6 +156,7 @@ export const RelationMetadata = z.object({
       opposite: z.string(),
     }),
     z.object({ type: z.literal('predicate'), error: z.boolean() }),
+    z.object({ type: z.literal('base') }),
     z.object({ type: z.literal('builtin') }),
   ]),
 });

subprojects/generator/src/main/java/tools/refinery/generator/ModelFacadeFactory.java

@@ -10,14 +10,18 @@
 import tools.refinery.language.semantics.ModelInitializer;
 import tools.refinery.store.util.CancellationToken;
 
+// This class is used as a fluent builder, so it's not necessary to use the return value of all of its methods.
+@SuppressWarnings("UnusedReturnValue")
 public abstract sealed class ModelFacadeFactory<T extends ModelFacadeFactory<T>> permits ModelSemanticsFactory,
 		ModelGeneratorFactory {
 	@Inject
 	private Provider<ModelInitializer> initializerProvider;
 
 	private CancellationToken cancellationToken = CancellationToken.NONE;
 
-	private boolean keepNonExistingObjects = false;
+	private boolean keepNonExistingObjects;
+
+	private boolean keepShadowPredicates = true;
 
 	protected abstract T getSelf();
 
@@ -26,13 +30,21 @@ public T cancellationToken(CancellationToken cancellationToken) {
 		return getSelf();
 	}
 
-	public T keepNonExistingObjects(boolean removeNonExistentObjects) {
-		this.keepNonExistingObjects = removeNonExistentObjects;
+	public T keepNonExistingObjects(boolean keepNonExistentObjects) {
+		this.keepNonExistingObjects = keepNonExistentObjects;
+		return getSelf();
+	}
+
+	public T keepShadowPredicates(boolean keepShadowPredicates) {
+		this.keepShadowPredicates = keepShadowPredicates;
 		return getSelf();
 	}
 
 	protected ModelInitializer createModelInitializer() {
-		return initializerProvider.get();
+		var initializer = initializerProvider.get();
+		initializer.setKeepNonExistingObjects(keepNonExistingObjects);
+		initializer.setKeepShadowPredicates(keepShadowPredicates);
+		return initializer;
 	}
 
 	protected CancellationToken getCancellationToken() {

subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java

@@ -35,6 +35,10 @@ public final class ModelGeneratorFactory extends ModelFacadeFactory<ModelGenerat
 
 	private int stateCoderDepth = NeighborhoodCalculator.DEFAULT_DEPTH;
 
+	public ModelGeneratorFactory() {
+		keepShadowPredicates(false);
+	}
+
 	@Override
 	protected ModelGeneratorFactory getSelf() {
 		return this;
@@ -70,7 +74,7 @@ public ModelGenerator createGenerator(Problem problem) {
 				.with(DesignSpaceExplorationAdapter.builder())
 				.with(ReasoningAdapter.builder()
 						.requiredInterpretations(getRequiredInterpretations()));
-		initializer.configureStoreBuilder(storeBuilder, isKeepNonExistingObjects());
+		initializer.configureStoreBuilder(storeBuilder);
 		var store = storeBuilder.build();
 		var generator = new ModelGenerator(initializer.getProblemTrace(), store, initializer.getModelSeed(),
 				solutionSerializerProvider, cancellationToken, isKeepNonExistingObjects());

subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsFactory.java

@@ -15,6 +15,8 @@
 import java.util.Collection;
 import java.util.Set;
 
+// This class is used as a fluent builder, so it's not necessary to use the return value of all of its methods.
+@SuppressWarnings("UnusedReturnValue")
 public final class ModelSemanticsFactory extends ModelFacadeFactory<ModelSemanticsFactory> {
 	private boolean withCandidateInterpretations;
 
@@ -45,7 +47,7 @@ public ModelSemantics tryCreateSemantics(Problem problem) {
 						.throwOnFatalRejection(false))
 				.with(ReasoningAdapter.builder()
 						.requiredInterpretations(getRequiredInterpretations()));
-		initializer.configureStoreBuilder(storeBuilder, isKeepNonExistingObjects());
+		initializer.configureStoreBuilder(storeBuilder);
 		var store = storeBuilder.build();
 		return new ModelSemantics(initializer.getProblemTrace(), store, initializer.getModelSeed());
 	}

subprojects/generator/src/test/java/tools/refinery/generator/FileBasedSemanticsTest.java

@@ -6,6 +6,7 @@
 package tools.refinery.generator;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 import org.junit.jupiter.api.DynamicNode;
 import org.junit.jupiter.api.TestFactory;
 import tools.refinery.generator.tests.DynamicTestLoader;
@@ -18,8 +19,23 @@ class FileBasedSemanticsTest {
 	@Inject
 	private DynamicTestLoader loader;
 
+	@Inject
+	private Provider<ModelSemanticsFactory> semanticsFactoryProvider;
+
 	@TestFactory
-	Stream<DynamicNode> fileBasedTests() {
+	Stream<DynamicNode> testWithNonExistingObjects() {
+		return getFileBasedTests(true, true);
+	}
+
+	@TestFactory
+	Stream<DynamicNode> testWithoutNonExistingObjects() {
+		return getFileBasedTests(false, false);
+	}
+
+	private Stream<DynamicNode> getFileBasedTests(boolean keepNonExistingObjects, boolean keepShadowPredicates) {
+		loader.setSemanticsFactoryProvider(() -> semanticsFactoryProvider.get()
+				.keepNonExistingObjects(keepNonExistingObjects)
+				.keepShadowPredicates(keepShadowPredicates));
 		return loader.allFromClasspath(getClass());
 	}
 }

subprojects/generator/src/test/resources/tools/refinery/generator/crossreference/typeConstraint.problem

@@ -0,0 +1,85 @@
+% Copyright (c) 2024 The Refinery Authors <https://refinery.tools/>
+%
+% SPDX-License-Identifier: EPL-2.0
+
+% TEST WITH ERRORS: directed cross reference type constraint
+
+class A {
+    B[] foo
+}
+
+class B.
+
+foo(a1, b1).
+!foo(a2, b2).
+?foo(a3, b3).
+foo(a4, b4): error.
+
+% EXPECT EXACTLY:
+foo(a1, b1).
+!foo(a2, b2).
+?foo(a3, b3).
+foo(a4, b4): error.
+A(a1).
+B(b1).
+?A(a2).
+?B(b2).
+?A(a3).
+?B(b3).
+A(a4).
+B(b4).
+
+% TEST: directed cross reference with predicate type
+
+class A {
+    bar[] foo
+}
+
+pred bar(A a) <-> !foo(a, _).
+
+foo(a1, b1).
+
+% EXPECT:
+A(a1).
+bar(b1).
+
+% TEST WITH ERRORS: directed cross reference with predicate type and assertion
+
+class A {
+    bar[] foo
+}
+
+pred bar(A a) <-> !foo(a, _).
+
+!bar(b1).
+foo(a1, b1).
+
+% EXPECT EXACTLY:
+foo(a1, b1): error.
+A(a1).
+bar(b1): error.
+
+% TEST WITH ERRORS: undirected cross reference type constraint
+
+class A {
+    A[] bar opposite bar
+}
+
+bar(a1, b1).
+!bar(a2, b2).
+?bar(a3, b3).
+bar(a4, b4): error.
+
+% EXPECT EXACTLY:
+bar(a1, b1).
+!bar(a2, b2).
+?bar(a3, b3).
+bar(a4, b4): error.
+A(a1).
+A(b1).
+?A(a2).
+?A(b2).
+?A(a3).
+?A(b3).
+A(a4).
+A(b4).

subprojects/generator/src/test/resources/tools/refinery/generator/crossreference/undirectedMultiplicity.problem

@@ -0,0 +1,57 @@
+% Copyright (c) 2024 The Refinery Authors <https://refinery.tools/>
+%
+% SPDX-License-Identifier: EPL-2.0
+
+% TEST: upper bound propagation
+
+class Person {
+    Person[0..2] friend opposite friend
+}
+
+friend(a, b).
+friend(a, c).
+friend(b, c).
+!exists(Person::new).
+
+% EXPECT:
+friend(b, a).
+friend(c, a).
+friend(c, b).
+!friend(a, a).
+!friend(b, b).
+!friend(c, c).
+
+% TEST: lower bound propagation
+
+class Person {
+    Person[2..*] friend opposite friend
+}
+
+Person(a).
+!friend(a, a).
+!friend(b, b).
+!friend(c, c).
+!exists(Person::new).
+
+% EXPECT:
+friend(a, b).
+friend(a, c).
+friend(b, c).
+
+% TEST: upper and lower bound propagation
+
+class Person {
+    Person[2] friend opposite friend
+}
+
+friend(a, b).
+friend(a, c).
+!friend(b, b).
+!friend(c, c).
+!exists(Person::new).
+
+% EXPECT:
+friend(b, c).
+!friend(a, a).
+!friend(b, b).
+!friend(c, c).

subprojects/generator/src/testFixtures/java/tools/refinery/generator/tests/DynamicTestLoader.java

@@ -34,9 +34,13 @@ public class DynamicTestLoader {
 	@Inject
 	private Provider<SemanticsTestLoader> testLoaderProvider;
 
-	@Inject
 	private Provider<ModelSemanticsFactory> semanticsFactoryProvider;
 
+	@Inject
+	public void setSemanticsFactoryProvider(Provider<ModelSemanticsFactory> semanticsFactoryProvider) {
+		this.semanticsFactoryProvider = semanticsFactoryProvider;
+	}
+
 	public Stream<DynamicNode> allFromClasspath(Class<?> contextClass) {
 		var paths = getExtraPaths(contextClass);
 		if (paths.isEmpty()) {