From 47635325014f2951d203897eae4d8120787a283d Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Tue, 30 Sep 2014 11:25:47 -0700
Subject: [PATCH] adding compile-time option to replace arrays with maps in smt
 (define SPARSE_MAP)

---
 src/smt/smt_context.h |  7 ++++++-
 src/smt/smt_enode.cpp |  6 +++---
 src/smt/smt_enode.h   | 29 ++++++++++++++++++++++++++---
 src/util/map.h        |  2 +-
 4 files changed, 36 insertions(+), 8 deletions(-)

diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 7940b17be..5abdfa5f9 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -54,7 +54,11 @@ Revision History:
 // the case that each context only references a few expressions.
 // Using a map instead of a vector for the literals can compress space 
 // consumption.
+#ifdef SPARSE_MAP
+#define USE_BOOL_VAR_VECTOR 0
+#else
 #define USE_BOOL_VAR_VECTOR 1
+#endif
 
 namespace smt {
 
@@ -69,6 +73,7 @@ namespace smt {
         std::string last_failure_as_string() const;
         void set_progress_callback(progress_callback *callback);
 
+
     protected:
         ast_manager &               m_manager;
         smt_params &          m_fparams;
@@ -106,7 +111,7 @@ namespace smt {
         // -----------------------------------
         enode *                     m_true_enode;
         enode *                     m_false_enode;
-        ptr_vector<enode>           m_app2enode;    // app -> enode
+        app2enode_t                 m_app2enode;    // app -> enode
         ptr_vector<enode>           m_enodes;
         plugin_manager<theory>      m_theories;     // mapping from theory_id -> theory
         ptr_vector<theory>          m_theory_set;   // set of theories for fast traversal
diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index 98b8eaf8b..451577357 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -24,7 +24,7 @@ namespace smt {
     /**
        \brief Initialize an enode in the given memory position.
     */
-    enode * enode::init(ast_manager & m, void * mem, ptr_vector<enode> const & app2enode, app * owner, 
+    enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, 
                         unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                         bool cgc_enabled, bool update_children_parent) {
         SASSERT(m.is_bool(owner) || !merge_tf);
@@ -60,7 +60,7 @@ namespace smt {
         return n;
     }
 
-    enode * enode::mk(ast_manager & m, region & r, ptr_vector<enode> const & app2enode, app * owner, 
+    enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, 
                            unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                            bool cgc_enabled, bool update_children_parent) {
         SASSERT(m.is_bool(owner) || !merge_tf);
@@ -69,7 +69,7 @@ namespace smt {
         return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
     }
 
-    enode * enode::mk_dummy(ast_manager & m, ptr_vector<enode> const & app2enode, app * owner) {
+    enode * enode::mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner) {
         unsigned sz           = get_enode_size(owner->get_num_args());
         void * mem            = alloc_svect(char, sz);
         return init(m, mem, app2enode, owner, 0, false, false, 0, true, false);
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 505dea0ee..ca75028c3 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -38,6 +38,29 @@ namespace smt {
         }
     };
 
+    /** \ brief Use sparse maps in SMT solver.
+
+	Define this to use hash maps rather than vectors over ast
+	nodes. This is useful in the case there are many solvers, each
+	referencing few nodes from a large ast manager. There is some
+	unknown performance penalty for this. */
+
+    // #define SPARSE_MAP
+
+#ifndef SPARSE_MAP
+    typedef ptr_vector<enode> app2enode_t;    // app -> enode
+#else
+    class app2enode_t : public u_map<enode *> {
+    public:
+      void setx(unsigned x, enode *val, enode *def){
+	if(val == 0)
+	  erase(x);
+	else
+	  insert(x,val);
+      }
+    };
+#endif
+
     class tmp_enode;
 
     /**
@@ -115,7 +138,7 @@ namespace smt {
 
         friend class tmp_enode;
 
-        static enode * init(ast_manager & m, void * mem, ptr_vector<enode> const & app2enode, app * owner, 
+        static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, 
                             unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                             bool cgc_enabled, bool update_children_parent);
     public:
@@ -124,11 +147,11 @@ namespace smt {
             return sizeof(enode) + num_args * sizeof(enode*);
         }
         
-        static enode * mk(ast_manager & m, region & r, ptr_vector<enode> const & app2enode, app * owner, 
+        static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, 
                           unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                           bool cgc_enabled, bool update_children_parent);
 
-        static enode * mk_dummy(ast_manager & m, ptr_vector<enode> const & app2enode, app * owner);
+        static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner);
         
         static void del_dummy(enode * n) { dealloc_svect(reinterpret_cast<char*>(n)); }
 
diff --git a/src/util/map.h b/src/util/map.h
index 3e8e10891..d659b89c0 100644
--- a/src/util/map.h
+++ b/src/util/map.h
@@ -131,7 +131,7 @@ public:
     value const& get(key const& k, value const& default_value) const {
         entry* e = find_core(k);
         if (e) {
-            return e->m_value;
+	  return e->get_data().m_value;
         }
         else {
             return default_value;