inline void swap( ptr_vector<T,CA,A>& l, ptr_vector<T,CA,A>& r )
 {
     l.swap(r);
 }

void rule_properties::insert(ptr_vector<rule>& rules, rule* r) {
    if (rules.empty() || rules.back() != r) {
        rules.push_back(r);
    }
}

static
void mergeClass(ptr_vector<VertexInfo> &infos, NGHolder &g, unsigned eq_class,
                VertexInfoSet &cur_class_vertices, set<NFAVertex> *toRemove) {
    DEBUG_PRINTF("Replacing %zd vertices from equivalence class %u with a "
                 "single vertex.\n", cur_class_vertices.size(), eq_class);

    // replace equivalence class with a single vertex:
    // 1. create new vertex with matching properties
    // 2. wire all predecessors to new vertex
    // 2a. update info for new vertex with new predecessors
    // 2b. update each predecessor's successor list
    // 3. wire all successors to new vertex
    // 3a. update info for new vertex with new successors
    // 3b. update each successor's predecessor list
    // 4. remove old vertex

    // any differences between vertex properties were resolved during
    // initial partitioning, so we assume that every vertex in equivalence
    // class has the same CharReach et al.
    // so, we find the first vertex in our class and get all its properties

    /* For left equivalence, if the members have different reporting behaviour
     * we sometimes require two vertices to be created (one connected to accept
     * and one to accepteod) */

    NFAVertex old_v = (*cur_class_vertices.begin())->v;
    NFAVertex new_v = clone_vertex(g, old_v); /* set up new vertex with same
                                               * props */
    g[new_v].reports.clear(); /* populated as we pull in succs */

    VertexInfo *new_vertex_info = new VertexInfo(new_v, g);
    // store this vertex in our global vertex list
    infos.push_back(new_vertex_info);

    NFAVertex new_v_eod = NGHolder::null_vertex();
    VertexInfo *new_vertex_info_eod = nullptr;

    if (require_separate_eod_vertex(cur_class_vertices, g)) {
        new_v_eod = clone_vertex(g, old_v);
        g[new_v_eod].reports.clear();
        new_vertex_info_eod = new VertexInfo(new_v_eod, g);
        infos.push_back(new_vertex_info_eod);
    }

    const unsigned edgetop = (*cur_class_vertices.begin())->edge_top;
    for (VertexInfo *old_vertex_info : cur_class_vertices) {
        assert(old_vertex_info->equivalence_class == eq_class);

        // mark this vertex for removal
        toRemove->insert(old_vertex_info->v);

        // for each predecessor, add edge to new vertex and update info
        for (VertexInfo *pred_info : old_vertex_info->pred) {
            // update info for new vertex
            new_vertex_info->pred.insert(pred_info);
            if (new_vertex_info_eod) {
                new_vertex_info_eod->pred.insert(pred_info);
            }

            // update info for predecessor
            pred_info->succ.erase(old_vertex_info);

            // if edge doesn't exist, create it
            NFAEdge e = add_edge_if_not_present(pred_info->v, new_v, g).first;

            // put edge top, if applicable
            if (edgetop != (unsigned) -1) {
                g[e].top = edgetop;
            }

            pred_info->succ.insert(new_vertex_info);

            if (new_v_eod) {
                NFAEdge ee = add_edge_if_not_present(pred_info->v, new_v_eod,
                                                     g).first;

                // put edge top, if applicable
                if (edgetop != (unsigned) -1) {
                    g[ee].top = edgetop;
                }

                pred_info->succ.insert(new_vertex_info_eod);
            }
        }

        // for each successor, add edge from new vertex and update info
        for (VertexInfo *succ_info : old_vertex_info->succ) {
            NFAVertex succ_v = succ_info->v;

            // update info for successor
            succ_info->pred.erase(old_vertex_info);

            if (new_v_eod && succ_v == g.acceptEod) {
                // update info for new vertex
                new_vertex_info_eod->succ.insert(succ_info);
                insert(&g[new_v_eod].reports,
                       g[old_vertex_info->v].reports);

                add_edge_if_not_present(new_v_eod, succ_v, g);
                succ_info->pred.insert(new_vertex_info_eod);
//.........这里部分代码省略.........

void iz3pp(ast_manager &m,
	   const ptr_vector<expr> &cnsts_vec,
	   expr *tree,
	   std::ostream& out) {

  unsigned sz = cnsts_vec.size();
  expr* const* cnsts = &cnsts_vec[0];

  out << "(set-option :produce-interpolants true)\n";

  free_func_visitor visitor(m);
  expr_mark visited;
  bool print_low_level = true; // m_params.print_low_level_smt2();

#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env);

  smt2_pp_environment_dbg env(m);

  for (unsigned i = 0; i < sz; ++i) {
    expr* e = cnsts[i];
    for_each_expr(visitor, visited, e);
  }

  // name all the constraints
  hash_map<expr *, symbol> cnames;
  int ctr = 1;
  for(unsigned i = 0; i < sz; i++){
    symbol nm;
    std::ostringstream s;
    s << "f!" << (ctr++);
    cnames[cnsts[i]] = symbol(s.str().c_str());
  }

  func_decl_set &funcs = visitor.funcs();
  func_decl_set::iterator it  = funcs.begin(), end = funcs.end();

  obj_hashtable<class sort>& sorts = visitor.sorts();
  obj_hashtable<class sort>::iterator sit = sorts.begin(), send = sorts.end();



  for (; sit != send; ++sit) {
    PP(*sit);
  }

  for (; it != end; ++it) {
    func_decl* f = *it;
    if(f->get_family_id() == null_family_id){
      PP(f);
      out << "\n";
    }
  }

  for (unsigned i = 0; i < sz; ++i) {
    out << "(assert ";
    expr* r = cnsts[i];
    symbol nm = cnames[r];
    out << "(! ";
    PP(r);
    out << " :named ";
    if (is_smt2_quoted_symbol(nm)) {
      out << mk_smt2_quoted_symbol(nm);
    }
    else {
      out << nm;
    }
    out << ")";
    out << ")\n";
  }
  out << "(check-sat)\n";
  out << "(get-interpolant ";
  iz3pp_helper pp(m);
  pp.print_tree(pp.cook(tree),cnames,out);
  out << ")\n";
}

void goal::get_formulas(ptr_vector<expr> & result) {
    unsigned sz = size();
    for (unsigned i = 0; i < sz; i++) {
        result.push_back(form(i));
    }
}

 virtual void get_unsat_core(ptr_vector<expr> & r) {
     SASSERT(m_context);
     unsigned sz = m_context->get_unsat_core_size();
     for (unsigned i = 0; i < sz; i++)
         r.push_back(m_context->get_unsat_core_expr(i));
 }

 virtual void set_next_arg(cmd_context & ctx, expr * arg) {
     m_targets.push_back(arg);
 }

    void reduce(proof* pf, proof_ref &out)
    {
        proof *res = NULL;

        m_todo.reset();
        m_todo.push_back(pf);
        ptr_buffer<proof> args;
        bool dirty = false;

        while (!m_todo.empty()) {
            proof *p, *tmp, *pp;
            unsigned todo_sz;

            p = m_todo.back();
            if (m_cache.find(p, tmp)) {
                res = tmp;
                m_todo.pop_back();
                continue;
            }

            dirty = false;
            args.reset();
            todo_sz = m_todo.size();
            for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
                pp = m.get_parent(p, i);
                if (m_cache.find(pp, tmp)) {
                    args.push_back(tmp);
                    dirty = dirty || pp != tmp;
                } else {
                    m_todo.push_back(pp);
                }
            }

            if (todo_sz < m_todo.size()) { continue; }
            else { m_todo.pop_back(); }

            if (m.is_hypothesis(p)) {
                // hyp: replace by a corresponding unit
                if (m_units.find(m.get_fact(p), tmp)) {
                    res = tmp;
                } else { res = p; }
            }

            else if (!dirty) { res = p; }

            else if (m.is_lemma(p)) {
                //lemma: reduce the premise; remove reduced consequences from conclusion
                SASSERT(args.size() == 1);
                res = mk_lemma_core(args.get(0), m.get_fact(p));
                compute_mark1(res);
            } else if (m.is_unit_resolution(p)) {
                // unit: reduce untis; reduce the first premise; rebuild unit resolution
                res = mk_unit_resolution_core(args.size(), args.c_ptr());
                compute_mark1(res);
            } else  {
                // other: reduce all premises; reapply
                if (m.has_fact(p)) { args.push_back(to_app(m.get_fact(p))); }
                SASSERT(p->get_decl()->get_arity() == args.size());
                res = m.mk_app(p->get_decl(), args.size(), (expr * const*)args.c_ptr());
                m_pinned.push_back(res);
                compute_mark1(res);
            }

            SASSERT(res);
            m_cache.insert(p, res);

            if (m.has_fact(res) && m.is_false(m.get_fact(res))) { break; }
        }

        out = res;
    }

 virtual void prepare(cmd_context & ctx) { 
     parametric_cmd::prepare(ctx);
     m_targets.resize(0);
 }

 ~datatype_decl() {
     std::for_each(m_constructors.begin(), m_constructors.end(), delete_proc<constructor_decl>());
 }

 void set_next_arg(cmd_context & ctx, expr * arg) override {
     m_targets.push_back(arg);
 }

 void prepare(cmd_context & ctx) override {
     parametric_cmd::prepare(ctx);
     m_targets.resize(0);
 }

 void add_parent(term* p) { m_parents.push_back(p); }

 void visit(func_decl * f, bool & visited) {
     if (get_color(f) != CLOSED) {
         m_todo.push_back(f);
         visited = false;
     }
 }