From 2c9a45705fbd9d2417422039352a58f2d942ae4b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Tue, 24 Feb 2026 16:39:44 +0100 Subject: [PATCH 01/10] feat(reasoning): basic SMT solver support --- .../impl/FilteredInterpretation.java | 11 + .../logic/term/realinterval/RoundingMode.java | 3 +- .../store-reasoning-smt/build.gradle.kts | 3 + .../store/reasoning/smt/SmtPropagator.java | 49 +++- .../refinery/store/reasoning/smt/SmtRule.java | 13 + .../smt/internal/BoundSmtPropagator.java | 62 +++++ .../smt/internal/PreparedSmtRule.java | 124 +++++++++ .../smt/internal/context/ModelContext.java | 132 +++++++++ .../smt/internal/context/TermToExpr.java | 106 ++++++++ .../solver/PartialFunctionMonitor.java | 257 ++++++++++++++++++ .../smt/internal/solver/RuleBasedSolver.java | 128 +++++++++ .../smt/internal/solver/RuleMonitor.java | 64 +++++ .../smt/internal/solver/VariableMonitor.java | 68 +++++ .../store/reasoning/smt/SmtReasoningTest.java | 188 +++++++++++++ .../AbstractPartialInterpretation.java | 35 +++ .../interpretation/PartialInterpretation.java | 5 + ...eryBasedFunctionInterpretationFactory.java | 20 +- ...eryBasedRelationInterpretationFactory.java | 55 +++- .../translator/MissingInterpretation.java | 10 + .../opposite/OppositeInterpretation.java | 19 +- 20 files changed, 1334 insertions(+), 18 deletions(-) create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/BoundSmtPropagator.java create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/PreparedSmtRule.java create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/ModelContext.java create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/TermToExpr.java create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/PartialFunctionMonitor.java create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/RuleBasedSolver.java create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/RuleMonitor.java create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/VariableMonitor.java create mode 100644 subprojects/store-reasoning-smt/src/test/java/tools/refinery/store/reasoning/smt/SmtReasoningTest.java 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/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..fb65927bd 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,54 @@ /* - * 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.smt.internal.BoundSmtPropagator; +import tools.refinery.store.reasoning.smt.internal.PreparedSmtRule; import tools.refinery.z3.Z3SolverLoader; -public class SmtPropagator { - public void propagate() { +import java.util.ArrayList; +import java.util.List; + +public class SmtPropagator implements ModelStoreConfiguration { + private final List rules = new ArrayList<>(); + + public SmtPropagator rule(RelationalQuery precondition, Term assertedTerm) { + return rule(new SmtRule(precondition, assertedTerm)); + } + + public SmtPropagator rule(SmtRule rule) { + rules.add(rule); + return this; + } + + public SmtPropagator rules(SmtRule... rules) { + return rules(List.of(rules)); + } + + public SmtPropagator rules(List rules) { + this.rules.addAll(rules); + 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)); } } diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java new file mode 100644 index 000000000..40e29dc74 --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java @@ -0,0 +1,13 @@ +/* + * SPDX-FileCopyrightText: 2026 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.smt; + +import tools.refinery.logic.dnf.RelationalQuery; +import tools.refinery.logic.term.Term; +import tools.refinery.logic.term.truthvalue.TruthValue; + +public record SmtRule(RelationalQuery precondition, Term assertedTerm) { +} 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..0527c210c --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/BoundSmtPropagator.java @@ -0,0 +1,62 @@ +/* + * 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) { + this.propagator = propagator; + context = new ModelContext(model, rules); + 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..72f1c645c --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/PreparedSmtRule.java @@ -0,0 +1,124 @@ +/* + * 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.PartialFunctionCallTerm; +import tools.refinery.store.reasoning.representation.AnyPartialFunction; +import tools.refinery.store.reasoning.smt.SmtRule; +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(SmtRule 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 partialPrecondition = Query.builder(precondition.name() + "#partial") + .symbolicParameters(symbolicParameters) + .clause(partialLiterals) + .build(); + var candidatePrecondition = Query.builder(precondition.name() + "#candidate") + .symbolicParameters(symbolicParameters) + .clause(candidateLiterals) + .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/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..a9c03dd5b --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/ModelContext.java @@ -0,0 +1,132 @@ +/* + * 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.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; + +public class ModelContext implements AutoCloseable { + public static final int SOLVER_TIMEOUT = 10000; + + private final Model model; + private final ModelQueryAdapter queryEngine; + private ReasoningAdapter reasoningAdapter; + private final List rules; + 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<>(); + + public ModelContext(Model model, Collection rules) { + this.model = model; + queryEngine = model.getAdapter(ModelQueryAdapter.class); + this.rules = List.copyOf(rules); + context = new Context(); + boolSort = context.getBoolSort(); + intSort = context.getIntSort(); + realSort = context.getRealSort(); + stringSort = context.getStringSort(); + termToExpr = new TermToExpr(this); + } + + 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); + params.add("timeout", SOLVER_TIMEOUT); + 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; + } + + @Override + public void close() { + context.close(); + } +} diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/TermToExpr.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/TermToExpr.java new file mode 100644 index 000000000..1166aca21 --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/TermToExpr.java @@ -0,0 +1,106 @@ +/* + * 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 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.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/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..a47392a2a --- /dev/null +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/solver/RuleBasedSolver.java @@ -0,0 +1,128 @@ +/* + * 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 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 { + 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; + 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 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(); + 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(); + cachedResult = switch (status) { + case SATISFIABLE -> { + if (!variableMonitor.isTracking()) { + yield PropagationResult.UNCHANGED; + } + var model = 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/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() { From 9f269ae9559cb8152520e4b5196aabd9e1053f8e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Wed, 25 Feb 2026 19:42:45 +0100 Subject: [PATCH 02/10] feat(language): theory assertion actions --- .../frontend/src/language/problem.grammar | 6 +- .../src/language/problemLanguageSupport.ts | 2 +- subprojects/language-model/problem.aird | 133 +++++++++++++++--- .../src/main/resources/model/problem.ecore | 4 + .../src/main/resources/model/problem.genmodel | 3 + .../language-semantics/build.gradle.kts | 1 + .../language/semantics/ModelInitializer.java | 21 +++ .../internal/query/RuleCompiler.java | 44 +++++- .../tools/refinery/language/Problem.xtext | 7 +- .../store/reasoning/smt/SmtPropagator.java | 9 +- 10 files changed, 206 insertions(+), 24 deletions(-) diff --git a/subprojects/frontend/src/language/problem.grammar b/subprojects/frontend/src/language/problem.grammar index 5a84008a3..345809d73 100644 --- a/subprojects/frontend/src/language/problem.grammar +++ b/subprojects/frontend/src/language/problem.grammar @@ -173,7 +173,9 @@ Atom { RelationName "+"? ParameterList } Consequent { ("," | Action)+ } -Action { +Action { AssertionAction | TermAction } + +AssertionAction { (NotOp | UnknownOp)? RelationName ParameterList (":" Expr)? @@ -183,6 +185,8 @@ AssertionArgument { NodeName | StarArgument } AssertionActionArgument { VariableName | StarArgument } +TermAction { ckw<"assert"> Expr } + Constant { Real | String | StarMult | LogicValue } LogicValue { diff --git a/subprojects/frontend/src/language/problemLanguageSupport.ts b/subprojects/frontend/src/language/problemLanguageSupport.ts index c03b82174..a2c711398 100644 --- a/subprojects/frontend/src/language/problemLanguageSupport.ts +++ b/subprojects/frontend/src/language/problemLanguageSupport.ts @@ -42,7 +42,7 @@ const parserWithMetadata = parser.configure({ default: t.modifier, 'shadow propagation decision concretization': t.modifier, 'true false unknown error': t.keyword, - 'candidate may must': t.operatorKeyword, + 'candidate may must assert': t.operatorKeyword, is: t.operatorKeyword, NotOp: t.operator, UnknownOp: t.operator, diff --git a/subprojects/language-model/problem.aird b/subprojects/language-model/problem.aird index ec6897291..f400a2bb8 100644 --- a/subprojects/language-model/problem.aird +++ b/subprojects/language-model/problem.aird @@ -19,7 +19,7 @@ - + @@ -6355,7 +6355,7 @@ - + @@ -6368,7 +6368,7 @@ - + @@ -6455,6 +6455,10 @@ + + + + @@ -6463,10 +6467,6 @@ - - - - @@ -6475,7 +6475,25 @@ - + + + + + + + + + + + + + + + + + + + @@ -6558,6 +6576,38 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -6573,7 +6623,7 @@ - + KEEP_LOCATION @@ -6760,6 +6810,15 @@ + + + + + italic + + + + @@ -6776,15 +6835,6 @@ - - - - - italic - - - - @@ -6834,6 +6884,53 @@ + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + + + + italic + + + + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + 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..f27813f9e 100644 --- a/subprojects/language-model/src/main/resources/model/problem.ecore +++ b/subprojects/language-model/src/main/resources/model/problem.ecore @@ -326,4 +326,8 @@ + + + diff --git a/subprojects/language-model/src/main/resources/model/problem.genmodel b/subprojects/language-model/src/main/resources/model/problem.genmodel index 555aaa825..d9462b808 100644 --- a/subprojects/language-model/src/main/resources/model/problem.genmodel +++ b/subprojects/language-model/src/main/resources/model/problem.genmodel @@ -277,5 +277,8 @@ + + + diff --git a/subprojects/language-semantics/build.gradle.kts b/subprojects/language-semantics/build.gradle.kts index 98e5b3666..fe39ada70 100644 --- a/subprojects/language-semantics/build.gradle.kts +++ b/subprojects/language-semantics/build.gradle.kts @@ -19,6 +19,7 @@ dependencies { api(project(":refinery-store-reasoning")) api(libs.eclipseCollections) implementation(project(":refinery-store-reasoning-scope")) + implementation(project(":refinery-store-reasoning-smt")) runtimeOnly(libs.eclipseCollections.impl) testImplementation(project(":refinery-store-dse-visualization")) testImplementation(project(":refinery-store-query-interpreter")) 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..28084cc87 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 @@ -44,6 +44,8 @@ import tools.refinery.store.reasoning.scope.ScopePropagator; import tools.refinery.store.reasoning.seed.ModelSeed; import tools.refinery.store.reasoning.seed.Seed; +import tools.refinery.store.reasoning.smt.SmtPropagator; +import tools.refinery.store.reasoning.smt.SmtRule; import tools.refinery.store.reasoning.translator.ConcretizationSettings; import tools.refinery.store.reasoning.translator.TranslationException; import tools.refinery.store.reasoning.translator.attribute.AttributeInfo; @@ -134,6 +136,8 @@ public class ModelInitializer { private ScopePropagator scopePropagator; + private SmtPropagator smtPropagator; + private int nodeCount; private ModelSeed.Builder modelSeedBuilder; @@ -243,6 +247,12 @@ public void configureStoreBuilder(ModelStoreBuilder storeBuilder) { } collectPredicates(storeBuilder); collectRules(storeBuilder); + if (smtPropagator != null) { + if (storeBuilder.tryGetAdapter(PropagationBuilder.class).isEmpty()) { + throw new TracedException(problem, "SMT rules require a PropagationBuilder"); + } + storeBuilder.with(smtPropagator); + } storeBuilder.tryGetAdapter(StateCoderBuilder.class) .ifPresent(stateCoderBuilder -> stateCoderBuilder.individuals(individuals)); if (!keepShadowPredicates) { @@ -1073,6 +1083,7 @@ private void collectRule(RuleDefinition ruleDefinition, ModelStoreBuilder storeB ConcretenessSpecification.CANDIDATE); rules.addAll(propagationRules); rules.addAll(concretizationRules); + addSmtRules(ruleCompiler.toSmtRules(name, ruleDefinition)); problemTrace.putPropagationRuleDefinition(ruleDefinition, List.copyOf(rules)); storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(propagationBuilder -> { propagationBuilder.rules(propagationRules); @@ -1103,4 +1114,14 @@ private void collectRule(RuleDefinition ruleDefinition, ModelStoreBuilder storeB throw TracedException.addTrace(ruleDefinition, e); } } + + private void addSmtRules(Collection smtRules) { + if (smtRules.isEmpty()) { + return; + } + if (smtPropagator == null) { + smtPropagator = new SmtPropagator(); + } + smtPropagator.rules(smtRules); + } } 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..dc2c18bd9 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 @@ -32,6 +32,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.smt.SmtRule; import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; import java.util.*; @@ -166,8 +167,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 +208,43 @@ 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 Collection toSmtRules(String name, RuleDefinition ruleDefinition) { + var preparedRule = prepareRule(ruleDefinition, false); + var parameterMap = preparedRule.parameterMap(); + var consequents = ruleDefinition.getConsequents(); + if (consequents.isEmpty()) { + return List.of(); + } + var actions = consequents.getFirst().getActions(); + int actionCount = actions.size(); + var rules = new ArrayList(); + 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); + rules.add(new SmtRule(query, term)); + } catch (RuntimeException e) { + throw TracedException.addTrace(action, e); + } + } + return rules; + } + public Rule toRule(String name, RuleDefinition ruleDefinition) { var preparedRule = prepareRule(ruleDefinition, true); var parameters = preparedRule.allParameters(); 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..13334868d 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext @@ -140,7 +140,7 @@ Consequent: actions+=Action ("," actions+=Action)*; Action: - AssertionAction; + AssertionAction | TheoryAction; AssertionAction: relation=[Relation|QualifiedName] @@ -150,6 +150,9 @@ AssertionAction: relation=[Relation|QualifiedName] "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")"; +TheoryAction: + "assert" term=Expr; + Expr: AssignmentExpr; @@ -330,7 +333,7 @@ NonContainmentIdentifier: ID | QUOTED_ID | "as" | "atom" | "multi" | "problem" | "module" | "datatype" | "aggregator" | "primitive" | "decision" | "propagation" | "concretization" | - "shadow"; + "shadow" | "assert"; Integer returns ecore::EBigInteger: INT; 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 fb65927bd..567826039 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 @@ -12,12 +12,16 @@ 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.z3.Z3SolverLoader; 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<>(); @@ -35,7 +39,7 @@ public SmtPropagator rules(SmtRule... rules) { return rules(List.of(rules)); } - public SmtPropagator rules(List rules) { + public SmtPropagator rules(Collection rules) { this.rules.addAll(rules); return this; } @@ -50,5 +54,8 @@ public void apply(ModelStoreBuilder storeBuilder) { } storeBuilder.getAdapter(PropagationBuilder.class) .propagator(model -> new BoundSmtPropagator(this, model, preparedRules)); + // SMT rules rely on `PARTIAL` interpretations for attributes. + storeBuilder.getAdapter(ReasoningBuilder.class) + .requiredInterpretations(Set.of(Concreteness.PARTIAL, Concreteness.CANDIDATE)); } } From e9fd31bd2bd8b853fb5ae1eec2e01bfa3ba82519 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Sat, 28 Feb 2026 19:11:00 +0100 Subject: [PATCH 03/10] fix(language): used variables in theory actions --- .../language/validation/ProblemValidator.java | 49 +++++++++++++------ 1 file changed, 34 insertions(+), 15 deletions(-) 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..9ca9f677e 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 @@ -165,8 +165,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); } } @@ -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,23 +808,38 @@ 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; } - var iterator = value.eAllContents(); + if (expr instanceof VariableOrNodeExpr variableOrNodeExpr) { + collectUsedParameters(variableOrNodeExpr, usedParameters); + return; + } + 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) { var variables = new HashSet(); From 234f00b26250b95d3c4a7b9cf71e6c7d998d5d06 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Thu, 5 Mar 2026 23:17:22 +0100 Subject: [PATCH 04/10] feat(language): theory concretization rules Also validates the appropraite use of theory actions. --- .../ProblemContentProposalProvider.java | 12 ++++--- .../language/semantics/ModelInitializer.java | 3 ++ .../refinery/language/utils/ProblemUtil.java | 16 +++++++++- .../language/validation/ProblemValidator.java | 31 +++++++++++++------ .../refinery/store/reasoning/smt/SmtRule.java | 11 ++++++- .../smt/internal/PreparedSmtRule.java | 27 ++++++++++------ 6 files changed, 73 insertions(+), 27 deletions(-) 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-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java index 28084cc87..b1c0d243c 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 @@ -1092,6 +1092,9 @@ private void collectRule(RuleDefinition ruleDefinition, ModelStoreBuilder storeB } case CONCRETIZATION -> { var rules = ruleCompiler.toPropagationRules(name, ruleDefinition, ConcretenessSpecification.CANDIDATE); + addSmtRules(ruleCompiler.toSmtRules(name, ruleDefinition).stream() + .map(smtRule -> smtRule.withConcreteness(ConcretenessSpecification.CANDIDATE)) + .toList()); problemTrace.putPropagationRuleDefinition(ruleDefinition, rules); storeBuilder.tryGetAdapter(PropagationBuilder.class) .ifPresent(propagationBuilder -> propagationBuilder.concretizationRules(rules)); 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..bbf509617 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 @@ -66,7 +66,21 @@ public static boolean isShadow(EObject eObject) { 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/validation/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java index 9ca9f677e..36f7e2edd 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 @@ -841,13 +841,28 @@ private static void collectUsedParameters(VariableOrNodeExpr variableOrNodeExpr, } @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 @@ -857,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) { diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java index 40e29dc74..16fcab2d3 100644 --- a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java +++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java @@ -8,6 +8,15 @@ 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 SmtRule(RelationalQuery precondition, Term assertedTerm) { +public record SmtRule(RelationalQuery precondition, Term assertedTerm, + ConcretenessSpecification concreteness) { + public SmtRule(RelationalQuery precondition, Term assertedTerm) { + this(precondition, assertedTerm, ConcretenessSpecification.UNSPECIFIED); + } + + public SmtRule withConcreteness(ConcretenessSpecification newConcreteness) { + return new SmtRule(precondition, assertedTerm, newConcreteness); + } } 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 index 72f1c645c..554b3c5a7 100644 --- 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 @@ -11,8 +11,7 @@ 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.literal.*; import tools.refinery.logic.rewriter.TermRewriter; import tools.refinery.logic.term.NodeVariable; import tools.refinery.logic.term.Term; @@ -20,6 +19,7 @@ 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.smt.SmtRule; @@ -61,14 +61,21 @@ public static PreparedSmtRule of(SmtRule rule) { partialLiterals.add(not(MULTI_VIEW.call(variable))); candidateLiterals.add(must(EXISTS_SYMBOL.call(variable))); } - var partialPrecondition = Query.builder(precondition.name() + "#partial") - .symbolicParameters(symbolicParameters) - .clause(partialLiterals) - .build(); - var candidatePrecondition = Query.builder(precondition.name() + "#candidate") - .symbolicParameters(symbolicParameters) - .clause(candidateLiterals) - .build(); + + var concreteness = rule.concreteness(); + 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); From 77a07ecedcd5101694e02d39786ea936657836eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Fri, 6 Mar 2026 15:06:47 +0100 Subject: [PATCH 05/10] fix(language): variables in theory actions --- subprojects/language-model/problem.aird | 179 +++++++++++++----- .../src/main/resources/model/problem.ecore | 5 +- .../state/DerivedVariableComputer.java | 10 +- 3 files changed, 137 insertions(+), 57 deletions(-) diff --git a/subprojects/language-model/problem.aird b/subprojects/language-model/problem.aird index f400a2bb8..c293a38b6 100644 --- a/subprojects/language-model/problem.aird +++ b/subprojects/language-model/problem.aird @@ -19,7 +19,7 @@ - + @@ -6355,20 +6355,16 @@ - + - - - - - + @@ -6455,10 +6451,6 @@ - - - - @@ -6475,16 +6467,20 @@ - + + + + + - + @@ -6493,7 +6489,20 @@ - + + + + + + + + + + + + + + @@ -6592,21 +6601,53 @@ - - - + + + + + + + + + + + + + + + + + + + - - + + - - + + - - - - - + + + + + + + + + + + + + + + + + + + + + @@ -6645,15 +6686,6 @@ - - - - - italic - - - - @@ -6760,7 +6792,7 @@ - + @@ -6799,7 +6831,7 @@ - + KEEP_LOCATION @@ -6810,15 +6842,6 @@ - - - - - italic - - - - @@ -6884,7 +6907,7 @@ - + KEEP_LOCATION @@ -6894,6 +6917,14 @@ + + + + + + + + @@ -6907,7 +6938,7 @@ - + @@ -6922,15 +6953,59 @@ - + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + italic + + + + + + + + + + + + + - - - + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + diff --git a/subprojects/language-model/src/main/resources/model/problem.ecore b/subprojects/language-model/src/main/resources/model/problem.ecore index f27813f9e..973ef9e28 100644 --- a/subprojects/language-model/src/main/resources/model/problem.ecore +++ b/subprojects/language-model/src/main/resources/model/problem.ecore @@ -326,8 +326,7 @@ - - + + 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. + } } } } From 307c526efdc4aa34e573b348a12ef5a458ea34b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Sat, 7 Mar 2026 01:12:51 +0100 Subject: [PATCH 06/10] feat(reasoning): SMT solver timeout --- .../context/InterruptibleWrapper.java | 123 ++++++++++++++++++ .../smt/internal/context/ModelContext.java | 9 +- .../smt/internal/solver/RuleBasedSolver.java | 5 +- .../tools/refinery/store/model/Model.java | 3 + .../store/model/internal/ModelImpl.java | 5 + 5 files changed, 142 insertions(+), 3 deletions(-) create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/InterruptibleWrapper.java 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 index a9c03dd5b..25fa39027 100644 --- 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 @@ -29,6 +29,7 @@ import java.util.HashMap; import java.util.List; import java.util.Map; +import java.util.concurrent.Callable; public class ModelContext implements AutoCloseable { public static final int SOLVER_TIMEOUT = 10000; @@ -45,6 +46,7 @@ public class ModelContext implements AutoCloseable { 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) { this.model = model; @@ -56,6 +58,7 @@ public ModelContext(Model model, Collection rules) { realSort = context.getRealSort(); stringSort = context.getStringSort(); termToExpr = new TermToExpr(this); + interruptibleWrapper = new InterruptibleWrapper(model.getCancellationToken(), context); } public Context getZ3Context() { @@ -125,8 +128,12 @@ public Expr getExpr(PreparedSmtRule rule, Tuple input) { return result; } + public T callWithInterrupt(Callable callable) { + return interruptibleWrapper.call(callable); + } + @Override public void close() { - context.close(); + interruptibleWrapper.shutdown(); } } 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 index a47392a2a..ad3c368b7 100644 --- 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 @@ -36,6 +36,7 @@ public RuleBasedSolver(ModelContext context, Concreteness concreteness, List
 new RuleMonitor(this, rule))
@@ -77,7 +78,7 @@ private Status doCheckSatisfiable() {
 		for (var ruleMonitor : ruleMonitors) {
 			ruleMonitor.addAssertions(solver);
 		}
-		return solver.check();
+		return context.callWithInterrupt(solver::check);
 	}
 
 	private void startIfNeeded() {
@@ -113,7 +114,7 @@ public PropagationResult concretize(Object reason) {
 				if (!variableMonitor.isTracking()) {
 					yield PropagationResult.UNCHANGED;
 				}
-				var model = solver.getModel();
+				var model = context.callWithInterrupt(solver::getModel);
 				if (model == null) {
 					yield new PropagationRejectedResult(reason, REJECTION_NO_MODEL, true);
 				}
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();

From 9d10ff9fa7641cb67e180c448591c49f84531bd5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= 
Date: Mon, 9 Mar 2026 21:48:10 +0100
Subject: [PATCH 07/10] feat(reasoning): SMT solver resource limit

---
 .../reasoning/smt/internal/context/ModelContext.java   |  4 +++-
 .../reasoning/smt/internal/solver/RuleBasedSolver.java | 10 ++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)

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
index 25fa39027..6db498caa 100644
--- 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
@@ -32,7 +32,8 @@
 import java.util.concurrent.Callable;
 
 public class ModelContext implements AutoCloseable {
-	public static final int SOLVER_TIMEOUT = 10000;
+	public static final int SOLVER_TIMEOUT = 10_000;
+	public static final int SOLVER_RLIMIT = 1_000_000;
 
 	private final Model model;
 	private final ModelQueryAdapter queryEngine;
@@ -91,6 +92,7 @@ public RuleBasedSolver createSolver(Concreteness concreteness) {
 		var params = context.mkParams();
 		params.add("model", concreteness == Concreteness.CANDIDATE);
 		params.add("timeout", SOLVER_TIMEOUT);
+		params.add("rlimit", SOLVER_RLIMIT);
 		solver.setParameters(params);
 		return new RuleBasedSolver(this, concreteness, rules, solver);
 	}
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
index ad3c368b7..cb75698ea 100644
--- 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
@@ -7,6 +7,8 @@
 
 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;
@@ -18,6 +20,8 @@
 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";
@@ -96,6 +100,9 @@ public PropagationResult checkSatisfiable(Object reason) {
 			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);
@@ -109,6 +116,9 @@ public PropagationResult concretize(Object reason) {
 			return cachedResult;
 		}
 		var status = doCheckSatisfiable();
+		if (LOGGER.isTraceEnabled()) {
+			LOGGER.trace("concretize {}", solver.getStatistics());
+		}
 		cachedResult = switch (status) {
 			case SATISFIABLE -> {
 				if (!variableMonitor.isTracking()) {

From 7cc3776a40815b7c98927b88815c193b783a3f52 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= 
Date: Wed, 18 Mar 2026 20:24:31 +0100
Subject: [PATCH 08/10] feat(reasoning): theory selection by imports

---
 settings.gradle.kts                           |   1 +
 .../frontend/src/editor/EditorTheme.ts        |   2 +
 .../frontend/src/language/problem.grammar     |   7 +-
 .../src/language/problemLanguageSupport.ts    |   7 +-
 subprojects/generator/build.gradle.kts        |   1 +
 .../contentassist/ProblemProposalUtils.java   |  10 +-
 subprojects/language-model/problem.aird       | 243 ++++++++++++++++--
 .../src/main/resources/model/problem.ecore    |   4 +
 .../src/main/resources/model/problem.genmodel |   3 +
 .../language-semantics-z3/build.gradle.kts    |  19 ++
 .../language/semantics/z3/Z3Annotations.java  |  92 +++++++
 .../language/semantics/z3/Z3Library.java      |  26 ++
 .../semantics/z3/Z3TheoryProvider.java        |  35 +++
 ...y.language.annotations.AnnotationValidator |   5 +
 ....refinery.language.library.RefineryLibrary |   5 +
 ...y.language.semantics.theory.TheoryProvider |   5 +
 .../semantics/z3/builtin/theory/z3.refinery   |   9 +
 .../z3/builtin/theory/z3/core.refinery        |   5 +
 .../language-semantics/build.gradle.kts       |   1 -
 .../language/semantics/ModelInitializer.java  |  51 ++--
 .../annotations/TopLevelAnnotations.java      |  67 +++++
 .../internal/query/FunctionCompiler.java      |   2 +-
 .../internal/query/RuleCompiler.java          |  19 +-
 .../semantics/theory/TheoryProvider.java      |  18 ++
 .../theory/internal/TheoryManager.java        | 183 +++++++++++++
 .../tools/refinery/language/Problem.xtext     |  12 +-
 .../annotations/BuiltinAnnotations.java       |  27 +-
 .../library/ClasspathBasedLibrary.java        |   1 -
 .../ProblemResourceDescriptionStrategy.java   |  24 +-
 .../scoping/imports/ImportAdapter.java        |  51 +---
 .../typesystem/SignatureProvider.java         |   4 +
 .../utils/BuiltinAnnotationContext.java       |  25 +-
 .../refinery/language/utils/ProblemUtil.java  |   2 +-
 .../refinery/language/utils/ServiceUtil.java  |  54 ++++
 .../language/validation/ProblemValidator.java |  20 +-
 .../store/reasoning/smt/SmtPropagator.java    |  25 +-
 .../store/reasoning/smt/Z3Theory.java         |  41 +++
 .../reasoning/smt/expr/SmtExprChecker.java    |  60 +++++
 .../context => expr}/TermToExpr.java          |   3 +-
 .../smt/internal/BoundSmtPropagator.java      |   5 +-
 .../smt/internal/PreparedSmtRule.java         |   9 +-
 .../smt/internal/context/ModelContext.java    |  18 +-
 .../store/reasoning/theory/Theory.java        |  16 ++
 .../store/reasoning/theory/TheoryRule.java}   |  12 +-
 .../store/reasoning/theory/TheorySupport.java |  30 +++
 45 files changed, 1085 insertions(+), 174 deletions(-)
 create mode 100644 subprojects/language-semantics-z3/build.gradle.kts
 create mode 100644 subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Annotations.java
 create mode 100644 subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Library.java
 create mode 100644 subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3TheoryProvider.java
 create mode 100644 subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.annotations.AnnotationValidator
 create mode 100644 subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.library.RefineryLibrary
 create mode 100644 subprojects/language-semantics-z3/src/main/resources/META-INF/services/tools.refinery.language.semantics.theory.TheoryProvider
 create mode 100644 subprojects/language-semantics-z3/src/main/resources/tools/refinery/language/semantics/z3/builtin/theory/z3.refinery
 create mode 100644 subprojects/language-semantics-z3/src/main/resources/tools/refinery/language/semantics/z3/builtin/theory/z3/core.refinery
 create mode 100644 subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/annotations/TopLevelAnnotations.java
 create mode 100644 subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/theory/TheoryProvider.java
 create mode 100644 subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/theory/internal/TheoryManager.java
 create mode 100644 subprojects/language/src/main/java/tools/refinery/language/utils/ServiceUtil.java
 create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/Z3Theory.java
 create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/expr/SmtExprChecker.java
 rename subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/{internal/context => expr}/TermToExpr.java (97%)
 create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/Theory.java
 rename subprojects/{store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java => store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheoryRule.java} (50%)
 create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheorySupport.java

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 345809d73..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 "."
   } |
@@ -185,7 +188,7 @@ AssertionArgument { NodeName | StarArgument }
 
 AssertionActionArgument { VariableName | StarArgument }
 
-TermAction { ckw<"assert"> Expr }
+TermAction { ckw<"assert"> Expr (ckw<"using"> ( TheoryName | "{" sep<",", TheoryName> "}"))? }
 
 Constant { Real | String | StarMult | LogicValue }
 
@@ -221,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 a2c711398..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 assert': 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/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 c293a38b6..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
+        
+        
+      
+      
+    
     
     
     
@@ -6476,6 +6562,10 @@
               
               
             
+            
+              
+              
+            
             
             
           
@@ -6504,6 +6594,19 @@
           
           
         
+        
+          
+          
+            
+              
+              
+            
+            
+            
+          
+          
+          
+        
         
         
           
@@ -6649,6 +6752,22 @@
           
           
         
+        
+          
+            
+          
+          
+            
+          
+          
+            
+          
+          
+          
+          
+          
+          
+        
       
     
     
@@ -6907,13 +7026,13 @@
       
       
     
-    
+    
       
       
       KEEP_LOCATION
       KEEP_SIZE
       KEEP_RATIO
-      
+      
         
       
       
@@ -6925,16 +7044,24 @@
         
         
       
+      
+        
+        
+        
+          
+        
+        
+      
     
     
       
       
-      
+      
         
-        
+        
           italic
         
-        
+        
       
       
     
@@ -6997,15 +7124,44 @@
     
       
       
-      
+      
         
-        
+        
           italic
         
-        
+        
       
       
     
+    
+      
+      
+      
+        
+      
+      
+      
+        
+        
+        
+          italic
+          
+        
+        
+      
+    
+    
+      
+      
+      
+        
+        
+        
+          labelSize
+        
+      
+      
+    
     
     
     
@@ -7023,7 +7179,7 @@
             
           
           
-          
+          
         
         
           
@@ -7049,7 +7205,7 @@
             
           
           
-          
+          
         
         
           
@@ -7263,6 +7419,15 @@
           
           
         
+        
+          
+          
+            
+            
+          
+          
+          
+        
         
         
           
@@ -7728,6 +7893,22 @@
           
           
         
+        
+          
+            
+          
+          
+            
+          
+          
+            
+          
+          
+          
+          
+          
+          
+        
       
     
     
@@ -8035,7 +8216,7 @@
       
       
     
-    
+    
       
       
       KEEP_LOCATION
@@ -8410,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 973ef9e28..2ee7b70b9 100644
--- a/subprojects/language-model/src/main/resources/model/problem.ecore
+++ b/subprojects/language-model/src/main/resources/model/problem.ecore
@@ -328,5 +328,9 @@
   
   
     
+    
+    
   
+  
 
diff --git a/subprojects/language-model/src/main/resources/model/problem.genmodel b/subprojects/language-model/src/main/resources/model/problem.genmodel
index d9462b808..0114d59c1 100644
--- a/subprojects/language-model/src/main/resources/model/problem.genmodel
+++ b/subprojects/language-model/src/main/resources/model/problem.genmodel
@@ -279,6 +279,9 @@
     
     
       
+      
+      
     
+    
   
 
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/Z3TheoryProvider.java b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3TheoryProvider.java
new file mode 100644
index 000000000..b918523a9
--- /dev/null
+++ b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3TheoryProvider.java
@@ -0,0 +1,35 @@
+/*
+ * 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.smt.Z3Theory;
+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/build.gradle.kts b/subprojects/language-semantics/build.gradle.kts
index fe39ada70..98e5b3666 100644
--- a/subprojects/language-semantics/build.gradle.kts
+++ b/subprojects/language-semantics/build.gradle.kts
@@ -19,7 +19,6 @@ dependencies {
 	api(project(":refinery-store-reasoning"))
 	api(libs.eclipseCollections)
 	implementation(project(":refinery-store-reasoning-scope"))
-	implementation(project(":refinery-store-reasoning-smt"))
 	runtimeOnly(libs.eclipseCollections.impl)
 	testImplementation(project(":refinery-store-dse-visualization"))
 	testImplementation(project(":refinery-store-query-interpreter"))
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 b1c0d243c..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;
@@ -44,8 +46,6 @@
 import tools.refinery.store.reasoning.scope.ScopePropagator;
 import tools.refinery.store.reasoning.seed.ModelSeed;
 import tools.refinery.store.reasoning.seed.Seed;
-import tools.refinery.store.reasoning.smt.SmtPropagator;
-import tools.refinery.store.reasoning.smt.SmtRule;
 import tools.refinery.store.reasoning.translator.ConcretizationSettings;
 import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.reasoning.translator.attribute.AttributeInfo;
@@ -108,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;
 
@@ -136,8 +142,6 @@ public class ModelInitializer {
 
 	private ScopePropagator scopePropagator;
 
-	private SmtPropagator smtPropagator;
-
 	private int nodeCount;
 
 	private ModelSeed.Builder modelSeedBuilder;
@@ -153,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);
@@ -247,12 +253,7 @@ public void configureStoreBuilder(ModelStoreBuilder storeBuilder) {
 			}
 			collectPredicates(storeBuilder);
 			collectRules(storeBuilder);
-			if (smtPropagator != null) {
-				if (storeBuilder.tryGetAdapter(PropagationBuilder.class).isEmpty()) {
-					throw new TracedException(problem, "SMT rules require a PropagationBuilder");
-				}
-				storeBuilder.with(smtPropagator);
-			}
+			theoryManager.configure(storeBuilder);
 			storeBuilder.tryGetAdapter(StateCoderBuilder.class)
 					.ifPresent(stateCoderBuilder -> stateCoderBuilder.individuals(individuals));
 			if (!keepShadowPredicates) {
@@ -407,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())));
 	}
@@ -1083,7 +1080,7 @@ private void collectRule(RuleDefinition ruleDefinition, ModelStoreBuilder storeB
 						ConcretenessSpecification.CANDIDATE);
 				rules.addAll(propagationRules);
 				rules.addAll(concretizationRules);
-				addSmtRules(ruleCompiler.toSmtRules(name, ruleDefinition));
+				ruleCompiler.createTheoryRules(name, ruleDefinition, ConcretenessSpecification.UNSPECIFIED);
 				problemTrace.putPropagationRuleDefinition(ruleDefinition, List.copyOf(rules));
 				storeBuilder.tryGetAdapter(PropagationBuilder.class).ifPresent(propagationBuilder -> {
 					propagationBuilder.rules(propagationRules);
@@ -1092,9 +1089,7 @@ private void collectRule(RuleDefinition ruleDefinition, ModelStoreBuilder storeB
 			}
 			case CONCRETIZATION -> {
 				var rules = ruleCompiler.toPropagationRules(name, ruleDefinition, ConcretenessSpecification.CANDIDATE);
-				addSmtRules(ruleCompiler.toSmtRules(name, ruleDefinition).stream()
-						.map(smtRule -> smtRule.withConcreteness(ConcretenessSpecification.CANDIDATE))
-						.toList());
+				ruleCompiler.createTheoryRules(name, ruleDefinition, ConcretenessSpecification.CANDIDATE);
 				problemTrace.putPropagationRuleDefinition(ruleDefinition, rules);
 				storeBuilder.tryGetAdapter(PropagationBuilder.class)
 						.ifPresent(propagationBuilder -> propagationBuilder.concretizationRules(rules));
@@ -1117,14 +1112,4 @@ private void collectRule(RuleDefinition ruleDefinition, ModelStoreBuilder storeB
 			throw TracedException.addTrace(ruleDefinition, e);
 		}
 	}
-
-	private void addSmtRules(Collection smtRules) {
-		if (smtRules.isEmpty()) {
-			return;
-		}
-		if (smtPropagator == null) {
-			smtPropagator = new SmtPropagator();
-		}
-		smtPropagator.rules(smtRules);
-	}
 }
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 dc2c18bd9..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,7 +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.smt.SmtRule;
+import tools.refinery.store.reasoning.theory.TheoryRule;
 import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
 
 import java.util.*;
@@ -49,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) {
@@ -212,16 +216,16 @@ private static String getPropagationActionName(String name, int actionCount, int
 		return actionCount == 1 ? name : name + "#" + (i + 1);
 	}
 
-	public Collection toSmtRules(String name, RuleDefinition ruleDefinition) {
+	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 List.of();
+			return;
 		}
 		var actions = consequents.getFirst().getActions();
 		int actionCount = actions.size();
-		var rules = new ArrayList();
 		for (int i = 0; i < actionCount; i++) {
 			var action = actions.get(i);
 			if (!(action instanceof TheoryAction theoryAction)) {
@@ -237,12 +241,13 @@ public Collection toSmtRules(String name, RuleDefinition ruleDefinition
 						.map(Variable::asNodeVariable)
 						.toList();
 				var query = preparedRule.buildQuery(actionName, parameters, moreCommonLiterals, queryCompiler);
-				rules.add(new SmtRule(query, term));
+				var theoryRule = new TheoryRule(query, term, concretenessSpecification);
+				theoryManager.addRule(theoryAction, theoryRule);
+
 			} catch (RuntimeException e) {
 				throw TracedException.addTrace(action, e);
 			}
 		}
-		return rules;
 	}
 
 	public Rule toRule(String name, RuleDefinition ruleDefinition) {
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 13334868d..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")
@@ -151,7 +154,12 @@ AssertionAction:
 	"(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")";
 
 TheoryAction:
-	"assert" term=Expr;
+	"assert" term=Expr
+	(theoryOverride?="using" (
+		theories+=[TheoryDeclaration|QualifiedName] |
+		"{" (theories+=[TheoryDeclaration|QualifiedName]
+		("," theories+=[TheoryDeclaration|QualifiedName])*)? "}"
+	))?;
 
 Expr:
 	AssignmentExpr;
@@ -333,7 +341,7 @@ NonContainmentIdentifier:
 	ID | QUOTED_ID | "as" | "atom" | "multi" | "problem" | "module" |
 	"datatype" | "aggregator" | "primitive" |
 	"decision" | "propagation" | "concretization" |
-	"shadow" | "assert";
+	"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/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 bbf509617..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,7 +60,7 @@ 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;
 		};
 	}
 
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/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java
index 36f7e2edd..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;
@@ -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
@@ -1029,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/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 567826039..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
@@ -16,6 +16,7 @@
 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;
 
 import java.util.ArrayList;
@@ -24,26 +25,38 @@
 import java.util.Set;
 
 public class SmtPropagator implements ModelStoreConfiguration {
-	private final List rules = new ArrayList<>();
+	private final List rules = new ArrayList<>();
+	private int timeout;
+	private int rlimit;
 
 	public SmtPropagator rule(RelationalQuery precondition, Term assertedTerm) {
-		return rule(new SmtRule(precondition, assertedTerm));
+		return rule(new TheoryRule(precondition, assertedTerm));
 	}
 
-	public SmtPropagator rule(SmtRule rule) {
+	public SmtPropagator rule(TheoryRule rule) {
 		rules.add(rule);
 		return this;
 	}
 
-	public SmtPropagator rules(SmtRule... rules) {
+	public SmtPropagator rules(TheoryRule... rules) {
 		return rules(List.of(rules));
 	}
 
-	public SmtPropagator rules(Collection 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();
@@ -53,7 +66,7 @@ public void apply(ModelStoreBuilder storeBuilder) {
 			queryEngineBuilder.queries(preparedRule.partialPrecondition(), preparedRule.candidatePrecondition());
 		}
 		storeBuilder.getAdapter(PropagationBuilder.class)
-				.propagator(model -> new BoundSmtPropagator(this, model, preparedRules));
+				.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/Z3Theory.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/Z3Theory.java
new file mode 100644
index 000000000..7f2de231f
--- /dev/null
+++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/Z3Theory.java
@@ -0,0 +1,41 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Refinery Authors 
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.smt;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+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;
+
+public 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/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/internal/context/TermToExpr.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/expr/TermToExpr.java
similarity index 97%
rename from subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/TermToExpr.java
rename to subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/expr/TermToExpr.java
index 1166aca21..197553614 100644
--- a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/internal/context/TermToExpr.java
+++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/expr/TermToExpr.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.smt.internal.context;
+package tools.refinery.store.reasoning.smt.expr;
 
 import com.microsoft.z3.Context;
 import com.microsoft.z3.Expr;
@@ -14,6 +14,7 @@
 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;
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
index 0527c210c..d488a8c5e 100644
--- 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
@@ -22,9 +22,10 @@ public class BoundSmtPropagator implements BoundPropagator, ModelListener {
 	private final RuleBasedSolver propagationSolver;
 	private final RuleBasedSolver concretizationSolver;
 
-	public BoundSmtPropagator(SmtPropagator propagator, Model model, Collection rules) {
+	public BoundSmtPropagator(SmtPropagator propagator, Model model, Collection rules,
+							  int timeout, int rlimit) {
 		this.propagator = propagator;
-		context = new ModelContext(model, rules);
+		context = new ModelContext(model, rules, timeout, rlimit);
 		propagationSolver = context.createSolver(Concreteness.PARTIAL);
 		concretizationSolver = context.createSolver(Concreteness.CANDIDATE);
 	}
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
index 554b3c5a7..c4da399f6 100644
--- 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
@@ -11,7 +11,8 @@
 import tools.refinery.logic.dnf.Query;
 import tools.refinery.logic.dnf.RelationalQuery;
 import tools.refinery.logic.dnf.SymbolicParameter;
-import tools.refinery.logic.literal.*;
+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;
@@ -22,7 +23,7 @@
 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.smt.SmtRule;
+import tools.refinery.store.reasoning.theory.TheoryRule;
 import tools.refinery.store.tuple.Tuple;
 
 import java.util.ArrayList;
@@ -40,7 +41,7 @@
 public record PreparedSmtRule(RelationalQuery partialPrecondition, RelationalQuery candidatePrecondition,
 							  Term assertedTerm, ObjectIntMap parameterMap,
 							  List influences) {
-	public static PreparedSmtRule of(SmtRule rule) {
+	public static PreparedSmtRule of(TheoryRule rule) {
 		var precondition = rule.precondition().getDnf();
 		var symbolicParameters = precondition.getSymbolicParameters();
 		var parameterVariables = symbolicParameters.stream().map(SymbolicParameter::getVariable).toList();
@@ -62,7 +63,7 @@ public static PreparedSmtRule of(SmtRule rule) {
 			candidateLiterals.add(must(EXISTS_SYMBOL.call(variable)));
 		}
 
-		var concreteness = rule.concreteness();
+		var concreteness = rule.concretenessSpecification();
 		var partialPreconditionBuilder = Query.builder(precondition.name() + "#partial")
 				.symbolicParameters(symbolicParameters);
 		if (concreteness != ConcretenessSpecification.CANDIDATE) {
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
index 6db498caa..19e7d3b84 100644
--- 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
@@ -21,6 +21,7 @@
 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;
@@ -32,13 +33,12 @@
 import java.util.concurrent.Callable;
 
 public class ModelContext implements AutoCloseable {
-	public static final int SOLVER_TIMEOUT = 10_000;
-	public static final int SOLVER_RLIMIT = 1_000_000;
-
 	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;
@@ -49,10 +49,12 @@ public class ModelContext implements AutoCloseable {
 	private final Map>> exprCache = new HashMap<>();
 	private final InterruptibleWrapper interruptibleWrapper;
 
-	public ModelContext(Model model, Collection rules) {
+	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();
@@ -91,8 +93,12 @@ public RuleBasedSolver createSolver(Concreteness concreteness) {
 		var solver = context.mkSolver();
 		var params = context.mkParams();
 		params.add("model", concreteness == Concreteness.CANDIDATE);
-		params.add("timeout", SOLVER_TIMEOUT);
-		params.add("rlimit", SOLVER_RLIMIT);
+		if (timeout > 0) {
+			params.add("timeout", timeout);
+		}
+		if (rlimit > 0) {
+			params.add("rlimit", rlimit);
+		}
 		solver.setParameters(params);
 		return new RuleBasedSolver(this, concreteness, rules, solver);
 	}
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-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheoryRule.java
similarity index 50%
rename from subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java
rename to subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheoryRule.java
index 16fcab2d3..40a3489a7 100644
--- a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtRule.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/theory/TheoryRule.java
@@ -3,20 +3,20 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.smt;
+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 SmtRule(RelationalQuery precondition, Term assertedTerm,
-					  ConcretenessSpecification concreteness) {
-	public SmtRule(RelationalQuery precondition, Term assertedTerm) {
+public record TheoryRule(RelationalQuery precondition, Term assertedTerm,
+						 ConcretenessSpecification concretenessSpecification) {
+	public TheoryRule(RelationalQuery precondition, Term assertedTerm) {
 		this(precondition, assertedTerm, ConcretenessSpecification.UNSPECIFIED);
 	}
 
-	public SmtRule withConcreteness(ConcretenessSpecification newConcreteness) {
-		return new SmtRule(precondition, assertedTerm, newConcreteness);
+	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;
+	}
+}

From ac7aa9b2557040a572b69bbce21cb35766dd3763 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= 
Date: Wed, 3 Jun 2026 15:05:34 +0200
Subject: [PATCH 09/10] feat(reasoning): mutable function values in theory
 actions

---
 .../validation/ActionTargetCollector.java     | 35 ++++++++++++++++---
 1 file changed, 30 insertions(+), 5 deletions(-)

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);
+		}
+	}
 }

From 419ff71c77b9e3a0043cb4cd77bd27f8fc0606ec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= 
Date: Wed, 3 Jun 2026 16:07:34 +0200
Subject: [PATCH 10/10] refactor(semantics): make Z3Theory package private

---
 .../java/tools/refinery/language/semantics/z3}/Z3Theory.java | 5 +++--
 .../refinery/language/semantics/z3/Z3TheoryProvider.java     | 1 -
 2 files changed, 3 insertions(+), 3 deletions(-)
 rename subprojects/{store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt => language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3}/Z3Theory.java (88%)

diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/Z3Theory.java b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Theory.java
similarity index 88%
rename from subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/Z3Theory.java
rename to subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Theory.java
index 7f2de231f..0a63d8d8a 100644
--- a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/Z3Theory.java
+++ b/subprojects/language-semantics-z3/src/main/java/tools/refinery/language/semantics/z3/Z3Theory.java
@@ -3,9 +3,10 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.smt;
+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;
@@ -13,7 +14,7 @@
 
 import java.util.Collection;
 
-public class Z3Theory implements Theory {
+class Z3Theory implements Theory {
 	private final SmtExprChecker checker = new SmtExprChecker();
 	private final int timeout;
 	private final int 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
index b918523a9..242594398 100644
--- 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
@@ -9,7 +9,6 @@
 import tools.refinery.language.annotations.Annotations;
 import tools.refinery.language.semantics.ProblemTrace;
 import tools.refinery.language.semantics.theory.TheoryProvider;
-import tools.refinery.store.reasoning.smt.Z3Theory;
 import tools.refinery.store.reasoning.theory.Theory;
 
 import java.util.Optional;