From cbdf98b1074f8952daf6da4a2949e29513a3f6f4 Mon Sep 17 00:00:00 2001
From: Ceriel Jacobs <c.j.h.jacobs@vu.nl>
Date: Wed, 23 Nov 2022 19:29:39 +0100
Subject: [PATCH] revisited issue #64 and #98, for termination properties of
 the restricted chase

---
 src/vlog/common/concepts.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/vlog/common/concepts.cpp b/src/vlog/common/concepts.cpp
index 08eb41f1..6f84d42f 100644
--- 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) {