From 286b6de0e20fedeb3cede1b90f4f728be3fdb74a Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 31 Jan 2024 18:26:32 +0100 Subject: refactor: serialize solutions as modules --- .../language/semantics/SolutionSerializer.java | 18 ++++++++++++++---- .../language/semantics/SolutionSerializerTest.java | 16 +++++++++++++--- 2 files changed, 27 insertions(+), 7 deletions(-) diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java index 537d94ca..1bd419d8 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java @@ -68,7 +68,9 @@ public class SolutionSerializer { private Model model; private ReasoningAdapter reasoningAdapter; private PartialInterpretation existsInterpretation; + private Problem originalProblem; private Problem problem; + private NodeDeclaration nodeDeclaration; private final MutableIntObjectMap nodes = IntObjectMaps.mutable.empty(); @Inject @@ -87,14 +89,22 @@ public class SolutionSerializer { reasoningAdapter = model.getAdapter(ReasoningAdapter.class); existsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL); - var originalProblem = trace.getProblem(); + originalProblem = trace.getProblem(); problem = copyProblem(originalProblem, uri); + problem.setKind(ModuleKind.MODULE); problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement); problem.getNodes().removeIf(this::shouldRemoveNode); + nodeDeclaration = ProblemFactory.eINSTANCE.createNodeDeclaration(); + nodeDeclaration.setKind(NodeKind.NODE); + nodeDeclaration.getNodes().addAll(problem.getNodes()); + problem.getStatements().add(nodeDeclaration); nameProvider.setProblem(problem); addExistsAssertions(); addClassAssertions(); addReferenceAssertions(); + if (nodeDeclaration.getNodes().isEmpty()) { + problem.getStatements().remove(nodeDeclaration); + } return problem; } @@ -104,8 +114,8 @@ public class SolutionSerializer { private boolean shouldRemoveNode(Node newNode) { var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(newNode); - var scope = scopeProvider.getScope(trace.getProblem(), ProblemPackage.Literals.ASSERTION__RELATION); - var originalNode = semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class); + var scope = scopeProvider.getScope(originalProblem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE); + var originalNode = semanticsUtils.maybeGetElement(originalProblem, scope, qualifiedName, Node.class); if (originalNode == null) { return false; } @@ -238,7 +248,7 @@ public class SolutionSerializer { var nodeName = nameProvider.getNextName(typeName); node = ProblemFactory.eINSTANCE.createNode(); node.setName(nodeName); - problem.getNodes().add(node); + nodeDeclaration.getNodes().add(node); nodes.put(nodeId, node); } addAssertion(candidateRelation, LogicValue.TRUE, node); diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/SolutionSerializerTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/SolutionSerializerTest.java index b682a7d6..949b7047 100644 --- a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/SolutionSerializerTest.java +++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/SolutionSerializerTest.java @@ -72,7 +72,7 @@ class SolutionSerializerTest { solution.eResource().save(outputStream, Map.of()); actualOutput = outputStream.toString(); } - assertThat(actualOutput, is(prefix + "\n" + expectedOutput)); + assertThat(actualOutput, is("module.\n\n" + prefix + "\n" + expectedOutput)); } static Stream solutionSerializerTest() { @@ -81,6 +81,7 @@ class SolutionSerializerTest { """, """ scope Foo = 3. """, """ + declare foo1, foo2, foo3. !exists(Foo::new). Foo(foo1). Foo(foo2). @@ -94,6 +95,7 @@ class SolutionSerializerTest { """, """ scope Foo = 1. """, """ + declare foo1, bar1, bar2. !exists(Foo::new). !exists(Bar::new). Foo(foo1). @@ -112,6 +114,7 @@ class SolutionSerializerTest { """, """ scope Foo = 1, Bar = 2. """, """ + declare foo1, bar1, bar2. !exists(Foo::new). !exists(Bar::new). Foo(foo1). @@ -131,6 +134,7 @@ class SolutionSerializerTest { scope Person += 0. """, """ + declare a, b, c. !exists(Person::new). Person(a). Person(b). @@ -156,6 +160,7 @@ class SolutionSerializerTest { scope Foo += 0. """, """ + declare foo. !exists(Foo::new). Foo(foo). default !bar(*, *). @@ -166,6 +171,7 @@ class SolutionSerializerTest { """, """ scope Foo = 1, Bar = 0. """, """ + declare foo1. !exists(Foo::new). !exists(Bar::new). Foo(foo1). @@ -180,6 +186,7 @@ class SolutionSerializerTest { scope Foo += 0. """, """ + declare a. !exists(Foo::new). Foo(a). default !ref(*, *). @@ -200,29 +207,32 @@ class SolutionSerializerTest { !exists(Foo::new). scope Foo = 2. """, """ + declare foo1, foo2. !exists(a). !exists(Foo::new). Foo(foo1). Foo(foo2). """), Arguments.of(""" - node a. + declare a. class Foo. """, """ Foo(a). ?exists(a). scope Foo = 2, Foo += 1. """, """ + declare foo1. !exists(Foo::new). Foo(a). Foo(foo1). """), Arguments.of(""" - node a. + declare a. class Foo. """, """ Foo(a). ?exists(a). scope Foo = 1, Foo += 1. """, """ + declare foo1. !exists(a). !exists(Foo::new). Foo(foo1). -- cgit v1.2.3-70-g09d2