Merge pull request #57 from kris7t/logic-extract

Refactor logic expressions

buildSrc/src/main/kotlin/tools/refinery/gradle/internal/java-conventions.gradle.kts

@@ -101,6 +101,14 @@ tasks {
 publishing.publications {
 	create<MavenPublication>("mavenJava") {
 		from(components["java"])
+		pom {
+			licenses {
+				license {
+					name = "Eclipse Public License - v 2.0"
+					url = "https://www.eclipse.org/legal/epl-2.0/"
+				}
+			}
+		}
 	}
 }
 

buildSrc/src/main/kotlin/tools/refinery/gradle/interpreter-library.gradle.kts

@@ -8,7 +8,6 @@ package tools.refinery.gradle
 import tools.refinery.gradle.utils.SonarPropertiesUtils
 
 plugins {
-	id("maven-publish")
 	id("tools.refinery.gradle.java-library")
 	id("tools.refinery.gradle.sonarqube")
 }

gradle.properties

@@ -1,4 +1,4 @@
-# SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+# SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
 #
 # SPDX-License-Identifier: EPL-2.0
 

gradle/libs.versions.toml

@@ -41,6 +41,7 @@ mwe-utils = { group = "org.eclipse.emf", name = "org.eclipse.emf.mwe.utils", ver
 mwe2-launch = { group = "org.eclipse.emf", name = "org.eclipse.emf.mwe2.launch", version.ref = "mwe2" }
 mwe2-lib = { group = "org.eclipse.emf", name = "org.eclipse.emf.mwe2.lib", version.ref = "mwe2" }
 ortools = { group = "com.google.ortools", name = "ortools-java", version = "9.9.3963" }
+refinery-z3 = { group = "tools.refinery.z3", name = "refinery-z3-solver", version = "4.12.6" }
 slf4j-api = { group = "org.slf4j", name = "slf4j-api", version.ref = "slf4j" }
 slf4j-simple = { group = "org.slf4j", name = "slf4j-simple", version.ref = "slf4j" }
 slf4j-log4j = { group = "org.slf4j", name = "log4j-over-slf4j", version.ref = "slf4j" }

settings.gradle.kts

@@ -19,17 +19,21 @@ include(
 		"language-model",
 		"language-semantics",
 		"language-web",
+		"logic",
 		"store",
 		"store-dse",
 		"store-dse-visualization",
 		"store-query",
 		"store-query-interpreter",
 		"store-reasoning",
 		"store-reasoning-scope",
+		"store-reasoning-smt",
 )
 
 for (project in rootProject.children) {
 	val projectName = project.name
 	project.name = "${rootProject.name}-$projectName"
 	project.projectDir = file("subprojects/$projectName")
 }
+
+includeBuild("z3")

subprojects/frontend/src/editor/EditorTheme.ts

@@ -166,6 +166,11 @@ export default styled('div', {
     '.tok-problem-abstract': {
       fontStyle: 'italic',
     },
+    '.tok-problem-datatype, .tok-problem-aggregator': {
+      '&, & .tok-typeName': {
+        color: theme.palette.primary.main,
+      },
+    },
     '.tok-problem-containment': {
       fontWeight: theme.typography.fontWeightEditorBold,
       textDecorationSkipInk: 'none',

subprojects/frontend/src/language/problem.grammar

@@ -9,13 +9,16 @@
 @external prop implicitCompletion from './props'
 
 @precedence {
+  cast,
   prefix,
+  range @left,
   exponential @right,
   multiplicative @left,
   additive @left,
-  range @left,
   lattice @left,
   comparison @left,
+  boolean @left,
+  assignment,
   feature @cut
 }
 
@@ -42,6 +45,12 @@ statement {
     kw<"enum"> RelationName
     (EnumBody { "{" sep<",", AtomNodeName> "}" } | ".")
   } |
+  DatatypeDeclaration {
+    kw<"extern"> ckw<"datatype"> DatatypeName "."
+  } |
+  AggregatorDeclaration {
+    kw<"extern"> ckw<"aggregator"> AggregatorName "."
+  } |
   PredicateDefinition {
     (
       (kw<"error"> | ckw<"contained"> | kw<"containment">)? kw<"pred"> |
@@ -50,10 +59,10 @@ statement {
     RelationName ParameterList<Parameter>?
     PredicateBody { ("<->" sep<OrOp, Conjunction>)? "." }
   } |
-  FunctionDefinition {
-    kw<"fn"> PrimitiveType RelationName ParameterList<Parameter>?
-    FunctionBody { ("=" sep<OrOp, Case>)? "." }
-  } |
+  // FunctionDefinition {
+  //   kw<"fn"> RelationName RelationName ParameterList<Parameter>?
+  //   FunctionBody { ("=" sep<OrOp, Case>)? "." }
+  // } |
   //RuleDefinition {
   //  kw<"rule">
   //  RuleName ParameterList<Parameter>?
@@ -77,7 +86,7 @@ FeatureDeclaration {
       ReferenceKind !feature ~featureHead
     } |
     FeatureDeclarationHeadWithoutKind {
-      (PrimitiveType | kw<"bool">)? ~featureHead
+      ~featureHead
     }
   )
   RelationName
@@ -87,36 +96,42 @@ FeatureDeclaration {
   ";"?
 }
 
-Parameter { Modality? RelationName? VariableName }
+Parameter { RelationName? VariableName }
 
 // Use @dynamicPrecedence to prevent a(b) from being parsed as Expr { a } Expr { b }
 // instead of Atom { a(b) }
 // Being looser with token sequencing enables more consistent syntactic highlighting.
 Conjunction { ("," | NextConjunction[@dynamicPrecedence=-10] { Expr })+ }
 
-Case { Conjunction ("->" Expr)? }
+// Case { Conjunction ("->" Expr)? }
 
 OrOp { ";" }
 
 Expr {
-  UnaryExpr | BinaryExpr | Aggregation | VariableName | Atom | Constant | "(" Expr ")"
+  AssignmentExpr | UnaryExpr | BinaryExpr | CastExpr | Aggregation |
+  VariableName | Atom | Constant | "(" Expr ")"
 }
 
+AssignmentExpr { !assignment VariableName kw<"is"> Expr }
+
 BinaryExpr {
+  Expr !boolean ("&&" | "||" | "^^") Expr |
   Expr !comparison ComparisonOp Expr |
   Expr !lattice (LatticeMeet | "\\/") Expr |
-  Expr !range ".." Expr |
   Expr !additive ("+" | "-") Expr |
-  Expr !multiplicative (StarMult | Divide) Expr |
-  Expr !exponential "**" Expr
+  Expr !multiplicative (Star | Divide) Expr |
+  Expr !exponential "**" Expr |
+  Expr !range ".." Expr
 }
 
 UnaryExpr {
-  !prefix ("+" | "-" | "!" | kw<"count"> | Modality) Expr
+  !prefix ("+" | "-" | "!" | kw<"count">) Expr
 }
 
+CastExpr { !cast Expr kw<"as"> DatatypeName }
+
 Aggregation {
-  AggregationOp "{" Expr "|" Expr "}"
+  AggregatorName "{" Expr "|" Expr "}"
 }
 
 Atom { RelationName "+"? ParameterList<Expr> }
@@ -137,22 +152,10 @@ ReferenceKind {
   kw<"refers"> | ckw<"contains"> | kw<"container">
 }
 
-PrimitiveType {
-  kw<"int"> | kw<"real"> | kw<"string">
-}
-
 LogicValue {
   kw<"true"> | kw<"false"> | kw<"unknown"> | kw<"error">
 }
 
-Modality {
-  kw<"must"> | kw<"may"> | kw<"current">
-}
-
-AggregationOp {
-  ckw<"sum"> | ckw<"prod"> | ckw<"min"> | ckw<"max">
-}
-
 ComparisonOp { SymbolicComparisonOp | kw<"in"> }
 
 ScopeElement { RelationName ("=" | "+=") Multiplicity }
@@ -165,6 +168,8 @@ Multiplicity { (IntMult "..")? (IntMult | StarMult)}
 // but will go with the transtive closure (and highlight `a` as a relation) if forced.
 RelationName { QualifiedName ~name }
 
+DatatypeName { QualifiedName }
+
 //RuleName { QualifiedName }
 
 AtomNodeName { QualifiedName }
@@ -175,8 +180,12 @@ NodeName { QualifiedName }
 
 ModuleName { QualifiedName }
 
+AggregatorName { QualifiedName }
+
 QualifiedName[implicitCompletion=true] { "::"? identifier (QualifiedNameSeparator "::" identifier)* }
 
+StarMult { Star }
+
 kw<term> { @specialize[@name={term},implicitCompletion=true]<identifier, term> }
 
 ckw<term> { @extend[@name={term},implicitCompletion=true]<identifier, term> }
@@ -216,7 +225,7 @@ sep1<separator, content> { content (separator content)* }
 
   IntMult { int }
 
-  StarMult { "*" }
+  Star { "*" }
 
   Real { (exponential | int ("." (int | exponential))?) }
 
@@ -229,7 +238,7 @@ sep1<separator, content> { content (separator content)* }
 
   SymbolicComparisonOp {
     ">" | ">=" | "<" | "<=" | "==" | "!=" |
-    "<:" | ":>" | "===" | "!=="
+    "===" | "!=="
   }
 
   NotOp { "!" }

subprojects/frontend/src/language/problemLanguageSupport.ts

@@ -29,21 +29,22 @@ const parserWithMetadata = parser.configure({
       BlockComment: t.blockComment,
       'module problem class enum pred fn scope': t.definitionKeyword,
       'import as declare atom multi': t.definitionKeyword,
+      'extern datatype aggregator': t.definitionKeyword,
       'abstract extends refers contains container opposite': t.modifier,
-      'default error contained containment': t.modifier,
+      default: t.modifier,
       'true false unknown error': t.keyword,
-      'int real string bool': t.keyword,
-      'may must current count': t.operatorKeyword,
-      'sum prod min max in': t.operatorKeyword,
+      'count in is': t.operatorKeyword,
       // 'new delete': t.keyword,
       NotOp: t.operator,
       UnknownOp: t.operator,
       OrOp: t.separator,
       StarArgument: t.keyword,
-      'IntMult StarMult Real': t.number,
-      StarMult: t.number,
+      'IntMult Real': t.number,
+      'StarMult/Star': t.number,
       String: t.string,
       'RelationName/QualifiedName': t.typeName,
+      'DatatypeName/QualifiedName': t.keyword,
+      'AggregatorName/QualifiedName': t.operatorKeyword,
       // 'RuleName/QualifiedName': t.typeName,
       'AtomNodeName/QualifiedName': t.atom,
       'VariableName/QualifiedName': t.variableName,
@@ -60,7 +61,7 @@ const parserWithMetadata = parser.configure({
       NodeDeclaration: indentDeclaration,
       ScopeDeclaration: indentDeclaration,
       PredicateBody: indentPredicateOrRule,
-      FunctionBody: indentPredicateOrRule,
+      // FunctionBody: indentPredicateOrRule,
       // RuleBody: indentPredicateOrRule,
       BlockComment: indentBlockComment,
     }),
@@ -69,7 +70,7 @@ const parserWithMetadata = parser.configure({
       EnumBody: foldInside,
       ParameterList: foldInside,
       PredicateBody: foldInside,
-      FunctionBody: foldInside,
+      // FunctionBody: foldInside,
       // RuleBody: foldInside,
       Conjunction: foldConjunction,
       // Consequent: foldWholeNode,

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

@@ -6,6 +6,7 @@
 package tools.refinery.generator;
 
 import tools.refinery.language.semantics.ProblemTrace;
+import tools.refinery.logic.AbstractValue;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.reasoning.ReasoningAdapter;
@@ -52,7 +53,8 @@ public Concreteness getConcreteness() {
 		return concreteness;
 	}
 
-	public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) {
+	public <A extends AbstractValue<A, C>, C> PartialInterpretation<A, C> getPartialInterpretation(
+			PartialSymbol<A, C> partialSymbol) {
 		return reasoningAdapter.getPartialInterpretation(concreteness, partialSymbol);
 	}
 }

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

@@ -9,6 +9,7 @@
 import tools.refinery.language.model.problem.Problem;
 import tools.refinery.language.semantics.ProblemTrace;
 import tools.refinery.language.semantics.SolutionSerializer;
+import tools.refinery.logic.AbstractValue;
 import tools.refinery.store.dse.strategy.BestFirstStoreManager;
 import tools.refinery.store.map.Version;
 import tools.refinery.store.model.ModelStore;
@@ -24,7 +25,7 @@ public class ModelGenerator extends ModelFacade {
 	private boolean lastGenerationSuccessful;
 
 	ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed,
-                          Provider<SolutionSerializer> solutionSerializerProvider) {
+				   Provider<SolutionSerializer> solutionSerializerProvider) {
 		super(problemTrace, store, modelSeed, Concreteness.CANDIDATE);
 		this.solutionSerializerProvider = solutionSerializerProvider;
 		initialVersion = getModel().commit();
@@ -66,7 +67,8 @@ public void generate() {
 	}
 
 	@Override
-	public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) {
+	public <A extends AbstractValue<A, C>, C> PartialInterpretation<A, C> getPartialInterpretation(
+			PartialSymbol<A, C> partialSymbol) {
 		checkSuccessfulGeneration();
 		return super.getPartialInterpretation(partialSymbol);
 	}

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

@@ -12,7 +12,10 @@
 import org.eclipse.emf.ecore.util.EcoreUtil;
 import org.eclipse.xtext.diagnostics.Severity;
 import org.eclipse.xtext.naming.IQualifiedNameConverter;
-import org.eclipse.xtext.resource.*;
+import org.eclipse.xtext.resource.FileExtensionProvider;
+import org.eclipse.xtext.resource.IEObjectDescription;
+import org.eclipse.xtext.resource.IResourceFactory;
+import org.eclipse.xtext.resource.XtextResourceSet;
 import org.eclipse.xtext.scoping.impl.GlobalResourceDescriptionProvider;
 import org.eclipse.xtext.util.CancelIndicator;
 import org.eclipse.xtext.util.LazyStringInputStream;
@@ -25,7 +28,7 @@
 import tools.refinery.language.naming.NamingUtil;
 import tools.refinery.language.resource.ProblemResourceDescriptionStrategy;
 import tools.refinery.language.resource.ProblemResourceDescriptionStrategy.ShadowingKey;
-import tools.refinery.language.scoping.imports.ImportAdapter;
+import tools.refinery.language.scoping.imports.ImportAdapterProvider;
 import tools.refinery.language.scoping.imports.ImportCollector;
 import tools.refinery.store.util.CancellationToken;
 
@@ -61,6 +64,9 @@ public class ProblemLoader {
 	@Inject
 	private IQualifiedNameConverter qualifiedNameConverter;
 
+	@Inject
+	private ImportAdapterProvider importAdapterProvider;
+
 	private CancellationToken cancellationToken = CancellationToken.NONE;
 
 	private final List<Path> extraPaths = new ArrayList<>();
@@ -125,7 +131,7 @@ public Problem loadUri(URI uri) throws IOException {
 
 	private XtextResourceSet createResourceSet() {
 		var resourceSet = resourceSetProvider.get();
-		var adapter = ImportAdapter.getOrInstall(resourceSet);
+		var adapter = importAdapterProvider.getOrInstall(resourceSet);
 		adapter.getLibraryPaths().addAll(0, extraPaths);
 		return resourceSet;
 	}

subprojects/interpreter-rete-recipes/src/main/resources/model/recipes.ecore

@@ -399,4 +399,15 @@
     <eStructuralFeatures xsi:type="ecore:EAttribute" name="connectivity" eType="#//Connectivity"/>
   </eClassifiers>
   <eClassifiers xsi:type="ecore:EDataType" name="Connectivity" instanceClassName="tools.refinery.interpreter.matchers.psystem.basicenumerables.Connectivity"/>
+  <eClassifiers xsi:type="ecore:EClass" name="OuterJoinNodeRecipe" eSuperTypes="#//ReteNodeRecipe">
+    <eOperations name="getArity" unique="false" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EInt">
+      <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
+        <details key="body" value="&lt;%tools.refinery.interpreter.rete.recipes.ProjectionIndexerRecipe%> _parent = this.getParent();&#xA;&lt;%tools.refinery.interpreter.rete.recipes.Mask%> _mask = _parent.getMask();&#xA;&lt;%org.eclipse.emf.common.util.EList%>&lt;&lt;%java.lang.Integer%>> _sourceIndices = _mask.getSourceIndices();&#xA;return _sourceIndices.size();"/>
+      </eAnnotations>
+    </eOperations>
+    <eStructuralFeatures xsi:type="ecore:EReference" name="parent" eType="#//ProjectionIndexerRecipe"
+        containment="true" resolveProxies="false"/>
+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="defaultValue" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EJavaObject"/>
+  </eClassifiers>
+  <eClassifiers xsi:type="ecore:EClass" name="OuterJoinIndexerRecipe" eSuperTypes="#//IndexerRecipe"/>
 </ecore:EPackage>

subprojects/interpreter-rete-recipes/src/main/resources/model/recipes.ecore.license

@@ -1,4 +1,4 @@
 Copyright (c) 2004-2014 Gabor Bergmann and Daniel Varro
-Copyright (c) 2023 The Refinery Authors <https://refinery.tools>
+Copyright (c) 2023-2024 The Refinery Authors <https://refinery.tools>
 
 SPDX-License-Identifier: EPL-2.0