From 5cc8c8bde618b8a36f86778aa25812c6762e3d65 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Wed, 24 Jun 2015 15:00:47 +0100
Subject: [PATCH] udoc: micro optimization for compiler_guard

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
---
 src/muz/rel/udoc_relation.cpp | 20 ++++++++------------
 src/muz/rel/udoc_relation.h   |  1 -
 2 files changed, 8 insertions(+), 13 deletions(-)

diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index d90270d9f..140d1e94d 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -723,12 +723,9 @@ namespace datalog {
         conds.push_back(m.mk_eq(e1, e2));
     }
 
-    void udoc_relation::compile_guard(expr* g, udoc& d, bit_vector const& discard_cols) const {
-        d.reset(dm);
-        d.push_back(dm.allocateX()); 
-        apply_guard(g, d, discard_cols);
-    }
-    void udoc_relation::apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const {
+    void udoc_relation::compile_guard(expr* g, udoc& result, bit_vector const& discard_cols) const {
+        result.push_back(dm.allocateX());
+
         // datastructure to store equalities with columns that will be projected out
         union_find_default_ctx union_ctx;
         subset_ints equalities(union_ctx);
@@ -737,6 +734,7 @@ namespace datalog {
         }        
         apply_guard(g, result, equalities, discard_cols);
     }
+
     bool udoc_relation::apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const {
         udoc_plugin& p = get_plugin();
         unsigned num_bits;
@@ -753,9 +751,6 @@ namespace datalog {
         return false;
     }
 
-
-
-
     bool udoc_relation::apply_bv_eq(
         expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const {
         udoc_plugin& p = get_plugin();
@@ -926,9 +921,10 @@ namespace datalog {
             expr_ref guard(m);
             for (unsigned i = 0; i < num_bits; ++i) {
                 m_equalities.mk_var();
-            }        
-            t.extract_guard(condition, guard, m_reduced_condition);            
-            t.compile_guard(guard, m_udoc, m_empty_bv);
+            }
+            t.extract_guard(condition, guard, m_reduced_condition);
+            m_udoc.push_back(dm.allocateX());
+            t.apply_guard(guard, m_udoc, m_equalities, m_empty_bv);
 
             TRACE("doc", 
                   tout << "original condition: " << mk_pp(condition, m) << "\n";
diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h
index 40f2222fc..d988252da 100644
--- a/src/muz/rel/udoc_relation.h
+++ b/src/muz/rel/udoc_relation.h
@@ -72,7 +72,6 @@ namespace datalog {
         void extract_equalities(
             expr* e1, expr* e2, expr_ref_vector& conds, 
             subset_ints& equalities, unsigned_vector& roots) const;
-        void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
         void apply_guard(expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const;
         bool apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const;
         bool apply_bv_eq(expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const;