From 2444440edcd66edabd4c019f0522d4cd8bcade16 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Mon, 2 Feb 2015 11:28:57 +0000
Subject: [PATCH] DoC: implement get_size_estimate_bytes()

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/doc.cpp           | 7 +++++++
 src/muz/rel/doc.h             | 8 ++++++++
 src/muz/rel/rel_context.cpp   | 7 -------
 src/muz/rel/tbv.h             | 2 ++
 src/muz/rel/udoc_relation.cpp | 4 ++++
 src/muz/rel/udoc_relation.h   | 1 +
 6 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 67e2f1e2b..a27d20c56 100644
--- a/src/muz/rel/doc.cpp
+++ b/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;
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index fcb134d9e..ca5af005b 100644
--- a/src/muz/rel/doc.h
+++ b/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;
+    }
 };
 
 
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index 4fd9a8fe9..9fa7eadd0 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/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);
 
diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h
index d667ccaa2..ad98b8095 100644
--- a/src/muz/rel/tbv.h
+++ b/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; }
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index ffb4b6e22..8e971ac1e 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/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):
diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h
index a9d31e7d3..40f2222fc 100644
--- a/src/muz/rel/udoc_relation.h
+++ b/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; }