mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

Rename pobs into pob_manager

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-26 21:20:54 -04:00
parent 176c0a97f7
commit 1910b4c87c
2 changed files with 8 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz/spacer/spacer_context.cpp
View file

@ -2123,9 +2123,10 @@ void pred_transformer::frames::simplify_formulas ()
/// pred_transformer::pobs /// pred_transformer::pobs
pob* pred_transformer::pobs::mk_pob(pob *parent, pob* pred_transformer::pob_manager::mk_pob(pob *parent,
unsigned level, unsigned depth, unsigned level, unsigned depth,
expr *post, app_ref_vector const &b) { expr *post,
app_ref_vector const &b) {
if (!m_pt.ctx.reuse_pobs()) { if (!m_pt.ctx.reuse_pobs()) {
pob* n = alloc(pob, parent, m_pt, level, depth); pob* n = alloc(pob, parent, m_pt, level, depth);

8
src/muz/spacer/spacer_context.h
View file

@ -269,9 +269,9 @@ class pred_transformer {
}; };
/** /**
manager of proof-obligations (pobs) manager of proof-obligations (pob_manager)
*/ */
class pobs { class pob_manager {
typedef ptr_buffer<pob, 1> pob_buffer; typedef ptr_buffer<pob, 1> pob_buffer;
typedef obj_map<expr, pob_buffer > expr2pob_buffer; typedef obj_map<expr, pob_buffer > expr2pob_buffer;
@ -280,7 +280,7 @@ class pred_transformer {
expr2pob_buffer m_pobs; expr2pob_buffer m_pobs;
pob_ref_vector m_pinned; pob_ref_vector m_pinned;
public: public:
pobs(pred_transformer &pt) : m_pt(pt) {} pob_manager(pred_transformer &pt) : m_pt(pt) {}
pob* mk_pob(pob *parent, unsigned level, unsigned depth, pob* mk_pob(pob *parent, unsigned level, unsigned depth,
expr *post, app_ref_vector const &b); expr *post, app_ref_vector const &b);
@ -362,7 +362,7 @@ class pred_transformer {
ptr_vector<datalog::rule> m_rules; // rules used to derive transformer ptr_vector<datalog::rule> m_rules; // rules used to derive transformer
scoped_ptr<prop_solver> m_solver; // solver context scoped_ptr<prop_solver> m_solver; // solver context
ref<solver> m_reach_solver; // context for reachability facts ref<solver> m_reach_solver; // context for reachability facts
pobs m_pobs; // proof obligations created so far pob_manager m_pobs; // proof obligations created so far
frames m_frames; // frames with lemmas frames m_frames; // frames with lemmas
reach_fact_ref_vector m_reach_facts; // reach facts reach_fact_ref_vector m_reach_facts; // reach facts
unsigned m_rf_init_sz; // number of reach fact from INIT unsigned m_rf_init_sz; // number of reach fact from INIT