/**
    \brief From \c cont which is list of indexes of tail literals of rule \c r, select
    the index pointing to a literal with at least one bound variable that will be the next
    bound literal in the process of creating an adorned rule. If all literals are unbound,
    return -1.
  */
 int mk_magic_sets::pop_bound(unsigned_vector & cont, rule * r, const var_idx_set & bound_vars) {
     float best_cost;
     int candidate_index = -1;
     unsigned n = cont.size();
     for (unsigned i=0; i<n; i++) {
         app * lit = r->get_tail(cont[i]);
         unsigned bound_cnt = get_bound_arg_count(lit, bound_vars);
         if (bound_cnt==0) {
             continue;
         }
         float cost = get_unbound_cost(lit, bound_vars);
         if (candidate_index==-1 || cost<best_cost) {
             best_cost = cost;
             candidate_index = i;
         }
     }
     if (candidate_index==-1) {
         return -1;
     }
     if (candidate_index != static_cast<int>(n-1)) {
         std::swap(cont[candidate_index], cont[n-1]);
     }
     unsigned res = cont.back();
     cont.pop_back();
     return res;
 }

 void sort_core(svector<Numeral> & as, unsigned_vector & xs, numeral_buffer<Numeral, numeral_manager> & buffer) {
     std::sort(xs.begin(), xs.end());
     unsigned num = as.size();
     for (unsigned i = 0; i < num; i++) {
         m().swap(as[i], buffer[xs[i]]);
     }
 }

void sym_mux::collect_indices(expr* e, unsigned_vector& indices) const
{
    indices.reset();
    index_collector collector(*this);
    for_each_expr(collector, m_visited, e);
    m_visited.reset();
    collector.extract(indices);
}

 void extract(unsigned_vector& indices)
 {
     for (unsigned i = 0; i < m_indices.size(); ++i) {
         if (m_indices[i]) {
             indices.push_back(i);
         }
     }
 }

 void get_renaming_args(const unsigned_vector & map, const relation_signature & orig_sig, 
         expr_ref_vector & renaming_arg) {
     ast_manager & m = renaming_arg.get_manager();
     unsigned sz = map.size();
     unsigned ofs = sz-1;
     renaming_arg.resize(sz, static_cast<expr *>(0));
     for(unsigned i=0; i<sz; i++) {
         if(map[i]!=UINT_MAX) {
             renaming_arg.set(ofs-i, m.mk_var(map[i], orig_sig[i]));
         }
     }
 }

 void accumulate(tbv const& t, unsigned_vector& acc) {
     ddnf_node* n = find(t);
     ptr_vector<ddnf_node> todo;
     todo.push_back(n);
     while (!todo.empty()) {
         n = todo.back();
         todo.pop_back();
         unsigned id = n->get_id();
         if (m_marked[id]) continue;
         acc.push_back(id);
         m_marked[id] = true;
         unsigned sz = n->num_children();
         for (unsigned i = 0; i < sz; ++i) {
             todo.push_back((*n)[i]);
         }
     }
 }

 void udoc_relation::expand_column_vector(unsigned_vector& v, const udoc_relation* other) const {
     unsigned_vector orig;
     orig.swap(v);
     for (unsigned i = 0; i < orig.size(); ++i) {
         unsigned col, limit;
         if (orig[i] < get_num_cols()) {
             col = column_idx(orig[i]);
             limit = col + column_num_bits(orig[i]);
         } else {
             unsigned idx = orig[i] - get_num_cols();
             col = get_num_bits() + other->column_idx(idx);
             limit = col + other->column_num_bits(idx);
         }
         for (; col < limit; ++col) {
             v.push_back(col);
         }
     }
 }

void tactic2solver::pop_core(unsigned n) {
    unsigned new_lvl = m_scopes.size() - n;
    unsigned old_sz  = m_scopes[new_lvl];
    m_assertions.shrink(old_sz);
    m_scopes.shrink(new_lvl);
    m_result = 0;
}

 void pop(unsigned num_scopes) {
     SASSERT(m_bounds.empty()); // bounds must be flushed before pop.
     if (num_scopes > 0) {
         SASSERT(num_scopes <= m_enum_consts_lim.size());
         unsigned new_sz = m_enum_consts_lim.size() - num_scopes;
         unsigned lim = m_enum_consts_lim[new_sz];
         for (unsigned i = m_enum_consts.size(); i > lim; ) {
             --i;
             func_decl* f = m_enum_consts[i].get();
             func_decl* f_fresh = m_enum2bv.find(f);
             m_bv2enum.erase(f_fresh);
             m_enum2bv.erase(f);
             m_enum2def.erase(f);
         }
         m_enum_consts_lim.resize(new_sz);
         m_enum_consts.resize(lim);
         m_enum_defs.resize(lim);
         m_enum_bvs.resize(lim);
     }
     m_rw.reset();
 }

static void display_results() {
    if (g_opt) {
        for (unsigned i = 0; i < g_handles.size(); ++i) {
            expr_ref lo = g_opt->get_lower(g_handles[i]);
            expr_ref hi = g_opt->get_upper(g_handles[i]);
            if (lo == hi) {
                std::cout << "   " << lo << "\n";
            }
            else {
                std::cout << "  [" << lo << ":" << hi << "]\n";
            }
        }
    }
}

 void group_by(table_fact const& in, table_fact& out) {
     out.reset();
     for (unsigned i = 0; i < m_group_by_cols.size(); ++i) {
         out.push_back(in[m_group_by_cols[i]]);
     }
 }

 virtual void operator()(table_base& _t) {
     lazy_table& t = get(_t);
     t.set(alloc(lazy_table_filter_identical, m_cols.size(), m_cols.c_ptr(), t));
 }

 void push() {
     m_enum_consts_lim.push_back(m_enum_consts.size());
 }

 unsigned scope_level() const override { return m_scopes.size(); }