Merge pull request #2150 from b-scholz/subsumption_fix

Subsumption fix #2145
souffle-lang · Dec 8, 2021 · 244cb07 · 244cb07
2 parents 0a4dd3a + 5bef4c1
commit 244cb07
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 28 deletions.
diff --git a/src/ast2ram/seminaive/ClauseTranslator.cpp b/src/ast2ram/seminaive/ClauseTranslator.cpp
@@ -139,8 +139,8 @@ std::string ClauseTranslator::getClauseAtomName(const ast::Clause& clause, const
     if (isA<ast::SubsumptiveClause>(clause)) {
         // find the dominated / dominating heads
         const auto& body = clause.getBodyLiterals();
-        auto dominatedHeadAtom = dynamic_cast<const ast::Atom*>(body[dominatedHead]);
-        auto dominatingHeadAtom = dynamic_cast<const ast::Atom*>(body[dominatingHead]);
+        auto dominatedHeadAtom = dynamic_cast<const ast::Atom*>(body[0]);
+        auto dominatingHeadAtom = dynamic_cast<const ast::Atom*>(body[1]);
 
         if (clause.getHead() == atom) {
             if (mode == SubsumeDeleteCurrentDelta || mode == SubsumeDeleteCurrentCurrent) {
@@ -535,8 +535,8 @@ Own<ram::Operation> ClauseTranslator::addBodyLiteralConstraints(
         if (mode == SubsumeRejectNewNew || mode == SubsumeDeleteCurrentCurrent) {
             // find the dominated / dominating heads
             const auto& body = clause.getBodyLiterals();
-            auto dominatedHeadAtom = dynamic_cast<const ast::Atom*>(body[dominatedHead]);
-            auto dominatingHeadAtom = dynamic_cast<const ast::Atom*>(body[dominatingHead]);
+            auto dominatedHeadAtom = dynamic_cast<const ast::Atom*>(body[0]);
+            auto dominatingHeadAtom = dynamic_cast<const ast::Atom*>(body[1]);
             op = addDistinct(std::move(op), dominatedHeadAtom, dominatingHeadAtom);
         }
         return op;
@@ -686,12 +686,6 @@ Own<ram::Condition> ClauseTranslator::getFunctionalDependencies(const ast::Claus
 }
 
 std::vector<ast::Atom*> ClauseTranslator::getAtomOrdering(const ast::Clause& clause) const {
-    // set dominating/dominated head of clause
-    if (isA<ast::SubsumptiveClause>(clause)) {
-        dominatedHead = 0;
-        dominatingHead = 1;
-    }
-
     auto atoms = ast::getBodyLiterals<ast::Atom>(clause);
 
     const auto& plan = clause.getExecutionPlan();
@@ -709,23 +703,8 @@ std::vector<ast::Atom*> ClauseTranslator::getAtomOrdering(const ast::Clause& cla
     const auto& order = orders.at(version);
     auto sz = order->getOrder().size();
     std::vector<unsigned int> newOrder(sz);
-
     std::transform(order->getOrder().begin(), order->getOrder().end(), newOrder.begin(),
             [](unsigned int i) -> unsigned int { return i - 1; });
-
-    // assign dominatedHead/dominatingHead index in case
-    // a query plan has been specified for a subsumptive
-    // clause.
-    if (isA<ast::SubsumptiveClause>(clause)) {
-        for (std::size_t i = 0; i < sz; ++i) {
-            if (order->getOrder()[i] == 0) {
-                dominatedHead = newOrder[0];
-            } else if (order->getOrder()[i] == 1) {
-                dominatingHead = newOrder[1];
-            }
-        }
-    }
-
     return reorderAtoms(atoms, newOrder);
 }
 

diff --git a/src/ast2ram/seminaive/ClauseTranslator.h b/src/ast2ram/seminaive/ClauseTranslator.h
@@ -133,9 +133,6 @@ class ClauseTranslator : public ast2ram::ClauseTranslator {
 private:
     std::vector<const ast::Argument*> generators;
     std::vector<const ast::Node*> operators;
-
-    // Index of dominated/dominating heads in a subsumptive clause
-    mutable int dominatedHead{0}, dominatingHead{1};
 };
 
 }  // namespace souffle::ast2ram::seminaive
diff --git a/tests/semantic/subsumption_multiple_rules/C.csv b/tests/semantic/subsumption_multiple_rules/C.csv
@@ -0,0 +1 @@
+1
diff --git a/tests/semantic/subsumption_multiple_rules/subsumption_multiple_rules.dl b/tests/semantic/subsumption_multiple_rules/subsumption_multiple_rules.dl
@@ -50,3 +50,14 @@ eql(2, 3).
 rel(a, b) <= rel(c, d) :- eql(a, c), eql(b, d), a <= c, b <= d.
 
 .output rel
+
+// check query plan
+.decl C(x:number) btree_delete
+.decl D(x:number, y:number)
+C(1).
+D(1, 1).
+C(x1) <= C(x2) :-
+    D(x1, x2),
+    x1 <= x2.
+    .plan 0:(1,3,2)
+.output C