From 9c230941cc4179ec5aa9a73b3b928bce16f47d4d Mon Sep 17 00:00:00 2001
From: Nuno Lopes <t-nclaud@microsoft.com>
Date: Tue, 23 Apr 2013 12:01:50 -0700
Subject: [PATCH] [datalog] improve performance of smt2 frontend  - delay calls
 to make_annotations and process_costs untill needed  - remove debug exception
 handler in join()

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
---
 src/muz_qe/dl_instruction.cpp | 16 +---------------
 src/muz_qe/rel_context.cpp    |  9 +++++----
 src/muz_qe/rel_context.h      |  2 +-
 3 files changed, 7 insertions(+), 20 deletions(-)

diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp
index 296fa95f3..b103d743e 100644
--- a/src/muz_qe/dl_instruction.cpp
+++ b/src/muz_qe/dl_instruction.cpp
@@ -359,21 +359,7 @@ namespace datalog {
                 r2.get_signature().output(ctx.get_rel_context().get_manager(), tout);
                 tout<<":"<<r2.get_size_estimate_rows()<<" ->\n";);
 
-            try {
-                ctx.set_reg(m_res, (*fn)(r1, r2));
-            }
-            catch(...)
-            {
-                std::string annotation;
-                unsigned sz;
-                ctx.get_register_annotation(m_rel1, annotation);
-                sz = ctx.reg(m_rel1)?ctx.reg(m_rel1)->get_size_estimate_rows():0;
-                std::cout << m_rel1 << "\t" << sz << "\t" << annotation << "\n";
-                ctx.get_register_annotation(m_rel2, annotation);
-                sz = ctx.reg(m_rel2)?ctx.reg(m_rel2)->get_size_estimate_rows():0;
-                std::cout << m_rel2 << "\t" << sz << "\t" << annotation << "\n";
-                throw;
-            }
+            ctx.set_reg(m_res, (*fn)(r1, r2));
 
             TRACE("dl", 
                 ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout);
diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp
index ef5639279..731ab8b63 100644
--- a/src/muz_qe/rel_context.cpp
+++ b/src/muz_qe/rel_context.cpp
@@ -179,9 +179,7 @@ namespace datalog {
             scoped_query.reset();
         }
         m_context.record_transformed_rules();
-        TRACE("dl", m_ectx.report_big_relations(100, tout););
-        m_code.process_all_costs();
-        m_code.make_annotations(m_ectx);        
+        TRACE("dl", display_profile(tout););
         return result;
     }
  
@@ -480,7 +478,10 @@ namespace datalog {
         get_rmanager().display(out);
     }
 
-    void rel_context::display_profile(std::ostream& out) const {
+    void rel_context::display_profile(std::ostream& out) {
+        m_code.make_annotations(m_ectx);
+        m_code.process_all_costs();  
+
         out << "\n--------------\n";
         out << "Instructions\n";
         m_code.display(*this, out);
diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h
index 3e019cb50..8e4c6f2de 100644
--- a/src/muz_qe/rel_context.h
+++ b/src/muz_qe/rel_context.h
@@ -105,7 +105,7 @@ namespace datalog {
         void display_output_facts(rule_set const& rules, std::ostream & out) const;
         void display_facts(std::ostream & out) const;
 
-        void display_profile(std::ostream& out) const;
+        void display_profile(std::ostream& out);
 
         lbool saturate();