From 24de0a9b908321fed4ee76a09b346737939dc447 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 8 Dec 2015 16:37:08 -0800
Subject: [PATCH] seq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 15 +++++++--------
 src/smt/theory_seq.h   |  5 +++--
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 48b034965..213e671db 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -44,14 +44,13 @@ void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d
 
 expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) {
     std::pair<expr*, enode_pair_dependency*> value;
-    if (m_map.find(e, value)) {
-        d = value.second;
-        return value.first;
-    }
-    else {
-        d = 0;
-        return e;
+    d = 0;
+    // TBD add path compression?
+    while (m_map.find(e, value)) {
+        d = d ? m_dm.mk_join(d, value.second) : value.second;;
+        e = value.first;
     }
+    return e;
 }
 
 void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
@@ -77,7 +76,7 @@ theory_seq::theory_seq(ast_manager& m):
     theory(m.mk_family_id("seq")), 
     m(m),
     m_dam(m_dep_array_value_manager, m_alloc),
-    m_rep(m),    
+    m_rep(m, m_dm),    
     m_ineqs(m),
     m_axioms(m),
     m_axioms_head(0),
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 505b3aa5e..4aee7e61c 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -46,17 +46,18 @@ namespace smt {
         
         typedef union_find<theory_seq> th_union_find;
         typedef trail_stack<theory_seq> th_trail_stack;
-
+        
         class solution_map {
             enum map_update { INS, DEL };
             ast_manager& m;
+            enode_pair_dependency_manager&      m_dm;
             obj_map<expr, std::pair<expr*, enode_pair_dependency*> > m_map;            
             expr_ref_vector m_lhs, m_rhs;
             ptr_vector<enode_pair_dependency> m_deps;
             svector<map_update>    m_updates;
             unsigned_vector        m_limit;
         public:
-            solution_map(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {}
+            solution_map(ast_manager& m, enode_pair_dependency_manager& dm): m(m), m_dm(dm), m_lhs(m), m_rhs(m) {}
             void  update(expr* e, expr* r, enode_pair_dependency* d);
             expr* find(expr* e, enode_pair_dependency*& d);
             void push_scope() { m_limit.push_back(m_updates.size()); }