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

proof_utils: use expr_mark instead of hashtable

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-07 08:50:31 -07:00
parent 2a6b694373
commit a40e0dce0c
2 changed files with 18 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -202,6 +202,8 @@ void hypothesis_reducer::reset() {
m_pinned_active_hyps.reset(); m_pinned_active_hyps.reset();
m_pinned.reset(); m_pinned.reset();
m_hyp_mark.reset(); m_hyp_mark.reset();
m_open_mark.reset();
m_visited.reset();
} }
void hypothesis_reducer::compute_hypsets(proof *pr) { void hypothesis_reducer::compute_hypsets(proof *pr) {
@ -211,8 +213,7 @@ void hypothesis_reducer::compute_hypsets(proof *pr) {
while (!todo.empty()) { while (!todo.empty()) {
proof* p = todo.back(); proof* p = todo.back();
if (m_active_hyps.contains(p)) { if (m_visited.is_marked(p)) {
SASSERT(m_parent_hyps.contains(p));
todo.pop_back(); todo.pop_back();
continue; continue;
} }
@ -222,15 +223,15 @@ void hypothesis_reducer::compute_hypsets(proof *pr) {
SASSERT(m.is_proof(p->get_arg(i))); SASSERT(m.is_proof(p->get_arg(i)));
proof *parent = to_app(p->get_arg(i)); proof *parent = to_app(p->get_arg(i));
if (!m_active_hyps.contains(parent)) { if (!m_visited.is_marked(parent))
SASSERT(!m_parent_hyps.contains(parent));
todo.push_back(parent); todo.push_back(parent);
}
} }
if (todo.size() > todo_sz) continue; if (todo.size() > todo_sz) continue;
todo.pop_back(); todo.pop_back();
m_visited.mark(p);
// create active_hyps-set and parent_hyps-set for step p // create active_hyps-set and parent_hyps-set for step p
proof_set* active_hyps = alloc(proof_set); proof_set* active_hyps = alloc(proof_set);
m_pinned_active_hyps.insert(active_hyps); m_pinned_active_hyps.insert(active_hyps);
@ -243,6 +244,8 @@ void hypothesis_reducer::compute_hypsets(proof *pr) {
// fill both sets // fill both sets
if (m.is_hypothesis(p)) { if (m.is_hypothesis(p)) {
active_hyps->insert(p); active_hyps->insert(p);
m_open_mark.mark(p);
parent_hyps->insert(m.get_fact(p)); parent_hyps->insert(m.get_fact(p));
m_hyp_mark.mark(m.get_fact(p)); m_hyp_mark.mark(m.get_fact(p));
} }
@ -251,9 +254,11 @@ void hypothesis_reducer::compute_hypsets(proof *pr) {
proof* parent = m.get_parent(p, i); proof* parent = m.get_parent(p, i);
set_union(*parent_hyps, *m_parent_hyps.find(parent)); set_union(*parent_hyps, *m_parent_hyps.find(parent));
if (!m.is_lemma(p)) if (!m.is_lemma(p)) {
// lemmas clear all hypotheses // lemmas clear all hypotheses
set_union(*active_hyps, *m_active_hyps.find(parent)); set_union(*active_hyps, *m_active_hyps.find(parent));
m_open_mark.mark(p, !active_hyps->empty());
}
} }
} }
} }
@ -267,12 +272,9 @@ void hypothesis_reducer::collect_units(proof* pr) {
while (pit.hasNext()) { while (pit.hasNext()) {
proof* p = pit.next(); proof* p = pit.next();
if (!m.is_hypothesis(p)) { if (!m.is_hypothesis(p)) {
proof_set* active_hyps = m_active_hyps.find(p);
SASSERT(active_hyps);
// collect units that are hyp-free and are used as // collect units that are hyp-free and are used as
// hypotheses in the proof pr // hypotheses in the proof pr
if (active_hyps->empty() && m.has_fact(p) && if (!m_open_mark.is_marked(p) && m.has_fact(p) &&
m_hyp_mark.is_marked(m.get_fact(p))) m_hyp_mark.is_marked(m.get_fact(p)))
m_units.insert(m.get_fact(p), p); m_units.insert(m.get_fact(p), p);
} }
@ -383,9 +385,7 @@ proof* hypothesis_reducer::reduce_core(proof* pf) {
m_cache.insert(p, res); m_cache.insert(p, res);
// bail out as soon as found a sub-proof of false // bail out as soon as found a sub-proof of false
SASSERT(m_active_hyps.contains(res)); if (!m_open_mark.is_marked(res) && m.has_fact(res) && m.is_false(m.get_fact(res)))
proof_set* active_hyps = m_active_hyps.find(res);
if (active_hyps->empty() && m.has_fact(res) && m.is_false(m.get_fact(res)))
return res; return res;
} }
UNREACHABLE(); UNREACHABLE();
@ -399,7 +399,7 @@ proof* hypothesis_reducer::mk_lemma_core(proof* premise, expr *fact) {
proof_set* active_hyps = m_active_hyps.find(premise); proof_set* active_hyps = m_active_hyps.find(premise);
// if there is no active hypothesis return the premise // if there is no active hypothesis return the premise
if (active_hyps->empty()) { if (!m_open_mark.is_marked(premise)) {
// XXX just in case premise might go away // XXX just in case premise might go away
m_pinned.push_back(premise); m_pinned.push_back(premise);
return premise; return premise;

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

@ -84,7 +84,11 @@ private:
// during proof transformation // during proof transformation
obj_map<proof, expr_set*> m_parent_hyps; obj_map<proof, expr_set*> m_parent_hyps;
/// marks if an expression is ever used as a hypothesis in a proof
expr_mark m_hyp_mark; expr_mark m_hyp_mark;
/// marks a proof as open, i.e., has a non-discharged hypothesis as ancestor
expr_mark m_open_mark;
expr_mark m_visited;
void reset(); void reset();