mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
Pobs are always managed
Removed options to allow unmanaged pobs. Other minor cleanups.
This commit is contained in:
parent
1910b4c87c
commit
c00c6b4285
|
@ -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)'),
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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, 1> 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<expr, pob_buffer > 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<const pob*, const pob*, bool>
|
||||
{bool operator() (const pob *pn1, const pob *pn2) const;};
|
||||
|
||||
struct pob_gt :
|
||||
public std::binary_function<const pob*, const pob*, bool> {
|
||||
pob_lt lt;
|
||||
bool operator() (const pob *n1, const pob *n2) const
|
||||
{return lt(n2, n1);}
|
||||
struct pob_lt_proc : public std::binary_function<const pob*, const pob*, bool> {
|
||||
bool operator() (const pob *pn1, const pob *pn2) const;
|
||||
};
|
||||
|
||||
struct pob_ref_gt :
|
||||
public std::binary_function<const pob_ref&, const model_ref &, bool> {
|
||||
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<const pob*, const pob*, bool> {
|
||||
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*, std::vector<pob*>, pob_gt_proc> pob_queue_ty;
|
||||
pob_ref m_root;
|
||||
unsigned m_max_level;
|
||||
unsigned m_min_depth;
|
||||
|
||||
std::priority_queue<pob_ref, std::vector<pob_ref>,
|
||||
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;}
|
||||
|
||||
|
|
Loading…
Reference in a new issue