Fix PartitionBodyLiteralsTransformer with subsumptive clause

quentin · quentin · commit 0447ecd020cf · 2025-11-04T17:01:27.000+01:00
The `PartitionBodyLiteralsTransformer` did not handle subsumptive clauses and treated them as normal clause. It's a design flaw of `SubsumptiveClause` being a subclass of `Clause`. Similar issue could happen for any transformation that rewrites a `Clause`. fix #2551
diff --git a/src/ast/SubsumptiveClause.h b/src/ast/SubsumptiveClause.h
@@ -34,6 +34,10 @@ namespace souffle::ast {
  * Format:
  *     A(x1,...) <= A(y1,...) :- <Body> .
  *
+ *
+ * Internally the least and greatest atoms of the rule's head are added to the clause body literals at
+ * index `0` and `1` in `bodyLiterals`. The least atom of the rule's head is stored in the `head`.
+ *
  */
 class SubsumptiveClause : public Clause {
 public:
diff --git a/src/ast/transform/PartitionBodyLiterals.cpp b/src/ast/transform/PartitionBodyLiterals.cpp
@@ -70,6 +70,8 @@ bool PartitionBodyLiteralsTransformer::transform(TranslationUnit& translationUni
         Graph<std::string> variableGraph = Graph<std::string>();
         std::set<std::string> ruleVariables;
 
+        const bool isSubsumption = isA<SubsumptiveClause>(clause);
+
         // Add in the nodes
         // The nodes of G are the variables in the rule
         visit(clause, [&](const ast::Variable& var) {
@@ -110,6 +112,26 @@ bool PartitionBodyLiteralsTransformer::transform(TranslationUnit& translationUni
         std::set<std::string> headComponent;
         visit(*clause.getHead(), [&](const ast::Variable& var) { headComponent.insert(var.getName()); });
 
+        if (isSubsumption) {
+            // this works because subsumptive clause first two literals are the least and greatest atoms
+            // of the original clause's head: `A(least, ... ) <= A(greatest, ...) :- ...`.
+            std::set<std::string> leastAtomVariables;
+            std::set<std::string> greatestAtomVariables;
+            visit(literalsToConsider[0],
+                    [&](const ast::Variable& var) { leastAtomVariables.insert(var.getName()); });
+            visit(literalsToConsider[1],
+                    [&](const ast::Variable& var) { greatestAtomVariables.insert(var.getName()); });
+            // Create edge between any couple of variables taken respectively from the least and greatest
+            // atoms: `least <-> greatest`, since in the previous step of the algorithm we already linked
+            // variables within each atom.
+            if (!(leastAtomVariables.empty() || greatestAtomVariables.empty())) {
+                const auto vL = *leastAtomVariables.begin();
+                const auto vG = *greatestAtomVariables.begin();
+                variableGraph.insert(vL, vG);
+                variableGraph.insert(vG, vL);
+            }
+        }
+
         if (!headComponent.empty()) {
             variableGraph.visit(*headComponent.begin(), [&](const std::string& var) {
                 headComponent.insert(var);
@@ -181,10 +203,17 @@ bool PartitionBodyLiteralsTransformer::transform(TranslationUnit& translationUni
             clausesToAdd.push_back(std::move(disconnectedClause));
         }
 
-        // Create the replacement clause
-        // a(x) <- b(x), c(y), d(z). --> a(x) <- newrel0(), newrel1(), b(x).
-        auto replacementClause =
-                mk<Clause>(clone(clause.getHead()), std::move(replacementAtoms), nullptr, clause.getSrcLoc());
+        // Create the replacement clause. The original literals must appear first and in order to
+        // satisfy the SubsumptiveClause invariants.
+        //
+        // `a(x) <- b(x), c(y), d(z). --> a(x) <- b(x), newrel0(), newrel1().`
+        Clause* replacementClause;
+        if (isSubsumption) {
+            replacementClause =
+                    new SubsumptiveClause(clone(clause.getHead()), {}, nullptr, clause.getSrcLoc());
+        } else {
+            replacementClause = new Clause(clone(clause.getHead()), {}, nullptr, clause.getSrcLoc());
+        }
 
         // Add the remaining body literals to the clause
         for (Literal* bodyLiteral : clause.getBodyLiterals()) {
@@ -201,9 +230,11 @@ bool PartitionBodyLiteralsTransformer::transform(TranslationUnit& translationUni
             }
         }
 
+        replacementClause->addToBody(std::move(replacementAtoms));
+
         // Replace the old clause with the new one
         clausesToRemove.push_back(&clause);
-        clausesToAdd.push_back(std::move(replacementClause));
+        clausesToAdd.push_back(std::unique_ptr<Clause>(replacementClause));
     });
 
     // Adjust the program
diff --git a/src/ast/transform/SubsumptionQualifier.cpp b/src/ast/transform/SubsumptionQualifier.cpp
@@ -72,6 +72,7 @@ bool SubsumptionQualifierTransformer::transform(TranslationUnit& translationUnit
         // rewrite relation representation
         if (relation->getRepresentation() == RelationRepresentation::DEFAULT && hasSubsumptiveRule) {
             relation->setRepresentation(RelationRepresentation::BTREE_DELETE);
+            changed = true;
         }
     }
     return changed;
diff --git a/tests/evaluation/CMakeLists.txt b/tests/evaluation/CMakeLists.txt
@@ -165,3 +165,4 @@ positive_test(issue2160)
 add_subdirectory(issue2508)
 souffle_positive_functor_test(issue2508 CATEGORY evaluation)
 positive_test(issue2532)
+positive_test(issue2551)
diff --git a/tests/evaluation/issue2551/issue2551.dl b/tests/evaluation/issue2551/issue2551.dl
@@ -0,0 +1,11 @@
+.decl m(s: number)
+.output r
+.decl r(s: number)
+.output m
+r(1).
+m(1).
+m(2).
+// m = {1,2} before subsumption, and then expect m = {1} because
+// m(2) is subsumed by m(1):
+//    m(2) <= m(1) :- !r(2), m(1).
+m(x) <= m(y) :- !r(x), m(y).
diff --git a/tests/evaluation/issue2551/issue2551.err b/tests/evaluation/issue2551/issue2551.err
diff --git a/tests/evaluation/issue2551/issue2551.out b/tests/evaluation/issue2551/issue2551.out
diff --git a/tests/evaluation/issue2551/m.csv b/tests/evaluation/issue2551/m.csv
@@ -0,0 +1 @@
+1
diff --git a/tests/evaluation/issue2551/r.csv b/tests/evaluation/issue2551/r.csv
@@ -0,0 +1 @@
+1

Original file line number	Diff line number	Diff line change
`@@ -72,6 +72,7 @@ bool SubsumptionQualifierTransformer::transform(TranslationUnit& translationUnit`
`72`	`72`	`// rewrite relation representation`
`73`	`73`	`if (relation->getRepresentation() == RelationRepresentation::DEFAULT && hasSubsumptiveRule) {`
`74`	`74`	`relation->setRepresentation(RelationRepresentation::BTREE_DELETE);`
	`75`	`+ changed = true;`
`75`	`76`	`}`
`76`	`77`	`}`
`77`	`78`	`return changed;`