53 class pob;  variable
54 typedef ref<pob> pob_ref;
55 typedef sref_vector<pob> pob_ref_vector;
56 typedef sref_buffer<pob> pob_ref_buffer;
112 typedef pob pob;  typedef
297         typedef ptr_buffer<pob, 1> pob_buffer;
313         pob* mk_pob(pob *parent, unsigned level, unsigned depth,
316         pob* mk_pob(pob *parent, unsigned level, unsigned depth,  in mk_pob()
323         pob* find_pob(pob* parent, expr *post);
514     reach_fact *mk_rf(pob &n, model &mdl, const datalog::rule &r);
519     pob* mk_pob(pob *parent, unsigned level, unsigned depth,  in mk_pob()
523     pob* find_pob(pob *parent, expr *post) {  in find_pob()
527     pob* mk_pob(pob *parent, unsigned level, unsigned depth,  in mk_pob()
532     lbool is_reachable(pob& n, expr_ref_vector* core, model_ref *model,
569     bool is_blocked (pob &n, unsigned &uses_level);
571     bool is_qblocked (pob &n);
592 class pob {
624     ptr_vector<pob>  m_kids;
633     pob (pob* parent, pred_transformer& pt,
636     ~pob() {if (m_parent) { m_parent->erase_child(*this); }}  in ~pob()
651     void inherit(pob const &p);
659     pob* parent () const { return m_parent.get (); }  in parent()
683     const ptr_vector<pob> &children() const {return m_kids;}  in children()
684     void add_child (pob &v) {m_kids.push_back (&v);}  in add_child()
685     void erase_child (pob &v) {m_kids.erase (&v);}  in erase_child()
719         pob &m_p;
721         on_expand_event(pob &p) : m_p(p) {m_p.on_expand();}  in on_expand_event()
726 inline std::ostream &operator<<(std::ostream &out, pob const &p) {
731     bool operator() (const pob *pn1, const pob *pn2) const;
735     bool operator() (const pob *n1, const pob *n2) const {  in operator()
772     pob&                         m_parent;
787     pob* create_next_child (model &mdl);
791     derivation (pob& parent, datalog::rule const& rule,
799     pob *create_first_child (model &mdl);
803     pob *create_next_child ();
806     pob& get_parent () const { return m_parent; }  in get_parent()
816     typedef std::priority_queue<pob*, std::vector<pob*>, pob_gt_proc> pob_queue_ty;
827     pob* top();
829     void push (pob &n);
842     pob& get_root() const {return *m_root.get ();}  in get_root()
843     void set_root(pob& n);
844     bool is_root(pob& n) const {return m_root.get () == &n;}  in is_root()
992     bool gpdr_create_split_children(pob &n, const datalog::rule &r,
1000     void log_expand_pob(pob &);
1005     bool is_requeue(pob &n);
1009     bool is_reachable(pob &n);
1010     lbool expand_pob(pob &n, pob_ref_buffer &out);
1011     bool create_children(pob& n, const datalog::rule &r,
1054     lbool handle_unknown(pob &n, const datalog::rule *r, model &model);
1114     pob& get_root() const {return m_pob_queue.get_root();}  in get_root()
1135     void new_pob_eh(pob *p);