From b79b8c9bc46ad2a90b21c8ed01ab2330d4bc0a51 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Apr 2020 15:08:28 -0700
Subject: [PATCH] fix #3777

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/dl_rule_transformer.cpp | 26 +++++++++-----------------
 src/muz/rel/dl_mk_explanations.cpp   | 16 +++++++++++-----
 src/muz/rel/dl_mk_explanations.h     |  2 ++
 3 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/src/muz/base/dl_rule_transformer.cpp b/src/muz/base/dl_rule_transformer.cpp
index c610d95b9..cc9269378 100644
--- a/src/muz/base/dl_rule_transformer.cpp
+++ b/src/muz/base/dl_rule_transformer.cpp
@@ -36,21 +36,15 @@ namespace datalog {
     }
 
     void rule_transformer::reset() {
-        plugin_vector::iterator it = m_plugins.begin();
-        plugin_vector::iterator end = m_plugins.end();
-        for(; it!=end; ++it) {            
-            dealloc(*it);
-        }
+        for (auto* p : m_plugins) 
+            dealloc(p);
         m_plugins.reset();
         m_dirty = false;
     }
 
     void rule_transformer::cancel() {
-        plugin_vector::iterator it = m_plugins.begin();
-        plugin_vector::iterator end = m_plugins.end();
-        for(; it!=end; ++it) {
-            (*it)->cancel();
-        }
+        for (auto* p : m_plugins) 
+            p->cancel();
     }
 
     struct rule_transformer::plugin_comparator {
@@ -69,7 +63,7 @@ namespace datalog {
     void rule_transformer::register_plugin(plugin * p) {
         m_plugins.push_back(p);
         p->attach(*this);
-        m_dirty=true;
+        m_dirty = true;
     }
 
     bool rule_transformer::operator()(rule_set & rules) {
@@ -81,7 +75,7 @@ namespace datalog {
             tout<<"init:\n";
             rules.display(tout);
         );
-        rule_set* new_rules = alloc(rule_set, rules);
+        scoped_ptr<rule_set> new_rules = alloc(rule_set, rules);      
         plugin_vector::iterator it = m_plugins.begin();
         plugin_vector::iterator end = m_plugins.end();
         for(; it!=end && !m_context.canceled(); ++it) {
@@ -91,7 +85,7 @@ namespace datalog {
             IF_VERBOSE(1, verbose_stream() << "(transform " << typeid(p).name() << "...";);
             stopwatch sw;
             sw.start();
-            rule_set * new_rules1 = p(*new_rules);
+            scoped_ptr<rule_set> new_rules1 = p(*new_rules);
             sw.stop();
             double sec = sw.get_seconds();
             if (sec < 0.001) sec = 0.0;
@@ -104,13 +98,12 @@ namespace datalog {
                 !new_rules1->close()) {
                 warning_msg("a rule transformation skipped "
                             "because it destratified negation");
-                dealloc(new_rules1);
+                new_rules1 = nullptr;
                 IF_VERBOSE(1, verbose_stream() << "no-op " << sec << "s)\n";);
                 continue;
             }
             modified = true;
-            dealloc(new_rules);
-            new_rules = new_rules1;
+            new_rules = new_rules1.detach();
             new_rules->ensure_closed();
 
             IF_VERBOSE(1, verbose_stream() << new_rules->get_num_rules() << " rules " << sec << "s)\n";);
@@ -122,7 +115,6 @@ namespace datalog {
         if (modified) {
             rules.replace_rules(*new_rules);
         }
-        dealloc(new_rules);
         return modified;
     }
 
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index 5aa2b54c9..f10cdd87b 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -628,6 +628,9 @@ namespace datalog {
         );
     }
 
+    mk_explanations::~mk_explanations() {
+    }
+
     func_decl * mk_explanations::get_union_decl(context & ctx) {
         ast_manager & m = ctx.get_manager();
         sort_ref s(ctx.get_decl_util().mk_rule_sort(), m);
@@ -669,7 +672,7 @@ namespace datalog {
 
     func_decl * mk_explanations::get_e_decl(func_decl * orig_decl) {
         decl_map::obj_map_entry * e = m_e_decl_map.insert_if_not_there2(orig_decl, 0);
-        if (e->get_data().m_value==0) {
+        if (e->get_data().m_value == nullptr) {
             relation_signature e_domain;
             e_domain.append(orig_decl->get_arity(), orig_decl->get_domain());
             e_domain.push_back(m_e_sort);
@@ -790,8 +793,11 @@ namespace datalog {
 
         product_relation & prod_rel = static_cast<product_relation &>(e_rel);
         SASSERT(prod_rel.size()==2);
-        SASSERT(prod_rel[0].get_plugin().is_sieve_relation());
-        SASSERT(prod_rel[1].get_plugin().is_sieve_relation());
+       
+        if (!prod_rel[0].get_plugin().is_sieve_relation())
+            throw default_exception("explanations are not supported for this query");
+        if (!prod_rel[1].get_plugin().is_sieve_relation())
+            throw default_exception("explanations are not supported for this query");
         sieve_relation * srels[] = { 
             static_cast<sieve_relation *>(&prod_rel[0]),
             static_cast<sieve_relation *>(&prod_rel[1]) };
@@ -876,10 +882,10 @@ namespace datalog {
         if (!m_context.generate_explanations()) {
             return nullptr;
         }
-        rule_set * res = alloc(rule_set, m_context);
+        scoped_ptr<rule_set> res = alloc(rule_set, m_context);
         transform_facts(m_context.get_rel_context()->get_rmanager(), source, *res);
         transform_rules(source, *res);
-        return res;
+        return res.detach();
     }
     
 };
diff --git a/src/muz/rel/dl_mk_explanations.h b/src/muz/rel/dl_mk_explanations.h
index a96d50cb3..47f5f2bed 100644
--- a/src/muz/rel/dl_mk_explanations.h
+++ b/src/muz/rel/dl_mk_explanations.h
@@ -66,6 +66,8 @@ namespace datalog {
         */
         mk_explanations(context & ctx);
 
+        ~mk_explanations() override;
+
         /**
            \brief Return explanation predicate that corresponds to \c orig_decl.
         */