From 20e1247461c3b6be51c08d2d6104bd1aea9bc8c3 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 2 Jul 2013 14:09:17 -0500
Subject: [PATCH] Make uf strong solver user-context dependent, fixes bug 522.

---
 src/theory/uf/theory_uf_strong_solver.cpp | 8 ++++----
 src/theory/uf/theory_uf_strong_solver.h   | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 71a342f76..c8b7d76eb 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -408,9 +408,9 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in
 
 
 
-StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
+StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
           d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ),
-          d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( 0 ),
+          d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ),
           d_cardinality_assertions( c ), d_hasCard( c, false ){
   d_cardinality_term = n;
 }
@@ -990,7 +990,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
       }
     }
   }
-  d_aloc_cardinality++;
+  d_aloc_cardinality = d_aloc_cardinality + 1;
 
   //check for abort case
   if( options::ufssAbortCardinality()==d_aloc_cardinality ){
@@ -1574,7 +1574,7 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
     SortModel* rm = NULL;
     if( tn.isSort() ){
       Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
-      rm  = new SortModel( n, d_th->getSatContext(), this );
+      rm  = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this );
     }else{
       /*
       if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index d263d8cc7..fa8d60b49 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -207,7 +207,7 @@ public:
     /** cardinality */
     context::CDO< int > d_cardinality;
     /** maximum allocated cardinality */
-    int d_aloc_cardinality;
+    context::CDO< int > d_aloc_cardinality;
     /** cardinality lemma term */
     Node d_cardinality_term;
     /** cardinality totality terms */
@@ -228,7 +228,7 @@ public:
     /** get totality lemma terms */
     Node getTotalityLemmaTerm( int cardinality, int i );
   public:
-    SortModel( Node n, context::Context* c, StrongSolverTheoryUF* thss );
+    SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss );
     virtual ~SortModel(){}
     /** initialize */
     void initialize( OutputChannel* out );
-- 
2.30.2