DoC: implement get_size_estimate_bytes()

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>

src/muz/rel/doc.cpp

@@ -107,6 +107,13 @@ doc& doc_manager::fillX(doc& src) {
     m.fillX(src.pos());
     return src;
 }
+
+unsigned doc_manager::get_size_estimate_bytes(const doc& d) const {
+    return m.get_size_estimate_bytes(d.pos())
+        + d.neg().get_size_estimate_bytes(m)
+        + sizeof(doc);
+}
+
 bool doc_manager::set_and(doc& dst, doc const& src)  {
     // (A \ B) & (C \ D) = (A & C) \ (B u D)
     if (!m.set_and(dst.pos(), src.pos())) return false;

src/muz/rel/doc.h

@@ -87,6 +87,7 @@ public:
     std::ostream& display(std::ostream& out, doc const& b) const;
     std::ostream& display(std::ostream& out, doc const& b, unsigned hi, unsigned lo) const;
     unsigned num_tbits() const { return m.num_tbits(); }
+    unsigned get_size_estimate_bytes(const doc& d) const;
     doc* project(doc_manager& dstm, bit_vector const& to_delete, doc const& src);
     bool well_formed(doc const& d) const;
     bool merge(doc& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols);
@@ -326,6 +327,13 @@ public:
         }
     }
 
+    unsigned get_size_estimate_bytes(const M& m) const {
+        unsigned sz = sizeof(T*) * size();
+        for (unsigned i = 0; i < size(); ++i) {
+            sz += m.get_size_estimate_bytes(*m_elems[i]);
+        }
+        return sz;
+    }
 };
 
 

src/muz/rel/rel_context.cpp

@@ -172,8 +172,6 @@ namespace datalog {
 
             compiler::compile(m_context, m_context.get_rules(), m_code, termination_code);
 
-            TRACE("dl", m_code.display(m_ectx, tout); );
-
             bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time);
 
             if (time_limit || restart_time!=0) {
@@ -628,11 +626,6 @@ namespace datalog {
         m_code.make_annotations(m_ectx);
         m_code.process_all_costs();  
 
-        out << "\n--------------\n";
-        out << "Instructions\n";
-        m_code.display(m_ectx, out);
-
-        out << "\n--------------\n";
         out << "Big relations\n";
         m_ectx.report_big_relations(1000, out);
 

src/muz/rel/tbv.h

@@ -57,6 +57,8 @@ public:
     tbv* allocate(tbv const& bv, unsigned const* permutation);
 
     void deallocate(tbv* bv);
+
+    unsigned get_size_estimate_bytes(const tbv&) const { return m.num_bytes(); }
         
     void copy(tbv& dst, tbv const& src) const;
     unsigned num_tbits() const { return m.num_bits()/2; }

src/muz/rel/udoc_relation.cpp

@@ -181,6 +181,10 @@ namespace datalog {
         m_elems.display(dm, out); out << "\n";
     }
 
+    unsigned udoc_relation::get_size_estimate_bytes() const {
+        return sizeof(*this) + m_elems.get_size_estimate_bytes(dm);
+    }
+
     // -------------
 
     udoc_plugin::udoc_plugin(relation_manager& rm):

src/muz/rel/udoc_relation.h

@@ -53,6 +53,7 @@ namespace datalog {
         virtual void display(std::ostream& out) const;
         virtual bool is_precise() const { return true; }
         virtual unsigned get_size_estimate_rows() const { return m_elems.size(); }
+        virtual unsigned get_size_estimate_bytes() const;
 
         doc_manager& get_dm() const { return dm; }
         udoc const& get_udoc() const { return m_elems; }