From 7f149a36d7da605835ae79d1dab64e2c99cf34b0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 25 Feb 2022 08:03:46 -0800
Subject: [PATCH] refining model update rules for del_rule #5865 #5866

---
 src/muz/base/dl_util.cpp                  | 18 ++++++++++++------
 src/muz/base/dl_util.h                    |  2 +-
 src/muz/transforms/dl_mk_rule_inliner.cpp | 12 ++++++------
 3 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index eb832f93e..03a8f1c99 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -281,14 +281,19 @@ namespace datalog {
         return get_max_var(has_var);
     }
 
-    void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable) {
+    void del_rule(horn_subsume_model_converter* mc, rule& r, lbool unreachable) {
         if (mc) {
             ast_manager& m = mc->get_manager();
             expr_ref_vector body(m);
-            if (unreachable) {
+            TRACE("dl", tout << "unreachable: " << unreachable << " " << r.get_decl()->get_name() << "\n");
+            switch (unreachable) {
+            case l_true:
                 body.push_back(m.mk_true());
-            }
-            else {
+                break;
+            case l_false:
+                body.push_back(m.mk_false());
+                break;
+            default:
                 for (unsigned i = 0; i < r.get_tail_size(); ++i) {
                     if (r.is_neg_tail(i)) {
                         body.push_back(m.mk_not(r.get_tail(i)));
@@ -297,11 +302,12 @@ namespace datalog {
                         body.push_back(r.get_tail(i));
                     }
                 }
+                break;
             }
-            TRACE("dl_dr", 
+            TRACE("dl", 
                   tout << mk_pp(r.get_head(), m) << " :- \n";
                   for (unsigned i = 0; i < body.size(); ++i) {
-                      tout << mk_pp(body[i].get(), m) << "\n";
+                      tout << mk_pp(body.get(i), m) << "\n";
                   });
                       
             mc->insert(r.get_head(), body.size(), body.data());
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index 1b69a2733..565b58c84 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -353,7 +353,7 @@ namespace datalog {
         unsigned get_max_rule_var(const rule& r);
     };
 
-    void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable);
+    void del_rule(horn_subsume_model_converter* mc, rule& r, lbool unreachable);
 
     void resolve_rule(rule_manager& rm,
                       replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, 
diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index 1d4f05155..7b22b4133 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -410,7 +410,7 @@ namespace datalog {
         TRACE("dl", tout << "inlined rules after mutual inlining:\n" << m_inlined_rules;  );
 
         for (rule * r : m_inlined_rules) {
-            datalog::del_rule(m_mc, *r, false);
+            datalog::del_rule(m_mc, *r, l_undef);
         }
     }
 
@@ -449,7 +449,7 @@ namespace datalog {
             }
         }
         if (modified) {
-            datalog::del_rule(m_mc, *r0, true);
+            datalog::del_rule(m_mc, *r0, l_false);
         }
 
         return modified;
@@ -473,7 +473,7 @@ namespace datalog {
         if (something_done && m_mc) {
             for (rule* r : orig) {
                 if (inlining_allowed(orig, r->get_decl())) {
-                    datalog::del_rule(m_mc, *r, true);
+                    datalog::del_rule(m_mc, *r, l_undef);
                 }
             }
         }
@@ -558,7 +558,7 @@ namespace datalog {
                 // nothing unifies with the tail atom, therefore the rule is unsatisfiable
                 // (we can say this because relation pred doesn't have any ground facts either)
                 res = nullptr;
-                datalog::del_rule(m_mc, *r, false);
+                datalog::del_rule(m_mc, *r, l_false);
                 return true;
             }
             if (!is_oriented_rewriter(inlining_candidate, strat)) {
@@ -568,7 +568,7 @@ namespace datalog {
                 goto process_next_tail;
             }
             if (!try_to_inline_rule(*r, *inlining_candidate, ti, res)) {
-                datalog::del_rule(m_mc, *r, false);
+                datalog::del_rule(m_mc, *r, l_false);
                 res = nullptr;
             }
             return true;
@@ -801,7 +801,7 @@ namespace datalog {
                 if (num_tail_unifiers == 1) {
                     TRACE("dl", tout << "setting invalid: " << j << "\n";);
                     valid.set(j, false);
-                    datalog::del_rule(m_mc, *r2, true);
+                    datalog::del_rule(m_mc, *r2, l_true);
                     del_rule(r2, j);
                 }