From c00c6b4285a2b901141d49a229e24ceb61e01de3 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 26 Jun 2018 21:36:18 -0400 Subject: [PATCH] Pobs are always managed Removed options to allow unmanaged pobs. Other minor cleanups. --- src/muz/base/fp_params.pyg | 1 - src/muz/spacer/spacer_context.cpp | 26 ++++++---------- src/muz/spacer/spacer_context.h | 52 +++++++++++++++++-------------- 3 files changed, 37 insertions(+), 42 deletions(-) diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index c96a12ca2..31ab3a358 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -160,7 +160,6 @@ def_module_params('fp', '2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin'), ('spacer.iuc.old_hyp_reducer', BOOL, False, 'use old hyp reducer instead of new implementation, for debugging only'), ('spacer.validate_lemmas', BOOL, False, 'Validate each lemma after generalization'), - ('spacer.reuse_pobs', BOOL, True, 'Reuse pobs'), ('spacer.ground_pobs', BOOL, True, 'Ground pobs by using values from a model'), ('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'), ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'), diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index bf7743bae..48550df12 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -137,15 +137,15 @@ void pob::get_skolems(app_ref_vector &v) { pob* pob_queue::top () { /// nothing in the queue - if (m_obligations.empty()) { return nullptr; } + if (m_data.empty()) { return nullptr; } /// top queue element is above max level - if (m_obligations.top()->level() > m_max_level) { return nullptr; } + if (m_data.top()->level() > m_max_level) { return nullptr; } /// top queue element is at the max level, but at a higher than base depth - if (m_obligations.top ()->level () == m_max_level && - m_obligations.top()->depth() > m_min_depth) { return nullptr; } + if (m_data.top ()->level () == m_max_level && + m_data.top()->depth() > m_min_depth) { return nullptr; } /// there is something good in the queue - return m_obligations.top ().get (); + return m_data.top (); } void pob_queue::set_root(pob& root) @@ -160,14 +160,14 @@ pob_queue::~pob_queue() {} void pob_queue::reset() { - while (!m_obligations.empty()) { m_obligations.pop(); } - if (m_root) { m_obligations.push(m_root); } + while (!m_data.empty()) { m_data.pop(); } + if (m_root) { m_data.push(m_root.get()); } } void pob_queue::push(pob &n) { TRACE("pob_queue", tout << "pob_queue::push(" << n.post()->get_id() << ")\n";); - m_obligations.push (&n); + m_data.push (&n); n.get_context().new_pob_eh(&n); } @@ -2127,13 +2127,6 @@ pob* pred_transformer::pob_manager::mk_pob(pob *parent, unsigned level, unsigned depth, expr *post, app_ref_vector const &b) { - - if (!m_pt.ctx.reuse_pobs()) { - pob* n = alloc(pob, parent, m_pt, level, depth); - n->set_post(post, b); - return n; - } - // create a new pob and set its post to normalize it pob p(parent, m_pt, level, depth, false); p.set_post(post, b); @@ -2211,7 +2204,6 @@ void context::updt_params() { m_use_ctp = m_params.spacer_ctp(); m_use_inc_clause = m_params.spacer_use_inc_clause(); m_blast_term_ite = m_params.spacer_blast_term_ite(); - m_reuse_pobs = m_params.spacer_reuse_pobs(); m_use_ind_gen = m_params.spacer_use_inductive_generalizer(); m_use_array_eq_gen = m_params.spacer_use_array_eq_generalizer(); m_validate_lemmas = m_params.spacer_validate_lemmas(); @@ -3936,7 +3928,7 @@ bool context::is_inductive() { } /// pob_lt operator -inline bool pob_lt::operator() (const pob *pn1, const pob *pn2) const +inline bool pob_lt_proc::operator() (const pob *pn1, const pob *pn2) const { SASSERT (pn1); SASSERT (pn2); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 6823f0406..480b8ecf5 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -270,14 +270,27 @@ class pred_transformer { /** manager of proof-obligations (pob_manager) + + Pobs are determined uniquely by their post-condition and a parent pob. + They are managed by pob_manager and remain live through the + life of the manager */ class pob_manager { + // a buffer that contains space for one pob and allocates more + // space if needed typedef ptr_buffer pob_buffer; + // Type for the map from post-conditions to pobs. The common + // case is that each post-condition corresponds to a single + // pob. Other cases are handled by expanding the buffer typedef obj_map expr2pob_buffer; + // parent predicate transformer pred_transformer &m_pt; + // map from post-conditions to pobs expr2pob_buffer m_pobs; + + // a store pob_ref_vector m_pinned; public: pob_manager(pred_transformer &pt) : m_pt(pt) {} @@ -673,22 +686,14 @@ public: }; -struct pob_lt : - public std::binary_function -{bool operator() (const pob *pn1, const pob *pn2) const;}; - -struct pob_gt : - public std::binary_function { - pob_lt lt; - bool operator() (const pob *n1, const pob *n2) const - {return lt(n2, n1);} +struct pob_lt_proc : public std::binary_function { + bool operator() (const pob *pn1, const pob *pn2) const; }; -struct pob_ref_gt : - public std::binary_function { - pob_gt gt; - bool operator() (const pob_ref &n1, const pob_ref &n2) const - {return gt (n1.get (), n2.get ());} +struct pob_gt_proc : public std::binary_function { + bool operator() (const pob *n1, const pob *n2) const { + return pob_lt_proc()(n2, n1); + } }; /** @@ -767,36 +772,37 @@ public: class pob_queue { + + typedef std::priority_queue, pob_gt_proc> pob_queue_ty; pob_ref m_root; unsigned m_max_level; unsigned m_min_depth; - std::priority_queue, - pob_ref_gt> m_obligations; + pob_queue_ty m_data; public: pob_queue(): m_root(nullptr), m_max_level(0), m_min_depth(0) {} ~pob_queue(); void reset(); - pob * top (); - void pop () {m_obligations.pop ();} + pob* top(); + void pop() {m_data.pop ();} void push (pob &n); void inc_level () { - SASSERT (!m_obligations.empty () || m_root); + SASSERT (!m_data.empty () || m_root); m_max_level++; m_min_depth++; - if (m_root && m_obligations.empty()) { m_obligations.push(m_root); } + if (m_root && m_data.empty()) { m_data.push(m_root.get()); } } pob& get_root() const {return *m_root.get ();} void set_root(pob& n); - bool is_root (pob& n) const {return m_root.get () == &n;} + bool is_root(pob& n) const {return m_root.get () == &n;} unsigned max_level() const {return m_max_level;} unsigned min_depth() const {return m_min_depth;} - size_t size() const {return m_obligations.size();} + size_t size() const {return m_data.size();} }; @@ -910,7 +916,6 @@ class context { bool m_use_ctp; bool m_use_inc_clause; bool m_blast_term_ite; - bool m_reuse_pobs; bool m_use_ind_gen; bool m_use_array_eq_gen; bool m_validate_lemmas; @@ -1007,7 +1012,6 @@ public: bool use_ctp() {return m_use_ctp;} bool use_inc_clause() {return m_use_inc_clause;} bool blast_term_ite() {return m_blast_term_ite;} - bool reuse_pobs() {return m_reuse_pobs;} bool elim_aux() {return m_elim_aux;} bool reach_dnf() {return m_reach_dnf;}