diff --git a/settings.gradle.kts b/settings.gradle.kts index 98b850824..33a22830f 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -24,6 +24,7 @@ include( "language-ide", "language-model", "language-semantics", + "language-semantics-z3", "language-web", "logic", "store", diff --git a/subprojects/frontend/src/editor/EditorTheme.ts b/subprojects/frontend/src/editor/EditorTheme.ts index 4cf2e9264..a3b57059e 100644 --- a/subprojects/frontend/src/editor/EditorTheme.ts +++ b/subprojects/frontend/src/editor/EditorTheme.ts @@ -8,6 +8,7 @@ import annotationSVG from '@material-icons/svg/svg/alternate_email/baseline.svg? import cancelSVG from '@material-icons/svg/svg/cancel/baseline.svg?raw'; import namespaceSVG from '@material-icons/svg/svg/data_object/baseline.svg?raw'; import expandMoreSVG from '@material-icons/svg/svg/expand_more/baseline.svg?raw'; +import extensionSVG from '@material-icons/svg/svg/extension/baseline.svg?raw'; import functionsSVG from '@material-icons/svg/svg/functions/baseline.svg?raw'; import infoSVG from '@material-icons/svg/svg/info/baseline.svg?raw'; import labelOutlinedSVG from '@material-icons/svg/svg/label/outline.svg?raw'; @@ -655,6 +656,7 @@ export default styled('div', { ...completionIconStyle('rule', gearSVG, { opacity: 0.7 }), ...completionIconStyle('variable', variableSVG), ...completionIconStyle('attribute', attributeSVG), + ...completionIconStyle('theory', extensionSVG, { opacity: 0.7 }), '.cm-tooltip.cm-completionInfo': { ...((theme.components?.MuiTooltip?.styleOverrides?.tooltip as | CSSObject diff --git a/subprojects/frontend/src/language/problem.grammar b/subprojects/frontend/src/language/problem.grammar index 5a84008a3..bbc7cb06e 100644 --- a/subprojects/frontend/src/language/problem.grammar +++ b/subprojects/frontend/src/language/problem.grammar @@ -51,6 +51,9 @@ statement { AggregatorDeclaration { AnnotationKeyword ckw<"aggregator"> AggregatorName "." } | + TheoryDeclaration { + AnnotationKeyword ckw<"theory"> TheoryName "." + } OverloadedDeclaration { AnnotationKeyword ckw<"primitive"> RelationName ParameterList "." } | @@ -173,7 +176,9 @@ Atom { RelationName "+"? ParameterList } Consequent { ("," | Action)+ } -Action { +Action { AssertionAction | TermAction } + +AssertionAction { (NotOp | UnknownOp)? RelationName ParameterList (":" Expr)? @@ -183,6 +188,8 @@ AssertionArgument { NodeName | StarArgument } AssertionActionArgument { VariableName | StarArgument } +TermAction { ckw<"assert"> Expr (ckw<"using"> ( TheoryName | "{" sep<",", TheoryName> "}"))? } + Constant { Real | String | StarMult | LogicValue } LogicValue { @@ -217,6 +224,8 @@ ModuleName { QualifiedName } AggregatorName { QualifiedName } +TheoryName { QualifiedName } + AnnotationName { QualifiedName } ID { identifier | QuotedID } diff --git a/subprojects/frontend/src/language/problemLanguageSupport.ts b/subprojects/frontend/src/language/problemLanguageSupport.ts index c03b82174..262b0e8f2 100644 --- a/subprojects/frontend/src/language/problemLanguageSupport.ts +++ b/subprojects/frontend/src/language/problemLanguageSupport.ts @@ -34,15 +34,15 @@ const parserWithMetadata = parser.configure({ BlockComment: t.blockComment, 'module problem class enum pred scope': t.definitionKeyword, 'import as declare atom multi': t.definitionKeyword, - 'datatype aggregator primitive': t.definitionKeyword, + 'datatype aggregator primitive theory': t.definitionKeyword, 'AnnotationKeyword/#': t.definitionKeyword, rule: t.definitionKeyword, - 'abstract extends refers contains container partial': t.modifier, + 'abstract extends refers contains container using': t.modifier, 'opposite subsets': t.modifier, default: t.modifier, 'shadow propagation decision concretization': t.modifier, 'true false unknown error': t.keyword, - 'candidate may must': t.operatorKeyword, + 'partial candidate may must assert': t.operatorKeyword, is: t.operatorKeyword, NotOp: t.operator, UnknownOp: t.operator, @@ -54,6 +54,7 @@ const parserWithMetadata = parser.configure({ 'RelationName!': t.typeName, 'DatatypeName!': t.keyword, 'AggregatorName!': t.operatorKeyword, + 'TheoryName!': t.keyword, 'RuleName!': t.typeName, 'AtomNodeName!': t.atom, 'VariableName!': t.variableName, diff --git a/subprojects/generator/build.gradle.kts b/subprojects/generator/build.gradle.kts index a60ec800b..c46f248c5 100644 --- a/subprojects/generator/build.gradle.kts +++ b/subprojects/generator/build.gradle.kts @@ -17,6 +17,7 @@ dependencies { api(project(":refinery-language-semantics")) implementation(project(":refinery-store-query-interpreter")) implementation(project(":refinery-store-reasoning-scope")) + runtimeOnly(project(":refinery-language-semantics-z3")) testFixturesApi(testFixtures(project(":refinery-language"))) testFixturesImplementation(libs.junit.api) } diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/impl/FilteredInterpretation.java b/subprojects/generator/src/main/java/tools/refinery/generator/impl/FilteredInterpretation.java index 5d40ab142..162321902 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/impl/FilteredInterpretation.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/impl/FilteredInterpretation.java @@ -9,6 +9,7 @@ import tools.refinery.logic.term.truthvalue.TruthValue; import tools.refinery.store.map.Cursor; import tools.refinery.store.map.FilteredCursor; +import tools.refinery.store.query.resultset.ResultSetListener; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.interpretation.PartialInterpretation; import tools.refinery.store.reasoning.literal.Concreteness; @@ -53,6 +54,16 @@ public Cursor getAll() { return new FilteredInterpretationCursor(wrappedInterpretation.getAll()); } + @Override + public void addListener(ResultSetListener listener) { + throw new UnsupportedOperationException("Filtered interpretations do not support listeners"); + } + + @Override + public void removeListener(ResultSetListener listener) { + throw new UnsupportedOperationException("Filtered interpretations do not support listeners"); + } + private boolean tupleExists(Tuple key) { int arity = key.getSize(); for (int i = 0; i < arity; i++) { diff --git a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemContentProposalProvider.java b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemContentProposalProvider.java index 494d2e9ff..e36831a85 100644 --- a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemContentProposalProvider.java +++ b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemContentProposalProvider.java @@ -9,9 +9,7 @@ import org.eclipse.xtext.Keyword; import org.eclipse.xtext.ide.editor.contentassist.ContentAssistContext; import org.eclipse.xtext.ide.editor.contentassist.IdeContentProposalProvider; -import tools.refinery.language.model.problem.AnnotationDeclaration; -import tools.refinery.language.model.problem.Parameter; -import tools.refinery.language.model.problem.ParametricDefinition; +import tools.refinery.language.model.problem.*; import tools.refinery.language.utils.ProblemUtil; import java.util.Set; @@ -22,14 +20,18 @@ public class ProblemContentProposalProvider extends IdeContentProposalProvider { @Override protected boolean filterKeyword(Keyword keyword, ContentAssistContext context) { var currentModel = context.getCurrentModel(); - if (SHADOW_KEYWORDS.contains(keyword.getValue())) { + var value = keyword.getValue(); + if (SHADOW_KEYWORDS.contains(value)) { return ProblemUtil.mayReferToShadow(currentModel); } - if ("pred".equals(keyword.getValue()) && + if ("pred".equals(value) && (currentModel instanceof Parameter || currentModel instanceof ParametricDefinition)) { // The {@code pred} keyword may only appear as a parameter kind in annotation declarations. return EcoreUtil2.getContainerOfType(currentModel, AnnotationDeclaration.class) != null; } + if ("assert".equals(value)) { + return ProblemUtil.supportsTheoryActions(currentModel); + } return super.filterKeyword(keyword, context); } } diff --git a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemProposalUtils.java b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemProposalUtils.java index 5d11fac1b..873906922 100644 --- a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemProposalUtils.java +++ b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemProposalUtils.java @@ -145,8 +145,9 @@ private static String getEClassDescription(IEObjectDescription candidate, EObjec if (ProblemPackage.Literals.AGGREGATOR_DECLARATION.isSuperTypeOf(eClass)) { return "aggregator"; } - if (ProblemPackage.Literals.ANNOTATION_DECLARATION.isSuperTypeOf(eClass)) { - // In contexts where we are auto-completing an annotation name, its type is obvious. + if (ProblemPackage.Literals.ANNOTATION_DECLARATION.isSuperTypeOf(eClass) || + ProblemPackage.Literals.THEORY_DECLARATION.isSuperTypeOf(eClass)) { + // In contexts where we are auto-completing an annotation or theory name, its type is obvious. return null; } return eClass.getName(); @@ -168,7 +169,7 @@ private static String getEClassDescription(IEObjectDescription candidate, EObjec return "atom"; } if (isMulti(candidate, eObject)) { - return "mutli"; + return "multi"; } return "node"; } @@ -347,6 +348,9 @@ private static String getEClassKind(EClass eClass, IEObjectDescription candidate if (ProblemPackage.Literals.AGGREGATOR_DECLARATION.isSuperTypeOf(eClass)) { return "aggregator"; } + if (ProblemPackage.Literals.THEORY_DECLARATION.isSuperTypeOf(eClass)) { + return "theory"; + } if (ProblemPackage.Literals.PROBLEM.isSuperTypeOf(eClass)) { return "module"; } diff --git a/subprojects/language-model/problem.aird b/subprojects/language-model/problem.aird index ec6897291..288bb8370 100644 --- a/subprojects/language-model/problem.aird +++ b/subprojects/language-model/problem.aird @@ -1,13 +1,13 @@ - + src/main/resources/model/problem.ecore src/main/resources/model/problem.genmodel build/resources/main/model/problem.ecore build/resources/main/model/problem.genmodel - + @@ -19,11 +19,11 @@ - + - + @@ -610,6 +610,19 @@ + + + + + + + + + + + + + @@ -1540,17 +1553,17 @@ - + - + - + - + @@ -1698,6 +1711,38 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -1823,7 +1868,7 @@ - + KEEP_LOCATION @@ -1980,7 +2025,7 @@ - + KEEP_LOCATION @@ -3404,6 +3449,47 @@ + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + @@ -6355,20 +6441,16 @@ - + - - - - - + @@ -6463,10 +6545,6 @@ - - - - @@ -6475,7 +6553,59 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -6558,6 +6688,86 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -6573,7 +6783,7 @@ - + KEEP_LOCATION @@ -6595,15 +6805,6 @@ - - - - - italic - - - - @@ -6710,7 +6911,7 @@ - + @@ -6749,7 +6950,7 @@ - + KEEP_LOCATION @@ -6776,15 +6977,6 @@ - - - - - italic - - - - @@ -6834,6 +7026,142 @@ + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + + + + + + + + + + + + + + + + + + + + italic + + + + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + italic + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + italic + + + + + + + + + + + + + + + + + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + + + + + + italic + + + + + + + + + + + + + labelSize + + + + @@ -6851,7 +7179,7 @@ - + @@ -6877,7 +7205,7 @@ - + @@ -7091,6 +7419,15 @@ + + + + + + + + + @@ -7556,6 +7893,22 @@ + + + + + + + + + + + + + + + + @@ -7863,7 +8216,7 @@ - + KEEP_LOCATION @@ -8238,6 +8591,26 @@ + + + + + + + + + + + + + + + italic + + + + + diff --git a/subprojects/language-model/src/main/resources/model/problem.ecore b/subprojects/language-model/src/main/resources/model/problem.ecore index 2e206e231..2ee7b70b9 100644 --- a/subprojects/language-model/src/main/resources/model/problem.ecore +++ b/subprojects/language-model/src/main/resources/model/problem.ecore @@ -326,4 +326,11 @@ + + + + + + diff --git a/subprojects/language-model/src/main/resources/model/problem.genmodel b/subprojects/language-model/src/main/resources/model/problem.genmodel index 555aaa825..0114d59c1 100644 --- a/subprojects/language-model/src/main/resources/model/problem.genmodel +++ b/subprojects/language-model/src/main/resources/model/problem.genmodel @@ -277,5 +277,11 @@ + + + + + + diff --git a/subprojects/language-semantics-z3/build.gradle.kts b/subprojects/language-semantics-z3/build.gradle.kts new file mode 100644 index 000000000..821c4f74d --- /dev/null +++ b/subprojects/language-semantics-z3/build.gradle.kts @@ -0,0 +1,19 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ + +plugins { + id("tools.refinery.gradle.java-library") +} + +mavenArtifact { + name = "Language Semantics Z3" + description = "Partial modeling language bindings for the Z3 SMT solver" +} + +dependencies { + api(project(":refinery-language-semantics")) + implementation(project(":refinery-store-reasoning-smt")) +} diff --git a/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Annotations.java b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Annotations.java new file mode 100644 index 000000000..fe7724f03 --- /dev/null +++ b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Annotations.java @@ -0,0 +1,92 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.semantics.z3; + +import org.eclipse.xtext.naming.QualifiedName; +import tools.refinery.language.annotations.Annotation; +import tools.refinery.language.annotations.DeclarativeAnnotationValidator; +import tools.refinery.language.annotations.ValidateAnnotation; + +import java.math.BigInteger; + +public class Z3Annotations extends DeclarativeAnnotationValidator { + public static final QualifiedName Z3_TIMEOUT = Z3Library.Z3_LIBRARY.append("z3Timeout"); + public static final String Z3_TIMEOUT_MILLISECONDS = "milliseconds"; + public static final QualifiedName Z3_RLIMIT = Z3Library.Z3_LIBRARY.append("z3Rlimit"); + public static final String Z3_RLIMIT_RLIMIT = "rlimit"; + + public static final BigInteger MAX_TIMEOUT_MILLISECONDS = + getValueFromEnvironment("REFINERY_Z3_MAX_TIMEOUT_MS", 10_000); + public static final BigInteger DEFAULT_TIMEOUT_MILLISECONDS = + getBoundedValueFromEnvironment("REFINERY_Z3_DEFAULT_TIMEOUT_MS", MAX_TIMEOUT_MILLISECONDS); + public static final BigInteger MAX_RLIMIT = + getValueFromEnvironment("REFINERY_Z3_MAX_RLIMIT", 100_000); + public static final BigInteger DEFAULT_RLIMIT = + getBoundedValueFromEnvironment("REFINERY_Z3_DEFAULT_RLIMIT", MAX_RLIMIT); + + private static BigInteger getValueFromEnvironment(String name, int defaultValue) { + return getValueFromEnvironment(name, BigInteger.valueOf(defaultValue)); + } + + private static BigInteger getBoundedValueFromEnvironment(String name, BigInteger maxValue) { + var value = getValueFromEnvironment(name, maxValue); + if (value.compareTo(maxValue) > 0) { + throw new IllegalArgumentException("%s cannot be larger than %s.".formatted(name, maxValue)); + } + return value; + } + + private static BigInteger getValueFromEnvironment(String name, BigInteger defaultValue) { + var stringValue = System.getenv(name); + if (stringValue == null) { + return defaultValue; + } + BigInteger value; + try { + value = new BigInteger(stringValue); + } catch (NullPointerException e) { + throw new IllegalArgumentException("%s must be an integer.".formatted(name), e); + } + if (value.compareTo(BigInteger.ZERO) <= 0) { + throw new IllegalArgumentException("%s must be positive.".formatted(name)); + } + return value; + } + + @ValidateAnnotation("Z3_TIMEOUT") + private void validateTimeout(Annotation annotation) { + var timeoutOption = annotation.getBigInteger(Z3_TIMEOUT_MILLISECONDS); + if (timeoutOption.isEmpty()) { + error("Must specify timeout %s.".formatted(Z3_TIMEOUT_MILLISECONDS), annotation); + return; + } + var timeout = timeoutOption.get(); + if (timeout.compareTo(BigInteger.ZERO) <= 0) { + error("Timeout must be positive.", annotation); + return; + } + if (timeout.compareTo(MAX_TIMEOUT_MILLISECONDS) > 0) { + error("Timeout cannot be larger than %s.".formatted(MAX_TIMEOUT_MILLISECONDS), annotation); + } + } + + @ValidateAnnotation("Z3_RLIMIT") + private void validateRlimit(Annotation annotation) { + var rlimitOption = annotation.getBigInteger(Z3_RLIMIT_RLIMIT); + if (rlimitOption.isEmpty()) { + error("Must specify %s.".formatted(Z3_RLIMIT_RLIMIT), annotation); + return; + } + var rlimit = rlimitOption.get(); + if (rlimit.compareTo(BigInteger.ZERO) <= 0) { + error("Resource limit must be positive.", annotation); + return; + } + if (rlimit.compareTo(MAX_RLIMIT) > 0) { + error("Resource limit cannot be larger than %s.".formatted(MAX_RLIMIT), annotation); + } + } +} diff --git a/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Library.java b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Library.java new file mode 100644 index 000000000..77d8abcdf --- /dev/null +++ b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Library.java @@ -0,0 +1,26 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.semantics.z3; + +import org.eclipse.xtext.naming.QualifiedName; +import tools.refinery.language.library.ClasspathBasedLibrary; + +import java.util.List; + +public class Z3Library extends ClasspathBasedLibrary { + public static final QualifiedName Z3_LIBRARY = QualifiedName.create("builtin", "theory", "z3"); + public static final QualifiedName Z3_CORE_LIBRARY = Z3_LIBRARY.append("core"); + + public Z3Library() { + addLibrary(Z3_LIBRARY); + addLibrary(Z3_CORE_LIBRARY); + } + + @Override + public List getAutomaticImports() { + return List.of(Z3_CORE_LIBRARY); + } +} diff --git a/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Theory.java b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Theory.java new file mode 100644 index 000000000..0a63d8d8a --- /dev/null +++ b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Theory.java @@ -0,0 +1,42 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.semantics.z3; + +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.reasoning.smt.SmtPropagator; +import tools.refinery.store.reasoning.smt.expr.SmtExprChecker; +import tools.refinery.store.reasoning.theory.Theory; +import tools.refinery.store.reasoning.theory.TheoryRule; +import tools.refinery.store.reasoning.theory.TheorySupport; + +import java.util.Collection; + +class Z3Theory implements Theory { + private final SmtExprChecker checker = new SmtExprChecker(); + private final int timeout; + private final int rlimit; + + public Z3Theory(int timeout, int rlimit) { + this.timeout = timeout; + this.rlimit = rlimit; + } + + @Override + public TheorySupport checkSupport(TheoryRule theoryRule) { + if (checker.isSupported(theoryRule.assertedTerm())) { + return TheorySupport.ENABLED_BY_DEFAULT; + } + return TheorySupport.UNSUPPORTED; + } + + @Override + public void createPropagator(ModelStoreBuilder storeBuilder, Collection collectedRules) { + storeBuilder.with(new SmtPropagator() + .rules(collectedRules) + .timeout(timeout) + .rlimit(rlimit)); + } +} diff --git a/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3TheoryProvider.java b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3TheoryProvider.java new file mode 100644 index 000000000..242594398 --- /dev/null +++ b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3TheoryProvider.java @@ -0,0 +1,34 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.semantics.z3; + +import org.eclipse.xtext.naming.QualifiedName; +import tools.refinery.language.annotations.Annotations; +import tools.refinery.language.semantics.ProblemTrace; +import tools.refinery.language.semantics.theory.TheoryProvider; +import tools.refinery.store.reasoning.theory.Theory; + +import java.util.Optional; + +public class Z3TheoryProvider implements TheoryProvider { + public static final QualifiedName Z3_THEORY = Z3Library.Z3_CORE_LIBRARY.append("z3"); + + @Override + public Optional createTheory(QualifiedName theoryName, Annotations annotations, ProblemTrace trace) { + if (!Z3_THEORY.equals(theoryName)) { + return Optional.empty(); + } + int timeout = annotations.getAnnotation(Z3Annotations.Z3_TIMEOUT) + .flatMap(annotation -> annotation.getBigInteger(Z3Annotations.Z3_TIMEOUT_MILLISECONDS)) + .orElse(Z3Annotations.DEFAULT_TIMEOUT_MILLISECONDS) + .intValue(); + int rlimit = annotations.getAnnotation(Z3Annotations.Z3_RLIMIT) + .flatMap(annotation -> annotation.getBigInteger(Z3Annotations.Z3_RLIMIT_RLIMIT)) + .orElse(Z3Annotations.DEFAULT_RLIMIT) + .intValue(); + return Optional.of(new Z3Theory(timeout, rlimit)); + } +} diff --git a/subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.annotations.AnnotationValidator b/subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.annotations.AnnotationValidator new file mode 100644 index 000000000..2aab494d0 --- /dev/null +++ b/subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.annotations.AnnotationValidator @@ -0,0 +1,5 @@ +# SPDX-FileCopyrightText: 2026 The Refinery Authors +# +# SPDX-License-Identifier: EPL-2.0 + +tools.refinery.language.semantics.z3.Z3Annotations diff --git a/subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.library.RefineryLibrary b/subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.library.RefineryLibrary new file mode 100644 index 000000000..aeadaee78 --- /dev/null +++ b/subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.library.RefineryLibrary @@ -0,0 +1,5 @@ +# SPDX-FileCopyrightText: 2026 The Refinery Authors +# +# SPDX-License-Identifier: EPL-2.0 + +tools.refinery.language.semantics.z3.Z3Library diff --git a/subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.semantics.theory.TheoryProvider b/subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.semantics.theory.TheoryProvider new file mode 100644 index 000000000..6dc0bd290 --- /dev/null +++ b/subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.semantics.theory.TheoryProvider @@ -0,0 +1,5 @@ +# SPDX-FileCopyrightText: 2026 The Refinery Authors +# +# SPDX-License-Identifier: EPL-2.0 + +tools.refinery.language.semantics.z3.Z3TheoryProvider diff --git a/subprojects/language-semantics-z3/src/main/resources/tools/refinery/language/semantics/z3/builtin/theory/z3.refinery b/subprojects/language-semantics-z3/src/main/resources/tools/refinery/language/semantics/z3/builtin/theory/z3.refinery new file mode 100644 index 000000000..698b87a11 --- /dev/null +++ b/subprojects/language-semantics-z3/src/main/resources/tools/refinery/language/semantics/z3/builtin/theory/z3.refinery @@ -0,0 +1,9 @@ +% SPDX-FileCopyrightText: 2026 The Refinery Authors +% +% SPDX-License-Identifier: EPL-2.0 + +import builtin::theory::z3::core. + +#pred z3Timeout(int milliseconds). + +#pred z3Rlimit(int rlimit). diff --git a/subprojects/language-semantics-z3/src/main/resources/tools/refinery/language/semantics/z3/builtin/theory/z3/core.refinery b/subprojects/language-semantics-z3/src/main/resources/tools/refinery/language/semantics/z3/builtin/theory/z3/core.refinery new file mode 100644 index 000000000..6a3a29115 --- /dev/null +++ b/subprojects/language-semantics-z3/src/main/resources/tools/refinery/language/semantics/z3/builtin/theory/z3/core.refinery @@ -0,0 +1,5 @@ +% SPDX-FileCopyrightText: 2026 The Refinery Authors +% +% SPDX-License-Identifier: EPL-2.0 + +#theory z3. diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java index 6e1d5f605..d9072d300 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java @@ -7,6 +7,7 @@ import com.google.inject.Inject; import org.eclipse.xtext.naming.IQualifiedNameProvider; +import tools.refinery.language.annotations.AnnotationContext; import tools.refinery.language.expressions.ExprToTerm; import tools.refinery.language.library.BuiltinLibrary; import tools.refinery.language.model.problem.*; @@ -14,10 +15,11 @@ import tools.refinery.language.scoping.imports.ImportCollector; import tools.refinery.language.semantics.internal.MutableRelationCollector; import tools.refinery.language.semantics.internal.MutableSeed; +import tools.refinery.language.semantics.internal.annotations.TopLevelAnnotations; import tools.refinery.language.semantics.internal.query.FunctionCompiler; import tools.refinery.language.semantics.internal.query.QueryCompiler; import tools.refinery.language.semantics.internal.query.RuleCompiler; -import tools.refinery.language.typesystem.DataExprType; +import tools.refinery.language.semantics.theory.internal.TheoryManager; import tools.refinery.language.typesystem.SignatureProvider; import tools.refinery.language.utils.BuiltinAnnotationContext; import tools.refinery.language.utils.BuiltinSymbols; @@ -106,13 +108,19 @@ public class ModelInitializer { @Inject private ExprToTerm exprToTerm; + @Inject + private AnnotationContext annotationContext; + + @Inject + private TheoryManager theoryManager; + private boolean keepNonExistingObjects; private boolean keepShadowPredicates = true; private Problem problem; - private final Set importedProblems = new HashSet<>(); + private final Set importedProblems = new LinkedHashSet<>(); private BuiltinSymbols builtinSymbols; @@ -149,11 +157,13 @@ public void readProblem(Problem problem) { this.problem = problem; loadImportedProblems(); importedProblems.add(problem); + var topLevelAnnotations = new TopLevelAnnotations(annotationContext, problem, importedProblems); + theoryManager.initialize(topLevelAnnotations, problemTrace, importedProblems); mutableRelationCollector.collectMutableRelations(importedProblems); problemTrace.setProblem(problem); queryCompiler.setProblemTrace(problemTrace); - ruleCompiler.setQueryCompiler(queryCompiler); - functionCompiler.setQueryCompiler(queryCompiler); + ruleCompiler.initialize(queryCompiler, theoryManager); + functionCompiler.initialize(queryCompiler); try { builtinSymbols = importAdapterProvider.getBuiltinSymbols(problem); var nodeInfo = collectPartialRelation(builtinSymbols.node(), 1, TruthValue.TRUE, TruthValue.TRUE); @@ -243,6 +253,7 @@ public void configureStoreBuilder(ModelStoreBuilder storeBuilder) { } collectPredicates(storeBuilder); collectRules(storeBuilder); + theoryManager.configure(storeBuilder); storeBuilder.tryGetAdapter(StateCoderBuilder.class) .ifPresent(stateCoderBuilder -> stateCoderBuilder.individuals(individuals)); if (!keepShadowPredicates) { @@ -397,12 +408,8 @@ private void collectAttribute(DatatypeDeclaration datatypeDeclaration, Reference private AnyAbstractDomain getAbstractDomain(DatatypeDeclaration datatype, Relation relation) { var type = signatureProvider.getDataType(datatype); - if (!(type instanceof DataExprType dataExprType)) { - throw new TracedException(relation, "Invalid type '%s' for function '%s'.".formatted( - type, relation.getName())); - } return importAdapterProvider.getTermInterpreter(relation) - .getDomain(dataExprType) + .getDomain(type) .orElseThrow(() -> new TracedException(relation, "No abstract domain for datatype '%s'.".formatted(datatype.getName()))); } @@ -1073,6 +1080,7 @@ private void collectRule(RuleDefinition ruleDefinition, ModelStoreBuilder storeB ConcretenessSpecification.CANDIDATE); rules.addAll(propagationRules); rules.addAll(concretizationRules); + ruleCompiler.createTheoryRules(name, ruleDefinition, ConcretenessSpecification.UNSPECIFIED); problemTrace.putPropagationRuleDefinition(ruleDefinition, List.copyOf(rules)); storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(propagationBuilder -> { propagationBuilder.rules(propagationRules); @@ -1081,6 +1089,7 @@ private void collectRule(RuleDefinition ruleDefinition, ModelStoreBuilder storeB } case CONCRETIZATION -> { var rules = ruleCompiler.toPropagationRules(name, ruleDefinition, ConcretenessSpecification.CANDIDATE); + ruleCompiler.createTheoryRules(name, ruleDefinition, ConcretenessSpecification.CANDIDATE); problemTrace.putPropagationRuleDefinition(ruleDefinition, rules); storeBuilder.tryGetAdapter(PropagationBuilder.class) .ifPresent(propagationBuilder -> propagationBuilder.concretizationRules(rules)); diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/annotations/TopLevelAnnotations.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/annotations/TopLevelAnnotations.java new file mode 100644 index 000000000..60744236a --- /dev/null +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/annotations/TopLevelAnnotations.java @@ -0,0 +1,67 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.semantics.internal.annotations; + +import org.eclipse.emf.ecore.EObject; +import org.eclipse.xtext.naming.QualifiedName; +import tools.refinery.language.annotations.Annotation; +import tools.refinery.language.annotations.AnnotationContext; +import tools.refinery.language.annotations.Annotations; +import tools.refinery.language.model.problem.Problem; + +import java.util.Collection; +import java.util.Optional; +import java.util.stream.Stream; + +public class TopLevelAnnotations implements Annotations { + private final Problem annotatedElement; + private final Collection allAnnotations; + + public TopLevelAnnotations(AnnotationContext context, Problem problem, Collection importedProblems) { + annotatedElement = problem; + allAnnotations = importedProblems.stream() + .map(context::annotationsFor) + .toList(); + } + + @Override + public EObject getAnnotatedElement() { + return annotatedElement; + } + + @Override + public boolean hasAnnotation(QualifiedName annotationName) { + for (var annotations : allAnnotations) { + if (annotations.hasAnnotation(annotationName)) { + return true; + } + } + return false; + } + + @Override + public Optional getAnnotation(QualifiedName annotationName) { + for (var annotations : allAnnotations) { + var result = annotations.getAnnotation(annotationName); + if (result.isPresent()) { + return result; + } + } + return Optional.empty(); + } + + @Override + public Stream getAnnotations(QualifiedName annotationName) { + return allAnnotations.stream() + .flatMap(annotations -> annotations.getAnnotations(annotationName)); + } + + @Override + public Stream getAllAnnotations() { + return allAnnotations.stream() + .flatMap(Annotations::getAllAnnotations); + } +} diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/query/FunctionCompiler.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/query/FunctionCompiler.java index cbbd4712a..bf6527e4e 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/query/FunctionCompiler.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/query/FunctionCompiler.java @@ -43,7 +43,7 @@ public class FunctionCompiler { private QueryCompiler queryCompiler; - public void setQueryCompiler(QueryCompiler queryCompiler) { + public void initialize(QueryCompiler queryCompiler) { this.queryCompiler = queryCompiler; } diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/query/RuleCompiler.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/query/RuleCompiler.java index e645f27b3..cb7259746 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/query/RuleCompiler.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/query/RuleCompiler.java @@ -10,6 +10,7 @@ import tools.refinery.language.model.problem.*; import tools.refinery.language.semantics.SemanticsUtils; import tools.refinery.language.semantics.TracedException; +import tools.refinery.language.semantics.theory.internal.TheoryManager; import tools.refinery.language.utils.BuiltinAnnotationContext; import tools.refinery.language.utils.ParameterBinding; import tools.refinery.language.validation.ReferenceCounter; @@ -32,6 +33,7 @@ import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.representation.PartialFunction; import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.theory.TheoryRule; import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; import java.util.*; @@ -48,8 +50,11 @@ public class RuleCompiler { private QueryCompiler queryCompiler; - public void setQueryCompiler(QueryCompiler queryCompiler) { + private TheoryManager theoryManager; + + public void initialize(QueryCompiler queryCompiler, TheoryManager theoryManager) { this.queryCompiler = queryCompiler; + this.theoryManager = theoryManager; } public DecisionRule toDecisionRule(String name, RuleDefinition ruleDefinition) { @@ -166,8 +171,12 @@ public Collection toPropagationRules(String name, RuleDefinition ruleDefin var rules = new ArrayList(actionCount); var postConditionModality = new ConcreteModality(concreteness, ModalitySpecification.MAY); for (int i = 0; i < actionCount; i++) { - var actionName = actionCount == 1 ? name : name + "#" + (i + 1); var action = actions.get(i); + if (action instanceof TheoryAction) { + continue; + // Theory actions are handled separately. + } + var actionName = getPropagationActionName(name, actionCount, i); try { var wrappedAction = wrapAction(action, preparedRule); var parameters = wrappedAction.getNodeVariables(); @@ -203,6 +212,44 @@ public Collection toPropagationRules(String name, RuleDefinition ruleDefin return rules; } + private static String getPropagationActionName(String name, int actionCount, int i) { + return actionCount == 1 ? name : name + "#" + (i + 1); + } + + public void createTheoryRules(String name, RuleDefinition ruleDefinition, + ConcretenessSpecification concretenessSpecification) { + var preparedRule = prepareRule(ruleDefinition, false); + var parameterMap = preparedRule.parameterMap(); + var consequents = ruleDefinition.getConsequents(); + if (consequents.isEmpty()) { + return; + } + var actions = consequents.getFirst().getActions(); + int actionCount = actions.size(); + for (int i = 0; i < actionCount; i++) { + var action = actions.get(i); + if (!(action instanceof TheoryAction theoryAction)) { + continue; + } + var actionName = getPropagationActionName(name, actionCount, i); + try { + var expr = theoryAction.getTerm(); + var moreCommonLiterals = new ArrayList(); + var term = queryCompiler.interpretTerm(expr, parameterMap, moreCommonLiterals) + .asType(TruthValue.class); + var parameters = term.getInputVariables(Set.copyOf(parameterMap.values())).stream() + .map(Variable::asNodeVariable) + .toList(); + var query = preparedRule.buildQuery(actionName, parameters, moreCommonLiterals, queryCompiler); + var theoryRule = new TheoryRule(query, term, concretenessSpecification); + theoryManager.addRule(theoryAction, theoryRule); + + } catch (RuntimeException e) { + throw TracedException.addTrace(action, e); + } + } + } + public Rule toRule(String name, RuleDefinition ruleDefinition) { var preparedRule = prepareRule(ruleDefinition, true); var parameters = preparedRule.allParameters(); diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/theory/TheoryProvider.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/theory/TheoryProvider.java new file mode 100644 index 000000000..09b7fa0e4 --- /dev/null +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/theory/TheoryProvider.java @@ -0,0 +1,18 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.semantics.theory; + +import org.eclipse.xtext.naming.QualifiedName; +import tools.refinery.language.annotations.Annotations; +import tools.refinery.language.semantics.ProblemTrace; +import tools.refinery.store.reasoning.theory.Theory; + +import java.util.Optional; + +@FunctionalInterface +public interface TheoryProvider { + Optional createTheory(QualifiedName theoryName, Annotations annotations, ProblemTrace trace); +} diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/theory/internal/TheoryManager.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/theory/internal/TheoryManager.java new file mode 100644 index 000000000..8c128260e --- /dev/null +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/theory/internal/TheoryManager.java @@ -0,0 +1,183 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.semantics.theory.internal; + +import com.google.inject.Inject; +import com.google.inject.Injector; +import org.eclipse.xtext.naming.IQualifiedNameProvider; +import tools.refinery.language.annotations.Annotations; +import tools.refinery.language.model.problem.Problem; +import tools.refinery.language.model.problem.TheoryAction; +import tools.refinery.language.model.problem.TheoryDeclaration; +import tools.refinery.language.semantics.ProblemTrace; +import tools.refinery.language.semantics.TracedException; +import tools.refinery.language.semantics.theory.TheoryProvider; +import tools.refinery.language.utils.BuiltinAnnotationContext; +import tools.refinery.language.utils.ServiceUtil; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.reasoning.theory.Theory; +import tools.refinery.store.reasoning.theory.TheoryRule; +import tools.refinery.store.reasoning.theory.TheorySupport; + +import java.util.*; + +public class TheoryManager { + private static final List> DEFAULT_THEORY_PROVIDERS = + ServiceUtil.loadServices(TheoryProvider.class); + + private final List theoryProviders; + private final IQualifiedNameProvider qualifiedNameProvider; + private final BuiltinAnnotationContext builtinAnnotationContext; + private Annotations annotations; + private ProblemTrace trace; + private final Map theories = new LinkedHashMap<>(); + + @Inject + public TheoryManager(Injector injector, IQualifiedNameProvider qualifiedNameProvider, + BuiltinAnnotationContext builtinAnnotationContext) { + this.qualifiedNameProvider = qualifiedNameProvider; + theoryProviders = ServiceUtil.instantiate(injector, DEFAULT_THEORY_PROVIDERS); + this.builtinAnnotationContext = builtinAnnotationContext; + } + + public List getTheoryProviders() { + return theoryProviders; + } + + public void initialize(Annotations annotations, ProblemTrace trace, Collection importedProblems) { + this.annotations = annotations; + this.trace = trace; + theories.clear(); + for (var problem : importedProblems) { + for (var statement : problem.getStatements()) { + if (statement instanceof TheoryDeclaration theoryDeclaration) { + var theory = getTheory(theoryDeclaration); + int priority = builtinAnnotationContext.getPriority(theoryDeclaration); + theories.put(theoryDeclaration, new ManagedTheory(theoryDeclaration, theory, priority)); + } + } + } + } + + private Theory getTheory(TheoryDeclaration theoryDeclaration) { + var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(theoryDeclaration); + if (qualifiedName == null) { + throw new TracedException(theoryDeclaration, "No qualified name for theory."); + } + try { + for (var theoryProvider : theoryProviders) { + var result = theoryProvider.createTheory(qualifiedName, annotations, trace); + if (result.isPresent()) { + return result.get(); + } + } + } catch (RuntimeException e) { + throw new TracedException(theoryDeclaration, "Error while instantiating theory.", e); + } + throw new TracedException(theoryDeclaration, "No theory registered for theory declaration '%s'." + .formatted(theoryDeclaration.getName())); + } + + public void addRule(TheoryAction action, TheoryRule rule) { + if (action.isTheoryOverride()) { + addRuleWithTheoryOverride(action, rule); + return; + } + addRuleWithDefaultTheories(action, rule); + } + + private void addRuleWithTheoryOverride(TheoryAction action, TheoryRule rule) { + for (var theory : action.getTheories()) { + if (theory == null || theory.eIsProxy()) { + throw new TracedException(action, "Unresolved reference to theory."); + } + var managedTheory = theories.get(theory); + if (managedTheory == null) { + throw new TracedException(action, "Unknown theory '%s'.".formatted(theory.getName())); + } + var support = managedTheory.checkSupport(rule); + if (!support.isSupported()) { + throw new TracedException(action, "Theory '%s' does not support this assertion." + .formatted(theory.getName())); + } + managedTheory.addRule(rule); + } + } + + private void addRuleWithDefaultTheories(TheoryAction action, TheoryRule rule) { + int maxPriority = Integer.MIN_VALUE; + var matchedTheories = new ArrayList(); + boolean supported = false; + for (var managedTheory : theories.values()) { + var support = managedTheory.checkSupport(rule); + supported = supported || support.isSupported(); + if (support.isEnabledByDefault()) { + int priority = managedTheory.getPriority(); + if (priority < maxPriority) { + continue; + } + if (priority > maxPriority) { + maxPriority = priority; + matchedTheories.clear(); + } + matchedTheories.add(managedTheory); + } + } + if (matchedTheories.isEmpty()) { + if (supported) { + throw new TracedException(action, "No default theory is available for this assertion. " + + "Use the 'using' keyword to specify the intended theories."); + } + throw new TracedException(action, "No imported theory supports this assertion."); + } + for (var managedTheory : matchedTheories) { + managedTheory.addRule(rule); + } + } + + public void configure(ModelStoreBuilder storeBuilder) { + for (var managedTheory : theories.values()) { + managedTheory.configure(storeBuilder); + } + } + + private final static class ManagedTheory { + private final TheoryDeclaration declaration; + private final Theory theory; + private final int priority; + private final List rules; + + public ManagedTheory(TheoryDeclaration declaration, Theory theory, int priority) { + this.declaration = declaration; + this.theory = theory; + this.priority = priority; + rules = new ArrayList<>(); + } + + public int getPriority() { + return priority; + } + + public TheorySupport checkSupport(TheoryRule rule) { + return theory.checkSupport(rule); + } + + public void addRule(TheoryRule rule) { + rules.add(rule); + } + + public void configure(ModelStoreBuilder storeBuilder) { + if (rules.isEmpty()) { + return; + } + try { + theory.createPropagator(storeBuilder, rules); + } catch (RuntimeException e) { + throw new TracedException(declaration, "Error while creating propagator.", e); + } + } + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext index 3af136f25..78df107d6 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext @@ -41,6 +41,9 @@ AnnotatedStatement returns Statement: {OverloadedDeclaration.annotations=current} "#" "primitive" shadow?="shadow"? name=Identifier "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")" "." + | + {TheoryDeclaration.annotations=current} + "#" "theory" name=Identifier "." | {PredicateDefinition.annotations=current} (kind=ErrorPredicateKind | kind=PredicateKind? "pred") @@ -140,7 +143,7 @@ Consequent: actions+=Action ("," actions+=Action)*; Action: - AssertionAction; + AssertionAction | TheoryAction; AssertionAction: relation=[Relation|QualifiedName] @@ -150,6 +153,14 @@ AssertionAction: relation=[Relation|QualifiedName] "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")"; +TheoryAction: + "assert" term=Expr + (theoryOverride?="using" ( + theories+=[TheoryDeclaration|QualifiedName] | + "{" (theories+=[TheoryDeclaration|QualifiedName] + ("," theories+=[TheoryDeclaration|QualifiedName])*)? "}" + ))?; + Expr: AssignmentExpr; @@ -330,7 +341,7 @@ NonContainmentIdentifier: ID | QUOTED_ID | "as" | "atom" | "multi" | "problem" | "module" | "datatype" | "aggregator" | "primitive" | "decision" | "propagation" | "concretization" | - "shadow"; + "shadow" | "assert" | "theory" | "using"; Integer returns ecore::EBigInteger: INT; diff --git a/subprojects/language/src/main/java/tools/refinery/language/annotations/BuiltinAnnotations.java b/subprojects/language/src/main/java/tools/refinery/language/annotations/BuiltinAnnotations.java index fdda6a89e..43ef90420 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/annotations/BuiltinAnnotations.java +++ b/subprojects/language/src/main/java/tools/refinery/language/annotations/BuiltinAnnotations.java @@ -150,7 +150,7 @@ private void validateDecide(Annotation annotation) { var concretize = annotationsFor(relation).getAnnotation(CONCRETIZE) .flatMap(a -> a.getBoolean(CONCRETIZE_AUTO)); boolean defaultValue; - if (concretize.isPresent() && Boolean.FALSE.equals(concretize.get())) { + if (concretize.isPresent() && !concretize.get()) { defaultValue = false; } else { defaultValue = ProblemUtil.isDecideByDefault(relation); @@ -198,19 +198,21 @@ private void validateClassDeclarationDecide(Annotation annotation, ClassDeclarat } } - @ValidateAnnotation("PRIORITY") - @ValidateAnnotation("WEIGHT") - private void validateDecisionRuleAnnotation(Annotation annotation) { - if (!(annotation.getAnnotatedElement() instanceof RuleDefinition ruleDefinition) || - !RuleKind.DECISION.equals(ruleDefinition.getKind())) { - var message = "@%s can only be applied to decision rules." - .formatted(annotation.getAnnotation().getDeclaration().getName()); - error(message, annotation); - } + // This method does not make sense inverted. + @SuppressWarnings("BooleanMethodIsAlwaysInverted") + private boolean isDecisionRuleDefinition(EObject annotatedElement) { + return annotatedElement instanceof RuleDefinition ruleDefinition && + RuleKind.DECISION.equals(ruleDefinition.getKind()); } @ValidateAnnotation("PRIORITY") private void validatePriority(Annotation annotation) { + var annotatedElement = annotation.getAnnotatedElement(); + if (!isDecisionRuleDefinition(annotatedElement) && !(annotatedElement instanceof TheoryDeclaration)) { + var message = "@%s can only be applied to decision rules and theory declarations." + .formatted(annotation.getAnnotation().getDeclaration().getName()); + error(message, annotation); + } var value = annotation.getBigInteger(PRIORITY_VALUE) .map(BigInteger::intValue) .orElse(DecisionSettings.DEFAULT_PRIORITY); @@ -223,6 +225,11 @@ private void validatePriority(Annotation annotation) { @ValidateAnnotation("WEIGHT") private void validateWeight(Annotation annotation) { + if (!isDecisionRuleDefinition(annotation.getAnnotatedElement())) { + var message = "@%s can only be applied to decision rules." + .formatted(annotation.getAnnotation().getDeclaration().getName()); + error(message, annotation); + } var coefficient = annotation.getBigDecimal(WEIGHT_COEFFICIENT); var exponent = annotation.getBigDecimal(WEIGHT_EXPONENT); if (coefficient.isEmpty() && exponent.isEmpty()) { diff --git a/subprojects/language/src/main/java/tools/refinery/language/library/ClasspathBasedLibrary.java b/subprojects/language/src/main/java/tools/refinery/language/library/ClasspathBasedLibrary.java index 6e4b5fe16..9fa3ca2b6 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/library/ClasspathBasedLibrary.java +++ b/subprojects/language/src/main/java/tools/refinery/language/library/ClasspathBasedLibrary.java @@ -29,7 +29,6 @@ public abstract class ClasspathBasedLibrary implements RefineryLibrary { protected ClasspathBasedLibrary(Class context) { this.context = context == null ? getClass() : context; - } protected ClasspathBasedLibrary() { diff --git a/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java b/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java index c7e75e4c5..1d2f0c447 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java +++ b/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java @@ -39,6 +39,7 @@ public class ProblemResourceDescriptionStrategy extends DefaultResourceDescripti public static final String SHADOWING_KEY_RELATION = "relation"; public static final String SHADOWING_KEY_AGGREGATOR = "aggregator"; public static final String SHADOWING_KEY_ANNOTATION = "annotation"; + public static final String SHADOWING_KEY_THEORY = "theory"; public static final String PREFERRED_NAME = DATA_PREFIX + "PREFERRED_NAME"; public static final String PREFERRED_NAME_TRUE = "true"; public static final String IMPORTS = DATA_PREFIX + "IMPORTS"; @@ -145,7 +146,8 @@ public static boolean shouldExport(EObject eObject) { protected Map getUserData(EObject eObject) { var builder = ImmutableMap.builder(); - if (eObject instanceof Problem problem) { + switch (eObject) { + case Problem problem -> { builder.put(SHADOWING_KEY, SHADOWING_KEY_PROBLEM); var explicitImports = importCollector.getDirectImports(eObject.eResource()); var importsString = explicitImports.toList().stream() @@ -153,17 +155,19 @@ protected Map getUserData(EObject eObject) { .collect(Collectors.joining(IMPORTS_SEPARATOR)); builder.put(IMPORTS, importsString); builder.put(MODULE_KIND, problem.getKind().getName()); - } else if (eObject instanceof Node node) { - addNodeUserData(node, builder); - } else if (eObject instanceof Relation relation) { - addRelationUserData(relation, builder); - } else if (eObject instanceof RuleDefinition) { + } + case Node node -> addNodeUserData(node, builder); + case Relation relation -> addRelationUserData(relation, builder); + case RuleDefinition _ -> { // Rule definitions and predicates live in the same namespace. builder.put(SHADOWING_KEY, SHADOWING_KEY_RELATION); - } else if (eObject instanceof AggregatorDeclaration) { - builder.put(SHADOWING_KEY, SHADOWING_KEY_AGGREGATOR); - } else if (eObject instanceof AnnotationDeclaration) { - builder.put(SHADOWING_KEY, SHADOWING_KEY_ANNOTATION); + } + case AggregatorDeclaration _ -> builder.put(SHADOWING_KEY, SHADOWING_KEY_AGGREGATOR); + case AnnotationDeclaration _ -> builder.put(SHADOWING_KEY, SHADOWING_KEY_ANNOTATION); + case TheoryDeclaration _ -> builder.put(SHADOWING_KEY, SHADOWING_KEY_THEORY); + case null, default -> { + // No user data to add. + } } if (ProblemUtil.isError(eObject)) { builder.put(ERROR_PREDICATE, ERROR_PREDICATE_TRUE); diff --git a/subprojects/language/src/main/java/tools/refinery/language/resource/state/DerivedVariableComputer.java b/subprojects/language/src/main/java/tools/refinery/language/resource/state/DerivedVariableComputer.java index 7e7628435..d11bd9d42 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/resource/state/DerivedVariableComputer.java +++ b/subprojects/language/src/main/java/tools/refinery/language/resource/state/DerivedVariableComputer.java @@ -86,8 +86,14 @@ protected void installDerivedRuleDefinitionState(RuleDefinition definition, Set< } for (var consequent : definition.getConsequents()) { for (var action : consequent.getActions()) { - if (action instanceof AssertionAction assertionAction) { - createVariablesForScope(new ImplicitVariableScope(assertionAction, knownVariables)); + switch (action) { + case AssertionAction assertionAction -> + createVariablesForScope(new ImplicitVariableScope(assertionAction, knownVariables)); + case TheoryAction theoryAction -> + createVariablesForScope(new ImplicitVariableScope(theoryAction, knownVariables)); + default -> { + // No variables to infer. + } } } } diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java index 229892d99..fdb8cac7d 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java +++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java @@ -28,6 +28,7 @@ import tools.refinery.language.library.internal.CompositeLibrary; import tools.refinery.language.model.problem.Problem; import tools.refinery.language.utils.BuiltinSymbols; +import tools.refinery.language.utils.ServiceUtil; import java.io.File; import java.nio.file.Path; @@ -35,15 +36,15 @@ public class ImportAdapter extends AdapterImpl { private static final Logger LOG = Logger.getLogger(ImportAdapter.class); - private static final List> DEFAULT_LIBRARIES; - private static final List> DEFAULT_TERM_INTERPRETERS; - private static final List> DEFAULT_ANNOTATION_VALIDATORS; + private static final List> DEFAULT_LIBRARIES = + ServiceUtil.loadServices(RefineryLibrary.class); + private static final List> DEFAULT_TERM_INTERPRETERS = + ServiceUtil.loadServices(TermInterpreter.class); + private static final List> DEFAULT_ANNOTATION_VALIDATORS = + ServiceUtil.loadServices(AnnotationValidator.class); private static final List DEFAULT_PATHS; static { - DEFAULT_LIBRARIES = loadServices(RefineryLibrary.class); - DEFAULT_TERM_INTERPRETERS = loadServices(TermInterpreter.class); - DEFAULT_ANNOTATION_VALIDATORS = loadServices(AnnotationValidator.class); var pathEnv = System.getenv("REFINERY_LIBRARY_PATH"); if (pathEnv == null) { DEFAULT_PATHS = List.of(); @@ -55,22 +56,6 @@ public class ImportAdapter extends AdapterImpl { } } - private static List> loadServices(Class serviceClass) { - return ServiceLoader.load(serviceClass).stream() - .>mapMulti((provider, consumer) -> { - Class implementationClass = null; - try { - implementationClass = provider.type(); - } catch (ServiceConfigurationError e) { - LOG.error("Error loading service: " + serviceClass.getName(), e); - } - if (implementationClass != null) { - consumer.accept(implementationClass); - } - }) - .toList(); - } - private ResourceSet resourceSet; private final List libraries; private final List termInterpreters; @@ -88,30 +73,14 @@ private static List> loadServices(Class serviceClass) @Inject public ImportAdapter(Injector injector) { - libraries = instantiate(injector, DEFAULT_LIBRARIES); + libraries = ServiceUtil.instantiate(injector, DEFAULT_LIBRARIES); compositeLibrary = new CompositeLibrary(libraries); - termInterpreters = instantiate(injector, DEFAULT_TERM_INTERPRETERS); + termInterpreters = ServiceUtil.instantiate(injector, DEFAULT_TERM_INTERPRETERS); termInterpreter = new CompositeTermInterpreter(termInterpreters); - annotationValidators = instantiate(injector, DEFAULT_ANNOTATION_VALIDATORS); + annotationValidators = ServiceUtil.instantiate(injector, DEFAULT_ANNOTATION_VALIDATORS); annotationValidator = new CompositeAnnotationValidator(annotationValidators); } - private List instantiate(Injector injector, List> implementationClasses) { - var instances = new ArrayList(implementationClasses.size()); - for (var implementationClass : implementationClasses) { - T instance = null; - try { - instance = injector.getInstance(implementationClass); - } catch (RuntimeException e) { - LOG.error("Error loading service: " + implementationClass.getName(), e); - } - if (instance != null) { - instances.add(instance); - } - } - return instances; - } - void setResourceSet(ResourceSet resourceSet) { this.resourceSet = resourceSet; for (var resource : resourceSet.getResources()) { diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java index 9af3fd975..5ec7c3b16 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java +++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java @@ -91,6 +91,10 @@ public FixedType getDataType(Relation relation) { if (!(relation instanceof DatatypeDeclaration datatypeDeclaration)) { return FixedType.INVALID; } + return getDataType(datatypeDeclaration); + } + + public DataExprType getDataType(DatatypeDeclaration datatypeDeclaration) { var dataTypes = cache.get(DATATYPE_CACHE, datatypeDeclaration.eResource(), () -> new HashMap()); return dataTypes.computeIfAbsent(datatypeDeclaration, this::computeDataType); diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinAnnotationContext.java b/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinAnnotationContext.java index c41ea54c1..fbbb4b853 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinAnnotationContext.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinAnnotationContext.java @@ -9,13 +9,11 @@ import com.google.inject.Singleton; import org.eclipse.emf.ecore.EObject; import tools.refinery.language.annotations.AnnotationContext; +import tools.refinery.language.annotations.Annotations; import tools.refinery.language.annotations.BuiltinAnnotations; import tools.refinery.language.documentation.DocumentationCommentParser; import tools.refinery.language.documentation.TypeHashProvider; -import tools.refinery.language.model.problem.ClassDeclaration; -import tools.refinery.language.model.problem.Parameter; -import tools.refinery.language.model.problem.Relation; -import tools.refinery.language.model.problem.RuleDefinition; +import tools.refinery.language.model.problem.*; import java.math.BigInteger; import java.util.Optional; @@ -66,11 +64,7 @@ public boolean isClassDeclarationDecide(ClassDeclaration classDeclaration) { public DecisionSettings getDecisionSettings(RuleDefinition ruleDefinition) { var annotations = annotationContext.annotationsFor(ruleDefinition); - var priorityAnnotation = annotations.getAnnotation(BuiltinAnnotations.PRIORITY); - int priority = priorityAnnotation.map(annotation -> annotation.getBigInteger(BuiltinAnnotations.PRIORITY_VALUE) - .map(BigInteger::intValue) - .orElse(DecisionSettings.DEFAULT_PRIORITY)) - .orElse(DecisionSettings.DEFAULT_PRIORITY); + int priority = getPriority(annotations); var weighAnnotation = annotations.getAnnotation(BuiltinAnnotations.WEIGHT); if (weighAnnotation.isEmpty()) { return new DecisionSettings(priority); @@ -84,6 +78,19 @@ public DecisionSettings getDecisionSettings(RuleDefinition ruleDefinition) { return new DecisionSettings(priority, coefficient, exponent); } + public int getPriority(TheoryDeclaration theoryDeclaration) { + var annotations = annotationContext.annotationsFor(theoryDeclaration); + return getPriority(annotations); + } + + private int getPriority(Annotations annotations) { + var priorityAnnotation = annotations.getAnnotation(BuiltinAnnotations.PRIORITY); + return priorityAnnotation.map(annotation -> annotation.getBigInteger(BuiltinAnnotations.PRIORITY_VALUE) + .map(BigInteger::intValue) + .orElse(DecisionSettings.DEFAULT_PRIORITY)) + .orElse(DecisionSettings.DEFAULT_PRIORITY); + } + public String getColor(EObject eObject) { if (!(eObject instanceof ClassDeclaration)) { return null; diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java index 35cdee9d7..91fabae25 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java @@ -60,13 +60,27 @@ public static boolean isShadow(EObject eObject) { case PredicateDefinition predicateDefinition -> predicateDefinition.getKind() == PredicateKind.SHADOW; case FunctionDefinition functionDefinition -> functionDefinition.isShadow(); case OverloadedDeclaration overloadedDeclaration -> overloadedDeclaration.isShadow(); - default -> false; + case null, default -> false; }; } public static boolean mayReferToShadow(EObject context) { var definitionContext = EcoreUtil2.getContainerOfType(context, ParametricDefinition.class); - return isShadow(definitionContext) || definitionContext instanceof RuleDefinition; + if (!isShadow(definitionContext) && !(definitionContext instanceof RuleDefinition)) { + return false; + } + var theoryAction = EcoreUtil2.getContainerOfType(context, TheoryAction.class); + // Theory assertions must be abstract interpretable. + return theoryAction == null; + } + + public static boolean supportsTheoryActions(EObject context) { + var rule = EcoreUtil2.getContainerOfType(context, RuleDefinition.class); + if (rule == null) { + return false; + } + var kind = rule.getKind(); + return kind == RuleKind.PROPAGATION || kind == RuleKind.CONCRETIZATION; } public static boolean isAtomNode(Node node) { diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ServiceUtil.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ServiceUtil.java new file mode 100644 index 000000000..d088ff705 --- /dev/null +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ServiceUtil.java @@ -0,0 +1,54 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.utils; + +import com.google.inject.Injector; +import org.apache.log4j.Logger; + +import java.util.ArrayList; +import java.util.List; +import java.util.ServiceConfigurationError; +import java.util.ServiceLoader; + +public class ServiceUtil { + private static final Logger LOG = Logger.getLogger(ServiceUtil.class); + + private ServiceUtil() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static List> loadServices(Class serviceClass) { + return ServiceLoader.load(serviceClass).stream() + .>mapMulti((provider, consumer) -> { + Class implementationClass = null; + try { + implementationClass = provider.type(); + } catch (ServiceConfigurationError e) { + LOG.error("Error loading service: " + serviceClass.getName(), e); + } + if (implementationClass != null) { + consumer.accept(implementationClass); + } + }) + .toList(); + } + + public static List instantiate(Injector injector, List> implementationClasses) { + var instances = new ArrayList(implementationClasses.size()); + for (var implementationClass : implementationClasses) { + T instance = null; + try { + instance = injector.getInstance(implementationClass); + } catch (RuntimeException e) { + LOG.error("Error loading service: " + implementationClass.getName(), e); + } + if (instance != null) { + instances.add(instance); + } + } + return instances; + } +} diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ActionTargetCollector.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ActionTargetCollector.java index e4b7bcab6..01ed3eee5 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/validation/ActionTargetCollector.java +++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ActionTargetCollector.java @@ -62,13 +62,38 @@ protected Set doGetActionTargets(Problem problem) { private static void collectTargets(RuleDefinition ruleDefinition, HashSet targets) { for (var consequent : ruleDefinition.getConsequents()) { for (var action : consequent.getActions()) { - if (action instanceof AssertionAction assertionAction) { - var target = assertionAction.getRelation(); - if (target != null) { - targets.add(target); - } + switch (action) { + case AssertionAction assertionAction -> collectTarget(assertionAction.getRelation(), targets); + case TheoryAction theoryAction -> collectTargetFunctions(theoryAction.getTerm(), targets); + case null, default -> throw new IllegalArgumentException("Unknown action: " + action); } } } } + + private static void collectTargetFunctions(Expr expr, HashSet targets) { + if (expr instanceof Atom atom) { + collectTargetFunction(atom, targets); + } + var iterator = expr.eAllContents(); + while (iterator.hasNext()) { + var child = iterator.next(); + if (child instanceof Atom atom) { + collectTargetFunction(atom, targets); + } + if (!(child instanceof Expr)) { + iterator.prune(); + } + } + } + + private static void collectTargetFunction(Atom atom, HashSet targets) { + collectTarget(atom.getRelation(), targets); + } + + private static void collectTarget(Relation target, HashSet targets) { + if (target != null) { + targets.add(target); + } + } } diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java index ac19c7e49..29e3ffd7f 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java +++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java @@ -24,10 +24,7 @@ import tools.refinery.language.model.problem.*; import tools.refinery.language.naming.NamingUtil; import tools.refinery.language.scoping.imports.ImportAdapterProvider; -import tools.refinery.language.typesystem.FixedType; -import tools.refinery.language.typesystem.InvalidType; -import tools.refinery.language.typesystem.ProblemTypeAnalyzer; -import tools.refinery.language.typesystem.SignatureProvider; +import tools.refinery.language.typesystem.*; import tools.refinery.language.utils.BuiltinAnnotationContext; import tools.refinery.language.utils.ParameterBinding; import tools.refinery.language.utils.ProblemUtil; @@ -165,8 +162,8 @@ public void checkEmptyName(NamedElement namedElement) { boolean isEmpty = "".equals(name); if (isNull || isEmpty) { var message = "A name must be specified for the element."; - error(message, namedElement, ProblemPackage.Literals.NAMED_ELEMENT__NAME, INSIGNIFICANT_INDEX, - INVALID_NAME_ISSUE); + error(message, namedElement, ProblemPackage.Literals.NAMED_ELEMENT__NAME, INSIGNIFICANT_INDEX, + INVALID_NAME_ISSUE); } } @@ -239,6 +236,7 @@ public void checkUniqueDeclarations(Problem problem) { var nodes = new ArrayList(); var aggregators = new ArrayList(); var annotationDeclarations = new ArrayList(); + var theoryDeclarations = new ArrayList(); for (var statement : problem.getStatements()) { switch (statement) { case Relation relation -> relations.add(relation); @@ -247,6 +245,7 @@ public void checkUniqueDeclarations(Problem problem) { case NodeDeclaration nodeDeclaration -> nodes.addAll(nodeDeclaration.getNodes()); case AggregatorDeclaration aggregatorDeclaration -> aggregators.add(aggregatorDeclaration); case AnnotationDeclaration annotationDeclaration -> annotationDeclarations.add(annotationDeclaration); + case TheoryDeclaration theoryDeclaration -> theoryDeclarations.add(theoryDeclaration); default -> { // Nothing to check. } @@ -256,6 +255,7 @@ public void checkUniqueDeclarations(Problem problem) { checkUniqueSimpleNames(nodes); checkUniqueSimpleNames(aggregators); checkUniqueSimpleNames(annotationDeclarations); + checkUniqueSimpleNames(theoryDeclarations); } @Check @@ -787,8 +787,12 @@ public void checkRuleParameters(RuleDefinition ruleDefinition) { private static void countRuleParameterUsages(Consequent consequent, Map useCounts) { var usedParameters = new HashSet(); for (var action : consequent.getActions()) { - if (action instanceof AssertionAction assertionAction) { - collectUsedParameters(assertionAction, usedParameters); + switch (action) { + case AssertionAction assertionAction -> collectUsedParameters(assertionAction, usedParameters); + case TheoryAction theoryAction -> collectUsedParameters(theoryAction, usedParameters); + default -> { + // No parameters to collect. + } } } for (var usedParameter : usedParameters) { @@ -804,31 +808,61 @@ private static void collectUsedParameters(AssertionAction assertionAction, HashS usedParameters.add(usedParameter); } } - var value = assertionAction.getValue(); - if (value instanceof VariableOrNodeExpr variableOrNodeExpr && - variableOrNodeExpr.getVariableOrNode() instanceof Parameter usedParameter && - !usedParameter.eIsProxy()) { - usedParameters.add(usedParameter); + collectUsedParameters(assertionAction.getValue(), usedParameters); + } + + private static void collectUsedParameters(TheoryAction theoryAction, HashSet usedParameters) { + collectUsedParameters(theoryAction.getTerm(), usedParameters); + } + + private static void collectUsedParameters(Expr expr, HashSet usedParameters) { + if (expr == null) { + return; + } + if (expr instanceof VariableOrNodeExpr variableOrNodeExpr) { + collectUsedParameters(variableOrNodeExpr, usedParameters); + return; } - var iterator = value.eAllContents(); + var iterator = expr.eAllContents(); while (iterator.hasNext()) { - var expr = iterator.next(); - if (expr instanceof VariableOrNodeExpr variableOrNodeExpr && - variableOrNodeExpr.getVariableOrNode() instanceof Parameter usedParameter && - !usedParameter.eIsProxy()) { - usedParameters.add(usedParameter); + var childExpr = iterator.next(); + if (childExpr instanceof VariableOrNodeExpr variableOrNodeExpr) { + collectUsedParameters(variableOrNodeExpr, usedParameters); + iterator.prune(); } } } + private static void collectUsedParameters(VariableOrNodeExpr variableOrNodeExpr, + HashSet usedParameters) { + if (variableOrNodeExpr.getVariableOrNode() instanceof Parameter usedParameter && !usedParameter.eIsProxy()) { + usedParameters.add(usedParameter); + } + } + @Check - public void checkAssertionActions(AssertionAction assertionAction) { + public void checkAssertionAction(AssertionAction assertionAction) { + var variables = getAllowedVariables(assertionAction); + checkOnlyAllowedVariables(assertionAction.getValue(), variables); + } + + private static HashSet getAllowedVariables(EObject eObject) { + var parametricDefinition = EcoreUtil2.getContainerOfType(eObject, ParametricDefinition.class); var variables = new HashSet(); - var ruleDeclaration = EcoreUtil2.getContainerOfType(assertionAction, ParametricDefinition.class); - if (ruleDeclaration != null) { - variables.addAll(ruleDeclaration.getParameters()); + if (parametricDefinition != null) { + variables.addAll(parametricDefinition.getParameters()); + } + return variables; + } + + @Check + public void checkTheoryAction(TheoryAction theoryAction) { + var variables = getAllowedVariables(theoryAction); + checkOnlyAllowedVariables(theoryAction.getTerm(), variables); + if (!ProblemUtil.supportsTheoryActions(theoryAction)) { + acceptError("Theory actions may only appear in propagation or concretization rules.", theoryAction, null, + 0, INVALID_RULE_ISSUE); } - checkOnlyAllowedVariables(assertionAction.getValue(), variables); } @Check @@ -838,11 +872,7 @@ public void checkAssertion(Assertion assertion) { @Check public void checkCase(Case match) { - var variables = new HashSet(); - var functionDeclaration = EcoreUtil2.getContainerOfType(match, ParametricDefinition.class); - if (functionDeclaration != null) { - variables.addAll(functionDeclaration.getParameters()); - } + var variables = getAllowedVariables(match); var value = match.getValue(); var condition = match.getCondition(); if (value == null) { @@ -999,12 +1029,22 @@ public void checkTypeScope(TypeScope typeScope) { return; } if (ProblemUtil.isShadow(type)) { - var message = "Shadow relations '%s' is not allowed in type scopes.".formatted(type.getName()); + var message = "Shadow relation '%s' is not allowed in type scopes.".formatted(type.getName()); acceptError(message, typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 0, SHADOW_RELATION_ISSUE); } } + @Check + public void checkDatatype(DatatypeDeclaration datatypeDeclaration) { + var dataExprType = signatureProvider.getDataType(datatypeDeclaration); + var termInterpreter = importAdapterProvider.getTermInterpreter(datatypeDeclaration); + if (termInterpreter.getDomain(dataExprType).isEmpty()) { + var message = "Datatype '%s' has no associated abstract domain.".formatted(datatypeDeclaration.getName()); + acceptError(message, datatypeDeclaration, ProblemPackage.Literals.NAMED_ELEMENT__NAME, 0, TYPE_ERROR); + } + } + private void checkArity(EObject eObject, EReference reference, int expectedArity) { var value = eObject.eGet(reference); if (!(value instanceof Relation relation) || relation.eIsProxy()) { diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/realinterval/RoundingMode.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/realinterval/RoundingMode.java index cb6b64d47..87b52014d 100644 --- a/subprojects/logic/src/main/java/tools/refinery/logic/term/realinterval/RoundingMode.java +++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/realinterval/RoundingMode.java @@ -41,7 +41,8 @@ public RealBound infinity() { } }; - private static final int PRECISION = 16; + public static final int PRECISION = 16; + private static final MathContext CEILING_CONTEXT = new MathContext(PRECISION, java.math.RoundingMode.CEILING); private static final MathContext FLOOR_CONTEXT = new MathContext(PRECISION, java.math.RoundingMode.FLOOR); diff --git a/subprojects/store-reasoning-smt/build.gradle.kts b/subprojects/store-reasoning-smt/build.gradle.kts index dcaf0ee62..e8a8397cb 100644 --- a/subprojects/store-reasoning-smt/build.gradle.kts +++ b/subprojects/store-reasoning-smt/build.gradle.kts @@ -15,6 +15,9 @@ mavenArtifact { dependencies { api(project(":refinery-store-reasoning")) + implementation(libs.eclipseCollections) implementation(libs.refinery.z3) + runtimeOnly(libs.eclipseCollections.impl) testImplementation(project(":refinery-store-query-interpreter")) + testImplementation(project(":refinery-store-reasoning-scope")) } diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtPropagator.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtPropagator.java index b63ab5612..78e2c552d 100644 --- a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtPropagator.java +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtPropagator.java @@ -1,19 +1,74 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2026 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.smt; -import com.microsoft.z3.Context; +import tools.refinery.logic.dnf.RelationalQuery; +import tools.refinery.logic.term.Term; +import tools.refinery.logic.term.truthvalue.TruthValue; +import tools.refinery.store.dse.propagation.PropagationBuilder; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.model.ModelStoreConfiguration; +import tools.refinery.store.query.ModelQueryBuilder; +import tools.refinery.store.reasoning.ReasoningBuilder; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.smt.internal.BoundSmtPropagator; +import tools.refinery.store.reasoning.smt.internal.PreparedSmtRule; +import tools.refinery.store.reasoning.theory.TheoryRule; import tools.refinery.z3.Z3SolverLoader; -public class SmtPropagator { - public void propagate() { +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import java.util.Set; + +public class SmtPropagator implements ModelStoreConfiguration { + private final List rules = new ArrayList<>(); + private int timeout; + private int rlimit; + + public SmtPropagator rule(RelationalQuery precondition, Term assertedTerm) { + return rule(new TheoryRule(precondition, assertedTerm)); + } + + public SmtPropagator rule(TheoryRule rule) { + rules.add(rule); + return this; + } + + public SmtPropagator rules(TheoryRule... rules) { + return rules(List.of(rules)); + } + + public SmtPropagator rules(Collection rules) { + this.rules.addAll(rules); + return this; + } + + public SmtPropagator timeout(int timeout) { + this.timeout = timeout; + return this; + } + + public SmtPropagator rlimit(int rlimit) { + this.rlimit = rlimit; + return this; + } + + @Override + public void apply(ModelStoreBuilder storeBuilder) { Z3SolverLoader.loadNativeLibraries(); - try (var context = new Context()) { - var solver = context.mkSolver(); - solver.check(); + var preparedRules = rules.stream().map(PreparedSmtRule::of).toList(); + var queryEngineBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class); + for (var preparedRule : preparedRules) { + queryEngineBuilder.queries(preparedRule.partialPrecondition(), preparedRule.candidatePrecondition()); } + storeBuilder.getAdapter(PropagationBuilder.class) + .propagator(model -> new BoundSmtPropagator(this, model, preparedRules, timeout, rlimit)); + // SMT rules rely on `PARTIAL` interpretations for attributes. + storeBuilder.getAdapter(ReasoningBuilder.class) + .requiredInterpretations(Set.of(Concreteness.PARTIAL, Concreteness.CANDIDATE)); } } diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/expr/SmtExprChecker.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/expr/SmtExprChecker.java new file mode 100644 index 000000000..08f0cdf35 --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/expr/SmtExprChecker.java @@ -0,0 +1,60 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt.expr; + +import tools.refinery.logic.AbstractValue; +import tools.refinery.logic.term.BinaryTerm; +import tools.refinery.logic.term.ConstantTerm; +import tools.refinery.logic.term.Term; +import tools.refinery.logic.term.UnaryTerm; +import tools.refinery.logic.term.abstractdomain.*; +import tools.refinery.logic.term.operators.*; +import tools.refinery.store.reasoning.literal.ConcretenessSpecification; +import tools.refinery.store.reasoning.literal.PartialFunctionCallTerm; + +import java.math.BigDecimal; +import java.math.BigInteger; + +public class SmtExprChecker { + // Use raw types to avoid having to check and capture specific sorts that are already validated by the Term data + // structure and types. + public boolean isSupported(Term term) { + return switch (term) { + case ConstantTerm constantTerm -> isSupported(constantTerm); + case PartialFunctionCallTerm partialFunctionCallTerm -> isSupported(partialFunctionCallTerm); + case UnaryTerm unaryTerm -> switch (unaryTerm) { + case NotTerm _, PlusTerm _, MinusTerm _ -> isSupported(unaryTerm.getBody()); + default -> false; + }; + case BinaryTerm binaryTerm -> switch (binaryTerm) { + case AbstractDomainEqTerm _, AbstractDomainNotEqTerm _, + AbstractDomainGreaterEqTerm _, AbstractDomainGreaterTerm _, + AbstractDomainLessEqTerm _, AbstractDomainLessTerm _, + AndTerm _, OrTerm _, XorTerm _, AddTerm _, SubTerm _, MulTerm _, + DivTerm _, PowTerm _ -> + isSupported(binaryTerm.getLeft()) && isSupported(binaryTerm.getRight()); + default -> false; + }; + default -> false; + }; + } + + private boolean isSupported(ConstantTerm term) { + var value = term.getValue(); + if (!(value instanceof AbstractValue abstractValue) || !abstractValue.isConcrete()) { + return false; + } + var concreteValue = abstractValue.getArbitrary(); + return switch (concreteValue) { + case Boolean _, BigInteger _, BigDecimal _, String _ -> true; + case null, default -> false; + }; + } + + private boolean isSupported(PartialFunctionCallTerm partialFunctionCallTerm) { + return partialFunctionCallTerm.getConcreteness() == ConcretenessSpecification.UNSPECIFIED; + } +} diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/expr/TermToExpr.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/expr/TermToExpr.java new file mode 100644 index 000000000..197553614 --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/expr/TermToExpr.java @@ -0,0 +1,107 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt.expr; + +import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; +import org.eclipse.collections.api.map.primitive.ObjectIntMap; +import tools.refinery.logic.AbstractValue; +import tools.refinery.logic.term.*; +import tools.refinery.logic.term.abstractdomain.*; +import tools.refinery.logic.term.operators.*; +import tools.refinery.store.reasoning.literal.ConcretenessSpecification; +import tools.refinery.store.reasoning.literal.PartialFunctionCallTerm; +import tools.refinery.store.reasoning.smt.internal.context.ModelContext; +import tools.refinery.store.tuple.Tuple; + +import java.math.BigDecimal; +import java.math.BigInteger; + +public class TermToExpr { + private static final String UNSUPPORTED_TERM = "Unsupported term: %s"; + private static final String UNSUPPORTED_CONSTANT = "Unsupported constant: %s"; + + private final ModelContext modelContext; + private final Context context; + + public TermToExpr(ModelContext modelContext) { + this.modelContext = modelContext; + context = modelContext.getZ3Context(); + } + + // Use raw types to avoid having to check and capture specific sorts that are already validated by the Term data + // structure and types. + @SuppressWarnings({"rawtypes", "unchecked"}) + public Expr toExpr(Term term, Tuple parameterTuple, ObjectIntMap parameterMap) { + return switch (term) { + case ConstantTerm constantTerm -> toExpr(constantTerm); + case PartialFunctionCallTerm partialFunctionCallTerm -> + toExpr(partialFunctionCallTerm, parameterTuple, parameterMap); + case UnaryTerm unaryTerm -> { + var body = (Expr) toExpr(unaryTerm.getBody(), parameterTuple, parameterMap); + yield switch (unaryTerm) { + case NotTerm _ -> context.mkNot(body); + case PlusTerm _ -> body; + case MinusTerm _ -> context.mkUnaryMinus(body); + default -> throw new IllegalArgumentException(UNSUPPORTED_TERM.formatted(unaryTerm)); + }; + } + case BinaryTerm binaryTerm -> { + var x = (Expr) toExpr(binaryTerm.getLeft(), parameterTuple, parameterMap); + var y = (Expr) toExpr(binaryTerm.getRight(), parameterTuple, parameterMap); + yield switch (binaryTerm) { + case AbstractDomainEqTerm _ -> context.mkEq(x, y); + case AbstractDomainNotEqTerm _ -> context.mkNot(context.mkEq(x, y)); + case AbstractDomainGreaterEqTerm _ -> context.mkGe(x, y); + case AbstractDomainGreaterTerm _ -> context.mkGt(x, y); + case AbstractDomainLessEqTerm _ -> context.mkLe(x, y); + case AbstractDomainLessTerm _ -> context.mkLt(x, y); + case AndTerm _ -> context.mkAnd(x, y); + case OrTerm _ -> context.mkOr(x, y); + case XorTerm _ -> context.mkXor(x, y); + case AddTerm _ -> context.mkAdd(x, y); + case SubTerm _ -> context.mkSub(x, y); + case MulTerm _ -> context.mkMul(x, y); + case DivTerm _ -> context.mkDiv(x, y); + case PowTerm _ -> context.mkPower(x, y); + default -> throw new IllegalArgumentException(UNSUPPORTED_TERM.formatted(binaryTerm)); + }; + } + default -> throw new IllegalArgumentException(UNSUPPORTED_TERM.formatted(term)); + }; + } + + public Expr toExpr(ConstantTerm term) { + var value = term.getValue(); + if (!(value instanceof AbstractValue abstractValue) || !abstractValue.isConcrete()) { + throw new IllegalArgumentException(UNSUPPORTED_CONSTANT.formatted(value)); + } + var concreteValue = abstractValue.getArbitrary(); + return switch (concreteValue) { + case Boolean booleanValue -> context.mkBool(booleanValue); + case BigInteger intValue -> context.mkInt(intValue.toString(10)); + case BigDecimal realValue -> context.mkReal(realValue.toString()); + case String stringValue -> context.mkString(stringValue); + case null, default -> throw new IllegalArgumentException(UNSUPPORTED_CONSTANT.formatted(abstractValue)); + }; + } + + public Expr toExpr(PartialFunctionCallTerm partialFunctionCallTerm, Tuple parameterTuple, + ObjectIntMap parameterMap) { + if (partialFunctionCallTerm.getConcreteness() != ConcretenessSpecification.UNSPECIFIED) { + throw new IllegalArgumentException( + "Partial function call with specified concreteness: " + partialFunctionCallTerm); + } + var arguments = partialFunctionCallTerm.getArguments(); + var argumentsArray = new int[arguments.size()]; + for (int i = 0; i < argumentsArray.length; i++) { + argumentsArray[i] = parameterTuple.get(parameterMap.get(arguments.get(i))); + } + var argumentsTuple = Tuple.of(argumentsArray); + var declaration = modelContext.getVariable(partialFunctionCallTerm.getPartialFunction(), argumentsTuple); + return context.mkConst(declaration); + } +} diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/BoundSmtPropagator.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/BoundSmtPropagator.java new file mode 100644 index 000000000..d488a8c5e --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/BoundSmtPropagator.java @@ -0,0 +1,63 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt.internal; + +import tools.refinery.store.dse.propagation.BoundPropagator; +import tools.refinery.store.dse.propagation.PropagationResult; +import tools.refinery.store.model.Model; +import tools.refinery.store.model.ModelListener; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.smt.SmtPropagator; +import tools.refinery.store.reasoning.smt.internal.context.ModelContext; +import tools.refinery.store.reasoning.smt.internal.solver.RuleBasedSolver; + +import java.util.Collection; + +public class BoundSmtPropagator implements BoundPropagator, ModelListener { + private final SmtPropagator propagator; + private final ModelContext context; + private final RuleBasedSolver propagationSolver; + private final RuleBasedSolver concretizationSolver; + + public BoundSmtPropagator(SmtPropagator propagator, Model model, Collection rules, + int timeout, int rlimit) { + this.propagator = propagator; + context = new ModelContext(model, rules, timeout, rlimit); + propagationSolver = context.createSolver(Concreteness.PARTIAL); + concretizationSolver = context.createSolver(Concreteness.CANDIDATE); + } + + @Override + public PropagationResult propagateOne() { + return propagationSolver.checkSatisfiable(propagator); + } + + @Override + public boolean concretizationRequested() { + return concretizationSolver.isChanged(); + } + + @Override + public PropagationResult concretizeOne() { + return concretizationSolver.concretize(propagator); + } + + @Override + public PropagationResult checkConcretization() { + return concretizationSolver.checkSatisfiable(propagator); + } + + @Override + public void afterRestore() { + propagationSolver.markChanged(); + concretizationSolver.markChanged(); + } + + @Override + public void beforeClose() { + context.close(); + } +} diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/PreparedSmtRule.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/PreparedSmtRule.java new file mode 100644 index 000000000..c4da399f6 --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/PreparedSmtRule.java @@ -0,0 +1,132 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt.internal; + +import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; +import org.eclipse.collections.api.map.primitive.ObjectIntMap; +import tools.refinery.logic.dnf.Dnf; +import tools.refinery.logic.dnf.Query; +import tools.refinery.logic.dnf.RelationalQuery; +import tools.refinery.logic.dnf.SymbolicParameter; +import tools.refinery.logic.literal.CallPolarity; +import tools.refinery.logic.literal.Literal; +import tools.refinery.logic.rewriter.TermRewriter; +import tools.refinery.logic.term.NodeVariable; +import tools.refinery.logic.term.Term; +import tools.refinery.logic.term.bool.BoolTerms; +import tools.refinery.logic.term.truthvalue.TruthValue; +import tools.refinery.logic.term.truthvalue.TruthValueTerms; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.literal.ConcretenessSpecification; +import tools.refinery.store.reasoning.literal.PartialFunctionCallTerm; +import tools.refinery.store.reasoning.representation.AnyPartialFunction; +import tools.refinery.store.reasoning.theory.TheoryRule; +import tools.refinery.store.tuple.Tuple; + +import java.util.ArrayList; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Set; + +import static tools.refinery.logic.literal.Literals.check; +import static tools.refinery.logic.literal.Literals.not; +import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL; +import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMust; +import static tools.refinery.store.reasoning.literal.PartialLiterals.must; +import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; + +public record PreparedSmtRule(RelationalQuery partialPrecondition, RelationalQuery candidatePrecondition, + Term assertedTerm, ObjectIntMap parameterMap, + List influences) { + public static PreparedSmtRule of(TheoryRule rule) { + var precondition = rule.precondition().getDnf(); + var symbolicParameters = precondition.getSymbolicParameters(); + var parameterVariables = symbolicParameters.stream().map(SymbolicParameter::getVariable).toList(); + var helper = Dnf.builder(precondition.name() + "#helper") + .symbolicParameters(symbolicParameters) + .clause( + precondition.call(CallPolarity.POSITIVE, parameterVariables), + check(BoolTerms.not(TruthValueTerms.must(rule.assertedTerm()))) + ) + .build(); + int literalCount = symbolicParameters.size() + 1; + var partialLiterals = new ArrayList(literalCount); + var candidateLiterals = new ArrayList(literalCount); + partialLiterals.add(must(helper.call(CallPolarity.POSITIVE, parameterVariables))); + candidateLiterals.add(candidateMust(helper.call(CallPolarity.POSITIVE, parameterVariables))); + for (var symbolicParameter : symbolicParameters) { + var variable = symbolicParameter.getVariable(); + partialLiterals.add(not(MULTI_VIEW.call(variable))); + candidateLiterals.add(must(EXISTS_SYMBOL.call(variable))); + } + + var concreteness = rule.concretenessSpecification(); + var partialPreconditionBuilder = Query.builder(precondition.name() + "#partial") + .symbolicParameters(symbolicParameters); + if (concreteness != ConcretenessSpecification.CANDIDATE) { + partialPreconditionBuilder.clause(partialLiterals); + } + var partialPrecondition = partialPreconditionBuilder.build(); + var candidatePreconditionBuilder = Query.builder(precondition.name() + "#candidate") + .symbolicParameters(symbolicParameters); + if (concreteness != ConcretenessSpecification.PARTIAL) { + candidatePreconditionBuilder.clause(candidateLiterals); + } + var candidatePrecondition = candidatePreconditionBuilder.build(); + + var assertedTerm = rule.assertedTerm(); + int arity = parameterVariables.size(); + var mutableParameterMap = ObjectIntMaps.mutable.withInitialCapacity(arity); + for (int i = 0; i < arity; i++) { + mutableParameterMap.put(parameterVariables.get(i).asNodeVariable(), i); + } + var parameterMap = mutableParameterMap.toImmutable(); + var collector = new InfluenceCollector(parameterMap); + collector.collectFromTerm(assertedTerm); + return new PreparedSmtRule(partialPrecondition, candidatePrecondition, assertedTerm, parameterMap, + collector.getInfluences()); + } + + public RelationalQuery getQuery(Concreteness concreteness) { + return switch (concreteness) { + case PARTIAL -> partialPrecondition; + case CANDIDATE -> candidatePrecondition; + }; + } + + public record Influence(AnyPartialFunction partialFunction, Tuple parameterIndices) { + } + + private static class InfluenceCollector implements TermRewriter { + private final ObjectIntMap parameterMap; + private final Set influences = new LinkedHashSet<>(); + + public InfluenceCollector(ObjectIntMap parameterMap) { + this.parameterMap = parameterMap; + } + + public List getInfluences() { + return List.copyOf(influences); + } + + public void collectFromTerm(Term term) { + rewriteTerm(term); + } + + @Override + public Term rewriteTerm(Term term) { + if (term instanceof PartialFunctionCallTerm callTerm) { + var partialFunction = callTerm.getPartialFunction(); + var parameterIndexArray = callTerm.getArguments().stream() + .mapToInt(parameterMap::get) + .toArray(); + var parameterIndices = Tuple.of(parameterIndexArray); + influences.add(new Influence(partialFunction, parameterIndices)); + } + return term.rewriteSubTerms(this); + } + } +} diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/InterruptibleWrapper.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/InterruptibleWrapper.java new file mode 100644 index 000000000..d95172c89 --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/InterruptibleWrapper.java @@ -0,0 +1,123 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt.internal.context; + +import com.microsoft.z3.Context; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; +import tools.refinery.store.util.CancellationToken; + +import java.util.concurrent.*; + +public class InterruptibleWrapper { + private static final Logger LOGGER = LoggerFactory.getLogger(InterruptibleWrapper.class); + + private final CancellationToken cancellationToken; + private final Context context; + private final ExecutorService executor; + + private Thread workerThread; + private Future currentFuture; + private boolean terminated; + + public InterruptibleWrapper(CancellationToken cancellationToken, Context context) { + this.cancellationToken = cancellationToken; + this.context = context; + this.executor = Executors.newSingleThreadExecutor(runnable -> { + var thread = new Thread(() -> { + try { + runnable.run(); + } finally { + context.close(); + } + }, "SMT-worker"); + thread.setDaemon(true); + workerThread = thread; + return thread; + }); + } + + public T call(Callable callable) { + if (terminated) { + throw new CancellationException("SMT solver was already interrupted"); + } + if (currentFuture != null) { + throw new IllegalStateException("A task is already pending"); + } + + Future future = executor.submit(callable); + currentFuture = future; + try { + while (true) { + try { + return future.get(100, TimeUnit.MILLISECONDS); + } catch (TimeoutException e) { + try { + cancellationToken.checkCancelled(); + } catch (RuntimeException cancelled) { + shutdown(); + throw cancelled; + } + } catch (InterruptedException e) { + shutdown(); + // Only restore the interrupt flag if we have managed to shut down the `ExecutorService` + // or logged that Z3 got stuck. + Thread.currentThread().interrupt(); + var cancellationException = new CancellationException("Interrupted while waiting for SMT result"); + cancellationException.initCause(e); + throw cancellationException; + } catch (ExecutionException e) { + throw rethrow(e.getCause()); + } + } + } finally { + currentFuture = null; + } + } + + public void shutdown() { + if (terminated) { + return; + } + terminated = true; + + context.interrupt(); + + if (currentFuture != null) { + currentFuture.cancel(true); + } + + executor.shutdown(); + + boolean success; + try { + success = executor.awaitTermination(100, TimeUnit.MILLISECONDS); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + success = false; + LOGGER.warn("Interrupted while waiting for executor termination", e); + } + if (!success) { + executor.shutdownNow(); + // We intentionally leak the thread with the stuck Z3 instance for rapid response, + // but lower its priority to avoid excessive CPU usage + if (workerThread != null) { + workerThread.setPriority(Thread.MIN_PRIORITY); + } + LOGGER.warn("Z3 is still running"); + } + } + + private RuntimeException rethrow(Throwable cause) { + if (cause instanceof RuntimeException runtimeException) { + return runtimeException; + } + if (cause instanceof Error error) { + throw error; + } + return new RuntimeException(cause); + } +} diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/ModelContext.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/ModelContext.java new file mode 100644 index 000000000..19e7d3b84 --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/ModelContext.java @@ -0,0 +1,147 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt.internal.context; + +import com.microsoft.z3.*; +import tools.refinery.logic.AbstractValue; +import tools.refinery.logic.dnf.Query; +import tools.refinery.logic.term.intinterval.IntIntervalDomain; +import tools.refinery.logic.term.realinterval.RealIntervalDomain; +import tools.refinery.logic.term.string.StringDomain; +import tools.refinery.logic.term.truthvalue.TruthValueDomain; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.ModelQueryAdapter; +import tools.refinery.store.query.resultset.ResultSet; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.interpretation.PartialInterpretation; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.representation.AnyPartialFunction; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.reasoning.smt.expr.TermToExpr; +import tools.refinery.store.reasoning.smt.internal.PreparedSmtRule; +import tools.refinery.store.reasoning.smt.internal.solver.RuleBasedSolver; +import tools.refinery.store.tuple.Tuple; + +import java.util.Collection; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.concurrent.Callable; + +public class ModelContext implements AutoCloseable { + private final Model model; + private final ModelQueryAdapter queryEngine; + private ReasoningAdapter reasoningAdapter; + private final List rules; + private final int timeout; + private final int rlimit; + private final Context context; + private final Sort boolSort; + private final Sort intSort; + private final Sort realSort; + private final Sort stringSort; + private final TermToExpr termToExpr; + private final Map>> variableCache = new HashMap<>(); + private final Map>> exprCache = new HashMap<>(); + private final InterruptibleWrapper interruptibleWrapper; + + public ModelContext(Model model, Collection rules, int timeout, int rlimit) { + this.model = model; + queryEngine = model.getAdapter(ModelQueryAdapter.class); + this.rules = List.copyOf(rules); + this.timeout = timeout; + this.rlimit = rlimit; + context = new Context(); + boolSort = context.getBoolSort(); + intSort = context.getIntSort(); + realSort = context.getRealSort(); + stringSort = context.getStringSort(); + termToExpr = new TermToExpr(this); + interruptibleWrapper = new InterruptibleWrapper(model.getCancellationToken(), context); + } + + public Context getZ3Context() { + return context; + } + + public ResultSet getResultSet(Query query) { + return queryEngine.getResultSet(query); + } + + public , C> PartialInterpretation getPartialInterpretation( + Concreteness concreteness, PartialSymbol partialSymbol) { + return getReasoningAdapter().getPartialInterpretation(concreteness, partialSymbol); + } + + public , C> PartialInterpretationRefiner getRefiner( + PartialSymbol partialSymbol) { + return getReasoningAdapter().getRefiner(partialSymbol); + } + + private ReasoningAdapter getReasoningAdapter() { + if (reasoningAdapter == null) { + reasoningAdapter = model.getAdapter(ReasoningAdapter.class); + } + return reasoningAdapter; + } + + public RuleBasedSolver createSolver(Concreteness concreteness) { + var solver = context.mkSolver(); + var params = context.mkParams(); + params.add("model", concreteness == Concreteness.CANDIDATE); + if (timeout > 0) { + params.add("timeout", timeout); + } + if (rlimit > 0) { + params.add("rlimit", rlimit); + } + solver.setParameters(params); + return new RuleBasedSolver(this, concreteness, rules, solver); + } + + public FuncDecl getVariable(AnyPartialFunction partialFunction, Tuple input) { + var cache = variableCache.computeIfAbsent(partialFunction, _ -> new HashMap<>()); + var sort = getSort(partialFunction); + return cache.computeIfAbsent(input, key -> context.mkConstDecl(partialFunction.name() + key, sort)); + } + + private Sort getSort(AnyPartialFunction partialFunction) { + var abstractDomain = partialFunction.abstractDomain(); + if (TruthValueDomain.INSTANCE.equals(abstractDomain)) { + return boolSort; + } + if (IntIntervalDomain.INSTANCE.equals(abstractDomain)) { + return intSort; + } + if (RealIntervalDomain.INSTANCE.equals(abstractDomain)) { + return realSort; + } + if (StringDomain.INSTANCE.equals(abstractDomain)) { + return stringSort; + } + throw new IllegalArgumentException("Unknown abstract domain %s for partial function %s" + .formatted(abstractDomain, partialFunction)); + } + + public Expr getExpr(PreparedSmtRule rule, Tuple input) { + var cache = exprCache.computeIfAbsent(rule, _ -> new HashMap<>()); + // We know that this was translated from `Term`. + @SuppressWarnings("unchecked") + var result = (Expr) cache.computeIfAbsent(input, parameterTuple -> + termToExpr.toExpr(rule.assertedTerm(), parameterTuple, rule.parameterMap())); + return result; + } + + public T callWithInterrupt(Callable callable) { + return interruptibleWrapper.call(callable); + } + + @Override + public void close() { + interruptibleWrapper.shutdown(); + } +} diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/PartialFunctionMonitor.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/PartialFunctionMonitor.java new file mode 100644 index 000000000..8a2afb237 --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/PartialFunctionMonitor.java @@ -0,0 +1,257 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt.internal.solver; + +import com.microsoft.z3.*; +import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; +import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; +import org.jetbrains.annotations.NotNull; +import tools.refinery.logic.AbstractValue; +import tools.refinery.logic.term.intinterval.IntBound; +import tools.refinery.logic.term.intinterval.IntInterval; +import tools.refinery.logic.term.intinterval.IntIntervalDomain; +import tools.refinery.logic.term.realinterval.RealBound; +import tools.refinery.logic.term.realinterval.RealInterval; +import tools.refinery.logic.term.realinterval.RealIntervalDomain; +import tools.refinery.logic.term.realinterval.RoundingMode; +import tools.refinery.logic.term.string.StringDomain; +import tools.refinery.logic.term.string.StringValue; +import tools.refinery.logic.term.truthvalue.TruthValue; +import tools.refinery.logic.term.truthvalue.TruthValueDomain; +import tools.refinery.store.dse.propagation.PropagationRejectedResult; +import tools.refinery.store.dse.propagation.PropagationResult; +import tools.refinery.store.query.resultset.ResultSetListener; +import tools.refinery.store.reasoning.interpretation.PartialInterpretation; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.representation.PartialFunction; +import tools.refinery.store.tuple.Tuple; + +import java.math.BigDecimal; + +// Z3 assertions create unchecked generic arrays. +// Moreover, we need to convert `FuncDecl` to the specific Z3 sort for assertions. +@SuppressWarnings("unchecked") +class PartialFunctionMonitor, C> implements ResultSetListener { + private final RuleBasedSolver ruleBasedSolver; + private final PartialFunction partialFunction; + private final PartialInterpretation partialInterpretation; + private final PartialInterpretationRefiner refiner; + private final MutableObjectIntMap refCounts; + + public PartialFunctionMonitor(RuleBasedSolver ruleBasedSolver, PartialFunction partialFunction) { + this.ruleBasedSolver = ruleBasedSolver; + this.partialFunction = partialFunction; + var context = ruleBasedSolver.getContext(); + this.partialInterpretation = context.getPartialInterpretation(ruleBasedSolver.getConcreteness(), + partialFunction); + partialInterpretation.addListener(this); + this.refiner = context.getRefiner(partialFunction); + this.refCounts = ObjectIntMaps.mutable.empty(); + } + + @Override + public void put(Tuple key, A fromValue, A toValue) { + if (refCounts.containsKey(key)) { + ruleBasedSolver.markChanged(); + } + } + + public void addRef(Tuple key) { + int newValue = refCounts.addToValue(key, 1); + if (newValue == 1) { + ruleBasedSolver.markChanged(); + } + } + + public void removeRef(Tuple key) { + int newValue = refCounts.addToValue(key, -1); + if (newValue < 0) { + throw new IllegalStateException("Invalid reference count for variable %s%s" + .formatted(partialFunction.name(), key)); + } + if (newValue == 0) { + refCounts.remove(key); + } + } + + public void addAssertions(Solver solver) { + var context = ruleBasedSolver.getContext(); + var z3Context = context.getZ3Context(); + for (var entry : refCounts.keyValuesView()) { + var tuple = entry.getOne(); + var variable = context.getVariable(partialFunction, tuple); + var value = partialInterpretation.get(tuple); + addAssertion(z3Context, solver, variable, value); + } + } + + private void addAssertion(Context context, Solver solver, FuncDecl variable, A value) { + switch (value) { + case TruthValue truthValue -> addAssertion(context, solver, (FuncDecl) variable, truthValue); + case IntInterval intValue -> addAssertion(context, solver, (FuncDecl) variable, intValue); + case RealInterval realValue -> addAssertion(context, solver, (FuncDecl) variable, realValue); + case StringValue stringValue -> addAssertion(context, solver, (FuncDecl) variable, stringValue); + default -> throw new IllegalArgumentException("Unknown value %s for partial function %s".formatted( + value, partialFunction)); + } + } + + private void addAssertion(Context context, Solver solver, FuncDecl variable, TruthValue value) { + switch (value) { + case UNKNOWN -> { + // Nothing to assert. + } + case TRUE -> solver.add(context.mkConst(variable)); + case FALSE -> solver.add(context.mkNot(context.mkConst(variable))); + case ERROR -> solver.add(context.mkFalse()); + } + } + + private void addAssertion(Context context, Solver solver, FuncDecl variable, IntInterval intValue) { + if (intValue.isError()) { + solver.add(context.mkFalse()); + return; + } + if (intValue.isConcrete()) { + var concreteValue = intValue.getConcrete(); + if (concreteValue == null) { + throw new IllegalStateException("Concrete value cannot be null for concrete int interval"); + } + solver.add(context.mkEq(context.mkConst(variable), context.mkInt(concreteValue.toString(10)))); + return; + } + if (intValue.lowerBound() instanceof IntBound.Finite(var lowerBound)) { + solver.add(context.mkGe(context.mkConst(variable), context.mkInt(lowerBound.toString(10)))); + } + if (intValue.upperBound() instanceof IntBound.Finite(var upperBound)) { + solver.add(context.mkLe(context.mkConst(variable), context.mkInt(upperBound.toString(10)))); + } + } + + private void addAssertion(Context context, Solver solver, FuncDecl variable, RealInterval realValue) { + if (realValue.isError()) { + solver.add(context.mkFalse()); + return; + } + if (realValue.isConcrete()) { + var concreteValue = realValue.getConcrete(); + if (concreteValue == null) { + throw new IllegalStateException("Concrete value cannot be null for concrete real interval"); + } + solver.add(context.mkEq(context.mkConst(variable), context.mkReal(concreteValue.toString()))); + return; + } + if (realValue.lowerBound() instanceof RealBound.Finite(var lowerBound)) { + solver.add(context.mkGe(context.mkConst(variable), context.mkReal(lowerBound.toString()))); + } + if (realValue.upperBound() instanceof RealBound.Finite(var upperBound)) { + solver.add(context.mkLe(context.mkConst(variable), context.mkReal(upperBound.toString()))); + } + } + + private void addAssertion(Context context, Solver solver, FuncDecl variable, StringValue stringValue) { + switch (stringValue) { + case StringValue.Unknown _ -> { + // Nothing to assert. + } + case StringValue.Concrete(var concreteValue) -> solver.add(context.mkEq(context.mkConst(variable), + context.mkString(concreteValue))); + case StringValue.Error _ -> solver.add(context.mkFalse()); + } + } + + public boolean isTracking() { + return refCounts.notEmpty(); + } + + public PropagationResult refineWithModel(Model model, Object reason) { + boolean changed = false; + var context = ruleBasedSolver.getContext(); + for (var entry : refCounts.keyValuesView()) { + var tuple = entry.getOne(); + var variable = context.getVariable(partialFunction, tuple); + var z3Value = model.getConstInterp(variable); + if (z3Value == null) { + // Any value is valid. + continue; + } + var value = getValue(z3Value, tuple); + var oldValue = partialInterpretation.get(tuple); + if (!oldValue.equals(value)) { + changed = true; + if (!refiner.merge(tuple, value)) { + return new PropagationRejectedResult(reason, "Failed to merge"); + } + } + } + return changed ? PropagationResult.PROPAGATED : PropagationResult.UNCHANGED; + } + + private @NotNull A getValue(Expr z3Value, Tuple tuple) { + var abstractDomain = partialFunction.abstractDomain(); + A value = null; + if (TruthValueDomain.INSTANCE.equals(abstractDomain)) { + value = (A) getTruthValue((Expr) z3Value); + } else if (IntIntervalDomain.INSTANCE.equals(abstractDomain)) { + value = (A) getIntValue((Expr) z3Value); + } else if (RealIntervalDomain.INSTANCE.equals(abstractDomain)) { + value = (A) getRealValue((Expr) z3Value); + } else if (StringDomain.INSTANCE.equals(abstractDomain)) { + value = (A) getStringValue((Expr) z3Value); + } + if (value == null) { + throw new IllegalStateException("Unknown value %s in SMT model for %s%s".formatted( + z3Value, partialFunction.name(), tuple)); + } + return value; + } + + public TruthValue getTruthValue(Expr value) { + if (value.isTrue()) { + return TruthValue.TRUE; + } + if (value.isFalse()) { + return TruthValue.FALSE; + } + return TruthValue.UNKNOWN; + } + + public IntInterval getIntValue(Expr value) { + if (value instanceof IntNum intNum) { + var concreteValue = intNum.getBigInteger(); + return IntInterval.of(concreteValue); + } + return null; + } + + public RealInterval getRealValue(Expr value) { + if (value instanceof RatNum ratNum) { + var numerator = new BigDecimal(ratNum.getBigIntNumerator()); + var denominator = new BigDecimal(ratNum.getBigIntDenominator()); + var lowerBound = numerator.divide(denominator, RoundingMode.FLOOR.context()); + var upperBound = numerator.divide(denominator, RoundingMode.CEIL.context()); + return RealInterval.of(lowerBound, upperBound); + } + if (value instanceof AlgebraicNum algebraicNum) { + var precision = RoundingMode.PRECISION + 1; + var lowerBoundRat = algebraicNum.toLower(precision); + var lowerBound = new BigDecimal(lowerBoundRat.getBigIntNumerator()) + .divide(new BigDecimal(lowerBoundRat.getBigIntDenominator()), RoundingMode.FLOOR.context()); + var upperBoundRat = algebraicNum.toUpper(precision); + var upperBound = new BigDecimal(upperBoundRat.getBigIntNumerator()) + .divide(new BigDecimal(upperBoundRat.getBigIntDenominator()), RoundingMode.CEIL.context()); + return RealInterval.of(lowerBound, upperBound); + } + return null; + } + + public StringValue getStringValue(Expr value) { + if (value.isString()) { + return StringValue.of(value.getString()); + } + return null; + } +} diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/RuleBasedSolver.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/RuleBasedSolver.java new file mode 100644 index 000000000..cb75698ea --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/RuleBasedSolver.java @@ -0,0 +1,139 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt.internal.solver; + +import com.microsoft.z3.Solver; +import com.microsoft.z3.Status; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; +import tools.refinery.store.dse.propagation.PropagationRejectedResult; +import tools.refinery.store.dse.propagation.PropagationResult; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.representation.AnyPartialFunction; +import tools.refinery.store.reasoning.smt.internal.PreparedSmtRule; +import tools.refinery.store.reasoning.smt.internal.context.ModelContext; +import tools.refinery.store.tuple.Tuple; + +import java.util.List; + +public class RuleBasedSolver { + private static final Logger LOGGER = LoggerFactory.getLogger(RuleBasedSolver.class); + + public static final String REJECTION_UNSAT = "SMT problem is not satisfiable"; + public static final String REJECTION_UNKNOWN = "SMT solver failed to return model"; + public static final String REJECTION_NO_MODEL = REJECTION_UNKNOWN + " unexpectedly"; + + private final ModelContext context; + private final Concreteness concreteness; + private final Solver solver; + private final VariableMonitor variableMonitor; + private final List ruleMonitors; + private boolean started; + private boolean changed = true; + private PropagationResult cachedResult; + + public RuleBasedSolver(ModelContext context, Concreteness concreteness, List rules, + Solver solver) { + this.context = context; + this.concreteness = concreteness; + this.solver = solver; + solver.interrupt(); + variableMonitor = new VariableMonitor(this); + ruleMonitors = rules.stream() + .map(rule -> new RuleMonitor(this, rule)) + .toList(); + } + + public ModelContext getContext() { + return context; + } + + public Concreteness getConcreteness() { + return concreteness; + } + + public boolean isChanged() { + return changed; + } + + public void markChanged() { + changed = true; + } + + private void markUnchanged() { + changed = false; + } + + private boolean canReuseResult() { + return !isChanged() && cachedResult != null && cachedResult != PropagationResult.PROPAGATED; + } + + public void changeRef(AnyPartialFunction partialFunction, Tuple tuple, boolean add) { + variableMonitor.changeRef(partialFunction, tuple, add); + } + + private Status doCheckSatisfiable() { + startIfNeeded(); + solver.reset(); + variableMonitor.addAssertions(solver); + for (var ruleMonitor : ruleMonitors) { + ruleMonitor.addAssertions(solver); + } + return context.callWithInterrupt(solver::check); + } + + private void startIfNeeded() { + if (started) { + return; + } + for (var rule : ruleMonitors) { + rule.start(); + } + started = true; + } + + public PropagationResult checkSatisfiable(Object reason) { + if (canReuseResult()) { + return cachedResult; + } + var status = doCheckSatisfiable(); + if (LOGGER.isTraceEnabled()) { + LOGGER.trace("checkSatisfiable {}", solver.getStatistics()); + } + cachedResult = switch (status) { + case SATISFIABLE, UNKNOWN -> PropagationResult.UNCHANGED; + case UNSATISFIABLE -> new PropagationRejectedResult(reason, REJECTION_UNSAT); + }; + markUnchanged(); + return cachedResult; + } + + public PropagationResult concretize(Object reason) { + if (canReuseResult()) { + return cachedResult; + } + var status = doCheckSatisfiable(); + if (LOGGER.isTraceEnabled()) { + LOGGER.trace("concretize {}", solver.getStatistics()); + } + cachedResult = switch (status) { + case SATISFIABLE -> { + if (!variableMonitor.isTracking()) { + yield PropagationResult.UNCHANGED; + } + var model = context.callWithInterrupt(solver::getModel); + if (model == null) { + yield new PropagationRejectedResult(reason, REJECTION_NO_MODEL, true); + } + yield variableMonitor.refineWithModel(model, reason); + } + case UNKNOWN -> new PropagationRejectedResult(reason, REJECTION_UNKNOWN); + case UNSATISFIABLE -> new PropagationRejectedResult(reason, REJECTION_UNSAT); + }; + markUnchanged(); + return cachedResult; + } +} diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/RuleMonitor.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/RuleMonitor.java new file mode 100644 index 000000000..0a59cc20f --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/RuleMonitor.java @@ -0,0 +1,64 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt.internal.solver; + +import com.microsoft.z3.Solver; +import tools.refinery.store.query.resultset.ResultSet; +import tools.refinery.store.query.resultset.ResultSetListener; +import tools.refinery.store.reasoning.smt.internal.PreparedSmtRule; +import tools.refinery.store.tuple.Tuple; + +public class RuleMonitor implements ResultSetListener { + private final RuleBasedSolver solver; + private final PreparedSmtRule rule; + private final ResultSet resultSet; + + public RuleMonitor(RuleBasedSolver solver, PreparedSmtRule rule) { + this.solver = solver; + this.rule = rule; + this.resultSet = solver.getContext().getResultSet(rule.getQuery(solver.getConcreteness())); + } + + public void start() { + var cursor = resultSet.getAll(); + while (cursor.move()) { + changeRefs(cursor.getKey(), true); + } + resultSet.addListener(this); + } + + // Z3 assertions create unchecked generic arrays. + @SuppressWarnings("unchecked") + public void addAssertions(Solver z3solver) { + var context = solver.getContext(); + var cursor = resultSet.getAll(); + while (cursor.move()) { + var key = cursor.getKey(); + z3solver.add(context.getExpr(rule, key)); + } + } + + @Override + public void put(Tuple key, Boolean fromValue, Boolean toValue) { + if (fromValue != toValue) { + changeRefs(key, toValue); + } + } + + private void changeRefs(Tuple key, boolean add) { + solver.markChanged(); + for (var influence : rule.influences()) { + var indexTuple = influence.parameterIndices(); + int arity = indexTuple.getSize(); + var nodeArray = new int[arity]; + for (int i = 0; i < arity; i++) { + nodeArray[i] = key.get(indexTuple.get(i)); + } + var nodeTuple = Tuple.of(nodeArray); + solver.changeRef(influence.partialFunction(), nodeTuple, add); + } + } +} diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/VariableMonitor.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/VariableMonitor.java new file mode 100644 index 000000000..248dd5159 --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/VariableMonitor.java @@ -0,0 +1,68 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt.internal.solver; + +import com.microsoft.z3.Model; +import com.microsoft.z3.Solver; +import tools.refinery.store.dse.propagation.PropagationResult; +import tools.refinery.store.reasoning.representation.AnyPartialFunction; +import tools.refinery.store.reasoning.representation.PartialFunction; +import tools.refinery.store.tuple.Tuple; + +import java.util.HashMap; +import java.util.Map; + +class VariableMonitor { + private final RuleBasedSolver ruleBasedSolver; + private final Map> monitorMap = new HashMap<>(); + + public VariableMonitor(RuleBasedSolver ruleBasedSolver) { + this.ruleBasedSolver = ruleBasedSolver; + } + + public void changeRef(AnyPartialFunction partialFunction, Tuple tuple, boolean add) { + var monitor = getMonitor(partialFunction); + if (add) { + monitor.addRef(tuple); + return; + } + monitor.removeRef(tuple); + } + + private PartialFunctionMonitor getMonitor(AnyPartialFunction partialFunction) { + var monitor = monitorMap.get(partialFunction); + if (monitor == null) { + monitor = new PartialFunctionMonitor<>(ruleBasedSolver, (PartialFunction) partialFunction); + monitorMap.put(partialFunction, monitor); + } + return monitor; + } + + public void addAssertions(Solver solver) { + for (var entry : monitorMap.entrySet()) { + entry.getValue().addAssertions(solver); + } + } + public boolean isTracking() { + for (var monitor : monitorMap.values()) { + if (monitor.isTracking()) { + return true; + } + } + return false; + } + + public PropagationResult refineWithModel(Model model, Object reason) { + var result = PropagationResult.UNCHANGED; + for (var monitor : monitorMap.values()) { + result = result.andThen(monitor.refineWithModel(model, reason)); + if (result.isRejected()) { + break; + } + } + return result; + } +} diff --git a/subprojects/store-reasoning-smt/src/test/java/tools/refinery/store/reasoning/smt/SmtReasoningTest.java b/subprojects/store-reasoning-smt/src/test/java/tools/refinery/store/reasoning/smt/SmtReasoningTest.java new file mode 100644 index 000000000..b9b9f9fd4 --- /dev/null +++ b/subprojects/store-reasoning-smt/src/test/java/tools/refinery/store/reasoning/smt/SmtReasoningTest.java @@ -0,0 +1,188 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt; + +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.Arguments; +import org.junit.jupiter.params.provider.MethodSource; +import tools.refinery.logic.dnf.Query; +import tools.refinery.logic.term.Variable; +import tools.refinery.logic.term.cardinalityinterval.CardinalityInterval; +import tools.refinery.logic.term.cardinalityinterval.CardinalityIntervals; +import tools.refinery.logic.term.intinterval.IntBound; +import tools.refinery.logic.term.intinterval.IntInterval; +import tools.refinery.logic.term.intinterval.IntIntervalDomain; +import tools.refinery.logic.term.truthvalue.TruthValue; +import tools.refinery.store.dse.propagation.PropagationAdapter; +import tools.refinery.store.dse.strategy.BestFirstStoreManager; +import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.query.interpreter.QueryInterpreterAdapter; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.ReasoningStoreAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.representation.PartialFunction; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.reasoning.scope.ScopePropagator; +import tools.refinery.store.reasoning.seed.ModelSeed; +import tools.refinery.store.reasoning.translator.attribute.AttributeInfo; +import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; +import tools.refinery.store.reasoning.translator.metamodel.Metamodel; +import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator; +import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; +import tools.refinery.store.reasoning.translator.predicate.PredicateTranslator; +import tools.refinery.store.statecoding.StateCoderAdapter; +import tools.refinery.store.statecoding.neighborhood.NeighborhoodCalculator; +import tools.refinery.store.tuple.Tuple; + +import java.math.BigInteger; +import java.util.List; +import java.util.Set; +import java.util.stream.Stream; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.*; +import static tools.refinery.logic.literal.Literals.not; +import static tools.refinery.logic.term.intinterval.IntIntervalTerms.*; +import static tools.refinery.store.reasoning.literal.PartialLiterals.partialCheck; + +class SmtReasoningTest { + private static final CardinalityInterval PERSON_SCOPE = CardinalityIntervals.exactly(5); + private static final IntInterval DEFAULT_AGE = IntInterval.of(0, IntBound.Infinite.POSITIVE_INFINITY); + + private final PartialRelation person = PartialSymbol.of("Person", 1); + private final PartialRelation parents = PartialSymbol.of("parents", 2); + private final PartialRelation invalidParentsMultiplicity = PartialSymbol.of("parents::invalidMultiplicity", 1); + private final PartialFunction age = PartialSymbol.of("age", 1, + IntIntervalDomain.INSTANCE); + private final PartialRelation isolated = PartialSymbol.of("isolated", 1); + private final PartialRelation invalidParentAge = PartialSymbol.of("invalidParentAge", 2); + + @ParameterizedTest(name = "isolated = {0}") + @MethodSource + void modelGenerationTest(CardinalityInterval isolatedScope) { + var store = getModelStore(isolatedScope); + + try (var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(getModelSeed())) { + var bestFirst = new BestFirstStoreManager(store, 1); + bestFirst.startExploration(model.commit(), 0); + var solutions = bestFirst.getSolutionStore().getSolutions(); + assertThat(solutions, hasSize(1)); + model.restore(solutions.getFirst().version()); + + var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); + var isolatedInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, isolated); + var ageCursor = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, age).getAll(); + while (ageCursor.move()) { + var key = ageCursor.getKey(); + var value = ageCursor.getValue(); + var isolated = isolatedInterpretation.get(key); + if (isolated.may()) { + // Isolated nodes should not have a concrete age. + assertThat(value, is(DEFAULT_AGE)); + } else { + // We must concretize each age with an `invalidParentAge` constraint. + assertThat(value, hasProperty("concrete", is(true))); + } + assertThat(value, hasProperty("concrete", is(!isolated.may()))); + } + } + } + + public static Stream modelGenerationTest() { + return Stream.of( + Arguments.of(CardinalityIntervals.NONE), + Arguments.of(CardinalityIntervals.ONE), + Arguments.of(PERSON_SCOPE) + ); + } + + private ModelStore getModelStore(CardinalityInterval isolatedScope) { + var metamodel = Metamodel.builder() + .type(person) + .reference(parents, builder -> builder + .source(person) + .target(person) + .multiplicity(CardinalityIntervals.atMost(2), invalidParentsMultiplicity)) + .attribute(age, new AttributeInfo(person, DEFAULT_AGE)) + .build(); + + var p = Variable.of("p"); + var q = Variable.of("q"); + return ModelStore.builder() + .with(QueryInterpreterAdapter.builder()) + .with(PropagationAdapter.builder()) + .with(StateCoderAdapter.builder() + .stateCodeCalculatorFactory(NeighborhoodCalculator.factory())) + .with(DesignSpaceExplorationAdapter.builder()) + .with(ReasoningAdapter.builder()) + .with(new MultiObjectTranslator()) + .with(new MetamodelTranslator(metamodel)) + .with(new PredicateTranslator( + isolated, + Query.of(isolated.name(), builder -> builder + .parameter(p) + .clause( + person.call(p), + not(parents.call(p, Variable.of())), + not(parents.call(Variable.of(), p)) + )), + List.of(person), + Set.of(), + false, + isolatedScope.equals(CardinalityIntervals.NONE) ? TruthValue.FALSE : TruthValue.UNKNOWN + )) + .with(new PredicateTranslator( + invalidParentAge, + Query.of(invalidParentAge.name(), builder -> builder + .parameters(p, q) + .clause( + parents.call(p, q), + partialCheck(less( + age.call(q), + add(age.call(p), constant(IntInterval.of(18))))) + )), + List.of(person, person), + Set.of(), + false, + TruthValue.FALSE + )) + .with(new ScopePropagator() + .scope(person, PERSON_SCOPE) + .scope(isolated, isolatedScope)) + .with(new SmtPropagator() + .rule( + Query.of("parent", builder -> builder + .parameters(p, q) + .clause(parents.call(p, q))), + greaterEq(age.call(q), add(age.call(p), constant(IntInterval.of(18)))) + )) + .build(); + } + + private ModelSeed getModelSeed() { + int newPerson = 0; + return ModelSeed.builder(1) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .reducedValue(CardinalityIntervals.ONE) + .put(Tuple.of(newPerson), CardinalityIntervals.SET)) + .seed(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, builder -> builder + .reducedValue(TruthValue.FALSE)) + .seed(ContainmentHierarchyTranslator.CONTAINER_SYMBOL, builder -> builder + .reducedValue(TruthValue.FALSE)) + .seed(ContainmentHierarchyTranslator.CONTAINS_SYMBOL, builder -> builder + .reducedValue(TruthValue.FALSE)) + .seed(person, builder -> builder + .reducedValue(TruthValue.FALSE) + .put(Tuple.of(newPerson), TruthValue.TRUE)) + .seed(parents, builder -> builder + .reducedValue(TruthValue.UNKNOWN)) + .seed(age, builder -> builder + .reducedValue(DEFAULT_AGE)) + .build(); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java index 4f51957ba..4ec47db1a 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java @@ -6,15 +6,21 @@ package tools.refinery.store.reasoning.interpretation; import tools.refinery.logic.AbstractValue; +import tools.refinery.store.query.resultset.ResultSetListener; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.tuple.Tuple; + +import java.util.ArrayList; +import java.util.List; public abstract class AbstractPartialInterpretation, C> implements PartialInterpretation { private final ReasoningAdapter adapter; private final PartialSymbol partialSymbol; private final Concreteness concreteness; + private final List> listeners = new ArrayList<>(); protected AbstractPartialInterpretation(ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol partialSymbol) { @@ -37,4 +43,33 @@ public PartialSymbol getPartialSymbol() { public Concreteness getConcreteness() { return concreteness; } + + @Override + public void addListener(ResultSetListener listener) { + if (listeners.isEmpty()) { + startListeningForChanges(); + } + listeners.add(listener); + } + + @Override + public void removeListener(ResultSetListener listener) { + listeners.remove(listener); + if (listeners.isEmpty()) { + stopListeningForChanges(); + } + } + + protected abstract void startListeningForChanges(); + + protected abstract void stopListeningForChanges(); + + protected void notifyChange(Tuple key, A oldValue, A newValue) { + int listenerCount = listeners.size(); + // Use a for loop instead of a for-each loop to avoid {@code Iterator} allocation overhead. + //noinspection ForLoopReplaceableByForEach + for (int i = 0; i < listenerCount; i++) { + listeners.get(i).put(key, oldValue, newValue); + } + } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java index 5a304030e..bba5ad83e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java @@ -8,6 +8,7 @@ import tools.refinery.logic.AbstractValue; import tools.refinery.store.map.Cursor; import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.query.resultset.ResultSetListener; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.representation.PartialSymbol; @@ -23,6 +24,10 @@ public non-sealed interface PartialInterpretation, Cursor getAll(); + void addListener(ResultSetListener listener); + + void removeListener(ResultSetListener listener); + @FunctionalInterface interface Factory, C> { PartialInterpretation create(ReasoningAdapter adapter, Concreteness concreteness, diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedFunctionInterpretationFactory.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedFunctionInterpretationFactory.java index 86b67b19f..4c673bbaa 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedFunctionInterpretationFactory.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedFunctionInterpretationFactory.java @@ -13,6 +13,7 @@ import tools.refinery.store.query.ModelQueryAdapter; import tools.refinery.store.query.ModelQueryBuilder; import tools.refinery.store.query.resultset.ResultSet; +import tools.refinery.store.query.resultset.ResultSetListener; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.representation.PartialSymbol; @@ -56,7 +57,7 @@ public void configure(ModelStoreBuilder storeBuilder, Set required } private static class FunctionInterpretation, C> - extends AbstractPartialInterpretation { + extends AbstractPartialInterpretation implements ResultSetListener { private final ResultSet resultSet; private final A errorValue; @@ -77,5 +78,22 @@ public A get(Tuple key) { public Cursor getAll() { return resultSet.getAll(); } + + @Override + protected void startListeningForChanges() { + resultSet.addListener(this); + } + + @Override + protected void stopListeningForChanges() { + resultSet.removeListener(this); + } + + @Override + public void put(Tuple key, A fromValue, A toValue) { + var fromValueOrError = fromValue == null ? errorValue : fromValue; + var toValueOrError = toValue == null ? errorValue : toValue; + notifyChange(key, fromValueOrError, toValueOrError); + } } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java index 5ada47324..f88a5f32b 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java @@ -5,16 +5,17 @@ */ package tools.refinery.store.reasoning.interpretation; +import tools.refinery.logic.dnf.Query; +import tools.refinery.logic.term.truthvalue.TruthValue; import tools.refinery.store.map.Cursor; import tools.refinery.store.model.ModelStoreBuilder; import tools.refinery.store.query.ModelQueryAdapter; import tools.refinery.store.query.ModelQueryBuilder; -import tools.refinery.logic.dnf.Query; import tools.refinery.store.query.resultset.ResultSet; +import tools.refinery.store.query.resultset.ResultSetListener; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.representation.PartialSymbol; -import tools.refinery.logic.term.truthvalue.TruthValue; import tools.refinery.store.tuple.Tuple; import java.util.Set; @@ -69,7 +70,8 @@ public void configure(ModelStoreBuilder storeBuilder, Set required } } - private static class TwoValuedInterpretation extends AbstractPartialInterpretation { + private static class TwoValuedInterpretation extends AbstractPartialInterpretation + implements ResultSetListener { private final ResultSet resultSet; protected TwoValuedInterpretation( @@ -89,6 +91,21 @@ public Cursor getAll() { return new TwoValuedCursor(resultSet.getAll()); } + @Override + protected void startListeningForChanges() { + resultSet.addListener(this); + } + + @Override + protected void stopListeningForChanges() { + resultSet.removeListener(this); + } + + @Override + public void put(Tuple key, Boolean fromValue, Boolean toValue) { + notifyChange(key, TruthValue.of(fromValue), TruthValue.of(toValue)); + } + private record TwoValuedCursor(Cursor cursor) implements Cursor { @Override public Tuple getKey() { @@ -115,6 +132,8 @@ public boolean move() { private static class FourValuedInterpretation extends AbstractPartialInterpretation { private final ResultSet mayResultSet; private final ResultSet mustResultSet; + private ResultSetListener mayListener; + private ResultSetListener mustListener; public FourValuedInterpretation( ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol partialSymbol, @@ -128,11 +147,7 @@ public FourValuedInterpretation( public TruthValue get(Tuple key) { boolean isMay = mayResultSet.get(key); boolean isMust = mustResultSet.get(key); - if (isMust) { - return isMay ? TruthValue.TRUE : TruthValue.ERROR; - } else { - return isMay ? TruthValue.UNKNOWN : TruthValue.FALSE; - } + return TruthValue.of(isMay, isMust); } @Override @@ -140,6 +155,30 @@ public Cursor getAll() { return new FourValuedCursor(); } + @Override + protected void startListeningForChanges() { + if (mayListener == null) { + mayListener = (key, oldValue, newValue) -> { + boolean mustValue = mustResultSet.get(key); + notifyChange(key, TruthValue.of(oldValue, mustValue), TruthValue.of(newValue, mustValue)); + }; + } + if (mustListener == null) { + mustListener = (key, oldValue, newValue) -> { + boolean mayValue = mayResultSet.get(key); + notifyChange(key, TruthValue.of(mayValue, oldValue), TruthValue.of(mayValue, newValue)); + }; + } + mayResultSet.addListener(mayListener); + mustResultSet.addListener(mustListener); + } + + @Override + protected void stopListeningForChanges() { + mayResultSet.removeListener(mayListener); + mustResultSet.removeListener(mustListener); + } + private final class FourValuedCursor implements Cursor { private final Cursor mayCursor; private Cursor mustCursor; diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/Theory.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/Theory.java new file mode 100644 index 000000000..f315d7e47 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/Theory.java @@ -0,0 +1,16 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.theory; + +import tools.refinery.store.model.ModelStoreBuilder; + +import java.util.Collection; + +public interface Theory { + TheorySupport checkSupport(TheoryRule theoryRule); + + void createPropagator(ModelStoreBuilder storeBuilder, Collection collectedRules); +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheoryRule.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheoryRule.java new file mode 100644 index 000000000..40a3489a7 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheoryRule.java @@ -0,0 +1,22 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.theory; + +import tools.refinery.logic.dnf.RelationalQuery; +import tools.refinery.logic.term.Term; +import tools.refinery.logic.term.truthvalue.TruthValue; +import tools.refinery.store.reasoning.literal.ConcretenessSpecification; + +public record TheoryRule(RelationalQuery precondition, Term assertedTerm, + ConcretenessSpecification concretenessSpecification) { + public TheoryRule(RelationalQuery precondition, Term assertedTerm) { + this(precondition, assertedTerm, ConcretenessSpecification.UNSPECIFIED); + } + + public TheoryRule withConcreteness(ConcretenessSpecification newConcreteness) { + return new TheoryRule(precondition, assertedTerm, newConcreteness); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheorySupport.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheorySupport.java new file mode 100644 index 000000000..9d2dcaa5e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheorySupport.java @@ -0,0 +1,30 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.theory; + +public enum TheorySupport { + ENABLED_BY_DEFAULT, + EXPLICIT_ONLY, + UNSUPPORTED; + + public boolean isEnabledByDefault() { + return this == ENABLED_BY_DEFAULT; + } + + public boolean isSupported() { + return this != UNSUPPORTED; + } + + public TheorySupport meet(TheorySupport other) { + if (this == UNSUPPORTED || other == UNSUPPORTED) { + return UNSUPPORTED; + } + if (this == EXPLICIT_ONLY || other == EXPLICIT_ONLY) { + return EXPLICIT_ONLY; + } + return ENABLED_BY_DEFAULT; + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/MissingInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/MissingInterpretation.java index 115926987..0efa72691 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/MissingInterpretation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/MissingInterpretation.java @@ -30,6 +30,16 @@ public Cursor getAll() { return fail(); } + @Override + protected void startListeningForChanges() { + // No changes to track. + } + + @Override + protected void stopListeningForChanges() { + // No changes to track. + } + private T fail() { throw new UnsupportedOperationException("No interpretation for shadow predicate: " + getPartialSymbol()); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java index 75828086a..e5a782b6d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java @@ -8,6 +8,7 @@ import tools.refinery.logic.AbstractValue; import tools.refinery.store.map.AnyVersionedMap; import tools.refinery.store.map.Cursor; +import tools.refinery.store.query.resultset.ResultSetListener; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.interpretation.AbstractPartialInterpretation; import tools.refinery.store.reasoning.interpretation.PartialInterpretation; @@ -17,7 +18,8 @@ import java.util.Set; -class OppositeInterpretation, C> extends AbstractPartialInterpretation { +class OppositeInterpretation, C> extends AbstractPartialInterpretation + implements ResultSetListener { private final PartialInterpretation opposite; private OppositeInterpretation(ReasoningAdapter adapter, Concreteness concreteness, @@ -43,6 +45,21 @@ public static , C1> Factory of(PartialS }; } + @Override + protected void startListeningForChanges() { + opposite.addListener(this); + } + + @Override + protected void stopListeningForChanges() { + opposite.removeListener(this); + } + + @Override + public void put(Tuple key, A fromValue, A toValue) { + notifyChange(OppositeUtils.flip(key), fromValue, toValue); + } + private record OppositeCursor(Cursor opposite) implements Cursor { @Override public Tuple getKey() { diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/Model.java b/subprojects/store/src/main/java/tools/refinery/store/model/Model.java index 6c0ca86e6..3eb6ef9a1 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/model/Model.java +++ b/subprojects/store/src/main/java/tools/refinery/store/model/Model.java @@ -10,6 +10,7 @@ import tools.refinery.store.map.Versioned; import tools.refinery.store.representation.AnySymbol; import tools.refinery.store.representation.Symbol; +import tools.refinery.store.util.CancellationToken; import java.util.Optional; @@ -38,6 +39,8 @@ default AnyInterpretation getInterpretation(AnySymbol symbol) { void removeListener(ModelListener listener); + CancellationToken getCancellationToken(); + void checkCancelled(); @Override diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelImpl.java b/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelImpl.java index 0b3b70eb8..0fc3ca5ab 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelImpl.java +++ b/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelImpl.java @@ -196,6 +196,11 @@ public void removeListener(ModelListener listener) { listeners.remove(listener); } + @Override + public CancellationToken getCancellationToken() { + return cancellationToken; + } + @Override public void checkCancelled() { cancellationToken.checkCancelled();