mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Use vector instead of a hashtable to represent a set

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-07 09:45:17 -07:00
parent e84ca25f05
commit c5fb1c1223
2 changed files with 33 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/muz/spacer/spacer_proof_utils.cpp
View file

@ -229,29 +229,43 @@ void hypothesis_reducer::compute_hypsets(proof *pr) {
m_visited.mark(p);
// create active_hyps-set and parent_hyps-set for step p
proof_set* active_hyps = alloc(proof_set);
m_pinned_active_hyps.insert(active_hyps);
m_active_hyps.insert(p, active_hyps);
proof_ptr_vector* active_hyps = nullptr;
// fill both sets
if (m.is_hypothesis(p)) {
active_hyps->insert(p);
// create active_hyps-set for step p
proof_ptr_vector* active_hyps = alloc(proof_ptr_vector);
m_pinned_active_hyps.insert(active_hyps);
m_active_hyps.insert(p, active_hyps);
active_hyps->push_back(p);
m_open_mark.mark(p);
m_hyp_mark.mark(m.get_fact(p));
continue;
}
else {
for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
proof* parent = m.get_parent(p, i);
if (!m.is_lemma(p)) {
// lemmas clear all hypotheses
set_union(*active_hyps, *m_active_hyps.find(parent));
m_open_mark.mark(p, !active_hyps->empty());
ast_fast_mark1 seen;
active_hyps = alloc(proof_ptr_vector);
for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
proof* parent = m.get_parent(p, i);
// lemmas clear all hypotheses above them
if (m.is_lemma(p)) continue;
for (auto *x : *m_active_hyps.find(parent)) {
if (!seen.is_marked(x)) {
seen.mark(x);
active_hyps->push_back(x);
m_open_mark.mark(p);
}
}
}
if (active_hyps->empty()) {
dealloc(active_hyps);
m_active_hyps.insert(p, &m_empty_vector);
}
else {
m_pinned_active_hyps.push_back(active_hyps);
m_active_hyps.insert(p, active_hyps);
}
}
}
@ -404,7 +418,7 @@ proof* hypothesis_reducer::mk_lemma_core(proof* premise, expr *fact) {
SASSERT(m.is_false(m.get_fact(premise)));
SASSERT(m_active_hyps.contains(premise));
proof_set* active_hyps = m_active_hyps.find(premise);
proof_ptr_vector* active_hyps = m_active_hyps.find(premise);
// if there is no active hypothesis return the premise
if (!m_open_mark.is_marked(premise)) {

9
src/muz/spacer/spacer_proof_utils.h
View file

@ -57,16 +57,17 @@ public:
proof_ref reduce(proof* pf);
private:
typedef obj_hashtable<expr> expr_set;
typedef obj_hashtable<proof> proof_set;
typedef ptr_vector<proof> proof_ptr_vector;
ast_manager &m;
proof_ptr_vector m_empty_vector;
// created expressions
expr_ref_vector m_pinned;
// created sets of active hypothesis
ptr_vector<proof_set> m_pinned_active_hyps;
ptr_vector<proof_ptr_vector> m_pinned_active_hyps;
// maps a proof to the transformed proof
obj_map<proof, proof*> m_cache;
@ -75,7 +76,7 @@ private:
obj_map<expr, proof*> m_units;
// maps a proof node to the set of its active (i.e., in scope) hypotheses
obj_map<proof, proof_set*> m_active_hyps;
obj_map<proof, proof_ptr_vector*> m_active_hyps;
/// marks if an expression is ever used as a hypothesis in a proof
expr_mark m_hyp_mark;