From 35f184a6b9d4f132ac6f1da1a8dce7d461a98959 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Apr 2020 14:39:54 -0700
Subject: [PATCH] fix #3826

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/model_core.cpp                |  7 +-
 src/muz/base/dl_engine_base.h           |  3 +-
 src/muz/base/dl_rule.cpp                |  1 -
 src/muz/base/dl_rule_set.cpp            | 65 +++++++-----------
 src/muz/base/dl_util.h                  | 88 ++++++++++++-------------
 src/muz/fp/horn_tactic.cpp              | 19 ++----
 src/muz/rel/dl_relation_manager.cpp     |  8 +++
 src/muz/rel/dl_relation_manager.h       |  3 +-
 src/muz/rel/rel_context.cpp             | 23 ++++---
 src/muz/rel/rel_context.h               |  2 +
 src/muz/transforms/dl_mk_coi_filter.cpp |  3 +-
 11 files changed, 108 insertions(+), 114 deletions(-)

diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index 08c57f437..a3b88b291 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -47,7 +47,12 @@ bool model_core::eval(func_decl* f, expr_ref & r) const {
 }
 
 void model_core::register_decl(func_decl * d, expr * v) {
-    SASSERT(d->get_arity() == 0);
+    if (d->get_arity() > 0) {
+        func_interp* fi = alloc(func_interp, m, d->get_arity());
+        fi->set_else(v);
+        register_decl(d, fi);
+        return;
+    }
     TRACE("model", tout << "register " << d->get_name() << "\n";
           if (v) tout << mk_pp(v, m) << "\n";
           );
diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h
index 2a5b91387..0caed35e5 100644
--- a/src/muz/base/dl_engine_base.h
+++ b/src/muz/base/dl_engine_base.h
@@ -96,8 +96,9 @@ namespace datalog {
             throw default_exception(std::string("certificates are not supported for ") + m_name);
         }
         virtual model_ref get_model() {
-            return model_ref(alloc(model, m));
+            return model_ref();
         }
+
         virtual void get_rules_along_trace (rule_ref_vector& rules) {
             throw default_exception(std::string("get_rules_along_trace is not supported for ") + m_name);
         }
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 40b7df07d..5b8e1c733 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -1019,7 +1019,6 @@ namespace datalog {
     void rule::display(context & ctx, std::ostream & out) const {
         ast_manager & m = ctx.get_manager();
         out << m_name.str () << ":\n";
-        //out << mk_pp(m_head, m);
         output_predicate(ctx, m_head, out);
         if (m_tail_size == 0) {
             out << ".\n";
diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index 829aa0103..04f50a53e 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -188,12 +188,10 @@ namespace datalog {
         unsigned curr_index = init_len;
         rule_dependencies reversed(*this, true);
 
-        iterator pit = begin();
-        iterator pend = end();
-        for (; pit!=pend; ++pit) {
-            func_decl * pred = pit->m_key;
+        for (auto& kv : *this) {
+            func_decl * pred = kv.m_key;
             unsigned deg = in_degree(pred);
-            if (deg==0) {
+            if (deg == 0) {
                 res.push_back(pred);
             }
             else {
@@ -201,13 +199,10 @@ namespace datalog {
             }
         }
 
-        while (curr_index<res.size()) { //res.size() can change in the loop iteration
+        while (curr_index < res.size()) { //res.size() can change in the loop iteration
             func_decl * curr = res[curr_index];
             const item_set & children = reversed.get_deps(curr);
-            item_set::iterator cit = children.begin();
-            item_set::iterator cend = children.end();
-            for (; cit!=cend; ++cit) {
-                func_decl * child = *cit;
+            for (func_decl * child : children) {
                 deg_map::obj_map_entry * e = degs.find_core(child);
                 SASSERT(e);
                 unsigned & child_deg = e->get_data().m_value;
@@ -227,20 +222,14 @@ namespace datalog {
         return true;
     }
 
-    void rule_dependencies::display(std::ostream & out ) const
-    {
-        iterator pit = begin();
-        iterator pend = end();
-        for (; pit != pend; ++pit) {
-            func_decl * pred = pit->m_key;
-            const item_set & deps = *pit->m_value;
-            item_set::iterator dit=deps.begin();
-            item_set::iterator dend=deps.end();
-            if (dit == dend) {
-                out<<pred->get_name()<<" - <none>\n";
+    void rule_dependencies::display(std::ostream & out ) const {
+        for (auto const& kv : *this) {
+            func_decl * pred = kv.m_key;
+            const item_set & deps = *kv.m_value;
+            if (deps.empty()) {
+                out << pred->get_name()<<" - <none>\n";
             }
-            for (; dit != dend; ++dit) {
-                func_decl * dep = *dit;
+            for (func_decl* dep : deps) {
                 out << pred->get_name() << " -> " << dep->get_name() << "\n";
             }
         }
@@ -473,9 +462,8 @@ namespace datalog {
         bool change = true;
         while (change) {
             change = false;
-            func_decl_set::iterator it = non_founded.begin(), end = non_founded.end();
-            for (; it != end; ++it) {
-                rule_vector const& rv = get_predicate_rules(*it);
+            for (func_decl * f : non_founded) {
+                rule_vector const& rv = get_predicate_rules(f);
                 bool found = false;
                 for (unsigned i = 0; !found && i < rv.size(); ++i) {
                     rule const& r = *rv[i];
@@ -484,8 +472,8 @@ namespace datalog {
                         is_founded = founded.contains(r.get_decl(j));
                     }
                     if (is_founded) {
-                        founded.insert(*it);
-                        non_founded.remove(*it);
+                        founded.insert(f);
+                        non_founded.remove(f);
                         change = true;
                         found  = true;
                     }
@@ -497,19 +485,12 @@ namespace datalog {
     void rule_set::display(std::ostream & out) const {
         out << "; rule count: " << get_num_rules() << "\n";
         out << "; predicate count: " << m_head2rules.size() << "\n";
-        func_decl_set::iterator pit = m_output_preds.begin();
-        func_decl_set::iterator pend = m_output_preds.end();
-        for (; pit != pend; ++pit) {
-            out << "; output: " << (*pit)->get_name() << '\n';
+        for (func_decl * f : m_output_preds) {
+            out << "; output: " << f->get_name() << '\n';
         }
-        decl2rules::iterator it  = m_head2rules.begin();
-        decl2rules::iterator end = m_head2rules.end();
-        for (; it != end; ++it) {
-            ptr_vector<rule> * rules = it->m_value;
-            ptr_vector<rule>::iterator it2  = rules->begin();
-            ptr_vector<rule>::iterator end2 = rules->end();
-            for (; it2 != end2; ++it2) {
-                rule * r = *it2;
+        for (auto const& kv : m_head2rules) {
+            ptr_vector<rule> * rules = kv.m_value;
+            for (rule* r : *rules) {
                 if (!r->passes_output_thresholds(m_context)) {
                     continue;
                 }
@@ -722,8 +703,8 @@ namespace datalog {
     void rule_stratifier::display(std::ostream& out) const {
         m_deps.display(out << "dependencies\n");
         out << "strata\n";
-        for (unsigned i = 0; i < m_strats.size(); ++i) {
-            for (auto * item : *m_strats[i]) {
+        for (auto * s : m_strats) {
+            for (auto * item : *s) {
                 out << item->get_name() << " ";
             }
             out << "\n";
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index 7e38b9e9f..b17bc2417 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -88,7 +88,7 @@ namespace datalog {
         for (unsigned i = 0; i < n; i++) {
             expr * arg = src->get_arg(i);
             if (!is_var(arg)) {
-                tgt[i]=arg;
+                tgt[i] = arg;
             }
         }
     }
@@ -168,12 +168,12 @@ namespace datalog {
         }
 
         bool empty() const {
-            return size()==0;
+            return size() == 0;
         }
 
         void get(unsigned i, unsigned & index1, unsigned & index2) const {
-            index1=m_args1[i];
-            index2=m_args2[i];
+            index1 = m_args1[i];
+            index2 = m_args2[i];
         }
 
         void reset() {
@@ -192,11 +192,11 @@ namespace datalog {
         */
         template<typename T>
         void fill_into_second(const app * f1, T & tgt) const {
-            unsigned n=size();
-            for(unsigned i=0; i<n; i++) {
+            unsigned n = size();
+            for (unsigned i = 0; i < n; i++) {
                 unsigned f1_index, tgt_index;
                 get(i, f1_index, tgt_index);
-                tgt[tgt_index]=f1->get_arg(f1_index);
+                tgt[tgt_index] = f1->get_arg(f1_index);
             }
         }
 
@@ -216,19 +216,19 @@ namespace datalog {
             //TODO: optimize number of checks when variable occurs multiple times
             unsigned a1num = expr_cont_get_size(a1);
             unsigned a2num = expr_cont_get_size(a2);
-            for(unsigned i1=0; i1<a1num; i1++) {
-                expr * e1=expr_cont_get(a1,i1);
-                if(!is_var(e1)) {
+            for (unsigned i1 = 0; i1<a1num; i1++) {
+                expr * e1 = expr_cont_get(a1,i1);
+                if (!is_var(e1)) {
                     continue;
                 }
-                var* v1=to_var(e1);
-                for(unsigned i2=0; i2<a2num; i2++) {
-                    expr * e2=expr_cont_get(a2,i2);
-                    if(!is_var(e2)) {
+                var* v1 = to_var(e1);
+                for (unsigned i2 = 0; i2<a2num; i2++) {
+                    expr * e2 = expr_cont_get(a2,i2);
+                    if (!is_var(e2)) {
                         continue;
                     }
-                    var* v2=to_var(e2);
-                    if(v1->get_idx()==v2->get_idx()) {
+                    var* v2 = to_var(e2);
+                    if (v1->get_idx() == v2->get_idx()) {
                         add_pair(i1, i2);
                     }
                 }
@@ -244,14 +244,14 @@ namespace datalog {
 
     template<class T>
     void project_out_vector_columns(T & container, unsigned removed_col_cnt, const unsigned * removed_cols) {
-        if(removed_col_cnt==0) {
+        if (removed_col_cnt==0) {
             return;
         }
         unsigned n = container.size();
         unsigned ofs = 1;
         unsigned r_i = 1;
-        for(unsigned i=removed_cols[0]+1; i<n; i++) {
-            if(r_i!=removed_col_cnt && removed_cols[r_i]==i) {
+        for (unsigned i=removed_cols[0]+1; i<n; i++) {
+            if (r_i!=removed_col_cnt && removed_cols[r_i]==i) {
                 r_i++;
                 ofs++;
                 continue;
@@ -271,14 +271,14 @@ namespace datalog {
     template<class T, class M>
     void project_out_vector_columns(ref_vector<T,M> & container, unsigned removed_col_cnt, 
             const unsigned * removed_cols) {
-        if(removed_col_cnt==0) {
+        if (removed_col_cnt==0) {
             return;
         }
         unsigned n = container.size();
         unsigned ofs = 1;
         unsigned r_i = 1;
-        for(unsigned i=removed_cols[0]+1; i<n; i++) {
-            if(r_i!=removed_col_cnt && removed_cols[r_i]==i) {
+        for (unsigned i=removed_cols[0]+1; i<n; i++) {
+            if (r_i!=removed_col_cnt && removed_cols[r_i]==i) {
                 r_i++;
                 ofs++;
                 continue;
@@ -319,11 +319,11 @@ namespace datalog {
 
     template<class T>
     void permutate_by_cycle(T & container, unsigned cycle_len, const unsigned * permutation_cycle) {
-        if(cycle_len<2) {
+        if (cycle_len<2) {
             return;
         }
         typename T::data aux = container[permutation_cycle[0]];
-        for(unsigned i=1; i<cycle_len; i++) {
+        for (unsigned i=1; i<cycle_len; i++) {
             container[permutation_cycle[i-1]]=container[permutation_cycle[i]];
         }
         container[permutation_cycle[cycle_len-1]]=aux;
@@ -331,11 +331,11 @@ namespace datalog {
 
     template<class T, class M>
     void permutate_by_cycle(ref_vector<T,M> & container, unsigned cycle_len, const unsigned * permutation_cycle) {
-        if(cycle_len<2) {
+        if (cycle_len<2) {
             return;
         }
         T * aux = container.get(permutation_cycle[0]);
-        for(unsigned i=1; i<cycle_len; i++) {
+        for (unsigned i=1; i<cycle_len; i++) {
             container.set(permutation_cycle[i-1], container.get(permutation_cycle[i]));
         }
         container.set(permutation_cycle[cycle_len-1], aux);
@@ -385,14 +385,14 @@ namespace datalog {
 
     template<class T, class U>
     bool vectors_equal(const T & c1, const U & c2) {
-        if(c1.size()!=c2.size()) {
+        if (c1.size()!=c2.size()) {
             return false;
         }
         typename T::data * it1 = c1.c_ptr();
         typename T::data * end1 = c1.c_ptr()+c1.size();
         typename U::data * it2 = c2.c_ptr();
-        for(; it1!=end1; ++it1, ++it2) {
-            if(*it1!=*it2) { 
+        for (; it1!=end1; ++it1, ++it2) {
+            if (*it1!=*it2) { 
                 return false;
             }
         }
@@ -436,7 +436,7 @@ namespace datalog {
     void dealloc_ptr_vector_content(ptr_vector<T> & v) {
         typename ptr_vector<T>::iterator it = v.begin();
         typename ptr_vector<T>::iterator end = v.end();
-        for(; it!=end; ++it) {
+        for (; it!=end; ++it) {
             dealloc(*it);
         }
     }
@@ -448,7 +448,7 @@ namespace datalog {
     void push_into_vector(VectType & vector, const U & src) {
         typename U::iterator it = src.begin();
         typename U::iterator end = src.end();
-        for(; it!=end; ++it) {
+        for (; it!=end; ++it) {
             vector.push_back(*it);
         }
     }
@@ -457,7 +457,7 @@ namespace datalog {
     void push_into_vector(VectType & vector, const ref_vector<U,M> & src) {
         U * const * it = src.begin();
         U * const * end = src.end();
-        for(; it!=end; ++it) {
+        for (; it!=end; ++it) {
             vector.push_back(*it);
         }
     }
@@ -466,7 +466,7 @@ namespace datalog {
     void insert_into_set(SetType & tgt, const U & src) {
         typename U::const_iterator it = src.begin();
         typename U::const_iterator end = src.end();
-        for(; it!=end; ++it) {
+        for (; it!=end; ++it) {
             tgt.insert(*it);
         }
     }
@@ -480,8 +480,8 @@ namespace datalog {
     template<class T>
     bool remove_from_vector(T & v, const typename T::data & el) {
         unsigned sz = v.size();
-        for(unsigned i=0; i<sz; i++) {
-            if(v[i]==el) {
+        for (unsigned i=0; i<sz; i++) {
+            if (v[i]==el) {
                 std::swap(v[i], v.back());
                 v.pop_back();
                 return true;
@@ -515,28 +515,28 @@ namespace datalog {
 
     template<class T, class U>
     void sort_two_arrays(unsigned len, T* keys, U* vals) {
-        if(len<2) {
+        if (len<2) {
             return;
         }
-        if(len==2) {
-            if(keys[0]>keys[1]) {
+        if (len==2) {
+            if (keys[0]>keys[1]) {
                 std::swap(keys[0], keys[1]);
                 std::swap(vals[0], vals[1]);
             }
             return;
         }
         unsigned_vector numbers;
-        for(unsigned i=0; i<len; i++) {
+        for (unsigned i=0; i<len; i++) {
             numbers.push_back(i);
         }
         aux__index_comparator<T> cmp(keys);
         std::sort(numbers.begin(), numbers.end(), cmp);
-        for(unsigned i=0; i<len; i++) {
+        for (unsigned i=0; i<len; i++) {
             unsigned prev_i = i;
-            for(;;) {
+            for (;;) {
                 unsigned src_i = numbers[prev_i];
                 numbers[prev_i]=prev_i;
-                if(src_i==i) {
+                if (src_i==i) {
                     break;
                 }
                 std::swap(keys[prev_i], keys[src_i]);
@@ -565,8 +565,8 @@ namespace datalog {
     template<class Container>
     void add_sequence_without_set(unsigned start, unsigned count, const Container & complement, unsigned_vector & v) {
         unsigned after_last = start+count;
-        for(unsigned i=start; i<after_last; i++) {
-            if(!complement.contains(i)) {
+        for (unsigned i=start; i<after_last; i++) {
+            if (!complement.contains(i)) {
                 v.push_back(i);
             }
         }
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 4077bc7c5..dd63b81ae 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -283,13 +283,8 @@ class horn_tactic : public tactic {
                 g->reset();
                 if (produce_models) {
                     model_ref md = m_ctx.get_model();
-                    model_converter_ref mc2 = model2model_converter(&*md);
-                    if (mc) {
-                        mc = concat(mc.get(), mc2.get());
-                    }
-                    else {
-                        mc = mc2;
-                    }
+                    model_converter_ref mc2 = model2model_converter(md.get());
+                    mc = concat(mc.get(), mc2.get());
                 }
                 break;
             }
@@ -314,14 +309,12 @@ class horn_tactic : public tactic {
         }
 
         void simplify(expr* q,
-                    goal_ref const& g,
-                    goal_ref_buffer & result,
-                    model_converter_ref & mc,
-                    proof_converter_ref & pc) {
+                      goal_ref const& g,
+                      goal_ref_buffer & result,
+                      model_converter_ref & mc,
+                      proof_converter_ref & pc) {
 
             expr_ref fml(m);
-
-
             func_decl* query_pred = to_app(q)->get_decl();
             m_ctx.set_output_predicate(query_pred);
             m_ctx.get_rules(); // flush adding rules.
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 89f7fdda3..48196e874 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -115,6 +115,14 @@ namespace datalog {
         e->get_data().m_value = rel;
     }
 
+    decl_set relation_manager::collect_predicates() const {
+        decl_set res;
+        for (auto const& kv : m_relations) {
+            res.insert(kv.m_key);
+        }
+        return res;
+    }
+
     void relation_manager::collect_non_empty_predicates(decl_set & res) const {
         for (auto const& kv : m_relations) {
             if (!kv.m_value->fast_empty()) {
diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h
index f81785332..0fd92b3a7 100644
--- a/src/muz/rel/dl_relation_manager.h
+++ b/src/muz/rel/dl_relation_manager.h
@@ -115,7 +115,7 @@ namespace datalog {
           m_next_relation_fid(0) {}
 
         virtual ~relation_manager();
-
+        
         void reset();
         void reset_relations();
 
@@ -155,6 +155,7 @@ namespace datalog {
             }
         }
 
+        decl_set collect_predicates() const;
         void collect_non_empty_predicates(decl_set & res) const;
         void restrict_predicates(const decl_set & preds);
 
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index 047b2224e..a6ab5411c 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -257,16 +257,6 @@ namespace datalog {
                     is_approx = true;
                 }
                 rel.to_formula(e);
-#if 0
-                // Alternative format: 
-                // List the signature of the relation as 
-                // part of the answer.
-                expr_ref_vector args(m);
-                for (unsigned j = 0; j < q->get_arity(); ++j) {
-                    args.push_back(m.mk_var(j, q->get_domain(j)));
-                }
-                e = m.mk_implies(m.mk_app(q, args.size(), args.c_ptr()), e);
-#endif
                 ans.push_back(e);
             }
             SASSERT(!m_last_result_relation);
@@ -294,6 +284,19 @@ namespace datalog {
         return res;
     }
 
+    model_ref rel_context::get_model() {
+        model_ref md = alloc(model, m);
+        auto& rm = get_rmanager();
+        func_decl_set decls = rm.collect_predicates();
+        expr_ref fml(m);
+        for (func_decl* p : decls) {
+            rm.get_relation(p).to_formula(fml);
+            md->register_decl(p, fml);
+        }
+        (*m_context.get_model_converter())(md);
+        return md;
+    }
+
     void rel_context::transform_rules() {
         rule_transformer transf(m_context);
         transf.register_plugin(alloc(mk_coi_filter, m_context));
diff --git a/src/muz/rel/rel_context.h b/src/muz/rel/rel_context.h
index dbcc42248..be8638ff6 100644
--- a/src/muz/rel/rel_context.h
+++ b/src/muz/rel/rel_context.h
@@ -91,6 +91,8 @@ namespace datalog {
 
         void transform_rules() override;
 
+        model_ref get_model() override;
+
         bool try_get_size(func_decl* pred, unsigned& rel_size) const override;
         /**
            \brief query result if it contains fact.
diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index dc1f7ba1a..8c34325a4 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/src/muz/transforms/dl_mk_coi_filter.cpp
@@ -104,13 +104,14 @@ namespace datalog {
             generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl_coi");
             for (auto const& kv : engine) {
                 if (!kv.m_value.is_reachable()) {
-                    mc0->add(kv.m_key, m.mk_false());
+                    unreachable.insert(kv.m_key);
                 }
             }
             for (func_decl* f : unreachable) {
                 mc0->add(f, m.mk_false());
             }
             m_context.add_model_converter(mc0);
+            TRACE("dl", m_context.get_model_converter()->display(tout););
         }
         CTRACE("dl", res, res->display(tout););
         return res.detach();