revisited issue #64 and #98, for termination properties of the restri…

…cted chase
karmaresearch · Nov 23, 2022 · cbdf98b · cbdf98b
1 parent cfc7b0d
commit cbdf98b
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/vlog/common/concepts.cpp b/src/vlog/common/concepts.cpp
@@ -1471,6 +1471,11 @@ void Program::rewriteRule(std::vector<Literal> &lHeads, std::vector<Literal> &lB
     std::vector<Literal> nh;
     nh.push_back(newHead);
     addRule(nh, lBody);
+    if (allrules[allrules.size() - 1].isExistential()) {
+        // if the rule just added is existential, also add "2-way atomic decomposition", to fix termination
+        // properties of the restricted chase.
+        addRule(nh, lHeads);
+    }
 
     // Then, for each original head, create a rule with the generated head as body.
     for (auto h : lHeads) {