SMT solver integration

settings.gradle.kts

@@ -24,6 +24,7 @@ include(
 		"language-ide",
 		"language-model",
 		"language-semantics",
+		"language-semantics-z3",
 		"language-web",
 		"logic",
 		"store",

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

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<Parameter> "."
   } |
@@ -173,7 +176,9 @@ Atom { RelationName "+"? ParameterList<Expr> }
 
 Consequent { ("," | Action)+ }
 
-Action {
+Action { AssertionAction | TermAction }
+
+AssertionAction {
   (NotOp | UnknownOp)? RelationName
   ParameterList<AssertionActionArgument>
   (":" Expr)?
@@ -183,6 +188,8 @@ AssertionArgument { NodeName | StarArgument }
 
 AssertionActionArgument { VariableName | StarArgument }
 
+TermAction { ckw<"assert"> Expr (ckw<"using"> ( TheoryName | "{" sep<",", TheoryName> "}"))? }
+
 Constant { Real | String | StarMult | LogicValue }
 
 LogicValue {
@@ -217,6 +224,8 @@ ModuleName { QualifiedName }
 
 AggregatorName { QualifiedName }
 
+TheoryName { QualifiedName }
+
 AnnotationName { QualifiedName }
 
 ID { identifier | QuotedID }

subprojects/frontend/src/language/problemLanguageSupport.ts

@@ -34,15 +34,15 @@ const parserWithMetadata = parser.configure({
       BlockComment: t.blockComment,
       'module problem class enum pred scope': t.definitionKeyword,
       'import as declare atom multi': t.definitionKeyword,
-      'datatype aggregator primitive': t.definitionKeyword,
+      'datatype aggregator primitive theory': t.definitionKeyword,
       'AnnotationKeyword/#': t.definitionKeyword,
       rule: t.definitionKeyword,
-      'abstract extends refers contains container partial': t.modifier,
+      'abstract extends refers contains container using': t.modifier,
       'opposite subsets': t.modifier,
       default: t.modifier,
       'shadow propagation decision concretization': t.modifier,
       'true false unknown error': t.keyword,
-      'candidate may must': t.operatorKeyword,
+      'partial candidate may must assert': t.operatorKeyword,
       is: t.operatorKeyword,
       NotOp: t.operator,
       UnknownOp: t.operator,
@@ -54,6 +54,7 @@ const parserWithMetadata = parser.configure({
       'RelationName!': t.typeName,
       'DatatypeName!': t.keyword,
       'AggregatorName!': t.operatorKeyword,
+      'TheoryName!': t.keyword,
       'RuleName!': t.typeName,
       'AtomNodeName!': t.atom,
       'VariableName!': t.variableName,

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

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<Tuple, A> getAll() {
 		return new FilteredInterpretationCursor(wrappedInterpretation.getAll());
 	}
 
+	@Override
+	public void addListener(ResultSetListener<A> listener) {
+		throw new UnsupportedOperationException("Filtered interpretations do not support listeners");
+	}
+
+	@Override
+	public void removeListener(ResultSetListener<A> 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++) {

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

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";
 		}