port Jakob's update to union_find from polysat branch

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/sat/smt/array_solver.h

@@ -32,7 +32,7 @@ namespace array {
         typedef sat::literal literal;
         typedef sat::bool_var bool_var;
         typedef sat::literal_vector literal_vector;
-        typedef union_find<solver, euf::solver>  array_union_find;
+        typedef union_find<solver>  array_union_find;
 
 
         struct stats {

src/sat/smt/bv_solver.h

@@ -49,7 +49,7 @@ namespace bv {
         typedef std::pair<numeral, unsigned> value_sort_pair;
         typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
         typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
-        typedef union_find<solver, euf::solver>  bv_union_find;
+        typedef union_find<solver>  bv_union_find;
         typedef std::pair<theory_var, unsigned> var_pos;
 
         friend class ackerman;

src/sat/smt/dt_solver.h

@@ -36,7 +36,7 @@ namespace dt {
         typedef sat::bool_var bool_var;
         typedef sat::literal literal;
         typedef sat::literal_vector literal_vector;
-        typedef union_find<solver, euf::solver>  dt_union_find;
+        typedef union_find<solver>  dt_union_find;
 
         struct var_data {
             ptr_vector<enode> m_recognizers; //!< recognizers of this equivalence class that are being watched.

src/util/union_find.h

@@ -35,7 +35,7 @@ class union_find_default_ctx {
     _trail_stack m_stack;
 };
 
-template<typename Ctx = union_find_default_ctx, typename StackCtx = Ctx>
+template<typename Ctx = union_find_default_ctx>
 class union_find {
     Ctx &                         m_ctx;
     trail_stack &                 m_trail_stack;